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

# wlar0 = # wlar, # apebs = # wlar, # apebs1 = # wlar, avhdr.leb = VTBL_LNUM, avhdr.vol = VTBL_VOLID, apebs1[vtblpnum1] = mkpeb(aehdr0, avhdr0, buf, align↑(datasize(buf, LEB_SIZE), EB_PAGE_SIZE), boolvar), wlar[vtblpnum1] = wl-entry(m0, free), wlar[vtblpnum4] = wl-entry(m1, used), apebs[vtblpnum1] = mkpeb(aehdr, empty, mkempbuf(LEB_SIZE), 0, false), apebs[vtblpnum4] = mkpeb(aehdr1, avhdr, buf, m3, false), vtblpnum ≠ vtblpnum4, vtblpnum4 ≠ vtblpnum1, aehdr.valid?, vtblpnum1 < # wlar, vtblpnum4 < # wlar, bflipset-cons(bflipset0, wlar), bflipset-cons(bflipset, wlar), bflipset-cons(bflipset1, wlar0), id(apebs1, apebs, mapped-pebs(vols)), id○(apebs1, apebs, vtblpnum1), is-aligned(LEB_SIZE, EB_PAGE_SIZE), ubi-io-inv(apebs), ubi-io-inv(apebs1), ubi-io-peb-inv(mkpeb(aehdr0, avhdr0, buf, align↑(datasize(buf, LEB_SIZE), EB_PAGE_SIZE), boolvar)), ubi-io-peb-inv(mkpeb(aehdr1, avhdr, buf, m3, false)), unique-sqns(apebs), unique-sqns(apebs1), valid-ebatbl(apebs1, wlar0, vols, vtblpnum), valid-ebatbl(apebs, wlar, vols, vtblpnum4), valid-eraseq(apebs, q), valid-eraseq(wlar, q), valid-eraseq(q), valid-eraseq(apebs1, q + eq-entry(vtblpnum4, VTBL_VOLID × VTBL_LNUM) '), valid-eraseq(wlar0, q + eq-entry(vtblpnum4, VTBL_VOLID × VTBL_LNUM) '), valid-eraseq(q + eq-entry(vtblpnum4, VTBL_VOLID × VTBL_LNUM) '), valid-global-sqn(apebs, sqnum), valid-global-sqn(apebs1, sqnum0), valid-peb(mkpeb(aehdr1, avhdr, buf, m3, false)), valid-vtbl(apebs1, vols, wlar0, vtblpnum), valid-vtbl(apebs, vols, wlar, vtblpnum4), valid-wl(apebs, wlar), valid-wl(apebs1, wlar0), ¬ vtblpnum4 ∈ q, ¬ VTBL_VOLID ∈ vols, ¬ vtblpnum ∈ q, bflipset = ∅ → m1 + WL_THRESHOLD ≤ m0, ∀ v, m. ¬ v ∈ vols ∧ is-encoded(to-vtbl(vols)[v, m], buf) → valid-ebatbl(apebs1, wlar0, vols[v, fill(mkebatbl(m), unmapped)], vtblpnum) ∧ valid-vtbl(apebs1, vols[v, fill(mkebatbl(m), unmapped)], wlar0, vtblpnum) ⊦ ⟪ubi_erase_worker_helper#(vtblpnum4; wlar0, apebs1; err); q1 := q + eq-entry(vtblpnum4, VTBL_VOLID × VTBL_LNUM) '; if err = ESUCCESS then q1 := q1.butlast⟫ ( # apebs1 = # wlar0 ∧ unique-sqns(apebs1) ∧ valid-global-sqn(apebs1, sqnum0) ∧ valid-wl(apebs1, wlar0) ∧ valid-eraseq(q1) ∧ valid-eraseq(wlar0, q1) ∧ valid-eraseq(apebs1, q1) ∧ bflipset-cons(bflipset1, wlar0) ∧ valid-ebatbl(apebs1, wlar0, vols, vtblpnum) ∧ valid-vtbl(apebs1, vols, wlar0, vtblpnum) ∧ ubi-io-inv(apebs1) ∧ ( id(apebs1, apebs, mapped-pebs(vols)) ∧ q1.lebrefs ⊆ q.lebrefs ++ (VTBL_VOLID × VTBL_LNUM) ∨ (∃ v, m, n. v ∈ vols ∧ m < # vols[v] ∧ vols[v][m] ≠ unmapped ∧ vols = vols[v, vols[v][m, ⌜n⌝ ]] ∧ id(apebs1, apebs, mapped-pebs(vols) -- vols[v][m].pnum) ∧ apebs1[n].data = apebs[vols[v][m].pnum].data ∧ apebs1[n].fill ≤ apebs[vols[v][m].pnum].fill ∧ q1.lebrefs ⊆ q.lebrefs ++ (v × m))))

User applied rule insert program lemma

And obtained the following new goals

Proof step 144:
ubi-cons(apebs, vols, wlar, q0 + eq-entry(m, lref) ' + q1, bflipset, vtblpnum, sqnum), m < # wlar, ubi-io-inv(apebs), wlar = wlar0, apebs = apebs0 ⊦ ⟪ubi_erase_worker_helper#(m; wlar, apebs; err)⟫ ( (err = ESUCCESS → ubi-cons(apebs, vols, wlar, q0 + q1, bflipset, vtblpnum, sqnum)) ∧ (err ≠ ESUCCESS → ubi-cons(apebs, vols, wlar, q0 + eq-entry(m, lref) ' + q1, bflipset, vtblpnum, sqnum)) ∧ ubi-io-inv(apebs) ∧ wlar[m].status ≠ used ∧ (err = ESUCCESS ∨ ⌊err⌋ ) ∧ id○(wlar, wlar0, m) ∧ id○(apebs, apebs0, m) ∧ id(apebs, apebs0, mapped-pebs(vols)))
Proof step 145:
# apebs1 = # wlar, # apebs = # wlar, # wlar0 = # wlar, avhdr.leb = VTBL_LNUM, avhdr.vol = VTBL_VOLID, apebs[vtblpnum4] = mkpeb(aehdr1, avhdr, buf, m3, false), apebs[vtblpnum1] = mkpeb(aehdr, empty, mkempbuf(LEB_SIZE), 0, false), wlar[vtblpnum4] = 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), apebs1 = apebs1, apebs2 = apebs1, bflipset2 = bflipset1, lref0 = VTBL_VOLID × VTBL_LNUM, m2 = vtblpnum4, q2 = q, q3 = [], sqnum1 = sqnum0, vols0 = vols, vtblpnum0 = vtblpnum, wlar0 = wlar0, wlar1 = wlar0, aehdr.valid?, vtblpnum4 < # wlar, vtblpnum1 < # wlar, vtblpnum4 < # wlar0, bflipset-cons(bflipset1, wlar0), bflipset-cons(bflipset, wlar), bflipset-cons(bflipset0, wlar), id(apebs1, apebs, mapped-pebs(vols)), id○(apebs1, apebs, vtblpnum1), is-aligned(LEB_SIZE, EB_PAGE_SIZE), ubi-cons(apebs1, vols, wlar0, q + eq-entry(vtblpnum4, VTBL_VOLID × VTBL_LNUM) ' + [], bflipset1, vtblpnum, sqnum0), ubi-io-inv(apebs), ubi-io-inv(apebs1), ubi-io-peb-inv(mkpeb(aehdr1, avhdr, 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), valid-ebatbl(apebs, wlar, vols, vtblpnum4), valid-ebatbl(apebs1, wlar0, vols, vtblpnum), valid-eraseq(q + eq-entry(vtblpnum4, VTBL_VOLID × VTBL_LNUM) '), valid-eraseq(wlar0, q + eq-entry(vtblpnum4, VTBL_VOLID × VTBL_LNUM) '), valid-eraseq(apebs1, q + eq-entry(vtblpnum4, VTBL_VOLID × VTBL_LNUM) '), valid-eraseq(q), valid-eraseq(wlar, q), valid-eraseq(apebs, q), valid-global-sqn(apebs1, sqnum0), valid-global-sqn(apebs, sqnum), valid-peb(mkpeb(aehdr1, avhdr, buf, m3, false)), valid-vtbl(apebs, vols, wlar, vtblpnum4), valid-vtbl(apebs1, vols, wlar0, vtblpnum), valid-wl(apebs1, wlar0), valid-wl(apebs, wlar), bflipset = ∅ → m1 + WL_THRESHOLD ≤ m0, ∀ v, m. ¬ v ∈ vols ∧ is-encoded(to-vtbl(vols)[v, m], buf) → valid-ebatbl(apebs1, wlar0, vols[v, fill(mkebatbl(m), unmapped)], vtblpnum) ∧ valid-vtbl(apebs1, vols[v, fill(mkebatbl(m), unmapped)], wlar0, vtblpnum) ⊦ [ubi_erase_worker_helper#(vtblpnum4; wlar0, apebs1; err)] ( (err = ESUCCESS → ubi-cons(apebs1, vols0, wlar0, q2 + q3, bflipset2, vtblpnum0, sqnum1)) ∧ (err ≠ ESUCCESS → ubi-cons(apebs1, vols0, wlar0, q2 + eq-entry(m2, lref0) ' + q3, bflipset2, vtblpnum0, sqnum1)) ∧ ubi-io-inv(apebs1) ∧ wlar0[m2].status ≠ used ∧ (err = ESUCCESS ∨ ⌊err⌋ ) ∧ id○(wlar0, wlar1, m2) ∧ id○(apebs1, apebs2, m2) ∧ id(apebs1, apebs2, mapped-pebs(vols0)) → ⟪q1 := q + eq-entry(vtblpnum4, VTBL_VOLID × VTBL_LNUM) '; if err = ESUCCESS then q1 := q1.butlast⟫ ( # apebs1 = # wlar0 ∧ unique-sqns(apebs1) ∧ valid-global-sqn(apebs1, sqnum0) ∧ valid-wl(apebs1, wlar0) ∧ valid-eraseq(q1) ∧ valid-eraseq(wlar0, q1) ∧ valid-eraseq(apebs1, q1) ∧ bflipset-cons(bflipset1, wlar0) ∧ valid-ebatbl(apebs1, wlar0, vols, vtblpnum) ∧ valid-vtbl(apebs1, vols, wlar0, vtblpnum) ∧ ubi-io-inv(apebs1) ∧ ( id(apebs1, apebs, mapped-pebs(vols)) ∧ q1.lebrefs ⊆ q.lebrefs ++ (VTBL_VOLID × VTBL_LNUM) ∨ (∃ v, m, n. v ∈ vols ∧ m < # vols[v] ∧ vols[v][m] ≠ unmapped ∧ vols = vols[v, vols[v][m, ⌜n⌝ ]] ∧ id(apebs1, apebs, mapped-pebs(vols) -- vols[v][m].pnum) ∧ apebs1[n].data = apebs[vols[v][m].pnum].data ∧ apebs1[n].fill ≤ apebs[vols[v][m].pnum].fill ∧ q1.lebrefs ⊆ q.lebrefs ++ (v × m))))), vtblpnum = vtblpnum4, vtblpnum4 = vtblpnum1, vtblpnum4 ∈ q, VTBL_VOLID ∈ vols, vtblpnum ∈ q

Rule argument

spec: <toplevel> name: prepost-erase-worker-helper seq: ubi-cons (apebs, vols, wlar, q0 + eq-entry(m, lref) ' + q1, bflipset, vtblpnum, sqnum), m < # wlar, ubi-io-inv(apebs), wlar = wlar0, apebs = apebs0 ⊦ ⟪ubi_erase_worker_helper#(m; wlar, apebs; err)⟫ ( ( err = ESUCCESS → ubi-cons (apebs, vols, wlar, q0 + q1, bflipset, vtblpnum, sqnum)) ∧ ( err ≠ ESUCCESS → ubi-cons (apebs, vols, wlar, q0 + eq-entry(m, lref) ' + q1, bflipset, vtblpnum, sqnum)) ∧ ubi-io-inv(apebs) ∧ wlar[m].status ≠ used ∧ (err = ESUCCESS ∨ ⌊err⌋ ) ∧ id○(wlar, wlar0, m) ∧ id○(apebs, apebs0, m) ∧ id(apebs, apebs0, mapped-pebs(vols))) subst: [m, apebs, wlar, err, vols, q0, lref, q1, bflipset, vtblpnum, sqnum, wlar0, apebs0] → [vtblpnum4, apebs1, wlar0, err, vols, q, VTBL_VOLID × VTBL_LNUM, [], bflipset1, vtblpnum, sqnum0, wlar0, apebs1] flags: <all paths>

Additional information

Used simplifier rules: ⊦ q + [] = q; (s)%a: ⊦ (q + q0) + q1 = q + q0 + q1; from specification list[erasequeue-base]%⊦ ubi-cons(apebs, vols, wlar, q, bflipset, n0, n1) ↔ # apebs = # wlar ∧ unique-sqns(apebs) ∧ valid-global-sqn(apebs, n1) ∧ valid-wl(apebs, wlar) ∧ valid-eraseq(q) ∧ valid-eraseq(wlar, q) ∧ valid-eraseq(apebs, q) ∧ ¬ VTBL_VOLID ∈ vols ∧ bflipset-cons(bflipset, wlar) ∧ valid-ebatbl(apebs, wlar, vols, n0) ∧ valid-vtbl(apebs, vols, wlar, n0); (s)% ⊦ valid-vtbl(apebs, vols, wlar, n0) → n0 < # wlar; (ss)