[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 396 from proof prepost-atomic-leb-change (previous step)

# apebs0 = # wlar, LEB_SIZE = n2 + n0, wlar[m] = wl-entry(m2, used), vols[v][m0] = ⌜m⌝ , wlar[n1] = wl-entry(m1, free), apebs0[n1] = mkpeb(aehdr, empty, mkempbuf(LEB_SIZE), 0, false), aehdr.valid?, m0 < # vols[v], n1 < # wlar, m < # wlar, bflipset-cons(bflipset, wlar), bflipset-cons(bflipset -- m, wlar), is-aligned(n0, EB_PAGE_SIZE), ubi-io-inv(apebs0[n1, mkpeb(aehdr, avidhdr(v, m0, sqnum, 0, 0), mkempbuf(LEB_SIZE), 0, false)]), ubi-io-inv(apebs0), unique-sqns(apebs0), valid-ebatbl(apebs0, wlar, vols, vtblpnum1), valid-eraseq(q), valid-eraseq(wlar, q), valid-eraseq(apebs0, q), valid-eraseq(q + eq-entry(m, v × m0) '), valid-global-sqn(apebs0, sqnum + 1), valid-global-sqn(apebs0, sqnum), valid-peb(mkpeb(aehdr, avidhdr(v, m0, sqnum, 0, 0), mkempbuf(LEB_SIZE), 0, false)), valid-peb(v, m0, apebs0[m]), valid-vtbl(apebs0, vols, wlar, vtblpnum1), valid-wl(apebs0, wlar), v ∈ vols, n0 ≤ LEB_SIZE ⊦ m = vtblpnum1, vtblpnum1 = n1, m ∈ q, vtblpnum1 ∈ q, VTBL_VOLID ∈ vols, valid-ebatbl (apebs0[n1, mkpeb(aehdr, avidhdr(v, m0, sqnum, 0, 0), mkempbuf(LEB_SIZE), 0, false)], wlar[m, wl-entry(m2, erasing)][n1, wl-entry(m1, used)], vols[v, vols[v][m0, ⌜n1⌝ ]], vtblpnum1) ∧ valid-eraseq(apebs0[n1, mkpeb(aehdr, avidhdr(v, m0, sqnum, 0, 0), mkempbuf(LEB_SIZE), 0, false)], q + eq-entry(m, v × m0) ') ∧ valid-eraseq(wlar[m, wl-entry(m2, erasing)][n1, wl-entry(m1, used)], q + eq-entry(m, v × m0) ') ∧ valid-wl (apebs0[n1, mkpeb(aehdr, avidhdr(v, m0, sqnum, 0, 0), mkempbuf(LEB_SIZE), 0, false)], wlar[m, wl-entry(m2, erasing)][n1, wl-entry(m1, used)]) ∧ unique-sqns(apebs0[n1, mkpeb(aehdr, avidhdr(v, m0, sqnum, 0, 0), mkempbuf(LEB_SIZE), 0, false)])

User applied rule insert rewrite lemma

And obtained the following new goals

Proof step 397:
stat ≠ erasing ⊦ wlar[n] = wl-entry(m0, stat) → (valid-eraseq(wlar[n, wl-entry(m1, used)], q) ↔ valid-eraseq(wlar, q))
Proof step 398:
# apebs0 = # wlar, LEB_SIZE = n2 + n0, apebs0[n1] = mkpeb(aehdr, empty, mkempbuf(LEB_SIZE), 0, false), wlar[n1] = wl-entry(m1, free), vols[v][m0] = ⌜m⌝ , wlar[m] = wl-entry(m2, used), wlar[m, wl-entry(m2, erasing)][n1] = wl-entry(m1, free), aehdr.valid?, m < # wlar, n1 < # wlar, m0 < # vols[v], bflipset-cons(bflipset -- m, wlar), bflipset-cons(bflipset, wlar), is-aligned(n0, EB_PAGE_SIZE), ubi-io-inv(apebs0), ubi-io-inv(apebs0[n1, mkpeb(aehdr, avidhdr(v, m0, sqnum, 0, 0), mkempbuf(LEB_SIZE), 0, false)]), unique-sqns(apebs0), valid-ebatbl(apebs0, wlar, vols, vtblpnum1), valid-eraseq(q + eq-entry(m, v × m0) '), valid-eraseq(apebs0, q), valid-eraseq(wlar, q), valid-eraseq(q), valid-global-sqn(apebs0, sqnum), valid-global-sqn(apebs0, sqnum + 1), valid-peb(v, m0, apebs0[m]), valid-peb(mkpeb(aehdr, avidhdr(v, m0, sqnum, 0, 0), mkempbuf(LEB_SIZE), 0, false)), valid-vtbl(apebs0, vols, wlar, vtblpnum1), valid-wl(apebs0, wlar), v ∈ vols, n0 ≤ LEB_SIZE ⊦ free = erasing, m = vtblpnum1, vtblpnum1 = n1, VTBL_VOLID ∈ vols, vtblpnum1 ∈ q, m ∈ q, valid-ebatbl (apebs0[n1, mkpeb(aehdr, avidhdr(v, m0, sqnum, 0, 0), mkempbuf(LEB_SIZE), 0, false)], wlar[m, wl-entry(m2, erasing)][n1, wl-entry(m1, used)], vols[v, vols[v][m0, ⌜n1⌝ ]], vtblpnum1) ∧ valid-eraseq(apebs0[n1, mkpeb(aehdr, avidhdr(v, m0, sqnum, 0, 0), mkempbuf(LEB_SIZE), 0, false)], q + eq-entry(m, v × m0) ') ∧ valid-eraseq(wlar[m, wl-entry(m2, erasing)], q + eq-entry(m, v × m0) ') ∧ valid-wl (apebs0[n1, mkpeb(aehdr, avidhdr(v, m0, sqnum, 0, 0), mkempbuf(LEB_SIZE), 0, false)], wlar[m, wl-entry(m2, erasing)][n1, wl-entry(m1, used)]) ∧ unique-sqns(apebs0[n1, mkpeb(aehdr, avidhdr(v, m0, sqnum, 0, 0), mkempbuf(LEB_SIZE), 0, false)])

Rule argument

spec: ubi-base name: valid-eraseqw-use seq: stat ≠ erasing ⊦ wlar[n] = wl-entry(m0, stat) → ( valid-eraseq(wlar[n, wl-entry(m1, used)], q) ↔ valid-eraseq(wlar, q)) subst: [stat, m0, q, m1, n, wlar] → [free, m1, q + eq-entry(m, v × m0) ', m1, n1, wlar[m, wl-entry(m2, erasing)]] flags: <all paths>

Additional information

Used simplifier rules: lf-mapped-valid-peb: ⊦ v ∈ vols ∧ m < # vols[v] ∧ vols[v][m] = ⌜n⌝ ∧ valid-ebatbl(apebs, wlar, vols, n0) ∧ valid-wl(apebs, wlar) → valid-peb(v, m, apebs[n]);%lf-mapped-info: ⊦ v ∈ vols ∧ m < # vols[v] ∧ vols[v][m] = ⌜n⌝ ∧ valid-ebatbl(apebs, wlar, vols, n0) → wlar[n].status = used ∧ n ≠ n0 ∧ n < # wlar;%lf-used-valid-peb: ⊦ n < # wlar ∧ wlar[n] = wl-entry(m, used) ∧ apebs[n] = apeb ∧ valid-wl(apebs, wlar) → valid-peb(apeb);%lf-used-info: ⊦ n < # wlar ∧ wlar[n] = wl-entry(m, used) ∧ valid-eraseq(wlar, q) → ¬ n ∈ q;% ⊦ free ≠ erasing; (s)%n < # wlar ⊦ valid-eraseq(wlar, q) ∧ wlar[n] = wl-entry(m, free) → ¬ n ∈ q; (s)% ⊦ ¬ valid-peb(mkpeb(aehdr, empty, buf, m, boolvar)); (s)%m ≠ n ⊦ wlar[m, wle][n] = wlar[n]; (s) Used terms: free, m1, q + eq-entry(m, v × m0) ', m1, n1, wlar[m, wl-entry(m2, erasing)]