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

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

Heuristic elimination applied rule insert elim lemma

And obtained the following new goals

Proof step 236:
# 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, q0 = q, 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-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)) ⊦ ⟪ubi_wl_put_peb#(none, n1; wlar, q)⟫ ( # apebs0 = # wlar ∧ 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) ∧ valid-eraseq(q) ∧ valid-eraseq(wlar, q) ∧ valid-eraseq (apebs0[n1, mkpeb(aehdr, avidhdr(v, m0, sqnum, datasize(buf, n0), checksum(buf, datasize(buf, n0))), buf1 + mkempbuf(n4), # buf1, false)], q) ∧ bflipset-cons(bflipset, wlar) ∧ valid-ebatbl (apebs0[n1, mkpeb(aehdr, avidhdr(v, m0, sqnum, datasize(buf, n0), checksum(buf, datasize(buf, n0))), buf1 + mkempbuf(n4), # buf1, false)], wlar, vols, vtblpnum1) ∧ valid-vtbl(apebs0, vols, wlar, 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.lebrefs = q0.lebrefs), vtblpnum1 = n1, VTBL_VOLID ∈ vols, vtblpnum1 ∈ q, ∃ buf0. buf = mkempbuf(n0) + buf0

Rule argument

spec: nat name: elim-sub seq: n ≤ m ⊦ n0 = m - n ↔ m = n0 + n subst: [n, m, n0] → [# buf1, LEB_SIZE, n]

Additional information

Used simplifier rules: n ≤ m ⊦ n0 = m - n ↔ m = n0 + n; (elim) Used terms: # buf1, LEB_SIZE, n