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

# 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[vtblpnum1] = wl-entry(m0, used), wlar[n1] = wl-entry(m1, free), apebs0[n1] = mkpeb(aehdr, empty, mkempbuf(LEB_SIZE), 0, false), aehdr = aechdr(m2), aehdr.valid?, vtblpnum1 < # wlar, n1 < # wlar, valid-sqns(VTBL_VOLID, VTBL_LNUM, apebs0).max < sqnum, bflipset-cons(bflipset -- 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, 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-eraseq(q + eq-entry(vtblpnum1, VTBL_VOLID × VTBL_LNUM) '), valid-global-sqn(apebs0, sqnum), valid-peb (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-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, 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[vtblpnum1, wl-entry(m0, erasing)][n1, wl-entry(m1, used)]), vtblpnum1 ∈ q, VTBL_VOLID ∈ vols, ∃ buf0. buf = mkempbuf(n0) + buf0, m2 = m1 ∧ ( m < # wlar ∧ m ≠ n1 ∧ wlar[vtblpnum1, wl-entry(m0, erasing)][m].status = used → apebs0[m].vidhdr.vol ≠ VTBL_VOLID ∨ apebs0[m].vidhdr.leb ≠ VTBL_LNUM)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

Proof step 101:
# apebs0 = # wlar, apebs0[m].vidhdr.leb = VTBL_LNUM, wlar[vtblpnum1, wl-entry(m0, erasing)][m].status = used, apebs0[m].vidhdr.vol = VTBL_VOLID, 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[vtblpnum1] = wl-entry(m0, used), wlar[n1] = wl-entry(m1, free), apebs0[n1] = mkpeb(aechdr(m2), empty, mkempbuf(LEB_SIZE), 0, false), m < # wlar, vtblpnum1 < # wlar, n1 < # wlar, valid-sqns(VTBL_VOLID, VTBL_LNUM, apebs0).max < sqnum, bflipset-cons(bflipset -- vtblpnum1, wlar), bflipset-cons(bflipset, wlar), is-aligned(n0, EB_PAGE_SIZE), ubi-io-inv (apebs0 [n1, mkpeb (aechdr(m2), 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(aechdr(m2), 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-eraseq(q + eq-entry(vtblpnum1, VTBL_VOLID × VTBL_LNUM) '), valid-global-sqn(apebs0, sqnum), valid-peb (mkpeb (aechdr(m2), 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-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 ⊦ m = n1, vtblpnum1 = n1, valid-wl (apebs0 [n1, mkpeb (aechdr(m2), 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[vtblpnum1, wl-entry(m0, erasing)][n1, wl-entry(m1, used)]), vtblpnum1 ∈ q, VTBL_VOLID ∈ vols, ∃ buf0. buf = mkempbuf(n0) + buf0

Rule argument

Additional information

Used simplifier rules: ubi-io-inv-fwd: n < # apebs ⊦ apebs[n] = apeb ∧ ubi-io-inv(apebs) → ubi-io-peb-inv(apeb);% ⊦ ubi-io-peb-inv(mkpeb(aehdr, empty, mkempbuf(LEB_SIZE), 0, false)); (s)%lf-01: ⊦ m < n ∧ n = n0 → m < n0; (forward) from specification nat-basic%n < # wlar ⊦ valid-wl(apebs, wlar) ∧ wlar[n] = wl-entry(m0, free) ∧ apebs[n] = mkpeb(aechdr(m1), avhdr, buf, m2, boolvar) → (m0 = m1 ↔ true); (ss)% ⊦ m < n → (n ≤ m ↔ false); (s)% ⊦ m < n ↔ ¬ n ≤ m; (ss)% ⊦ aechdr(m).valid?; (s)