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

# wlar = # wlar0, # apebs = # wlar0, # apebs0 = # wlar0, apebs[m] = mkpeb(aehdr, avhdr, buf, m2, false), wlar0[m] = wl-entry(m0, erasing), wlar[m] = wl-entry(m1, erasing), err = ESUCCESS, err = err0, m < # wlar0, m < # apebs, bflipset-cons(bflipset, wlar0), bflipset-cons(bflipset, wlar), id○(wlar, wlar0, m), id○(apebs, apebs0, m), ubi-io-inv(apebs0), ubi-io-inv(apebs), ubi-io-peb-inv(mkpeb(aehdr, avhdr, buf, m2, false)), unique-sqns(apebs0), unique-sqns(apebs), valid-ebatbl(apebs0, wlar0, vols, vtblpnum1), valid-ebatbl(apebs, wlar, 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-eraseq(apebs, q0 + eq-entry(m, lref) ' + q1), valid-eraseq(wlar, q0 + eq-entry(m, lref) ' + q1), valid-global-sqn(apebs0, sqnum), valid-global-sqn(apebs, sqnum), valid-vtbl(apebs0, vols, wlar0, vtblpnum1), valid-vtbl(apebs, vols, wlar, vtblpnum1), valid-wl(apebs0, wlar0), valid-wl(apebs, wlar), ⌊err0⌋ ∨ err0 = ESUCCESS ⊦ ⟪wlar[m] := wl-entry(wlar[m].ec, erroneous)⟫ ( ( err = ESUCCESS → # apebs[m, apebs[m].bad:= true] = # wlar ∧ unique-sqns(apebs[m, apebs[m].bad:= true]) ∧ valid-global-sqn(apebs[m, apebs[m].bad:= true], sqnum) ∧ valid-wl(apebs[m, apebs[m].bad:= true], wlar) ∧ valid-eraseq(wlar, q0 + q1) ∧ valid-eraseq(apebs[m, apebs[m].bad:= true], q0 + q1) ∧ bflipset-cons(bflipset, wlar) ∧ valid-ebatbl(apebs[m, apebs[m].bad:= true], wlar, vols, vtblpnum1) ∧ valid-vtbl(apebs[m, apebs[m].bad:= true], vols, wlar, vtblpnum1)) ∧ ( err ≠ ESUCCESS → # apebs[m, apebs[m].bad:= true] = # wlar ∧ unique-sqns(apebs[m, apebs[m].bad:= true]) ∧ valid-global-sqn(apebs[m, apebs[m].bad:= true], sqnum) ∧ valid-wl(apebs[m, apebs[m].bad:= true], wlar) ∧ valid-eraseq(wlar, q0 + eq-entry(m, lref) ' + q1) ∧ valid-eraseq(apebs[m, apebs[m].bad:= true], q0 + eq-entry(m, lref) ' + q1) ∧ bflipset-cons(bflipset, wlar) ∧ valid-ebatbl(apebs[m, apebs[m].bad:= true], wlar, vols, vtblpnum1) ∧ valid-vtbl(apebs[m, apebs[m].bad:= true], vols, wlar, vtblpnum1)) ∧ ubi-io-inv(apebs[m, apebs[m].bad:= true]) ∧ wlar[m].status ≠ used ∧ (err = ESUCCESS ∨ ⌊err⌋ ) ∧ id○(wlar, wlar0, m) ∧ id○(apebs[m, apebs[m].bad:= true], apebs0, m) ∧ id(apebs[m, apebs[m].bad:= true], apebs0, mapped-pebs(vols))), err1 = ESUCCESS, vtblpnum1 = m, vtblpnum1 ∈ q1, vtblpnum1 ∈ q0, VTBL_VOLID ∈ vols

Heuristic symbolic execution applied rule assign right

And obtained the following new goals

Proof step 137:
# apebs0 = # wlar0, # apebs = # wlar0, # wlar = # wlar0, wlar[m] = wl-entry(m1, erasing), wlar0[m] = wl-entry(m0, erasing), apebs[m] = mkpeb(aehdr, avhdr, buf, m2, false), err = err0, err = ESUCCESS, m < # wlar, m < # apebs, m < # wlar0, bflipset-cons(bflipset, wlar), bflipset-cons(bflipset, wlar0), id○(apebs, apebs0, m), id○(wlar, wlar0, m), ubi-io-inv(apebs), ubi-io-inv(apebs0), ubi-io-peb-inv(mkpeb(aehdr, avhdr, buf, m2, false)), unique-sqns(apebs), unique-sqns(apebs0), valid-ebatbl(apebs, wlar, vols, vtblpnum1), valid-ebatbl(apebs0, wlar0, vols, vtblpnum1), valid-eraseq(wlar, q0 + eq-entry(m, lref) ' + q1), valid-eraseq(apebs, q0 + eq-entry(m, lref) ' + q1), 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(apebs, sqnum), valid-global-sqn(apebs0, sqnum), valid-vtbl(apebs, vols, wlar, vtblpnum1), valid-vtbl(apebs0, vols, wlar0, vtblpnum1), valid-wl(apebs, wlar), valid-wl(apebs0, wlar0), ⌊err0⌋ ∨ err0 = ESUCCESS ⊦ err1 = ESUCCESS, vtblpnum1 = m, VTBL_VOLID ∈ vols, vtblpnum1 ∈ q0, vtblpnum1 ∈ q1, ( err = ESUCCESS → # apebs[m, apebs[m].bad:= true] = # wlar[m, wl-entry(wlar[m].ec, erroneous)] ∧ unique-sqns(apebs[m, apebs[m].bad:= true]) ∧ valid-global-sqn(apebs[m, apebs[m].bad:= true], sqnum) ∧ valid-wl(apebs[m, apebs[m].bad:= true], wlar[m, wl-entry(wlar[m].ec, erroneous)]) ∧ valid-eraseq(wlar[m, wl-entry(wlar[m].ec, erroneous)], q0 + q1) ∧ valid-eraseq(apebs[m, apebs[m].bad:= true], q0 + q1) ∧ bflipset-cons(bflipset, wlar[m, wl-entry(wlar[m].ec, erroneous)]) ∧ valid-ebatbl(apebs[m, apebs[m].bad:= true], wlar[m, wl-entry(wlar[m].ec, erroneous)], vols, vtblpnum1) ∧ valid-vtbl(apebs[m, apebs[m].bad:= true], vols, wlar[m, wl-entry(wlar[m].ec, erroneous)], vtblpnum1)) ∧ ( err ≠ ESUCCESS → # apebs[m, apebs[m].bad:= true] = # wlar[m, wl-entry(wlar[m].ec, erroneous)] ∧ unique-sqns(apebs[m, apebs[m].bad:= true]) ∧ valid-global-sqn(apebs[m, apebs[m].bad:= true], sqnum) ∧ valid-wl(apebs[m, apebs[m].bad:= true], wlar[m, wl-entry(wlar[m].ec, erroneous)]) ∧ valid-eraseq(wlar[m, wl-entry(wlar[m].ec, erroneous)], q0 + eq-entry(m, lref) ' + q1) ∧ valid-eraseq(apebs[m, apebs[m].bad:= true], q0 + eq-entry(m, lref) ' + q1) ∧ bflipset-cons(bflipset, wlar[m, wl-entry(wlar[m].ec, erroneous)]) ∧ valid-ebatbl(apebs[m, apebs[m].bad:= true], wlar[m, wl-entry(wlar[m].ec, erroneous)], vols, vtblpnum1) ∧ valid-vtbl(apebs[m, apebs[m].bad:= true], vols, wlar[m, wl-entry(wlar[m].ec, erroneous)], vtblpnum1)) ∧ ubi-io-inv(apebs[m, apebs[m].bad:= true]) ∧ wlar[m, wl-entry(wlar[m].ec, erroneous)][m].status ≠ used ∧ (err = ESUCCESS ∨ ⌊err⌋ ) ∧ id○(wlar[m, wl-entry(wlar[m].ec, erroneous)], wlar0, m) ∧ id○(apebs[m, apebs[m].bad:= true], apebs0, m) ∧ id(apebs[m, apebs[m].bad:= true], apebs0, mapped-pebs(vols))

Rule argument

Additional information

Used simplifier rules: ⊦ ¬ ⌊ESUCCESS⌋ ; (s)% ⊦ 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)