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

# apebs = # wlar, wlar[vtblpnum1].status = free, 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), apebs = apebs, apebs0 = apebs, apebs1 = apebs, buf0 = copy(buf, 0, mkbuf(LEB_SIZE), 0, LEB_SIZE), m2 = avhdr.leb, n1 = LEB_SIZE, n2 = vtblpnum1, q = q, q0 = q, q1 = q, v0 = avhdr.vol, vols = vols, vols0 = vols, vols1 = vols, vtblpnum3 = vtblpnum4, vtblpnum4 = vtblpnum4, aehdr.valid?, vtblpnum2 < # wlar, vtblpnum1 < # wlar, bflipset-cons(bflipset, wlar), bflipset-cons(bflipset0, wlar), is-aligned(LEB_SIZE, EB_PAGE_SIZE), ubi-cons(apebs, vols, wlar, q, bflipset0, vtblpnum4, sqnum), 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(q), valid-eraseq(wlar, q), valid-eraseq(apebs, q), valid-global-sqn(apebs, sqnum), valid-peb(mkpeb(aehdr1, avhdr, buf, m3, false)), valid-vtbl(apebs, vols, wlar, vtblpnum4), valid-wl(apebs, wlar), LEB_SIZE ≤ # copy(buf, 0, mkbuf(LEB_SIZE), 0, LEB_SIZE), LEB_SIZE ≤ LEB_SIZE, bflipset = ∅ → m1 + WL_THRESHOLD ≤ m0, avhdr.vol ∈ vols ∧ avhdr.leb < # vols[avhdr.vol] ∨ avhdr.vol = VTBL_VOLID ∧ avhdr.leb = VTBL_LNUM ⊦ [ubi_atomic_leb_change# (avhdr.vol, avhdr.leb, vtblpnum1, LEB_SIZE, copy(buf, 0, mkbuf(LEB_SIZE), 0, LEB_SIZE), EB_PAGE_SIZE ; vols, wlar, q, bflipset0, vtblpnum4, sqnum, apebs ; err0)] ( (err0 = ESUCCESS ∨ ⌊err0⌋ ) ∧ id○(apebs, apebs1, n2) ∧ 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) ∧ ( v0 ∈ vols1 ∨ is-encoded(to-vtbl(vols1), subarray(buf0, 0, n1)) ∧ n1 = LEB_SIZE ∨ err0 ≠ ESUCCESS → valid-ebatbl(apebs, wlar, vols, vtblpnum4) ∧ valid-vtbl(apebs, vols, wlar, vtblpnum4)) ∧ ( err0 = ESUCCESS ∧ v0 = VTBL_VOLID ∧ m2 = VTBL_LNUM → (∀ v0, m0. ¬ v0 ∈ vols1 ∧ is-encoded(to-vtbl(vols1)[v0, m0], subarray(buf0, 0, n1)) ∧ n1 = LEB_SIZE → valid-ebatbl(apebs, wlar, vols[v0, fill(mkebatbl(m0), unmapped)], vtblpnum4) ∧ valid-vtbl(apebs, vols[v0, fill(mkebatbl(m0), unmapped)], wlar, vtblpnum4))) ∧ (err0 = ESUCCESS ∧ v0 ∈ vols1 ∧ vols1[v0][m2] ≠ unmapped → q = q1 + eq-entry(vols1[v0][m2].pnum, v0 × m2)) ∧ (err0 = ESUCCESS ∧ v0 = VTBL_VOLID ∧ m2 = VTBL_LNUM → q = q1 + eq-entry(vtblpnum3, v0 × m2)) ∧ id(apebs, apebs1, mapped-pebs(vols1)) ∧ (v0 = VTBL_VOLID ∧ m2 = VTBL_LNUM ∨ err0 ≠ ESUCCESS → vols = vols1) ∧ (v0 ∈ vols1 ∧ err0 = ESUCCESS → vols = vols1[v0, vols1[v0][m2, ⌜n2⌝ ]]) ∧ ( err0 = ESUCCESS → apebs[n2].fill = align↑(datasize(buf0, n1), EB_PAGE_SIZE) ∧ apebs[n2].data = subarray(buf0, 0, n1) + mkempbuf(LEB_SIZE - n1) ∧ q.lebrefs ⊆ q1.lebrefs ++ (v0 × m2)) ∧ (err0 ≠ ESUCCESS → q.lebrefs = q1.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) ∧ ¬ VTBL_VOLID ∈ vols ∧ 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

Rule argument

Additional information

Used simplifier rules: ⊦ wl-entry(m, stat).status = stat; (s)%append-a: ⊦ (buf + buf0) + buf1 = buf + buf0 + buf1; from specification array-splice[buffer]% ⊦ buf + mkempbuf(0) = buf; (s)% ⊦ m - m = 0; (s)% ⊦ q + eqent = q + eqent '; (s)%# buf = n ⊦ subarray(buf, 0, n) = buf; (s)%⊦ 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)%# buf = m, # buf0 = m ⊦ copy(buf, 0, buf0, 0, m) = buf; (s)% ⊦ # mkbuf(n) = n; (s)%⊦ ubi-io-peb-inv(mkpeb(aehdr, avhdr, buf, n, boolvar)) → # buf = LEB_SIZE; (s)% ⊦ m ≤ m; (s)