Proof step 44 from proof inv-wl-worker (previous step)

Heuristic symbolic execution applied rule choose right

And obtained the following new goals

• Proof step 45:

  # apebs = # wlar, wlar[vtblpnum1] = wl-entry(m0, free), wlar[vtblpnum2] = wl-entry(m1, used), apebs[vtblpnum1] = mkpeb(aehdr, empty, mkempbuf(LEB_SIZE), 0, false), apebs[vtblpnum2] = mkpeb(aehdr0, avhdr0, buf1, m2, false), aehdr.valid?, vtblpnum1 < # wlar, vtblpnum2 < # wlar, bflipset-cons(bflipset0, wlar), bflipset-cons(bflipset, wlar), ubi-io-inv(apebs), ubi-io-peb-inv(mkpeb(aehdr0, avhdr0, buf1, m2, 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-peb(mkpeb(aehdr0, avhdr0, buf1, m2, false)), valid-vtbl(apebs, vols, wlar, vtblpnum4), valid-wl(apebs, wlar), bflipset = ∅ → m1 + WL_THRESHOLD ≤ m0, ⌊err0⌋ ∨ err0 = ESUCCESS ⊦ ⟪err := err0; bitflips := ?; buf0 := mkbuf(LEB_SIZE); if err = ESUCCESS then buf0 := copy(apebs[vtblpnum2].data, 0, buf0, 0, LEB_SIZE) else {n0 := 0; n := LEB_SIZE; choose buf with # buf = # buf0 ∧ range=(buf, 0, buf0, 0, n0) ∧ range=(buf, n0 + n, buf0, n0 + n, # buf0 - n0 + n) in buf0 := buf}; vols0 := vols; q0 := q; apebs0 := apebs; err1 := err, buf := buf0; if err1 = ESUCCESS then ubi_atomic_leb_change# (avhdr0.vol, avhdr0.leb, vtblpnum1, LEB_SIZE, buf, EB_PAGE_SIZE; vols, wlar, q, bflipset0, vtblpnum4, sqnum, apebs; err1); if err1 ≠ ESUCCESS then debug#("ubi: wear-leveling of PEB " + vtblpnum2.toString + " to PEB " + vtblpnum1.toString + " failed"); if err1 = ESUCCESS then {ubi_erase_worker_helper#(vtblpnum2; wlar, apebs; err1); if err1 = ESUCCESS then q := q.butlast}⟫ ( # 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(bflipset0, wlar) ∧ valid-ebatbl(apebs, wlar, vols, vtblpnum4) ∧ valid-vtbl(apebs, vols, wlar, vtblpnum4) ∧ ubi-io-inv(apebs) ∧ ( vols0 = vols ∧ id(apebs, apebs0, mapped-pebs(vols)) ∧ q.lebrefs ⊆ q0.lebrefs ++ (VTBL_VOLID × VTBL_LNUM) ∨ (∃ v, m, n. v ∈ vols0 ∧ m < # vols0[v] ∧ vols0[v][m] ≠ unmapped ∧ vols = vols0[v, vols0[v][m, ⌜n⌝ ]] ∧ id(apebs, apebs0, mapped-pebs(vols0) -- vols0[v][m].pnum) ∧ apebs[n].data = apebs0[vols0[v][m].pnum].data ∧ apebs[n].fill ≤ apebs0[vols0[v][m].pnum].fill ∧ q.lebrefs ⊆ q0.lebrefs ++ (v × m)))), vtblpnum4 = vtblpnum1, vtblpnum2 ∈ q, vtblpnum4 ∈ q, VTBL_VOLID ∈ vols

• Proof step 174:

  # apebs = # wlar, wlar[vtblpnum1] = wl-entry(m0, free), wlar[vtblpnum2] = wl-entry(m1, used), apebs[vtblpnum1] = mkpeb(aehdr, empty, mkempbuf(LEB_SIZE), 0, false), apebs[vtblpnum2] = mkpeb(aehdr0, avhdr0, buf1, m2, false), aehdr.valid?, vtblpnum1 < # wlar, vtblpnum2 < # wlar, bflipset-cons(bflipset0, wlar), bflipset-cons(bflipset, wlar), ubi-io-inv(apebs), ubi-io-peb-inv(mkpeb(aehdr0, avhdr0, buf1, m2, 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-peb(mkpeb(aehdr0, avhdr0, buf1, m2, false)), valid-vtbl(apebs, vols, wlar, vtblpnum4), valid-wl(apebs, wlar), bflipset = ∅ → m1 + WL_THRESHOLD ≤ m0 ⊦ vtblpnum4 = vtblpnum1, vtblpnum2 ∈ q, vtblpnum4 ∈ q, VTBL_VOLID ∈ vols, ∃ err0. ⌊err0⌋ ∨ err0 = ESUCCESS

Rule argument

Additional information