[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 80 from proof delta-wear-leveling (previous step)

# apebs0 = # wlar, # apebs = # wlar, # wlar1 = # wlar, avhdr0.leb = VTBL_LNUM, avhdr0.vol = VTBL_VOLID, wlar[n2] = wl-entry(m0, used), wlar[vtblpnum1] = wl-entry(m3, free), apebs[n2] = mkpeb(aehdr, avhdr0, buf1, m2, false), ecs(wlar1) = ecs(wlar), err = ESUCCESS, vtblpnum2 = n2, Δ wlar1 = Δ wlar, n2 < # wlar, vtblpnum1 < # wlar, bflipset-cons(bflipset, wlar1), bflipset-cons(bflipset0, wlar), id(apebs0, apebs, mapped-pebs(vols)), id○(apebs0, apebs, vtblpnum1), is-aligned(LEB_SIZE, EB_PAGE_SIZE), ubi-io-inv(apebs0), ubi-io-inv(apebs), ubi-io-peb-inv(mkpeb(aehdr, avhdr0, buf1, m2, false)), unique-sqns(apebs0), unique-sqns(apebs), valid-ebatbl(apebs, wlar, vols, n2), valid-ebatbl(apebs0, wlar1, vols, n0), valid-eraseq(q0), valid-eraseq(wlar1, q0), valid-eraseq(apebs0, q0), valid-eraseq(q), valid-eraseq(wlar, q), valid-eraseq(apebs, q), valid-global-sqn(apebs0, n), valid-global-sqn(apebs, n1), valid-vtbl(apebs, vols, wlar, n2), valid-vtbl(apebs0, vols, wlar1, n0), valid-wl(apebs0, wlar1), valid-wl(apebs, wlar), m0 + WL_THRESHOLD ≤ m3, err = ESUCCESS → (∀ v, m. ¬ v ∈ vols ∧ is-encoded(to-vtbl(vols)[v, m], buf1) → valid-ebatbl(apebs0, wlar1, vols[v, fill(mkebatbl(m), unmapped)], n0) ∧ valid-vtbl(apebs0, vols[v, fill(mkebatbl(m), unmapped)], wlar1, n0)), err = ESUCCESS → q0 = q + eq-entry(n2, VTBL_VOLID × VTBL_LNUM) ', err = ESUCCESS → apebs0[vtblpnum1].fill = align↑(datasize(apebs0[vtblpnum1].data, LEB_SIZE), EB_PAGE_SIZE) ∧ apebs0[vtblpnum1].data = buf1 ∧ q0.lebrefs ⊆ q.lebrefs ++ (VTBL_VOLID × VTBL_LNUM), err ≠ ESUCCESS → q0.lebrefs = q.lebrefs, err = ESUCCESS → wlar1[vtblpnum1].ec = m3 ∧ wlar1[n2].ec = m0, err = ESUCCESS ∨ ⌊err⌋ ⊦ [ubi_erase_worker_helper#(vtblpnum2; wlar1, apebs0; err); if err = ESUCCESS then q0 := q0.butlast] ( # apebs0 = # wlar1 ∧ unique-sqns(apebs0) ∧ valid-global-sqn(apebs0, n) ∧ valid-wl(apebs0, wlar1) ∧ valid-eraseq(q0) ∧ valid-eraseq(wlar1, q0) ∧ valid-eraseq(apebs0, q0) ∧ bflipset-cons(bflipset, wlar1) ∧ valid-ebatbl(apebs0, wlar1, vols, n0) ∧ valid-vtbl(apebs0, vols, wlar1, n0) ∧ ubi-io-inv(apebs0) ∧ ( id(apebs0, apebs, mapped-pebs(vols)) ∧ q0.lebrefs ⊆ q.lebrefs ++ (VTBL_VOLID × VTBL_LNUM) ∨ (∃ v, m, n. v ∈ vols ∧ m < # vols[v] ∧ vols[v][m] ≠ unmapped ∧ vols = vols[v, vols[v][m, ⌜n⌝ ]] ∧ id(apebs0, apebs, mapped-pebs(vols) -- vols[v][m].pnum) ∧ apebs0[n].data = apebs[vols[v][m].pnum].data ∧ apebs0[n].fill ≤ apebs[vols[v][m].pnum].fill ∧ q0.lebrefs ⊆ q.lebrefs ++ (v × m))) → err = ESUCCESS → Δ wlar1 < Δ wlar), vtblpnum1 = n2, VTBL_VOLID ∈ vols

Heuristic simplifier applied rule simplifier

And obtained the following new goals

Proof step 81:
# apebs0 = # wlar, # apebs = # wlar, # wlar1 = # wlar, apebs0[vtblpnum1].fill = align↑(datasize(apebs0[vtblpnum1].data, LEB_SIZE), EB_PAGE_SIZE), avhdr0.leb = VTBL_LNUM, avhdr0.vol = VTBL_VOLID, wlar[n2] = wl-entry(wlar1[n2].ec, used), wlar[vtblpnum1] = wl-entry(wlar1[vtblpnum1].ec, free), apebs[n2] = mkpeb(aehdr, avhdr0, apebs0[vtblpnum1].data, m2, false), ecs(wlar1) = ecs(wlar), Δ wlar1 = Δ wlar, vtblpnum1 ≠ n2, n2 < # wlar, vtblpnum1 < # wlar, bflipset-cons(bflipset, wlar1), bflipset-cons(bflipset0, wlar), id(apebs0, apebs, mapped-pebs(vols)), id○(apebs0, apebs, vtblpnum1), is-aligned(LEB_SIZE, EB_PAGE_SIZE), ubi-io-inv(apebs0), ubi-io-inv(apebs), ubi-io-peb-inv(mkpeb(aehdr, avhdr0, apebs0[vtblpnum1].data, m2, false)), unique-sqns(apebs0), unique-sqns(apebs), valid-ebatbl(apebs, wlar, vols, n2), valid-ebatbl(apebs0, wlar1, vols, n0), valid-eraseq(q + eq-entry(n2, VTBL_VOLID × VTBL_LNUM) '), valid-eraseq(wlar1, q + eq-entry(n2, VTBL_VOLID × VTBL_LNUM) '), valid-eraseq(apebs0, q + eq-entry(n2, VTBL_VOLID × VTBL_LNUM) '), valid-eraseq(q), valid-eraseq(wlar, q), valid-eraseq(apebs, q), valid-global-sqn(apebs0, n), valid-global-sqn(apebs, n1), valid-vtbl(apebs, vols, wlar, n2), valid-vtbl(apebs0, vols, wlar1, n0), valid-wl(apebs0, wlar1), valid-wl(apebs, wlar), wlar1[n2].ec + WL_THRESHOLD ≤ wlar1[vtblpnum1].ec, ¬ VTBL_VOLID ∈ vols, ∀ v, m. ¬ v ∈ vols ∧ is-encoded(to-vtbl(vols)[v, m], apebs0[vtblpnum1].data) → valid-ebatbl(apebs0, wlar1, vols[v, fill(mkebatbl(m), unmapped)], n0) ∧ valid-vtbl(apebs0, vols[v, fill(mkebatbl(m), unmapped)], wlar1, n0) ⊦ [ubi_erase_worker_helper#(n2; wlar1, apebs0; err); q0 := q + eq-entry(n2, VTBL_VOLID × VTBL_LNUM) '; if err = ESUCCESS then q0 := q0.butlast] ( # apebs0 = # wlar1 ∧ unique-sqns(apebs0) ∧ valid-global-sqn(apebs0, n) ∧ valid-wl(apebs0, wlar1) ∧ valid-eraseq(q0) ∧ valid-eraseq(wlar1, q0) ∧ valid-eraseq(apebs0, q0) ∧ bflipset-cons(bflipset, wlar1) ∧ valid-ebatbl(apebs0, wlar1, vols, n0) ∧ valid-vtbl(apebs0, vols, wlar1, n0) ∧ ubi-io-inv(apebs0) ∧ ( id(apebs0, apebs, mapped-pebs(vols)) ∧ q0.lebrefs ⊆ q.lebrefs ++ (VTBL_VOLID × VTBL_LNUM) ∨ (∃ v, m, n. v ∈ vols ∧ m < # vols[v] ∧ vols[v][m] ≠ unmapped ∧ vols = vols[v, vols[v][m, ⌜n⌝ ]] ∧ id(apebs0, apebs, mapped-pebs(vols) -- vols[v][m].pnum) ∧ apebs0[n].data = apebs[vols[v][m].pnum].data ∧ apebs0[n].fill ≤ apebs[vols[v][m].pnum].fill ∧ q0.lebrefs ⊆ q.lebrefs ++ (v × m))) → err = ESUCCESS → Δ wlar1 < Δ wlar)

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% ⊦ valid-vtbl(apebs, vols, wlar, n0) → n0 < # wlar; (ss)% ⊦ lref ∈ s0 ++ lref0 ↔ lref = lref0 ∨ lref ∈ s0; (s)% ⊦ s0 ⊆ s0 ++ lref; (s)% ⊦ s1 ++ lref ⊆ s2 ↔ s1 ⊆ s2 ∧ lref ∈ s2; (ws)% ⊦ (q + eq-entry(n, v × m) ').lebrefs = q.lebrefs ++ (v × m); (s)% ⊦ eqent ∈ eqent0 ' ↔ eqent = eqent0; (s)% ⊦ eqent ∈ q + q0 ↔ eqent ∈ q ∨ eqent ∈ q0; (s)%a: ⊦ (q + q0) + q1 = q + q0 + q1; from specification list[erasequeue-base]%in-15: ⊦ q + eqent ' = q0 → eqent ∈ q0; (forward) from specification list[erasequeue-base]