[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 55 from proof inv-create-volume (previous step)

# wlar0 = # wlar2, # apebs2[vtblpnum].data = LEB_SIZE, # apebs0 = # wlar2, # apebs = # wlar, # apebs2 = # wlar2, apebs2[vtblpnum].fill = align↑(datasize(apebs2[vtblpnum].data, LEB_SIZE), EB_PAGE_SIZE), apebs0[vtblpnum] = mkpeb(aehdr, empty, mkempbuf(LEB_SIZE), 0, false), wlar2[vtblpnum] = wl-entry(m, free), aehdr.valid?, vtblpnum < # wlar2, bflipset-cons(bflipset, wlar2), bflipset-cons(bflipset, wlar), bflipset-cons(bflipset0, wlar0), id(apebs0, apebs, mapped-pebs(vols)), id(apebs2, apebs0, mapped-pebs(vols)), id(apebs2, apebs, mapped-pebs(vols)), id○(apebs2, apebs0, vtblpnum), is-aligned(LEB_SIZE, EB_PAGE_SIZE), is-encoded(to-vtbl(vols)[v, n], apebs2[vtblpnum].data), ubi-io-inv(apebs0), ubi-io-inv(apebs), ubi-io-inv(apebs2), unique-sqns(apebs0), unique-sqns(apebs), unique-sqns(apebs2), valid-ebatbl(apebs0, wlar2, vols, vtblpnum3), valid-ebatbl(apebs, wlar, vols, vtblpnum3), valid-eraseq(wlar2, []), valid-eraseq(apebs, q), valid-eraseq(wlar, q), valid-eraseq(q), valid-eraseq(apebs2, eq-entry(vtblpnum3, VTBL_VOLID × VTBL_LNUM) '), valid-eraseq(wlar0, eq-entry(vtblpnum3, VTBL_VOLID × VTBL_LNUM) '), valid-global-sqn(apebs0, sqnum), valid-global-sqn(apebs, sqnum), valid-global-sqn(apebs2, sqnum0), valid-vtbl(apebs0, vols, wlar2, vtblpnum3), valid-vtbl(apebs, vols, wlar, vtblpnum3), valid-wl(apebs0, wlar2), valid-wl(apebs, wlar), valid-wl(apebs2, wlar0), # to-vtbl(vols)[v, n] * (ENCODED_NAT_SIZE + ENCODED_VOLID_SIZE) + ENCODED_NAT_SIZE ≤ LEB_SIZE, 2 * ENCODED_NAT_SIZE + (ENCODED_VOLID_SIZE + ENCODED_NAT_SIZE) * # vols + ENCODED_VOLID_SIZE ≤ LEB_SIZE, to-vtbl(vols)[v, n] = to-vtbl(vols) → valid-ebatbl(apebs2, wlar0, vols, vtblpnum0) ∧ valid-vtbl(apebs2, vols, wlar0, vtblpnum0), ∀ v0, m0. ¬ v0 ∈ vols ∧ to-vtbl(vols)[v, n] = to-vtbl(vols)[v0, m0] → valid-ebatbl(apebs2, wlar0, vols[v0, fill(mkebatbl(m0), unmapped)], vtblpnum0) ∧ valid-vtbl(apebs2, vols[v0, fill(mkebatbl(m0), unmapped)], wlar0, vtblpnum0) ⊦ v = VTBL_VOLID, vtblpnum3 = vtblpnum, v ∈ vols, vtblpnum3 ∈ q, VTBL_VOLID ∈ vols, valid-ebatbl(apebs2, wlar0, vols[v, fill(mkebatbl(n), unmapped)], vtblpnum0) ∧ valid-vtbl(apebs2, vols[v, fill(mkebatbl(n), unmapped)], wlar0, vtblpnum0)

Heuristic elimination applied rule insert elim lemma

And obtained the following new goals

Proof step 56:
# apebs2 = # wlar2, # apebs = # wlar, # apebs0 = # wlar2, # buf = LEB_SIZE, # wlar0 = # wlar2, wlar2[vtblpnum] = wl-entry(m, free), apebs0[vtblpnum] = mkpeb(aehdr, empty, mkempbuf(LEB_SIZE), 0, false), apebs2[vtblpnum] = mkpeb(aehdr0, avhdr, buf, m1, boolvar), m1 = align↑(datasize(buf, LEB_SIZE), EB_PAGE_SIZE), aehdr.valid?, vtblpnum < # wlar2, bflipset-cons(bflipset0, wlar0), bflipset-cons(bflipset, wlar), bflipset-cons(bflipset, wlar2), id(apebs2, apebs, mapped-pebs(vols)), id(apebs2, apebs0, mapped-pebs(vols)), id(apebs0, apebs, mapped-pebs(vols)), id○(apebs2, apebs0, vtblpnum), is-aligned(LEB_SIZE, EB_PAGE_SIZE), is-encoded(to-vtbl(vols)[v, n], buf), ubi-io-inv(apebs2), ubi-io-inv(apebs), ubi-io-inv(apebs0), unique-sqns(apebs2), unique-sqns(apebs), unique-sqns(apebs0), valid-ebatbl(apebs, wlar, vols, vtblpnum3), valid-ebatbl(apebs0, wlar2, vols, vtblpnum3), valid-eraseq(wlar0, eq-entry(vtblpnum3, VTBL_VOLID × VTBL_LNUM) '), valid-eraseq(apebs2, eq-entry(vtblpnum3, VTBL_VOLID × VTBL_LNUM) '), valid-eraseq(q), valid-eraseq(wlar, q), valid-eraseq(apebs, q), valid-eraseq(wlar2, []), valid-global-sqn(apebs2, sqnum0), valid-global-sqn(apebs, sqnum), valid-global-sqn(apebs0, sqnum), valid-vtbl(apebs, vols, wlar, vtblpnum3), valid-vtbl(apebs0, vols, wlar2, vtblpnum3), valid-wl(apebs2, wlar0), valid-wl(apebs, wlar), valid-wl(apebs0, wlar2), 2 * ENCODED_NAT_SIZE + (ENCODED_VOLID_SIZE + ENCODED_NAT_SIZE) * # vols + ENCODED_VOLID_SIZE ≤ LEB_SIZE, # to-vtbl(vols)[v, n] * (ENCODED_NAT_SIZE + ENCODED_VOLID_SIZE) + ENCODED_NAT_SIZE ≤ LEB_SIZE, to-vtbl(vols)[v, n] = to-vtbl(vols) → valid-ebatbl(apebs2, wlar0, vols, vtblpnum0) ∧ valid-vtbl(apebs2, vols, wlar0, vtblpnum0), ∀ v0, m0. ¬ v0 ∈ vols ∧ to-vtbl(vols)[v, n] = to-vtbl(vols)[v0, m0] → valid-ebatbl(apebs2, wlar0, vols[v0, fill(mkebatbl(m0), unmapped)], vtblpnum0) ∧ valid-vtbl(apebs2, vols[v0, fill(mkebatbl(m0), unmapped)], wlar0, vtblpnum0) ⊦ v = VTBL_VOLID, vtblpnum3 = vtblpnum, VTBL_VOLID ∈ vols, vtblpnum3 ∈ q, v ∈ vols, valid-ebatbl(apebs2, wlar0, vols[v, fill(mkebatbl(n), unmapped)], vtblpnum0) ∧ valid-vtbl(apebs2, vols[v, fill(mkebatbl(n), unmapped)], wlar0, vtblpnum0)

Rule argument

spec: apeb name: elim seq: ⊦ ( ( (aehdr = apeb.echdr ∧ avhdr = apeb.vidhdr) ∧ buf = apeb.data) ∧ m = apeb.fill) ∧ (boolvar ↔ apeb.bad) ↔ apeb = mkpeb(aehdr, avhdr, buf, m, boolvar) subst: [apeb, aehdr, avhdr, buf, m, boolvar] → [apebs2[vtblpnum], aehdr0, avhdr, buf, m1, boolvar]

Additional information

Used simplifier rules: ⊦ ( ((aehdr = apeb.echdr ∧ avhdr = apeb.vidhdr) ∧ buf = apeb.data) ∧ m = apeb.fill) ∧ (boolvar ↔ apeb.bad) ↔ apeb = mkpeb(aehdr, avhdr, buf, m, boolvar); (elim) Used terms: apebs2[vtblpnum], aehdr0, avhdr, buf, m1, boolvar