proof.v 5.99 KB
Newer Older
Ralf Jung's avatar
Ralf Jung committed
1
From iris.program_logic Require Export weakestpre.
2
From iris.base_logic Require Import invariants lib.saved_prop.
Ralf Jung's avatar
Ralf Jung committed
3 4
From iris.heap_lang Require Export lang.
From iris.heap_lang Require Import proofmode.
5
From iris.algebra Require Import auth gset.
Ralf Jung's avatar
Ralf Jung committed
6
From iris_examples.barrier Require Export barrier.
Ralf Jung's avatar
Ralf Jung committed
7 8 9 10
Set Default Proof Using "Type".

(** The CMRAs/functors we need. *)
Class barrierG Σ := BarrierG {
11
  barrier_inG :> inG Σ (authR (gset_disjUR gname));
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
12
  barrier_savedPropG :> savedPropG Σ;
Ralf Jung's avatar
Ralf Jung committed
13
}.
14 15
Definition barrierΣ : gFunctors :=
  #[ GFunctor (authRF (gset_disjUR gname)); savedPropΣ ].
Ralf Jung's avatar
Ralf Jung committed
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).

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's avatar
Ralf Jung committed
30 31

Definition recv (l : loc) (R : iProp Σ) : iProp Σ :=
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's avatar
Ralf Jung committed
37

38 39
Definition send (l : loc) (P : iProp Σ) : iProp Σ :=
  ( γ, inv N (barrier_inv l γ P))%I.
Ralf Jung's avatar
Ralf Jung committed
40 41

(** Setoids *)
42
Instance barrier_inv_ne l γ : NonExpansive (barrier_inv l γ).
Jacques-Henri Jourdan's avatar
Jacques-Henri Jourdan committed
43
Proof. solve_proper. Qed.
Ralf Jung's avatar
Ralf Jung committed
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.
53
  iIntros (Φ) "_ HΦ". iApply wp_fupd. wp_lam. wp_alloc l as "Hl".
Ralf Jung's avatar
Ralf Jung committed
54
  iApply ("HΦ" with "[> -]").
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's avatar
Ralf Jung committed
64 65 66 67 68
Qed.

Lemma signal_spec l P :
  {{{ send l P  P }}} signal #l {{{ RET #(); True }}}.
Proof.
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's avatar
Ralf Jung committed
76 77 78 79 80 81
Qed.

Lemma wait_spec l P:
  {{{ recv l P }}} wait #l {{{ RET #(); P }}}.
Proof.
  rename P into R.
82
  iIntros (Φ) "HR HΦ". iDestruct "HR" as (γ P R' γsp) "(#Hinv & HR & H◯ & #Hsp)".
Ralf Jung's avatar
Ralf Jung committed
83
  iLöb as "IH". wp_rec. wp_bind (! _)%E.
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's avatar
Ralf Jung committed
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.
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's avatar
Ralf Jung committed
137 138 139 140
Qed.

Lemma recv_weaken l P1 P2 : (P1 - P2) - recv l P1 - recv l P2.
Proof.
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's avatar
Ralf Jung committed
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.

149
Typeclasses Opaque send recv.