[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 33 from proof prepost-erase-worker-helper (previous step)

# apebs0 = # wlar0, # apebs1 = # wlar0, # wlar1 = # wlar0, UBI_ERASE_RETRIES = n0 + vtblpnum2, wlar0[m] = wl-entry(m0, erasing), wlar1[m] = wl-entry(m1, erasing), apebs1[m] = mkpeb(aehdr, avhdr, buf, m2, false), apebs = apebs1[m, mkpeb(empty, empty, mkempbuf(LEB_SIZE), 0, false)], err = err0, err = ESUCCESS, wlar = wlar1[m, wlar1[m].ec:= (wlar1[m].ec + 1)], m < # wlar1, m < # wlar0, m < # apebs1, bflipset-cons(bflipset, wlar0), bflipset-cons(bflipset, wlar1), id○(apebs1, apebs0, m), id○(wlar1, wlar0, m), ubi-io-inv(apebs), ubi-io-inv(apebs0), ubi-io-inv(apebs1), ubi-io-peb-inv(mkpeb(aehdr, avhdr, buf, m2, false)), unique-sqns(apebs0), unique-sqns(apebs1), valid-ebatbl(apebs0, wlar0, vols, vtblpnum1), valid-ebatbl(apebs1, wlar1, vols, vtblpnum1), valid-eraseq(q0 + eq-entry(m, lref) ' + q1), valid-eraseq(wlar0, q0 + eq-entry(m, lref) ' + q1), valid-eraseq(apebs0, q0 + eq-entry(m, lref) ' + q1), valid-eraseq(wlar1, q0 + eq-entry(m, lref) ' + q1), valid-eraseq(apebs1, q0 + eq-entry(m, lref) ' + q1), valid-global-sqn(apebs0, sqnum), valid-global-sqn(apebs1, sqnum), valid-vtbl(apebs0, vols, wlar0, vtblpnum1), valid-vtbl(apebs1, vols, wlar1, vtblpnum1), valid-wl(apebs0, wlar0), valid-wl(apebs1, wlar1), vtblpnum2 ≤ UBI_ERASE_RETRIES, vtblpnum2 ≤ UBI_ERASE_RETRIES + 1, ⌊err0⌋ ∨ err0 = ESUCCESS ⊦ ⟪aubi_io_write_echdr#(m, aechdr(wlar[m].ec); apebs; err); vtblpnum := vtblpnum2 + 1⟫ ( vtblpnum ≤ UBI_ERASE_RETRIES + 1 ∧ m < # apebs ∧ id○(apebs, apebs0, m) ∧ id○(wlar, wlar0, m) ∧ # apebs = # wlar ∧ unique-sqns(apebs) ∧ valid-global-sqn(apebs, sqnum) ∧ valid-wl(apebs, wlar) ∧ valid-eraseq(wlar, q0 + eq-entry(m, lref) ' + q1) ∧ valid-eraseq(apebs, q0 + eq-entry(m, lref) ' + q1) ∧ bflipset-cons(bflipset, wlar) ∧ valid-ebatbl(apebs, wlar, vols, vtblpnum1) ∧ valid-vtbl(apebs, vols, wlar, vtblpnum1) ∧ ubi-io-inv(apebs) ∧ (err = ESUCCESS → apebs[m].echdr = aechdr(wlar[m].ec) ∧ apebs[m].vidhdr = empty ∧ ¬ apebs[m].bad) ∧ UBI_ERASE_RETRIES < n0 + vtblpnum), err1 = ESUCCESS, vtblpnum1 = m, vtblpnum1 ∈ q1, vtblpnum1 ∈ q0, VTBL_VOLID ∈ vols

Heuristic simplifier applied rule simplifier

And obtained the following new goals

Proof step 34:
# wlar1 = # wlar0, # apebs1 = # wlar0, # apebs0 = # wlar0, UBI_ERASE_RETRIES = n0 + vtblpnum2, apebs1[m] = mkpeb(aehdr, avhdr, buf, m2, false), wlar1[m] = wl-entry(m1, erasing), wlar0[m] = wl-entry(m0, erasing), apebs = apebs1[m, mkpeb(empty, empty, mkempbuf(LEB_SIZE), 0, false)], err1 ≠ ESUCCESS, vtblpnum1 ≠ m, m < # wlar0, bflipset-cons(bflipset, wlar1), bflipset-cons(bflipset, wlar0), id○(wlar1, wlar0, m), id○(apebs1, apebs0, m), ubi-io-inv(apebs1), ubi-io-inv(apebs0), ubi-io-inv(apebs1[m, mkpeb(empty, empty, mkempbuf(LEB_SIZE), 0, false)]), ubi-io-peb-inv(mkpeb(aehdr, avhdr, buf, m2, false)), unique-sqns(apebs1), unique-sqns(apebs0), valid-ebatbl(apebs1, wlar1, vols, vtblpnum1), valid-ebatbl(apebs0, wlar0, vols, vtblpnum1), valid-eraseq(apebs1, q0 + eq-entry(m, lref) ' + q1), valid-eraseq(wlar1, q0 + eq-entry(m, lref) ' + q1), valid-eraseq(apebs0, q0 + eq-entry(m, lref) ' + q1), valid-eraseq(wlar0, q0 + eq-entry(m, lref) ' + q1), valid-eraseq(q0 + eq-entry(m, lref) ' + q1), valid-global-sqn(apebs1, sqnum), valid-global-sqn(apebs0, sqnum), valid-vtbl(apebs1, vols, wlar1, vtblpnum1), valid-vtbl(apebs0, vols, wlar0, vtblpnum1), valid-wl(apebs1, wlar1), valid-wl(apebs0, wlar0), vtblpnum2 ≤ UBI_ERASE_RETRIES + 1, vtblpnum2 ≤ UBI_ERASE_RETRIES, ¬ VTBL_VOLID ∈ vols, ¬ vtblpnum1 ∈ q0, ¬ vtblpnum1 ∈ q1 ⊦ ⟪aubi_io_write_echdr#(m, aechdr(wlar1[m, wlar1[m].ec:= (wlar1[m].ec + 1)][m].ec); apebs; err); vtblpnum := vtblpnum2 + 1⟫ ( vtblpnum ≤ UBI_ERASE_RETRIES + 1 ∧ m < # apebs ∧ id○(apebs, apebs0, m) ∧ # apebs = # wlar0 ∧ unique-sqns(apebs) ∧ valid-global-sqn(apebs, sqnum) ∧ valid-wl(apebs, wlar1[m, wlar1[m].ec:= (wlar1[m].ec + 1)]) ∧ valid-eraseq(wlar1[m, wlar1[m].ec:= (wlar1[m].ec + 1)], q0 + eq-entry(m, lref) ' + q1) ∧ valid-eraseq(apebs, q0 + eq-entry(m, lref) ' + q1) ∧ valid-ebatbl(apebs, wlar1[m, wlar1[m].ec:= (wlar1[m].ec + 1)], vols, vtblpnum1) ∧ valid-vtbl(apebs, vols, wlar1, vtblpnum1) ∧ ubi-io-inv(apebs) ∧ (err = ESUCCESS → apebs[m].echdr = aechdr(wlar1[m].ec + 1) ∧ apebs[m].vidhdr = empty ∧ ¬ apebs[m].bad) ∧ UBI_ERASE_RETRIES < n0 + vtblpnum)

Rule argument

Additional information

Used simplifier rules: a: ⊦ (q + q0) + q1 = q + q0 + q1; from specification list[erasequeue-base]%valid-eraseqp-in0: ⊦ valid-eraseq(wlar, q0 + eq-entry(n, lref) ' + q1) → wlar[n].status = erasing; (forward) from specification ubi-base%idexcept-size: ⊦ id○(wlar, wlar0, n) → # wlar = # wlar0; (forward) from specification array-copy[wlarray-base]%idexcept-size: ⊦ id○(apebs, apebs0, n) → # apebs = # apebs0; (forward) from specification array-copy[apebs]%lf-01: ⊦ m < n ∧ n = n0 → m < n0; (forward) from specification nat-basic% ⊦ (wle.ec:= m).ec = m; (s)% ⊦ m < # wlar → wlar[m, wle][m] = wle; (s)%⊦ m ≠ n0 → ( valid-vtbl(apebs, vols, wlar[m, wle], n0) ↔ valid-vtbl(apebs, vols, wlar, n0)); (s)%stat ≠ used ⊦ wlar[n] = wl-entry(m, stat) ∧ bflipset-cons(bflipset, wlar) → ¬ n ∈ bflipset; (s)%wle.status ≠ used ⊦ bflipset-cons(bflipset, wlar[m, wle]) ↔ bflipset-cons(bflipset, wlar) ∧ ¬ m ∈ bflipset; (s)% ⊦ used ≠ erasing; (s)% ⊦ wl-entry(m, stat).status = stat; (s)% ⊦ wl-entry(m, stat).ec:= m0 = wl-entry(m0, stat); (s)% ⊦ wl-entry(m, stat).ec = m; (s)% ⊦ # wlar[n, wle] = # wlar; (s)% ⊦ id○(wlar[n, wle], wlar0, n) ↔ id○(wlar, wlar0, n); (s)% ⊦ ¬ ⌊ESUCCESS⌋ ; (s)