Proof step 75 from proof refine-write (previous step)

Heuristic symbolic execution applied rule skip right

And obtained the following new goals

• Proof step 76:

  # apebs = # wlar, # apebs0 = # wlar, wlar[n2] = wl-entry(m1, used), avols[v][vtblpnum3] = mapped(buf2, m), vols[v][vtblpnum3] = ⌜n2⌝ , apebs0[n2] = mkpeb(aehdr, avhdr, buf2, m0, false), apebs = apebs0 [vols[v][vtblpnum3].pnum, mkpeb (apebs0[vols[v][vtblpnum3].pnum].echdr, apebs0[vols[v][vtblpnum3].pnum].vidhdr, subarray(apebs0[vols[v][vtblpnum3].pnum].data, 0, vtblpnum5) + subarray(buf, n3, n) + mkempbuf(LEB_SIZE - vtblpnum5 - n), vtblpnum5 + n, apebs0[vols[v][vtblpnum3].pnum].bad) ], err = err0, err = ESUCCESS, avhdr.valid?, aehdr.valid?, n2 < # wlar, vtblpnum3 < # avols[v], vols[v][vtblpnum3].pnum < # apebs0, vtblpnum3 < # vols[v], abs(avols, apebs0, vols, q), bflipset-cons(bflipset, wlar), ebm-cons(avols), is-aligned(n, EB_PAGE_SIZE), is-aligned(vtblpnum5, EB_PAGE_SIZE), ubi-io-inv(apebs), ubi-io-inv(apebs0), ubi-io-peb-inv(mkpeb(aehdr, avhdr, buf2, m0, false)), unique-sqns(apebs), unique-sqns(apebs0), valid-ebatbl(apebs, wlar, vols, vtblpnum4), valid-ebatbl(apebs0, wlar, vols, vtblpnum4), valid-eraseq(apebs, q), valid-eraseq(apebs0, q), valid-eraseq(wlar, q), valid-eraseq(q), valid-global-sqn(apebs, sqnum), valid-global-sqn(apebs0, sqnum), valid-vtbl(apebs, vols, wlar, vtblpnum4), valid-vtbl(apebs0, vols, wlar, vtblpnum4), valid-wl(apebs, wlar), valid-wl(apebs0, wlar), v ∈ avols, v ∈ vols, m0 ≤ vtblpnum5, m ≤ vtblpnum5, n + n3 ≤ # buf, vtblpnum5 + n ≤ LEB_SIZE, 0 + vtblpnum5 ≤ # apebs0[vols[v][vtblpnum3].pnum].data, n3 + n ≤ # buf, LEB_SIZE - vtblpnum5 ≥ n, LEB_SIZE ≥ vtblpnum5, ⌊err0⌋ ∨ err0 = ESUCCESS ⊦ ⟨ebm_write#(v, vtblpnum3, vtblpnum5, n3, n, buf; avols; err1)⟩ (abs(avols, apebs, vols, q) ∧ err = err1), vols[v][vtblpnum3] = unmapped, n = 0, vtblpnum4 = n2, VTBL_VOLID ∈ vols

Rule argument

Additional information