From 73a32b6be5f270510e4478237ac8c06360014aa2 Mon Sep 17 00:00:00 2001
From: Dan Frumin <dfrumin@cs.ru.nl>
Date: Fri, 24 May 2019 11:25:54 +0200
Subject: [PATCH] bump iris

---
 guix.scm                        |  8 +++----
 opam                            |  2 +-
 theories/examples/symbol.v      | 12 ++++++-----
 theories/examples/ticket_lock.v |  5 ++++-
 theories/logic/adequacy.v       |  4 ++--
 theories/logic/spec_ra.v        |  6 +++---
 theories/logic/spec_rules.v     | 37 +++++++++++++++++----------------
 theories/prelude/bijections.v   |  7 ++++---
 8 files changed, 44 insertions(+), 37 deletions(-)

diff --git a/guix.scm b/guix.scm
index e21e5a3..0c694b0 100644
--- a/guix.scm
+++ b/guix.scm
@@ -30,10 +30,10 @@
   #:use-module (gnu packages coq)
   #:use-module ((guix licenses) #:prefix license:))
 
-(define stdpp-commit "d6eb24f23eeb42529210a4d422392d7950d920c0")
-(define stdpp-sha256 (base32 "1m1ys10f16v5ndxmwfjnw43p0qdb6fkk08z8864357zwmpvf2vgg")) ;; sha256 hash of the specific std++ checkout
-(define iris-commit "a9031f7f4979974426c5c9fa4ac315863b99c362")
-(define iris-sha256 (base32 "05kmbljc68ndnl8jyn3xy14f3vhcbxq7n2n3bkjyyfiyl8b2vaql")) ;; sha256 hash of the specific std++ checkout
+(define stdpp-commit "f8719169e3ed75123d88c59d292ddd0972351ad3")
+(define stdpp-sha256 (base32 "0fb7vj5l8j8ms7v3ag74i61q8hygc8w692dlfyli9vxbds7ff7lc")) ;; sha256 hash of the specific std++ checkout
+(define iris-commit "c9984c7fc0b2067b11012099ce7884c981e492ed")
+(define iris-sha256 (base32 "1lf3k6h2jc26r3ns44qnd4l9b769a2bx17xc3fni6m39y8w5h0py")) ;; sha256 hash of the specific std++ checkout
 (define %source-dir (dirname (current-filename)))
 
 (define-public coq-stdpp
diff --git a/opam b/opam
index b5e192c..08e2cbf 100644
--- a/opam
+++ b/opam
@@ -9,6 +9,6 @@ build: [make "-j%{jobs}%"]
 install: [make "install"]
 remove: ["rm" "-rf" "%{lib}%/coq/user-contrib/reloc"]
 depends: [
-  "coq-iris" { (= "dev.2019-04-25.1.a9031f7f") | (= "dev") }
+  "coq-iris" { (= "dev.2019-05-24.0.c9984c7f") | (= "dev") }
   "coq-autosubst" { = "dev.coq86" }
 ]
diff --git a/theories/examples/symbol.v b/theories/examples/symbol.v
index 10d97f3..7117295 100644
--- a/theories/examples/symbol.v
+++ b/theories/examples/symbol.v
@@ -64,7 +64,7 @@ Section rules.
   Proof.
     iIntros "Hn Hm".
     by iDestruct (own_valid_2 with "Hn Hm")
-      as %[?%mnat_included _]%auth_valid_discrete_2.
+      as %[?%mnat_included _]%auth_both_valid.
   Qed.
 
   Lemma same_size (n m : nat) :
@@ -152,7 +152,7 @@ Section proof.
     iModIntro. iExists _. iFrame. iNext. iIntros "Hs1'".
     rel_load_r. rel_pure_r. rel_pure_r.
     iDestruct (own_valid_2 with "Ha Hn")
-      as %[?%mnat_included _]%auth_valid_discrete_2.
+      as %[?%mnat_included _]%auth_both_valid.
     rel_op_l. rel_op_r. rewrite bool_decide_true; last lia.
     rel_pure_r. rel_load_r. rel_op_r.
     iMod ("Hcl" with "[Ha Hs1' Hs2' Htbl1' Htbl2' Hls]") as "_".
@@ -189,7 +189,7 @@ Section proof.
     iInv sizeN as (m ls) "(Ha & Hs1' & >Hs2' & >Htbl1' & >Htbl2' & Hls)" "Hcl".
     iModIntro. iExists _. iFrame. iNext. iIntros "Hs1'".
     iDestruct (own_valid_2 with "Ha Hn")
-      as %[?%mnat_included _]%auth_valid_discrete_2.
+      as %[?%mnat_included _]%auth_both_valid.
     iMod ("Hcl" with "[Ha Hs1' Hs2' Htbl1' Htbl2' Hls]") as "_".
     { iNext. iExists _,_. by iFrame. }
     clear ls. repeat rel_pure_l.
@@ -225,7 +225,8 @@ Section proof.
     rel_alloc_r size2 as "[Hs2 Hs2']"; repeat rel_pure_r.
     rel_alloc_l tbl1 as "[Htbl1 Htbl1']"; repeat rel_pure_l.
     rel_alloc_r tbl2 as "[Htbl2 Htbl2']"; repeat rel_pure_r.
-    iMod (own_alloc (● (0%nat : mnat))) as (γ) "Ha"; first done.
+    iMod (own_alloc (● (0%nat : mnat))) as (γ) "Ha".
+    { by apply auth_auth_valid. }
     iMod (inv_alloc sizeN _ (table_inv γ size1 size2 tbl1 tbl2) with "[Hs1 Hs2 Htbl1 Htbl2 Ha]") as "#Hinv".
     { iNext. iExists _,_. iFrame. iApply lrel_list_nil. }
     rel_apply_r refines_newlock_r.
@@ -303,7 +304,8 @@ Section proof.
     rel_alloc_r size2 as "[Hs2 Hs2']"; repeat rel_pure_r.
     rel_alloc_l tbl1 as "[Htbl1 Htbl1']"; repeat rel_pure_l.
     rel_alloc_r tbl2 as "[Htbl2 Htbl2']"; repeat rel_pure_r.
-    iMod (own_alloc (● (0%nat : mnat))) as (γ) "Ha"; first done.
+    iMod (own_alloc (● (0%nat : mnat))) as (γ) "Ha".
+    { by apply auth_auth_valid. }
     iMod (inv_alloc sizeN _ (table_inv γ size1 size2 tbl1 tbl2) with "[Hs1 Hs2 Htbl1 Htbl2 Ha]") as "#Hinv".
     { iNext. iExists _,_. iFrame. iApply lrel_list_nil. }
     rel_apply_r refines_newlock_r.
diff --git a/theories/examples/ticket_lock.v b/theories/examples/ticket_lock.v
index 24db89b..c4491dc 100644
--- a/theories/examples/ticket_lock.v
+++ b/theories/examples/ticket_lock.v
@@ -50,7 +50,10 @@ Section refinement.
   Qed.
 
   Lemma newIssuedTickets : (|==> ∃ γ, issuedTickets γ 0)%I.
-  Proof. iMod (own_alloc (● (GSet ∅))) as (γ) "Hγ"; [done|eauto]. Qed.
+  Proof.
+    iMod (own_alloc (● (GSet ∅))) as (γ) "Hγ"; [|by eauto].
+    by apply auth_auth_valid.
+  Qed.
 
   Lemma issueNewTicket γ m :
     issuedTickets γ m ==∗
diff --git a/theories/logic/adequacy.v b/theories/logic/adequacy.v
index 5ead070..caa0974 100644
--- a/theories/logic/adequacy.v
+++ b/theories/logic/adequacy.v
@@ -32,7 +32,7 @@ Proof.
   iMod (own_alloc (● (to_tpool [e'], to_gen_heap (heap σ))
     ⋅ ◯ ((to_tpool [e'] : tpoolUR, ∅) : cfgUR)))
     as (γc) "[Hcfg1 Hcfg2]".
-  { apply auth_valid_discrete_2. split=>//.
+  { apply auth_both_valid. split=>//.
     - apply prod_included. split=>///=.
       apply: ucmra_unit_least.
     - split=>//. apply to_tpool_valid. apply to_gen_heap_valid. }
@@ -55,7 +55,7 @@ Proof.
     iInv specN as (tp σ') ">[Hown Hsteps]" "Hclose"; iDestruct "Hsteps" as %Hsteps'.
     rewrite tpool_mapsto_eq /tpool_mapsto_def /=.
     iDestruct (own_valid_2 with "Hown Hj") as %Hvalid.
-    move: Hvalid=> /auth_valid_discrete_2
+    move: Hvalid=> /auth_both_valid
        [/prod_included [/tpool_singleton_included Hv2 _] _].
     destruct tp as [|? tp']; simplify_eq/=.
     iMod ("Hclose" with "[-]") as "_".
diff --git a/theories/logic/spec_ra.v b/theories/logic/spec_ra.v
index 2d72003..c2abfec 100644
--- a/theories/logic/spec_ra.v
+++ b/theories/logic/spec_ra.v
@@ -1,6 +1,6 @@
 (* ReLoC -- Relational logic for fine-grained concurrency *)
 (** A resource algebra for the specification programs. *)
-From iris.algebra Require Import auth gmap agree list frac.
+From iris.algebra Require Import auth excl gmap agree list frac.
 From iris.bi Require Export fractional.
 From iris.base_logic Require Export gen_heap invariants.
 From iris.proofmode Require Import tactics.
@@ -137,7 +137,7 @@ Section mapsto.
   Proof.
     apply bi.wand_intro_r.
     rewrite heapS_mapsto_eq -own_op -auth_frag_op own_valid uPred.discrete_valid.
-    f_equiv=> /auth_own_valid /=.
+    f_equiv=> /=.
     rewrite pair_op op_singleton right_id pair_op.
     move=> [_ Hv]. move:Hv => /=.
     rewrite singleton_valid.
@@ -147,7 +147,7 @@ Section mapsto.
   Lemma mapsto_valid l q v : l ↦ₛ{q} v -∗ ✓ q.
   Proof.
     rewrite heapS_mapsto_eq /heapS_mapsto_def own_valid !uPred.discrete_valid.
-    apply pure_mono=> /auth_own_valid /= [_ Hfoo].
+    apply pure_mono=> /auth_frag_valid /= [_ Hfoo].
     revert Hfoo. simpl. rewrite singleton_valid.
     by intros [? _].
   Qed.
diff --git a/theories/logic/spec_rules.v b/theories/logic/spec_rules.v
index 1904ed2..bc9b1ff 100644
--- a/theories/logic/spec_rules.v
+++ b/theories/logic/spec_rules.v
@@ -1,6 +1,6 @@
 (* ReLoC -- Relational logic for fine-grained concurrency *)
 (** Rules for updating the specification program. *)
-From iris.algebra Require Import auth frac agree gmap list.
+From iris.algebra Require Import auth excl frac agree gmap list.
 From iris.proofmode Require Import tactics.
 From iris.heap_lang Require Export lang notation.
 From reloc.logic Require Export spec_ra.
@@ -62,10 +62,11 @@ Section rules.
     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'))). }
+    { eapply auth_update, prod_local_update_1.
+      by eapply (singleton_local_update _ j (Excl (fill K e))),
+        (exclusive_local_update _ (Excl (fill K e'))). }
     iFrame "Hj". iApply "Hclose". iNext. iExists (<[j:=fill K e']> tp), σ.
     rewrite to_tpool_insert'; last eauto.
     iFrame. iPureIntro.
@@ -105,7 +106,7 @@ Section rules.
     rewrite /spec_ctx tpool_mapsto_eq /tpool_mapsto_def /=.
     iInv specN as (tp σ) ">[Hown %]" "Hclose".
     iDestruct (own_valid_2 with "Hown Hj")
-      as %[[?%tpool_singleton_included' _]%prod_included _]%auth_valid_discrete_2.
+      as %[[?%tpool_singleton_included' _]%prod_included _]%auth_both_valid.
     destruct (exist_fresh (used_proph_id σ)) as [p Hp].
     iMod (own_update_2 with "Hown Hj") as "[Hown Hj]".
     { by eapply auth_update, prod_local_update_1,
@@ -125,7 +126,7 @@ Section rules.
     rewrite /spec_ctx tpool_mapsto_eq /tpool_mapsto_def /=.
     iInv specN as (tp σ) ">[Hown %]" "Hclose".
     iDestruct (own_valid_2 with "Hown Hj")
-      as %[[?%tpool_singleton_included' _]%prod_included _]%auth_valid_discrete_2.
+      as %[[?%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 #()))). }
@@ -146,7 +147,7 @@ Section rules.
     iInv specN as (tp σ) ">[Hown %]" "Hclose".
     destruct (exist_fresh (dom (gset loc) (heap σ))) as [l Hl%not_elem_of_dom].
     iDestruct (own_valid_2 with "Hown Hj")
-      as %[[?%tpool_singleton_included' _]%prod_included ?]%auth_valid_discrete_2.
+      as %[[?%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 (#l)%E))). }
@@ -171,9 +172,9 @@ Section rules.
     rewrite heapS_mapsto_eq /heapS_mapsto_def /=.
     iInv specN as (tp σ) ">[Hown %]" "Hclose".
     iDestruct (own_valid_2 with "Hown Hj")
-      as %[[?%tpool_singleton_included' _]%prod_included ?]%auth_valid_discrete_2.
+      as %[[?%tpool_singleton_included' _]%prod_included ?]%auth_both_valid.
     iDestruct (own_valid_2 with "Hown Hl")
-      as %[[? ?%gen_heap_singleton_included]%prod_included ?]%auth_valid_discrete_2.     iMod (own_update_2 with "Hown Hj") as "[Hown Hj]".
+      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, singleton_local_update,
         (exclusive_local_update _ (Excl (fill K (of_val v)))). }
     iFrame "Hj Hl". iApply "Hclose". iNext.
@@ -193,9 +194,9 @@ Section rules.
     rewrite heapS_mapsto_eq /heapS_mapsto_def /=.
     iInv specN as (tp σ) ">[Hown %]" "Hclose".
     iDestruct (own_valid_2 with "Hown Hj")
-      as %[[?%tpool_singleton_included' _]%prod_included _]%auth_valid_discrete_2.
+      as %[[?%tpool_singleton_included' _]%prod_included _]%auth_both_valid.
     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, singleton_local_update,
         (exclusive_local_update _ (Excl (fill K #()))). }
@@ -223,9 +224,9 @@ Section rules.
     rewrite /spec_ctx tpool_mapsto_eq /tpool_mapsto_def heapS_mapsto_eq /heapS_mapsto_def.
     iInv specN as (tp σ) ">[Hown %]" "Hclose".
     iDestruct (own_valid_2 with "Hown Hj")
-      as %[[?%tpool_singleton_included' _]%prod_included ?]%auth_valid_discrete_2.
+      as %[[?%tpool_singleton_included' _]%prod_included ?]%auth_both_valid.
     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, singleton_local_update,
         (exclusive_local_update _ (Excl (fill K (# false)))). }
@@ -248,9 +249,9 @@ Section rules.
     rewrite /spec_ctx tpool_mapsto_eq /tpool_mapsto_def heapS_mapsto_eq /heapS_mapsto_def.
     iInv specN as (tp σ) ">[Hown %]" "Hclose".
     iDestruct (own_valid_2 with "Hown Hj")
-      as %[[?%tpool_singleton_included' _]%prod_included _]%auth_valid_discrete_2.
+      as %[[?%tpool_singleton_included' _]%prod_included _]%auth_both_valid.
     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, singleton_local_update,
         (exclusive_local_update _ (Excl (fill K (# true)))). }
@@ -275,9 +276,9 @@ Section rules.
     rewrite /spec_ctx tpool_mapsto_eq /tpool_mapsto_def heapS_mapsto_eq /heapS_mapsto_def.
     iInv specN as (tp σ) ">[Hown %]" "Hclose".
     iDestruct (own_valid_2 with "Hown Hj")
-      as %[[?%tpool_singleton_included' _]%prod_included _]%auth_valid_discrete_2.
+      as %[[?%tpool_singleton_included' _]%prod_included _]%auth_both_valid.
     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, singleton_local_update,
         (exclusive_local_update _ (Excl (fill K (# i1)))). }
@@ -300,7 +301,7 @@ Section rules.
     rewrite /spec_ctx tpool_mapsto_eq /tpool_mapsto_def.
     iInv specN as (tp σ) ">[Hown %]" "Hclose".
     iDestruct (own_valid_2 with "Hown Hj")
-      as %[[?%tpool_singleton_included' _]%prod_included ?]%auth_valid_discrete_2.
+      as %[[?%tpool_singleton_included' _]%prod_included ?]%auth_both_valid.
     assert (j < length tp)%nat by eauto using lookup_lt_Some.
     iMod (own_update_2 with "Hown Hj") as "[Hown Hj]".
     { by eapply auth_update, prod_local_update_1,
diff --git a/theories/prelude/bijections.v b/theories/prelude/bijections.v
index cfe7174..158ac06 100644
--- a/theories/prelude/bijections.v
+++ b/theories/prelude/bijections.v
@@ -66,7 +66,8 @@ Section logic.
   Lemma alloc_empty_bij : (|==> ∃ γ, BIJ γ ∅)%I.
   Proof.
     rewrite BIJ_eq /BIJ_def.
-    iMod (own_alloc (● (∅ : bijUR))) as (γ) "H"; first done.
+    iMod (own_alloc (● (∅ : bijUR))) as (γ) "H".
+    { by apply auth_auth_valid. }
     iModIntro; iExists _; iFrame. iPureIntro. apply empty_bijective.
   Qed.
 
@@ -115,8 +116,8 @@ Section logic.
   Proof.
     iIntros "HL H1 H2". rewrite BIJ_eq /BIJ_def inBij_eq /inBij_def.
     iDestruct "HL" as "[HL HL1]"; iDestruct "HL1" as %HL.
-    iDestruct (own_valid_2 with "HL H1") as %Hv1%auth_valid_discrete_2.
-    iDestruct (own_valid_2 with "HL H2") as %Hv2%auth_valid_discrete_2.
+    iDestruct (own_valid_2 with "HL H1") as %Hv1%auth_both_valid.
+    iDestruct (own_valid_2 with "HL H2") as %Hv2%auth_both_valid.
     iPureIntro.
     destruct Hv1 as [Hv1 _]; destruct Hv2 as [Hv2 _].
     apply gset_included, elem_of_subseteq_singleton in Hv1;
-- 
GitLab