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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 27:

  # apebs0 = # wlar, # apebs = # wlar, wlar[m0] = wl-entry(m1, used), apebs[m0] = mkpeb(aehdr, avhdr, buf1, m, false), vols[v][vtblpnum4] = ⌜m0⌝ , err ≠ ESUCCESS, m0 ≠ vtblpnum, n ≠ 0, vtblpnum4 < # vols[v], m0 < # wlar, bflipset-cons(bflipset, wlar), is-aligned(vtblpnum3, EB_PAGE_SIZE), is-aligned(n, EB_PAGE_SIZE), ubi-io-inv(apebs0), ubi-io-inv(apebs), ubi-io-peb-inv(mkpeb(aehdr, avhdr, buf1, m, false)), unique-sqns(apebs0), unique-sqns(apebs), valid-ebatbl(apebs0, wlar, vols, vtblpnum), valid-ebatbl(apebs, wlar, vols, vtblpnum), valid-eraseq(apebs0, q), valid-eraseq(apebs, q), valid-eraseq(wlar, q), valid-eraseq(q), valid-global-sqn(apebs0, sqnum), valid-global-sqn(apebs, sqnum), valid-peb(mkpeb(aehdr, avhdr, buf1, m, false)), valid-peb(v, vtblpnum4, mkpeb(aehdr, avhdr, buf1, m, false)), valid-peb(v, vtblpnum4, apebs0[m0]), valid-vtbl(apebs0, vols, wlar, vtblpnum), valid-vtbl(apebs, vols, wlar, vtblpnum), valid-wl(apebs0, wlar), valid-wl(apebs, wlar), v ∈ vols, vtblpnum3 + n ≤ LEB_SIZE, n0 + n ≤ # buf, m ≤ vtblpnum3, ¬ m0 ∈ q, ¬ VTBL_VOLID ∈ vols, ¬ vtblpnum ∈ q ⊦ ⟪let buf1 = mkbuf(vtblpnum3 + n), bitflips = ? in {aubi_io_read_data#(m0, 0, 0, vtblpnum3, apebs0; buf1; bitflips, err); if err = ESUCCESS then {buf1 := copy(buf, n0, buf1, vtblpnum3, n); debug#("ubi: moving data from PEB " + m0.toString); ubi_change#(v, vtblpnum4, vtblpnum3 + n, buf1, EB_PAGE_SIZE; vols, wlar, q, bflipset, vtblpnum, sqnum, apebs0; err)} else debug#("ubi: failed to read data from PEB " + m0.toString)}⟫ ( # apebs0 = # wlar ∧ unique-sqns(apebs0) ∧ valid-global-sqn(apebs0, sqnum) ∧ valid-wl(apebs0, wlar) ∧ valid-eraseq(q) ∧ valid-eraseq(wlar, q) ∧ valid-eraseq(apebs0, q) ∧ ¬ VTBL_VOLID ∈ vols ∧ bflipset-cons(bflipset, wlar) ∧ valid-ebatbl(apebs0, wlar, vols, vtblpnum) ∧ valid-vtbl(apebs0, vols, wlar, vtblpnum) ∧ ubi-io-inv(apebs0))

Rule argument

Additional information