[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 76 from proof inv-wl-worker (previous step)

# 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(aehdr1, avhdr, buf, m3, false), apebs0 = apebs, q0 = q, vols0 = vols, vtblpnum3 = vtblpnum4, aehdr.valid?, vtblpnum1 < # wlar, vtblpnum2 < # wlar, bflipset-cons(bflipset0, wlar), bflipset-cons(bflipset, wlar), is-aligned(LEB_SIZE, EB_PAGE_SIZE), ubi-io-inv(apebs), ubi-io-peb-inv(mkpeb(aehdr1, avhdr, buf, m3, 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(aehdr1, avhdr, buf, m3, false)), valid-vtbl(apebs, vols, wlar, vtblpnum4), valid-wl(apebs, wlar), bflipset = ∅ → m1 + WL_THRESHOLD ≤ m0, avhdr.vol ∈ vols ∧ avhdr.leb < # vols[avhdr.vol] ∨ avhdr.vol = VTBL_VOLID ∧ avhdr.leb = VTBL_LNUM ⊦ ∀ vols, wlar, q, bflipset0, vtblpnum4, sqnum, apebs, err0. (err0 = ESUCCESS ∨ ⌊err0⌋ ) ∧ id○(apebs, apebs0, vtblpnum1) ∧ ubi-io-inv(apebs) ∧ # 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) ∧ ( avhdr.vol ∈ vols0 ∨ is-encoded(to-vtbl(vols0), buf) ∨ err0 ≠ ESUCCESS → valid-ebatbl(apebs, wlar, vols, vtblpnum4) ∧ valid-vtbl(apebs, vols, wlar, vtblpnum4)) ∧ ( err0 = ESUCCESS ∧ avhdr.vol = VTBL_VOLID ∧ avhdr.leb = VTBL_LNUM → (∀ v, m. ¬ v ∈ vols0 ∧ is-encoded(to-vtbl(vols0)[v, m], buf) → valid-ebatbl(apebs, wlar, vols[v, fill(mkebatbl(m), unmapped)], vtblpnum4) ∧ valid-vtbl(apebs, vols[v, fill(mkebatbl(m), unmapped)], wlar, vtblpnum4))) ∧ ( err0 = ESUCCESS ∧ avhdr.vol ∈ vols0 ∧ vols0[avhdr.vol][avhdr.leb] ≠ unmapped → q = q0 + eq-entry(vols0[avhdr.vol][avhdr.leb].pnum, avhdr.vol × avhdr.leb) ') ∧ (err0 = ESUCCESS ∧ avhdr.vol = VTBL_VOLID ∧ avhdr.leb = VTBL_LNUM → q = q0 + eq-entry(vtblpnum3, avhdr.vol × avhdr.leb) ') ∧ id(apebs, apebs0, mapped-pebs(vols0)) ∧ (avhdr.vol = VTBL_VOLID ∧ avhdr.leb = VTBL_LNUM ∨ err0 ≠ ESUCCESS → vols = vols0) ∧ (avhdr.vol ∈ vols0 ∧ err0 = ESUCCESS → vols = vols0[avhdr.vol, vols0[avhdr.vol][avhdr.leb, ⌜vtblpnum1⌝ ]]) ∧ ( err0 = ESUCCESS → apebs[vtblpnum1].fill = align↑(datasize(apebs[vtblpnum1].data, LEB_SIZE), EB_PAGE_SIZE) ∧ apebs[vtblpnum1].data = buf ∧ q.lebrefs ⊆ q0.lebrefs ++ (avhdr.vol × avhdr.leb)) ∧ (err0 ≠ ESUCCESS → q.lebrefs = q0.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, sqnum) ∧ valid-wl(apebs, wlar) ∧ valid-eraseq(q) ∧ valid-eraseq(wlar, q) ∧ valid-eraseq(apebs, q) ∧ 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, VTBL_VOLID ∈ vols, vtblpnum4 ∈ q, vtblpnum2 ∈ q

Heuristic simplifier applied rule simplifier

And obtained the following new goals

Proof step 77:
# apebs1 = # wlar, # apebs = # wlar, # wlar0 = # wlar, apebs[vtblpnum2] = mkpeb(aehdr1, avhdr, buf, m3, false), apebs[vtblpnum1] = mkpeb(aehdr, empty, mkempbuf(LEB_SIZE), 0, false), wlar[vtblpnum2] = wl-entry(m1, used), wlar[vtblpnum1] = wl-entry(m0, free), vtblpnum4 ≠ vtblpnum1, aehdr.valid?, vtblpnum2 < # wlar, vtblpnum1 < # wlar, bflipset-cons(bflipset1, wlar0), bflipset-cons(bflipset, wlar), bflipset-cons(bflipset0, wlar), id(apebs1, apebs, mapped-pebs(vols)), id○(apebs1, apebs, vtblpnum1), is-aligned(LEB_SIZE, EB_PAGE_SIZE), ubi-io-inv(apebs1), ubi-io-inv(apebs), ubi-io-peb-inv(mkpeb(aehdr1, avhdr, buf, m3, false)), unique-sqns(apebs1), unique-sqns(apebs), valid-ebatbl(apebs, wlar, vols, vtblpnum4), valid-eraseq(q1), valid-eraseq(wlar0, q1), valid-eraseq(apebs1, q1), valid-eraseq(q), valid-eraseq(wlar, q), valid-eraseq(apebs, q), valid-global-sqn(apebs1, sqnum0), valid-global-sqn(apebs, sqnum), valid-peb(mkpeb(aehdr1, avhdr, buf, m3, false)), valid-vtbl(apebs, vols, wlar, vtblpnum4), valid-wl(apebs1, wlar0), valid-wl(apebs, wlar), ¬ vtblpnum2 ∈ q, ¬ vtblpnum4 ∈ q, ¬ VTBL_VOLID ∈ vols, ¬ VTBL_VOLID ∈ vols1, avhdr.vol ∈ vols ∨ is-encoded(to-vtbl(vols), buf) ∨ err ≠ ESUCCESS → valid-ebatbl(apebs1, wlar0, vols1, vtblpnum) ∧ valid-vtbl(apebs1, vols1, wlar0, vtblpnum), err = ESUCCESS ∧ avhdr.vol = VTBL_VOLID ∧ avhdr.leb = VTBL_LNUM → (∀ v, m. ¬ v ∈ vols ∧ is-encoded(to-vtbl(vols)[v, m], buf) → valid-ebatbl(apebs1, wlar0, vols1[v, fill(mkebatbl(m), unmapped)], vtblpnum) ∧ valid-vtbl(apebs1, vols1[v, fill(mkebatbl(m), unmapped)], wlar0, vtblpnum)), err = ESUCCESS ∧ avhdr.vol ∈ vols ∧ vols[avhdr.vol][avhdr.leb] ≠ unmapped → q1 = q + eq-entry(vols[avhdr.vol][avhdr.leb].pnum, avhdr.vol × avhdr.leb) ', err = ESUCCESS ∧ avhdr.vol = VTBL_VOLID ∧ avhdr.leb = VTBL_LNUM → q1 = q + eq-entry(vtblpnum4, avhdr.vol × avhdr.leb) ', avhdr.vol = VTBL_VOLID ∧ avhdr.leb = VTBL_LNUM ∨ err ≠ ESUCCESS → vols1 = vols, avhdr.vol ∈ vols ∧ err = ESUCCESS → vols1 = vols[avhdr.vol, vols[avhdr.vol][avhdr.leb, ⌜vtblpnum1⌝ ]], err = ESUCCESS → apebs1[vtblpnum1].fill = align↑(datasize(apebs1[vtblpnum1].data, LEB_SIZE), EB_PAGE_SIZE) ∧ apebs1[vtblpnum1].data = buf ∧ q1.lebrefs ⊆ q.lebrefs ++ (avhdr.vol × avhdr.leb), err ≠ ESUCCESS → q1.lebrefs = q.lebrefs, bflipset = ∅ → m1 + WL_THRESHOLD ≤ m0, err = ESUCCESS ∨ ⌊err⌋ , avhdr.vol ∈ vols ∧ avhdr.leb < # vols[avhdr.vol] ∨ avhdr.vol = VTBL_VOLID ∧ avhdr.leb = VTBL_LNUM ⊦ ⟪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; wlar0, apebs1; err); if err = ESUCCESS then q1 := q1.butlast}⟫ ( # apebs1 = # wlar0 ∧ unique-sqns(apebs1) ∧ valid-global-sqn(apebs1, sqnum0) ∧ valid-wl(apebs1, wlar0) ∧ valid-eraseq(q1) ∧ valid-eraseq(wlar0, q1) ∧ valid-eraseq(apebs1, q1) ∧ bflipset-cons(bflipset1, wlar0) ∧ valid-ebatbl(apebs1, wlar0, vols1, vtblpnum) ∧ valid-vtbl(apebs1, vols1, wlar0, vtblpnum) ∧ ubi-io-inv(apebs1) ∧ ( vols = vols1 ∧ id(apebs1, apebs, mapped-pebs(vols1)) ∧ q1.lebrefs ⊆ q.lebrefs ++ (VTBL_VOLID × VTBL_LNUM) ∨ (∃ v, m, n. v ∈ vols ∧ m < # vols[v] ∧ vols[v][m] ≠ unmapped ∧ vols1 = vols[v, vols[v][m, ⌜n⌝ ]] ∧ id(apebs1, apebs, mapped-pebs(vols) -- vols[v][m].pnum) ∧ apebs1[n].data = apebs[vols[v][m].pnum].data ∧ apebs1[n].fill ≤ apebs[vols[v][m].pnum].fill ∧ q1.lebrefs ⊆ q.lebrefs ++ (v × m))))

Rule argument

Additional information

Used simplifier rules: lf-01: ⊦ m < n ∧ n = n0 → m < n0; (forward) from specification nat-basic%idexcept-size: ⊦ id○(apebs, apebs0, n) → # apebs = # apebs0; (forward) from specification array-copy[apebs]