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

Heuristic symbolic execution applied rule assign left

And obtained the following new goals

• Proof step 370:

  # apebs = # wlar, apebs[n4] = mkpeb(aehdr, avhdr, buf2, m0, false), wlar[n4] = wl-entry(m1, used), avols0[v][vtblpnum3] = mapped(buf2, m), vols[v][vtblpnum3] = ⌜n4⌝ , err0 = err2, avhdr.valid?, aehdr.valid?, vtblpnum3 < # avols0[v], n4 < # wlar, vtblpnum3 < # vols[v], abs(avols0, apebs0, vols0, q0), abs(avols0, apebs, vols, q), bflipset-cons(bflipset, wlar), ebm-cons(avols0), is-aligned(n0, EB_PAGE_SIZE), is-aligned(vtblpnum5, EB_PAGE_SIZE), ubi-io-inv(apebs), ubi-io-peb-inv(mkpeb(aehdr, avhdr, buf2, m0, false)), unique-sqns(apebs), valid-ebatbl(apebs, wlar, vols, vtblpnum4), valid-eraseq(apebs, q), valid-eraseq(wlar, q), valid-eraseq(q), valid-global-sqn(apebs, sqnum), valid-vtbl(apebs, vols, wlar, vtblpnum4), valid-wl(apebs, wlar), v ∈ avols0, v ∈ vols, vtblpnum5 ≤ LEB_SIZE, vtblpnum5 + n0 ≤ LEB_SIZE, m0 ≤ vtblpnum5, m ≤ vtblpnum5, n0 + n3 ≤ # buf0, m0 ≤ LEB_SIZE, m ≤ LEB_SIZE, n3 + n0 ≤ # buf0, ⌊err3⌋ , ⌊err0⌋ ∨ err0 = ESUCCESS ⊦ ∃ err0. (⌊err0⌋ ∨ err0 = ESUCCESS) ∧ ⟨err := err0; if err = ESUCCESS then if avols0[v][vtblpnum3].mapped? then if n0 ≠ 0 then avols0[v][vtblpnum3] := mapped (subarray(avols0[v][vtblpnum3].data, 0, vtblpnum5) + subarray(buf0, n3, n0) + mkempbuf(LEB_SIZE - vtblpnum5 - n0), vtblpnum5 + n0) else avols0[v][vtblpnum3] := mapped(mkempbuf(vtblpnum5) + subarray(buf0, n3, n0) + mkempbuf(LEB_SIZE - vtblpnum5 - n0), vtblpnum5 + n0) else if avols0[v][vtblpnum3].mapped? then choose n1 with n1 < n0 ∧ is-aligned(n1, EB_PAGE_SIZE) in if n1 ≠ 0 then avols0[v][vtblpnum3] := mapped (subarray(avols0[v][vtblpnum3].data, 0, vtblpnum5) + subarray(buf0, n3, n1) + mkempbuf(LEB_SIZE - vtblpnum5 - n1), vtblpnum5 + n1) ifnone skip else if n0 ≠ 0 then avols0[v][vtblpnum3] := unmapped⟩ (abs(avols0, apebs0, vols0, q0) ∧ err2 = err), err2 = ESUCCESS, n0 = 0, vtblpnum4 = n4, VTBL_VOLID ∈ vols

Rule argument

Additional information