[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 85 from proof prepost-write-once (previous step)

# apebs2 = # wlar0, # apebs0 = # wlar, q0.head = eq-entry(m4, lref), LEB_SIZE = (n0 + m1) + m0, apebs2[vtblpnum1] = mkpeb(aehdr, empty, mkempbuf(LEB_SIZE), 0, false), wlar0[vtblpnum1] = wl-entry(m5, free), vols0[v][m] = unmapped, aehdr.valid?, vtblpnum1 < # wlar0, m < # vols0[v], bflipset-cons(bflipset, wlar0), bflipset-cons(bflipset, wlar), id(apebs2, apebs0, mapped-pebs(vols0)), is-aligned(m0, EB_PAGE_SIZE), is-aligned(m1, EB_PAGE_SIZE), ubi-io-inv(apebs2), ubi-io-inv(apebs0), ubi-io-inv(apebs2[vtblpnum1, mkpeb(aehdr, avidhdr(v, m, sqnum, 0, 0), mkempbuf(LEB_SIZE), 0, false)]), ubi-io-inv(apebs2[vtblpnum1, mkpeb(aehdr, avidhdr(v, m, sqnum, 0, 0), mkempbuf(m0) + subarray(buf, m2, m1) + mkempbuf(n0), m0 + m1, false)]), unique-sqns(apebs2), unique-sqns(apebs0), valid-ebatbl(apebs2, wlar0, vols0, vtblpnum2), valid-ebatbl(apebs0, wlar, vols0, vtblpnum2), valid-eraseq(apebs2, q1), valid-eraseq(wlar0, q1), valid-eraseq(q1), valid-eraseq(q0), valid-eraseq(wlar, q0), valid-eraseq(apebs0, q0), valid-global-sqn(apebs2, sqnum), valid-global-sqn(apebs0, sqnum), valid-vtbl(apebs2, vols0, wlar0, vtblpnum2), valid-vtbl(apebs0, vols0, wlar, vtblpnum2), valid-wl(apebs2, wlar0), valid-wl(apebs0, wlar), v ∈ vols0, m0 + m1 ≤ LEB_SIZE, m1 + m2 ≤ # buf, m1 ≤ LEB_SIZE, m2 + m1 ≤ # buf, m0 ≤ LEB_SIZE, m1 + m0 ≤ LEB_SIZE, q1.lebrefs ⊆ q0.lebrefs, apebs0 = apebs2 ∧ wlar = wlar0 ∧ q0 = q1 ∨ id○(apebs0, apebs2, vtblpnum1) ∧ id○(wlar, wlar0, vtblpnum1) ∧ q0 = eq-entry(vtblpnum1, lref) ' + q1 ⊦ m1 = 0, vtblpnum2 = vtblpnum1, valid-peb(mkpeb(aehdr, avidhdr(v, m, sqnum, 0, 0), subarray(mkempbuf(LEB_SIZE), 0, m0) + subarray(buf, m2, m1) + mkempbuf(n0), m0 + m1, false)), vtblpnum2 ∈ q1, VTBL_VOLID ∈ vols0, vtblpnum2 ∈ q0, unique-sqns(apebs2[vtblpnum1, mkpeb(aehdr, avidhdr(v, m, sqnum, 0, 0), mkempbuf(m0) + subarray(buf, m2, m1) + mkempbuf(n0), m0 + m1, false)]) ∧ valid-global-sqn (apebs2[vtblpnum1, mkpeb(aehdr, avidhdr(v, m, sqnum, 0, 0), mkempbuf(m0) + subarray(buf, m2, m1) + mkempbuf(n0), m0 + m1, false)], sqnum + 1) ∧ valid-wl (apebs2[vtblpnum1, mkpeb(aehdr, avidhdr(v, m, sqnum, 0, 0), mkempbuf(m0) + subarray(buf, m2, m1) + mkempbuf(n0), m0 + m1, false)], wlar0[vtblpnum1, wl-entry(m5, used)]) ∧ valid-eraseq(wlar0[vtblpnum1, wl-entry(m5, used)], q1) ∧ valid-eraseq(apebs2[vtblpnum1, mkpeb(aehdr, avidhdr(v, m, sqnum, 0, 0), mkempbuf(m0) + subarray(buf, m2, m1) + mkempbuf(n0), m0 + m1, false)], q1) ∧ valid-ebatbl (apebs2[vtblpnum1, mkpeb(aehdr, avidhdr(v, m, sqnum, 0, 0), mkempbuf(m0) + subarray(buf, m2, m1) + mkempbuf(n0), m0 + m1, false)], wlar0[vtblpnum1, wl-entry(m5, used)], vols0[v, vols0[v][m, ⌜vtblpnum1⌝ ]], vtblpnum2) ∧ (∃ n. vols0[v, vols0[v][m, ⌜vtblpnum1⌝ ]] = vols0[v, vols0[v][m, ⌜n⌝ ]] ∧ apebs2[vtblpnum1, mkpeb(aehdr, avidhdr(v, m, sqnum, 0, 0), mkempbuf(m0) + subarray(buf, m2, m1) + mkempbuf(n0), m0 + m1, false)][n].fill = m0 + m1 ∧ apebs2[vtblpnum1, mkpeb(aehdr, avidhdr(v, m, sqnum, 0, 0), mkempbuf(m0) + subarray(buf, m2, m1) + mkempbuf(n0), m0 + m1, false)][n].data = mkempbuf(m0) + subarray(buf, m2, m1) + mkempbuf(n0))

Heuristic simplifier applied rule simplifier

And obtained the following new goals

Proof step 86:
# apebs0 = # wlar, # apebs2 = # wlar0, q0.head = eq-entry(m4, lref), LEB_SIZE = (n0 + m1) + m0, vols0[v][m] = unmapped, wlar0[vtblpnum1] = wl-entry(m5, free), apebs2[vtblpnum1] = mkpeb(aehdr, empty, mkempbuf(LEB_SIZE), 0, false), aehdr.valid?, m < # vols0[v], vtblpnum1 < # wlar0, bflipset-cons(bflipset, wlar), bflipset-cons(bflipset, wlar0), id(apebs2, apebs0, mapped-pebs(vols0)), is-aligned(m1, EB_PAGE_SIZE), is-aligned(m0, EB_PAGE_SIZE), ubi-io-inv(apebs2[vtblpnum1, mkpeb(aehdr, avidhdr(v, m, sqnum, 0, 0), mkempbuf(m0) + subarray(buf, m2, m1) + mkempbuf(n0), m0 + m1, false)]), ubi-io-inv(apebs2[vtblpnum1, mkpeb(aehdr, avidhdr(v, m, sqnum, 0, 0), mkempbuf(LEB_SIZE), 0, false)]), ubi-io-inv(apebs0), ubi-io-inv(apebs2), unique-sqns(apebs0), unique-sqns(apebs2), valid-ebatbl(apebs0, wlar, vols0, vtblpnum2), valid-ebatbl(apebs2, wlar0, vols0, vtblpnum2), valid-eraseq(apebs0, q0), valid-eraseq(wlar, q0), valid-eraseq(q0), valid-eraseq(q1), valid-eraseq(wlar0, q1), valid-eraseq(apebs2, q1), valid-global-sqn(apebs0, sqnum), valid-global-sqn(apebs2, sqnum), valid-vtbl(apebs0, vols0, wlar, vtblpnum2), valid-vtbl(apebs2, vols0, wlar0, vtblpnum2), valid-wl(apebs0, wlar), valid-wl(apebs2, wlar0), v ∈ vols0, m1 + m0 ≤ LEB_SIZE, m0 ≤ LEB_SIZE, m2 + m1 ≤ # buf, m1 ≤ LEB_SIZE, m1 + m2 ≤ # buf, m0 + m1 ≤ LEB_SIZE, q1.lebrefs ⊆ q0.lebrefs, apebs0 = apebs2 ∧ wlar = wlar0 ∧ q0 = q1 ∨ id○(apebs0, apebs2, vtblpnum1) ∧ id○(wlar, wlar0, vtblpnum1) ∧ q0 = eq-entry(vtblpnum1, lref) ' + q1 ⊦ m1 = 0, vtblpnum2 = vtblpnum1, valid-peb(v, m, mkpeb(aehdr, avidhdr(v, m, sqnum, 0, 0), mkempbuf(m0) + subarray(buf, m2, m1) + mkempbuf(n0), m0 + m1, false)), vtblpnum2 ∈ q0, VTBL_VOLID ∈ vols0, vtblpnum2 ∈ q1, unique-sqns(apebs2[vtblpnum1, mkpeb(aehdr, avidhdr(v, m, sqnum, 0, 0), mkempbuf(m0) + subarray(buf, m2, m1) + mkempbuf(n0), m0 + m1, false)]) ∧ valid-global-sqn (apebs2[vtblpnum1, mkpeb(aehdr, avidhdr(v, m, sqnum, 0, 0), mkempbuf(m0) + subarray(buf, m2, m1) + mkempbuf(n0), m0 + m1, false)], sqnum + 1) ∧ valid-wl (apebs2[vtblpnum1, mkpeb(aehdr, avidhdr(v, m, sqnum, 0, 0), mkempbuf(m0) + subarray(buf, m2, m1) + mkempbuf(n0), m0 + m1, false)], wlar0[vtblpnum1, wl-entry(m5, used)]) ∧ valid-eraseq(wlar0[vtblpnum1, wl-entry(m5, used)], q1) ∧ valid-eraseq(apebs2[vtblpnum1, mkpeb(aehdr, avidhdr(v, m, sqnum, 0, 0), mkempbuf(m0) + subarray(buf, m2, m1) + mkempbuf(n0), m0 + m1, false)], q1) ∧ valid-ebatbl (apebs2[vtblpnum1, mkpeb(aehdr, avidhdr(v, m, sqnum, 0, 0), mkempbuf(m0) + subarray(buf, m2, m1) + mkempbuf(n0), m0 + m1, false)], wlar0[vtblpnum1, wl-entry(m5, used)], vols0[v, vols0[v][m, ⌜vtblpnum1⌝ ]], vtblpnum2) ∧ (∃ n. vols0[v, vols0[v][m, ⌜vtblpnum1⌝ ]] = vols0[v, vols0[v][m, ⌜n⌝ ]] ∧ apebs2[vtblpnum1, mkpeb(aehdr, avidhdr(v, m, sqnum, 0, 0), mkempbuf(m0) + subarray(buf, m2, m1) + mkempbuf(n0), m0 + m1, false)][n].fill = m0 + m1 ∧ apebs2[vtblpnum1, mkpeb(aehdr, avidhdr(v, m, sqnum, 0, 0), mkempbuf(m0) + subarray(buf, m2, m1) + mkempbuf(n0), m0 + m1, false)][n].data = mkempbuf(m0) + subarray(buf, m2, m1) + mkempbuf(n0))

Rule argument

Additional information

Used simplifier rules: ⊦ valid-peb (mkpeb(aehdr, avidhdr(v, m, n, n0, n2), buf, n1, boolvar)) ↔ valid-peb (v, m, mkpeb(aehdr, avidhdr(v, m, n, n0, n2), buf, n1, boolvar)); (ss)%append-a: ⊦ (buf + buf0) + buf1 = buf + buf0 + buf1; from specification array-splice[buffer]% ⊦ n1 ≤ n0 → subarray(mkempbuf(n0), 0, n1) = mkempbuf(n1); (s)