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

Heuristic conditional left split applied rule if left

And obtained the following new goals

• Proof step 347:

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

• Proof step 365:

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

Rule argument

Additional information