This is a listing of all goals defined over the current specification. Axioms are yellow, proof obligations purple and theorems green. Click on individual names to get more information on the proof.
| Name: | Sequent: | Type: |
|---|---|---|
| rely | ⊦ rely(me, O1, H1, O2, H2) ↔ (∀ r. (O1(r) = me ↔ O2(r) = me) ∧ (O1(r) = me → (r ∈ H1 ↔ r ∈ H2) ∧ (r ∈ H1 → H1[r] = H2[r]))) | An Axiom |
| owned | ⊦ !(id, O, P)(H) ↔ P(H) ∧ (∀ r. r ∈ H → O(r) = id) | An Axiom |
| guar | ⊦ guar(me, O1, H1, O2, H2) ↔ (∀ id. id ≠ me → rely(id, O1, H1, O2, H2)) | An Axiom |
| sep | ⊦ (R0 * R1)(H0, H1) ↔ (∃ H2, H3, H4, H5. H2 ⊥ H3 ∧ H4 ⊥ H5 ∧ H2 ∪ H3 = H0 ∧ H4 ∪ H5 = H1 ∧ R0(H2, H4) ∧ R1(H3, H5)) | An Axiom |
| new | ⊦ (↑ P)(H0, H1) ↔ P(H1) | An Axiom |
| old | ⊦ (↓ P)(H0, H1) ↔ P(H0) | An Axiom |
| alloc | ⊦ r ≠ null ∧ ¬ r ∈ H1 ∧ rely(me, O1(r ; me), H1 ++ r, O2, H2) → ((P0 * true)(H1) ↔ (!(me, O2, r =>_) * P0 * true)(H1 ++ r)) | A User Theorem |
| alloc-p | ⊦ r ≠ null ∧ ¬ r ∈ H1 ∧ rely(me, O1(r ; me), H1 ++ r, O2, H2) → ((!(me, O1, P) * P0)(H1) ↔ (!(me, O2, r =>_ * P) * P0)(H1 ++ r)) | A User Theorem |
| compact-local | ⊦ !(me, O, P0) * !(me, O, P1) = !(me, O, P0 * P1) | A User Theorem |
| ex-shift-o | ⊦ (!(me, O, _∃ oP) * P)(H) ↔ (∃ o. (!(me, O, oP(o)) * P)(H)) | A User Theorem |
| ex-shift-o-p | ⊦ (!(me, O, _∃ oP * P0) * P)(H) ↔ (∃ o. (!(me, O, oP(o) * P0) * P)(H)) | A User Theorem |
| guar-refl | ⊦ guar(me, O, H, O, H) | A User Theorem |
| guar-rely | ⊦ guar(id, O1, H1, O2, H2) ∧ id ≠ me → (¬ rely(me, O1, H1, O2, H2) ↔ false) | A User Theorem |
| lift-map | ⊦ r => o = !(me, O(r ; me), r => o) | A User Theorem |
| lift-mapex | ⊦ r =>_ = !(me, O(r ; me), r =>_) | A User Theorem |
| merge-new | ⊦ ↑ P0 * ↑ P1 = ↑ (P0 * P1) | A User Theorem |
| owned-P | ⊦ !(me, O, P)(H) ∧ ¬ P(H) → false | A User Theorem |
| owned-emp | ⊦ !(me, O, emp) = emp | A User Theorem |
| owned-r | ⊦ !(me, O, P)(H) ∧ O(r) ≠ me → ¬ r ∈ H | A User Theorem |
| prop-new | ⊦ ↓ (⌜bv⌝ ) = ↑ (⌜bv⌝ ) | A User Theorem |
| propagate | ⊦ id ≠ me ∧ rely(me, O1, H1, O2, H2) ∧ (!(me, O2, P) * P0)(H1) → ((!(id, O2, P1) * true)(H2) ↔ (!(me, O2, P) * !(id, O2, P1) * true)(H2)) | A User Theorem |
| rely-refl | ⊦ rely(me, O, H, O, H) | A User Theorem |
| rely-trans | ⊦ rely(me, O0, H0, O1, H1) ∧ rely(me, O1, H1, O2, H2) → rely(me, O0, H0, O2, H2) | A User Theorem |
| split-old | ⊦ ↓ (P0 * P1) = ↓ P0 * ↓ P1 | A User Theorem |
| split-union | ⊦ R0(H0, H1) ∧ R1(H2, H3) ∧ H0 ⊥ H2 ∧ H1 ⊥ H3 → (¬ (R0 * R1)(H0 ∪ H2, H1 ∪ H3) ↔ false) | A User Theorem |
| switch-ownership | ⊦ rely(me, O1, H1, O2, H2) → !(me, O1, P) = !(me, O2, P) | A User Theorem |
| to-new | ⊦ (↓ P)(H, H) ↔ (↑ P)(H, H) | A User Theorem |
| true-new | ⊦ ↓ true = ↑ true | A User Theorem |
| write-known | ⊦ rely(me, O1, H1[r, o1], O2, H2) → ((!(me, O2, r => o0) * P0)(H1) ↔ (!(me, O2, r => o1) * P0)(H1[r, o1]) ∧ H1[r] = o0 ∧ r ∈ H1) | A User Theorem |
| write-known-p | ⊦ rely(me, O1, H1[r, o1], O2, H2) → ((!(me, O2, r => o0 * P) * P0)(H1) ↔ (!(me, O2, r => o1 * P) * P0)(H1[r, o1]) ∧ H1[r] = o0 ∧ r ∈ H1) | A User Theorem |
| write-unknown | ⊦ rely(me, O1, H1[r, o1], O2, H2) → ((!(me, O2, r =>_) * P0)(H1) ↔ (!(me, O2, r => o1) * P0)(H1[r, o1]) ∧ r ∈ H1) | A User Theorem |
| write-unknown-p | ⊦ rely(me, O1, H1[r, o1], O2, H2) → ((!(me, O2, r =>_ * P) * P0)(H1) ↔ (!(me, O2, r => o1 * P) * P0)(H1[r, o1]) ∧ r ∈ H1) | A User Theorem |