Proof step 26 from proof inv-change (previous step)

Heuristic elimination applied rule insert elim lemma

And obtained the following new goals

• Proof step 27:

  # apebs = # wlar, # apebs1 = # wlar0, q.head = eq-entry(m, lref), LEB_SIZE = n1 + n0, LEB_SIZE = n2 + n0, wlar0[vtblpnum] = wl-entry(m0, free), apebs1[vtblpnum] = mkpeb(aehdr, empty, mkempbuf(LEB_SIZE), 0, false), apebs2 = apebs1, q2 = q1, vols0 = vols, vtblpnum1 = vtblpnum4, aehdr.valid?, vtblpnum < # wlar0, vtblpnum3 < # vols[v], bflipset-cons(bflipset, wlar), bflipset-cons(bflipset, wlar0), id(apebs1, apebs, mapped-pebs(vols)), is-aligned(n0, EB_PAGE_SIZE), ubi-io-inv(apebs1), ubi-io-inv(apebs), 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)] ( (err = ESUCCESS ∨ ⌊err⌋ ) ∧ id○(apebs1, apebs2, vtblpnum) ∧ ubi-io-inv(apebs1) ∧ # 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) ∧ ( v ∈ vols0 ∨ is-encoded(to-vtbl(vols0), subarray(buf, 0, LEB_SIZE)) ∧ n0 = LEB_SIZE ∨ err ≠ ESUCCESS → valid-ebatbl(apebs1, wlar0, vols, vtblpnum4) ∧ valid-vtbl(apebs1, vols, wlar0, vtblpnum4)) ∧ ( err = ESUCCESS ∧ v = VTBL_VOLID ∧ vtblpnum3 = VTBL_LNUM → (∀ v0, m0. ¬ v0 ∈ vols0 ∧ is-encoded(to-vtbl(vols0)[v0, m0], subarray(buf, 0, LEB_SIZE)) ∧ n0 = LEB_SIZE → valid-ebatbl(apebs1, wlar0, vols[v0, fill(mkebatbl(m0), unmapped)], vtblpnum4) ∧ valid-vtbl(apebs1, vols[v0, fill(mkebatbl(m0), unmapped)], wlar0, vtblpnum4))) ∧ (err = ESUCCESS ∧ v ∈ vols0 ∧ vols0[v][vtblpnum3] ≠ unmapped → q1 = q2 + eq-entry(vols0[v][vtblpnum3].pnum, v × vtblpnum3) ') ∧ (err = ESUCCESS ∧ v = VTBL_VOLID ∧ vtblpnum3 = VTBL_LNUM → q1 = q2 + eq-entry(vtblpnum1, VTBL_VOLID × VTBL_LNUM) ') ∧ id(apebs1, apebs2, mapped-pebs(vols0)) ∧ (v = VTBL_VOLID ∧ vtblpnum3 = VTBL_LNUM ∨ err ≠ ESUCCESS → vols = vols0) ∧ (v ∈ vols0 ∧ err = ESUCCESS → vols = vols0[v, vols0[v][vtblpnum3, ⌜vtblpnum⌝ ]]) ∧ ( err = ESUCCESS → apebs1[vtblpnum].fill = align↑(datasize(buf, n0), EB_PAGE_SIZE) ∧ apebs1[vtblpnum].data = subarray(buf, 0, n0) + mkempbuf(n2) ∧ q1.lebrefs ⊆ q2.lebrefs ++ (v × vtblpnum3)) ∧ (err ≠ ESUCCESS → q1.lebrefs = q2.lebrefs) → ⟪if err ≠ ESUCCESS then debug#("ubi: change to PEB " + vtblpnum.toString + " failed")⟫ ( valid-ebatbl(apebs1, wlar0, vols, vtblpnum4) ∧ valid-vtbl(apebs1, vols, wlar0, vtblpnum4) ∧ (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

Additional information

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