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

# 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), m < # wlar0, bflipset-cons(bflipset, wlar1), bflipset-cons(bflipset, wlar0), id○(wlar1, wlar0, m), id○(apebs1, apebs0, m), ubi-io-inv(apebs1[m, mkpeb(aehdr0, avhdr0, buf0, m3, false)]), ubi-io-inv(apebs1), ubi-io-inv(apebs0), ubi-io-peb-inv(mkpeb(aehdr, avhdr, buf, m2, false)), ubi-io-peb-inv(mkpeb(aehdr0, avhdr0, buf0, m3, 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, ⌊err0⌋ ⊦ err1 = ESUCCESS, vtblpnum1 = m, avhdr0.valid?, vtblpnum1 ∈ q1, vtblpnum1 ∈ q0, VTBL_VOLID ∈ vols, unique-sqns(apebs1[m, mkpeb(aehdr0, avhdr0, buf0, m3, false)]) ∧ valid-global-sqn(apebs1[m, mkpeb(aehdr0, avhdr0, buf0, m3, false)], sqnum) ∧ valid-wl(apebs1[m, mkpeb(aehdr0, avhdr0, buf0, m3, false)], wlar1[m, wl-entry(m1 + 1, erasing)]) ∧ valid-eraseq(wlar1[m, wl-entry(m1 + 1, erasing)], q0 + eq-entry(m, lref) ' + q1) ∧ valid-eraseq(apebs1[m, mkpeb(aehdr0, avhdr0, buf0, m3, false)], q0 + eq-entry(m, lref) ' + q1) ∧ valid-ebatbl(apebs1[m, mkpeb(aehdr0, avhdr0, buf0, m3, false)], wlar1[m, wl-entry(m1 + 1, erasing)], vols, vtblpnum1)

User applied rule case distinction

And obtained the following new goals

Proof step 94:
# 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), m < # wlar0, bflipset-cons(bflipset, wlar0), bflipset-cons(bflipset, wlar1), id○(apebs1, apebs0, m), id○(wlar1, wlar0, m), ubi-io-inv(apebs0), ubi-io-inv(apebs1), ubi-io-inv(apebs1[m, mkpeb(aehdr0, avhdr0, buf0, m3, false)]), ubi-io-peb-inv(mkpeb(aehdr0, avhdr0, buf0, m3, false)), 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⌋ ⊦ err1 = ESUCCESS, vtblpnum1 = m, avhdr0.valid?, valid-global-sqn(apebs1[m, mkpeb(aehdr0, avhdr0, buf0, m3, false)], sqnum), VTBL_VOLID ∈ vols, vtblpnum1 ∈ q0, vtblpnum1 ∈ q1
Proof step 97:
# 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), m < # wlar0, bflipset-cons(bflipset, wlar0), bflipset-cons(bflipset, wlar1), id○(apebs1, apebs0, m), id○(wlar1, wlar0, m), ubi-io-inv(apebs0), ubi-io-inv(apebs1), ubi-io-inv(apebs1[m, mkpeb(aehdr0, avhdr0, buf0, m3, false)]), ubi-io-peb-inv(mkpeb(aehdr0, avhdr0, buf0, m3, false)), 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⌋ ⊦ err1 = ESUCCESS, vtblpnum1 = m, avhdr0.valid?, valid-wl(apebs1[m, mkpeb(aehdr0, avhdr0, buf0, m3, false)], wlar1[m, wl-entry(m1 + 1, erasing)]), VTBL_VOLID ∈ vols, vtblpnum1 ∈ q0, vtblpnum1 ∈ q1
Proof step 100:
# 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), m < # wlar0, bflipset-cons(bflipset, wlar0), bflipset-cons(bflipset, wlar1), id○(apebs1, apebs0, m), id○(wlar1, wlar0, m), ubi-io-inv(apebs0), ubi-io-inv(apebs1), ubi-io-inv(apebs1[m, mkpeb(aehdr0, avhdr0, buf0, m3, false)]), ubi-io-peb-inv(mkpeb(aehdr0, avhdr0, buf0, m3, false)), 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⌋ ⊦ err1 = ESUCCESS, vtblpnum1 = m, avhdr0.valid?, valid-eraseq(apebs1[m, mkpeb(aehdr0, avhdr0, buf0, m3, false)], q0 + eq-entry(m, lref) ' + q1), VTBL_VOLID ∈ vols, vtblpnum1 ∈ q0, vtblpnum1 ∈ q1

Rule argument

pos: right 7

Additional information

Used simplifier rules: ⊦ used ≠ erasing; (s)%stat ≠ used, stat0 ≠ used ⊦ wlar[m] = wl-entry(m0, stat) → ( valid-ebatbl(apebs, wlar[m, wl-entry(m1, stat0)], vols, n) ↔ valid-ebatbl(apebs, wlar, vols, n)); (ss)%stat ≠ used ⊦ wlar[m] = wl-entry(m0, stat) → ( valid-ebatbl(apebs[m, apeb], wlar, vols, n) ↔ valid-ebatbl(apebs, wlar, vols, n)); (ss)%⊦ wlar[m] = wl-entry(m0, stat) → ( valid-eraseq(wlar[m, wl-entry(m1, stat)], q) ↔ valid-eraseq(wlar, q)); (ss)%a: ⊦ (q + q0) + q1 = q + q0 + q1; from specification list[erasequeue-base]% ⊦ m < n ↔ ¬ n ≤ m; (ss)% ⊦ valid-eraseq(wlar, q0 + eq-entry(m, lref) ' + q1) → ¬ # wlar ≤ m; (s)%m < # apebs ⊦ unique-sqns(apebs) → ( unique-sqns(apebs[m, apeb]) ↔ ¬ valid-peb(apeb) ∨ ¬ apeb.vidhdr.sqn ∈ valid-sqns(apeb.vidhdr.vol, apeb.vidhdr.leb, apebs) \ (valid-peb(apeb.vidhdr.vol, apeb.vidhdr.leb, apebs[m]) ⊃ {apebs[m].vidhdr.sqn} ;∅ )); (ss)% ⊦ ¬ avhdr.valid? → ¬ valid-peb(mkpeb(aehdr, avhdr, buf, m, boolvar)); (s)