Proof step 8 from proof prepost-write-once (previous step)

Heuristic symbolic execution applied rule let right

And obtained the following new goals

• Proof step 9:

  # apebs0 = # wlar, LEB_SIZE = (n1 + m0) + m1, vols0[v][m] = unmapped, apebs = apebs0, n = m1, n0 = m2, q = q0, vols = vols0, vtblpnum0 = m0, vtblpnum1 = m, m < # vols0[v], bflipset-cons(bflipset, wlar), is-aligned(m1, EB_PAGE_SIZE), is-aligned(m0, EB_PAGE_SIZE), ubi-io-inv(apebs0), unique-sqns(apebs0), valid-ebatbl(apebs0, wlar, vols0, vtblpnum2), valid-eraseq(apebs0, q0), valid-eraseq(wlar, q0), valid-eraseq(q0), valid-global-sqn(apebs0, sqnum), valid-vtbl(apebs0, vols0, wlar, vtblpnum2), valid-wl(apebs0, wlar), v ∈ vols0, m1 ≤ LEB_SIZE, m1 + m2 ≤ # buf, m0 + m1 ≤ LEB_SIZE ⊦ ⟪ubi_wl_get_peb#(; vtblpnum, wlar, q, apebs; err); if err = ESUCCESS then let m = ? in {ubi_next_sqnum#(; sqnum; m); aubi_io_write_vidhdr#(vtblpnum, avidhdr(v, vtblpnum1, m, 0, 0); apebs; err); if err = ESUCCESS then {if n ≠ 0 then aubi_io_write_data#(vtblpnum, vtblpnum0, n0, n, buf; apebs; err); if err = ESUCCESS then {vols[v][vtblpnum1] := ⌜vtblpnum⌝ ; wlar[vtblpnum].status := used} else ubi_wl_put_peb#(v × vtblpnum1, vtblpnum; wlar, q); skip} else ubi_wl_put_peb#(none, vtblpnum; wlar, q)}⟫ ( # apebs = # wlar ∧ unique-sqns(apebs) ∧ valid-global-sqn(apebs, sqnum) ∧ valid-wl(apebs, wlar) ∧ valid-eraseq(q) ∧ valid-eraseq(wlar, q) ∧ valid-eraseq(apebs, q) ∧ ¬ VTBL_VOLID ∈ vols ∧ bflipset-cons(bflipset, wlar) ∧ valid-ebatbl(apebs, wlar, vols, vtblpnum2) ∧ valid-vtbl(apebs, vols, wlar, vtblpnum2) ∧ ubi-io-inv(apebs) ∧ id(apebs, apebs0, mapped-pebs(vols0)) ∧ q.lebrefs ⊆ q0.lebrefs ++ (v × m) ∧ (m1 = 0 → q.lebrefs ⊆ q0.lebrefs) ∧ (err = ESUCCESS ∨ ⌊err⌋ ) ∧ (err ≠ ESUCCESS → vols = vols0) ∧ ( err = ESUCCESS → (∃ n. vols = vols0[v, vols0[v][m, ⌜n⌝ ]] ∧ (m1 ≠ 0 → apebs[n].fill = m0 + m1) ∧ (m1 = 0 → apebs[n].fill = 0) ∧ apebs[n].data = mkempbuf(m0) + subarray(buf, m2, m1) + mkempbuf(n1)))), VTBL_VOLID ∈ vols0, vtblpnum2 ∈ q0

Rule argument

Additional information