[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 70 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), lref = VTBL_VOLID × VTBL_LNUM, q0 = q, vtblpnum = vtblpnum1, aehdr.valid?, n1 < # wlar, vtblpnum < # wlar, bflipset-cons(bflipset, wlar), is-aligned(n0, EB_PAGE_SIZE), ubi-io-inv (apebs0[n1, mkpeb(aehdr, avidhdr(VTBL_VOLID, VTBL_LNUM, 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(VTBL_VOLID, VTBL_LNUM, 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(apebs0, q), valid-eraseq(wlar, q), valid-eraseq(q), valid-global-sqn(apebs0, sqnum), valid-vtbl(apebs0, vols, wlar, vtblpnum1), valid-wl(apebs0, wlar), 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 ⊦ ⟪wlar := wlar[vtblpnum, wlar[vtblpnum].status:= erasing][n1, wl-entry(wlar[vtblpnum, wlar[vtblpnum].status:= erasing][n1].ec, used)]⟫ ( # apebs0 = # wlar ∧ unique-sqns (apebs0 [n1, mkpeb (aehdr, avidhdr(VTBL_VOLID, VTBL_LNUM, sqnum, datasize(buf, n0), checksum(buf, datasize(buf, n0))), subarray(buf, 0, n0) + mkempbuf(n2), align↑(datasize(buf, n0), EB_PAGE_SIZE), false) ]) ∧ valid-global-sqn (apebs0 [n1, mkpeb (aehdr, avidhdr(VTBL_VOLID, VTBL_LNUM, sqnum, datasize(buf, n0), checksum(buf, datasize(buf, n0))), subarray(buf, 0, n0) + mkempbuf(n2), align↑(datasize(buf, n0), EB_PAGE_SIZE), false) ], sqnum + 1) ∧ valid-wl (apebs0 [n1, mkpeb (aehdr, avidhdr(VTBL_VOLID, VTBL_LNUM, sqnum, datasize(buf, n0), checksum(buf, datasize(buf, n0))), subarray(buf, 0, n0) + mkempbuf(n2), align↑(datasize(buf, n0), EB_PAGE_SIZE), false) ], wlar) ∧ valid-eraseq(q0 + eq-entry(vtblpnum1, VTBL_VOLID × VTBL_LNUM) ') ∧ valid-eraseq(wlar, q0 + eq-entry(vtblpnum1, VTBL_VOLID × VTBL_LNUM) ') ∧ valid-eraseq (apebs0 [n1, mkpeb (aehdr, avidhdr(VTBL_VOLID, VTBL_LNUM, sqnum, datasize(buf, n0), checksum(buf, datasize(buf, n0))), subarray(buf, 0, n0) + mkempbuf(n2), align↑(datasize(buf, n0), EB_PAGE_SIZE), false) ], q0 + eq-entry(vtblpnum1, VTBL_VOLID × VTBL_LNUM) ') ∧ bflipset-cons(bflipset -- vtblpnum1, wlar) ∧ ( is-encoded(to-vtbl(vols), subarray(buf, 0, LEB_SIZE)) ∧ n0 = LEB_SIZE → valid-ebatbl (apebs0 [n1, mkpeb (aehdr, avidhdr(VTBL_VOLID, VTBL_LNUM, sqnum, datasize(buf, LEB_SIZE), checksum(buf, datasize(buf, LEB_SIZE))), subarray(buf, 0, LEB_SIZE), align↑(datasize(buf, LEB_SIZE), EB_PAGE_SIZE), false) ], wlar, vols, n1) ∧ valid-vtbl (apebs0 [n1, mkpeb (aehdr, avidhdr(VTBL_VOLID, VTBL_LNUM, sqnum, datasize(buf, LEB_SIZE), checksum(buf, datasize(buf, LEB_SIZE))), subarray(buf, 0, LEB_SIZE), align↑(datasize(buf, LEB_SIZE), EB_PAGE_SIZE), false) ], vols, wlar, n1)) ∧ (∀ v0, m. ¬ v0 ∈ vols ∧ is-encoded(to-vtbl(vols)[v0, m], subarray(buf, 0, LEB_SIZE)) ∧ n0 = LEB_SIZE → valid-ebatbl (apebs0 [n1, mkpeb (aehdr, avidhdr(VTBL_VOLID, VTBL_LNUM, sqnum, datasize(buf, LEB_SIZE), checksum(buf, datasize(buf, LEB_SIZE))), subarray(buf, 0, LEB_SIZE), align↑(datasize(buf, LEB_SIZE), EB_PAGE_SIZE), false) ], wlar, vols[v0, fill(mkebatbl(m), unmapped)], n1) ∧ valid-vtbl (apebs0 [n1, mkpeb (aehdr, avidhdr(VTBL_VOLID, VTBL_LNUM, sqnum, datasize(buf, LEB_SIZE), checksum(buf, datasize(buf, LEB_SIZE))), subarray(buf, 0, LEB_SIZE), align↑(datasize(buf, LEB_SIZE), EB_PAGE_SIZE), false) ], vols[v0, fill(mkebatbl(m), unmapped)], wlar, n1)) ∧ q + eq-entry(vtblpnum, lref) = q0 + eq-entry(vtblpnum1, VTBL_VOLID × VTBL_LNUM) ' ∧ id (apebs0 [n1, mkpeb (aehdr, avidhdr(VTBL_VOLID, VTBL_LNUM, sqnum, datasize(buf, n0), checksum(buf, datasize(buf, n0))), subarray(buf, 0, n0) + mkempbuf(n2), align↑(datasize(buf, n0), EB_PAGE_SIZE), false) ], apebs0, mapped-pebs(vols))), vtblpnum1 = n1, VTBL_VOLID ∈ vols, vtblpnum1 ∈ q, ∃ buf0. buf = mkempbuf(n0) + buf0

Heuristic symbolic execution applied rule assign right

And obtained the following new goals

Proof step 71:
# 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[n1] = wl-entry(m1, free), apebs0[n1] = mkpeb(aehdr, empty, mkempbuf(LEB_SIZE), 0, false), lref = VTBL_VOLID × VTBL_LNUM, q0 = q, vtblpnum = vtblpnum1, aehdr.valid?, n1 < # wlar[vtblpnum, wlar[vtblpnum].status:= erasing], vtblpnum < # wlar, n1 < # wlar, bflipset-cons(bflipset, wlar), is-aligned(n0, EB_PAGE_SIZE), ubi-io-inv (apebs0 [n1, mkpeb (aehdr, avidhdr(VTBL_VOLID, VTBL_LNUM, 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(VTBL_VOLID, VTBL_LNUM, 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-global-sqn(apebs0, sqnum), valid-vtbl(apebs0, vols, wlar, vtblpnum1), valid-wl(apebs0, wlar), 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 ⊦ vtblpnum1 = n1, vtblpnum1 ∈ q, VTBL_VOLID ∈ vols, ∃ buf0. buf = mkempbuf(n0) + buf0, # apebs0 = # wlar[vtblpnum, wlar[vtblpnum].status:= erasing][n1, wl-entry(wlar[vtblpnum, wlar[vtblpnum].status:= erasing][n1].ec, used)] ∧ unique-sqns (apebs0 [n1, mkpeb (aehdr, avidhdr(VTBL_VOLID, VTBL_LNUM, sqnum, datasize(buf, n0), checksum(buf, datasize(buf, n0))), subarray(buf, 0, n0) + mkempbuf(n2), align↑(datasize(buf, n0), EB_PAGE_SIZE), false) ]) ∧ valid-global-sqn (apebs0 [n1, mkpeb (aehdr, avidhdr(VTBL_VOLID, VTBL_LNUM, sqnum, datasize(buf, n0), checksum(buf, datasize(buf, n0))), subarray(buf, 0, n0) + mkempbuf(n2), align↑(datasize(buf, n0), EB_PAGE_SIZE), false) ], sqnum + 1) ∧ valid-wl (apebs0 [n1, mkpeb (aehdr, avidhdr(VTBL_VOLID, VTBL_LNUM, sqnum, datasize(buf, n0), checksum(buf, datasize(buf, n0))), subarray(buf, 0, n0) + mkempbuf(n2), align↑(datasize(buf, n0), EB_PAGE_SIZE), false) ], wlar[vtblpnum, wlar[vtblpnum].status:= erasing][n1, wl-entry(wlar[vtblpnum, wlar[vtblpnum].status:= erasing][n1].ec, used)]) ∧ valid-eraseq(q0 + eq-entry(vtblpnum1, VTBL_VOLID × VTBL_LNUM) ') ∧ valid-eraseq (wlar[vtblpnum, wlar[vtblpnum].status:= erasing][n1, wl-entry(wlar[vtblpnum, wlar[vtblpnum].status:= erasing][n1].ec, used)], q0 + eq-entry(vtblpnum1, VTBL_VOLID × VTBL_LNUM) ') ∧ valid-eraseq (apebs0 [n1, mkpeb (aehdr, avidhdr(VTBL_VOLID, VTBL_LNUM, sqnum, datasize(buf, n0), checksum(buf, datasize(buf, n0))), subarray(buf, 0, n0) + mkempbuf(n2), align↑(datasize(buf, n0), EB_PAGE_SIZE), false) ], q0 + eq-entry(vtblpnum1, VTBL_VOLID × VTBL_LNUM) ') ∧ bflipset-cons (bflipset -- vtblpnum1, wlar[vtblpnum, wlar[vtblpnum].status:= erasing][n1, wl-entry(wlar[vtblpnum, wlar[vtblpnum].status:= erasing][n1].ec, used)]) ∧ ( is-encoded(to-vtbl(vols), subarray(buf, 0, LEB_SIZE)) ∧ n0 = LEB_SIZE → valid-ebatbl (apebs0 [n1, mkpeb (aehdr, avidhdr(VTBL_VOLID, VTBL_LNUM, sqnum, datasize(buf, LEB_SIZE), checksum(buf, datasize(buf, LEB_SIZE))), subarray(buf, 0, LEB_SIZE), align↑(datasize(buf, LEB_SIZE), EB_PAGE_SIZE), false) ], wlar[vtblpnum, wlar[vtblpnum].status:= erasing][n1, wl-entry(wlar[vtblpnum, wlar[vtblpnum].status:= erasing][n1].ec, used)], vols, n1) ∧ valid-vtbl (apebs0 [n1, mkpeb (aehdr, avidhdr(VTBL_VOLID, VTBL_LNUM, sqnum, datasize(buf, LEB_SIZE), checksum(buf, datasize(buf, LEB_SIZE))), subarray(buf, 0, LEB_SIZE), align↑(datasize(buf, LEB_SIZE), EB_PAGE_SIZE), false) ], vols, wlar[vtblpnum, wlar[vtblpnum].status:= erasing][n1, wl-entry(wlar[vtblpnum, wlar[vtblpnum].status:= erasing][n1].ec, used)], n1)) ∧ (∀ v0, m. ¬ v0 ∈ vols ∧ is-encoded(to-vtbl(vols)[v0, m], subarray(buf, 0, LEB_SIZE)) ∧ n0 = LEB_SIZE → valid-ebatbl (apebs0 [n1, mkpeb (aehdr, avidhdr(VTBL_VOLID, VTBL_LNUM, sqnum, datasize(buf, LEB_SIZE), checksum(buf, datasize(buf, LEB_SIZE))), subarray(buf, 0, LEB_SIZE), align↑(datasize(buf, LEB_SIZE), EB_PAGE_SIZE), false) ], wlar[vtblpnum, wlar[vtblpnum].status:= erasing][n1, wl-entry(wlar[vtblpnum, wlar[vtblpnum].status:= erasing][n1].ec, used)], vols[v0, fill(mkebatbl(m), unmapped)], n1) ∧ valid-vtbl (apebs0 [n1, mkpeb (aehdr, avidhdr(VTBL_VOLID, VTBL_LNUM, sqnum, datasize(buf, LEB_SIZE), checksum(buf, datasize(buf, LEB_SIZE))), subarray(buf, 0, LEB_SIZE), align↑(datasize(buf, LEB_SIZE), EB_PAGE_SIZE), false) ], vols[v0, fill(mkebatbl(m), unmapped)], wlar[vtblpnum, wlar[vtblpnum].status:= erasing][n1, wl-entry(wlar[vtblpnum, wlar[vtblpnum].status:= erasing][n1].ec, used)], n1)) ∧ q + eq-entry(vtblpnum, lref) = q0 + eq-entry(vtblpnum1, VTBL_VOLID × VTBL_LNUM) ' ∧ id (apebs0 [n1, mkpeb (aehdr, avidhdr(VTBL_VOLID, VTBL_LNUM, sqnum, datasize(buf, n0), checksum(buf, datasize(buf, n0))), subarray(buf, 0, n0) + mkempbuf(n2), align↑(datasize(buf, n0), EB_PAGE_SIZE), false) ], apebs0, mapped-pebs(vols))

Rule argument

Additional information

Used simplifier rules: ⊦ wle.status:= stat = wl-entry(wle.ec, stat); (s)% ⊦ # wlar[n, wle] = # wlar; (s)% ⊦ valid-vtbl(apebs, vols, wlar, n0) → n0 < # wlar; (ss)