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: |
|---|---|---|
| vols-le | ⊦ vols0 ⊆ vols1 ↔ (∀ v. (v ∈ vols0 ↔ v ∈ vols1) ∧ (v ∈ vols0 → # vols0[v] = # vols1[v] ∧ (∀ m. m < # vols0[v] ∧ vols0[v][m] ≠ unmapped → vols0[v][m] = vols1[v][m]))) | An Axiom |
| valid-eraseq-strong-rec | ⊦ valid-eraseq-strong(apebs, vtbl, eqent ' + q) ↔ eqent.pnum < # apebs ∧ ¬ eqent.pnum ∈ q ∧ (∀ v, m. (valid-peb(v, m, apebs[eqent.pnum]) ↔ eqent.lebref = v × m) ∧ (eqent.lebref = v × m ∧ v ∈ vtbl ∧ m < vtbl[v] → apebs[eqent.pnum].vidhdr.sqn ≠ valid-sqns(v, m, apebs).max)) ∧ valid-eraseq-strong(apebs, vtbl, q) | An Axiom |
| valid-eraseq-strong-base | ⊦ valid-eraseq-strong(apebs, vtbl, []) | An Axiom |
| vols-is-max-weak | ⊦ is-max(apebs, vols, wlar, q, bflipset, n0, n1) ↔ ubi-cons(apebs, vols, wlar, q, bflipset, n0, n1) ∧ (∃ vtbl. is-encoded(vtbl, apebs[n0].data) ∧ valid-eraseq-strong(apebs, vtbl, q)) | An Axiom |
| valid-eraseq-stronger-rec | ⊦ valid-eraseq-stronger(apebs, eqent ' + q) ↔ eqent.pnum < # apebs ∧ ¬ eqent.pnum ∈ q ∧ (∀ v, m. (valid-peb(v, m, apebs[eqent.pnum]) ↔ eqent.lebref = v × m) ∧ (eqent.lebref = v × m → apebs[eqent.pnum].vidhdr.sqn ≠ valid-sqns(v, m, apebs).max)) ∧ valid-eraseq-stronger(apebs, q) | An Axiom |
| valid-eraseq-stronger-base | ⊦ valid-eraseq-stronger(apebs, []) | An Axiom |
| scan-all-inv | ⊦ scan-all-inv(n, apebs, recs, wlar, q, bflipset, nx, n1, err) ↔ ¬ ¬ ( n ≤ # apebs ∧ (err = ESUCCESS ∨ ⌊err⌋ ) ∧ ( err = ESUCCESS → ubi-io-inv(apebs) ∧ unique-sqns(apebs) ∧ # apebs = # wlar ∧ ¬ dups(nx) ∧ nx < n ∧ indices-erasing(wlar, nx) ∧ valid-global-sqn(subarray(apebs, 0, n), n1) ∧ valid-eraseq(subarray(wlar, 0, n), q) ∧ bflipset-cons(bflipset, subarray(wlar, 0, n)) ∧ valid-eraseq-stronger(subarray(apebs, 0, n), q) ∧ valid-wl(subarray(apebs, 0, n), subarray(wlar, 0, n)) ∧ valid-recs-sqns(apebs, recs) ∧ valid-recs(subarray(apebs, 0, n), subarray(wlar, 0, n), recs))) | An Axiom |
| unmapped-vols | ⊦ unmapped-vols(vols) ↔ (∀ v, m. v ∈ vols ∧ m < # vols[v] → vols[v][m] = unmapped) | An Axiom |
| valid-recs-sqns | ⊦ valid-recs-sqns(apebs, recs) ↔ (∀ ladr. ladr ∈ recs → recs[ladr].pnum < # apebs ∧ apebs[recs[ladr].pnum].vidhdr.sqn = recs[ladr].sqn) | An Axiom |
| valid-recs | ⊦ valid-recs(apebs, wlar, recs) ↔ (∀ ladr, m. ladr ∈ recs ∧ recs[ladr].pnum = m ↔ wlar[m].status = used ∧ m < # apebs ∧ apebs[m].vidhdr.vol = ladr.vol ∧ apebs[m].vidhdr.leb = ladr.leb) | An Axiom |
| valid-vtbl-weak | ⊦ valid-vtbl-weak(apebs, n) ↔ n < # apebs ∧ valid-peb(VTBL_VOLID, VTBL_LNUM, apebs[n]) ∧ apebs[n].vidhdr.sqn = valid-sqns(VTBL_VOLID, VTBL_LNUM, apebs).max ∧ (∃ vtbl. is-encoded(vtbl, apebs[n].data) ∧ ¬ VTBL_VOLID ∈ vtbl) | An Axiom |
| disj | ⊦ recs ⊥ vols ↔ (∀ v, m. ¬ v × m ∈ recs ∨ ¬ v ∈ vols ∨ ¬ m < # vols[v] ∨ vols[v][m] = unmapped) | An Axiom |
| vols-eraseq-bound | ⊦ vols1⌈vols0, q0⌉ ↔ (∀ v, m. v ∈ vols0 ∧ v ∈ vols1 ∧ m < # vols0[v] ∧ m < # vols1[v] ∧ vols0[v][m] = unmapped ∧ vols1[v][m] ≠ unmapped → eq-entry(vols1[v][m].pnum, v × m) ∈ q0) | An Axiom |
| indices-erasing-rec | ⊦ indices-erasing(wlar, n ' + nx) ↔ n < # wlar ∧ wlar[n].status = erasing ∧ indices-erasing(wlar, nx) | An Axiom |
| indices-erasing-base | ⊦ indices-erasing(wlar, []) | An Axiom |
| disj-remove | ⊦ v × m ∈ recs ∧ recs ⊥ vols → recs -- (v × m) ⊥ vols | A User Theorem |
| disj-shift | ⊦ v × m ∈ recs ∧ v ∈ vols ∧ recs ⊥ vols → recs -- (v × m) ⊥ vols[v, vols[v][m, ebae]] | A User Theorem |
| in-eraseq-strong-not-valid | ⊦ v ∈ vols ∧ m < # vols[v] ∧ valid-eraseq-strong(apebs, to-vtbl(vols), q) ∧ valid-peb(v, m, apebs[n]) ∧ apebs[n].vidhdr.sqn = valid-sqns(v, m, apebs).max → ¬ n ∈ q | A User Theorem |
| in-eraseq-strong-valid | ⊦ eq-entry(n, v × m) ∈ q ∧ valid-eraseq-strong(apebs, to-vtbl(vols), q) → valid-peb(v, m, apebs[n]) ∧ (v ∈ vols ∧ m < # vols[v] → apebs[n].vidhdr.sqn ≠ valid-sqns(v, m, apebs).max) | A User Theorem |
| indices-erasing-at | ⊦ n ∈ nx ∧ indices-erasing(wlar, nx) → wlar[n].status = erasing | A User Theorem |
| indices-erasing-eraseq | ⊦ indices-erasing(wlar0, nx) ∧ valid-eraseq(wlar0, q0) ∧ valid-eraseq(wlar1, q1) ∧ q0 ⊆ q1 → indices-erasing(wlar1, nx) | A User Theorem |
| indices-erasing-write-notin | ⊦ nx < m ∧ indices-erasing(wlar, nx) → indices-erasing(wlar[m, wle], nx) | A User Theorem |
| indices-erasing-write-prepend | m < # wlar ⊦ indices-erasing(wlar, nx) → (indices-erasing(wlar[m, wle], m ' + nx) ↔ wle.status = erasing) | A User Theorem |
| indices-set-erasing | ⊦ indices-erasing(wlar, nx) → indices-erasing(wlar[m, wl-entry(n, erasing)], nx) | A User Theorem |
| ubi-cons-same-vtbl | ⊦ ubi-cons(apebs, vols0, wlar0, q0, bflipset0, n0, n1) ∧ ubi-cons(apebs, vols1, wlar1, q1, bflipset1, m0, m1) → n0 = m0 | A User Theorem |
| ubi-io-initial-unique-sqns | ⊦ ubi-io-initial(apebs) → unique-sqns(apebs) | A User Theorem |
| ubi-io-initial-valid-sqns | ⊦ ubi-io-initial(apebs) → valid-sqns(v, m, apebs) = ∅ | A User Theorem |
| ubi-io-initial-valid-sqns-h | ⊦ n ≤ # apebs ∧ ubi-io-initial(apebs) → valid-sqns(v, m, apebs, n) = ∅ | A User Theorem |
| unmapped-vols-disj | ⊦ unmapped-vols(vols) → recs ⊥ vols | A User Theorem |
| unmapped-vols-unmapped | ⊦ v ∈ vols ∧ m < # vols[v] ∧ unmapped-vols(vols) → vols[v][m] ≠ ⌜n⌝ | A User Theorem |
| valid-eraseq-map-indices-nostatchange | ⊦ valid-eraseq(wlar, q) ∧ (∀ wle. f(wle).status = wle.status) ∧ valid-indices(wlar, nx) ∧ ¬ dups(nx) → valid-eraseq(wlar.mapIndices(nx, f), q) | A User Theorem |
| valid-eraseq-strong-imp-p | ⊦ valid-eraseq-strong(apebs, vtbl, q) → valid-eraseq(apebs, q) | A User Theorem |
| valid-eraseq-strong-imp-q | ⊦ valid-eraseq-strong(apebs, vtbl, q) → valid-eraseq(q) | A User Theorem |
| valid-eraseq-strong-notinvols | n < # apebs ⊦ (¬ v ∈ vtbl ∨ ¬ m < vtbl[v]) ∧ valid-eraseq-strong(apebs, vtbl, q) ∧ valid-peb(v, m, apebs[n]) ∧ ¬ n ∈ q → valid-eraseq-strong(apebs, vtbl, q + eq-entry(n, v × m) ') | A User Theorem |
| valid-eraseq-stronger-imp-strong | ⊦ valid-eraseq-stronger(apebs, q) → valid-eraseq-strong(apebs, vtbl, q) | A User Theorem |
| valid-eraseq-stronger-next | m < # apebs ⊦ valid-eraseq-stronger(subarray(apebs, 0, m), q) → valid-eraseq-stronger(subarray(apebs, 0, m + 1), q) | A User Theorem |
| valid-eraseq-stronger-next-append-lref | m < # apebs ⊦ valid-eraseq-stronger(subarray(apebs, 0, m), q) → ( valid-eraseq-stronger(subarray(apebs, 0, m + 1), q + eq-entry(m, v × n) ') ↔ valid-peb(v, n, apebs[m]) ∧ apebs[m].vidhdr.sqn ≠ valid-sqns(v, n, apebs, m + 1).max) | A User Theorem |
| valid-eraseq-stronger-next-append-none | m < # apebs ⊦ valid-eraseq-stronger(subarray(apebs, 0, m), q) → (valid-eraseq-stronger(subarray(apebs, 0, m + 1), q + eq-entry(m, none) ') ↔ ¬ valid-peb(apebs[m])) | A User Theorem |
| valid-eraseq-stronger-no-maxsqnum | ⊦ n < # apebs ∧ valid-peb(v, m, apebs[n]) ∧ apebs[n].vidhdr.sqn = valid-sqns(v, m, apebs).max ∧ valid-eraseq-stronger(apebs, q) → ¬ n ∈ q | A User Theorem |
| valid-eraseq-stronger-one | ⊦ valid-eraseq-stronger(apebs, eq-entry(m, lref) ') ↔ m < # apebs ∧ (lref = none → ¬ valid-peb(apebs[m])) ∧ (lref ≠ none → valid-peb(lref.vol, lref.leb, apebs[m]) ∧ apebs[m].vidhdr.sqn ≠ valid-sqns(lref.vol, lref.leb, apebs).max) | A User Theorem |
| valid-eraseq-stronger-prev-append-lref | m < # apebs, m0 < m ⊦ valid-eraseq-stronger(subarray(apebs, 0, m), q) ∧ valid-peb(v, n, apebs[m]) ∧ valid-sqns(v, n, apebs, m).max < apebs[m].vidhdr.sqn ∧ valid-peb(v, n, apebs[m0]) ∧ ¬ m0 ∈ q → valid-eraseq-stronger(subarray(apebs, 0, m + 1), q + eq-entry(m0, v × n) ') | A User Theorem |
| valid-recs-emptyset | ⊦ valid-recs(mkapebs(0), mkwlarray(0), ∅) | A User Theorem |
| valid-recs-in-nonempty-sqns | m < # apebs, # wlar = # apebs ⊦ valid-recs(subarray(apebs, 0, m), subarray(wlar, 0, m), recs) ∧ valid-wl(subarray(apebs, 0, m), subarray(wlar, 0, m)) ∧ v × n ∈ recs → valid-sqns(v, n, apebs, m) ≠ ∅ | A User Theorem |
| valid-recs-next-add | m < # apebs, # wlar = # apebs ⊦ valid-recs(subarray(apebs, 0, m), subarray(wlar, 0, m), recs) ∧ apebs[m] = mkpeb(aehdr, avidhdr(v, n, m0, m1, m4), buf, m2, boolvar) ∧ ¬ v × n ∈ recs → valid-recs(subarray(apebs, 0, m + 1), subarray(wlar[m, wl-entry(m3, used)], 0, m + 1), recs[v × n, recovery-entry(m, m0)]) | A User Theorem |
| valid-recs-next-samerecs | m < # apebs, # wlar = # apebs, stat ≠ used ⊦ valid-recs(subarray(apebs, 0, m), subarray(wlar, 0, m), recs) → valid-recs(subarray(apebs, 0, m + 1), subarray(wlar[m, wl-entry(m0, stat)], 0, m + 1), recs) | A User Theorem |
| valid-recs-next-update | m < # apebs, # wlar = # apebs ⊦ valid-recs(subarray(apebs, 0, m), subarray(wlar, 0, m), recs) ∧ apebs[m] = mkpeb(aehdr, avidhdr(v, n, m0, m1, m5), buf, m2, boolvar) ∧ v × n ∈ recs ∧ recs[v × n] = recovery-entry(m3, m4) → valid-recs (subarray(apebs, 0, m + 1), subarray(wlar[m, wl-entry(n0, used)][m3, wl-entry(n1, erasing)], 0, m + 1), recs[v × n, recovery-entry(m, m0)]) | A User Theorem |
| valid-recs-sqns-emptyset | ⊦ valid-recs-sqns(apebs, ∅) | A User Theorem |
| valid-recs-sqns-update | ⊦ valid-recs-sqns(apebs, recs) → (valid-recs-sqns(apebs, recs[v × m, recovery-entry(m0, m1)]) ↔ m0 < # apebs ∧ apebs[m0].vidhdr.sqn = m1) | A User Theorem |
| valid-vtbl-map-indices-erasing | ⊦ ¬ dups(nx) ∧ valid-indices(wlar, nx) ∧ valid-vtbl(apebs, vols, wlar, m) ∧ indices-erasing(wlar, nx) → valid-vtbl(apebs, vols, wlar.mapIndices(nx, f), m) | A User Theorem |
| valid-wl-map-indices | ⊦ valid-wl(apebs, wlar) ∧ valid-indices(wlar, nx) ∧ ¬ dups(nx) ∧ indices-erasing(wlar, nx) → valid-wl(apebs, wlar.mapIndices(nx, λ wle. wle.ec:= n)) | A User Theorem |
| vols-is-max-is-max-vols | ⊦ is-max(apebs, vols0, wlar0, q0, bflipset0, n0, n1) ∧ ubi-cons(apebs, vols1, wlar1, q1, bflipset1, m0, m1) → vols1 ⊆ vols0 | A User Theorem |
| vols-is-max-is-min-eraseq | ⊦ is-max(apebs, vols0, wlar0, q0, bflipset0, n0, n1) ∧ ubi-cons(apebs, vols1, wlar1, q1, bflipset, m0, m1) → q0.lebrefs ⊆ q1.lebrefs | A User Theorem |
| vols-le-antisym | ⊦ vols0 ⊆ vols1 ∧ vols1 ⊆ vols0 → vols0 = vols1 | A User Theorem |
| vols-le-refl | ⊦ ¬ vols0 ⊆ vols0 ↔ false | A User Theorem |
| vols-le-trans | ⊦ vols0 ⊆ vols1 ∧ vols1 ⊆ vols2 → vols0 ⊆ vols2 | A User Theorem |