Proof step 68 from proof inv-write (previous step)

Heuristic symbolic execution applied rule abort right

And obtained the following new goals

• Proof step 69:

  # apebs = # wlar, apebs[vols[v][vtblpnum4].pnum] = mkpeb(aehdr, avhdr, buf1, m, boolvar), buf0 = buf, vtblpnum0 = EB_PAGE_SIZE, vtblpnum1 = vtblpnum3, vtblpnum2 = vtblpnum4, vtblpnum4 < # vols[v], bflipset-cons(bflipset, wlar), is-aligned(n, EB_PAGE_SIZE), is-aligned(vtblpnum3, EB_PAGE_SIZE), ubi-io-inv(apebs), unique-sqns(apebs), valid-ebatbl(apebs, wlar, vols, vtblpnum), valid-eraseq(q), valid-eraseq(wlar, q), valid-eraseq(apebs, q), valid-global-sqn(apebs, sqnum), valid-vtbl(apebs, vols, wlar, vtblpnum), valid-wl(apebs, wlar), v ∈ vols, vtblpnum3 + n ≤ LEB_SIZE, n0 + n ≤ # buf, vols[v][vtblpnum4] ≠ unmapped → m ≤ vtblpnum3, v ∈ vols → v ∈ vols ∧ ( vtblpnum2 < # vols[v] → vtblpnum1 + n ≤ LEB_SIZE → n0 + n ≤ # buf0 → is-aligned(n, EB_PAGE_SIZE) → is-aligned(vtblpnum1, EB_PAGE_SIZE) → (vtblpnum2 < # vols[v] ∧ v ∈ vols) ∧ ( vols[v][vtblpnum2] ≠ unmapped → vols[v][vtblpnum2].pnum < # apebs ∧ vols[v][vtblpnum2] ≠ unmapped ∧ vtblpnum2 < # vols[v] ∧ v ∈ vols)) ⊦ VTBL_VOLID ∈ vols, vtblpnum ∈ q, v ∈ vols ∧ vtblpnum2 < # vols[v] ∧ vtblpnum1 + n ≤ LEB_SIZE ∧ n0 + n ≤ # buf0 ∧ is-aligned(n, EB_PAGE_SIZE) ∧ is-aligned(vtblpnum1, EB_PAGE_SIZE) ∧ (vols[v][vtblpnum2] ≠ unmapped → apebs[vols[v][vtblpnum2].pnum].fill ≤ vtblpnum1)

Rule argument

Additional information