[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 21 from proof inv-change (previous step)

# apebs1 = # wlar0, # apebs = # wlar, apebs1[vtblpnum].fill = 0, q.head = eq-entry(m, lref), apebs1[vtblpnum].vidhdr = empty, LEB_SIZE = n1 + n0, wlar0[vtblpnum] = wl-entry(m0, free), vols0 = vols, vtblpnum4 ≠ vtblpnum, apebs1[vtblpnum].echdr.valid?, vtblpnum < # wlar0, vtblpnum3 < # vols[v], bflipset-cons(bflipset, wlar0), bflipset-cons(bflipset, wlar), id(apebs1, apebs, mapped-pebs(vols)), is-aligned(n0, EB_PAGE_SIZE), ubi-io-inv(apebs1), ubi-io-inv(apebs), unique-sqns(apebs1), unique-sqns(apebs), valid-ebatbl(apebs1, wlar0, vols, vtblpnum4), valid-ebatbl(apebs, wlar, vols, vtblpnum4), valid-eraseq(apebs1, q1), valid-eraseq(wlar0, q1), valid-eraseq(q1), valid-eraseq(apebs, q), valid-eraseq(wlar, q), valid-eraseq(q), valid-global-sqn(apebs1, sqnum), valid-global-sqn(apebs, sqnum), valid-vtbl(apebs1, vols, wlar0, vtblpnum4), valid-vtbl(apebs, vols, wlar, vtblpnum4), valid-wl(apebs1, wlar0), valid-wl(apebs, wlar), v ∈ vols, n0 ≤ # buf, n0 ≤ LEB_SIZE, q1.lebrefs ⊆ q.lebrefs, ¬ vtblpnum4 ∈ q, ¬ VTBL_VOLID ∈ vols, ¬ vtblpnum4 ∈ q1, apebs = apebs1 ∧ wlar = wlar0 ∧ q = q1 ∨ id○(apebs, apebs1, vtblpnum) ∧ id○(wlar, wlar0, vtblpnum) ∧ q = eq-entry(vtblpnum, lref) ' + q1 ⊦ ⟪ubi_atomic_leb_change#(v, vtblpnum3, vtblpnum, n0, buf, EB_PAGE_SIZE; vols, wlar0, q1, bflipset, vtblpnum4, sqnum, apebs1; err); if err ≠ ESUCCESS then debug#("ubi: change to PEB " + vtblpnum.toString + " failed")⟫ ( # apebs1 = # wlar0 ∧ unique-sqns(apebs1) ∧ valid-global-sqn(apebs1, sqnum) ∧ valid-wl(apebs1, wlar0) ∧ valid-eraseq(q1) ∧ valid-eraseq(wlar0, q1) ∧ valid-eraseq(apebs1, q1) ∧ ¬ VTBL_VOLID ∈ vols ∧ bflipset-cons(bflipset, wlar0) ∧ valid-ebatbl(apebs1, wlar0, vols, vtblpnum4) ∧ valid-vtbl(apebs1, vols, wlar0, vtblpnum4) ∧ ubi-io-inv(apebs1) ∧ (err = ESUCCESS ∨ ⌊err⌋ ) ∧ (err ≠ ESUCCESS → vols = vols0 ∧ id(apebs1, apebs, mapped-pebs(vols0)) ∧ q1.lebrefs ⊆ q.lebrefs) ∧ ( err = ESUCCESS → v ∈ vols0 ∧ vtblpnum3 < # vols0[v] ∧ q1.lebrefs ⊆ q.lebrefs ++ (v × vtblpnum3) ∧ (vols0[v][vtblpnum3] ≠ unmapped → id(apebs1, apebs, mapped-pebs(vols0) -- vols0[v][vtblpnum3].pnum)) ∧ (vols0[v][vtblpnum3] = unmapped → id(apebs1, apebs, mapped-pebs(vols0))) ∧ (∃ n. vols = vols0[v, vols0[v][vtblpnum3, ⌜n⌝ ]] ∧ apebs1[n].data = subarray(buf, 0, n0) + mkempbuf(n1) ∧ apebs1[n].fill = align↑(datasize(buf, n0), EB_PAGE_SIZE))))

Heuristic elimination applied rule insert elim lemma

And obtained the following new goals

Proof step 22:
# apebs = # wlar, # apebs1 = # wlar0, q.head = eq-entry(m, lref), LEB_SIZE = n1 + n0, wlar0[vtblpnum] = wl-entry(m0, free), apebs1[vtblpnum] = mkpeb(aehdr, avhdr, buf0, m1, boolvar), avhdr = empty, m1 = 0, vols0 = vols, aehdr.valid?, vtblpnum3 < # vols[v], vtblpnum < # wlar0, bflipset-cons(bflipset, wlar), bflipset-cons(bflipset, wlar0), id(apebs1, apebs, mapped-pebs(vols)), is-aligned(n0, EB_PAGE_SIZE), ubi-io-inv(apebs), ubi-io-inv(apebs1), unique-sqns(apebs), unique-sqns(apebs1), valid-ebatbl(apebs, wlar, vols, vtblpnum4), valid-ebatbl(apebs1, wlar0, vols, vtblpnum4), valid-eraseq(q), valid-eraseq(wlar, q), valid-eraseq(apebs, q), valid-eraseq(q1), valid-eraseq(wlar0, q1), valid-eraseq(apebs1, q1), valid-global-sqn(apebs, sqnum), valid-global-sqn(apebs1, sqnum), valid-vtbl(apebs, vols, wlar, vtblpnum4), valid-vtbl(apebs1, vols, wlar0, vtblpnum4), valid-wl(apebs, wlar), valid-wl(apebs1, wlar0), v ∈ vols, n0 ≤ LEB_SIZE, n0 ≤ # buf, q1.lebrefs ⊆ q.lebrefs, apebs = apebs1 ∧ wlar = wlar0 ∧ q = q1 ∨ id○(apebs, apebs1, vtblpnum) ∧ id○(wlar, wlar0, vtblpnum) ∧ q = eq-entry(vtblpnum, lref) ' + q1 ⊦ ⟪ubi_atomic_leb_change#(v, vtblpnum3, vtblpnum, n0, buf, EB_PAGE_SIZE; vols, wlar0, q1, bflipset, vtblpnum4, sqnum, apebs1; err); if err ≠ ESUCCESS then debug#("ubi: change to PEB " + vtblpnum.toString + " failed")⟫ ( # apebs1 = # wlar0 ∧ unique-sqns(apebs1) ∧ valid-global-sqn(apebs1, sqnum) ∧ valid-wl(apebs1, wlar0) ∧ valid-eraseq(q1) ∧ valid-eraseq(wlar0, q1) ∧ valid-eraseq(apebs1, q1) ∧ ¬ VTBL_VOLID ∈ vols ∧ bflipset-cons(bflipset, wlar0) ∧ valid-ebatbl(apebs1, wlar0, vols, vtblpnum4) ∧ valid-vtbl(apebs1, vols, wlar0, vtblpnum4) ∧ ubi-io-inv(apebs1) ∧ (err = ESUCCESS ∨ ⌊err⌋ ) ∧ (err ≠ ESUCCESS → vols = vols0 ∧ id(apebs1, apebs, mapped-pebs(vols0)) ∧ q1.lebrefs ⊆ q.lebrefs) ∧ ( err = ESUCCESS → v ∈ vols0 ∧ vtblpnum3 < # vols0[v] ∧ q1.lebrefs ⊆ q.lebrefs ++ (v × vtblpnum3) ∧ (vols0[v][vtblpnum3] ≠ unmapped → id(apebs1, apebs, mapped-pebs(vols0) -- vols0[v][vtblpnum3].pnum)) ∧ (vols0[v][vtblpnum3] = unmapped → id(apebs1, apebs, mapped-pebs(vols0))) ∧ (∃ n. vols = vols0[v, vols0[v][vtblpnum3, ⌜n⌝ ]] ∧ apebs1[n].data = subarray(buf, 0, n0) + mkempbuf(n1) ∧ apebs1[n].fill = align↑(datasize(buf, n0), EB_PAGE_SIZE)))), vtblpnum4 = vtblpnum, vtblpnum4 ∈ q, VTBL_VOLID ∈ vols, vtblpnum4 ∈ q1

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] → [apebs1[vtblpnum], aehdr, avhdr, buf0, 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: apebs1[vtblpnum], aehdr, avhdr, buf0, m1, boolvar