This is a listing of all goals defined over the current specification. Axioms are marked yellow, proved theorems green and unproved theorems blue. Click on individual names to get more information on the proof.
| Name: | Sequent: | Type: |
|---|---|---|
| valid-vtbl | ⊦ valid-vtbl(apebs, vols, wlar, n0) ↔ n0 < # apebs ∧ n0 < # wlar ∧ wlar[n0].status = used ∧ apebs[n0].vidhdr.vol = VTBL_VOLID ∧ apebs[n0].vidhdr.leb = VTBL_LNUM ∧ is-encoded(to-vtbl(vols), apebs[n0].data) | An Axiom |
| valid-ebatbl | ⊦ valid-ebatbl(apebs, wlar, vols, n0) ↔ (∀ v, m, n. vols[v][m] = ⌜n⌝ ∧ v ∈ vols ∧ m < # vols[v] ↔ wlar[n].status = used ∧ n < # apebs ∧ n < # wlar ∧ apebs[n].vidhdr.valid? ∧ apebs[n].vidhdr.vol = v ∧ apebs[n].vidhdr.leb = m ∧ n ≠ n0) | An Axiom |
| valid-eraseqp-rec | ⊦ valid-eraseq(apebs, eqent ' + q) ↔ eqent.pnum < # apebs ∧ (valid-peb(apebs[eqent.pnum]) → eqent.lebref = apebs[eqent.pnum].vidhdr.vol × apebs[eqent.pnum].vidhdr.leb) ∧ valid-eraseq(apebs, q) | An Axiom |
| valid-eraseqp-base | ⊦ valid-eraseq(apebs, []) | An Axiom |
| valid-eraseqw | ⊦ valid-eraseq(wlar, q) ↔ (∀ n. n ∈ q ↔ n < # wlar ∧ wlar[n].status = erasing) | An Axiom |
| valid-wl | ⊦ valid-wl(apebs, wlar) ↔ (∀ n. n < # wlar → (wlar[n].status = erroneous ↔ apebs[n].bad) ∧ (wlar[n].status = free → apebs[n].vidhdr = empty) ∧ (wlar[n].status ≠ erroneous ∧ wlar[n].status ≠ erasing → apebs[n].echdr = aechdr(wlar[n].ec)) ∧ (wlar[n].status = used → (∃ v, m. valid-peb(v, m, apebs[n]) ∧ apebs[n].vidhdr.sqn = valid-sqns(v, m, apebs).max))) | An Axiom |
| ubi-cons | ⊦ ubi-cons(apebs, vols, wlar, q, bflipset, n0, n1) ↔ # apebs = # wlar ∧ unique-sqns(apebs) ∧ valid-global-sqn(apebs, n1) ∧ valid-wl(apebs, wlar) ∧ valid-eraseq(q) ∧ valid-eraseq(wlar, q) ∧ valid-eraseq(apebs, q) ∧ ¬ VTBL_VOLID ∈ vols ∧ bflipset-cons(bflipset, wlar) ∧ valid-ebatbl(apebs, wlar, vols, n0) ∧ valid-vtbl(apebs, vols, wlar, n0) | An Axiom |
| valid-eraseqd-rec | ⊦ valid-eraseq(eqent ' + q) ↔ ¬ eqent.pnum ∈ q ∧ valid-eraseq(q) | An Axiom |
| valid-eraseqd-base | ⊦ valid-eraseq([]) | An Axiom |
| write-once-inv | ⊦ write-once-inv(apebs, vols, wlar, q, bflipset, n0, n1, v, m, n2, n3, buf, err) ↔ ubi-cons(apebs, vols, wlar, q, bflipset, n0, n1) ∧ v ∈ vols ∧ m < # vols[v] ∧ (err = ESUCCESS ∨ ⌊err⌋ ) ∧ (err ≠ ESUCCESS → vols[v][m] = unmapped) ∧ n3 ≤ # buf ∧ is-aligned(n2, EB_PAGE_SIZE) ∧ is-aligned(n3, EB_PAGE_SIZE) ∧ n2 + n3 ≤ LEB_SIZE | An Axiom |
| unique-sqns | ⊦ unique-sqns(apebs) ↔ (∀ v, m. unique-elems(valid-sqns(v, m, apebs))) | An Axiom |
| valid-global-sqn | ⊦ valid-global-sqn(apebs, n) ↔ (∀ v, m. valid-sqns(v, m, apebs) ≠ ∅ → n > valid-sqns(v, m, apebs).max) | An Axiom |
| erase-worker-inv | ⊦ erase-worker-inv(apebs0, wlar0, m, err, apebs, vols, wlar, q0, eqent, q1, bflipset, n0, n1) ↔ m ≤ UBI_ERASE_RETRIES + 1 ∧ eqent.pnum < # apebs ∧ id○(apebs, apebs0, eqent.pnum) ∧ id○(wlar, wlar0, eqent.pnum) ∧ ubi-cons(apebs, vols, wlar, q0 + (eqent + q1), bflipset, n0, n1) ∧ ubi-io-inv(apebs) ∧ (err = ESUCCESS → apebs[eqent.pnum].echdr = aechdr(wlar[eqent.pnum].ec) ∧ apebs[eqent.pnum].vidhdr = empty ∧ ¬ apebs[eqent.pnum].bad) | An Axiom |
| wl-threshold-nonzero | ⊦ WL_THRESHOLD = 0 ↔ false | An Axiom |
| bflipset-cons | ⊦ bflipset-cons(bflipset, wlar) ↔ (∀ n. n ∈ bflipset → n < # wlar ∧ wlar[n].status = used) | An Axiom |
| mapped-pebs | ⊦ n ∈ mapped-pebs(vols) ↔ (∃ v, m. v ∈ vols ∧ m < # vols[v] ∧ vols[v][m] = ⌜n⌝ ) | An Axiom |
| id-set | ⊦ id(apebs0, apebs1, ns) ↔ # apebs0 = # apebs1 ∧ (∀ n. n ∈ ns ∧ n < # apebs0 ∧ n < # apebs1 → apebs0[n] = apebs1[n]) | An Axiom |
| bflipset-subarray-add | n < # wlar ⊦ bflipset-cons(bflipset, subarray(wlar, 0, n)) → bflipset-cons(bflipset ++ n, subarray(wlar[n, wl-entry(m0, used)], 0, n + 1)) | A User Theorem |
| bflipset-subarray-erase-old | n < # wlar ⊦ bflipset-cons(bflipset, subarray(wlar, 0, n)) ∧ n0 < n → bflipset-cons(bflipset -- n0, subarray(wlar[n, wl-entry(m0, used)][n0, wl-entry(m1, erasing)], 0, n + 1)) | A User Theorem |
| bflipset-subarray-erase-old-add | n < # wlar ⊦ bflipset-cons(bflipset, subarray(wlar, 0, n)) ∧ n0 < n → bflipset-cons((bflipset ++ n) -- n0, subarray(wlar[n, wl-entry(m0, used)][n0, wl-entry(m1, erasing)], 0, n + 1)) | A User Theorem |
| bflipset-subarray-next | n < # wlar ⊦ bflipset-cons(bflipset, subarray(wlar, 0, n)) → bflipset-cons(bflipset, subarray(wlar[n, wle], 0, n + 1)) | A User Theorem |
| bitflip-cons-add | ⊦ bflipset-cons(bflipset, wlar) → (bflipset-cons(bflipset ++ n, wlar) ↔ n < # wlar ∧ wlar[n].status = used) | A User Theorem |
| bitflip-cons-del | ⊦ bflipset-cons(bflipset, wlar) → bflipset-cons(bflipset -- n, wlar) | A User Theorem |
| bitflip-cons-set | wle.status ≠ used ⊦ bflipset-cons(bflipset, wlar[m, wle]) ↔ bflipset-cons(bflipset, wlar) ∧ ¬ m ∈ bflipset | A User Theorem |
| bitflip-cons-set-used | ⊦ bflipset-cons(bflipset, wlar) → bflipset-cons(bflipset, wlar[m, wl-entry(n, used)]) | A User Theorem |
| bitflips-cons-empty | ⊦ bflipset-cons(∅, wlar) | A User Theorem |
| bitflips-cons-in | stat ≠ used ⊦ wlar[n] = wl-entry(m, stat) ∧ bflipset-cons(bflipset, wlar) → ¬ n ∈ bflipset | A User Theorem |
| datasize-alignup | ⊦ n ≤ # buf ∧ is-aligned(n, EB_PAGE_SIZE) → datasize(buf, align↑(datasize(buf, n), EB_PAGE_SIZE)) = datasize(buf, n) | A User Theorem |
| idset-idexpt | ⊦ id○(apebs1, apebs2, n) ∧ ¬ n ∈ ns → (id(apebs1, apebs0, ns) ↔ id(apebs2, apebs0, ns)) | A User Theorem |
| idset-idexpt-fwd | ⊦ id(apebs2, apebs1, ns) ∧ id○(apebs1, apebs0, n) → id(apebs2, apebs0, ns -- n) | A User Theorem |
| idset-mapped-pebs-write-unused | n < # wlar, stat ≠ used ⊦ wlar[n] = wl-entry(m, stat) ∧ id○(apebs, apebs0, n) ∧ valid-ebatbl(apebs, wlar, vols, n0) → id(apebs, apebs0, mapped-pebs(vols)) | A User Theorem |
| idset-refl | ⊦ id(apebs, apebs, ns) | A User Theorem |
| idset-trans-intersect | ⊦ id(apebs2, apebs1, ns0) ∧ id(apebs1, apebs0, ns1) → id(apebs2, apebs0, ns0 ∩ ns1) | A User Theorem |
| idset-weaken | ⊦ id(apebs1, apebs0, ns) → id(apebs1, apebs0, ns -- n) | A User Theorem |
| idset-write-notin | ¬ n ∈ ns ⊦ id(apebs1[n, apeb], apebs0, ns) ↔ id(apebs1, apebs0, ns) | A User Theorem |
| in-valid-eraseqp-valid-lref | ⊦ eq-entry(n, lref) ∈ q ∧ valid-eraseq(apebs, q) ∧ valid-peb(v, m, apebs[n]) → lref = v × m | A User Theorem |
| is-vtbl-pnum | n < # apebs, n < # wlar ⊦ apebs[n] = mkpeb(aehdr, avhdr, buf, m, boolvar) ∧ wlar[n] = wl-entry(m0, used) ∧ valid-wl(apebs, wlar) ∧ avhdr.vol = VTBL_VOLID ∧ avhdr.leb = VTBL_LNUM ∧ valid-ebatbl(apebs, wlar, vols, n0) ∧ ¬ VTBL_VOLID ∈ vols → n = n0 | A User Theorem |
| ls-at-subarray-pebs | n0 ≤ # apebs, n1 < n0 ⊦ subarray(apebs, 0, n0)[n1] = apebs[n1] | A User Theorem |
| ls-at-subarray-wlar | n0 ≤ # wlar, n1 < n0 ⊦ subarray(wlar, 0, n0)[n1] = wlar[n1] | A User Theorem |
| mapped-pebs-add-empty-vol | ⊦ ¬ v ∈ vols → mapped-pebs(vols[v, fill(mkebatbl(n), unmapped)]) = mapped-pebs(vols) | A User Theorem |
| mapped-pebs-at | ⊦ v ∈ vols ∧ m < # vols[v] ∧ vols[v][m] = ⌜n⌝ → n ∈ mapped-pebs(vols) | A User Theorem |
| mapped-pebs-rem-notmapped | stat ≠ used ⊦ wlar[n] = wl-entry(m0, stat) ∧ valid-ebatbl(apebs, wlar, vols, m1) → mapped-pebs(vols) -- n = mapped-pebs(vols) | A User Theorem |
| mapped-pebs-remap | ⊦ v ∈ vols ∧ m < # vols[v] ∧ vols[v][m] = ⌜n0⌝ ∧ valid-ebatbl(apebs, wlar, vols, m0) → mapped-pebs(vols[v, vols[v][m, ⌜n1⌝ ]]) = (mapped-pebs(vols) -- n0) ++ n1 | A User Theorem |
| mapped-pebs-unmap | ⊦ v ∈ vols ∧ m < # vols[v] ∧ vols[v][m] = ⌜n0⌝ ∧ valid-ebatbl(apebs, wlar, vols, m0) → mapped-pebs(vols[v, vols[v][m, unmapped]]) = mapped-pebs(vols) -- n0 | A User Theorem |
| mapped-pebs-unused | n < # wlar, stat ≠ used ⊦ wlar[n] = wl-entry(m, stat) ∧ valid-ebatbl(apebs, wlar, vols, n0) → ¬ n ∈ mapped-pebs(vols) | A User Theorem |
| unique-sqns-2-valid-pebs | ⊦ m0 < # apebs ∧ m1 < # apebs ∧ valid-peb(v, m, apebs[m0]) ∧ valid-peb(v, m, apebs[m1]) ∧ unique-sqns(apebs) ∧ m0 ≠ m1 → apebs[m0].vidhdr.sqn ≠ apebs[m1].vidhdr.sqn | A User Theorem |
| unique-sqns-update | m < # apebs ⊦ unique-sqns(apebs) → ( unique-sqns(apebs[m, apeb]) ↔ ¬ valid-peb(apeb) ∨ ¬ apeb.vidhdr.sqn ∈ valid-sqns(apeb.vidhdr.vol, apeb.vidhdr.leb, apebs) \ (valid-peb(apeb.vidhdr.vol, apeb.vidhdr.leb, apebs[m]) ⊃ {apebs[m].vidhdr.sqn} ;∅)) | A User Theorem |
| unique-sqns-write-valid | m < # apebs ⊦ apebs[m] = mkpeb(aehdr, avhdr, buf0, m0, boolvar0) ∧ valid-peb(mkpeb(aehdr, avhdr, buf0, m0, boolvar0)) ∧ valid-peb(mkpeb(aehdr, avhdr, buf1, m1, boolvar1)) → (unique-sqns(apebs[m, mkpeb(aehdr, avhdr, buf1, m1, boolvar1)]) ↔ unique-sqns(apebs)) | A User Theorem |
| valid-ebatbl-add-unmapped-vol | ⊦ ¬ v ∈ vols ∧ valid-ebatbl(apebs, wlar, vols, n0) ∧ wlar[n1] = wl-entry(m2, free) → valid-ebatbl(apebs[n1, apeb], wlar[n1, wl-entry(m1, used)][n0, wl-entry(m0, erasing)], vols[v, fill(mkebatbl(n), unmapped)], n1) | A User Theorem |
| valid-ebatbl-map | n < # wlar, n < # apebs ⊦ v ∈ vols ∧ m < # vols[v] ∧ vols[v][m] = unmapped ∧ n ≠ n0 ∧ apebs[n].vidhdr.valid? ∧ apebs[n].vidhdr.vol = v ∧ apebs[n].vidhdr.leb = m ∧ wlar[n].status ≠ used → (valid-ebatbl(apebs, wlar[n, wl-entry(m0, used)], vols[v, vols[v][m, ⌜n⌝ ]], n0) ↔ valid-ebatbl(apebs, wlar, vols, n0)) | A User Theorem |
| valid-ebatbl-move-vtbl | ⊦ wlar[n1] = wl-entry(m1, free) ∧ valid-ebatbl(apebs, wlar, vols, n0) → valid-ebatbl(apebs[n1, apeb], wlar[n1, wle][n0, wl-entry(m0, erasing)], vols, n1) | A User Theorem |
| valid-ebatbl-remap | n < # wlar, n < # apebs ⊦ v ∈ vols ∧ m < # vols[v] ∧ vols[v][m] = ⌜n1⌝ ∧ n ≠ n0 ∧ n1 ≠ n0 ∧ apebs[n].vidhdr.valid? ∧ apebs[n].vidhdr.vol = v ∧ apebs[n].vidhdr.leb = m ∧ wlar[n].status ≠ used ∧ valid-ebatbl(apebs, wlar, vols, n0) → valid-ebatbl(apebs, wlar[n, wl-entry(m0, used)][n1, wl-entry(m1, erasing)], vols[v, vols[v][m, ⌜n⌝ ]], n0) | A User Theorem |
| valid-ebatbl-unmap | ⊦ v ∈ vols ∧ m < # vols[v] ∧ vols[v][m] = ⌜n⌝ ∧ valid-ebatbl(apebs, wlar, vols, n0) → valid-ebatbl(apebs, wlar[n, wl-entry(m0, erasing)], vols[v, vols[v][m, unmapped]], n0) | A User Theorem |
| valid-ebatbl-update-vhdrs-unused | stat ≠ used ⊦ wlar[m] = wl-entry(m0, stat) → (valid-ebatbl(apebs[m, apeb], wlar, vols, n) ↔ valid-ebatbl(apebs, wlar, vols, n)) | A User Theorem |
| valid-ebatbl-update-wlar-unused | stat ≠ used, stat0 ≠ used ⊦ wlar[m] = wl-entry(m0, stat) → (valid-ebatbl(apebs, wlar[m, wl-entry(m1, stat0)], vols, n) ↔ valid-ebatbl(apebs, wlar, vols, n)) | A User Theorem |
| valid-ebatbl-write-data | ⊦ apebs[n] = mkpeb(aehdr, avhdr, buf0, m0, boolvar) → (valid-ebatbl(apebs[n, mkpeb(aehdr, avhdr, buf1, m1, boolvar)], wlar, vols, n0) ↔ valid-ebatbl(apebs, wlar, vols, n0)) | A User Theorem |
| valid-eraseq-array-0 | ⊦ valid-eraseq(mkwlarray(0), []) | A User Theorem |
| valid-eraseq-next-erasing | m < # wlar ⊦ valid-eraseq(subarray(wlar, 0, m), q) → valid-eraseq(subarray(wlar[m, wl-entry(m0, erasing)], 0, m + 1), q + eq-entry(m, lref) ') | A User Theorem |
| valid-eraseq-prev-erasing | m < # wlar ⊦ m1 < m ∧ valid-eraseq(subarray(wlar, 0, m), q) → valid-eraseq(subarray(wlar[m, wl-entry(m0, used)][m1, wl-entry(m2, erasing)], 0, m + 1), q + eq-entry(m1, lref) ') | A User Theorem |
| valid-eraseqd-append | ⊦ valid-eraseq(q + eqent ') ↔ ¬ eqent.pnum ∈ q ∧ valid-eraseq(q) | A User Theorem |
| valid-eraseqd-nodups-middle0 | ⊦ valid-eraseq(q0 + eq-entry(m, lref) ' + q1) → ¬ m ∈ q0 | A User Theorem |
| valid-eraseqd-nodups-middle1 | ⊦ valid-eraseq(q0 + eq-entry(m, lref) ' + q1) → ¬ m ∈ q1 | A User Theorem |
| valid-eraseqd-nodups-middle2 | ⊦ valid-eraseq(q0 + eq-entry(m, lref) ' + q1) → ¬ m ∈ q0 + q1 | A User Theorem |
| valid-eraseqd-nodups0 | ⊦ valid-eraseq(q0 + q1) ∧ m ∈ q0 → ¬ m ∈ q1 | A User Theorem |
| valid-eraseqd-nodups1 | ⊦ valid-eraseq(q0 + q1) ∧ m ∈ q1 → ¬ m ∈ q0 | A User Theorem |
| valid-eraseqd-one | ⊦ valid-eraseq(eqent ') | A User Theorem |
| valid-eraseqd-rem-middle | ⊦ valid-eraseq(q0 + eqent ' + q1) → valid-eraseq(q0 + q1) | A User Theorem |
| valid-eraseqp-append | ⊦ valid-eraseq(apebs, q) → (valid-eraseq(apebs, q + eq-entry(n, lref) ') ↔ n < # apebs ∧ (valid-peb(apebs[n]) → lref = apebs[n].vidhdr.vol × apebs[n].vidhdr.leb)) | A User Theorem |
| valid-eraseqp-in | ⊦ n ∈ q ∧ valid-eraseq(wlar, q) ∧ wlar[n] = wl-entry(m, stat) → wlar[n] = wl-entry(m, erasing) | A User Theorem |
| valid-eraseqp-in0 | ⊦ valid-eraseq(wlar, q0 + eq-entry(n, lref) ' + q1) → wlar[n].status = erasing | A User Theorem |
| valid-eraseqp-invalidate | m < # apebs ⊦ ¬ valid-peb(apeb) ∧ valid-eraseq(apebs, q) → valid-eraseq(apebs[m, apeb], q) | A User Theorem |
| valid-eraseqp-one | ⊦ valid-eraseq(apebs, eq-entry(n, lref) ') ↔ n < # apebs ∧ (valid-peb(apebs[n]) → lref = apebs[n].vidhdr.vol × apebs[n].vidhdr.leb) | A User Theorem |
| valid-eraseqp-rem-middle | ⊦ valid-eraseq(apebs, q0 + eqent ' + q1) → valid-eraseq(apebs, q0 + q1) | A User Theorem |
| valid-eraseqp-update-other | ⊦ ¬ m ∈ q → (valid-eraseq(apebs[m, apeb], q) ↔ valid-eraseq(apebs, q)) | A User Theorem |
| valid-eraseqp-valid-lebref | ⊦ n ∈ q ∧ valid-peb(v, m, apebs[n]) ∧ valid-eraseq(apebs, q) → eq-entry(n, v × m) ∈ q | A User Theorem |
| valid-eraseqw-free | stat ≠ erasing ⊦ valid-eraseq(wlar, q0 + eq-entry(m, lref) ' + q1) → (valid-eraseq(wlar[m, wl-entry(m0, stat)], q0 + q1) ↔ ¬ m ∈ q0 ∧ ¬ m ∈ q1) | A User Theorem |
| valid-eraseqw-free-in | n < # wlar ⊦ valid-eraseq(wlar, q) ∧ wlar[n] = wl-entry(m, free) → ¬ n ∈ q | A User Theorem |
| valid-eraseqw-size-left | ⊦ valid-eraseq(wlar, eq-entry(m, lref) ' + q1) → ¬ # wlar ≤ m | A User Theorem |
| valid-eraseqw-size-middle | ⊦ valid-eraseq(wlar, q0 + eq-entry(m, lref) ' + q1) → ¬ # wlar ≤ m | A User Theorem |
| valid-eraseqw-subarray-shift | n < # wlar, stat ≠ erasing ⊦ valid-eraseq(subarray(wlar, 0, n), q) → valid-eraseq(subarray(wlar[n, wl-entry(m, stat)], 0, n + 1), q) | A User Theorem |
| valid-eraseqw-unmap | stat ≠ erasing ⊦ n < # wlar ∧ wlar[n] = wl-entry(m0, stat) ∧ valid-eraseq(wlar, q) → valid-eraseq(wlar[n, wl-entry(m1, erasing)], q + eq-entry(n, lref) ') | A User Theorem |
| valid-eraseqw-update-ec | ⊦ wlar[m] = wl-entry(m0, stat) → (valid-eraseq(wlar[m, wl-entry(m1, stat)], q) ↔ valid-eraseq(wlar, q)) | A User Theorem |
| valid-eraseqw-use | stat ≠ erasing ⊦ wlar[n] = wl-entry(m0, stat) → (valid-eraseq(wlar[n, wl-entry(m1, used)], q) ↔ valid-eraseq(wlar, q)) | A User Theorem |
| valid-global-sqn-add-valid | m < # apebs ⊦ valid-peb(apeb) ∧ valid-global-sqn(apebs, n) ∧ apeb.vidhdr.sqn < n → valid-global-sqn(apebs[m, apeb], n) | A User Theorem |
| valid-global-sqn-array-0 | ⊦ valid-global-sqn(mkapebs(0), 0) | A User Theorem |
| valid-global-sqn-inc | ⊦ valid-global-sqn(apebs, n) → valid-global-sqn(apebs, n + m) | A User Theorem |
| valid-global-sqn-invalidate | m < # apebs ⊦ ¬ valid-peb(apeb) ∧ valid-global-sqn(apebs, n) → valid-global-sqn(apebs[m, apeb], n) | A User Theorem |
| valid-global-sqn-next | m < # apebs ⊦ valid-global-sqn(subarray(apebs, 0, m), n) → (valid-global-sqn(subarray(apebs, 0, m + 1), n) ↔ ¬ valid-peb(apebs[m]) ∨ apebs[m].vidhdr.sqn < n) | A User Theorem |
| valid-global-sqn-next-max | m < # apebs ⊦ valid-global-sqn(subarray(apebs, 0, m), n) ∧ valid-peb(apebs[m]) ∧ apebs[m] = mkpeb(aehdr, avidhdr(v, m0, m1, m2, m4), buf, m3, false) → valid-global-sqn(subarray(apebs, 0, m + 1), max(n, m1 + 1)) | A User Theorem |
| valid-global-sqn-not-leq | ⊦ valid-sqns(v, m, apebs) ≠ ∅ ∧ valid-global-sqn(apebs, n) → ¬ n ≤ valid-sqns(v, m, apebs).max | A User Theorem |
| valid-global-sqn-not-ls | ⊦ valid-sqns(v, m, apebs) ≠ ∅ ∧ valid-global-sqn(apebs, n) → ¬ n < valid-sqns(v, m, apebs).max | A User Theorem |
| valid-global-sqn-notin | ⊦ valid-global-sqn(apebs, n) → ¬ n ∈ valid-sqns(v, m, apebs) | A User Theorem |
| valid-global-sqn-write-valid | m < # apebs ⊦ apebs[m] = mkpeb(aehdr, avhdr, buf0, m0, boolvar0) ∧ valid-peb(mkpeb(aehdr, avhdr, buf0, m0, boolvar0)) ∧ valid-peb(mkpeb(aehdr, avhdr, buf1, m1, boolvar1)) → (valid-global-sqn(apebs[m, mkpeb(aehdr, avhdr, buf1, m1, boolvar1)], n) ↔ valid-global-sqn(apebs, n)) | A User Theorem |
| valid-vtbl-buf | ⊦ apebs[n0] = mkpeb(aehdr, avhdr, buf, m, boolvar) ∧ valid-vtbl(apebs, vols, wlar, n0) → is-encoded(to-vtbl(vols), buf) | A User Theorem |
| valid-vtbl-in-wlar | ⊦ valid-vtbl(apebs, vols, wlar, n0) → n0 < # wlar | A User Theorem |
| valid-vtbl-sqns-notempty | ⊦ valid-vtbl(apebs, vols, wlar, n0) ∧ valid-wl(apebs, wlar) → valid-sqns(VTBL_VOLID, VTBL_LNUM, apebs) ≠ ∅ | A User Theorem |
| valid-vtbl-update-other-pebs | ⊦ m ≠ n0 → (valid-vtbl(apebs[m, apeb], vols, wlar, n0) ↔ valid-vtbl(apebs, vols, wlar, n0)) | A User Theorem |
| valid-vtbl-update-other-wlar | ⊦ m ≠ n0 → (valid-vtbl(apebs, vols, wlar[m, wle], n0) ↔ valid-vtbl(apebs, vols, wlar, n0)) | A User Theorem |
| valid-vtbl-update-vols | ⊦ v ∈ vols → (valid-vtbl(apebs, vols[v, vols[v][m, ebae]], wlar, n0) ↔ valid-vtbl(apebs, vols, wlar, n0)) | A User Theorem |
| valid-vtbl-wlar-status | ⊦ wlar[n0] = wl-entry(m, stat) ∧ valid-vtbl(apebs, vols, wlar, n0) → stat = used | A User Theorem |
| valid-wl-array-0 | ⊦ valid-wl(mkapebs(0), mkwlarray(0)) | A User Theorem |
| valid-wl-ebatbl-used-imp-mapped | n < # wlar, # wlar = # apebs ⊦ wlar[n].status = used ∧ valid-ebatbl(apebs, wlar, vols, n0) ∧ valid-wl(apebs, wlar) ∧ n0 ≠ n → apebs[n].vidhdr.vol ∈ vols ∧ apebs[n].vidhdr.leb < # vols[apebs[n].vidhdr.vol] ∧ vols[apebs[n].vidhdr.vol][apebs[n].vidhdr.leb] = ⌜n⌝ | A User Theorem |
| valid-wl-ebatbl-used-imp-valid-ehdr | ⊦ v ∈ vols ∧ m < # vols[v] ∧ vols[v][m] = ⌜n⌝ ∧ valid-ebatbl(apebs, wlar, vols, n0) ∧ valid-wl(apebs, wlar) ∧ apebs[n] = mkpeb(aehdr, avhdr, buf, m0, boolvar) → aehdr.valid? | A User Theorem |
| valid-wl-erase | stat ≠ erroneous ⊦ wlar[m] = wl-entry(m0, stat) ∧ valid-wl(apebs, wlar) → valid-wl(apebs, wlar[m, wl-entry(m1, erasing)]) | A User Theorem |
| valid-wl-erasing-invalidate | m < # apebs ⊦ # apebs = # wlar ∧ ¬ valid-peb(apeb) ∧ valid-wl(apebs, wlar) ∧ wlar[m] = wl-entry(m0, erasing) ∧ ¬ apeb.bad → valid-wl(apebs[m, apeb], wlar) | A User Theorem |
| valid-wl-erasing-invalidate0 | m < # apebs ⊦ # apebs = # wlar ∧ ¬ valid-peb(apeb) ∧ ¬ apeb.bad ∧ valid-wl(apebs, wlar) → valid-wl(apebs[m, apeb], wlar[m, wl-entry(m0, erasing)]) | A User Theorem |
| valid-wl-erasing-update-ec | m < # wlar ⊦ wlar[m] = wl-entry(m0, erasing) → (valid-wl(apebs, wlar[m, wl-entry(m1, erasing)]) ↔ valid-wl(apebs, wlar)) | A User Theorem |
| valid-wl-free | m < # wlar ⊦ valid-wl(apebs, wlar) → (valid-wl(apebs, wlar[m, wl-entry(m1, free)]) ↔ apebs[m].echdr = aechdr(m1) ∧ apebs[m].vidhdr = empty ∧ ¬ apebs[m].bad) | A User Theorem |
| valid-wl-free-echdr | n < # wlar ⊦ valid-wl(apebs, wlar) ∧ wlar[n] = wl-entry(m0, free) ∧ apebs[n] = mkpeb(aechdr(m1), avhdr, buf, m2, boolvar) → (m0 = m1 ↔ true) | A User Theorem |
| valid-wl-map | 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)]) | A User Theorem |
| valid-wl-markbad | m < # apebs ⊦ # apebs = # wlar ∧ valid-wl(apebs, wlar) → valid-wl(apebs[m, mkpeb(aehdr, avhdr, buf, m0, true)], wlar[m, wl-entry(m1, erroneous)]) | A User Theorem |
| valid-wl-next-bad | m < # apebs, # apebs = # wlar ⊦ valid-wl(subarray(apebs, 0, m), subarray(wlar, 0, m)) → (valid-wl(subarray(apebs, 0, m + 1), subarray(wlar[m, wl-entry(m0, erroneous)], 0, m + 1)) ↔ apebs[m].bad) | A User Theorem |
| valid-wl-next-free | m < # apebs, # apebs = # wlar ⊦ valid-wl(subarray(apebs, 0, m), subarray(wlar, 0, m)) ∧ apebs[m] = mkpeb(aechdr(m0), empty, buf, m1, false) → valid-wl(subarray(apebs, 0, m + 1), subarray(wlar[m, wl-entry(m0, free)], 0, m + 1)) | A User Theorem |
| valid-wl-next-invalid-erase | m < # apebs, # apebs = # wlar ⊦ valid-wl(subarray(apebs, 0, m), subarray(wlar, 0, m)) ∧ ¬ valid-peb(apebs[m]) → (valid-wl(subarray(apebs, 0, m + 1), subarray(wlar[m, wl-entry(m0, erasing)], 0, m + 1)) ↔ ¬ apebs[m].bad) | A User Theorem |
| valid-wl-next-valid-erase | m < # apebs, # apebs = # wlar ⊦ valid-wl(subarray(apebs, 0, m), subarray(wlar, 0, m)) ∧ valid-peb(v, n, apebs[m]) ∧ (valid-sqns(v, n, apebs, m) ≠ ∅ → apebs[m].vidhdr.sqn < valid-sqns(v, n, apebs, m).max) → valid-wl(subarray(apebs, 0, m + 1), subarray(wlar[m, wl-entry(m0, erasing)], 0, m + 1)) | A User Theorem |
| valid-wl-next-valid-update | m < # apebs, # apebs = # wlar, m0 < m ⊦ valid-wl(subarray(apebs, 0, m), subarray(wlar, 0, m)) ∧ valid-peb(v, n, apebs[m]) ∧ valid-peb(v, n, apebs[m0]) ∧ apebs[m0].vidhdr.sqn = valid-sqns(v, n, apebs, m).max ∧ apebs[m].vidhdr.sqn > apebs[m0].vidhdr.sqn ∧ unique-sqns(apebs) ∧ apebs[m].echdr.ec = m2 → valid-wl(subarray(apebs, 0, m + 1), subarray(wlar[m, wl-entry(m2, used)][m0, wl-entry(m1, erasing)], 0, m + 1)) | A User Theorem |
| valid-wl-next-valid-use | m < # apebs, # apebs = # wlar ⊦ valid-wl(subarray(apebs, 0, m), subarray(wlar, 0, m)) ∧ valid-peb(v, n, apebs[m]) ∧ valid-sqns(v, n, apebs, m) = ∅ → (valid-wl(subarray(apebs, 0, m + 1), subarray(wlar[m, wl-entry(m0, used)], 0, m + 1)) ↔ apebs[m].echdr.ec = m0) | A User Theorem |
| valid-wl-use | 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) ∧ (∀ m. m < # wlar ∧ m ≠ n ∧ wlar[m].status = used → apebs[m].vidhdr.vol ≠ apeb.vidhdr.vol ∨ apebs[m].vidhdr.leb ≠ apeb.vidhdr.leb) ∧ apeb.echdr.ec = m0 → valid-wl(apebs[n, apeb], wlar[n, wl-entry(m0, used)]) | A User Theorem |
| valid-wl-used-echdr | n < # wlar ⊦ valid-wl(apebs, wlar) ∧ wlar[n] = wl-entry(m0, used) ∧ apebs[n] = mkpeb(aehdr, avhdr, buf, m2, boolvar) → (aehdr.ec = m0 ↔ true) | A User Theorem |
| valid-wl-write-unmapped | n < # apebs, # apebs = # wlar ⊦ valid-wl(apebs, wlar) ∧ valid-peb(apeb) ∧ 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) ∧ wlar[n].status = erasing ∧ valid-vtbl(apebs, vols, wlar, n0) ∧ ¬ VTBL_VOLID ∈ vols → valid-wl(apebs[n, apeb], wlar) | A User Theorem |
| valid-wl-write-valid | m < # apebs, # apebs = # wlar ⊦ apebs[m] = mkpeb(aehdr, avhdr, buf0, m0, boolvar0) ∧ valid-peb(mkpeb(aehdr, avhdr, buf0, m0, boolvar0)) ∧ valid-peb(mkpeb(aehdr, avhdr, buf1, m1, boolvar1)) ∧ wlar[m] = wl-entry(m2, used) → (valid-wl(apebs[m, mkpeb(aehdr, avhdr, buf1, m1, boolvar1)], wlar) ↔ valid-wl(apebs, wlar)) | A User Theorem |