[Imprint][Data Privacy Statement][E-Mail]

View long theorem info. View the proof. Back to main index. View the specification. View theorem base summary, View theorem base listing, the used properties by spec, the dependency list, the symbol table,

Proof step 144 from proof delta-wear-leveling (previous step)

# apebs = # wlar, apebs[vtblpnum2] = mkpeb(aechdr(m1), avidhdr(v0, m3, valid-sqns(v, m, apebs).max, m5, m6), buf1, m2, false), wlar[vtblpnum1] = wl-entry(m4, free), wlar[vtblpnum2] = wl-entry(m1, used), vols[v][m] = ⌜vtblpnum2⌝ , wlar0[vtblpnum2] = wl-entry(m0, stat), apebs1 = apebs, q1 = q, vols1 = vols, vtblpnum3 = n2, wlar0 = wlar, m < # vols[v], vtblpnum1 < # wlar, vtblpnum2 < # wlar, bflipset-cons(bflipset0, wlar), is-aligned(LEB_SIZE, EB_PAGE_SIZE), ubi-io-inv(apebs), ubi-io-peb-inv(mkpeb(aechdr(m1), avidhdr(v0, m3, valid-sqns(v, m, apebs).max, m5, m6), buf1, m2, false)), unique-sqns(apebs), valid-eraseq(apebs, q), valid-eraseq(wlar, q), valid-eraseq(q), valid-global-sqn(apebs, n1), valid-peb(v, m, mkpeb(aechdr(m1), avidhdr(v0, m3, valid-sqns(v, m, apebs).max, m5, m6), buf1, m2, false)), valid-vtbl(apebs, vols, wlar, n2), v ∈ vols, m1 + WL_THRESHOLD ≤ m4 ⊦ [ubi_atomic_leb_change# (v, m, vtblpnum1, LEB_SIZE, copy(apebs[vtblpnum2].data, 0, mkbuf(LEB_SIZE), 0, LEB_SIZE), EB_PAGE_SIZE ; vols, wlar, q, bflipset0, n2, n1, apebs ; err0)] ( Δ wlar = Δ wlar0 ∧ ecs(wlar) = ecs(wlar0) ∧ (err0 = ESUCCESS → wlar[vtblpnum1].ec = m4 ∧ wlar[vtblpnum2].ec = m0) → (err0 = ESUCCESS ∨ ⌊err0⌋ ) ∧ id○(apebs, apebs1, vtblpnum1) ∧ ubi-io-inv(apebs) ∧ # 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) ∧ (v ∈ vols1 ∨ is-encoded(to-vtbl(vols1), buf1) ∨ err0 ≠ ESUCCESS → valid-ebatbl(apebs, wlar, vols, n2) ∧ valid-vtbl(apebs, vols, wlar, n2)) ∧ ( err0 = ESUCCESS ∧ v = VTBL_VOLID ∧ m = VTBL_LNUM → (∀ v, m. ¬ v ∈ vols1 ∧ is-encoded(to-vtbl(vols1)[v, m], buf1) → valid-ebatbl(apebs, wlar, vols[v, fill(mkebatbl(m), unmapped)], n2) ∧ valid-vtbl(apebs, vols[v, fill(mkebatbl(m), unmapped)], wlar, n2))) ∧ (err0 = ESUCCESS ∧ v ∈ vols1 ∧ vols1[v][m] ≠ unmapped → q = q1 + eq-entry(vols1[v][m].pnum, v × m) ') ∧ (err0 = ESUCCESS ∧ v = VTBL_VOLID ∧ m = VTBL_LNUM → q = q1 + eq-entry(vtblpnum3, VTBL_VOLID × VTBL_LNUM) ') ∧ id(apebs, apebs1, mapped-pebs(vols1)) ∧ (v = VTBL_VOLID ∧ m = VTBL_LNUM ∨ err0 ≠ ESUCCESS → vols = vols1) ∧ (v ∈ vols1 ∧ err0 = ESUCCESS → vols = vols1[v, vols1[v][m, ⌜vtblpnum1⌝ ]]) ∧ ( err0 = ESUCCESS → apebs[vtblpnum1].fill = align↑(datasize(apebs[vtblpnum1].data, LEB_SIZE), EB_PAGE_SIZE) ∧ apebs[vtblpnum1].data = buf1 ∧ q.lebrefs ⊆ q1.lebrefs ++ (v × m)) ∧ (err0 ≠ ESUCCESS → q.lebrefs = q1.lebrefs) → [if err0 ≠ ESUCCESS then debug#("ubi: wear-leveling of PEB " + vtblpnum2.toString + " to PEB " + vtblpnum1.toString + " failed"); if err0 = ESUCCESS then {ubi_erase_worker_helper#(vtblpnum2; wlar, apebs; err0); if err0 = 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) ∧ 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))) → err0 = ESUCCESS → Δ wlar < Δ wlar0)), vtblpnum1 = vtblpnum2, vtblpnum2 = n2, VTBL_VOLID ∈ vols

Heuristic simplifier applied rule simplifier

And obtained the following new goals

Proof step 145:
# apebs = # wlar, vols[v][m] = ⌜vtblpnum2⌝ , wlar[vtblpnum2] = wl-entry(m0, used), wlar[vtblpnum1] = wl-entry(m4, free), apebs[vtblpnum2] = mkpeb(aechdr(m0), avidhdr(v0, m3, valid-sqns(v, m, apebs).max, m5, m6), buf1, m2, false), apebs1 = apebs, q1 = q, vols1 = vols, vtblpnum3 = n2, wlar0 = wlar, vtblpnum1 ≠ vtblpnum2, vtblpnum2 ≠ n2, vtblpnum2 < # wlar, vtblpnum1 < # wlar, m < # vols[v], bflipset-cons(bflipset0, wlar), is-aligned(LEB_SIZE, EB_PAGE_SIZE), ubi-io-inv(apebs), ubi-io-peb-inv(mkpeb(aechdr(m0), avidhdr(v0, m3, valid-sqns(v, m, apebs).max, m5, m6), buf1, m2, false)), unique-sqns(apebs), valid-eraseq(q), valid-eraseq(wlar, q), valid-eraseq(apebs, q), valid-global-sqn(apebs, n1), valid-peb(v, m, mkpeb(aechdr(m0), avidhdr(v0, m3, valid-sqns(v, m, apebs).max, m5, m6), buf1, m2, false)), valid-vtbl(apebs, vols, wlar, n2), v ∈ vols, m0 + WL_THRESHOLD ≤ m4, ¬ VTBL_VOLID ∈ vols ⊦ [ubi_atomic_leb_change# (v, m, vtblpnum1, LEB_SIZE, copy(apebs[vtblpnum2].data, 0, mkbuf(LEB_SIZE), 0, LEB_SIZE), EB_PAGE_SIZE ; vols, wlar, q, bflipset0, n2, n1, apebs ; err0)] ( Δ wlar = Δ wlar0 ∧ ecs(wlar) = ecs(wlar0) ∧ (err0 = ESUCCESS → wlar[vtblpnum1].ec = m4 ∧ wlar[vtblpnum2].ec = m0) → (err0 = ESUCCESS ∨ ⌊err0⌋ ) ∧ id○(apebs, apebs1, vtblpnum1) ∧ ubi-io-inv(apebs) ∧ # 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) ∧ (v ∈ vols1 ∨ is-encoded(to-vtbl(vols1), buf1) ∨ err0 ≠ ESUCCESS → valid-ebatbl(apebs, wlar, vols, n2) ∧ valid-vtbl(apebs, vols, wlar, n2)) ∧ ( err0 = ESUCCESS ∧ v = VTBL_VOLID ∧ m = VTBL_LNUM → (∀ v, m. ¬ v ∈ vols1 ∧ is-encoded(to-vtbl(vols1)[v, m], buf1) → valid-ebatbl(apebs, wlar, vols[v, fill(mkebatbl(m), unmapped)], n2) ∧ valid-vtbl(apebs, vols[v, fill(mkebatbl(m), unmapped)], wlar, n2))) ∧ (err0 = ESUCCESS ∧ v ∈ vols1 ∧ vols1[v][m] ≠ unmapped → q = q1 + eq-entry(vols1[v][m].pnum, v × m) ') ∧ (err0 = ESUCCESS ∧ v = VTBL_VOLID ∧ m = VTBL_LNUM → q = q1 + eq-entry(vtblpnum3, VTBL_VOLID × VTBL_LNUM) ') ∧ id(apebs, apebs1, mapped-pebs(vols1)) ∧ (v = VTBL_VOLID ∧ m = VTBL_LNUM ∨ err0 ≠ ESUCCESS → vols = vols1) ∧ (v ∈ vols1 ∧ err0 = ESUCCESS → vols = vols1[v, vols1[v][m, ⌜vtblpnum1⌝ ]]) ∧ ( err0 = ESUCCESS → apebs[vtblpnum1].fill = align↑(datasize(apebs[vtblpnum1].data, LEB_SIZE), EB_PAGE_SIZE) ∧ apebs[vtblpnum1].data = buf1 ∧ q.lebrefs ⊆ q1.lebrefs ++ (v × m)) ∧ (err0 ≠ ESUCCESS → q.lebrefs = q1.lebrefs) → [if err0 ≠ ESUCCESS then debug#("ubi: wear-leveling of PEB " + vtblpnum2.toString + " to PEB " + vtblpnum1.toString + " failed"); if err0 = ESUCCESS then {ubi_erase_worker_helper#(vtblpnum2; wlar, apebs; err0); if err0 = 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) ∧ 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))) → err0 = ESUCCESS → Δ wlar < Δ wlar0))

Rule argument

Additional information

Used simplifier rules: ubi-io-inv-fwd: n < # apebs ⊦ apebs[n] = apeb ∧ ubi-io-inv(apebs) → ubi-io-peb-inv(apeb); (forward) from specification ubi-asm% ⊦ m < n → (n ≤ m ↔ false); (s)% ⊦ m < n ↔ ¬ n ≤ m; (ss)% ⊦ wl-entry(m, stat) = wl-entry(m0, stat0) ↔ m = m0 ∧ stat = stat0; (ws)