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

# apebs1 = # wlar0, # wlar1 = # wlar, # apebs = # wlar, # apebs0 = # wlar, Δ wlar0 + m0 = Δ wlar, wlar1[vtblpnum1] = wl-entry(m4, stat0), wlar1[vtblpnum2] = wl-entry(m1, stat), apebs0[vtblpnum1] = mkpeb(aehdr, avhdr, buf, align↑(datasize(buf, LEB_SIZE), EB_PAGE_SIZE), boolvar), apebs[vtblpnum2] = mkpeb(aechdr(m1), avidhdr(v0, m3, valid-sqns(v, m, apebs).max, m5, m6), buf, m2, false), wlar[vtblpnum1] = wl-entry(m4, free), wlar[vtblpnum2] = wl-entry(m1, used), vols[v][m] = ⌜vtblpnum2⌝ , ecs(wlar1) = ecs(wlar), err = ESUCCESS, q0 = q + eq-entry(vtblpnum2, v × m) ', Δ wlar1 = Δ wlar, m1 + UBI_ERASE_RETRIES < ecs(wlar).max, vtblpnum2 < # wlar, m < # vols[v], vtblpnum1 < # wlar, bflipset-cons(bflipset, wlar0), bflipset-cons(bflipset0, wlar), bflipset-cons(bflipset, wlar1), id(apebs0, apebs, mapped-pebs(vols)), id○(apebs0, apebs, vtblpnum1), is-aligned(LEB_SIZE, EB_PAGE_SIZE), ubi-io-inv(apebs1), ubi-io-inv(apebs), ubi-io-inv(apebs0), ubi-io-peb-inv(mkpeb(aehdr, avhdr, buf, align↑(datasize(buf, LEB_SIZE), EB_PAGE_SIZE), boolvar)), ubi-io-peb-inv(mkpeb(aechdr(m1), avidhdr(v0, m3, valid-sqns(v, m, apebs).max, m5, m6), buf, m2, false)), unique-sqns(apebs1), unique-sqns(apebs), unique-sqns(apebs0), valid-ebatbl(apebs1, wlar0, vols[v, vols[v][m, ⌜vtblpnum1⌝ ]], n0), valid-ebatbl(apebs0, wlar1, vols[v, vols[v][m, ⌜vtblpnum1⌝ ]], n0), valid-eraseq(q0.butlast), valid-eraseq(wlar0, q0.butlast), valid-eraseq(apebs1, q0.butlast), valid-eraseq(apebs, q), valid-eraseq(wlar, q), valid-eraseq(q), valid-eraseq(apebs0, q + eq-entry(vtblpnum2, v × m) '), valid-eraseq(wlar1, q + eq-entry(vtblpnum2, v × m) '), valid-eraseq(q + eq-entry(vtblpnum2, v × m) '), valid-global-sqn(apebs1, n), valid-global-sqn(apebs, n1), valid-global-sqn(apebs0, n), valid-peb(v, m, mkpeb(aechdr(m1), avidhdr(v0, m3, valid-sqns(v, m, apebs).max, m5, m6), buf, m2, false)), 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), v ∈ vols, m1 + WL_THRESHOLD ≤ m4, m0 ≤ UBI_ERASE_RETRIES + 1, vols = vols[v, vols[v][m, ⌜vtblpnum1⌝ ]] ∧ id(apebs1, apebs, mapped-pebs(vols[v, vols[v][m, ⌜vtblpnum1⌝ ]])) ∧ q0.butlast.lebrefs ⊆ q.lebrefs ++ (VTBL_VOLID × VTBL_LNUM) ∨ (∃ v0, m0, n. v0 ∈ vols ∧ m0 < # vols[v0] ∧ vols[v0][m0] ≠ unmapped ∧ vols[v, vols[v][m, ⌜vtblpnum1⌝ ]] = vols[v0, vols[v0][m0, ⌜n⌝ ]] ∧ id(apebs1, apebs, mapped-pebs(vols) -- vols[v0][m0].pnum) ∧ apebs1[n].data = apebs[vols[v0][m0].pnum].data ∧ apebs1[n].fill ≤ apebs[vols[v0][m0].pnum].fill ∧ q0.butlast.lebrefs ⊆ q.lebrefs ++ (v0 × m0)) ⊦ m0 = 0, q0 = [], vtblpnum1 = vtblpnum2, vtblpnum2 = n2, Δ wlar0 < Δ wlar, VTBL_VOLID ∈ vols

Heuristic simplifier applied rule simplifier

And obtained the following new goals

Proof step 172:
# apebs0 = # wlar, # apebs = # wlar, # wlar1 = # wlar, # apebs1 = # wlar0, Δ wlar0 + m0 = Δ wlar, vols[v][m] = ⌜vtblpnum2⌝ , wlar[vtblpnum2] = wl-entry(m1, used), wlar[vtblpnum1] = wl-entry(m4, free), apebs[vtblpnum2] = mkpeb(aechdr(m1), avidhdr(v0, m3, valid-sqns(v, m, apebs).max, m5, m6), buf, m2, false), apebs0[vtblpnum1] = mkpeb(aehdr, avhdr, buf, align↑(datasize(buf, LEB_SIZE), EB_PAGE_SIZE), boolvar), wlar1[vtblpnum2] = wl-entry(m1, stat), wlar1[vtblpnum1] = wl-entry(m4, stat0), ecs(wlar1) = ecs(wlar), Δ wlar1 = Δ wlar, vtblpnum1 < # wlar, m < # vols[v], vtblpnum2 < # wlar, m1 + UBI_ERASE_RETRIES < ecs(wlar).max, bflipset-cons(bflipset, wlar1), bflipset-cons(bflipset0, wlar), bflipset-cons(bflipset, wlar0), 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-inv(apebs1), ubi-io-peb-inv(mkpeb(aechdr(m1), avidhdr(v0, m3, valid-sqns(v, m, apebs).max, m5, m6), buf, m2, false)), ubi-io-peb-inv(mkpeb(aehdr, avhdr, buf, align↑(datasize(buf, LEB_SIZE), EB_PAGE_SIZE), boolvar)), unique-sqns(apebs0), unique-sqns(apebs), unique-sqns(apebs1), valid-ebatbl(apebs0, wlar1, vols[v, vols[v][m, ⌜vtblpnum1⌝ ]], n0), valid-ebatbl(apebs1, wlar0, vols[v, vols[v][m, ⌜vtblpnum1⌝ ]], n0), valid-eraseq(q + eq-entry(vtblpnum2, v × m) '), valid-eraseq(wlar1, q + eq-entry(vtblpnum2, v × m) '), valid-eraseq(apebs0, q + eq-entry(vtblpnum2, v × m) '), valid-eraseq(wlar, q), valid-eraseq(apebs, q), valid-eraseq(apebs1, q), valid-eraseq(wlar0, q), valid-eraseq(q), valid-global-sqn(apebs0, n), valid-global-sqn(apebs, n1), valid-global-sqn(apebs1, n), valid-peb(v, m, mkpeb(aechdr(m1), avidhdr(v0, m3, valid-sqns(v, m, apebs).max, m5, m6), buf, m2, false)), valid-vtbl(apebs0, vols, wlar1, n0), valid-vtbl(apebs, vols, wlar, n2), valid-vtbl(apebs1, vols, wlar0, n0), valid-wl(apebs0, wlar1), valid-wl(apebs1, wlar0), v ∈ vols, m0 ≤ UBI_ERASE_RETRIES + 1, m1 + WL_THRESHOLD ≤ m4, Δ wlar ≤ Δ wlar0, vols = vols[v, vols[v][m, ⌜vtblpnum1⌝ ]] ∧ id(apebs1, apebs, mapped-pebs(vols[v, vols[v][m, ⌜vtblpnum1⌝ ]])) ∨ v1 ∈ vols ∧ m7 < # vols[v1] ∧ vols[v1][m7] ≠ unmapped ∧ vols[v, vols[v][m, ⌜vtblpnum1⌝ ]] = vols[v1, vols[v1][m7, ⌜n3⌝ ]] ∧ id(apebs1, apebs, mapped-pebs(vols) -- vols[v1][m7].pnum) ∧ apebs1[n3].data = apebs[vols[v1][m7].pnum].data ∧ apebs1[n3].fill ≤ apebs[vols[v1][m7].pnum].fill ⊦ m0 = 0, vtblpnum1 = vtblpnum2, vtblpnum2 = n2, VTBL_VOLID ∈ vols

Rule argument

Additional information

Used simplifier rules: ⊦ s0 ⊆ s0 ++ lref; (s)% ⊦ m < n ↔ ¬ n ≤ m; (ss)% ⊦ (q + eqent ').butlast = q; (s)%a: ⊦ (q + q0) + q1 = q + q0 + q1; from specification list[erasequeue-base]% ⊦ q + eqent ' ≠ []; (s)