[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 23 from proof refine-erase (previous step)

# apebs = # wlar0, wlar0[n] = wl-entry(m, stat), vols[v][vtblpnum2] = ⌜n⌝ , q = q0 + eq-entry(n, v × vtblpnum2) ', wlar = wlar0[n, wl-entry(m, erasing)], avols[v][vtblpnum2].mapped?, vtblpnum2 < # vols[v], vtblpnum2 < # avols[v], n < # wlar0, abs(avols, apebs, vols, q0), bflipset-cons(bflipset, wlar0), bflipset-cons(bflipset -- n, wlar0), ebm-cons(avols), ubi-io-inv(apebs), unique-sqns(apebs), valid-ebatbl(apebs, wlar0, vols, vtblpnum1), valid-ebatbl(apebs, wlar0[n, wl-entry(m, erasing)], vols[v, vols[v][vtblpnum2, unmapped]], vtblpnum1), valid-eraseq(q0), valid-eraseq(wlar0, q0), valid-eraseq(apebs, q0), valid-eraseq(apebs, q0 + eq-entry(n, v × vtblpnum2) '), valid-eraseq(wlar0[n, wl-entry(m, erasing)], q0 + eq-entry(n, v × vtblpnum2) '), valid-eraseq(q0 + eq-entry(n, v × vtblpnum2) '), valid-global-sqn(apebs, sqnum), valid-vtbl(apebs, vols, wlar0, vtblpnum1), valid-vtbl(apebs, vols, wlar0[n, wl-entry(m, erasing)], vtblpnum1), valid-wl(apebs, wlar0), valid-wl(apebs, wlar0[n, wl-entry(m, erasing)]), v ∈ vols, v ∈ avols, ¬ VTBL_VOLID ∈ vols ⊦ ⟪ubi_erase_all#(vols[v, vols[v][vtblpnum2, unmapped]], bflipset -- vols[v][vtblpnum2].pnum, vtblpnum1, sqnum; wlar, q, apebs; err)⟫ ⟨ebm_erase#(v, vtblpnum2; avols; err0)⟩ (abs(avols, apebs, vols[v, vols[v][vtblpnum2, unmapped]], q) ∧ err = err0)

User applied rule insert program lemma

And obtained the following new goals

Proof step 24:
ubi-cons(apebs, vols, wlar, q, bflipset, vtblpnum, sqnum), ubi-io-inv(apebs), apebs0 = apebs, q0 = q ⊦ ⟪ubi_erase_all#(vols, bflipset, vtblpnum, sqnum; wlar, q, apebs; err)⟫ ( ubi-cons(apebs, vols, wlar, q, bflipset, vtblpnum, sqnum) ∧ ubi-io-inv(apebs) ∧ id(apebs, apebs0, mapped-pebs(vols)) ∧ q ⊆ q0 ∧ (err = ESUCCESS → q = []) ∧ (err = ESUCCESS ∨ ⌊err⌋ ))
Proof step 25:
# apebs = # wlar0, vols[v][vtblpnum2] = ⌜n⌝ , wlar0[n] = wl-entry(m, stat), apebs = apebs, apebs1 = apebs, bflipset0 = bflipset -- vols[v][vtblpnum2].pnum, q = q0 + eq-entry(n, v × vtblpnum2) ', q = q, q1 = q, sqnum0 = sqnum, vols0 = vols[v, vols[v][vtblpnum2, unmapped]], vtblpnum0 = vtblpnum1, wlar = wlar0[n, wl-entry(m, erasing)], avols[v][vtblpnum2].mapped?, n < # wlar0, vtblpnum2 < # avols[v], vtblpnum2 < # vols[v], abs(avols, apebs, vols, q0), bflipset-cons(bflipset -- n, wlar0), bflipset-cons(bflipset, wlar0), ebm-cons(avols), ubi-cons(apebs, vols[v, vols[v][vtblpnum2, unmapped]], wlar, q, bflipset -- vols[v][vtblpnum2].pnum, vtblpnum1, sqnum), ubi-io-inv(apebs), unique-sqns(apebs), valid-ebatbl(apebs, wlar0[n, wl-entry(m, erasing)], vols[v, vols[v][vtblpnum2, unmapped]], vtblpnum1), valid-ebatbl(apebs, wlar0, vols, vtblpnum1), valid-eraseq(q0 + eq-entry(n, v × vtblpnum2) '), valid-eraseq(wlar0[n, wl-entry(m, erasing)], q0 + eq-entry(n, v × vtblpnum2) '), valid-eraseq(apebs, q0 + eq-entry(n, v × vtblpnum2) '), valid-eraseq(apebs, q0), valid-eraseq(wlar0, q0), valid-eraseq(q0), valid-global-sqn(apebs, sqnum), valid-vtbl(apebs, vols, wlar0[n, wl-entry(m, erasing)], vtblpnum1), valid-vtbl(apebs, vols, wlar0, vtblpnum1), valid-wl(apebs, wlar0[n, wl-entry(m, erasing)]), valid-wl(apebs, wlar0), v ∈ avols, v ∈ vols ⊦ [ubi_erase_all#(vols[v, vols[v][vtblpnum2, unmapped]], bflipset -- vols[v][vtblpnum2].pnum, vtblpnum1, sqnum; wlar, q, apebs; err)] ( ubi-cons(apebs, vols0, wlar, q, bflipset0, vtblpnum0, sqnum0) ∧ ubi-io-inv(apebs) ∧ id(apebs, apebs1, mapped-pebs(vols0)) ∧ q ⊆ q1 ∧ (err = ESUCCESS → q = []) ∧ (err = ESUCCESS ∨ ⌊err⌋ ) → ⟨ebm_erase#(v, vtblpnum2; avols; err0)⟩ (abs(avols, apebs, vols[v, vols[v][vtblpnum2, unmapped]], q) ∧ err = err0)), VTBL_VOLID ∈ vols

Rule argument

spec: ubi-asm name: inv-erase-all seq: ubi-cons(apebs, vols, wlar, q, bflipset, vtblpnum, sqnum), ubi-io-inv(apebs), apebs0 = apebs, q0 = q ⊦ ⟪ubi_erase_all# (vols, bflipset, vtblpnum, sqnum; wlar, q, apebs; err)⟫ ( ubi-cons(apebs, vols, wlar, q, bflipset, vtblpnum, sqnum) ∧ ubi-io-inv(apebs) ∧ id(apebs, apebs0, mapped-pebs(vols)) ∧ q ⊆ q0 ∧ (err = ESUCCESS → q = []) ∧ (err = ESUCCESS ∨ ⌊err⌋ )) subst: [sqnum, vtblpnum, bflipset, vols, apebs, q, wlar, err, apebs0, q0] → [sqnum, vtblpnum1, bflipset -- vols[v][vtblpnum2].pnum, vols[v, vols[v][vtblpnum2, unmapped]], apebs, q, wlar, err, apebs, q] flags: <all paths>

Additional information

Used simplifier rules: ⊦ 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)% ⊦ # wlar[n, wle] = # wlar; (s)% ⊦ v ∈ vols[v0, ebatbl] ↔ v = v0 ∨ v ∈ vols; (ws)% ⊦ wl-entry(m, stat).status = stat; (s)% ⊦ used ≠ erasing; (s)%wle.status ≠ used ⊦ bflipset-cons(bflipset, wlar[m, wle]) ↔ bflipset-cons(bflipset, wlar) ∧ ¬ m ∈ bflipset; (s)% ⊦ bflipset-cons(bflipset, wlar) → bflipset-cons(bflipset -- n, wlar); (ss)% ⊦ n ∈ ns -- n0 ↔ n ≠ n0 ∧ n ∈ ns; (s)%⊦ v ∈ vols ∧ m < # vols[v] ∧ vols[v][m] = ⌜n⌝ ∧ valid-ebatbl(apebs, wlar, vols, n0) → valid-ebatbl (apebs, wlar[n, wl-entry(m0, erasing)], vols[v, vols[v][m, unmapped]], n0); (ss)%⊦ v ∈ vols → ( valid-vtbl(apebs, vols[v, vols[v][m, ebae]], wlar, n0) ↔ valid-vtbl(apebs, vols, wlar, n0)); (s)%ne-01: ⊦ n ∈ ns → ns ≠ ∅; (forward) from specification set-basic[nat-set]% ⊦ ⌜m⌝ .pnum = m; (s)