Proof step 7 from proof inv-write (previous step)

Heuristic symbolic execution applied rule let right

And obtained the following new goals

• Proof step 8:

  # apebs = # wlar, apebs[vols[v][vtblpnum4].pnum] = mkpeb(aehdr, avhdr, buf1, m, boolvar), buf0 = buf, ebae = vols[v][vtblpnum2], vtblpnum0 = EB_PAGE_SIZE, vtblpnum1 = vtblpnum3, vtblpnum2 = vtblpnum4, vtblpnum4 < # vols[v], vtblpnum2 < # vols[v], bflipset-cons(bflipset, wlar), is-aligned(n, EB_PAGE_SIZE), is-aligned(vtblpnum3, EB_PAGE_SIZE), is-aligned(vtblpnum1, EB_PAGE_SIZE), ubi-io-inv(apebs), unique-sqns(apebs), valid-ebatbl(apebs, wlar, vols, vtblpnum), valid-eraseq(q), valid-eraseq(wlar, q), valid-eraseq(apebs, q), valid-global-sqn(apebs, sqnum), valid-vtbl(apebs, vols, wlar, vtblpnum), valid-wl(apebs, wlar), v ∈ vols, vtblpnum3 + n ≤ LEB_SIZE, n0 + n ≤ # buf, n0 + n ≤ # buf0, vtblpnum1 + n ≤ LEB_SIZE, vols[v][vtblpnum4] ≠ unmapped → m ≤ vtblpnum3, 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)), vols[v][vtblpnum2] ≠ unmapped → apebs[vols[v][vtblpnum2].pnum].fill ≤ vtblpnum1 ⊦ ⟪if ebae = unmapped then ubi_write_multiple#(v, vtblpnum2, vtblpnum1, n0, n, buf0, bflipset, vtblpnum; vols, wlar, q, sqnum, apebs; err) else 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⟫ ( # 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, vtblpnum) ∧ valid-vtbl(apebs, vols, wlar, vtblpnum) ∧ ubi-io-inv(apebs)), VTBL_VOLID ∈ vols, vtblpnum ∈ q

• Proof step 67:

  # apebs = # wlar, apebs[vols[v][vtblpnum4].pnum] = mkpeb(aehdr, avhdr, buf1, m, boolvar), buf0 = buf, vtblpnum0 = EB_PAGE_SIZE, vtblpnum1 = vtblpnum3, vtblpnum2 = vtblpnum4, vtblpnum4 < # vols[v], vtblpnum2 < # vols[v], bflipset-cons(bflipset, wlar), is-aligned(n, EB_PAGE_SIZE), is-aligned(vtblpnum3, EB_PAGE_SIZE), is-aligned(vtblpnum1, EB_PAGE_SIZE), ubi-io-inv(apebs), unique-sqns(apebs), valid-ebatbl(apebs, wlar, vols, vtblpnum), valid-eraseq(q), valid-eraseq(wlar, q), valid-eraseq(apebs, q), valid-global-sqn(apebs, sqnum), valid-vtbl(apebs, vols, wlar, vtblpnum), valid-wl(apebs, wlar), v ∈ vols, vtblpnum3 + n ≤ LEB_SIZE, n0 + n ≤ # buf, n0 + n ≤ # buf0, vtblpnum1 + n ≤ LEB_SIZE, vols[v][vtblpnum4] ≠ unmapped → m ≤ vtblpnum3, 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)), vols[v][vtblpnum2] ≠ unmapped → apebs[vols[v][vtblpnum2].pnum].fill ≤ vtblpnum1 ⊦ VTBL_VOLID ∈ vols, vtblpnum ∈ q, vtblpnum2 < # vols[v] ∧ v ∈ vols

Rule argument

Additional information