| # apebs = # wlar, wlar[vtblpnum2] = wl-entry(m1, used), wlar[vtblpnum1] = wl-entry(m0, free), apebs[vtblpnum2] = mkpeb(aehdr, avhdr0, buf1, m2, false), buf = mkbuf(LEB_SIZE), buf0 = buf, n = LEB_SIZE, n0 = 0, vtblpnum = 0, vtblpnum0 = vtblpnum2, vtblpnum2 < # wlar, vtblpnum1 < # wlar, bflipset-cons(bflipset0, wlar), ubi-io-inv(apebs), ubi-io-peb-inv(mkpeb(aehdr, avhdr0, buf1, m2, false)), unique-sqns(apebs), valid-ebatbl(apebs, wlar, vols, n2), valid-eraseq(q), valid-eraseq(wlar, q), valid-eraseq(apebs, q), valid-global-sqn(apebs, n1), valid-vtbl(apebs, vols, wlar, n2), valid-wl(apebs, wlar), m1 + WL_THRESHOLD ≤ m0 ⊦ [abort; wlar0 := wlar; vols1 := vols; q1 := q; apebs1 := apebs; if err = ESUCCESS then ubi_atomic_leb_change#(avhdr0.vol, avhdr0.leb, vtblpnum1, LEB_SIZE, buf0, EB_PAGE_SIZE; vols, wlar, q, bflipset0, n2, n1, apebs; err); if err ≠ ESUCCESS then debug#("ubi: wear-leveling of PEB " + vtblpnum2.toString + " to PEB " + vtblpnum1.toString + " failed"); if err = ESUCCESS then {ubi_erase_worker_helper#(vtblpnum2; wlar, apebs; err); if err = ESUCCESS then q := q.butlast}] ( # apebs = # wlar ∧ unique-sqns(apebs) ∧ valid-global-sqn(apebs, n1) ∧ 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, n2) ∧ valid-vtbl(apebs, vols, wlar, n2) ∧ ubi-io-inv(apebs) ∧ ( vols1 = vols ∧ id(apebs, apebs1, mapped-pebs(vols)) ∧ q.lebrefs ⊆ q1.lebrefs ++ (VTBL_VOLID × VTBL_LNUM) ∨ (∃ v, m, n. v ∈ vols1 ∧ m < # vols1[v] ∧ vols1[v][m] ≠ unmapped ∧ vols = vols1[v, vols1[v][m, ⌜n⌝ ]] ∧ id(apebs, apebs1, mapped-pebs(vols1) -- vols1[v][m].pnum) ∧ apebs[n].data = apebs1[vols1[v][m].pnum].data ∧ apebs[n].fill ≤ apebs1[vols1[v][m].pnum].fill ∧ q.lebrefs ⊆ q1.lebrefs ++ (v × m))) → err = ESUCCESS → Δ wlar < Δ wlar0), ubi-io-read-data-pre(vtblpnum0, vtblpnum, n0, n, buf0, apebs), VTBL_VOLID ∈ vols |