[Imprint][Data Privacy Statement][E-Mail]

View long theorem info. View the proof. Back to main index. View the specification. View theorem base summary, View theorem base listing, the used properties by spec, the dependency list, the symbol table,

Proof step 35 from proof inv-change (previous step)

# apebs0 = # wlar0, # apebs = # wlar, # apebs1 = # wlar0, # wlar1 = # wlar0, q.head = eq-entry(m, lref), LEB_SIZE = n2 + n0, wlar0[vtblpnum] = wl-entry(m0, free), apebs1[vtblpnum] = mkpeb(aehdr, empty, mkempbuf(LEB_SIZE), 0, false), err = ESUCCESS, aehdr.valid?, vtblpnum < # wlar0, vtblpnum3 < # vols[v], bflipset-cons(bflipset0, wlar1), bflipset-cons(bflipset, wlar), bflipset-cons(bflipset, wlar0), id(apebs0, apebs, mapped-pebs(vols)), id(apebs0, apebs1, mapped-pebs(vols)), id(apebs1, apebs, mapped-pebs(vols)), id○(apebs0, apebs1, vtblpnum), is-aligned(n0, EB_PAGE_SIZE), ubi-io-inv(apebs0), ubi-io-inv(apebs1), ubi-io-inv(apebs), unique-sqns(apebs0), unique-sqns(apebs), unique-sqns(apebs1), valid-ebatbl(apebs, wlar, vols, vtblpnum4), valid-ebatbl(apebs1, wlar0, vols, vtblpnum4), valid-ebatbl(apebs0, wlar1, vols1, vtblpnum0), valid-eraseq(q0), valid-eraseq(wlar1, q0), valid-eraseq(apebs0, q0), valid-eraseq(q), valid-eraseq(wlar, q), valid-eraseq(apebs, q), valid-eraseq(q1), valid-eraseq(wlar0, q1), valid-eraseq(apebs1, q1), valid-global-sqn(apebs0, sqnum0), valid-global-sqn(apebs, sqnum), valid-global-sqn(apebs1, sqnum), valid-vtbl(apebs, vols, wlar, vtblpnum4), valid-vtbl(apebs1, vols, wlar0, vtblpnum4), valid-vtbl(apebs0, vols1, wlar1, vtblpnum0), valid-wl(apebs0, wlar1), valid-wl(apebs, wlar), valid-wl(apebs1, wlar0), v ∈ vols, n0 ≤ LEB_SIZE, n0 ≤ # buf, q1.lebrefs ⊆ q.lebrefs, err = ESUCCESS → apebs0[vtblpnum].fill = align↑(datasize(buf, n0), EB_PAGE_SIZE) ∧ apebs0[vtblpnum].data = subarray(buf, 0, n0) + mkempbuf(n2) ∧ q0.lebrefs ⊆ q1.lebrefs ++ (v × vtblpnum3), err ≠ ESUCCESS → q0.lebrefs = q1.lebrefs, err = ESUCCESS ∧ vols[v][vtblpnum3] ≠ unmapped → q0 = q1 + eq-entry(vols[v][vtblpnum3].pnum, v × vtblpnum3) ', err ≠ ESUCCESS → vols1 = vols, err = ESUCCESS → vols1 = vols[v, vols[v][vtblpnum3, ⌜vtblpnum⌝ ]], apebs = apebs1 ∧ wlar = wlar0 ∧ q = q1 ∨ id○(apebs, apebs1, vtblpnum) ∧ id○(wlar, wlar0, vtblpnum) ∧ q = eq-entry(vtblpnum, lref) ' + q1, err = ESUCCESS ∨ ⌊err⌋ ⊦ vtblpnum4 = vtblpnum, vtblpnum0 ∈ q0, VTBL_VOLID ∈ vols1, vtblpnum4 ∈ q, VTBL_VOLID ∈ vols, vtblpnum4 ∈ q1, (err = ESUCCESS ∨ ⌊err⌋ ) ∧ (err ≠ ESUCCESS → vols1 = vols ∧ q0.lebrefs ⊆ q.lebrefs) ∧ ( err = ESUCCESS → q0.lebrefs ⊆ q.lebrefs ++ (v × vtblpnum3) ∧ (∃ n. vols1 = vols[v, vols[v][vtblpnum3, ⌜n⌝ ]] ∧ apebs0[n].data = subarray(buf, 0, n0) + mkempbuf(n2) ∧ apebs0[n].fill = align↑(datasize(buf, n0), EB_PAGE_SIZE)))

Heuristic simplifier applied rule simplifier

And obtained the following new goals

Proof step 36:
# apebs0 = # wlar0, # apebs = # wlar, # apebs1 = # wlar0, # wlar1 = # wlar0, apebs0[vtblpnum].data = subarray(buf, 0, n0) + mkempbuf(n2), apebs0[vtblpnum].fill = align↑(datasize(buf, n0), EB_PAGE_SIZE), q.head = eq-entry(m, lref), LEB_SIZE = n2 + n0, wlar0[vtblpnum] = wl-entry(m0, free), apebs1[vtblpnum] = mkpeb(aehdr, empty, mkempbuf(LEB_SIZE), 0, false), aehdr.valid?, vtblpnum < # wlar0, vtblpnum3 < # vols[v], bflipset-cons(bflipset0, wlar1), bflipset-cons(bflipset, wlar), bflipset-cons(bflipset, wlar0), id(apebs0, apebs, mapped-pebs(vols)), id(apebs0, apebs1, mapped-pebs(vols)), id(apebs1, apebs, mapped-pebs(vols)), id○(apebs0, apebs1, vtblpnum), is-aligned(n0, EB_PAGE_SIZE), ubi-io-inv(apebs0), ubi-io-inv(apebs1), ubi-io-inv(apebs), unique-sqns(apebs0), unique-sqns(apebs), unique-sqns(apebs1), valid-ebatbl(apebs, wlar, vols, vtblpnum4), valid-ebatbl(apebs1, wlar0, vols, vtblpnum4), valid-ebatbl(apebs0, wlar1, vols[v, vols[v][vtblpnum3, ⌜vtblpnum⌝ ]], vtblpnum0), valid-eraseq(q0), valid-eraseq(wlar1, q0), valid-eraseq(apebs0, q0), valid-eraseq(q), valid-eraseq(wlar, q), valid-eraseq(apebs, q), valid-eraseq(q1), valid-eraseq(wlar0, q1), valid-eraseq(apebs1, q1), valid-global-sqn(apebs0, sqnum0), valid-global-sqn(apebs, sqnum), valid-global-sqn(apebs1, sqnum), valid-vtbl(apebs, vols, wlar, vtblpnum4), valid-vtbl(apebs1, vols, wlar0, vtblpnum4), valid-vtbl(apebs0, vols, wlar1, vtblpnum0), valid-wl(apebs0, wlar1), valid-wl(apebs, wlar), valid-wl(apebs1, wlar0), v ∈ vols, n0 ≤ LEB_SIZE, n0 ≤ # buf, q1.lebrefs ⊆ q.lebrefs, q0.lebrefs ⊆ q1.lebrefs ++ (v × vtblpnum3), q0.lebrefs ⊆ q.lebrefs ++ (v × vtblpnum3), vols[v][vtblpnum3] ≠ unmapped → q0 = q1 + eq-entry(vols[v][vtblpnum3].pnum, v × vtblpnum3) ', apebs = apebs1 ∧ wlar = wlar0 ∧ q = q1 ∨ id○(apebs, apebs1, vtblpnum) ∧ id○(wlar, wlar0, vtblpnum) ∧ q = eq-entry(vtblpnum, lref) ' + q1 ⊦ vtblpnum4 = vtblpnum, vtblpnum0 ∈ q0, vtblpnum4 ∈ q, VTBL_VOLID ∈ vols, vtblpnum4 ∈ q1, ∃ n. vols[v, vols[v][vtblpnum3, ⌜vtblpnum⌝ ]] = vols[v, vols[v][vtblpnum3, ⌜n⌝ ]] ∧ apebs0[n].data = subarray(buf, 0, n0) + mkempbuf(n2) ∧ apebs0[n].fill = align↑(datasize(buf, n0), EB_PAGE_SIZE)

Rule argument

Additional information

Used simplifier rules: ⊦ s ⊆ s0 → s ++ lref ⊆ s0 ++ lref; (s)%sub-ntrans: ⊦ s2 ⊆ s3 ∧ ¬ s2 ⊆ s4 → ¬ s3 ⊆ s4; (forward) from specification set-basic[lebrefset]% ⊦ v ∈ vols[v0, ebatbl] ↔ v = v0 ∨ v ∈ vols; (ws)%⊦ v ∈ vols → ( valid-vtbl(apebs, vols[v, vols[v][m, ebae]], wlar, n0) ↔ valid-vtbl(apebs, vols, wlar, n0)); (s)