[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 428 from proof prepost-atomic-leb-change (previous step)

# apebs0 = # wlar, LEB_SIZE = n2 + n0, apebs0[n1] = mkpeb(aehdr, empty, mkempbuf(LEB_SIZE), 0, false), wlar[n1] = wl-entry(m1, free), vols[v][vtblpnum3] = unmapped, apebs = apebs0[n1, apebs0[n1].vidhdr:= avidhdr(v, m0, sqnum, 0, 0)], apebs1 = apebs0, buf = mkempbuf(n0) + buf0, err = ESUCCESS, err = err0, q0 = q, vols0 = vols, vtblpnum0 = vtblpnum1, vtblpnum2 = n1, vtblpnum3 = m0, aehdr.valid?, vtblpnum2 < # wlar, n1 < # apebs0, n1 < # wlar, vtblpnum3 < # vols[v], bflipset-cons(bflipset, wlar), is-aligned(n0, EB_PAGE_SIZE), ubi-io-inv(apebs0), ubi-io-inv(apebs), unique-sqns(apebs0), valid-ebatbl(apebs0, wlar, vols, vtblpnum1), valid-eraseq(apebs0, q), valid-eraseq(wlar, q), valid-eraseq(q), valid-global-sqn(apebs0, sqnum), valid-vtbl(apebs0, vols, wlar, vtblpnum1), valid-wl(apebs0, wlar), v ∈ vols, n0 ≤ LEB_SIZE, v ∈ vols ∧ m0 < # vols[v] ∨ v = VTBL_VOLID ∧ m0 = VTBL_LNUM, ⌊err0⌋ ∨ err0 = ESUCCESS ⊦ vtblpnum1 = n1, vtblpnum1 ∈ q, VTBL_VOLID ∈ vols, v = VTBL_VOLID ∧ m0 = VTBL_LNUM, (err = ESUCCESS ∨ ⌊err⌋ ) ∧ id○(apebs, apebs1, n1) ∧ ubi-io-inv(apebs) ∧ # apebs = # wlar[vtblpnum2, wl-entry(wlar[vtblpnum2].ec, used)] ∧ unique-sqns(apebs) ∧ valid-global-sqn(apebs, sqnum + 1) ∧ valid-wl(apebs, wlar[vtblpnum2, wl-entry(wlar[vtblpnum2].ec, used)]) ∧ valid-eraseq(q) ∧ valid-eraseq(wlar[vtblpnum2, wl-entry(wlar[vtblpnum2].ec, used)], q) ∧ valid-eraseq(apebs, q) ∧ ¬ VTBL_VOLID ∈ vols[v, vols[v][vtblpnum3, ⌜vtblpnum2⌝ ]] ∧ bflipset-cons(bflipset, wlar[vtblpnum2, wl-entry(wlar[vtblpnum2].ec, used)]) ∧ ( v ∈ vols0 ∨ is-encoded(to-vtbl(vols0), subarray(buf, 0, LEB_SIZE)) ∧ n0 = LEB_SIZE ∨ err ≠ ESUCCESS → valid-ebatbl(apebs, wlar[vtblpnum2, wl-entry(wlar[vtblpnum2].ec, used)], vols[v, vols[v][vtblpnum3, ⌜vtblpnum2⌝ ]], vtblpnum0) ∧ valid-vtbl(apebs, vols[v, vols[v][vtblpnum3, ⌜vtblpnum2⌝ ]], wlar[vtblpnum2, wl-entry(wlar[vtblpnum2].ec, used)], vtblpnum0)) ∧ ( err = ESUCCESS ∧ v = VTBL_VOLID ∧ m0 = VTBL_LNUM → (∀ v0, m0. ¬ v0 ∈ vols0 ∧ is-encoded(to-vtbl(vols0)[v0, m0], subarray(buf, 0, LEB_SIZE)) ∧ n0 = LEB_SIZE → valid-ebatbl (apebs, wlar[vtblpnum2, wl-entry(wlar[vtblpnum2].ec, used)], vols[v, vols[v][vtblpnum3, ⌜vtblpnum2⌝ ]][v0, fill(mkebatbl(m0), unmapped)], vtblpnum0) ∧ valid-vtbl (apebs, vols[v, vols[v][vtblpnum3, ⌜vtblpnum2⌝ ]][v0, fill(mkebatbl(m0), unmapped)], wlar[vtblpnum2, wl-entry(wlar[vtblpnum2].ec, used)], vtblpnum0))) ∧ (err = ESUCCESS ∧ v ∈ vols0 ∧ vols0[v][m0] ≠ unmapped → q = q0 + eq-entry(vols0[v][m0].pnum, v × m0) ') ∧ (err = ESUCCESS ∧ v = VTBL_VOLID ∧ m0 = VTBL_LNUM → q = q0 + eq-entry(vtblpnum1, VTBL_VOLID × VTBL_LNUM) ') ∧ id(apebs, apebs1, mapped-pebs(vols0)) ∧ (v = VTBL_VOLID ∧ m0 = VTBL_LNUM ∨ err ≠ ESUCCESS → vols[v, vols[v][vtblpnum3, ⌜vtblpnum2⌝ ]] = vols0) ∧ (v ∈ vols0 ∧ err = ESUCCESS → vols[v, vols[v][vtblpnum3, ⌜vtblpnum2⌝ ]] = vols0[v, vols0[v][m0, ⌜n1⌝ ]]) ∧ (err = ESUCCESS → apebs[n1].fill = datasize(buf, n0) ∧ apebs[n1].data = subarray(buf, 0, n0) + mkempbuf(n2) ∧ q.lebrefs ⊆ q0.lebrefs ++ (v × m0)) ∧ (err ≠ ESUCCESS → q.lebrefs = q0.lebrefs)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

Rule argument

Additional information

Used simplifier rules: ls-datasize-empbuf-append-lower: ⊦ datasize(mkempbuf(n) + buf, n) = 0;%lf-valid-wl-free-emptyvidhdr: n < # wlar, n < # apebs ⊦ wlar[n] = wl-entry(m, free) ∧ valid-wl(apebs, wlar) ∧ ubi-io-inv(apebs) → apebs[n].vidhdr = empty ∧ apebs[n].echdr.valid? ∧ apebs[n].fill = 0;%ubi-io-inv-fillcount0: n < # apebs ⊦ apebs[n] = mkpeb(aehdr, avhdr, buf, 0, false) ∧ ubi-io-inv(apebs) → (buf = mkempbuf(LEB_SIZE) ↔ true);% ⊦ mkpeb(aehdr, avhdr, buf, m, boolvar).echdr = aehdr; (s)% ⊦ mkpeb(aehdr, avhdr, buf, m, boolvar).vidhdr = avhdr; (s)% ⊦ m < n → (n ≤ m ↔ false); (s)% ⊦ m < n ↔ ¬ n ≤ m; (ss)% ⊦ mkpeb(aehdr, avhdr, buf, m, boolvar).data = buf; (s)% ⊦ mkpeb(aehdr, avhdr, buf, m, boolvar).fill = m; (s)% ⊦ wl-entry(m, stat).ec = m; (s)%⊦ mkpeb(aehdr, avhdr, buf, m, boolvar).vidhdr:= avhdr0 = mkpeb(aehdr, avhdr0, buf, m, boolvar); (s)% ⊦ m < n → n ≠ 0; (s)%f: ⊦ m < n → n ≠ 0; (forward) from specification nat-basic%lf-01: ⊦ m < n ∧ n = n0 → m < n0; (forward) from specification nat-basic%c: ⊦ m + n = n + m; from specification nat-basic% ⊦ s0 ⊆ s0 ++ lref; (s)% ⊦ mkempbuf(n0) + mkempbuf(n1) = mkempbuf(n0 + n1); (s)%n = # buf ⊦ subarray(buf + buf0, 0, n) = buf; (s)% ⊦ # mkempbuf(n) = n; (s)% ⊦ (apeb.vidhdr:= avhdr).data = apeb.data; (s)%append-a: ⊦ (buf + buf0) + buf1 = buf + buf0 + buf1; from specification array-splice[buffer]% ⊦ (apeb.vidhdr:= avhdr).fill = apeb.fill; (s)% ⊦ m < # apebs → apebs[m, apeb][m] = apeb; (s)% ⊦ id(apebs, apebs, ns); (s)%¬ n ∈ ns ⊦ id(apebs1[n, apeb], apebs0, ns) ↔ id(apebs1, apebs0, ns); (s)%n < # wlar, stat ≠ used ⊦ wlar[n] = wl-entry(m, stat) ∧ valid-ebatbl(apebs, wlar, vols, n0) → ¬ n ∈ mapped-pebs(vols); (s)% ⊦ used ≠ free; (s)%⊦ m ≠ n0 → ( valid-vtbl(apebs, vols, wlar[m, wle], n0) ↔ valid-vtbl(apebs, vols, wlar, n0)); (s)%⊦ v ∈ vols → ( valid-vtbl(apebs, vols[v, vols[v][m, ebae]], wlar, n0) ↔ valid-vtbl(apebs, vols, wlar, n0)); (s)%⊦ m ≠ n0 → ( valid-vtbl(apebs[m, apeb], vols, wlar, n0) ↔ valid-vtbl(apebs, vols, wlar, n0)); (s)%⊦ bflipset-cons(bflipset, wlar) → bflipset-cons(bflipset, wlar[m, wl-entry(n, used)]); (ss)% ⊦ v ∈ vols[v0, ebatbl] ↔ v = v0 ∨ v ∈ vols; (ws)% ⊦ # wlar[n, wle] = # wlar; (s)% ⊦ # apebs[n, apeb] = # apebs; (s)%⊦ apeb = apebs[n] ∧ apeb = apebs0[n] → (id○(apebs, apebs0, n) ↔ apebs = apebs0); (s)% ⊦ id○(apebs[n, apeb], apebs0, n) ↔ id○(apebs, apebs0, n); (s)% ⊦ ¬ ⌊ESUCCESS⌋ ; (s)