Merge branch 'master' of gitlab.mpi-sws.org:iris/reloc

.gitlab-ci.yml

@@ -18,8 +18,8 @@ variables:
     paths:
     - _opam/
   only:
-  - master
-  - /^ci/
+  - master@iris/reloc
+  - /^ci/@iris/reloc
   except:
   - triggers
   - schedules
@@ -38,7 +38,7 @@ build-coq.8.12.0:
 build-iris.dev:
   <<: *template
   variables:
-    OPAM_PINS: "coq version dev   coq-stdpp.dev git git+https://gitlab.mpi-sws.org/iris/stdpp.git#$STDPP_REV  coq-iris.dev git git+https://gitlab.mpi-sws.org/iris/iris.git#$IRIS_REV   coq-iris-heap-lang.dev git git+https://gitlab.mpi-sws.org/iris/iris.git#$IRIS_REV"
+    OPAM_PINS: "coq version 8.13.dev   coq-stdpp.dev git git+https://gitlab.mpi-sws.org/iris/stdpp.git#$STDPP_REV  coq-iris.dev git git+https://gitlab.mpi-sws.org/iris/iris.git#$IRIS_REV   coq-iris-heap-lang.dev git git+https://gitlab.mpi-sws.org/iris/iris.git#$IRIS_REV"
   except:
   only:
   - triggers

opam

@@ -9,6 +9,6 @@ build: [make "-j%{jobs}%"]
 install: [make "install"]
 remove: ["rm" "-rf" "%{lib}%/coq/user-contrib/reloc"]
 depends: [
-  "coq-iris-heap-lang" { (= "dev.2020-12-18.1.afe51813") | (= "dev") }
+  "coq-iris-heap-lang" { (= "dev.2021-04-22.1.35e8d8d7") | (= "dev") }
   "coq-autosubst" { = "dev" }
 ]

theories/examples/ticket_lock.v

@@ -2,7 +2,6 @@
 (** Ticket lock refines a simple spin lock *)
 From stdpp Require Import sets.
 From iris.algebra Require Export auth gset excl.
-From iris.base_logic Require Import auth.
 From reloc Require Import reloc lib.lock lib.counter.
 From iris.heap_lang.lib Require Export ticket_lock.
 
@@ -19,9 +18,9 @@ Definition lrel_lock `{relocG Σ} : lrel Σ :=
   ∃ A, (() → A) * (A → ()) * (A → ()).
 
 Class tlockG Σ :=
-  tlock_G :> authG Σ (gset_disjUR nat).
+  tlock_G :> inG Σ (authR (gset_disjUR nat)).
 Definition tlockΣ : gFunctors :=
-  #[ authΣ (gset_disjUR nat) ].
+  #[ GFunctor (authR $ gset_disjUR nat) ].
 Instance subG_tlockΣ {Σ} : subG tlockΣ Σ → tlockG Σ.
 Proof. solve_inG. Qed.
 
@@ -29,8 +28,8 @@ Definition lockPool := gset ((loc * loc * gname) * loc).
 Definition lockPoolR := gsetUR ((loc * loc * gname) * loc).
 
 Class lockPoolG Σ :=
-  lockPool_inG :> authG Σ lockPoolR.
-Definition lockPoolΣ := #[ authΣ lockPoolR ].
+  lockPool_inG :> inG Σ (authR lockPoolR).
+Definition lockPoolΣ := #[ GFunctor (authR $ lockPoolR) ].
 Instance subG_lockPoolΣ {Σ} : subG lockPoolΣ Σ → lockPoolG Σ.
 Proof. solve_inG. Qed.
 

theories/experimental/helping/helping_stack.v

@@ -21,7 +21,6 @@ are:
      ReLoC specification.
 *)
 From iris.algebra Require Import auth gmap agree list excl.
-From iris.base_logic.lib Require Import auth.
 From reloc Require Export reloc experimental.helping.offers.
 From reloc Require Import lib.list.
 From reloc.examples.stack Require Import CG_stack refinement.
@@ -89,7 +88,7 @@ Definition offerRegR :=
   gmapUR loc (agreeR (prodO valO (prodO gnameO (prodO natO (listO ectx_itemO))))).
 
 Class offerRegPreG Σ := OfferRegPreG {
-  offerReg_inG :> authG Σ offerRegR
+  offerReg_inG :> inG Σ (authR offerRegR)
 }.
 
 Definition offerize (x : (val * gname * nat * (list ectx_item))) :

theories/experimental/hocap/counter.v

@@ -4,13 +4,12 @@ From reloc Require Export reloc.
 From reloc.lib Require Export counter lock.
 From iris.algebra Require Export auth frac excl.
 From iris.bi.lib Require Export fractional.
-From iris.base_logic.lib Require Export auth.
 
 Class cnt_hocapG Σ := CntG {
-    cnt_hocapG_inG :> authG Σ (optionUR (prodR fracR (agreeR natO)));
+    cnt_hocapG_inG :> inG Σ (authR $ optionUR (prodR fracR (agreeR natO)));
 }.
 
-Definition cnt_hocapΣ := authΣ (optionUR (prodR fracR (agreeR natO))).
+Definition cnt_hocapΣ := GFunctor (authR (optionUR (prodR fracR (agreeR natO)))).
 
 Instance sub_cnt {Σ} : subG cnt_hocapΣ Σ → cnt_hocapG Σ.
 Proof. solve_inG. Qed.

theories/logic/adequacy.v

 (* ReLoC -- Relational logic for fine-grained concurrency *)
 (** Adequacy statements for the refinement proposition *)
 From iris.algebra Require Import auth frac agree.
-From iris.base_logic.lib Require Import auth.
 From iris.proofmode Require Import tactics.
 From iris.heap_lang Require Export adequacy.
 From reloc.logic Require Export spec_ra model.
@@ -11,7 +10,7 @@ Class relocPreG Σ := RelocPreG {
   reloc_preG_cfg  :> inG Σ (authR cfgUR)
 }.
 
-Definition relocΣ : gFunctors := #[heapΣ; authΣ cfgUR].
+Definition relocΣ : gFunctors := #[heapΣ; GFunctor (authR cfgUR)].
 Instance subG_relocPreG {Σ} : subG relocΣ Σ → relocPreG Σ.
 Proof. solve_inG. Qed.
 

theories/logic/model.v

@@ -30,7 +30,7 @@ Section lrel_ofe.
   Instance lrel_dist : Dist (lrel Σ) := λ n A B, ∀ w1 w2, A w1 w2 ≡{n}≡ B w1 w2.
   Lemma lrel_ofe_mixin : OfeMixin (lrel Σ).
   Proof. by apply (iso_ofe_mixin (lrel_car : lrel Σ → (val -d> val -d> iPropO Σ))). Qed.
-  Canonical Structure lrelC := OfeT (lrel Σ) lrel_ofe_mixin.
+  Canonical Structure lrelC := Ofe (lrel Σ) lrel_ofe_mixin.
 
   Global Instance lrel_cofe : Cofe lrelC.
   Proof.

theories/logic/spec_ra.v

@@ -11,9 +11,9 @@ Definition relocN := nroot .@ "reloc".
 Definition specN := relocN .@ "spec".
 
 (** The CMRA for the heap of the specification. *)
-Definition heapUR (L V : Type) `{Countable L} : ucmraT :=
+Definition heapUR (L V : Type) `{Countable L} : ucmra :=
   gmapUR L (prodR fracR (agreeR (leibnizO V))).
-Definition tpoolUR : ucmraT := gmapUR nat (exclR exprO).
+Definition tpoolUR : ucmra := gmapUR nat (exclR exprO).
 Definition cfgUR := prodUR tpoolUR (heapUR loc (option val)).
 
 (** The CMRA for the thread pool. *)

theories/prelude/bijections.v

@@ -3,7 +3,7 @@
 Originally from: "A Logical Relation for Monadic Encapsulation of State: Proving contextual equivalences in the presence of runST"
 by Amin Timany, Léo Stefanesco, Morten Krogh-Jespersen, Lars Birkedal *)
 From iris.algebra Require Import auth gset.
-From iris.base_logic Require Export auth invariants.
+From iris.base_logic Require Export invariants.
 From iris.proofmode Require Import tactics.
 Import uPred.
 
@@ -44,11 +44,11 @@ Qed.
 
 Definition bijUR := gsetUR (A * B).
 Class pBijPreG Σ := PBijPreG
-{ pBijPreG_inG :> authG Σ bijUR }.
+{ pBijPreG_inG :> inG Σ (authR bijUR) }.
 Class pBijG Σ := PBijG
-{ pBijG_inG :> authG Σ bijUR
+{ pBijG_inG :> inG Σ (authR bijUR)
 ; pBijG_name : gname }.
-Definition pBijΣ : gFunctors := #[ authΣ bijUR ].
+Definition pBijΣ : gFunctors := #[ GFunctor (authR bijUR) ].
 Global Instance subG_pBijΣ {Σ} : subG pBijΣ Σ → pBijPreG Σ.
 Proof. solve_inG. Qed.
 
@@ -94,7 +94,7 @@ Section logic.
     - apply auth_update_alloc.
       apply (gset_local_update _ _ (({[(a, b)]} : gset (A * B)) ∪ L)).
       apply union_subseteq_r.
-    - rewrite -gset_op_union auth_frag_op !own_op.
+    - rewrite -gset_op auth_frag_op !own_op.
       iDestruct "HL" as "[$ [$ _]]".
       iModIntro. iPureIntro.
       by apply bijective_extend.

theories/typing/interp.v

@@ -51,9 +51,9 @@ Section semtypes.
     interp τ Δ v v' -∗ ⌜val_is_unboxed v ∧ val_is_unboxed v'⌝.
   Proof.
     induction 1; simpl;
-    first [iIntros "[% %]"
+    first [iDestruct 1 as (? ?) "[% [% ?]]"
           |iDestruct 1 as (?) "[% %]"
-          |iDestruct 1 as (? ?) "[% [% ?]]"];
+          |iIntros "[% %]"];
     simplify_eq/=; eauto with iFrame.
   Qed.