Merge branch 'robbert/barrier_auth' into 'master'

Shorter barrier proof that uses auth instead of sts.

See merge request iris/examples!16

_CoqProject

@@ -9,7 +9,6 @@
 theories/barrier/proof.v
 theories/barrier/specification.v
 theories/barrier/barrier.v
-theories/barrier/protocol.v
 theories/barrier/example_client.v
 theories/barrier/example_joining_existentials.v
 

theories/barrier/proof.v

 From iris.program_logic Require Export weakestpre.
+From iris.base_logic Require Import invariants lib.saved_prop.
 From iris.heap_lang Require Export lang.
-From stdpp Require Import functions.
-From iris.base_logic Require Import lib.saved_prop lib.sts.
 From iris.heap_lang Require Import proofmode.
+From iris.algebra Require Import auth gset.
 From iris_examples.barrier Require Export barrier.
-From iris_examples.barrier Require Import protocol.
 Set Default Proof Using "Type".
 
 (** The CMRAs/functors we need. *)
 Class barrierG Σ := BarrierG {
-  barrier_stsG :> stsG Σ sts;
+  barrier_inG :> inG Σ (authR (gset_disjUR gname));
   barrier_savedPropG :> savedPropG Σ;
 }.
-Definition barrierΣ : gFunctors := #[stsΣ sts; savedPropΣ].
+Definition barrierΣ : gFunctors :=
+  #[ GFunctor (authRF (gset_disjUR gname)); savedPropΣ ].
 
 Instance subG_barrierΣ {Σ} : subG barrierΣ Σ → barrierG Σ.
 Proof. solve_inG. Qed.
@@ -20,181 +20,130 @@ Proof. solve_inG. Qed.
 (** Now we come to the Iris part of the proof. *)
 Section proof.
 Context `{!heapG Σ, !barrierG Σ} (N : namespace).
-Implicit Types I : gset gname.
 
-Definition ress (P : iProp Σ) (I : gset gname) : iProp Σ :=
-  (∃ Ψ : gname → iProp Σ,
-    ▷ (P -∗ [∗ set] i ∈ I, Ψ i) ∗ [∗ set] i ∈ I, saved_prop_own i (Ψ i))%I.
-
-Coercion state_to_val (s : state) : val :=
-  match s with State Low _ => #false | State High _ => #true end.
-Arguments state_to_val !_ / : simpl nomatch.
-
-Definition state_to_prop (s : state) (P : iProp Σ) : iProp Σ :=
-  match s with State Low _ => P | State High _ => True%I end.
-Arguments state_to_prop !_ _ / : simpl nomatch.
-
-Definition barrier_inv (l : loc) (P : iProp Σ) (s : state) : iProp Σ :=
-  (l ↦ s ∗ ress (state_to_prop s P) (state_I s))%I.
-
-Definition barrier_ctx (γ : gname) (l : loc) (P : iProp Σ) : iProp Σ :=
-  sts_ctx γ N (barrier_inv l P).
-
-Definition send (l : loc) (P : iProp Σ) : iProp Σ :=
-  (∃ γ, barrier_ctx γ l P ∗ sts_ownS γ low_states {[ Send ]})%I.
+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.
 
 Definition recv (l : loc) (R : iProp Σ) : iProp Σ :=
-  (∃ γ P Q i,
-    barrier_ctx γ l P ∗ sts_ownS γ (i_states i) {[ Change i ]} ∗
-    saved_prop_own i Q ∗ ▷ (Q -∗ R))%I.
+  (∃ γ P R' γsp,
+    inv N (barrier_inv l γ P) ∗
+    ▷ (R' -∗ R) ∗
+    own γ (◯ GSet {[ γsp ]}) ∗
+    saved_prop_own γsp R')%I.
 
-Global Instance barrier_ctx_persistent (γ : gname) (l : loc) (P : iProp Σ) :
-  Persistent (barrier_ctx γ l P).
-Proof. apply _. Qed.
+Definition send (l : loc) (P : iProp Σ) : iProp Σ :=
+  (∃ γ, inv N (barrier_inv l γ P))%I.
 
 (** Setoids *)
-Global Instance ress_ne n : Proper (dist n ==> (=) ==> dist n) ress.
-Proof. solve_proper. Qed.
-Global Instance state_to_prop_ne s :
-  NonExpansive (state_to_prop s).
-Proof. solve_proper. Qed.
-Global Instance barrier_inv_ne n l :
-  Proper (dist n ==> eq ==> dist n) (barrier_inv l).
-Proof. solve_proper. Qed.
-Global Instance barrier_ctx_ne γ l : NonExpansive (barrier_ctx γ l).
+Instance barrier_inv_ne l γ : NonExpansive (barrier_inv l γ).
 Proof. solve_proper. Qed.
 Global Instance send_ne l : NonExpansive (send l).
 Proof. solve_proper. Qed.
 Global Instance recv_ne l : NonExpansive (recv l).
 Proof. solve_proper. Qed.
 
-(** Helper lemmas *)
-Lemma ress_split i i1 i2 Q R1 R2 P I :
-  i ∈ I → i1 ∉ I → i2 ∉ I → i1 ≠ i2 →
-  saved_prop_own i Q -∗ saved_prop_own i1 R1 -∗ saved_prop_own i2 R2 -∗
-  (Q -∗ R1 ∗ R2) -∗ ress P I -∗
-  ress P ({[i1;i2]} ∪ I ∖ {[i]}).
-Proof.
-  iIntros (????) "#HQ #H1 #H2 HQR"; iDestruct 1 as (Ψ) "[HPΨ HΨ]".
-  iDestruct (big_opS_delete _ _ i with "HΨ") as "[#HΨi HΨ]"; first done.
-  iExists (<[i1:=R1]> (<[i2:=R2]> Ψ)). iSplitL "HQR HPΨ".
-  - iPoseProof (saved_prop_agree with "HQ HΨi") as "#Heq".
-    iNext. iRewrite "Heq" in "HQR". iIntros "HP". iSpecialize ("HPΨ" with "HP").
-    iDestruct (big_opS_delete _ _ i with "HPΨ") as "[HΨ HPΨ]"; first done.
-    iDestruct ("HQR" with "HΨ") as "[HR1 HR2]".
-    rewrite -assoc_L !big_opS_fn_insert'; [|abstract set_solver ..].
-    by iFrame.
-  - rewrite -assoc_L !big_opS_fn_insert; [|abstract set_solver ..]. eauto.
-Qed.
-
 (** Actual proofs *)
 Lemma newbarrier_spec (P : iProp Σ) :
   {{{ True }}} newbarrier #() {{{ l, RET #l; recv l P ∗ send l P }}}.
 Proof.
-  iIntros (Φ) "_ HΦ".
-  rewrite -wp_fupd /newbarrier /=. wp_lam. wp_alloc l as "Hl".
+  iIntros (Φ) "_ HΦ". iApply wp_fupd. wp_lam. wp_alloc l as "Hl".
   iApply ("HΦ" with "[> -]").
-  iMod (saved_prop_alloc P) as (γ) "#?".
-  iMod (sts_alloc (barrier_inv l P) _ N (State Low {[ γ ]}) with "[-]")
-    as (γ') "[#? Hγ']"; eauto.
-  { iNext. rewrite /barrier_inv /=. iFrame.
-    iExists (const P). rewrite !big_opS_singleton /=. eauto. }
-  iAssert (barrier_ctx γ' l P)%I as "#?".
-  { done. }
-  iAssert (sts_ownS γ' (i_states γ) {[Change γ]}
-    ∗ sts_ownS γ' low_states {[Send]})%I with "[> -]" as "[Hr Hs]".
-  { iApply sts_ownS_op; eauto using i_states_closed, low_states_closed.
-    - set_solver.
-    - iApply (sts_own_weaken with "Hγ'");
-        auto using sts.closed_op, i_states_closed, low_states_closed;
-        abstract set_solver. }
-  iModIntro. iSplitL "Hr".
-  - iExists γ', P, P, γ. iFrame. auto.
-  - rewrite /send. auto.
+  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 γ.
 Qed.
 
 Lemma signal_spec l P :
   {{{ send l P ∗ P }}} signal #l {{{ RET #(); True }}}.
 Proof.
-  rewrite /signal /=.
-  iIntros (Φ) "[Hs HP] HΦ". iDestruct "Hs" as (γ) "[#Hsts Hγ]". wp_lam.
-  iMod (sts_openS (barrier_inv l P) _ _ γ with "[Hγ]")
-    as ([p I]) "(% & [Hl Hr] & Hclose)"; eauto.
-  destruct p; [|done]. wp_store.
-  iSpecialize ("HΦ" with "[#]") => //. iFrame "HΦ".
-  iMod ("Hclose" $! (State High I) (∅ : propset token) with "[-]"); last done.
-  iSplit; [iPureIntro; by eauto using signal_step|].
-  rewrite /barrier_inv /ress /=. iNext. iFrame "Hl".
-  iDestruct "Hr" as (Ψ) "[Hr Hsp]"; iExists Ψ; iFrame "Hsp".
-  iNext. iIntros "_"; by iApply "Hr".
+  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.
 Qed.
 
 Lemma wait_spec l P:
   {{{ recv l P }}} wait #l {{{ RET #(); P }}}.
 Proof.
   rename P into R.
-  iIntros (Φ) "Hr HΦ"; iDestruct "Hr" as (γ P Q i) "(#Hsts & Hγ & #HQ & HQR)".
+  iIntros (Φ) "HR HΦ". iDestruct "HR" as (γ P R' γsp) "(#Hinv & HR & H◯ & #Hsp)".
   iLöb as "IH". wp_rec. wp_bind (! _)%E.
-  iMod (sts_openS (barrier_inv l P) _ _ γ with "[Hγ]")
-    as ([p I]) "(% & [Hl Hr] & Hclose)"; eauto.
-  wp_load. destruct p.
-  - iMod ("Hclose" $! (State Low I) {[ Change i ]} with "[Hl Hr]") as "Hγ".
-    { iSplit; first done. rewrite /barrier_inv /=. by iFrame. }
-    iAssert (sts_ownS γ (i_states i) {[Change i]})%I with "[> Hγ]" as "Hγ".
-    { iApply (sts_own_weaken with "Hγ"); eauto using i_states_closed. }
-    iModIntro. wp_if.
-    iApply ("IH" with "Hγ [HQR] [HΦ]"); auto.
-  - (* a High state: the comparison succeeds, and we perform a transition and
-    return to the client *)
-    iDestruct "Hr" as (Ψ) "[HΨ Hsp]".
-    iDestruct (big_opS_delete _ _ i with "Hsp") as "[#HΨi Hsp]"; first done.
-    iAssert (▷ (Ψ i ∗ [∗ set] j ∈ I ∖ {[i]}, Ψ j))%I with "[HΨ]" as "[HΨ HΨ']".
-    { iNext. iApply (big_opS_delete _ _ i); first done. by iApply "HΨ". }
-    iMod ("Hclose" $! (State High (I ∖ {[ i ]})) ∅ with "[HΨ' Hl Hsp]").
-    { iSplit; [iPureIntro; by eauto using wait_step|].
-      rewrite /barrier_inv /=. iNext. iFrame "Hl". iExists Ψ; iFrame. auto. }
-    iPoseProof (saved_prop_agree with "HQ HΨi") as "#Heq".
-    iModIntro. wp_if.
-    iApply "HΦ". iApply "HQR". by iRewrite "Heq".
+  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".
 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.
-  iIntros (?). iDestruct 1 as (γ P Q i) "(#Hsts & Hγ & #HQ & HQR)".
-  iMod (sts_openS (barrier_inv l P) _ _ γ with "[Hγ]")
-    as ([p I]) "(% & [Hl Hr] & Hclose)"; eauto.
-  iMod (saved_prop_alloc_cofinite I) as (i1) "[% #Hi1]".
-  iMod (saved_prop_alloc_cofinite (I ∪ {[i1]}))
-    as (i2) "[Hi2' #Hi2]"; iDestruct "Hi2'" as %Hi2.
-  rewrite ->not_elem_of_union, elem_of_singleton in Hi2; destruct Hi2.
-  iMod ("Hclose" $! (State p ({[i1; i2]} ∪ I ∖ {[i]}))
-                    {[Change i1; Change i2 ]} with "[-]") as "Hγ".
-  { iSplit; first by eauto using split_step.
-    rewrite /barrier_inv /=. iNext. iFrame "Hl".
-    by iApply (ress_split with "HQ Hi1 Hi2 HQR"). }
-  iAssert (sts_ownS γ (i_states i1) {[Change i1]}
-    ∗ sts_ownS γ (i_states i2) {[Change i2]})%I with "[> -]" as "[Hγ1 Hγ2]".
-  { iApply sts_ownS_op; eauto using i_states_closed, low_states_closed.
-    - abstract set_solver.
-    - iApply (sts_own_weaken with "Hγ");
-        eauto using sts.closed_op, i_states_closed.
-      abstract set_solver. }
-  iModIntro; iSplitL "Hγ1".
-  - iExists γ, P, R1, i1. iFrame; auto.
-  - iExists γ, P, R2, i2. iFrame; auto.
+  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.
 Qed.
 
 Lemma recv_weaken l P1 P2 : (P1 -∗ P2) -∗ recv l P1 -∗ recv l P2.
 Proof.
-  iIntros "HP". iDestruct 1 as (γ P Q i) "(#Hctx&Hγ&Hi&HP1)".
-  iExists γ, P, Q, i. iFrame "Hctx Hγ Hi".
-  iNext. iIntros "HQ". by iApply "HP"; iApply "HP1".
+  iIntros "HP". iDestruct 1 as (γ P R' i) "(#Hinv & HR & H◯)".
+  iExists γ, P, R', i. iIntros "{$Hinv $H◯} !> HQ". iApply "HP". by iApply "HR".
 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.
 
-Typeclasses Opaque barrier_ctx send recv.
+Typeclasses Opaque send recv.

theories/barrier/protocol.v

-From iris.algebra Require Export sts.
-From iris.base_logic Require Import lib.own.
-From stdpp Require Export gmap.
-Set Default Proof Using "Type".
-
-(** The STS describing the main barrier protocol. Every state has an index-set
-    associated with it. These indices are actually [gname], because we use them
-    with saved propositions. *)
-Inductive phase := Low | High.
-Record state := State { state_phase : phase; state_I : gset gname }.
-Add Printing Constructor state.
-Inductive token := Change (i : gname) | Send.
-
-Global Instance stateT_inhabited: Inhabited state := populate (State Low ∅).
-Global Instance Change_inj : Inj (=) (=) Change.
-Proof. by injection 1. Qed.
-
-Inductive prim_step : relation state :=
-  | ChangeI p I2 I1 : prim_step (State p I1) (State p I2)
-  | ChangePhase I : prim_step (State Low I) (State High I).
-
-Definition tok (s : state) : propset token :=
-  {[ t | ∃ i, t = Change i ∧ i ∉ state_I s ]} ∪
-  (if state_phase s is High then {[ Send ]} else ∅).
-Global Arguments tok !_ /.
-
-Canonical Structure sts := sts.Sts prim_step tok.
-
-(* The set of states containing some particular i *)
-Definition i_states (i : gname) : propset state := {[ s | i ∈ state_I s ]}.
-
-(* The set of low states *)
-Definition low_states : propset state := {[ s | state_phase s = Low ]}.
-
-Lemma i_states_closed i : sts.closed (i_states i) {[ Change i ]}.
-Proof.
-  split; first (intros [[] I]; set_solver).
-  (* If we do the destruct of the states early, and then inversion
-     on the proof of a transition, it doesn't work - we do not obtain
-     the equalities we need. So we destruct the states late, because this
-     means we can use "destruct" instead of "inversion". *)
-  intros s1 s2 Hs1 [T1 T2 Hdisj Hstep'].
-  inversion_clear Hstep' as [? ? ? ? Htrans _ _ Htok].
-  destruct Htrans as [[] ??|]; done || set_solver.
-Qed.
-
-Lemma low_states_closed : sts.closed low_states {[ Send ]}.
-Proof.
-  split; first (intros [??]; set_solver).
-  intros s1 s2 Hs1 [T1 T2 Hdisj Hstep'].
-  inversion_clear Hstep' as [? ? ? ? Htrans _ _ Htok].
-  destruct Htrans as [[] ??|]; done || set_solver.
-Qed.
-
-(* Proof that we can take the steps we need. *)
-Lemma signal_step I : sts.steps (State Low I, {[Send]}) (State High I, ∅).
-Proof. apply rtc_once. constructor; first constructor; set_solver. Qed.
-
-Lemma wait_step i I :
-  i ∈ I →
-  sts.steps (State High I, {[ Change i ]}) (State High (I ∖ {[ i ]}), ∅).
-Proof.
-  intros. apply rtc_once.
-  constructor; first constructor; [set_solver..|].
-  apply elem_of_equiv=>-[j|]; last set_solver.
-  destruct (decide (i = j)); set_solver.
-Qed.
-
-Lemma split_step p i i1 i2 I :
-  i ∈ I → i1 ∉ I → i2 ∉ I → i1 ≠ i2 →
-  sts.steps
-    (State p I, {[ Change i ]})
-    (State p ({[i1; i2]} ∪ I ∖ {[i]}), {[ Change i1; Change i2 ]}).
-Proof.
-  intros. apply rtc_once. constructor; first constructor.
-  - destruct p; set_solver.
-  - destruct p; set_solver.
-  - apply elem_of_equiv=> /= -[j|]; last set_solver.
-    set_unfold; rewrite !(inj_iff Change).
-    assert (Change j ∈ match p with Low => ∅ : propset token | High => {[Send]} end ↔ False)
-      as -> by (destruct p; set_solver).
-    destruct (decide (i1 = j)) as [->|]; first naive_solver.
-    destruct (decide (i2 = j)) as [->|]; first naive_solver.
-    destruct (decide (i = j)) as [->|]; naive_solver.
-Qed.