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

# apebs = # wlar, avhdr0.leb = VTBL_LNUM, avhdr0.vol = VTBL_VOLID, apebs[n2] = mkpeb(aehdr, avhdr0, buf1, m2, false), wlar[vtblpnum1] = wl-entry(m3, free), wlar[n2] = wl-entry(m0, used), apebs1 = apebs, n4 = n2, q1 = q, vols1 = vols, wlar0 = wlar, vtblpnum1 ≠ n2, vtblpnum1 < # wlar, n2 < # wlar, bflipset-cons(bflipset0, wlar), ubi-io-inv(apebs), ubi-io-peb-inv(mkpeb(aehdr, avhdr0, buf1, m2, false)), unique-sqns(apebs), valid-ebatbl(apebs, wlar, vols, n2), valid-eraseq(apebs, q), valid-eraseq(wlar, q), valid-eraseq(q), valid-global-sqn(apebs, n1), valid-vtbl(apebs, vols, wlar, n2), valid-wl(apebs, wlar), m0 + WL_THRESHOLD ≤ m3, ¬ VTBL_VOLID ∈ vols ⊦ [ubi_atomic_leb_change# (avhdr0.vol, avhdr0.leb, vtblpnum1, LEB_SIZE, copy(apebs[n2].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 = m3 ∧ wlar[n4].ec = m0) → [vtblpnum2 := n4; 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) ∧ ¬ VTBL_VOLID ∈ vols ∧ 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))

User applied rule insert program lemma

And obtained the following new goals

Proof step 69:
ubi-cons(apebs, vols, wlar, q, bflipset, vtblpnum, sqnum), ubi-io-inv(apebs), n0 ≤ # buf, n < # wlar, n0 ≤ LEB_SIZE, wlar[n].status = free, apebs0 = apebs, is-aligned(n0, EB_PAGE_SIZE), v ∈ vols ∧ m < # vols[v] ∨ v = VTBL_VOLID ∧ m = VTBL_LNUM, vols0 = vols, q0 = q, vtblpnum0 = vtblpnum ⊦ ⟪ubi_atomic_leb_change#(v, m, n, n0, buf, EB_PAGE_SIZE; vols, wlar, q, bflipset, vtblpnum, sqnum, apebs; err)⟫ ( (err = ESUCCESS ∨ ⌊err⌋ ) ∧ id○(apebs, apebs0, n) ∧ 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(bflipset, wlar) ∧ ( v ∈ vols0 ∨ is-encoded(to-vtbl(vols0), subarray(buf, 0, n0)) ∧ n0 = LEB_SIZE ∨ err ≠ ESUCCESS → valid-ebatbl(apebs, wlar, vols, vtblpnum) ∧ valid-vtbl(apebs, vols, wlar, vtblpnum)) ∧ ( err = ESUCCESS ∧ v = VTBL_VOLID ∧ m = VTBL_LNUM → (∀ v0, m0. ¬ v0 ∈ vols0 ∧ is-encoded(to-vtbl(vols0)[v0, m0], subarray(buf, 0, n0)) ∧ n0 = LEB_SIZE → valid-ebatbl(apebs, wlar, vols[v0, fill(mkebatbl(m0), unmapped)], vtblpnum) ∧ valid-vtbl(apebs, vols[v0, fill(mkebatbl(m0), unmapped)], wlar, vtblpnum))) ∧ (err = ESUCCESS ∧ v ∈ vols0 ∧ vols0[v][m] ≠ unmapped → q = q0 + eq-entry(vols0[v][m].pnum, v × m)) ∧ (err = ESUCCESS ∧ v = VTBL_VOLID ∧ m = VTBL_LNUM → q = q0 + eq-entry(vtblpnum0, v × m)) ∧ id(apebs, apebs0, mapped-pebs(vols0)) ∧ (v = VTBL_VOLID ∧ m = VTBL_LNUM ∨ err ≠ ESUCCESS → vols = vols0) ∧ (v ∈ vols0 ∧ err = ESUCCESS → vols = vols0[v, vols0[v][m, ⌜n⌝ ]]) ∧ ( err = ESUCCESS → apebs[n].fill = align↑(datasize(buf, n0), EB_PAGE_SIZE) ∧ apebs[n].data = subarray(buf, 0, n0) + mkempbuf(LEB_SIZE - n0) ∧ q.lebrefs ⊆ q0.lebrefs ++ (v × m)) ∧ (err ≠ ESUCCESS → q.lebrefs = q0.lebrefs))
Proof step 70:
# apebs = # wlar, avhdr0.leb = VTBL_LNUM, wlar[vtblpnum1].status = free, avhdr0.vol = VTBL_VOLID, wlar[n2] = wl-entry(m0, used), wlar[vtblpnum1] = wl-entry(m3, free), apebs[n2] = mkpeb(aehdr, avhdr0, buf1, m2, false), apebs = apebs, apebs1 = apebs, apebs2 = apebs, buf0 = copy(apebs[n2].data, 0, mkbuf(LEB_SIZE), 0, LEB_SIZE), m1 = avhdr0.leb, n2 = n2, n3 = LEB_SIZE, n4 = n2, n5 = vtblpnum1, q = q, q1 = q, q2 = q, v0 = avhdr0.vol, vols = vols, vols1 = vols, vols2 = vols, vtblpnum3 = n2, wlar0 = wlar, n2 < # wlar, vtblpnum1 < # wlar, bflipset-cons(bflipset0, wlar), is-aligned(LEB_SIZE, EB_PAGE_SIZE), ubi-cons(apebs, vols, wlar, q, bflipset0, n2, n1), ubi-io-inv(apebs), ubi-io-peb-inv(mkpeb(aehdr, avhdr0, buf1, m2, false)), unique-sqns(apebs), valid-ebatbl(apebs, wlar, vols, n2), valid-eraseq(q), valid-eraseq(wlar, q), valid-eraseq(apebs, q), valid-global-sqn(apebs, n1), valid-vtbl(apebs, vols, wlar, n2), valid-wl(apebs, wlar), m0 + WL_THRESHOLD ≤ m3, LEB_SIZE ≤ # copy(apebs[n2].data, 0, mkbuf(LEB_SIZE), 0, LEB_SIZE), LEB_SIZE ≤ LEB_SIZE, avhdr0.vol ∈ vols ∧ avhdr0.leb < # vols[avhdr0.vol] ∨ avhdr0.vol = VTBL_VOLID ∧ avhdr0.leb = VTBL_LNUM ⊦ [ubi_atomic_leb_change# (avhdr0.vol, avhdr0.leb, vtblpnum1, LEB_SIZE, copy(apebs[n2].data, 0, mkbuf(LEB_SIZE), 0, LEB_SIZE), EB_PAGE_SIZE ; vols, wlar, q, bflipset0, n2, n1, apebs ; err0)] ( (err0 = ESUCCESS ∨ ⌊err0⌋ ) ∧ id○(apebs, apebs2, n5) ∧ 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) ∧ ( v0 ∈ vols2 ∨ is-encoded(to-vtbl(vols2), subarray(buf0, 0, n3)) ∧ n3 = LEB_SIZE ∨ err0 ≠ ESUCCESS → valid-ebatbl(apebs, wlar, vols, n2) ∧ valid-vtbl(apebs, vols, wlar, n2)) ∧ ( err0 = ESUCCESS ∧ v0 = VTBL_VOLID ∧ m1 = VTBL_LNUM → (∀ v0, m0. ¬ v0 ∈ vols2 ∧ is-encoded(to-vtbl(vols2)[v0, m0], subarray(buf0, 0, n3)) ∧ n3 = LEB_SIZE → valid-ebatbl(apebs, wlar, vols[v0, fill(mkebatbl(m0), unmapped)], n2) ∧ valid-vtbl(apebs, vols[v0, fill(mkebatbl(m0), unmapped)], wlar, n2))) ∧ (err0 = ESUCCESS ∧ v0 ∈ vols2 ∧ vols2[v0][m1] ≠ unmapped → q = q2 + eq-entry(vols2[v0][m1].pnum, v0 × m1)) ∧ (err0 = ESUCCESS ∧ v0 = VTBL_VOLID ∧ m1 = VTBL_LNUM → q = q2 + eq-entry(vtblpnum3, v0 × m1)) ∧ id(apebs, apebs2, mapped-pebs(vols2)) ∧ (v0 = VTBL_VOLID ∧ m1 = VTBL_LNUM ∨ err0 ≠ ESUCCESS → vols = vols2) ∧ (v0 ∈ vols2 ∧ err0 = ESUCCESS → vols = vols2[v0, vols2[v0][m1, ⌜n5⌝ ]]) ∧ ( err0 = ESUCCESS → apebs[n5].fill = align↑(datasize(buf0, n3), EB_PAGE_SIZE) ∧ apebs[n5].data = subarray(buf0, 0, n3) + mkempbuf(LEB_SIZE - n3) ∧ q.lebrefs ⊆ q2.lebrefs ++ (v0 × m1)) ∧ (err0 ≠ ESUCCESS → q.lebrefs = q2.lebrefs) → Δ wlar = Δ wlar0 ∧ ecs(wlar) = ecs(wlar0) ∧ (err0 = ESUCCESS → wlar[vtblpnum1].ec = m3 ∧ wlar[n4].ec = m0) → [vtblpnum2 := n4; 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) ∧ ¬ VTBL_VOLID ∈ vols ∧ 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 = n2, VTBL_VOLID ∈ vols

Rule argument

spec: ubi-asm name: prepost-atomic-leb-change seq: ubi-cons(apebs, vols, wlar, q, bflipset, vtblpnum, sqnum), ubi-io-inv(apebs), n0 ≤ # buf, n < # wlar, n0 ≤ LEB_SIZE, wlar[n].status = free, apebs0 = apebs, is-aligned(n0, EB_PAGE_SIZE), v ∈ vols ∧ m < # vols[v] ∨ v = VTBL_VOLID ∧ m = VTBL_LNUM, vols0 = vols, q0 = q, vtblpnum0 = vtblpnum ⊦ ⟪ubi_atomic_leb_change# (v, m, n, n0, buf, EB_PAGE_SIZE ; vols, wlar, q, bflipset, vtblpnum, sqnum, apebs ; err)⟫ ( (err = ESUCCESS ∨ ⌊err⌋ ) ∧ id○(apebs, apebs0, n) ∧ 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(bflipset, wlar) ∧ ( v ∈ vols0 ∨ is-encoded(to-vtbl(vols0), subarray(buf, 0, n0)) ∧ n0 = LEB_SIZE ∨ err ≠ ESUCCESS → valid-ebatbl(apebs, wlar, vols, vtblpnum) ∧ valid-vtbl(apebs, vols, wlar, vtblpnum)) ∧ ( err = ESUCCESS ∧ v = VTBL_VOLID ∧ m = VTBL_LNUM → (∀ v0, m0. ¬ v0 ∈ vols0 ∧ is-encoded (to-vtbl(vols0)[v0, m0], subarray(buf, 0, n0)) ∧ n0 = LEB_SIZE → valid-ebatbl (apebs, wlar, vols[v0, fill(mkebatbl(m0), unmapped)], vtblpnum) ∧ valid-vtbl (apebs, vols[v0, fill(mkebatbl(m0), unmapped)], wlar, vtblpnum))) ∧ ( err = ESUCCESS ∧ v ∈ vols0 ∧ vols0[v][m] ≠ unmapped → q = q0 + eq-entry(vols0[v][m].pnum, v × m)) ∧ ( err = ESUCCESS ∧ v = VTBL_VOLID ∧ m = VTBL_LNUM → q = q0 + eq-entry(vtblpnum0, v × m)) ∧ id(apebs, apebs0, mapped-pebs(vols0)) ∧ ( v = VTBL_VOLID ∧ m = VTBL_LNUM ∨ err ≠ ESUCCESS → vols = vols0) ∧ ( v ∈ vols0 ∧ err = ESUCCESS → vols = vols0[v, vols0[v][m, ⌜n⌝ ]]) ∧ ( err = ESUCCESS → apebs[n].fill = align↑(datasize(buf, n0), EB_PAGE_SIZE) ∧ apebs[n].data = subarray(buf, 0, n0) + mkempbuf(LEB_SIZE - n0) ∧ q.lebrefs ⊆ q0.lebrefs ++ (v × m)) ∧ (err ≠ ESUCCESS → q.lebrefs = q0.lebrefs)) subst: [buf, n0, n, m, v, apebs, sqnum, vtblpnum, bflipset, q, wlar, vols, err, apebs0, vols0, q0, vtblpnum0] → [copy(apebs[n2].data, 0, mkbuf(LEB_SIZE), 0, LEB_SIZE), LEB_SIZE, vtblpnum1, avhdr0.leb, avhdr0.vol, apebs, n1, n2, bflipset0, q, wlar, vols, err0, apebs, vols, q, n2] flags: <all paths>

Additional information

Used simplifier rules: ⊦ ubi-cons(apebs, vols, wlar, q, bflipset, n0, n1) ↔ # 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(bflipset, wlar) ∧ valid-ebatbl(apebs, wlar, vols, n0) ∧ valid-vtbl(apebs, vols, wlar, n0); (s)% ⊦ mkpeb(aehdr, avhdr, buf, m, boolvar).data = buf; (s)%⊦ ubi-io-peb-inv(mkpeb(aehdr, avhdr, buf, n, boolvar)) → # buf = LEB_SIZE; (s)% ⊦ # mkbuf(n) = n; (s)%# buf = m, # buf0 = m ⊦ copy(buf, 0, buf0, 0, m) = buf; (s)% ⊦ m ≤ m; (s)% ⊦ is-aligned(LEB_SIZE, EB_PAGE_SIZE); (ss)% ⊦ wl-entry(m, stat).status = stat; (s)