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

# apebs0 = # wlar, LEB_SIZE = n3 + align↑(datasize(buf, LEB_SIZE), EB_PAGE_SIZE), apebs0[n1] = mkpeb(aehdr, empty, mkempbuf(LEB_SIZE), 0, false), wlar[n1] = wl-entry(m1, free), wlar[vtblpnum1] = wl-entry(m0, used), aehdr.valid?, n1 < # wlar, vtblpnum1 < # wlar, bflipset-cons(bflipset, wlar), is-aligned(LEB_SIZE, EB_PAGE_SIZE), is-encoded(to-vtbl(vols)[v, m], subarray(buf, 0, LEB_SIZE)), ubi-io-inv (apebs0 [n1, mkpeb(aehdr, avidhdr(VTBL_VOLID, VTBL_LNUM, sqnum, datasize(buf, LEB_SIZE), checksum(buf, datasize(buf, LEB_SIZE))), mkempbuf(LEB_SIZE), 0, false) ]), ubi-io-inv(apebs0), ubi-io-inv (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) ]), unique-sqns(apebs0), valid-ebatbl(apebs0, wlar, vols, vtblpnum1), valid-eraseq(q + eq-entry(vtblpnum1, VTBL_VOLID × VTBL_LNUM) '), 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, LEB_SIZE), EB_PAGE_SIZE) ≤ # buf, LEB_SIZE ≤ # buf ⊦ vtblpnum1 = n1, v ∈ vols, VTBL_VOLID ∈ vols, vtblpnum1 ∈ q, ∃ buf0. buf = mkempbuf(LEB_SIZE) + buf0, 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[vtblpnum1, wl-entry(m0, erasing)][n1, wl-entry(m1, used)], vols[v, fill(mkebatbl(m), unmapped)], n1) ∧ n1 < # 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) ] ∧ n1 < # wlar[vtblpnum1, wl-entry(m0, erasing)][n1, wl-entry(m1, used)] ∧ wlar[vtblpnum1, wl-entry(m0, erasing)][n1, wl-entry(m1, used)][n1].status = used ∧ 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) ] [n1 ] .vidhdr .vol = VTBL_VOLID ∧ 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) ] [n1 ] .vidhdr .leb = VTBL_LNUM ∧ is-encoded (to-vtbl(vols[v, fill(mkebatbl(m), unmapped)]), 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) ] [n1 ] .data)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

Proof step 79:
# apebs0 = # wlar, LEB_SIZE = n3 + align↑(datasize(buf, LEB_SIZE), EB_PAGE_SIZE), apebs0[n1] = mkpeb(aehdr, empty, mkempbuf(LEB_SIZE), 0, false), wlar[n1] = wl-entry(m1, free), wlar[vtblpnum1] = wl-entry(m0, used), aehdr.valid?, n1 < # wlar, vtblpnum1 < # wlar, bflipset-cons(bflipset, wlar), is-aligned(LEB_SIZE, EB_PAGE_SIZE), is-encoded(to-vtbl(vols)[v, m], subarray(buf, 0, LEB_SIZE)), ubi-io-inv (apebs0 [n1, mkpeb(aehdr, avidhdr(VTBL_VOLID, VTBL_LNUM, sqnum, datasize(buf, LEB_SIZE), checksum(buf, datasize(buf, LEB_SIZE))), mkempbuf(LEB_SIZE), 0, false) ]), ubi-io-inv(apebs0), ubi-io-inv (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) ]), unique-sqns(apebs0), valid-ebatbl(apebs0, wlar, vols, vtblpnum1), valid-eraseq(q + eq-entry(vtblpnum1, VTBL_VOLID × VTBL_LNUM) '), 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, LEB_SIZE), EB_PAGE_SIZE) ≤ # buf, LEB_SIZE ≤ # buf ⊦ vtblpnum1 = n1, 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[vtblpnum1, wl-entry(m0, erasing)][n1, wl-entry(m1, used)], vols[v, fill(mkebatbl(m), unmapped)], n1), v ∈ vols, VTBL_VOLID ∈ vols, vtblpnum1 ∈ q, ∃ buf0. buf = mkempbuf(LEB_SIZE) + buf0

Rule argument

Additional information

Used simplifier rules: ⊦ is-encoded(vtbl0, buf) → (is-encoded(vtbl1, buf) ↔ vtbl0 = vtbl1); (s)% ⊦ mkpeb(aehdr, avhdr, buf, m, boolvar).data = buf; (s)% ⊦ # mkebatbl(n) = n; (s)% ⊦ # fill(ebatbl, ebae) = # ebatbl; (s)% ⊦ to-vtbl(vols[v, ebatbl]) = to-vtbl(vols)[v, # ebatbl]; (s)% ⊦ avidhdr(v, m, m0, m1, m2).leb = m; (s)% ⊦ avidhdr(v, m, m0, m1, m2).vol = v; (s)% ⊦ mkpeb(aehdr, avhdr, buf, m, boolvar).vidhdr = avhdr; (s)% ⊦ m < # apebs → apebs[m, apeb][m] = apeb; (s)% ⊦ wl-entry(m, stat).status = stat; (s)%m < # wlar ⊦ wlar[m, wle][m] = wle; (s)% ⊦ m < n → (n ≤ m ↔ false); (s)% ⊦ m < n ↔ ¬ n ≤ m; (ss)% ⊦ # wlar[n, wle] = # wlar; (s)% ⊦ # apebs[n, apeb] = # apebs; (s)