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

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

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

Rule argument

Additional information

Used simplifier rules: ⊦ eqent + q = eqent ' + q; (s)%⊦ ubi-cons(apebs, vols, wlar, q, bflipset, n0, n1) ↔ # apebs = # wlar ∧ unique-sqns(apebs) ∧ valid-global-sqn(apebs, n1) ∧ valid-wl(apebs, wlar) ∧ valid-eraseq(q) ∧ valid-eraseq(wlar, q) ∧ valid-eraseq(apebs, q) ∧ ¬ VTBL_VOLID ∈ vols ∧ bflipset-cons(bflipset, wlar) ∧ valid-ebatbl(apebs, wlar, vols, n0) ∧ valid-vtbl(apebs, vols, wlar, n0); (s)