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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 66:

  # apebs = # wlar, wlar[n1] = wl-entry(m1, used), avols[v][vtblpnum3] = mapped(buf2, m), vols[v][vtblpnum3] = ⌜n1⌝ , apebs[n1] = mkpeb(aehdr, avhdr, buf2, m0, false), n ≠ 0, vtblpnum4 ≠ n1, avhdr.valid?, vtblpnum3 < # vols[v], vtblpnum3 < # avols[v], n1 < # wlar, abs(avols, apebs, vols, q), bflipset-cons(bflipset, wlar), ebm-cons(avols), is-aligned(n, EB_PAGE_SIZE), is-aligned(vtblpnum5, 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(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, m ≤ vtblpnum5, n + n0 ≤ # buf, n0 + n ≤ # buf, vtblpnum5 + n ≤ LEB_SIZE, m0 ≤ vtblpnum5, ¬ VTBL_VOLID ∈ vols ⊦ [aubi_io_write_data#(vols[v][vtblpnum3].pnum, vtblpnum5, n0, n, buf; apebs; err)] ( # apebs = # wlar ∧ unique-sqns(apebs) ∧ valid-global-sqn(apebs, sqnum) ∧ valid-wl(apebs, wlar) ∧ valid-eraseq(apebs, q) ∧ valid-ebatbl(apebs, wlar, vols, vtblpnum4) ∧ valid-vtbl(apebs, vols, wlar, vtblpnum4) ∧ ubi-io-inv(apebs) → ⟪if err ≠ ESUCCESS then {debug#("ubi: failed to write to PEB " + vols[v][vtblpnum3].pnum.toString); let buf1 = mkbuf(vtblpnum5 + n), bitflips = ? in {aubi_io_read_data#(vols[v][vtblpnum3].pnum, 0, 0, vtblpnum5, apebs; buf1; bitflips, err); if err = ESUCCESS then {buf1 := copy(buf, n0, buf1, vtblpnum5, n); debug#("ubi: moving data from PEB " + vols[v][vtblpnum3].pnum.toString); ubi_change#(v, vtblpnum3, vtblpnum5 + n, buf1, EB_PAGE_SIZE; vols, wlar, q, bflipset, vtblpnum4, sqnum, apebs; err)} else debug#("ubi: failed to read data from PEB " + vols[v][vtblpnum3].pnum.toString)}}⟫ ⟨ebm_write#(v, vtblpnum3, vtblpnum5, n0, n, buf; avols; err0)⟩ (abs(avols, apebs, vols, q) ∧ err = err0))

Rule argument

Additional information