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

# wlar1 = # wlar, # apebs = # wlar, # apebs0 = # wlar, # apebs1 = # wlar0, Δ wlar0 + m = Δ wlar, avhdr0.leb = VTBL_LNUM, avhdr0.vol = VTBL_VOLID, apebs[n2] = mkpeb(aehdr, avhdr0, buf, m2, false), wlar[vtblpnum1] = wl-entry(m1, free), wlar[n2] = wl-entry(m0, used), apebs0[vtblpnum1] = mkpeb(aehdr0, avhdr, buf, align↑(datasize(buf, LEB_SIZE), EB_PAGE_SIZE), boolvar), wlar1[n2] = wl-entry(m0, stat), wlar1[vtblpnum1] = wl-entry(m1, stat0), ecs(wlar1) = ecs(wlar), Δ wlar1 = Δ wlar, vtblpnum1 < # wlar, n2 < # wlar, m0 + UBI_ERASE_RETRIES < ecs(wlar).max, bflipset-cons(bflipset0, wlar), bflipset-cons(bflipset, wlar1), bflipset-cons(bflipset, wlar0), id(apebs0, apebs, mapped-pebs(vols)), id○(apebs0, apebs, vtblpnum1), is-aligned(LEB_SIZE, EB_PAGE_SIZE), ubi-io-inv(apebs), ubi-io-inv(apebs0), ubi-io-inv(apebs1), ubi-io-peb-inv(mkpeb(aehdr, avhdr0, buf, m2, false)), ubi-io-peb-inv(mkpeb(aehdr0, avhdr, buf, align↑(datasize(buf, LEB_SIZE), EB_PAGE_SIZE), boolvar)), unique-sqns(apebs), unique-sqns(apebs0), unique-sqns(apebs1), valid-ebatbl(apebs0, wlar1, vols, n0), valid-ebatbl(apebs, wlar, vols, n2), valid-ebatbl(apebs1, wlar0, vols, n0), valid-eraseq(apebs, q), valid-eraseq(wlar, q), valid-eraseq(apebs0, q + eq-entry(n2, VTBL_VOLID × VTBL_LNUM) '), valid-eraseq(wlar1, q + eq-entry(n2, VTBL_VOLID × VTBL_LNUM) '), valid-eraseq(q + eq-entry(n2, VTBL_VOLID × VTBL_LNUM) '), valid-eraseq(apebs1, q), valid-eraseq(wlar0, q), valid-eraseq(q), valid-global-sqn(apebs, n1), valid-global-sqn(apebs0, n), valid-global-sqn(apebs1, n), valid-vtbl(apebs0, vols, wlar1, n0), valid-vtbl(apebs, vols, wlar, n2), valid-vtbl(apebs1, vols, wlar0, n0), valid-wl(apebs, wlar), valid-wl(apebs0, wlar1), valid-wl(apebs1, wlar0), m ≤ UBI_ERASE_RETRIES + 1, m0 + WL_THRESHOLD ≤ m1, Δ wlar ≤ Δ wlar0, ∀ v, m. ¬ v ∈ vols ∧ is-encoded(to-vtbl(vols)[v, m], buf) → valid-ebatbl(apebs0, wlar1, vols[v, fill(mkebatbl(m), unmapped)], n0) ∧ valid-vtbl(apebs0, vols[v, fill(mkebatbl(m), unmapped)], wlar1, n0), id(apebs1, apebs, mapped-pebs(vols)) ∨ v ∈ vols ∧ m3 < # vols[v] ∧ vols[v][m3] ≠ unmapped ∧ vols = vols[v, vols[v][m3, ⌜n3⌝ ]] ∧ id(apebs1, apebs, mapped-pebs(vols) -- vols[v][m3].pnum) ∧ apebs1[n3].data = apebs[vols[v][m3].pnum].data ∧ apebs1[n3].fill ≤ apebs[vols[v][m3].pnum].fill ⊦ m = 0, vtblpnum1 = n2, VTBL_VOLID ∈ vols

Heuristic elimination applied rule insert elim lemma

And obtained the following new goals

Proof step 100:
# apebs1 = # wlar0, # apebs0 = # wlar, # apebs = # wlar, # wlar1 = # wlar, Δ wlar0 + m = Δ wlar, avhdr0.leb = VTBL_LNUM, avhdr0.vol = VTBL_VOLID, wlar1[vtblpnum1] = wl-entry(m1, stat0), wlar1[n2] = wl-entry(m0, stat), apebs0[vtblpnum1] = mkpeb(aehdr0, avhdr, buf, align↑(datasize(buf, LEB_SIZE), EB_PAGE_SIZE), boolvar), wlar[n2] = wl-entry(m0, used), wlar[vtblpnum1] = wl-entry(m1, free), apebs[n2] = mkpeb(aehdr, avhdr0, buf, m2, false), apebs1[n3] = mkpeb(aehdr1, avhdr1, buf0, m4, boolvar0), ecs(wlar1) = ecs(wlar), Δ wlar1 = Δ wlar, m0 + UBI_ERASE_RETRIES < ecs(wlar).max, n2 < # wlar, vtblpnum1 < # wlar, bflipset-cons(bflipset, wlar0), 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(apebs1), ubi-io-inv(apebs0), ubi-io-inv(apebs), ubi-io-peb-inv(mkpeb(aehdr0, avhdr, buf, align↑(datasize(buf, LEB_SIZE), EB_PAGE_SIZE), boolvar)), ubi-io-peb-inv(mkpeb(aehdr, avhdr0, buf, m2, false)), unique-sqns(apebs1), unique-sqns(apebs0), unique-sqns(apebs), valid-ebatbl(apebs1, wlar0, vols, n0), valid-ebatbl(apebs, wlar, vols, n2), valid-ebatbl(apebs0, wlar1, vols, n0), valid-eraseq(q), valid-eraseq(wlar0, q), valid-eraseq(apebs1, q), 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(wlar, q), valid-eraseq(apebs, q), valid-global-sqn(apebs1, n), valid-global-sqn(apebs0, n), valid-global-sqn(apebs, n1), valid-vtbl(apebs1, vols, wlar0, n0), valid-vtbl(apebs, vols, wlar, n2), valid-vtbl(apebs0, vols, wlar1, n0), valid-wl(apebs1, wlar0), valid-wl(apebs0, wlar1), valid-wl(apebs, wlar), Δ wlar ≤ Δ wlar0, m0 + WL_THRESHOLD ≤ m1, m ≤ UBI_ERASE_RETRIES + 1, ∀ v, m. ¬ v ∈ vols ∧ is-encoded(to-vtbl(vols)[v, m], buf) → valid-ebatbl(apebs0, wlar1, vols[v, fill(mkebatbl(m), unmapped)], n0) ∧ valid-vtbl(apebs0, vols[v, fill(mkebatbl(m), unmapped)], wlar1, n0), id(apebs1, apebs, mapped-pebs(vols)) ∨ v ∈ vols ∧ m3 < # vols[v] ∧ vols[v][m3] ≠ unmapped ∧ vols = vols[v, vols[v][m3, ⌜n3⌝ ]] ∧ id(apebs1, apebs, mapped-pebs(vols) -- vols[v][m3].pnum) ∧ buf0 = apebs[vols[v][m3].pnum].data ∧ m4 ≤ apebs[vols[v][m3].pnum].fill ⊦ m = 0, vtblpnum1 = n2, VTBL_VOLID ∈ vols

Rule argument

spec: apeb name: elim seq: ⊦ ( ( (aehdr = apeb.echdr ∧ avhdr = apeb.vidhdr) ∧ buf = apeb.data) ∧ m = apeb.fill) ∧ (boolvar ↔ apeb.bad) ↔ apeb = mkpeb(aehdr, avhdr, buf, m, boolvar) subst: [apeb, aehdr, avhdr, buf, m, boolvar] → [apebs1[n3], aehdr1, avhdr1, buf0, m4, boolvar0]

Additional information

Used simplifier rules: ⊦ ( ((aehdr = apeb.echdr ∧ avhdr = apeb.vidhdr) ∧ buf = apeb.data) ∧ m = apeb.fill) ∧ (boolvar ↔ apeb.bad) ↔ apeb = mkpeb(aehdr, avhdr, buf, m, boolvar); (elim) Used terms: apebs1[n3], aehdr1, avhdr1, buf0, m4, boolvar0