Merge branch 'hai/auth_frac' into 'master'

Bump Iris with changes in `auth`

See merge request !17

opam

@@ -9,6 +9,6 @@ build: [make "-j%{jobs}%"]
 install: [make "install"]
 remove: ["rm" "-rf" "%{lib}%/coq/user-contrib/iris_examples"]
 depends: [
-  "coq-iris" { (= "dev.2019-04-17.0.60d28bbb") | (= "dev") }
+  "coq-iris" { (= "dev.2019-05-24.0.c9984c7f") | (= "dev") }
   "coq-autosubst" { = "dev.coq86" }
 ]

theories/hocap/contrib_bag.v

@@ -50,7 +50,7 @@ Section proof.
     iIntros (Φ) "_ HΦ". iApply wp_fupd.
     iApply (newBag_spec b NB); eauto.
     iNext. iIntros (v γb) "[#Hbag Hcntn]".
-    iMod (own_alloc (●! ∅ ⋅ ◯! ∅)) as (γ) "[Hown Hpart]"; first done.
+    iMod (own_alloc (●! ∅ ⋅ ◯! ∅)) as (γ) "[Hown Hpart]"; first by apply auth_both_valid.
     iMod (inv_alloc NI _ (∃ X, bag_contents b γb X ∗ own γ (●! X))%I with "[Hcntn Hown]") as "#Hinv".
     { iNext. iExists _. iFrame. }
     iApply "HΦ". iModIntro. iExists _,_. iFrame "Hinv Hbag Hpart".

theories/lecture_notes/ccounter.v

@@ -58,7 +58,7 @@ Section ccounter.
     iIntros (Φ) "_ HΦ". rewrite -wp_fupd.
     wp_apply newcounter_spec; auto.
     iIntros (ℓ) "H"; iDestruct "H" as (γ₂) "[#HCnt Hown]".
-    iMod (own_alloc (●! m%nat ⋅ ◯! m%nat)) as (γ₁) "[Hγ Hγ']"; first done.
+    iMod (own_alloc (●! m%nat ⋅ ◯! m%nat)) as (γ₁) "[Hγ Hγ']"; first by apply auth_both_valid.
     iMod (inv_alloc (N .@ "counter") _ (ccounter_inv γ₁ γ₂) with "[Hγ Hown]").
     { iNext. iExists _. by iFrame. }
     iModIntro. iApply "HΦ". rewrite /is_ccounter; eauto.

theories/lecture_notes/coq_intro_example_2.v

@@ -29,7 +29,7 @@ Section monotone_counter.
      algebra we shall be using. The Iris library contains all the ingredients
      needed to compose this particular resource algebra from simpler components,
      however to illustrate how to define our own we will define it from scratch.
-     
+
      In the subsequent section we show how to obtain an equivalent resource
      algebra from the building blocks provided by the Iris Coq library. 
   *)
@@ -423,7 +423,7 @@ Section monotone_counter'.
   Proof.
     (* Use a simplified definition of validity for when the underlying CMRA is discrete, i.e., an RA.
        The general definition also involves the use of step-indices, which is not needed in our case. *)
-    rewrite auth_valid_discrete_2.
+    rewrite auth_both_valid.
     split.
     - intros [? _]; by apply mnat_included.
     - intros ?%mnat_included; done.
@@ -460,7 +460,7 @@ Section monotone_counter'.
     iIntros (Φ) "_ HCont".
     rewrite /newCounter -wp_fupd.
     wp_lam.
-    iMod (own_alloc (● (0%nat : mnatUR) ⋅ ◯ 0%nat)) as (γ) "[HAuth HFrac]".
+    iMod (own_alloc (● (0%nat : mnatUR) ⋅ ◯ (0%nat : mnatUR))) as (γ) "[HAuth HFrac]".
     - apply mcounterRA_valid_auth_frag'; auto.
     - wp_alloc ℓ as "Hpt".
       iMod (inv_alloc N _ (counter_inv' ℓ γ) with "[Hpt HAuth]") as "HInv".
@@ -505,7 +505,7 @@ Section monotone_counter'.
     iInv N as (k) ">[Hpt HOwnAuth]" "HClose".
     destruct (decide (k = m)); subst.
     + wp_cas_suc.
-      iMod (own_update γ ((● m ⋅ ◯ n)) (● (S m : mnatUR) ⋅ (◯ S n)) with "[HOwnFrag HOwnAuth]") as "[HOwnAuth HOwnFrag]".
+      iMod (own_update γ ((● m ⋅ ◯ n)) (● (S m : mnatUR) ⋅ (◯ (S n : mnatUR))) with "[HOwnFrag HOwnAuth]") as "[HOwnAuth HOwnFrag]".
       { apply mcounterRA_update'. }
       { rewrite own_op; iFrame. }
       iMod ("HClose" with "[Hpt HOwnAuth]") as "_".
@@ -606,7 +606,7 @@ Section ccounter.
     {{{ γ ℓ, RET #ℓ; is_ccounter γ ℓ 1 0%nat }}}.
   Proof.
     iIntros (Φ) "_ HΦ". rewrite -wp_fupd /newCounter /=. wp_lam. wp_alloc ℓ as "Hpt".
-    iMod (own_alloc (●! O%nat ⋅ ◯! 0%nat)) as (γ) "[Hγ Hγ']"; first done.
+    iMod (own_alloc (●! O%nat ⋅ ◯! 0%nat)) as (γ) "[Hγ Hγ']"; first by apply auth_both_valid.
     iMod (inv_alloc N _ (ccounter_inv γ ℓ) with "[Hpt Hγ]").
     { iNext. iExists 0%nat. by iFrame. }
     iModIntro. iApply "HΦ". rewrite /is_ccounter; eauto.

theories/logatom/elimination_stack/hocap_spec.v

@@ -165,7 +165,7 @@ Section logatom_hocap.
     iIntros (Φ) "_ HΦ". iApply wp_fupd. iApply logatom.new_stack_spec; first done.
     iIntros "!>" (γs s) "[Hstack Hcont]".
     iMod (own_alloc (● Excl' [] ⋅ ◯ Excl' [])) as (γw) "[Hs● Hs◯]".
-    { apply auth_valid_discrete_2. split; done. }
+    { apply auth_both_valid. split; done. }
     iApply ("HΦ" $! (γs, γw)). rewrite /hocap_is_stack. iFrame.
     iApply inv_alloc. eauto with iFrame.
   Qed.
@@ -212,11 +212,11 @@ Section logatom_hocap.
     iIntros (???) "Hf1 Hf2". iDestruct (own_valid_2 with "Hf1 Hf2") as %[].
   Qed.
   Next Obligation.
-    iIntros (???) "Ha1 Ha2". iDestruct (own_valid_2 with "Ha1 Ha2") as %[].
+    iIntros (???) "Ha1 Ha2". by iDestruct (own_valid_2 with "Ha1 Ha2") as %[].
   Qed.
   Next Obligation.
     iIntros (???) "Hf Ha". iDestruct (own_valid_2 with "Ha Hf") as
-      %[->%Excl_included%leibniz_equiv _]%auth_valid_discrete_2. done.
+      %[->%Excl_included%leibniz_equiv _]%auth_both_valid. done.
   Qed.
   Next Obligation.
     iIntros (???) "Hf Ha". iMod (own_update_2 with "Ha Hf") as "[? ?]".

theories/logatom/elimination_stack/stack.v

@@ -175,7 +175,7 @@ Section stack.
     wp_apply alloc_spec; first done. iIntros (head) "Hhead". wp_let.
     wp_apply alloc_spec; first done. iIntros (offer) "Hoffer". wp_let.
     iMod (own_alloc (● Excl' [] ⋅ ◯ Excl' [])) as (γs) "[Hs● Hs◯]".
-    { apply auth_valid_discrete_2. split; done. }
+    { apply auth_both_valid. split; done. }
     iMod (inv_alloc stackN _ (stack_inv γs head offer) with "[-HΦ Hs◯]").
     { iNext. iExists None, None, _. iFrame. done. }
     wp_pures. iApply "HΦ". iFrame "Hs◯". iModIntro. iExists _, _. auto.
@@ -209,7 +209,7 @@ Section stack.
     - (* The CAS succeeded. Update everything accordingly. *)
       iMod "AU" as (l') "[Hl' [_ Hclose]]".
       iDestruct (own_valid_2 with "Hs● Hl'") as
-        %[->%Excl_included%leibniz_equiv _]%auth_valid_discrete_2.
+        %[->%Excl_included%leibniz_equiv _]%auth_both_valid.
       iMod (own_update_2 with "Hs● Hl'") as "[Hs● Hl']".
       { eapply auth_update, option_local_update, (exclusive_local_update _ (Excl _)). done. }
       iMod ("Hclose" with "Hl'") as "HΦ". iModIntro.
@@ -283,7 +283,7 @@ Section stack.
       iDestruct "Hlist" as ">%". subst stack_rep.
       iMod "AU" as (l') "[Hl' [_ Hclose]]".
       iDestruct (own_valid_2 with "Hs● Hl'") as
-        %[->%Excl_included%leibniz_equiv _]%auth_valid_discrete_2.
+        %[->%Excl_included%leibniz_equiv _]%auth_both_valid.
       iMod ("Hclose" with "Hl'") as "HΦ".
       iSplitR "HΦ"; first by eauto 10 with iFrame.
       iIntros "!>". wp_pures. by iApply "HΦ".
@@ -305,7 +305,7 @@ Section stack.
         and we are done. *)
         iMod "AU" as (l') "[Hl' [_ Hclose]]".
         iDestruct (own_valid_2 with "Hs● Hl'") as
-          %[->%Excl_included%leibniz_equiv _]%auth_valid_discrete_2.
+          %[->%Excl_included%leibniz_equiv _]%auth_both_valid.
         destruct l as [|v' l]; simpl.
         { (* Contradiction. *) iDestruct "Hlist" as ">%". done. }
         iDestruct "Hlist" as (tail' q' rep') "[>Heq [>Htail' Hlist]]".
@@ -345,13 +345,13 @@ Section stack.
         iInv stackN as (stack_rep offer_rep l) "(>Hs● & >H↦ & Hlist & Hoff)".
         iMod "AUoff" as (l') "[Hl' [_ Hclose]]".
         iDestruct (own_valid_2 with "Hs● Hl'") as
-          %[->%Excl_included%leibniz_equiv _]%auth_valid_discrete_2.
+          %[->%Excl_included%leibniz_equiv _]%auth_both_valid.
         iMod (own_update_2 with "Hs● Hl'") as "[Hs● Hl']".
         { eapply auth_update, option_local_update, (exclusive_local_update _ (Excl _)). done. }
         iMod ("Hclose" with "Hl'") as "HQoff".
         iMod "AU" as (l') "[Hl' [_ Hclose]]".
         iDestruct (own_valid_2 with "Hs● Hl'") as
-          %[->%Excl_included%leibniz_equiv _]%auth_valid_discrete_2.
+          %[->%Excl_included%leibniz_equiv _]%auth_both_valid.
         iMod (own_update_2 with "Hs● Hl'") as "[Hs● Hl']".
         { eapply auth_update, option_local_update, (exclusive_local_update _ (Excl _)). done. }
         iMod ("Hclose" with "Hl'") as "HΦ".

theories/logatom/flat_combiner/misc.v

@@ -2,7 +2,7 @@
 
 From iris.program_logic Require Export weakestpre.
 From iris.heap_lang Require Export lang proofmode notation.
-From iris.algebra Require Import auth frac gmap agree.
+From iris.algebra Require Import excl auth frac gmap agree.
 From iris.bi Require Import fractional.
 From iris.base_logic Require Import auth.
 

theories/logatom/snapshot/atomic_snapshot.v

@@ -160,11 +160,11 @@ Section atomic_snapshot.
     wp_alloc ly as "Hly".
     set (Excl' (v1, v2)) as p.
     iMod (own_alloc (● p ⋅ ◯ p)) as (γ1) "[Hp⚫ Hp◯]". {
-      rewrite /p. apply auth_valid_discrete_2. split; done.
+      rewrite /p. apply auth_both_valid. split; done.
     }
     set (new_timestamp 0 v1) as t.
     iMod (own_alloc (● gmap_to_UR t ⋅ ◯ gmap_to_UR t)) as (γ2) "[Ht⚫ Ht◯]". {
-      rewrite /t /new_timestamp. apply auth_valid_discrete_2.
+      rewrite /t /new_timestamp. apply auth_both_valid.
       split; first done. rewrite /gmap_to_UR map_fmap_singleton. apply singleton_valid. done.
     }
     wp_pures. iApply ("Hp" $! (γ1, γ2)).
@@ -192,7 +192,7 @@ Section atomic_snapshot.
   Proof.
     iIntros "Hγ● Hγ◯".
     iDestruct (own_valid_2 with "Hγ● Hγ◯") as
-        %[H%Excl_included%leibniz_equiv _]%auth_valid_discrete_2.
+        %[H%Excl_included%leibniz_equiv _]%auth_both_valid.
     done.
   Qed.
 
@@ -223,7 +223,7 @@ Section atomic_snapshot.
   Proof.
     iIntros "[Hγ⚫ Hγ◯]".
     iDestruct (own_valid_2 with "Hγ⚫ Hγ◯") as
-        %[H Hv]%auth_valid_discrete_2. iPureIntro. intros t x HT2.
+        %[H Hv]%auth_both_valid. iPureIntro. intros t x HT2.
     pose proof (iffLR (lookup_included (gmap_to_UR T2) (gmap_to_UR T1)) H t) as Ht.
     rewrite !lookup_fmap HT2 /= in Ht.
     destruct (is_Some_included _ _ Ht) as [? [t2 [Ht2 ->]]%fmap_Some_1]; first by eauto.

theories/logatom/treiber2.v

@@ -156,7 +156,7 @@ Lemma auth_agree γ xs ys :
   own γ (● (Excl' xs)) -∗ own γ (◯ (Excl' ys)) -∗ ⌜xs = ys⌝.
 Proof.
   iIntros "Hγ● Hγ◯". by iDestruct (own_valid_2 with "Hγ● Hγ◯")
-    as %[<-%Excl_included%leibniz_equiv _]%auth_valid_discrete_2.
+    as %[<-%Excl_included%leibniz_equiv _]%auth_both_valid.
 Qed.
 
 (** The view of the authority can be updated together with the local view. *)
@@ -223,7 +223,8 @@ Proof.
      our camera named [γ], containing the empty list. This step (and the next)
      requires the fancy update modality that was introduced earlier. *)
   iMod (own_alloc (● (Some (Excl [])) ⋅ ◯ (Some (Excl []))))
-    as (γ) "[Hγ● Hγ◯]"; (* Validity is trivial. *) first done.
+    as (γ) "[Hγ● Hγ◯]";
+    (* Validity is trivial. *) first by apply auth_both_valid.
   (* We can then allocate the invariant (with mask [N]).  Note that we can use
      [eauto 10 with iFrame] to prove [▷ stack_inv ℓ γ]. *) 
   iMod (inv_alloc N _ (stack_inv ℓ γ) with "[Hl Hγ●]")

theories/logrel/F_mu_ref/rules_binary.v

 From iris.program_logic Require Import lifting.
-From iris.algebra Require Import auth frac agree gmap list.
+From iris.algebra Require Import excl auth frac agree gmap list.
 From iris_examples.logrel.F_mu_ref Require Export rules.
 From iris.proofmode Require Import tactics.
 Import uPred.
@@ -65,7 +65,7 @@ Section cfg.
     iInv specN as ">Hspec" "Hclose".
     iDestruct "Hspec" as (e'' σ) "[Hown %]".
     iDestruct (@own_valid_2 with "Hown Hj")
-      as %[[?%Excl_included%leibniz_equiv _]%prod_included Hvalid]%auth_valid_discrete_2; subst.
+      as %[[?%Excl_included%leibniz_equiv _]%prod_included Hvalid]%auth_both_valid; subst.
     iMod (own_update_2 with "Hown Hj") as "[Hown Hj]".
     { by eapply auth_update, prod_local_update_1, option_local_update,
         (exclusive_local_update _ (Excl (fill K e'))). }
@@ -93,7 +93,7 @@ Section cfg.
     iInv specN as ">Hinv'" "Hclose". iDestruct "Hinv'" as (e2 σ) "[Hown %]".
     destruct (exist_fresh (dom (gset positive) σ)) as [l Hl%not_elem_of_dom].
     iDestruct (own_valid_2 _ with "Hown Hj")
-      as %[[?%Excl_included%leibniz_equiv _]%prod_included ?]%auth_valid_discrete_2.
+      as %[[?%Excl_included%leibniz_equiv _]%prod_included ?]%auth_both_valid.
     subst.
     iMod (own_update_2 with "Hown Hj") as "[Hown Hj]".
     { by eapply auth_update, prod_local_update_1, option_local_update,
@@ -117,10 +117,10 @@ Section cfg.
     rewrite /spec_ctx /tpool_mapsto /heapS_mapsto.
     iInv specN as ">Hinv'" "Hclose". iDestruct "Hinv'" as (e2 σ) "[Hown %]".
     iDestruct (own_valid_2 _ with "Hown Hj")
-      as %[[?%Excl_included%leibniz_equiv _]%prod_included ?]%auth_valid_discrete_2.
+      as %[[?%Excl_included%leibniz_equiv _]%prod_included ?]%auth_both_valid.
     subst.
     iDestruct (own_valid_2 with "Hown Hl")
-      as %[[_ ?%gen_heap_singleton_included]%prod_included _]%auth_valid_discrete_2.
+      as %[[_ ?%gen_heap_singleton_included]%prod_included _]%auth_both_valid.
     iMod (own_update_2 with "Hown Hj") as "[Hown Hj]".
     { by eapply auth_update, prod_local_update_1, option_local_update,
         (exclusive_local_update _ (Excl (fill K (of_val v)))). }
@@ -139,10 +139,10 @@ Section cfg.
     rewrite /spec_ctx /tpool_mapsto /heapS_mapsto.
     iInv specN as ">Hinv'" "Hclose". iDestruct "Hinv'" as (e2 σ) "[Hown %]".
     iDestruct (own_valid_2 _ with "Hown Hj")
-      as %[[?%Excl_included%leibniz_equiv _]%prod_included ?]%auth_valid_discrete_2.
+      as %[[?%Excl_included%leibniz_equiv _]%prod_included ?]%auth_both_valid.
     subst.
     iDestruct (own_valid_2 _ with "Hown Hl")
-      as %[[_ Hl%gen_heap_singleton_included]%prod_included _]%auth_valid_discrete_2.
+      as %[[_ Hl%gen_heap_singleton_included]%prod_included _]%auth_both_valid.
     iMod (own_update_2 with "Hown Hj") as "[Hown Hj]".
     { by eapply auth_update, prod_local_update_1, option_local_update,
         (exclusive_local_update _ (Excl (fill K Unit))). }

theories/logrel/F_mu_ref/soundness.v

@@ -17,7 +17,7 @@ Proof.
   eapply (wp_adequacy Σ _); eauto.
   iIntros (Hinv ?).
   iMod (own_alloc (● to_gen_heap σ)) as (γ) "Hh".
-  { apply (auth_auth_valid _ (to_gen_heap_valid _ _ σ)). }
+  { by apply auth_auth_valid, to_gen_heap_valid. }
   iModIntro. iExists (λ σ _, own γ (● to_gen_heap σ)); iFrame.
   set (HeapΣ := (HeapG Σ Hinv (GenHeapG _ _ Σ _ _ _ γ))).
   iApply (wp_wand with "[]").

theories/logrel/F_mu_ref/soundness_binary.v

 From iris_examples.logrel.F_mu_ref Require Export context_refinement.
-From iris.algebra Require Import auth frac agree.
+From iris.algebra Require Import excl auth frac agree.
 From iris.proofmode Require Import tactics.
 From iris.program_logic Require Import adequacy.
 From iris_examples.logrel.F_mu_ref Require Import soundness.
@@ -16,10 +16,10 @@ Proof.
   eapply (wp_adequacy Σ); first by apply _.
   iIntros (Hinv ?).
   iMod (own_alloc (● to_gen_heap ∅)) as (γ) "Hh".
-  { apply (auth_auth_valid _ (to_gen_heap_valid _ _ ∅)). }
+  { by apply auth_auth_valid, to_gen_heap_valid. }
   iMod (own_alloc (● (Excl' e', ∅)
     ⋅ ◯ ((Excl' e', ∅) : cfgUR))) as (γc) "[Hcfg1 Hcfg2]".
-  { apply auth_valid_discrete_2. split=>//. }
+  { apply auth_both_valid. split=>//. }
   set (Hcfg := CFGSG _ _ γc).
   iMod (inv_alloc specN _ (spec_ctx ([e'], ∅)) with "[Hcfg1]") as "#Hcfg".
   { iNext. iExists e', ∅. iSplit; eauto.
@@ -38,7 +38,7 @@ Proof.
     iDestruct "Hinv" as (e'' σ) "[Hown %]".
     rewrite /tpool_mapsto /=.
     iDestruct (own_valid_2 with "Hown Hj") as %Hvalid.
-    move: Hvalid=> /auth_valid_discrete_2
+    move: Hvalid=> /auth_both_valid
       [/prod_included [Hv2 _] _]. apply Excl_included, leibniz_equiv in Hv2. subst.
     iMod ("Hclose" with "[-]") as "_".
     + iExists (#v2), σ. auto.

theories/logrel/F_mu_ref_conc/examples/stack/refinement.v

@@ -47,7 +47,7 @@ Section Stack_refinement.
     simpl. iApply wp_pure_step_later; trivial. iNext. simpl.
     iAsimpl.
     (* establishing the invariant *)
-    iMod (own_alloc (● (∅ : stackUR))) as (γ) "Hemp"; first done.
+    iMod (own_alloc (● (∅ : stackUR))) as (γ) "Hemp"; first by apply auth_auth_valid.
     set (istkG := StackG _ _ γ).
     change γ with (@stack_name _ istkG).
     change H1 with (@stack_inG _ istkG).

theories/logrel/F_mu_ref_conc/examples/stack/stack_rules.v

@@ -25,7 +25,7 @@ Section Rules.
   Lemma stack_mapstos_agree l v w : l ↦ˢᵗᵏ v ∗ l ↦ˢᵗᵏ w ⊢ ⌜v = w⌝.
   Proof.
     rewrite -own_op -auth_frag_op op_singleton own_valid.
-    by iIntros (->%auth_own_valid%singleton_valid%agree_op_invL').
+    by iIntros (->%auth_frag_valid%singleton_valid%agree_op_invL').
   Qed.
 
   Program Definition StackLink_pre (Q : D) : D -n> D := λne P v,
@@ -94,7 +94,7 @@ Section Rules.
   Proof.
     iIntros "[Howns Hls] Hl".
     iDestruct (own_valid_2 with "Howns Hl")
-      as %[[az [Haz Hq]]%singleton_included _]%auth_valid_discrete_2.
+      as %[[az [Haz Hq]]%singleton_included _]%auth_both_valid.
     rewrite lookup_fmap in Haz.
     assert (∃ z, h !! l = Some z) as Hz.
     { revert Haz; case: (h !! l) => [z|] Hz; first (by eauto); inversion Hz. }

theories/logrel/F_mu_ref_conc/rules_binary.v

 From iris.program_logic Require Export language ectx_language ectxi_language.
 From iris.program_logic Require Import lifting.
-From iris.algebra Require Import auth frac agree gmap list.
+From iris.algebra Require Import excl auth frac agree gmap list.
 From iris_examples.logrel.F_mu_ref_conc Require Export rules.
 From iris.proofmode Require Import tactics.
 Import uPred.
@@ -174,7 +174,7 @@ Section cfg.
     iInv specN as (tp σ) ">[Hown Hrtc]" "Hclose".
     iDestruct "Hrtc" as %Hrtc.
     iDestruct (own_valid_2 with "Hown Hj")
-      as %[[Htpj%tpool_singleton_included' _]%prod_included ?]%auth_valid_discrete_2.
+      as %[[Htpj%tpool_singleton_included' _]%prod_included ?]%auth_both_valid.
     iMod (own_update_2 with "Hown Hj") as "[Hown Hj]".
     { by eapply auth_update, prod_local_update_1,
         singleton_local_update, (exclusive_local_update _ (Excl (fill K e'))). }
@@ -221,7 +221,7 @@ Section cfg.