Proof step 44 from proof refine-erase (previous step)

Heuristic symbolic execution applied rule or right

And obtained the following new goals

• Proof step 45:

  # apebs = # wlar0, # apebs0 = # wlar1, wlar0[n] = wl-entry(m, stat), vols[v][vtblpnum2] = ⌜n⌝ , err = err1, avols[v][vtblpnum2].mapped?, vtblpnum2 < # vols[v], vtblpnum2 < # avols[v], n < # wlar0, abs(avols, apebs, vols, q0), bflipset-cons(bflipset -- n, wlar0), bflipset-cons(bflipset, wlar0), bflipset-cons(bflipset -- n, wlar1), ebm-cons(avols), id(apebs0, apebs, mapped-pebs(vols) -- n), ubi-io-inv(apebs), ubi-io-inv(apebs0), unique-sqns(apebs0), unique-sqns(apebs), valid-ebatbl(apebs, wlar0, vols, vtblpnum1), valid-ebatbl(apebs, wlar0[n, wl-entry(m, erasing)], vols[v, vols[v][vtblpnum2, unmapped]], vtblpnum1), valid-ebatbl(apebs0, wlar1, vols[v, vols[v][vtblpnum2, unmapped]], vtblpnum1), valid-eraseq(apebs0, q1), valid-eraseq(wlar1, q1), valid-eraseq(q1), valid-eraseq(q0), valid-eraseq(wlar0, q0), valid-eraseq(apebs, q0), valid-eraseq(apebs, q0 + eq-entry(n, v × vtblpnum2) '), valid-eraseq(wlar0[n, wl-entry(m, erasing)], q0 + eq-entry(n, v × vtblpnum2) '), valid-eraseq(q0 + eq-entry(n, v × vtblpnum2) '), valid-global-sqn(apebs0, sqnum), valid-global-sqn(apebs, sqnum), valid-vtbl(apebs, vols, wlar0, vtblpnum1), valid-vtbl(apebs, vols, wlar0[n, wl-entry(m, erasing)], vtblpnum1), valid-vtbl(apebs0, vols, wlar1, vtblpnum1), valid-wl(apebs0, wlar1), valid-wl(apebs, wlar0), valid-wl(apebs, wlar0[n, wl-entry(m, erasing)]), v ∈ vols, v ∈ avols, q1 ⊆ q0 + eq-entry(n, v × vtblpnum2) ', err1 = ESUCCESS → q1 = [], err1 = ESUCCESS ∨ ⌊err1⌋ ⊦ ⟨avols[v][vtblpnum2] := unmapped⟩ (abs(avols, apebs0, vols[v, vols[v][vtblpnum2, unmapped]], q1) ∧ err1 = err), ⟨skip⟩ (abs(avols, apebs0, vols[v, vols[v][vtblpnum2, unmapped]], q1) ∧ err1 = err), err = ESUCCESS, VTBL_VOLID ∈ vols

Rule argument

Additional information