[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 115 from proof inv-wl-worker (previous step)

# wlar2 = # wlar, # apebs0 = # wlar, # apebs = # wlar, # wlar0 = # wlar, # apebs1 = # wlar, apebs1[vtblpnum1] = mkpeb(aehdr0, avhdr0, buf, align↑(datasize(buf, LEB_SIZE), EB_PAGE_SIZE), boolvar), wlar[vtblpnum1] = wl-entry(m0, free), wlar[vtblpnum2] = wl-entry(m1, used), apebs[vtblpnum1] = mkpeb(aehdr, empty, mkempbuf(LEB_SIZE), 0, false), apebs[vtblpnum2] = mkpeb(aechdr(m1), avidhdr(v1, m4, valid-sqns(v, m, apebs).max, m6, m7), buf, m3, false), vols[v][m] = ⌜vtblpnum2⌝ , err = ESUCCESS, q1 = q + eq-entry(vtblpnum2, v × m) ', aehdr.valid?, vtblpnum2 < # wlar, m < # vols[v], vtblpnum1 < # wlar, bflipset-cons(bflipset0, wlar), bflipset-cons(bflipset, wlar), bflipset-cons(bflipset1, wlar0), id(apebs0, apebs, ((mapped-pebs(vols) -- vtblpnum2) ++ vtblpnum1) ∩ mapped-pebs(vols)), id(apebs1, apebs, mapped-pebs(vols)), id(apebs0, apebs1, (mapped-pebs(vols) -- vtblpnum2) ++ vtblpnum1), id(apebs0, apebs, mapped-pebs(vols) -- vtblpnum2 -- vtblpnum1), id○(apebs1, apebs, vtblpnum1), id○(apebs0, apebs1, vtblpnum2), id○(wlar2, wlar0, vtblpnum2), is-aligned(LEB_SIZE, EB_PAGE_SIZE), ubi-io-inv(apebs1), ubi-io-inv(apebs), ubi-io-inv(apebs0), ubi-io-peb-inv(mkpeb(aehdr0, avhdr0, buf, align↑(datasize(buf, LEB_SIZE), EB_PAGE_SIZE), boolvar)), ubi-io-peb-inv(mkpeb(aechdr(m1), avidhdr(v1, m4, valid-sqns(v, m, apebs).max, m6, m7), buf, m3, false)), unique-sqns(apebs), unique-sqns(apebs1), valid-ebatbl(apebs, wlar, vols, vtblpnum4), valid-ebatbl(apebs1, wlar0, vols[v, vols[v][m, ⌜vtblpnum1⌝ ]], vtblpnum), valid-eraseq(apebs, q), valid-eraseq(wlar, q), valid-eraseq(q), valid-eraseq(apebs1, q + eq-entry(vtblpnum2, v × m) '), valid-eraseq(wlar0, q + eq-entry(vtblpnum2, v × m) '), valid-eraseq(q + eq-entry(vtblpnum2, v × m) '), valid-global-sqn(apebs, sqnum), valid-global-sqn(apebs1, sqnum0), valid-peb(v, m, mkpeb(aechdr(m1), avidhdr(v1, m4, valid-sqns(v, m, apebs).max, m6, m7), buf, m3, false)), valid-peb(mkpeb(aechdr(m1), avidhdr(v1, m4, valid-sqns(v, m, apebs).max, m6, m7), buf, m3, false)), valid-vtbl(apebs1, vols, wlar0, vtblpnum), valid-vtbl(apebs, vols, wlar, vtblpnum4), valid-wl(apebs, wlar), valid-wl(apebs1, wlar0), v ∈ vols, err ≠ ESUCCESS → unique-sqns(apebs0) ∧ valid-global-sqn(apebs0, sqnum0) ∧ valid-wl(apebs0, wlar2) ∧ valid-eraseq(wlar2, q + eq-entry(vtblpnum2, v × m) ') ∧ valid-eraseq(apebs0, q + eq-entry(vtblpnum2, v × m) ') ∧ ¬ VTBL_VOLID ∈ vols[v, vols[v][m, ⌜vtblpnum1⌝ ]] ∧ bflipset-cons(bflipset1, wlar2) ∧ valid-ebatbl(apebs0, wlar2, vols[v, vols[v][m, ⌜vtblpnum1⌝ ]], vtblpnum) ∧ valid-vtbl(apebs0, vols, wlar2, vtblpnum), err = ESUCCESS → unique-sqns(apebs0) ∧ valid-global-sqn(apebs0, sqnum0) ∧ valid-wl(apebs0, wlar2) ∧ valid-eraseq(wlar2, q) ∧ valid-eraseq(apebs0, q) ∧ ¬ VTBL_VOLID ∈ vols[v, vols[v][m, ⌜vtblpnum1⌝ ]] ∧ bflipset-cons(bflipset1, wlar2) ∧ valid-ebatbl(apebs0, wlar2, vols[v, vols[v][m, ⌜vtblpnum1⌝ ]], vtblpnum) ∧ valid-vtbl(apebs0, vols, wlar2, vtblpnum), bflipset = ∅ → m1 + WL_THRESHOLD ≤ m0, err = ESUCCESS ∨ ⌊err⌋ ⊦ wlar2[vtblpnum2].status = used, q1 = [], vtblpnum = vtblpnum2, vtblpnum2 = vtblpnum4, vtblpnum4 = vtblpnum1, VTBL_VOLID ∈ vols, vtblpnum4 ∈ q, vtblpnum2 ∈ q, vtblpnum ∈ q, unique-sqns(apebs0) ∧ valid-global-sqn(apebs0, sqnum0) ∧ valid-wl(apebs0, wlar2) ∧ valid-eraseq(q1.butlast) ∧ valid-eraseq(wlar2, q1.butlast) ∧ valid-eraseq(apebs0, q1.butlast) ∧ bflipset-cons(bflipset1, wlar2) ∧ valid-ebatbl(apebs0, wlar2, vols[v, vols[v][m, ⌜vtblpnum1⌝ ]], vtblpnum) ∧ valid-vtbl(apebs0, vols, wlar2, vtblpnum) ∧ ( vols = vols[v, vols[v][m, ⌜vtblpnum1⌝ ]] ∧ id(apebs0, apebs, (mapped-pebs(vols) -- vtblpnum2) ++ vtblpnum1) ∧ q1.butlast.lebrefs ⊆ q.lebrefs ++ (VTBL_VOLID × VTBL_LNUM) ∨ (∃ v0, m2, n. v0 ∈ vols ∧ m2 < # vols[v0] ∧ vols[v0][m2] ≠ unmapped ∧ vols[v, vols[v][m, ⌜vtblpnum1⌝ ]] = vols[v0, vols[v0][m2, ⌜n⌝ ]] ∧ id(apebs0, apebs, mapped-pebs(vols) -- vols[v0][m2].pnum) ∧ apebs0[n].data = apebs[vols[v0][m2].pnum].data ∧ apebs0[n].fill ≤ apebs[vols[v0][m2].pnum].fill ∧ q1.butlast.lebrefs ⊆ q.lebrefs ++ (v0 × m2)))

Heuristic simplifier applied rule simplifier

And obtained the following new goals

Proof step 116:
# apebs1 = # wlar, # wlar0 = # wlar, # apebs = # wlar, # apebs0 = # wlar, # wlar2 = # wlar, vols[v][m] = ⌜vtblpnum2⌝ , apebs[vtblpnum2] = mkpeb(aechdr(m1), avidhdr(v1, m4, valid-sqns(v, m, apebs).max, m6, m7), buf, m3, false), apebs[vtblpnum1] = mkpeb(aehdr, empty, mkempbuf(LEB_SIZE), 0, false), wlar[vtblpnum2] = wl-entry(m1, used), wlar[vtblpnum1] = wl-entry(m0, free), apebs1[vtblpnum1] = mkpeb(aehdr0, avhdr0, buf, align↑(datasize(buf, LEB_SIZE), EB_PAGE_SIZE), boolvar), aehdr.valid?, vtblpnum1 < # wlar, m < # vols[v], vtblpnum2 < # wlar, bflipset-cons(bflipset1, wlar0), bflipset-cons(bflipset, wlar), bflipset-cons(bflipset0, wlar), bflipset-cons(bflipset1, wlar2), id(apebs0, apebs, mapped-pebs(vols) -- vtblpnum2 -- vtblpnum1), id(apebs0, apebs1, (mapped-pebs(vols) -- vtblpnum2) ++ vtblpnum1), id(apebs1, apebs, mapped-pebs(vols)), id(apebs0, apebs, ((mapped-pebs(vols) -- vtblpnum2) ++ vtblpnum1) ∩ mapped-pebs(vols)), id○(wlar2, wlar0, vtblpnum2), id○(apebs0, apebs1, vtblpnum2), id○(apebs1, apebs, vtblpnum1), is-aligned(LEB_SIZE, EB_PAGE_SIZE), ubi-io-inv(apebs0), ubi-io-inv(apebs), ubi-io-inv(apebs1), ubi-io-peb-inv(mkpeb(aechdr(m1), avidhdr(v1, m4, valid-sqns(v, m, apebs).max, m6, m7), buf, m3, false)), ubi-io-peb-inv(mkpeb(aehdr0, avhdr0, buf, align↑(datasize(buf, LEB_SIZE), EB_PAGE_SIZE), boolvar)), unique-sqns(apebs1), unique-sqns(apebs), unique-sqns(apebs0), valid-ebatbl(apebs1, wlar0, vols[v, vols[v][m, ⌜vtblpnum1⌝ ]], vtblpnum), valid-ebatbl(apebs, wlar, vols, vtblpnum4), valid-ebatbl(apebs0, wlar2, vols[v, vols[v][m, ⌜vtblpnum1⌝ ]], vtblpnum), valid-eraseq(q + eq-entry(vtblpnum2, v × m) '), valid-eraseq(wlar0, q + eq-entry(vtblpnum2, v × m) '), valid-eraseq(apebs1, q + eq-entry(vtblpnum2, v × m) '), valid-eraseq(q), valid-eraseq(wlar, q), valid-eraseq(apebs, q), valid-eraseq(wlar2, q), valid-eraseq(apebs0, q), valid-global-sqn(apebs1, sqnum0), valid-global-sqn(apebs, sqnum), valid-global-sqn(apebs0, sqnum0), valid-peb(mkpeb(aechdr(m1), avidhdr(v1, m4, valid-sqns(v, m, apebs).max, m6, m7), buf, m3, false)), valid-peb(v, m, mkpeb(aechdr(m1), avidhdr(v1, m4, valid-sqns(v, m, apebs).max, m6, m7), buf, m3, false)), valid-vtbl(apebs, vols, wlar, vtblpnum4), valid-vtbl(apebs1, vols, wlar0, vtblpnum), valid-vtbl(apebs0, vols, wlar2, vtblpnum), valid-wl(apebs1, wlar0), valid-wl(apebs, wlar), valid-wl(apebs0, wlar2), v ∈ vols, bflipset = ∅ → m1 + WL_THRESHOLD ≤ m0 ⊦ wlar2[vtblpnum2].status = used, vtblpnum = vtblpnum2, vtblpnum2 = vtblpnum4, vtblpnum4 = vtblpnum1, vtblpnum2 ∈ q, vtblpnum4 ∈ q, VTBL_VOLID ∈ vols, vtblpnum ∈ q, ∃ v0, m2, n. v0 ∈ vols ∧ m2 < # vols[v0] ∧ vols[v0][m2] ≠ unmapped ∧ vols[v, vols[v][m, ⌜vtblpnum1⌝ ]] = vols[v0, vols[v0][m2, ⌜n⌝ ]] ∧ id(apebs0, apebs, mapped-pebs(vols) -- vols[v0][m2].pnum) ∧ apebs0[n].data = apebs[vols[v0][m2].pnum].data ∧ apebs0[n].fill ≤ apebs[vols[v0][m2].pnum].fill, vols = vols[v, vols[v][m, ⌜vtblpnum1⌝ ]] ∧ id(apebs0, apebs, (mapped-pebs(vols) -- vtblpnum2) ++ vtblpnum1)

Rule argument

Additional information

Used simplifier rules: lf-vtbl-info: ⊦ valid-vtbl(apebs, vols, wlar, n) ∧ valid-eraseq(wlar, q) → ¬ n ∈ q;% ⊦ s0 ⊆ s0 ++ lref; (s)% ⊦ (q + eqent ').butlast = q; (s)% ⊦ v ∈ vols[v0, ebatbl] ↔ v = v0 ∨ v ∈ vols; (ws)%a: ⊦ (q + q0) + q1 = q + q0 + q1; from specification list[erasequeue-base]% ⊦ q + eqent ' ≠ []; (s)