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

Heuristic conditional right split applied rule if right

And obtained the following new goals

• Proof step 7:

  # apebs = # wlar, buf0 = buf, ebae = unmapped, ebae = vols[v][vtblpnum2], vtblpnum = vtblpnum4, vtblpnum0 = EB_PAGE_SIZE, vtblpnum1 = vtblpnum5, vtblpnum2 = vtblpnum3, vtblpnum2 < # vols[v], vtblpnum3 < # avols[v], abs(avols, apebs, vols, q), bflipset-cons(bflipset, wlar), ebm-cons(avols), is-aligned(vtblpnum1, EB_PAGE_SIZE), is-aligned(n, EB_PAGE_SIZE), is-aligned(vtblpnum5, EB_PAGE_SIZE), ubi-io-inv(apebs), 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 ∈ vols, v ∈ avols, vtblpnum1 + n ≤ LEB_SIZE, n0 + n ≤ # buf0, n + n0 ≤ # buf, vtblpnum5 + n ≤ LEB_SIZE, vols[v][vtblpnum2] ≠ unmapped → apebs[vols[v][vtblpnum2].pnum].fill ≤ vtblpnum1, v ∈ vols → v ∈ vols ∧ ( vtblpnum2 < # vols[v] → vtblpnum1 + n ≤ LEB_SIZE → n0 + n ≤ # buf0 → is-aligned(n, EB_PAGE_SIZE) → is-aligned(vtblpnum1, EB_PAGE_SIZE) → (vtblpnum2 < # vols[v] ∧ v ∈ vols) ∧ ( vols[v][vtblpnum2] ≠ unmapped → vols[v][vtblpnum2].pnum < # apebs ∧ vols[v][vtblpnum2] ≠ unmapped ∧ vtblpnum2 < # vols[v] ∧ v ∈ vols)), avols[v][vtblpnum3].mapped? → avols[v][vtblpnum3].fill ≤ vtblpnum5 ⊦ ⟪ubi_write_multiple#(v, vtblpnum2, vtblpnum1, n0, n, buf0, bflipset, vtblpnum; vols, wlar, q, sqnum, apebs; err)⟫ ⟨ebm_write#(v, vtblpnum3, vtblpnum5, n0, n, buf; avols; err0)⟩ (abs(avols, apebs, vols, q) ∧ err = err0), VTBL_VOLID ∈ vols

• Proof step 49:

  # apebs = # wlar, buf0 = buf, ebae = vols[v][vtblpnum2], vtblpnum = vtblpnum4, vtblpnum0 = EB_PAGE_SIZE, vtblpnum1 = vtblpnum5, vtblpnum2 = vtblpnum3, vtblpnum2 < # vols[v], vtblpnum3 < # avols[v], abs(avols, apebs, vols, q), bflipset-cons(bflipset, wlar), ebm-cons(avols), is-aligned(vtblpnum1, EB_PAGE_SIZE), is-aligned(n, EB_PAGE_SIZE), is-aligned(vtblpnum5, EB_PAGE_SIZE), ubi-io-inv(apebs), 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 ∈ vols, v ∈ avols, vtblpnum1 + n ≤ LEB_SIZE, n0 + n ≤ # buf0, n + n0 ≤ # buf, vtblpnum5 + n ≤ LEB_SIZE, vols[v][vtblpnum2] ≠ unmapped → apebs[vols[v][vtblpnum2].pnum].fill ≤ vtblpnum1, v ∈ vols → v ∈ vols ∧ ( vtblpnum2 < # vols[v] → vtblpnum1 + n ≤ LEB_SIZE → n0 + n ≤ # buf0 → is-aligned(n, EB_PAGE_SIZE) → is-aligned(vtblpnum1, EB_PAGE_SIZE) → (vtblpnum2 < # vols[v] ∧ v ∈ vols) ∧ ( vols[v][vtblpnum2] ≠ unmapped → vols[v][vtblpnum2].pnum < # apebs ∧ vols[v][vtblpnum2] ≠ unmapped ∧ vtblpnum2 < # vols[v] ∧ v ∈ vols)), avols[v][vtblpnum3].mapped? → avols[v][vtblpnum3].fill ≤ vtblpnum5 ⊦ ⟪if n ≠ 0 then {aubi_io_write_data#(ebae.pnum, vtblpnum1, n0, n, buf0; apebs; err); if err ≠ ESUCCESS then {debug#("ubi: failed to write to PEB " + ebae.pnum.toString); let buf = mkbuf(vtblpnum1 + n), bitflips = ? in {aubi_io_read_data#(ebae.pnum, 0, 0, vtblpnum1, apebs; buf; bitflips, err); if err = ESUCCESS then {buf := copy(buf0, n0, buf, vtblpnum1, n); debug#("ubi: moving data from PEB " + ebae.pnum.toString); ubi_change#(v, vtblpnum2, vtblpnum1 + n, buf, vtblpnum0; vols, wlar, q, bflipset, vtblpnum, sqnum, apebs; err)} else debug#("ubi: failed to read data from PEB " + ebae.pnum.toString)}}} else err := ESUCCESS⟫ ⟨ebm_write#(v, vtblpnum3, vtblpnum5, n0, n, buf; avols; err0)⟩ (abs(avols, apebs, vols, q) ∧ err = err0), ebae = unmapped, VTBL_VOLID ∈ vols

Rule argument

Additional information