[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 29 from proof prepost-write-multiple (previous step)

# apebs2 = # wlar1, # apebs0 = # wlar0, # apebs = # wlar, LEB_SIZE = (n1 + m0) + m1, vols0[v][m] = unmapped, m < # vols0[v], bflipset-cons(bflipset, wlar1), bflipset-cons(bflipset, wlar0), bflipset-cons(bflipset, wlar), id(apebs2, apebs0, mapped-pebs(vols0)), id(apebs2, apebs, mapped-pebs(vols0)), id(apebs, apebs0, mapped-pebs(vols0)), is-aligned(m1, EB_PAGE_SIZE), is-aligned(m0, EB_PAGE_SIZE), ubi-io-inv(apebs2), ubi-io-inv(apebs), ubi-io-inv(apebs0), unique-sqns(apebs2), unique-sqns(apebs0), unique-sqns(apebs), valid-ebatbl(apebs2, wlar1, vols1, vtblpnum3), valid-ebatbl(apebs0, wlar0, vols0, vtblpnum3), valid-ebatbl(apebs, wlar, vols0, vtblpnum3), valid-eraseq(q2), valid-eraseq(wlar1, q2), valid-eraseq(apebs2, q2), valid-eraseq(apebs0, q0), valid-eraseq(wlar0, q0), valid-eraseq(q0), valid-eraseq(q), valid-eraseq(wlar, q), valid-eraseq(apebs, q), valid-global-sqn(apebs2, sqnum1), valid-global-sqn(apebs0, sqnum0), valid-global-sqn(apebs, sqnum), valid-vtbl(apebs2, vols1, wlar1, vtblpnum3), valid-vtbl(apebs0, vols0, wlar0, vtblpnum3), valid-vtbl(apebs, vols0, wlar, vtblpnum3), valid-wl(apebs2, wlar1), valid-wl(apebs0, wlar0), valid-wl(apebs, wlar), v ∈ vols0, m0 + m1 ≤ LEB_SIZE, m1 + m2 ≤ # buf, vtblpnum4 ≤ UBI_WRITE_RETRIES, m2 + m1 ≤ # buf, m1 ≤ LEB_SIZE, q2.lebrefs ⊆ q.lebrefs ++ (v × m), q.lebrefs ⊆ q0.lebrefs ++ (v × m), q2.lebrefs ⊆ q0.lebrefs ++ (v × m), ⌊err⌋ , m1 = 0 → q2.lebrefs ⊆ q.lebrefs, err0 ≠ ESUCCESS → vols1 = vols0, m1 = 0 → q.lebrefs ⊆ q0.lebrefs, err0 = ESUCCESS → vols1 = vols0[v, vols0[v][m, ⌜n⌝ ]] ∧ (m1 ≠ 0 → apebs2[n].fill = m0 + m1) ∧ (m1 = 0 → apebs2[n].fill = 0) ∧ apebs2[n].data = mkempbuf(m0) + subarray(buf, m2, m1) + mkempbuf(n1), err0 = ESUCCESS ∨ ⌊err0⌋ ⊦ vtblpnum3 ∈ q2, VTBL_VOLID ∈ vols1, vtblpnum3 ∈ q, vtblpnum3 ∈ q0, VTBL_VOLID ∈ vols0, ( err0 = ESUCCESS → (∃ n. vols1 = vols0[v, vols0[v][m, ⌜n⌝ ]] ∧ (m1 ≠ 0 → apebs2[n].fill = m0 + m1) ∧ (m1 = 0 → apebs2[n].fill = 0) ∧ apebs2[n].data = mkempbuf(m0) + subarray(buf, m2, m1) + mkempbuf(n1))) ∧ (m1 = 0 → q2.lebrefs ⊆ q0.lebrefs) ∧ m < # vols1[v] ∧ v ∈ vols1

Heuristic elimination applied rule insert elim lemma

And obtained the following new goals

Proof step 30:
# apebs = # wlar, # apebs0 = # wlar0, # apebs2 = # wlar1, LEB_SIZE = (n1 + m0) + m1, vols0[v][m] = unmapped, apebs2[n] = mkpeb(aehdr, avhdr, buf0, m3, boolvar), m < # vols0[v], bflipset-cons(bflipset, wlar), bflipset-cons(bflipset, wlar0), bflipset-cons(bflipset, wlar1), id(apebs, apebs0, mapped-pebs(vols0)), id(apebs2, apebs, mapped-pebs(vols0)), id(apebs2, apebs0, mapped-pebs(vols0)), is-aligned(m0, EB_PAGE_SIZE), is-aligned(m1, EB_PAGE_SIZE), ubi-io-inv(apebs0), ubi-io-inv(apebs), ubi-io-inv(apebs2), unique-sqns(apebs), unique-sqns(apebs0), unique-sqns(apebs2), valid-ebatbl(apebs, wlar, vols0, vtblpnum3), valid-ebatbl(apebs0, wlar0, vols0, vtblpnum3), valid-ebatbl(apebs2, wlar1, vols1, vtblpnum3), valid-eraseq(apebs, q), valid-eraseq(wlar, q), valid-eraseq(q), valid-eraseq(q0), valid-eraseq(wlar0, q0), valid-eraseq(apebs0, q0), valid-eraseq(apebs2, q2), valid-eraseq(wlar1, q2), valid-eraseq(q2), valid-global-sqn(apebs, sqnum), valid-global-sqn(apebs0, sqnum0), valid-global-sqn(apebs2, sqnum1), valid-vtbl(apebs, vols0, wlar, vtblpnum3), valid-vtbl(apebs0, vols0, wlar0, vtblpnum3), valid-vtbl(apebs2, vols1, wlar1, vtblpnum3), valid-wl(apebs, wlar), valid-wl(apebs0, wlar0), valid-wl(apebs2, wlar1), v ∈ vols0, m1 ≤ LEB_SIZE, m2 + m1 ≤ # buf, vtblpnum4 ≤ UBI_WRITE_RETRIES, m1 + m2 ≤ # buf, m0 + m1 ≤ LEB_SIZE, q2.lebrefs ⊆ q0.lebrefs ++ (v × m), q.lebrefs ⊆ q0.lebrefs ++ (v × m), q2.lebrefs ⊆ q.lebrefs ++ (v × m), ⌊err⌋ , err0 = ESUCCESS → vols1 = vols0[v, vols0[v][m, ⌜n⌝ ]] ∧ (m1 ≠ 0 → m3 = m0 + m1) ∧ (m1 = 0 → m3 = 0) ∧ buf0 = mkempbuf(m0) + subarray(buf, m2, m1) + mkempbuf(n1), m1 = 0 → q.lebrefs ⊆ q0.lebrefs, err0 ≠ ESUCCESS → vols1 = vols0, m1 = 0 → q2.lebrefs ⊆ q.lebrefs, err0 = ESUCCESS ∨ ⌊err0⌋ ⊦ VTBL_VOLID ∈ vols0, vtblpnum3 ∈ q0, vtblpnum3 ∈ q, VTBL_VOLID ∈ vols1, vtblpnum3 ∈ q2, ( err0 = ESUCCESS → (∃ n. vols1 = vols0[v, vols0[v][m, ⌜n⌝ ]] ∧ (m1 ≠ 0 → apebs2[n].fill = m0 + m1) ∧ (m1 = 0 → apebs2[n].fill = 0) ∧ apebs2[n].data = mkempbuf(m0) + subarray(buf, m2, m1) + mkempbuf(n1))) ∧ (m1 = 0 → q2.lebrefs ⊆ q0.lebrefs) ∧ m < # vols1[v] ∧ v ∈ vols1

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[n], aehdr, avhdr, buf0, m3, 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[n], aehdr, avhdr, buf0, m3, boolvar