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

# 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))

Heuristic simplifier applied rule simplifier

And obtained the following new goals

Proof step 138:
# 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), 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-inv(apebs[m, mkpeb(aehdr, avhdr, buf, m2, true)]), 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) ⊦ err1 = ESUCCESS, vtblpnum1 = m, VTBL_VOLID ∈ vols, vtblpnum1 ∈ q0, vtblpnum1 ∈ q1, valid-ebatbl(apebs[m, mkpeb(aehdr, avhdr, buf, m2, true)], wlar[m, wl-entry(m1, erroneous)], vols, vtblpnum1) ∧ valid-eraseq(apebs[m, mkpeb(aehdr, avhdr, buf, m2, true)], q0 + q1) ∧ valid-eraseq(wlar[m, wl-entry(m1, erroneous)], q0 + q1) ∧ valid-wl(apebs[m, mkpeb(aehdr, avhdr, buf, m2, true)], wlar[m, wl-entry(m1, erroneous)]) ∧ valid-global-sqn(apebs[m, mkpeb(aehdr, avhdr, buf, m2, true)], sqnum) ∧ unique-sqns(apebs[m, mkpeb(aehdr, avhdr, buf, m2, true)])

Rule argument

Additional information

Used simplifier rules: ⊦ ubi-io-peb-inv(mkpeb(aehdr, avhdr, buf, n, boolvar)) → # buf = LEB_SIZE; (s)%⊦ ubi-io-peb-inv(mkpeb(aehdr, avhdr, buf, n, true)) ↔ # buf = LEB_SIZE; (ss)%⊦ ubi-io-inv(apebs) → ( ubi-io-inv(apebs[n, apeb]) ↔ n < # apebs ∧ ubi-io-peb-inv(apebs[n]) → ubi-io-peb-inv(apeb)); (ss)%⊦ mkpeb(aehdr, avhdr, buf, m, boolvar).bad:= boolvar0 = mkpeb(aehdr, avhdr, buf, m, boolvar0); (s)%n < # wlar, stat ≠ used ⊦ wlar[n] = wl-entry(m, stat) ∧ id○(apebs, apebs0, n) ∧ valid-ebatbl(apebs, wlar, vols, n0) → id(apebs, apebs0, mapped-pebs(vols)); (ss)%¬ n ∈ ns ⊦ id(apebs1[n, apeb], apebs0, ns) ↔ id(apebs1, apebs0, ns); (s)%n < # wlar, stat ≠ used ⊦ wlar[n] = wl-entry(m, stat) ∧ valid-ebatbl(apebs, wlar, vols, n0) → ¬ n ∈ mapped-pebs(vols); (s)% ⊦ id○(apebs[n, apeb], apebs0, n) ↔ id○(apebs, apebs0, n); (s)% ⊦ id○(wlar[n, wle], wlar0, n) ↔ id○(wlar, wlar0, n); (s)% ⊦ m < # wlar → wlar[m, wle][m] = wle; (s)%⊦ m ≠ n0 → ( valid-vtbl(apebs, vols, wlar[m, wle], n0) ↔ valid-vtbl(apebs, vols, wlar, n0)); (s)%⊦ m ≠ n0 → ( valid-vtbl(apebs[m, apeb], vols, wlar, n0) ↔ valid-vtbl(apebs, vols, wlar, n0)); (s)%stat ≠ used ⊦ wlar[n] = wl-entry(m, stat) ∧ bflipset-cons(bflipset, wlar) → ¬ n ∈ bflipset; (s)% ⊦ used ≠ erasing; (s)%wle.status ≠ used ⊦ bflipset-cons(bflipset, wlar[m, wle]) ↔ bflipset-cons(bflipset, wlar) ∧ ¬ m ∈ bflipset; (s)% ⊦ used ≠ erroneous; (s)% ⊦ wl-entry(m, stat).status = stat; (s)% ⊦ wl-entry(m, stat).ec = m; (s)% ⊦ # wlar[n, wle] = # wlar; (s)% ⊦ # apebs[n, apeb] = # apebs; (s)% ⊦ ¬ ⌊ESUCCESS⌋ ; (s)