proof.v 5.99 KB
 Ralf Jung committed Oct 19, 2017 1 ``````From iris.program_logic Require Export weakestpre. `````` Robbert Krebbers committed May 28, 2019 2 ``````From iris.base_logic Require Import invariants lib.saved_prop. `````` Ralf Jung committed Oct 19, 2017 3 4 ``````From iris.heap_lang Require Export lang. From iris.heap_lang Require Import proofmode. `````` Robbert Krebbers committed May 28, 2019 5 ``````From iris.algebra Require Import auth gset. `````` Ralf Jung committed Oct 19, 2017 6 ``````From iris_examples.barrier Require Export barrier. `````` Ralf Jung committed Oct 19, 2017 7 8 9 10 ``````Set Default Proof Using "Type". (** The CMRAs/functors we need. *) Class barrierG Σ := BarrierG { `````` Robbert Krebbers committed May 28, 2019 11 `````` barrier_inG :> inG Σ (authR (gset_disjUR gname)); `````` Jacques-Henri Jourdan committed Feb 22, 2018 12 `````` barrier_savedPropG :> savedPropG Σ; `````` Ralf Jung committed Oct 19, 2017 13 ``````}. `````` Robbert Krebbers committed May 28, 2019 14 15 ``````Definition barrierΣ : gFunctors := #[ GFunctor (authRF (gset_disjUR gname)); savedPropΣ ]. `````` Ralf Jung committed Oct 19, 2017 16 17 18 19 20 21 22 23 `````` Instance subG_barrierΣ {Σ} : subG barrierΣ Σ → barrierG Σ. Proof. solve_inG. Qed. (** Now we come to the Iris part of the proof. *) Section proof. Context `{!heapG Σ, !barrierG Σ} (N : namespace). `````` Robbert Krebbers committed May 28, 2019 24 25 26 27 28 29 ``````Definition barrier_inv (l : loc) (γ : gname) (P : iProp Σ) : iProp Σ := (∃ (b : bool) (γsps : gset gname), l ↦ #b ∗ own γ (● (GSet γsps)) ∗ ((if b then True else P) -∗ ([∗ set] γsp ∈ γsps, ∃ R, saved_prop_own γsp R ∗ ▷ R)))%I. `````` Ralf Jung committed Oct 19, 2017 30 31 `````` Definition recv (l : loc) (R : iProp Σ) : iProp Σ := `````` Robbert Krebbers committed May 28, 2019 32 33 34 35 36 `````` (∃ γ P R' γsp, inv N (barrier_inv l γ P) ∗ ▷ (R' -∗ R) ∗ own γ (◯ GSet {[ γsp ]}) ∗ saved_prop_own γsp R')%I. `````` Ralf Jung committed Oct 19, 2017 37 `````` `````` Robbert Krebbers committed May 28, 2019 38 39 ``````Definition send (l : loc) (P : iProp Σ) : iProp Σ := (∃ γ, inv N (barrier_inv l γ P))%I. `````` Ralf Jung committed Oct 19, 2017 40 41 `````` (** Setoids *) `````` Robbert Krebbers committed May 28, 2019 42 ``````Instance barrier_inv_ne l γ : NonExpansive (barrier_inv l γ). `````` Jacques-Henri Jourdan committed Feb 22, 2018 43 ``````Proof. solve_proper. Qed. `````` Ralf Jung committed Oct 19, 2017 44 45 46 47 48 49 50 51 52 ``````Global Instance send_ne l : NonExpansive (send l). Proof. solve_proper. Qed. Global Instance recv_ne l : NonExpansive (recv l). Proof. solve_proper. Qed. (** Actual proofs *) Lemma newbarrier_spec (P : iProp Σ) : {{{ True }}} newbarrier #() {{{ l, RET #l; recv l P ∗ send l P }}}. Proof. `````` Robbert Krebbers committed May 28, 2019 53 `````` iIntros (Φ) "_ HΦ". iApply wp_fupd. wp_lam. wp_alloc l as "Hl". `````` Ralf Jung committed Oct 19, 2017 54 `````` iApply ("HΦ" with "[> -]"). `````` Robbert Krebbers committed May 28, 2019 55 56 57 58 59 60 61 62 63 `````` iMod (saved_prop_alloc P) as (γsp) "#Hsp". iMod (own_alloc (● GSet {[ γsp ]} ⋅ ◯ GSet {[ γsp ]})) as (γ) "[H● H◯]". { by apply auth_both_valid. } iMod (inv_alloc N _ (barrier_inv l γ P) with "[Hl H●]") as "#Hinv". { iExists false, {[ γsp ]}. iIntros "{\$Hl \$H●} !> HP". rewrite big_sepS_singleton; eauto. } iModIntro; iSplitL "H◯". - iExists γ, P, P, γsp. iFrame; auto. - by iExists γ. `````` Ralf Jung committed Oct 19, 2017 64 65 66 67 68 ``````Qed. Lemma signal_spec l P : {{{ send l P ∗ P }}} signal #l {{{ RET #(); True }}}. Proof. `````` Robbert Krebbers committed May 28, 2019 69 70 71 72 73 74 75 `````` iIntros (Φ) "[Hs HP] HΦ". iDestruct "Hs" as (γ) "#Hinv". wp_lam. iInv N as ([] γsps) "(>Hl & H● & HRs)". { wp_store. iModIntro. iSplitR "HΦ"; last by iApply "HΦ". iExists true, γsps. iFrame. } wp_store. iDestruct ("HRs" with "HP") as "HRs". iModIntro. iSplitR "HΦ"; last by iApply "HΦ". iExists true, γsps. iFrame; eauto. `````` Ralf Jung committed Oct 19, 2017 76 77 78 79 80 81 ``````Qed. Lemma wait_spec l P: {{{ recv l P }}} wait #l {{{ RET #(); P }}}. Proof. rename P into R. `````` Robbert Krebbers committed May 28, 2019 82 `````` iIntros (Φ) "HR HΦ". iDestruct "HR" as (γ P R' γsp) "(#Hinv & HR & H◯ & #Hsp)". `````` Ralf Jung committed Oct 19, 2017 83 `````` iLöb as "IH". wp_rec. wp_bind (! _)%E. `````` Robbert Krebbers committed May 28, 2019 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 `````` iInv N as ([] γsps) "(>Hl & >H● & HRs)"; last first. { wp_load. iModIntro. iSplitL "Hl H● HRs". { iExists false, γsps. iFrame. } by wp_apply ("IH" with "[\$] [\$]"). } iSpecialize ("HRs" with "[//]"). wp_load. iDestruct (own_valid_2 with "H● H◯") as %[Hvalid%gset_disj_included%elem_of_subseteq_singleton _]%auth_both_valid. iDestruct (big_sepS_delete with "HRs") as "[HR'' HRs]"; first done. iDestruct "HR''" as (R'') "[#Hsp' HR'']". iDestruct (saved_prop_agree with "Hsp Hsp'") as "#Heq". iMod (own_update_2 with "H● H◯") as "H●". { apply (auth_update_dealloc _ _ (GSet (γsps ∖ {[ γsp ]}))). apply gset_disj_dealloc_local_update. } iIntros "!>". iSplitL "Hl H● HRs". { iDestruct (bi.later_intro with "HRs") as "HRs". iModIntro. iExists true, (γsps ∖ {[ γsp ]}). iFrame; eauto. } wp_if. iApply "HΦ". iApply "HR". by iRewrite "Heq". `````` Ralf Jung committed Oct 19, 2017 101 102 103 104 105 106 ``````Qed. Lemma recv_split E l P1 P2 : ↑N ⊆ E → recv l (P1 ∗ P2) ={E}=∗ recv l P1 ∗ recv l P2. Proof. rename P1 into R1; rename P2 into R2. `````` Robbert Krebbers committed May 28, 2019 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 `````` iIntros (?). iDestruct 1 as (γ P R' γsp) "(#Hinv & HR & H◯ & #Hsp)". iInv N as (b γsps) "(>Hl & >H● & HRs)". iDestruct (own_valid_2 with "H● H◯") as %[Hvalid%gset_disj_included%elem_of_subseteq_singleton _]%auth_both_valid. iMod (own_update_2 with "H● H◯") as "H●". { apply (auth_update_dealloc _ _ (GSet (γsps ∖ {[ γsp ]}))). apply gset_disj_dealloc_local_update. } set (γsps' := γsps ∖ {[γsp]}). iMod (saved_prop_alloc_cofinite γsps' R1) as (γsp1 Hγsp1) "#Hsp1". iMod (saved_prop_alloc_cofinite (γsps' ∪ {[ γsp1 ]}) R2) as (γsp2 [? ?%not_elem_of_singleton]%not_elem_of_union) "#Hsp2". iMod (own_update _ _ (● _ ⋅ (◯ GSet {[ γsp1 ]} ⋅ ◯ (GSet {[ γsp2 ]}))) with "H●") as "(H● & H◯1 & H◯2)". { rewrite -auth_frag_op gset_disj_union; last set_solver. apply auth_update_alloc, (gset_disj_alloc_empty_local_update _ {[ γsp1; γsp2 ]}). set_solver. } iModIntro. iSplitL "HR Hl HRs H●". { iModIntro. iExists b, ({[γsp1; γsp2]} ∪ γsps'). iIntros "{\$Hl \$H●} HP". iSpecialize ("HRs" with "HP"). iDestruct (big_sepS_delete with "HRs") as "[HR'' HRs]"; first done. iDestruct "HR''" as (R'') "[#Hsp' HR'']". iDestruct (saved_prop_agree with "Hsp Hsp'") as "#Heq". iAssert (▷ R')%I with "[HR'']" as "HR'"; [iNext; by iRewrite "Heq"|]. iDestruct ("HR" with "HR'") as "[HR1 HR2]". iApply big_sepS_union; [set_solver|iFrame "HRs"]. iApply big_sepS_union; [set_solver|]. iSplitL "HR1"; rewrite big_sepS_singleton; eauto. } iModIntro; iSplitL "H◯1". - iExists γ, P, R1, γsp1. iFrame; auto. - iExists γ, P, R2, γsp2. iFrame; auto. `````` Ralf Jung committed Oct 19, 2017 137 138 139 140 ``````Qed. Lemma recv_weaken l P1 P2 : (P1 -∗ P2) -∗ recv l P1 -∗ recv l P2. Proof. `````` Robbert Krebbers committed May 28, 2019 141 142 `````` iIntros "HP". iDestruct 1 as (γ P R' i) "(#Hinv & HR & H◯)". iExists γ, P, R', i. iIntros "{\$Hinv \$H◯} !> HQ". iApply "HP". by iApply "HR". `````` Ralf Jung committed Oct 19, 2017 143 144 145 146 147 148 ``````Qed. Lemma recv_mono l P1 P2 : (P1 ⊢ P2) → recv l P1 ⊢ recv l P2. Proof. iIntros (HP) "H". iApply (recv_weaken with "[] H"). iApply HP. Qed. End proof. `````` Robbert Krebbers committed May 28, 2019 149 ``Typeclasses Opaque send recv.``