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

# apebs0 = # wlar, LEB_SIZE = n2 + n0, LEB_SIZE = n4 + # buf1, apebs0[n1] = mkpeb(aehdr, empty, mkempbuf(LEB_SIZE), 0, false), wlar[n1] = wl-entry(m1, free), align↑(datasize(buf, n0), EB_PAGE_SIZE) = n3 + # buf1, lref = none, q0 = q, vtblpnum = n1, aehdr.valid?, n1 < # wlar, vtblpnum < # wlar, bflipset-cons(bflipset, wlar), is-aligned(n0, EB_PAGE_SIZE), is-aligned(# buf1, EB_PAGE_SIZE), ubi-io-inv (apebs0[n1, mkpeb(aehdr, avidhdr(v, m0, sqnum, datasize(buf, n0), checksum(buf, datasize(buf, n0))), buf1 + mkempbuf(n4), # buf1, false)]), ubi-io-inv(apebs0[n1, mkpeb(aehdr, avidhdr(v, m0, sqnum, datasize(buf, n0), checksum(buf, datasize(buf, n0))), mkempbuf(LEB_SIZE), 0, false)]), ubi-io-inv(apebs0), 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), n3 + # buf1 ≤ # buf, n3 + # buf1 ≤ LEB_SIZE, n0 ≤ LEB_SIZE, n0 ≤ # buf, # buf1 ≤ # buf, # buf1 ≤ LEB_SIZE, ⌊err0⌋ , v ∈ vols ∧ m0 < # vols[v] ∨ v = VTBL_VOLID ∧ m0 = VTBL_LNUM, datasize(buf1, # buf1) < datasize(buf, n0) ∨ checksum(buf1 + mkempbuf(n3), datasize(buf, n0)) ≠ checksum(buf, datasize(buf, n0)) ⊦ vtblpnum1 = n1, vtblpnum1 ∈ q, VTBL_VOLID ∈ vols, ∃ buf0. buf = mkempbuf(n0) + buf0, # apebs0 = # wlar[vtblpnum, wlar[vtblpnum].status:= erasing] ∧ unique-sqns (apebs0[n1, mkpeb(aehdr, avidhdr(v, m0, sqnum, datasize(buf, n0), checksum(buf, datasize(buf, n0))), buf1 + mkempbuf(n4), # buf1, false)]) ∧ valid-global-sqn (apebs0[n1, mkpeb(aehdr, avidhdr(v, m0, sqnum, datasize(buf, n0), checksum(buf, datasize(buf, n0))), buf1 + mkempbuf(n4), # buf1, false)], sqnum + 1) ∧ valid-wl (apebs0[n1, mkpeb(aehdr, avidhdr(v, m0, sqnum, datasize(buf, n0), checksum(buf, datasize(buf, n0))), buf1 + mkempbuf(n4), # buf1, false)], wlar[vtblpnum, wlar[vtblpnum].status:= erasing]) ∧ valid-eraseq(q + eq-entry(vtblpnum, lref)) ∧ valid-eraseq(wlar[vtblpnum, wlar[vtblpnum].status:= erasing], q + eq-entry(vtblpnum, lref)) ∧ valid-eraseq (apebs0[n1, mkpeb(aehdr, avidhdr(v, m0, sqnum, datasize(buf, n0), checksum(buf, datasize(buf, n0))), buf1 + mkempbuf(n4), # buf1, false)], q + eq-entry(vtblpnum, lref)) ∧ bflipset-cons(bflipset, wlar[vtblpnum, wlar[vtblpnum].status:= erasing]) ∧ valid-ebatbl (apebs0[n1, mkpeb(aehdr, avidhdr(v, m0, sqnum, datasize(buf, n0), checksum(buf, datasize(buf, n0))), buf1 + mkempbuf(n4), # buf1, false)], wlar[vtblpnum, wlar[vtblpnum].status:= erasing], vols, vtblpnum1) ∧ valid-vtbl(apebs0, vols, wlar[vtblpnum, wlar[vtblpnum].status:= erasing], vtblpnum1) ∧ id (apebs0[n1, mkpeb(aehdr, avidhdr(v, m0, sqnum, datasize(buf, n0), checksum(buf, datasize(buf, n0))), buf1 + mkempbuf(n4), # buf1, false)], apebs0, mapped-pebs(vols)) ∧ (q + eq-entry(vtblpnum, lref)).lebrefs = q0.lebrefs

Heuristic simplifier applied rule simplifier

And obtained the following new goals

Proof step 241:
# apebs0 = # wlar, LEB_SIZE = n2 + n0, LEB_SIZE = n4 + # buf1, apebs0[n1] = mkpeb(aehdr, empty, mkempbuf(LEB_SIZE), 0, false), wlar[n1] = wl-entry(m1, free), align↑(datasize(buf, n0), EB_PAGE_SIZE) = n3 + # buf1, aehdr.valid?, n1 < # wlar, bflipset-cons(bflipset, wlar), is-aligned(n0, EB_PAGE_SIZE), is-aligned(# buf1, EB_PAGE_SIZE), ubi-io-inv (apebs0[n1, mkpeb(aehdr, avidhdr(v, m0, sqnum, datasize(buf, n0), checksum(buf, datasize(buf, n0))), buf1 + mkempbuf(n4), # buf1, false)]), ubi-io-inv(apebs0[n1, mkpeb(aehdr, avidhdr(v, m0, sqnum, datasize(buf, n0), checksum(buf, datasize(buf, n0))), mkempbuf(LEB_SIZE), 0, false)]), ubi-io-inv(apebs0), unique-sqns(apebs0), valid-ebatbl(apebs0, wlar, vols, vtblpnum1), valid-eraseq(apebs0, q), valid-eraseq(wlar, q), valid-eraseq(q), valid-eraseq(q + eq-entry(n1, none) '), valid-global-sqn(apebs0, sqnum), valid-vtbl(apebs0, vols, wlar, vtblpnum1), valid-wl(apebs0, wlar), n3 + # buf1 ≤ # buf, n3 + # buf1 ≤ LEB_SIZE, n0 ≤ LEB_SIZE, n0 ≤ # buf, # buf1 ≤ # buf, # buf1 ≤ LEB_SIZE, ⌊err0⌋ , v ∈ vols ∧ m0 < # vols[v] ∨ v = VTBL_VOLID ∧ m0 = VTBL_LNUM, datasize(buf1, # buf1) < datasize(buf, n0) ∨ checksum(buf1 + mkempbuf(n3), datasize(buf, n0)) ≠ checksum(buf, datasize(buf, n0)) ⊦ vtblpnum1 = n1, vtblpnum1 ∈ q, VTBL_VOLID ∈ vols, ∃ buf0. buf = mkempbuf(n0) + buf0, valid-ebatbl (apebs0[n1, mkpeb(aehdr, avidhdr(v, m0, sqnum, datasize(buf, n0), checksum(buf, datasize(buf, n0))), buf1 + mkempbuf(n4), # buf1, false)], wlar[n1, wl-entry(m1, erasing)], vols, vtblpnum1) ∧ valid-eraseq (apebs0[n1, mkpeb(aehdr, avidhdr(v, m0, sqnum, datasize(buf, n0), checksum(buf, datasize(buf, n0))), buf1 + mkempbuf(n4), # buf1, false)], q + eq-entry(n1, none) ') ∧ valid-wl (apebs0[n1, mkpeb(aehdr, avidhdr(v, m0, sqnum, datasize(buf, n0), checksum(buf, datasize(buf, n0))), buf1 + mkempbuf(n4), # buf1, false)], wlar[n1, wl-entry(m1, erasing)]) ∧ valid-global-sqn (apebs0[n1, mkpeb(aehdr, avidhdr(v, m0, sqnum, datasize(buf, n0), checksum(buf, datasize(buf, n0))), buf1 + mkempbuf(n4), # buf1, false)], sqnum + 1) ∧ unique-sqns (apebs0[n1, mkpeb(aehdr, avidhdr(v, m0, sqnum, datasize(buf, n0), checksum(buf, datasize(buf, n0))), buf1 + mkempbuf(n4), # buf1, false)])

Rule argument

Additional information

Used simplifier rules: n < # wlar ⊦ valid-eraseq(wlar, q) ∧ wlar[n] = wl-entry(m, free) → ¬ n ∈ q; (s)% ⊦ eq-entry(m, lref).pnum = m; (s)% ⊦ valid-eraseq(q + eqent ') ↔ ¬ eqent.pnum ∈ q ∧ valid-eraseq(q); (ss)% ⊦ (q + eq-entry(n, none) ').lebrefs = q.lebrefs; (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)%⊦ m ≠ n0 → ( valid-vtbl(apebs, vols, wlar[m, wle], n0) ↔ valid-vtbl(apebs, vols, wlar, n0)); (s)%stat ≠ used ⊦ wlar[n] = wl-entry(m, stat) ∧ bflipset-cons(bflipset, wlar) → ¬ n ∈ bflipset; (s)% ⊦ used ≠ free; (s)%wle.status ≠ used ⊦ bflipset-cons(bflipset, wlar[m, wle]) ↔ bflipset-cons(bflipset, wlar) ∧ ¬ m ∈ bflipset; (s)% ⊦ used ≠ erasing; (s)% ⊦ wl-entry(m, stat).status = stat; (s)% ⊦ wl-entry(m, stat).ec = m; (s)%a: ⊦ (q + q0) + q1 = q + q0 + q1; from specification list[erasequeue-base]%stat ≠ erasing ⊦ n < # wlar ∧ wlar[n] = wl-entry(m0, stat) ∧ valid-eraseq(wlar, q) → valid-eraseq (wlar[n, wl-entry(m1, erasing)], q + eq-entry(n, lref) '); (ss)% ⊦ free ≠ erasing; (s)% ⊦ q + eqent = q + eqent '; (s)% ⊦ # wlar[n, wle] = # wlar; (s)% ⊦ wle.status:= stat = wl-entry(wle.ec, stat); (s)