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

# wlar1 = # wlar0, # apebs1 = # wlar0, # apebs0 = # wlar0, UBI_ERASE_RETRIES = n0 + vtblpnum2, apebs1[m] = mkpeb(aehdr0, avhdr, buf, m2, false), wlar1[m] = wl-entry(m3, 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), ubi-io-inv(apebs0), ubi-io-inv(apebs1[m, mkpeb(empty, empty, mkempbuf(LEB_SIZE), 0, false)]), ubi-io-inv(apebs1[m, mkpeb(aechdr(m3 + 1), empty, mkempbuf(LEB_SIZE), 0, false)]), ubi-io-peb-inv(mkpeb(aehdr0, 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 ⊦ err1 = ESUCCESS, vtblpnum1 = m, VTBL_VOLID ∈ vols, vtblpnum1 ∈ q0, vtblpnum1 ∈ q1, valid-ebatbl(apebs1[m, mkpeb(aechdr(m3 + 1), empty, mkempbuf(LEB_SIZE), 0, false)], wlar1[m, wl-entry(m3 + 1, erasing)], vols, vtblpnum1) ∧ valid-eraseq(apebs1[m, mkpeb(aechdr(m3 + 1), empty, mkempbuf(LEB_SIZE), 0, false)], q0 + eq-entry(m, lref) ' + q1) ∧ valid-eraseq(wlar1[m, wl-entry(m3 + 1, erasing)], q0 + eq-entry(m, lref) ' + q1) ∧ valid-wl(apebs1[m, mkpeb(aechdr(m3 + 1), empty, mkempbuf(LEB_SIZE), 0, false)], wlar1[m, wl-entry(m3 + 1, erasing)]) ∧ valid-global-sqn(apebs1[m, mkpeb(aechdr(m3 + 1), empty, mkempbuf(LEB_SIZE), 0, false)], sqnum) ∧ unique-sqns(apebs1[m, mkpeb(aechdr(m3 + 1), empty, mkempbuf(LEB_SIZE), 0, false)])

User applied rule case distinction

And obtained the following new goals

Proof step 50:
# apebs0 = # wlar0, # apebs1 = # wlar0, # wlar1 = # wlar0, UBI_ERASE_RETRIES = n0 + vtblpnum2, wlar0[m] = wl-entry(m0, erasing), wlar1[m] = wl-entry(m3, erasing), apebs1[m] = mkpeb(aehdr0, 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(apebs1[m, mkpeb(aechdr(m3 + 1), empty, mkempbuf(LEB_SIZE), 0, false)]), ubi-io-inv(apebs1[m, mkpeb(empty, empty, mkempbuf(LEB_SIZE), 0, false)]), ubi-io-inv(apebs0), ubi-io-inv(apebs1), ubi-io-peb-inv(mkpeb(aehdr0, 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 ⊦ err1 = ESUCCESS, vtblpnum1 = m, valid-eraseq(apebs1[m, mkpeb(aechdr(m3 + 1), empty, mkempbuf(LEB_SIZE), 0, false)], q0 + eq-entry(m, lref) ' + q1), vtblpnum1 ∈ q1, vtblpnum1 ∈ q0, VTBL_VOLID ∈ vols
Proof step 53:
# apebs0 = # wlar0, # apebs1 = # wlar0, # wlar1 = # wlar0, UBI_ERASE_RETRIES = n0 + vtblpnum2, wlar0[m] = wl-entry(m0, erasing), wlar1[m] = wl-entry(m3, erasing), apebs1[m] = mkpeb(aehdr0, 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(apebs1[m, mkpeb(aechdr(m3 + 1), empty, mkempbuf(LEB_SIZE), 0, false)]), ubi-io-inv(apebs1[m, mkpeb(empty, empty, mkempbuf(LEB_SIZE), 0, false)]), ubi-io-inv(apebs0), ubi-io-inv(apebs1), ubi-io-peb-inv(mkpeb(aehdr0, 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 ⊦ err1 = ESUCCESS, vtblpnum1 = m, valid-wl(apebs1[m, mkpeb(aechdr(m3 + 1), empty, mkempbuf(LEB_SIZE), 0, false)], wlar1[m, wl-entry(m3 + 1, erasing)]), vtblpnum1 ∈ q1, vtblpnum1 ∈ q0, VTBL_VOLID ∈ vols
Proof step 56:
# apebs0 = # wlar0, # apebs1 = # wlar0, # wlar1 = # wlar0, UBI_ERASE_RETRIES = n0 + vtblpnum2, wlar0[m] = wl-entry(m0, erasing), wlar1[m] = wl-entry(m3, erasing), apebs1[m] = mkpeb(aehdr0, 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(apebs1[m, mkpeb(aechdr(m3 + 1), empty, mkempbuf(LEB_SIZE), 0, false)]), ubi-io-inv(apebs1[m, mkpeb(empty, empty, mkempbuf(LEB_SIZE), 0, false)]), ubi-io-inv(apebs0), ubi-io-inv(apebs1), ubi-io-peb-inv(mkpeb(aehdr0, 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 ⊦ err1 = ESUCCESS, vtblpnum1 = m, valid-global-sqn(apebs1[m, mkpeb(aechdr(m3 + 1), empty, mkempbuf(LEB_SIZE), 0, false)], sqnum), vtblpnum1 ∈ q1, vtblpnum1 ∈ q0, VTBL_VOLID ∈ vols

Rule argument

pos: right 6

Additional information

Used simplifier rules: ⊦ m < n ↔ ¬ n ≤ m; (ss)%a: ⊦ (q + q0) + q1 = q + q0 + q1; from specification list[erasequeue-base]% ⊦ 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)% ⊦ ¬ valid-peb(mkpeb(aehdr, empty, buf, m, boolvar)); (s)%⊦ wlar[m] = wl-entry(m0, stat) → ( valid-eraseq(wlar[m, wl-entry(m1, stat)], q) ↔ valid-eraseq(wlar, q)); (ss)% ⊦ 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)