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

# apebs0 = # wlar0, wlar0[m] = wl-entry(m0, erasing), apebs1 = apebs0, err = ESUCCESS, err0 = EIO, vtblpnum0 = m, vtblpnum3 = 0, wlar1 = wlar0, m < # wlar0, bflipset-cons(bflipset, wlar0), erase-worker-inv(apebs0, wlar0, vtblpnum, err, apebs, vols, wlar, q0, eq-entry(m, lref), q1, bflipset, vtblpnum1, sqnum), ubi-io-inv(apebs0), unique-sqns(apebs0), valid-ebatbl(apebs0, wlar0, vols, vtblpnum1), 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(apebs0, sqnum), valid-vtbl(apebs0, vols, wlar0, vtblpnum1), valid-wl(apebs0, wlar0) ⊦ ⟪wlar[vtblpnum0] := wl-entry(wlar[vtblpnum0].ec, free)⟫ ( ( err = ESUCCESS → # apebs = # wlar ∧ unique-sqns(apebs) ∧ valid-global-sqn(apebs, sqnum) ∧ valid-wl(apebs, wlar) ∧ valid-eraseq(wlar, q0 + q1) ∧ valid-eraseq(apebs, q0 + q1) ∧ bflipset-cons(bflipset, wlar) ∧ valid-ebatbl(apebs, wlar, vols, vtblpnum1) ∧ valid-vtbl(apebs, vols, wlar, vtblpnum1)) ∧ ( err ≠ ESUCCESS → # 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) ∧ wlar[m].status ≠ used ∧ (err = ESUCCESS ∨ ⌊err⌋ ) ∧ id○(wlar, wlar0, m) ∧ id○(apebs, apebs0, m) ∧ id(apebs, apebs0, mapped-pebs(vols))), vtblpnum1 = m, vtblpnum1 ∈ q1, vtblpnum1 ∈ q0, VTBL_VOLID ∈ vols, err ≠ ESUCCESS ∧ vtblpnum ≤ UBI_ERASE_RETRIES

Heuristic symbolic execution applied rule assign right

And obtained the following new goals

Proof step 116:
# apebs0 = # wlar0, wlar0[m] = wl-entry(m0, erasing), apebs1 = apebs0, err = ESUCCESS, err0 = EIO, vtblpnum0 = m, vtblpnum3 = 0, wlar1 = wlar0, vtblpnum0 < # wlar, m < # wlar0, bflipset-cons(bflipset, wlar0), erase-worker-inv(apebs0, wlar0, vtblpnum, err, apebs, vols, wlar, q0, eq-entry(m, lref), q1, bflipset, vtblpnum1, sqnum), ubi-io-inv(apebs0), unique-sqns(apebs0), valid-ebatbl(apebs0, wlar0, 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-global-sqn(apebs0, sqnum), valid-vtbl(apebs0, vols, wlar0, vtblpnum1), valid-wl(apebs0, wlar0) ⊦ vtblpnum1 = m, VTBL_VOLID ∈ vols, vtblpnum1 ∈ q0, vtblpnum1 ∈ q1, err ≠ ESUCCESS ∧ vtblpnum ≤ UBI_ERASE_RETRIES, ( err = ESUCCESS → # apebs = # wlar[vtblpnum0, wl-entry(wlar[vtblpnum0].ec, free)] ∧ unique-sqns(apebs) ∧ valid-global-sqn(apebs, sqnum) ∧ valid-wl(apebs, wlar[vtblpnum0, wl-entry(wlar[vtblpnum0].ec, free)]) ∧ valid-eraseq(wlar[vtblpnum0, wl-entry(wlar[vtblpnum0].ec, free)], q0 + q1) ∧ valid-eraseq(apebs, q0 + q1) ∧ bflipset-cons(bflipset, wlar[vtblpnum0, wl-entry(wlar[vtblpnum0].ec, free)]) ∧ valid-ebatbl(apebs, wlar[vtblpnum0, wl-entry(wlar[vtblpnum0].ec, free)], vols, vtblpnum1) ∧ valid-vtbl(apebs, vols, wlar[vtblpnum0, wl-entry(wlar[vtblpnum0].ec, free)], vtblpnum1)) ∧ ( err ≠ ESUCCESS → # apebs = # wlar[vtblpnum0, wl-entry(wlar[vtblpnum0].ec, free)] ∧ unique-sqns(apebs) ∧ valid-global-sqn(apebs, sqnum) ∧ valid-wl(apebs, wlar[vtblpnum0, wl-entry(wlar[vtblpnum0].ec, free)]) ∧ valid-eraseq(wlar[vtblpnum0, wl-entry(wlar[vtblpnum0].ec, free)], q0 + eq-entry(m, lref) ' + q1) ∧ valid-eraseq(apebs, q0 + eq-entry(m, lref) ' + q1) ∧ bflipset-cons(bflipset, wlar[vtblpnum0, wl-entry(wlar[vtblpnum0].ec, free)]) ∧ valid-ebatbl(apebs, wlar[vtblpnum0, wl-entry(wlar[vtblpnum0].ec, free)], vols, vtblpnum1) ∧ valid-vtbl(apebs, vols, wlar[vtblpnum0, wl-entry(wlar[vtblpnum0].ec, free)], vtblpnum1)) ∧ ubi-io-inv(apebs) ∧ wlar[vtblpnum0, wl-entry(wlar[vtblpnum0].ec, free)][m].status ≠ used ∧ (err = ESUCCESS ∨ ⌊err⌋ ) ∧ id○(wlar[vtblpnum0, wl-entry(wlar[vtblpnum0].ec, free)], wlar0, m) ∧ id○(apebs, apebs0, m) ∧ id(apebs, apebs0, mapped-pebs(vols))

Rule argument

Additional information

Used simplifier rules: ⊦ erase-worker-inv (apebs0, wlar0, m, err, apebs, vols, wlar, q0, eqent, q1, bflipset, n0, n1) ↔ m ≤ UBI_ERASE_RETRIES + 1 ∧ eqent.pnum < # apebs ∧ id○(apebs, apebs0, eqent.pnum) ∧ id○(wlar, wlar0, eqent.pnum) ∧ ubi-cons(apebs, vols, wlar, q0 + (eqent + q1), bflipset, n0, n1) ∧ ubi-io-inv(apebs) ∧ ( err = ESUCCESS → apebs[eqent.pnum].echdr = aechdr(wlar[eqent.pnum].ec) ∧ apebs[eqent.pnum].vidhdr = empty ∧ ¬ apebs[eqent.pnum].bad); (s)% ⊦ eq-entry(m, lref).pnum = m; (s)% ⊦ eqent + q = eqent ' + q; (s)%a: ⊦ (q + q0) + q1 = q + q0 + q1; from specification list[erasequeue-base]%⊦ ubi-cons(apebs, vols, wlar, q, bflipset, n0, n1) ↔ # apebs = # wlar ∧ unique-sqns(apebs) ∧ valid-global-sqn(apebs, n1) ∧ valid-wl(apebs, wlar) ∧ valid-eraseq(q) ∧ valid-eraseq(wlar, q) ∧ valid-eraseq(apebs, q) ∧ ¬ VTBL_VOLID ∈ vols ∧ bflipset-cons(bflipset, wlar) ∧ valid-ebatbl(apebs, wlar, vols, n0) ∧ valid-vtbl(apebs, vols, wlar, n0); (s)% ⊦ m < n ↔ ¬ n ≤ m; (ss)% ⊦ valid-eraseq(wlar, q0 + eq-entry(m, lref) ' + q1) → ¬ # wlar ≤ m; (s)