[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 61 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), apebs = apebs1[m, mkpeb(empty, empty, mkempbuf(LEB_SIZE), 0, false)], err = err0, vtblpnum = m, m < # apebs1, 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(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, ⌊err0⌋ ∨ err0 = ESUCCESS ⊦ ⟪apebs[vtblpnum].echdr := aehdr; 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:= (m3 + 1)]) ∧ valid-eraseq(wlar1[m, wlar1[m].ec:= (m3 + 1)], q0 + eq-entry(m, lref) ' + q1) ∧ valid-eraseq(apebs, q0 + eq-entry(m, lref) ' + q1) ∧ valid-ebatbl(apebs, wlar1[m, wlar1[m].ec:= (m3 + 1)], vols, vtblpnum1) ∧ valid-vtbl(apebs, vols, wlar1, vtblpnum1) ∧ ubi-io-inv(apebs) ∧ (err = ESUCCESS → apebs[m].echdr = aechdr(m3 + 1) ∧ apebs[m].vidhdr = empty ∧ ¬ apebs[m].bad) ∧ UBI_ERASE_RETRIES < n0 + vtblpnum), err = ESUCCESS, err1 = ESUCCESS, vtblpnum1 = m, aehdr.valid?, VTBL_VOLID ∈ vols, vtblpnum1 ∈ q0, vtblpnum1 ∈ q1

Heuristic symbolic execution applied rule assign right

And obtained the following new goals

Proof step 62:
# 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), apebs = apebs1[m, mkpeb(empty, empty, mkempbuf(LEB_SIZE), 0, false)], err = err0, vtblpnum = m, vtblpnum < # apebs, m < # wlar0, m < # apebs1, bflipset-cons(bflipset, wlar0), bflipset-cons(bflipset, wlar1), id○(apebs1, apebs0, m), id○(wlar1, wlar0, m), 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, ⌊err0⌋ ∨ err0 = ESUCCESS ⊦ ⟪vtblpnum0 := vtblpnum2 + 1⟫ ( vtblpnum0 ≤ UBI_ERASE_RETRIES + 1 ∧ m < # apebs[vtblpnum, apebs[vtblpnum].echdr:= aehdr] ∧ id○(apebs[vtblpnum, apebs[vtblpnum].echdr:= aehdr], apebs0, m) ∧ # apebs[vtblpnum, apebs[vtblpnum].echdr:= aehdr] = # wlar0 ∧ unique-sqns(apebs[vtblpnum, apebs[vtblpnum].echdr:= aehdr]) ∧ valid-global-sqn(apebs[vtblpnum, apebs[vtblpnum].echdr:= aehdr], sqnum) ∧ valid-wl(apebs[vtblpnum, apebs[vtblpnum].echdr:= aehdr], wlar1[m, wlar1[m].ec:= (m3 + 1)]) ∧ valid-eraseq(wlar1[m, wlar1[m].ec:= (m3 + 1)], q0 + eq-entry(m, lref) ' + q1) ∧ valid-eraseq(apebs[vtblpnum, apebs[vtblpnum].echdr:= aehdr], q0 + eq-entry(m, lref) ' + q1) ∧ valid-ebatbl(apebs[vtblpnum, apebs[vtblpnum].echdr:= aehdr], wlar1[m, wlar1[m].ec:= (m3 + 1)], vols, vtblpnum1) ∧ valid-vtbl(apebs[vtblpnum, apebs[vtblpnum].echdr:= aehdr], vols, wlar1, vtblpnum1) ∧ ubi-io-inv(apebs[vtblpnum, apebs[vtblpnum].echdr:= aehdr]) ∧ ( err = ESUCCESS → apebs[vtblpnum, apebs[vtblpnum].echdr:= aehdr][m].echdr = aechdr(m3 + 1) ∧ apebs[vtblpnum, apebs[vtblpnum].echdr:= aehdr][m].vidhdr = empty ∧ ¬ apebs[vtblpnum, apebs[vtblpnum].echdr:= aehdr][m].bad) ∧ UBI_ERASE_RETRIES < n0 + vtblpnum0), err = ESUCCESS, err1 = ESUCCESS, vtblpnum1 = m, aehdr.valid?, vtblpnum1 ∈ q1, vtblpnum1 ∈ q0, VTBL_VOLID ∈ vols

Rule argument

Additional information

Used simplifier rules: ⊦ ⌊err⌋ → err ≠ ESUCCESS; (s)% ⊦ # apebs[n, apeb] = # apebs; (s)