[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 48 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 = ESUCCESS, err = err0, m < # apebs1, m < # wlar0, m < # apebs, 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 ⊦ err1 = ESUCCESS, vtblpnum1 = m, VTBL_VOLID ∈ vols, vtblpnum1 ∈ q0, vtblpnum1 ∈ q1, vtblpnum2 + 1 ≤ UBI_ERASE_RETRIES + 1 ∧ m < # apebs[m, apebs[m].echdr:= aechdr(m3 + 1)] ∧ id○(apebs[m, apebs[m].echdr:= aechdr(m3 + 1)], apebs0, m) ∧ # apebs[m, apebs[m].echdr:= aechdr(m3 + 1)] = # wlar0 ∧ unique-sqns(apebs[m, apebs[m].echdr:= aechdr(m3 + 1)]) ∧ valid-global-sqn(apebs[m, apebs[m].echdr:= aechdr(m3 + 1)], sqnum) ∧ valid-wl(apebs[m, apebs[m].echdr:= aechdr(m3 + 1)], 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[m, apebs[m].echdr:= aechdr(m3 + 1)], q0 + eq-entry(m, lref) ' + q1) ∧ valid-ebatbl(apebs[m, apebs[m].echdr:= aechdr(m3 + 1)], wlar1[m, wlar1[m].ec:= (m3 + 1)], vols, vtblpnum1) ∧ valid-vtbl(apebs[m, apebs[m].echdr:= aechdr(m3 + 1)], vols, wlar1, vtblpnum1) ∧ ubi-io-inv(apebs[m, apebs[m].echdr:= aechdr(m3 + 1)]) ∧ ( err = ESUCCESS → apebs[m, apebs[m].echdr:= aechdr(m3 + 1)][m].echdr = aechdr(m3 + 1) ∧ apebs[m, apebs[m].echdr:= aechdr(m3 + 1)][m].vidhdr = empty ∧ ¬ apebs[m, apebs[m].echdr:= aechdr(m3 + 1)][m].bad) ∧ UBI_ERASE_RETRIES < n0 + vtblpnum2 + 1

Heuristic simplifier applied rule simplifier

And obtained the following new goals

Proof step 49:
# 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)])

Rule argument

Additional information

Used simplifier rules: ⊦ ubi-io-peb-inv(mkpeb(aehdr, empty, mkempbuf(LEB_SIZE), 0, false)); (s)%⊦ ubi-io-inv(apebs) → ( ubi-io-inv(apebs[n, apeb]) ↔ n < # apebs ∧ ubi-io-peb-inv(apebs[n]) → ubi-io-peb-inv(apeb)); (ss)% ⊦ ¬ n < n; (s)% ⊦ wl-entry(m, stat).ec:= m0 = wl-entry(m0, stat); (s)% ⊦ m < n + 1 ↔ ¬ n < m; (s)% ⊦ mkpeb(aehdr, avhdr, buf, m, boolvar).bad ↔ boolvar; (s)% ⊦ mkpeb(aehdr, avhdr, buf, m, boolvar).vidhdr = avhdr; (s)% ⊦ aechdr(m) = aechdr(m0) ↔ m = m0; (s)% ⊦ mkpeb(aehdr, avhdr, buf, m, boolvar).echdr = aehdr; (s)%⊦ m ≠ n0 → ( valid-vtbl(apebs[m, apeb], vols, wlar, n0) ↔ valid-vtbl(apebs, vols, wlar, n0)); (s)% ⊦ id○(apebs[n, apeb], apebs0, n) ↔ id○(apebs, apebs0, n); (s)%m < # apebs ⊦ apebs[m, apeb][m, apeb0] = apebs[m, apeb0]; (s)% ⊦ valid-eraseq(wlar, q0 + eq-entry(m, lref) ' + q1) → ¬ # wlar ≤ m; (s)%a: ⊦ (q + q0) + q1 = q + q0 + q1; from specification list[erasequeue-base]% ⊦ m < n ↔ ¬ n ≤ m; (ss)%⊦ mkpeb(aehdr, avhdr, buf, m, boolvar).echdr:= aehdr0 = mkpeb(aehdr0, avhdr, buf, m, boolvar); (s)% ⊦ m < # apebs → apebs[m, apeb][m] = apeb; (s)%c: ⊦ m + n = n + m; from specification nat-basic%a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic% ⊦ n ≤ n0 ∧ n1 ≤ m → n + n1 ≤ n0 + m; (s)% ⊦ ¬ ⌊ESUCCESS⌋ ; (s)% ⊦ # apebs[n, apeb] = # apebs; (s)