Merge branch 'robbert/excl_auth' into 'master'

`excl_auth` camera

See merge request iris/iris!328

CHANGELOG.md

@@ -25,6 +25,9 @@ Coq development, but not every API-breaking change is listed.  Changes marked
   Coq goal `big star of context ⊢ proof mode goal`.
 * Rename `iProp`/`iPreProp` to `iPropO`/`iPrePropO` since they are `ofeT`s.
   Introduce `iProp` for the `Type` carrier of `iPropO`.
+* Move derived camera constructions (`frac_auth` and `ufrac_auth`) to the folder
+  `algebra/lib`.
+* Add derived camera construction `excl_auth A` for `auth (option (excl A))`.
 
 ## Iris 3.2.0 (released 2019-08-29)
 

_CoqProject

@@ -17,7 +17,6 @@ theories/algebra/big_op.v
 theories/algebra/cmra_big_op.v
 theories/algebra/sts.v
 theories/algebra/auth.v
-theories/algebra/frac_auth.v
 theories/algebra/gmap.v
 theories/algebra/ofe.v
 theories/algebra/base.v
@@ -39,7 +38,9 @@ theories/algebra/deprecated.v
 theories/algebra/proofmode_classes.v
 theories/algebra/ufrac.v
 theories/algebra/namespace_map.v
-theories/algebra/ufrac_auth.v
+theories/algebra/lib/excl_auth.v
+theories/algebra/lib/frac_auth.v
+theories/algebra/lib/ufrac_auth.v
 theories/bi/notation.v
 theories/bi/interface.v
 theories/bi/derived_connectives.v

theories/algebra/lib/excl_auth.v

+From iris.algebra Require Export auth excl updates.
+From iris.algebra Require Import local_updates.
+From iris.base_logic Require Import base_logic.
+
+Definition excl_authR (A : ofeT) : cmraT :=
+  authR (optionUR (exclR A)).
+Definition excl_authUR (A : ofeT) : ucmraT :=
+  authUR (optionUR (exclR A)).
+
+Definition excl_auth_auth {A : ofeT} (a : A) : excl_authR A :=
+  ● (Some (Excl a)).
+Definition excl_auth_frag {A : ofeT} (a : A) : excl_authR A :=
+  ◯ (Some (Excl a)).
+
+Typeclasses Opaque excl_auth_auth excl_auth_frag.
+
+Instance: Params (@excl_auth_auth) 1 := {}.
+Instance: Params (@excl_auth_frag) 2 := {}.
+
+Notation "●E a" := (excl_auth_auth a) (at level 10).
+Notation "◯E a" := (excl_auth_frag a) (at level 10).
+
+Section excl_auth.
+  Context {A : ofeT}.
+  Implicit Types a b : A.
+
+  Global Instance excl_auth_auth_ne : NonExpansive (@excl_auth_auth A).
+  Proof. solve_proper. Qed.
+  Global Instance excl_auth_auth_proper : Proper ((≡) ==> (≡)) (@excl_auth_auth A).
+  Proof. solve_proper. Qed.
+  Global Instance excl_auth_frag_ne : NonExpansive (@excl_auth_frag A).
+  Proof. solve_proper. Qed.
+  Global Instance excl_auth_frag_proper : Proper ((≡) ==> (≡)) (@excl_auth_frag A).
+  Proof. solve_proper. Qed.
+
+  Global Instance excl_auth_auth_discrete a : Discrete a → Discrete (●E a).
+  Proof. intros; apply auth_auth_discrete; [apply Some_discrete|]; apply _. Qed.
+  Global Instance excl_auth_frag_discrete a : Discrete a → Discrete (◯E a).
+  Proof. intros; apply auth_frag_discrete, Some_discrete; apply _. Qed.
+
+  Lemma excl_auth_validN n a : ✓{n} (●E a ⋅ ◯E a).
+  Proof. by rewrite auth_both_validN. Qed.
+  Lemma excl_auth_valid a : ✓ (●E a ⋅ ◯E a).
+  Proof. intros. by apply auth_both_valid_2. Qed.
+
+  Lemma excl_auth_agreeN n a b : ✓{n} (●E a ⋅ ◯E b) → a ≡{n}≡ b.
+  Proof.
+    rewrite auth_both_validN /= => -[Hincl Hvalid].
+    move: Hincl=> /Some_includedN_exclusive /(_ I) ?. by apply (inj Excl).
+  Qed.
+  Lemma excl_auth_agree a b : ✓ (●E a ⋅ ◯E b) → a ≡ b.
+  Proof.
+    intros. apply equiv_dist=> n. by apply excl_auth_agreeN, cmra_valid_validN.
+  Qed.
+  Lemma excl_auth_agreeL `{!LeibnizEquiv A} a b : ✓ (●E a ⋅ ◯E b) → a = b.
+  Proof. intros. by apply leibniz_equiv, excl_auth_agree. Qed.
+
+  Lemma excl_auth_agreeI {M} a b : ✓ (●E a ⋅ ◯E b) ⊢@{uPredI M} (a ≡ b).
+  Proof.
+    rewrite auth_both_validI bi.and_elim_r bi.and_elim_l.
+    apply bi.exist_elim=> -[[c|]|];
+      by rewrite bi.option_equivI /= excl_equivI //= bi.False_elim.
+  Qed.
+
+  Lemma excl_auth_frag_validN_op_1_l n a b : ✓{n} (◯E a ⋅ ◯E b) → False.
+  Proof. by rewrite -auth_frag_op auth_frag_validN. Qed.
+  Lemma excl_auth_frag_valid_op_1_l a b : ✓ (◯E a ⋅ ◯E b) → False.
+  Proof. by rewrite -auth_frag_op auth_frag_valid. Qed.
+
+  Lemma excl_auth_update a b a' : ●E a ⋅ ◯E b ~~> ●E a' ⋅ ◯E a'.
+  Proof.
+    intros. by apply auth_update, option_local_update, exclusive_local_update.
+  Qed.
+End excl_auth.

theories/base_logic/lib/boxes.v

 From iris.proofmode Require Import tactics.
-From iris.algebra Require Import excl auth gmap agree.
+From iris.algebra Require Import lib.excl_auth gmap agree.
 From iris.base_logic.lib Require Export invariants.
 Set Default Proof Using "Type".
 Import uPred.
@@ -7,10 +7,10 @@ Import uPred.
 (** The CMRAs we need. *)
 Class boxG Σ :=
   boxG_inG :> inG Σ (prodR
-    (authR (optionUR (exclR boolO)))
+    (excl_authR boolO)
     (optionR (agreeR (laterO (iPrePropO Σ))))).
 
-Definition boxΣ : gFunctors := #[ GFunctor (authR (optionUR (exclR boolO)) *
+Definition boxΣ : gFunctors := #[ GFunctor (excl_authR boolO *
                                             optionRF (agreeRF (▶ ∙)) ) ].
 
 Instance subG_boxΣ Σ : subG boxΣ Σ → boxG Σ.
@@ -21,14 +21,14 @@ Section box_defs.
 
   Definition slice_name := gname.
 
-  Definition box_own_auth (γ : slice_name) (a : auth (option (excl bool))) : iProp Σ :=
+  Definition box_own_auth (γ : slice_name) (a : excl_authR boolO) : iProp Σ :=
     own γ (a, None).
 
   Definition box_own_prop (γ : slice_name) (P : iProp Σ) : iProp Σ :=
     own γ (ε, Some (to_agree (Next (iProp_unfold P)))).
 
   Definition slice_inv (γ : slice_name) (P : iProp Σ) : iProp Σ :=
-    (∃ b, box_own_auth γ (● Excl' b) ∗ if b then P else True)%I.
+    (∃ b, box_own_auth γ (●E b) ∗ if b then P else True)%I.
 
   Definition slice (γ : slice_name) (P : iProp Σ) : iProp Σ :=
     (box_own_prop γ P ∗ inv N (slice_inv γ P))%I.
@@ -36,7 +36,7 @@ Section box_defs.
   Definition box (f : gmap slice_name bool) (P : iProp Σ) : iProp Σ :=
     (∃ Φ : slice_name → iProp Σ,
       ▷ (P ≡ [∗ map] γ ↦ _ ∈ f, Φ γ) ∗
-      [∗ map] γ ↦ b ∈ f, box_own_auth γ (◯ Excl' b) ∗ box_own_prop γ (Φ γ) ∗
+      [∗ map] γ ↦ b ∈ f, box_own_auth γ (◯E b) ∗ box_own_prop γ (Φ γ) ∗
                          inv N (slice_inv γ (Φ γ)))%I.
 End box_defs.
 
@@ -75,18 +75,18 @@ Global Instance box_proper f : Proper ((≡) ==> (≡)) (box N f).
 Proof. apply ne_proper, _. Qed.
 
 Lemma box_own_auth_agree γ b1 b2 :
-  box_own_auth γ (● Excl' b1) ∗ box_own_auth γ (◯ Excl' b2) ⊢ ⌜b1 = b2⌝.
+  box_own_auth γ (●E b1) ∗ box_own_auth γ (◯E b2) ⊢ ⌜b1 = b2⌝.
 Proof.
   rewrite /box_own_prop -own_op own_valid prod_validI /= and_elim_l.
-  by iDestruct 1 as % [[[] [=]%leibniz_equiv] ?]%auth_both_valid.
+  by iDestruct 1 as %?%excl_auth_agreeL.
 Qed.
 
 Lemma box_own_auth_update γ b1 b2 b3 :
-  box_own_auth γ (● Excl' b1) ∗ box_own_auth γ (◯ Excl' b2)
-  ==∗ box_own_auth γ (● Excl' b3) ∗ box_own_auth γ (◯ Excl' b3).
+  box_own_auth γ (●E b1) ∗ box_own_auth γ (◯E b2)
+  ==∗ box_own_auth γ (●E b3) ∗ box_own_auth γ (◯E b3).
 Proof.
   rewrite /box_own_auth -!own_op. apply own_update, prod_update; last done.
-  by apply auth_update, option_local_update, exclusive_local_update.
+  apply excl_auth_update.
 Qed.
 
 Lemma box_own_agree γ Q1 Q2 :
@@ -108,7 +108,7 @@ Lemma slice_insert_empty E q f Q P :
     slice N γ Q ∗ ▷?q box N (<[γ:=false]> f) (Q ∗ P).
 Proof.
   iDestruct 1 as (Φ) "[#HeqP Hf]".
-  iMod (own_alloc_cofinite (● Excl' false ⋅ ◯ Excl' false,
+  iMod (own_alloc_cofinite (●E false ⋅ ◯E false,
     Some (to_agree (Next (iProp_unfold Q)))) (dom _ f))
     as (γ) "[Hdom Hγ]"; first by (split; [apply auth_both_valid|]).
   rewrite pair_split. iDestruct "Hγ" as "[[Hγ Hγ'] #HγQ]".
@@ -225,7 +225,7 @@ Lemma box_empty E f P :
 Proof.
   iDestruct 1 as (Φ) "[#HeqP Hf]".
   iAssert (([∗ map] γ↦b ∈ f, ▷ Φ γ) ∗
-    [∗ map] γ↦b ∈ f, box_own_auth γ (◯ Excl' false) ∗  box_own_prop γ (Φ γ) ∗
+    [∗ map] γ↦b ∈ f, box_own_auth γ (◯E false) ∗  box_own_prop γ (Φ γ) ∗
       inv N (slice_inv γ (Φ γ)))%I with "[> Hf]" as "[HΦ ?]".
   { rewrite -big_sepM_sep -big_sepM_fupd. iApply (@big_sepM_impl with "[$Hf]").
     iIntros "!#" (γ b ?) "(Hγ' & #HγΦ & #Hinv)".

theories/heap_lang/lib/counter.v

 From iris.proofmode Require Import tactics.
-From iris.algebra Require Import frac_auth auth.
+From iris.algebra Require Import lib.frac_auth auth.
 From iris.base_logic.lib Require Export invariants.
 From iris.program_logic Require Export weakestpre.
 From iris.heap_lang Require Export lang.

theories/program_logic/ownp.v

 From iris.proofmode Require Import tactics classes.
-From iris.algebra Require Import excl auth.
+From iris.algebra Require Import lib.excl_auth.
 From iris.program_logic Require Export weakestpre.
 From iris.program_logic Require Import lifting adequacy.
 From iris.program_logic Require ectx_language.
@@ -16,24 +16,24 @@ union.
 
 Class ownPG (Λ : language) (Σ : gFunctors) := OwnPG {
   ownP_invG : invG Σ;
-  ownP_inG :> inG Σ (authR (optionUR (exclR (stateO Λ))));
+  ownP_inG :> inG Σ (excl_authR (stateO Λ));
   ownP_name : gname;
 }.
 
 Instance ownPG_irisG `{!ownPG Λ Σ} : irisG Λ Σ := {
   iris_invG := ownP_invG;
-  state_interp σ κs _ := own ownP_name (● (Excl' σ))%I;
+  state_interp σ κs _ := own ownP_name (●E σ)%I;
   fork_post _ := True%I;
 }.
 Global Opaque iris_invG.
 
 Definition ownPΣ (Λ : language) : gFunctors :=
   #[invΣ;
-    GFunctor (authR (optionUR (exclR (stateO Λ))))].
+    GFunctor (excl_authR (stateO Λ))].
 
 Class ownPPreG (Λ : language) (Σ : gFunctors) : Set := IrisPreG {
   ownPPre_invG :> invPreG Σ;
-  ownPPre_state_inG :> inG Σ (authR (optionUR (exclR (stateO Λ))))
+  ownPPre_state_inG :> inG Σ (excl_authR (stateO Λ))
 }.
 
 Instance subG_ownPΣ {Λ Σ} : subG (ownPΣ Λ) Σ → ownPPreG Λ Σ.
@@ -41,8 +41,7 @@ Proof. solve_inG. Qed.
 
 (** Ownership *)
 Definition ownP `{!ownPG Λ Σ} (σ : state Λ) : iProp Σ :=
-  own ownP_name (◯ (Excl' σ)).
-
+  own ownP_name (◯E σ).
 Typeclasses Opaque ownP.
 Instance: Params (@ownP) 3 := {}.
 
@@ -53,9 +52,9 @@ Theorem ownP_adequacy Σ `{!ownPPreG Λ Σ} s e σ φ :
 Proof.
   intros Hwp. apply (wp_adequacy Σ _).
   iIntros (? κs).
-  iMod (own_alloc (● (Excl' σ) ⋅ ◯ (Excl' σ))) as (γσ) "[Hσ Hσf]";
-    first by apply auth_both_valid.
-  iModIntro. iExists (λ σ κs, own γσ (● (Excl' σ)))%I, (λ _, True%I).
+  iMod (own_alloc (●E σ ⋅ ◯E σ)) as (γσ) "[Hσ Hσf]";
+    first by apply excl_auth_valid.
+  iModIntro. iExists (λ σ κs, own γσ (●E σ))%I, (λ _, True%I).
   iFrame "Hσ".
   iApply (Hwp (OwnPG _ _ _ _ γσ)). rewrite /ownP. iFrame.
 Qed.
@@ -69,9 +68,9 @@ Theorem ownP_invariance Σ `{!ownPPreG Λ Σ} s e σ1 t2 σ2 φ :
 Proof.
   intros Hwp Hsteps. eapply (wp_invariance Σ Λ s e σ1 t2 σ2 _)=> //.
   iIntros (? κs).
-  iMod (own_alloc (● (Excl' σ1) ⋅ ◯ (Excl' σ1))) as (γσ) "[Hσ Hσf]";
+  iMod (own_alloc (●E σ1 ⋅ ◯E σ1)) as (γσ) "[Hσ Hσf]";
     first by apply auth_both_valid.
-  iExists (λ σ κs' _, own γσ (● (Excl' σ)))%I, (λ _, True%I).
+  iExists (λ σ κs' _, own γσ (●E σ))%I, (λ _, True%I).
   iFrame "Hσ".
   iMod (Hwp (OwnPG _ _ _ _ γσ) with "[Hσf]") as "[$ H]";
     first by rewrite /ownP; iFrame.
@@ -118,8 +117,7 @@ Section lifting.
       iModIntro; iSplit; [by destruct s|]; iNext; iIntros (e2 σ2 efs Hstep).
       iDestruct "Hσκs" as "Hσ". rewrite /ownP.
       iMod (own_update_2 with "Hσ Hσf") as "[Hσ Hσf]".
-      { apply auth_update. apply option_local_update.
-         by apply (exclusive_local_update _ (Excl σ2)). }
+      { apply excl_auth_update. }
       iFrame "Hσ". iApply ("H" with "[]"); eauto with iFrame.
   Qed.