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

# buf0 = LEB_SIZE, # apebs0 = # wlar2, # apebs = # wlar, apebs0[vtblpnum] = mkpeb(aehdr, empty, mkempbuf(LEB_SIZE), 0, false), wlar2[vtblpnum] = wl-entry(m, free), apebs1 = apebs0, q0 = [], vols0 = vols, vtblpnum1 = vtblpnum3, aehdr.valid?, vtblpnum < # wlar2, bflipset-cons(bflipset, wlar2), bflipset-cons(bflipset, wlar), id(apebs0, apebs, mapped-pebs(vols)), is-aligned(LEB_SIZE, EB_PAGE_SIZE), is-encoded(to-vtbl(vols)[v, n], buf0), ubi-io-inv(apebs0), ubi-io-inv(apebs), unique-sqns(apebs0), unique-sqns(apebs), 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-global-sqn(apebs0, sqnum), valid-global-sqn(apebs, sqnum), valid-vtbl(apebs0, vols, wlar2, vtblpnum3), valid-vtbl(apebs, vols, wlar, vtblpnum3), valid-wl(apebs0, wlar2), valid-wl(apebs, wlar), # 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 ⊦ ∀ vols, wlar2, q0, bflipset, vtblpnum3, sqnum, apebs0, err. (err = ESUCCESS ∨ ⌊err⌋ ) ∧ id○(apebs0, apebs1, vtblpnum) ∧ ubi-io-inv(apebs0) ∧ # apebs0 = # wlar2 ∧ unique-sqns(apebs0) ∧ valid-global-sqn(apebs0, sqnum) ∧ valid-wl(apebs0, wlar2) ∧ valid-eraseq(q0) ∧ valid-eraseq(wlar2, q0) ∧ valid-eraseq(apebs0, q0) ∧ ¬ VTBL_VOLID ∈ vols0 ∧ bflipset-cons(bflipset, wlar2) ∧ ( is-encoded(to-vtbl(vols0), buf0) ∨ err ≠ ESUCCESS → valid-ebatbl(apebs0, wlar2, vols0, vtblpnum3) ∧ valid-vtbl(apebs0, vols0, wlar2, vtblpnum3)) ∧ ( err = ESUCCESS → (∀ v0, m. ¬ v0 ∈ vols0 ∧ is-encoded(to-vtbl(vols0)[v0, m], buf0) → valid-ebatbl(apebs0, wlar2, vols0[v0, fill(mkebatbl(m), unmapped)], vtblpnum3) ∧ valid-vtbl(apebs0, vols0[v0, fill(mkebatbl(m), unmapped)], wlar2, vtblpnum3))) ∧ (err = ESUCCESS → q0 = eq-entry(vtblpnum1, VTBL_VOLID × VTBL_LNUM) ') ∧ id(apebs0, apebs1, mapped-pebs(vols0)) ∧ vols = vols0 ∧ ( err = ESUCCESS → apebs0[vtblpnum].fill = align↑(datasize(apebs0[vtblpnum].data, LEB_SIZE), EB_PAGE_SIZE) ∧ apebs0[vtblpnum].data = buf0 ∧ q0.lebrefs ⊆ ∅ ++ (VTBL_VOLID × VTBL_LNUM)) ∧ (err ≠ ESUCCESS → q0.lebrefs = ∅) → ⟪if err = ESUCCESS then {vols[v] := mkebatbl(n); vols[v] := fill(vols[v], unmapped)}⟫ ( ¬ VTBL_VOLID ∈ vols ∧ valid-ebatbl(apebs0, wlar2, vols, vtblpnum3) ∧ valid-vtbl(apebs0, vols, wlar2, vtblpnum3) ∧ (err = ESUCCESS ∨ ⌊err⌋ ) ∧ id(apebs0, apebs, mapped-pebs(vols)) ∧ (err = ESUCCESS → ¬ v ∈ vols0 ∧ vols = vols0[v, fill(mkebatbl(n), unmapped)] ∧ q0.lebrefs ⊆ ∅ ++ (VTBL_VOLID × VTBL_LNUM)) ∧ (err ≠ ESUCCESS → q0.lebrefs ⊆ q.lebrefs ∧ vols = vols0)), v = VTBL_VOLID, vtblpnum3 = vtblpnum, vtblpnum3 ∈ q, VTBL_VOLID ∈ vols, v ∈ vols

Heuristic simplifier applied rule simplifier

And obtained the following new goals

Proof step 51:
# apebs2 = # wlar2, # apebs = # wlar, # apebs0 = # wlar2, # buf0 = LEB_SIZE, # wlar0 = # wlar2, wlar2[vtblpnum] = wl-entry(m, free), apebs0[vtblpnum] = mkpeb(aehdr, empty, mkempbuf(LEB_SIZE), 0, false), vols0 = vols, v ≠ VTBL_VOLID, vtblpnum3 ≠ vtblpnum, 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], buf0), 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(q1), valid-eraseq(wlar0, q1), valid-eraseq(apebs2, q1), 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, ¬ v ∈ vols, ¬ vtblpnum3 ∈ q, ¬ VTBL_VOLID ∈ vols, err = ESUCCESS → q1 = eq-entry(vtblpnum3, VTBL_VOLID × VTBL_LNUM) ', err = ESUCCESS → apebs2[vtblpnum].fill = align↑(datasize(apebs2[vtblpnum].data, LEB_SIZE), EB_PAGE_SIZE) ∧ apebs2[vtblpnum].data = buf0 ∧ q1.lebrefs ⊆ ∅ ++ (VTBL_VOLID × VTBL_LNUM), err ≠ ESUCCESS → q1.lebrefs = ∅, to-vtbl(vols)[v, n] = to-vtbl(vols) ∨ err ≠ ESUCCESS → valid-ebatbl(apebs2, wlar0, vols, vtblpnum0) ∧ valid-vtbl(apebs2, vols, wlar0, vtblpnum0), err = ESUCCESS → (∀ 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)), err = ESUCCESS ∨ ⌊err⌋ ⊦ ⟪if err = ESUCCESS then {vols[v] := mkebatbl(n); vols[v] := fill(vols[v], unmapped)}⟫ ( ¬ VTBL_VOLID ∈ vols ∧ valid-ebatbl(apebs2, wlar0, vols, vtblpnum0) ∧ valid-vtbl(apebs2, vols, wlar0, vtblpnum0) ∧ (err = ESUCCESS ∨ ⌊err⌋ ) ∧ id(apebs2, apebs, mapped-pebs(vols)) ∧ (err = ESUCCESS → ¬ v ∈ vols0 ∧ vols = vols0[v, fill(mkebatbl(n), unmapped)] ∧ q1.lebrefs ⊆ ∅ ++ (VTBL_VOLID × VTBL_LNUM)) ∧ (err ≠ ESUCCESS → q1.lebrefs ⊆ q.lebrefs ∧ vols = vols0))

Rule argument

Additional information

Used simplifier rules: lf-01: ⊦ m < n ∧ n = n0 → m < n0; (forward) from specification nat-basic%int-c: ⊦ ns ∩ ns0 = ns0 ∩ ns; from specification set-union[nat-set]%int-a: ⊦ (ns ∩ ns0) ∩ ns1 = ns ∩ ns0 ∩ ns1; from specification set-union[nat-set]% ⊦ ns ∩ ns = ns; (s)%idexcept-size: ⊦ id○(apebs, apebs0, n) → # apebs = # apebs0; (forward) from specification array-copy[apebs]%idset-trans-intersect: ⊦ id(apebs2, apebs1, ns0) ∧ id(apebs1, apebs0, ns1) → id(apebs2, apebs0, ns0 ∩ ns1); (forward) from specification ubi-base% ⊦ is-encoded(vtbl0, buf) → (is-encoded(vtbl1, buf) ↔ vtbl0 = vtbl1); (s)