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

# apebs0 = # wlar, LEB_SIZE = n4 + align↑(datasize(buf, LEB_SIZE), EB_PAGE_SIZE), LEB_SIZE = n2 + n0, LEB_SIZE = n3 + align↑(datasize(buf, n0), EB_PAGE_SIZE), 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), aehdr.valid?, m < # wlar, m0 < # vols[v], n1 < # wlar, bflipset-cons(bflipset, wlar), is-aligned(n0, EB_PAGE_SIZE), ubi-io-inv(apebs0[n1, mkpeb(aehdr, avidhdr(v, m0, sqnum, datasize(buf, n0), checksum(buf, datasize(buf, n0))), mkempbuf(LEB_SIZE), 0, false)]), ubi-io-inv(apebs0), ubi-io-inv (apebs0 [n1, mkpeb (aehdr, avidhdr(v, m0, sqnum, datasize(buf, n0), checksum(buf, datasize(buf, n0))), subarray(buf, 0, n0) + mkempbuf(n2), align↑(datasize(buf, n0), EB_PAGE_SIZE), 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-peb(v, m0, apebs0[m]), valid-peb (mkpeb (aehdr, avidhdr(v, m0, sqnum, datasize(buf, n0), checksum(buf, datasize(buf, n0))), subarray(buf, 0, n0) + mkempbuf(n2), align↑(datasize(buf, n0), EB_PAGE_SIZE), false)), valid-vtbl(apebs0, vols, wlar, vtblpnum1), valid-wl(apebs0, wlar), v ∈ vols, align↑(datasize(buf, LEB_SIZE), EB_PAGE_SIZE) ≤ LEB_SIZE, align↑(datasize(buf, n0), EB_PAGE_SIZE) ≤ # buf, align↑(datasize(buf, n0), EB_PAGE_SIZE) ≤ LEB_SIZE, n0 ≤ LEB_SIZE, n0 ≤ # buf ⊦ m = vtblpnum1, vtblpnum1 = n1, valid-wl (apebs0 [n1, mkpeb (aehdr, avidhdr(v, m0, sqnum, datasize(buf, n0), checksum(buf, datasize(buf, n0))), subarray(buf, 0, n0) + mkempbuf(n2), align↑(datasize(buf, n0), EB_PAGE_SIZE), false) ], wlar[m, wl-entry(m2, erasing)][n1, wl-entry(m1, used)]), VTBL_VOLID ∈ vols, vtblpnum1 ∈ q, m ∈ q, ∃ buf0. buf = mkempbuf(n0) + buf0

User applied rule insert rewrite lemma

And obtained the following new goals

Proof step 167:
n < # apebs, # apebs = # wlar ⊦ valid-wl(apebs, wlar) ∧ valid-peb(apeb) ∧ (valid-sqns(apeb.vidhdr.vol, apeb.vidhdr.leb, apebs) ≠ ∅ → apeb.vidhdr.sqn > valid-sqns(apeb.vidhdr.vol, apeb.vidhdr.leb, apebs).max) ∧ apeb.vidhdr.vol ∈ vols ∧ apeb.vidhdr.leb < # vols[apeb.vidhdr.vol] ∧ vols[apeb.vidhdr.vol][apeb.vidhdr.leb] = unmapped ∧ valid-ebatbl(apebs, wlar, vols, n0) ∧ valid-vtbl(apebs, vols, wlar, n0) ∧ ¬ VTBL_VOLID ∈ vols ∧ apeb.echdr.ec = m0 → valid-wl(apebs[n, apeb], wlar[n, wl-entry(m0, used)])
Proof step 168:
# apebs0 = # wlar, LEB_SIZE = n3 + align↑(datasize(buf, n0), EB_PAGE_SIZE), LEB_SIZE = n2 + n0, LEB_SIZE = n4 + align↑(datasize(buf, LEB_SIZE), EB_PAGE_SIZE), 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?, n1 < # wlar, m0 < # vols[v], m < # wlar, bflipset-cons(bflipset, wlar), is-aligned(n0, EB_PAGE_SIZE), ubi-io-inv (apebs0 [n1, mkpeb (aehdr, avidhdr(v, m0, sqnum, datasize(buf, n0), checksum(buf, datasize(buf, n0))), subarray(buf, 0, n0) + mkempbuf(n2), align↑(datasize(buf, n0), EB_PAGE_SIZE), false) ]), ubi-io-inv(apebs0), ubi-io-inv(apebs0[n1, mkpeb(aehdr, avidhdr(v, m0, sqnum, datasize(buf, n0), checksum(buf, datasize(buf, n0))), mkempbuf(LEB_SIZE), 0, false)]), 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), valid-peb (mkpeb (aehdr, avidhdr(v, m0, sqnum, datasize(buf, n0), checksum(buf, datasize(buf, n0))), subarray(buf, 0, n0) + mkempbuf(n2), align↑(datasize(buf, n0), EB_PAGE_SIZE), false)), valid-peb(v, m0, apebs0[m]), valid-vtbl(apebs0, vols, wlar, vtblpnum1), valid-wl(apebs0, wlar), v ∈ vols, n0 ≤ # buf, n0 ≤ LEB_SIZE, align↑(datasize(buf, n0), EB_PAGE_SIZE) ≤ LEB_SIZE, align↑(datasize(buf, n0), EB_PAGE_SIZE) ≤ # buf, align↑(datasize(buf, LEB_SIZE), EB_PAGE_SIZE) ≤ LEB_SIZE ⊦ m = vtblpnum1, vtblpnum1 = n1, valid-wl (apebs0 [n1, mkpeb (aehdr, avidhdr(v, m0, sqnum, datasize(buf, n0), checksum(buf, datasize(buf, n0))), subarray(buf, 0, n0) + mkempbuf(n2), align↑(datasize(buf, n0), EB_PAGE_SIZE), false) ], wlar[m, wl-entry(m2, erasing)][n1, wl-entry(m1, used)]), m ∈ q, vtblpnum1 ∈ q, VTBL_VOLID ∈ vols, ∃ buf0. buf = mkempbuf(n0) + buf0, n1 < # apebs0 ∧ # apebs0 = # wlar[m, wl-entry(m2, erasing)] ∧ valid-wl(apebs0, wlar[m, wl-entry(m2, erasing)]) ∧ valid-peb (mkpeb (aehdr, avidhdr(v, m0, sqnum, datasize(buf, n0), checksum(buf, datasize(buf, n0))), subarray(buf, 0, n0) + mkempbuf(n2), align↑(datasize(buf, n0), EB_PAGE_SIZE), false)) ∧ ( valid-sqns (mkpeb (aehdr, avidhdr(v, m0, sqnum, datasize(buf, n0), checksum(buf, datasize(buf, n0))), subarray(buf, 0, n0) + mkempbuf(n2), align↑(datasize(buf, n0), EB_PAGE_SIZE), false) .vidhdr .vol, mkpeb (aehdr, avidhdr(v, m0, sqnum, datasize(buf, n0), checksum(buf, datasize(buf, n0))), subarray(buf, 0, n0) + mkempbuf(n2), align↑(datasize(buf, n0), EB_PAGE_SIZE), false) .vidhdr .leb, apebs0) ≠ ∅ → mkpeb (aehdr, avidhdr(v, m0, sqnum, datasize(buf, n0), checksum(buf, datasize(buf, n0))), subarray(buf, 0, n0) + mkempbuf(n2), align↑(datasize(buf, n0), EB_PAGE_SIZE), false) .vidhdr .sqn > valid-sqns (mkpeb (aehdr, avidhdr(v, m0, sqnum, datasize(buf, n0), checksum(buf, datasize(buf, n0))), subarray(buf, 0, n0) + mkempbuf(n2), align↑(datasize(buf, n0), EB_PAGE_SIZE), false) .vidhdr .vol, mkpeb (aehdr, avidhdr(v, m0, sqnum, datasize(buf, n0), checksum(buf, datasize(buf, n0))), subarray(buf, 0, n0) + mkempbuf(n2), align↑(datasize(buf, n0), EB_PAGE_SIZE), false) .vidhdr .leb, apebs0) .max) ∧ mkpeb (aehdr, avidhdr(v, m0, sqnum, datasize(buf, n0), checksum(buf, datasize(buf, n0))), subarray(buf, 0, n0) + mkempbuf(n2), align↑(datasize(buf, n0), EB_PAGE_SIZE), false) .vidhdr .vol ∈ vols[v, vols[v][m0, unmapped]] ∧ mkpeb (aehdr, avidhdr(v, m0, sqnum, datasize(buf, n0), checksum(buf, datasize(buf, n0))), subarray(buf, 0, n0) + mkempbuf(n2), align↑(datasize(buf, n0), EB_PAGE_SIZE), false) .vidhdr .leb < # vols[v, vols[v][m0, unmapped]] [mkpeb (aehdr, avidhdr(v, m0, sqnum, datasize(buf, n0), checksum(buf, datasize(buf, n0))), subarray(buf, 0, n0) + mkempbuf(n2), align↑(datasize(buf, n0), EB_PAGE_SIZE), false) .vidhdr .vol ] ∧ vols[v, vols[v][m0, unmapped]] [mkpeb (aehdr, avidhdr(v, m0, sqnum, datasize(buf, n0), checksum(buf, datasize(buf, n0))), subarray(buf, 0, n0) + mkempbuf(n2), align↑(datasize(buf, n0), EB_PAGE_SIZE), false) .vidhdr .vol ] [mkpeb (aehdr, avidhdr(v, m0, sqnum, datasize(buf, n0), checksum(buf, datasize(buf, n0))), subarray(buf, 0, n0) + mkempbuf(n2), align↑(datasize(buf, n0), EB_PAGE_SIZE), false) .vidhdr .leb ] = unmapped ∧ valid-ebatbl(apebs0, wlar[m, wl-entry(m2, erasing)], vols[v, vols[v][m0, unmapped]], vtblpnum1) ∧ valid-vtbl(apebs0, vols[v, vols[v][m0, unmapped]], wlar[m, wl-entry(m2, erasing)], vtblpnum1) ∧ ¬ VTBL_VOLID ∈ vols[v, vols[v][m0, unmapped]] ∧ mkpeb (aehdr, avidhdr(v, m0, sqnum, datasize(buf, n0), checksum(buf, datasize(buf, n0))), subarray(buf, 0, n0) + mkempbuf(n2), align↑(datasize(buf, n0), EB_PAGE_SIZE), false) .echdr .ec = m1

Rule argument

spec: ubi-base name: valid-wl-map seq: n < # apebs, # apebs = # wlar ⊦ valid-wl(apebs, wlar) ∧ valid-peb(apeb) ∧ ( valid-sqns(apeb.vidhdr.vol, apeb.vidhdr.leb, apebs) ≠ ∅ → apeb.vidhdr.sqn > valid-sqns(apeb.vidhdr.vol, apeb.vidhdr.leb, apebs) .max) ∧ apeb.vidhdr.vol ∈ vols ∧ apeb.vidhdr.leb < # vols[apeb.vidhdr.vol] ∧ vols[apeb.vidhdr.vol][apeb.vidhdr.leb] = unmapped ∧ valid-ebatbl(apebs, wlar, vols, n0) ∧ valid-vtbl(apebs, vols, wlar, n0) ∧ ¬ VTBL_VOLID ∈ vols ∧ apeb.echdr.ec = m0 → valid-wl(apebs[n, apeb], wlar[n, wl-entry(m0, used)]) subst: [vols, n0, m0, wlar, apeb, n, apebs] → [vols[v, vols[v][m0, unmapped]], vtblpnum1, m1, wlar[m, wl-entry(m2, erasing)], mkpeb (aehdr, avidhdr (v, m0, sqnum, datasize(buf, n0), checksum(buf, datasize(buf, n0))), subarray(buf, 0, n0) + mkempbuf(n2), align↑(datasize(buf, n0), EB_PAGE_SIZE), false), n1, apebs0] flags: <all paths>

Additional information

Used terms: vols[v, vols[v][m0, unmapped]], vtblpnum1, m1, wlar[m, wl-entry(m2, erasing)], mkpeb (aehdr, avidhdr (v, m0, sqnum, datasize(buf, n0), checksum(buf, datasize(buf, n0))), subarray(buf, 0, n0) + mkempbuf(n2), align↑(datasize(buf, n0), EB_PAGE_SIZE), false), n1, apebs0