Commit 06c27d87 by Dan Frumin

### Get rid of the unnecessary oneShot algebra in the `or` proofs

parent 6c8c4c60
 ... ... @@ -87,23 +87,22 @@ Section rules. iApply binary_fundamental_masked; eauto with typeable. Qed. Definition shootInv `{oneshotG Σ} x γ : iProp Σ := (x ↦ᵢ #0 ∗ pending γ ∨ x ↦ᵢ #1 ∗ shot γ)%I. Definition or_inv x : iProp Σ := (x ↦ᵢ #0 ∨ x ↦ᵢ #1)%I. Definition orN := nroot .@ "orN". Ltac close_shoot := iNext; (iLeft + iRight); by iFrame. Lemma assign_safe `{oneshotG Σ} x γ : inv shootN (shootInv x γ) Lemma assign_safe x : inv orN (or_inv x) ⊢ ▷ WP #x <- #1 {{ _, True }}. Proof. iIntros "#Hinv". iNext. iInv shootN as ">[[Hx Ht] | [Hx Ht]]" "Hcl"; wp_store. + iMod (shoot with "Ht") as "Ht". iMod ("Hcl" with "[-]"); first close_shoot; eauto. + iMod ("Hcl" with "[-]"); first close_shoot; eauto. iNext. iInv orN as ">[Hx | Hx]" "Hcl"; wp_store; (iMod ("Hcl" with "[-]"); first close_shoot); eauto. Qed. Lemma bin_log_or_commute `{oneshotG Σ} Δ Γ E (v1 v1' v2 v2' : val) : ↑shootN ⊆ E → Lemma bin_log_or_commute Δ Γ E (v1 v1' v2 v2' : val) : ↑orN ⊆ E → ↑logrelN ⊆ E → {E,E;Δ;Γ} ⊨ v1 ≤log≤ v1' : TArrow TUnit TUnit -∗ {E,E;Δ;Γ} ⊨ v2 ≤log≤ v2' : TArrow TUnit TUnit -∗ ... ... @@ -115,16 +114,13 @@ Section rules. rel_alloc_r as y "Hy". repeat rel_let_l. repeat rel_let_r. rel_fork_r as j "Hj". rel_seq_r. iApply fupd_logrel. iMod new_pending as (γ) "Ht". iModIntro. iMod (inv_alloc shootN _ (shootInv x γ) with "[Hx Ht]") as "#Hinv". iMod (inv_alloc orN _ (or_inv x) with "[Hx]") as "#Hinv". { close_shoot. } rel_fork_l. iModIntro. iSplitR; [ by iApply assign_safe | ]. rel_seq_l. rel_load_l_atomic. iInv shootN as ">[[Hx Ht] | [Hx Ht]]" "Hcl"; iInv orN as ">[Hx|Hx]" "Hcl"; iExists _; iFrame; iModIntro; iNext; iIntros "Hx"; rel_op_l; rel_if_l. + apply bin_log_related_spec_ctx. ... ... @@ -163,8 +159,8 @@ Section rules. unlock. eauto. (* TODO :( *) Qed. Lemma bin_log_or_idem_l `{oneshotG Σ} Δ Γ E (v v' : val) : ↑shootN ⊆ E → Lemma bin_log_or_idem_l Δ Γ E (v v' : val) : ↑orN ⊆ E → ↑logrelN ⊆ E → {E,E;Δ;Γ} ⊨ v ≤log≤ v' : TArrow TUnit TUnit -∗ {E,E;Δ;Γ} ⊨ or v v ≤log≤ v' #() : TUnit. ... ... @@ -173,16 +169,13 @@ Section rules. unlock or. repeat rel_rec_l. rel_alloc_l as x "Hx". repeat rel_let_l. iApply fupd_logrel. iMod new_pending as (γ) "Ht". iModIntro. iMod (inv_alloc shootN _ (shootInv x γ)%I with "[Hx Ht]") as "#Hinv". iMod (inv_alloc orN _ (or_inv x)%I with "[Hx]") as "#Hinv". { close_shoot. } rel_fork_l. iModIntro. iSplitR; [ by iApply assign_safe | ]. rel_seq_l. rel_load_l_atomic. iInv shootN as ">[[Hx Ht] | [Hx Ht]]" "Hcl"; iInv orN as ">[Hx|Hx]" "Hcl"; iExists _; iFrame; iModIntro; iNext; iIntros "Hx"; rel_op_l; rel_if_l. + iMod ("Hcl" with "[-Hlog]"); first close_shoot. ... ... @@ -193,8 +186,8 @@ Section rules. iApply bin_log_related_unit. Qed. Lemma bin_log_or_bot_l `{oneshotG Σ} Δ Γ E (v v' : val) : ↑shootN ⊆ E → Lemma bin_log_or_bot_l Δ Γ E (v v' : val) : ↑orN ⊆ E → ↑logrelN ⊆ E → {E,E;Δ;Γ} ⊨ v ≤log≤ v' : TArrow TUnit TUnit -∗ {E,E;Δ;Γ} ⊨ or v bot ≤log≤ v' #() : TUnit. ... ... @@ -203,16 +196,13 @@ Section rules. unlock or. repeat rel_rec_l. rel_alloc_l as x "Hx". repeat rel_let_l. iApply fupd_logrel. iMod new_pending as (γ) "Ht". iModIntro. iMod (inv_alloc shootN _ (shootInv x γ)%I with "[Hx Ht]") as "#Hinv". iMod (inv_alloc orN _ (or_inv x)%I with "[Hx]") as "#Hinv". { close_shoot. } rel_fork_l. iModIntro. iSplitR; [ by iApply assign_safe | ]. rel_seq_l. rel_load_l_atomic. iInv shootN as ">[[Hx Ht] | [Hx Ht]]" "Hcl"; iInv orN as ">[Hx|Hx]" "Hcl"; iExists _; iFrame; iModIntro; iNext; iIntros "Hx"; rel_op_l; rel_if_l. + iMod ("Hcl" with "[-Hlog]"); first close_shoot. ... ...
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!