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

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

User applied rule insert rewrite lemma

And obtained the following new goals

Proof step 324:
m < # apebs ⊦ valid-peb(apeb) ∧ valid-global-sqn(apebs, n) ∧ apeb.vidhdr.sqn < n → valid-global-sqn(apebs[m, apeb], n)
Proof step 325:
# apebs0 = # wlar, LEB_SIZE = n2 + n0, wlar[vtblpnum1] = wl-entry(m0, used), apebs0[n1] = mkpeb(aehdr, empty, mkempbuf(LEB_SIZE), 0, false), wlar[n1] = wl-entry(m1, free), aehdr.valid?, vtblpnum1 < # wlar, n1 < # wlar, bflipset-cons(bflipset, wlar), is-aligned(n0, EB_PAGE_SIZE), ubi-io-inv(apebs0), ubi-io-inv(apebs0[n1, mkpeb(aehdr, avidhdr(VTBL_VOLID, VTBL_LNUM, sqnum, 0, 0), mkempbuf(LEB_SIZE), 0, false)]), unique-sqns(apebs0), valid-ebatbl(apebs0, wlar, vols, vtblpnum1), valid-eraseq(apebs0, q), valid-eraseq(wlar, q), valid-eraseq(q), valid-eraseq(q + eq-entry(vtblpnum1, VTBL_VOLID × VTBL_LNUM) '), valid-global-sqn(apebs0, sqnum), valid-vtbl(apebs0, vols, wlar, vtblpnum1), valid-wl(apebs0, wlar), n0 ≤ LEB_SIZE ⊦ vtblpnum1 = n1, VTBL_VOLID ∈ vols, vtblpnum1 ∈ q, ( ¬ v ∈ vols ∧ is-encoded(to-vtbl(vols)[v, m], mkempbuf(LEB_SIZE)) ∧ n0 = LEB_SIZE → valid-ebatbl (apebs0[n1, mkpeb(aehdr, avidhdr(VTBL_VOLID, VTBL_LNUM, sqnum, 0, 0), mkempbuf(LEB_SIZE), 0, false)], wlar[vtblpnum1, wl-entry(m0, erasing)][n1, wl-entry(m1, used)], vols[v, fill(mkebatbl(m), unmapped)], n1) ∧ valid-vtbl (apebs0[n1, mkpeb(aehdr, avidhdr(VTBL_VOLID, VTBL_LNUM, sqnum, 0, 0), mkempbuf(LEB_SIZE), 0, false)], vols[v, fill(mkebatbl(m), unmapped)], wlar[vtblpnum1, wl-entry(m0, erasing)][n1, wl-entry(m1, used)], n1)) ∧ ( is-encoded(to-vtbl(vols), mkempbuf(LEB_SIZE)) ∧ n0 = LEB_SIZE → valid-ebatbl (apebs0[n1, mkpeb(aehdr, avidhdr(VTBL_VOLID, VTBL_LNUM, sqnum, 0, 0), mkempbuf(LEB_SIZE), 0, false)], wlar[vtblpnum1, wl-entry(m0, erasing)][n1, wl-entry(m1, used)], vols, n1) ∧ valid-vtbl (apebs0[n1, mkpeb(aehdr, avidhdr(VTBL_VOLID, VTBL_LNUM, sqnum, 0, 0), mkempbuf(LEB_SIZE), 0, false)], vols, wlar[vtblpnum1, wl-entry(m0, erasing)][n1, wl-entry(m1, used)], n1)) ∧ bflipset-cons(bflipset -- vtblpnum1, wlar[vtblpnum1, wl-entry(m0, erasing)][n1, wl-entry(m1, used)]) ∧ valid-eraseq (apebs0[n1, mkpeb(aehdr, avidhdr(VTBL_VOLID, VTBL_LNUM, sqnum, 0, 0), mkempbuf(LEB_SIZE), 0, false)], q + eq-entry(vtblpnum1, VTBL_VOLID × VTBL_LNUM) ') ∧ valid-eraseq(wlar[vtblpnum1, wl-entry(m0, erasing)][n1, wl-entry(m1, used)], q + eq-entry(vtblpnum1, VTBL_VOLID × VTBL_LNUM) ') ∧ valid-wl (apebs0[n1, mkpeb(aehdr, avidhdr(VTBL_VOLID, VTBL_LNUM, sqnum, 0, 0), mkempbuf(LEB_SIZE), 0, false)], wlar[vtblpnum1, wl-entry(m0, erasing)][n1, wl-entry(m1, used)]) ∧ valid-global-sqn(apebs0[n1, mkpeb(aehdr, avidhdr(VTBL_VOLID, VTBL_LNUM, sqnum, 0, 0), mkempbuf(LEB_SIZE), 0, false)], sqnum + 1) ∧ unique-sqns(apebs0[n1, mkpeb(aehdr, avidhdr(VTBL_VOLID, VTBL_LNUM, sqnum, 0, 0), mkempbuf(LEB_SIZE), 0, false)]), n1 < # apebs0 ∧ valid-peb(mkpeb(aehdr, avidhdr(VTBL_VOLID, VTBL_LNUM, sqnum, 0, 0), mkempbuf(LEB_SIZE), 0, false)) ∧ valid-global-sqn(apebs0, sqnum + 1) ∧ mkpeb(aehdr, avidhdr(VTBL_VOLID, VTBL_LNUM, sqnum, 0, 0), mkempbuf(LEB_SIZE), 0, false).vidhdr.sqn < sqnum + 1
Proof step 330:
# apebs0 = # wlar, LEB_SIZE = n2 + n0, wlar[vtblpnum1] = wl-entry(m0, used), apebs0[n1] = mkpeb(aehdr, empty, mkempbuf(LEB_SIZE), 0, false), wlar[n1] = wl-entry(m1, free), aehdr.valid?, vtblpnum1 < # wlar, n1 < # wlar, n1 < # apebs0, mkpeb(aehdr, avidhdr(VTBL_VOLID, VTBL_LNUM, sqnum, 0, 0), mkempbuf(LEB_SIZE), 0, false).vidhdr.sqn < sqnum + 1, bflipset-cons(bflipset, wlar), is-aligned(n0, EB_PAGE_SIZE), ubi-io-inv(apebs0), ubi-io-inv(apebs0[n1, mkpeb(aehdr, avidhdr(VTBL_VOLID, VTBL_LNUM, sqnum, 0, 0), mkempbuf(LEB_SIZE), 0, false)]), unique-sqns(apebs0), valid-ebatbl(apebs0, wlar, vols, vtblpnum1), valid-eraseq(apebs0, q), valid-eraseq(wlar, q), valid-eraseq(q), valid-eraseq(q + eq-entry(vtblpnum1, VTBL_VOLID × VTBL_LNUM) '), valid-global-sqn(apebs0, sqnum), valid-global-sqn(apebs0, sqnum + 1), valid-peb(mkpeb(aehdr, avidhdr(VTBL_VOLID, VTBL_LNUM, sqnum, 0, 0), mkempbuf(LEB_SIZE), 0, false)), valid-vtbl(apebs0, vols, wlar, vtblpnum1), valid-wl(apebs0, wlar), n0 ≤ LEB_SIZE ⊦ vtblpnum1 = n1, VTBL_VOLID ∈ vols, vtblpnum1 ∈ q, ( ¬ v ∈ vols ∧ is-encoded(to-vtbl(vols)[v, m], mkempbuf(LEB_SIZE)) ∧ n0 = LEB_SIZE → valid-ebatbl (apebs0[n1, mkpeb(aehdr, avidhdr(VTBL_VOLID, VTBL_LNUM, sqnum, 0, 0), mkempbuf(LEB_SIZE), 0, false)], wlar[vtblpnum1, wl-entry(m0, erasing)][n1, wl-entry(m1, used)], vols[v, fill(mkebatbl(m), unmapped)], n1) ∧ valid-vtbl (apebs0[n1, mkpeb(aehdr, avidhdr(VTBL_VOLID, VTBL_LNUM, sqnum, 0, 0), mkempbuf(LEB_SIZE), 0, false)], vols[v, fill(mkebatbl(m), unmapped)], wlar[vtblpnum1, wl-entry(m0, erasing)][n1, wl-entry(m1, used)], n1)) ∧ ( is-encoded(to-vtbl(vols), mkempbuf(LEB_SIZE)) ∧ n0 = LEB_SIZE → valid-ebatbl (apebs0[n1, mkpeb(aehdr, avidhdr(VTBL_VOLID, VTBL_LNUM, sqnum, 0, 0), mkempbuf(LEB_SIZE), 0, false)], wlar[vtblpnum1, wl-entry(m0, erasing)][n1, wl-entry(m1, used)], vols, n1) ∧ valid-vtbl (apebs0[n1, mkpeb(aehdr, avidhdr(VTBL_VOLID, VTBL_LNUM, sqnum, 0, 0), mkempbuf(LEB_SIZE), 0, false)], vols, wlar[vtblpnum1, wl-entry(m0, erasing)][n1, wl-entry(m1, used)], n1)) ∧ bflipset-cons(bflipset -- vtblpnum1, wlar[vtblpnum1, wl-entry(m0, erasing)][n1, wl-entry(m1, used)]) ∧ valid-eraseq (apebs0[n1, mkpeb(aehdr, avidhdr(VTBL_VOLID, VTBL_LNUM, sqnum, 0, 0), mkempbuf(LEB_SIZE), 0, false)], q + eq-entry(vtblpnum1, VTBL_VOLID × VTBL_LNUM) ') ∧ valid-eraseq(wlar[vtblpnum1, wl-entry(m0, erasing)][n1, wl-entry(m1, used)], q + eq-entry(vtblpnum1, VTBL_VOLID × VTBL_LNUM) ') ∧ valid-wl (apebs0[n1, mkpeb(aehdr, avidhdr(VTBL_VOLID, VTBL_LNUM, sqnum, 0, 0), mkempbuf(LEB_SIZE), 0, false)], wlar[vtblpnum1, wl-entry(m0, erasing)][n1, wl-entry(m1, used)]) ∧ true ∧ unique-sqns(apebs0[n1, mkpeb(aehdr, avidhdr(VTBL_VOLID, VTBL_LNUM, sqnum, 0, 0), mkempbuf(LEB_SIZE), 0, false)])

Rule argument

spec: ubi-base name: valid-global-sqn-add-valid seq: m < # apebs ⊦ valid-peb(apeb) ∧ valid-global-sqn(apebs, n) ∧ apeb.vidhdr.sqn < n → valid-global-sqn(apebs[m, apeb], n) subst: [n, apeb, m, apebs] → [sqnum + 1, mkpeb (aehdr, avidhdr(VTBL_VOLID, VTBL_LNUM, sqnum, 0, 0), mkempbuf(LEB_SIZE), 0, false), n1, apebs0] flags: <all paths>

Additional information

Used terms: sqnum + 1, mkpeb (aehdr, avidhdr(VTBL_VOLID, VTBL_LNUM, sqnum, 0, 0), mkempbuf(LEB_SIZE), 0, false), n1, apebs0