[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 320 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), lref = VTBL_VOLID × VTBL_LNUM, q0 = q, vtblpnum = vtblpnum1, aehdr.valid?, n1 < # wlar[vtblpnum, wlar[vtblpnum].status:= erasing], vtblpnum < # wlar, n1 < # wlar, bflipset-cons(bflipset, wlar), is-aligned(n0, EB_PAGE_SIZE), ubi-io-inv(apebs0), ubi-io-inv(apebs0[n1, mkpeb(aehdr, avidhdr(VTBL_VOLID, VTBL_LNUM, sqnum, 0, 0), mkempbuf(LEB_SIZE), 0, false)]), 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), n0 ≤ LEB_SIZE ⊦ vtblpnum1 = n1, VTBL_VOLID ∈ vols, vtblpnum1 ∈ q, # apebs0 = # wlar[vtblpnum, wlar[vtblpnum].status:= erasing][n1, wl-entry(wlar[vtblpnum, wlar[vtblpnum].status:= erasing][n1].ec, used)] ∧ unique-sqns(apebs0[n1, apebs0[n1].vidhdr:= avidhdr(VTBL_VOLID, VTBL_LNUM, sqnum, 0, 0)]) ∧ valid-global-sqn(apebs0[n1, apebs0[n1].vidhdr:= avidhdr(VTBL_VOLID, VTBL_LNUM, sqnum, 0, 0)], sqnum + 1) ∧ valid-wl (apebs0[n1, apebs0[n1].vidhdr:= avidhdr(VTBL_VOLID, VTBL_LNUM, sqnum, 0, 0)], wlar[vtblpnum, wlar[vtblpnum].status:= erasing][n1, wl-entry(wlar[vtblpnum, wlar[vtblpnum].status:= erasing][n1].ec, used)]) ∧ valid-eraseq(q0 + eq-entry(vtblpnum1, VTBL_VOLID × VTBL_LNUM) ') ∧ valid-eraseq (wlar[vtblpnum, wlar[vtblpnum].status:= erasing][n1, wl-entry(wlar[vtblpnum, wlar[vtblpnum].status:= erasing][n1].ec, used)], q0 + eq-entry(vtblpnum1, VTBL_VOLID × VTBL_LNUM) ') ∧ valid-eraseq(apebs0[n1, apebs0[n1].vidhdr:= avidhdr(VTBL_VOLID, VTBL_LNUM, sqnum, 0, 0)], q0 + eq-entry(vtblpnum1, VTBL_VOLID × VTBL_LNUM) ') ∧ bflipset-cons (bflipset -- vtblpnum1, wlar[vtblpnum, wlar[vtblpnum].status:= erasing][n1, wl-entry(wlar[vtblpnum, wlar[vtblpnum].status:= erasing][n1].ec, used)]) ∧ ( is-encoded(to-vtbl(vols), mkempbuf(LEB_SIZE)) ∧ n0 = LEB_SIZE → valid-ebatbl (apebs0[n1, apebs0[n1].vidhdr:= avidhdr(VTBL_VOLID, VTBL_LNUM, sqnum, 0, 0)], wlar[vtblpnum, wlar[vtblpnum].status:= erasing][n1, wl-entry(wlar[vtblpnum, wlar[vtblpnum].status:= erasing][n1].ec, used)], vols, n1) ∧ valid-vtbl (apebs0[n1, apebs0[n1].vidhdr:= avidhdr(VTBL_VOLID, VTBL_LNUM, sqnum, 0, 0)], vols, wlar[vtblpnum, wlar[vtblpnum].status:= erasing][n1, wl-entry(wlar[vtblpnum, wlar[vtblpnum].status:= erasing][n1].ec, used)], n1)) ∧ (∀ v, m. ¬ v ∈ vols ∧ is-encoded(to-vtbl(vols)[v, m], mkempbuf(LEB_SIZE)) ∧ n0 = LEB_SIZE → valid-ebatbl (apebs0[n1, apebs0[n1].vidhdr:= avidhdr(VTBL_VOLID, VTBL_LNUM, sqnum, 0, 0)], wlar[vtblpnum, wlar[vtblpnum].status:= erasing][n1, wl-entry(wlar[vtblpnum, wlar[vtblpnum].status:= erasing][n1].ec, used)], vols[v, fill(mkebatbl(m), unmapped)], n1) ∧ valid-vtbl (apebs0[n1, apebs0[n1].vidhdr:= avidhdr(VTBL_VOLID, VTBL_LNUM, sqnum, 0, 0)], vols[v, fill(mkebatbl(m), unmapped)], wlar[vtblpnum, wlar[vtblpnum].status:= erasing][n1, wl-entry(wlar[vtblpnum, wlar[vtblpnum].status:= erasing][n1].ec, used)], n1)) ∧ q + eq-entry(vtblpnum, lref) = q0 + eq-entry(vtblpnum1, VTBL_VOLID × VTBL_LNUM) ' ∧ id(apebs0[n1, apebs0[n1].vidhdr:= avidhdr(VTBL_VOLID, VTBL_LNUM, sqnum, 0, 0)], apebs0, mapped-pebs(vols)) ∧ apebs0[n1].data = mkempbuf(LEB_SIZE)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

Rule argument

Additional information

Used simplifier rules: ubi-io-inv-fillcount0: n < # apebs ⊦ apebs[n] = mkpeb(aehdr, avhdr, buf, 0, false) ∧ ubi-io-inv(apebs) → (buf = mkempbuf(LEB_SIZE) ↔ true);% ⊦ eq-entry(m, lref).pnum = m; (s)% ⊦ valid-eraseq(q + eqent ') ↔ ¬ eqent.pnum ∈ q ∧ valid-eraseq(q); (ss)% ⊦ m < n → (n ≤ m ↔ false); (s)% ⊦ m < n ↔ ¬ n ≤ m; (ss)% ⊦ mkpeb(aehdr, avhdr, buf, m, boolvar).data = buf; (s)% ⊦ wl-entry(m, stat).ec = m; (s)%⊦ mkpeb(aehdr, avhdr, buf, m, boolvar).vidhdr:= avhdr0 = mkpeb(aehdr, avhdr0, buf, m, boolvar); (s)%lf-01: ⊦ m < n ∧ n = n0 → m < n0; (forward) from specification nat-basic% ⊦ 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)%a: ⊦ (q + q0) + q1 = q + q0 + q1; from specification list[erasequeue-base]% ⊦ q + q0 = q + q1 ↔ q0 = q1; (s)% ⊦ q + eqent = q + eqent '; (s)% ⊦ m ≠ n → wlar[n, wle][m] = wlar[m]; (s)% ⊦ # wlar[n, wle] = # wlar; (s)% ⊦ wle.status:= stat = wl-entry(wle.ec, stat); (s)