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

Heuristic symbolic execution applied rule if positive left

And obtained the following new goals

• Proof step 345:

  ⟨fail_or_success#(; ; err); if err = ESUCCESS then avols[v][vtblpnum] := mapped(subarray(buf, 0, n) + mkempbuf(LEB_SIZE - n), n)⟩ (avols = avols0 ∧ err = err2), # 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), n0 = 0, vtblpnum4 = n4, VTBL_VOLID ∈ vols

Rule argument

Additional information

Used simplifier rules: ⊦ v ∈ vols ∧ abs(avols, apebs, vols, q) → v ∈ avols; (ss)%⊦ v ∈ vols ∧ m < # vols[v] ∧ abs(avols, apebs, vols, q) → m < # avols[v]; (ss)% ⊦ n + 0 = n; (s)%a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic%c: ⊦ m + n = n + m; from specification nat-basic% ⊦ # mkbuf(n) = n; (s)% ⊦ m ≤ n ↔ ¬ n < m; (ss)% ⊦ ¬ m + n < m; (s)%m1 + n ≤ # buf ⊦ subarray(copy(buf0, m0, buf, m1, n), m1, n) = subarray(buf0, m0, n); (s)% ⊦ # copy(buf, m, buf0, m0, n) = # buf0; (s)% ⊦ m + n - m = n; (s)% ⊦ m - m = 0; (s)% ⊦ m ≤ m + n; (s)% ⊦ m + n ≤ m + n0 ↔ n ≤ n0; (s)% ⊦ m ≤ m; (s)%n1 + n2 ≤ m0, m0 + m1 ≤ # buf ⊦ subarray(copy(buf0, n0, buf, n1, n2), m0, m1) = subarray(buf, m0, m1); (s)% ⊦ subarray(buf, n, 0) = mkbuf(0); (s)% ⊦ buf + mkbuf(0) = buf; (s)%append-a: ⊦ (buf + buf0) + buf1 = buf + buf0 + buf1; from specification array-splice[buffer]% ⊦ #(buf + buf0) = # buf + # buf0; (s)% ⊦ # subarray(buf, m, n) = n; (s)% ⊦ EB_PAGE_SIZE ≠ 0; (s)%m ≠ 0, is-aligned(n1, m) ⊦ is-aligned(n0 + n1, m) ↔ is-aligned(n0, m); (s)