update dependencies

coq-lambda-rust.opam

@@ -13,7 +13,7 @@ the type system, and safety proof for some Rust libraries.
 """
 
 depends: [
-  "coq-iris" { (= "dev.2021-05-05.0.6f18e8cd") | (= "dev") }
+  "coq-iris" { (= "dev.2021-06-03.0.2959900d") | (= "dev") }
 ]
 
 build: [make "-j%{jobs}%"]

theories/lang/adequacy.v

@@ -4,8 +4,8 @@ From lrust.lang Require Export heap.
 From lrust.lang Require Import proofmode notation.
 Set Default Proof Using "Type".
 
-Class lrustPreG Σ := HeapPreG {
-  lrust_preG_irig :> invPreG Σ;
+Class lrustPreG Σ := HeapGpreS {
+  lrust_preG_irig :> invGpreS Σ;
   lrust_preG_heap :> inG Σ (authR heapUR);
   lrust_preG_heap_freeable :> inG Σ (authR heap_freeableUR)
 }.
@@ -26,7 +26,7 @@ Proof.
   { apply (auth_auth_valid (to_heap _)), to_heap_valid. }
   iMod (own_alloc (● (∅ : heap_freeableUR))) as (fγ) "Hfγ";
     first by apply auth_auth_valid.
-  set (Hheap := HeapG _ _ _ vγ fγ).
+  set (Hheap := HeapGS _ _ _ vγ fγ).
   iModIntro. iExists (λ σ _, heap_ctx σ), (λ _, True%I). iSplitL.
   { iExists ∅. by iFrame. }
   by iApply (Hwp (LRustG _ _ Hheap)).

theories/lang/heap.v

@@ -18,7 +18,7 @@ Definition heapUR : ucmra :=
 Definition heap_freeableUR : ucmra :=
   gmapUR block (prodR fracR (gmapR Z (exclR unitO))).
 
-Class heapG Σ := HeapG {
+Class heapGS Σ := HeapGS {
   heap_inG :> inG Σ (authR heapUR);
   heap_freeable_inG :> inG Σ (authR heap_freeableUR);
   heap_name : gname;
@@ -34,7 +34,7 @@ Definition heap_freeable_rel (σ : state) (hF : heap_freeableUR) : Prop :=
     qs.2 ≠ ∅ ∧ ∀ i, is_Some (σ !! (blk, i)) ↔ is_Some (qs.2 !! i).
 
 Section definitions.
-  Context `{!heapG Σ}.
+  Context `{!heapGS Σ}.
 
   Definition heap_mapsto_st (st : lock_state)
              (l : loc) (q : Qp) (v: val) : iProp Σ :=
@@ -106,7 +106,7 @@ Section to_heap.
 End to_heap.
 
 Section heap.
-  Context `{!heapG Σ}.
+  Context `{!heapGS Σ}.
   Implicit Types P Q : iProp Σ.
   Implicit Types σ : state.
   Implicit Types E : coPset.

theories/lang/lib/arc.v

@@ -99,7 +99,7 @@ Definition try_unwrap_full : val :=
     else #2.
 
 (** The CMRA we need. *)
-(* Not bundling heapG, as it may be shared with other users. *)
+(* Not bundling heapGS, as it may be shared with other users. *)
 
 (* See rc.v for understanding the structure of this CMRA.
    The only additional thing is the [optionR (exclR unitO))], used to handle

theories/lang/lifting.v

@@ -7,11 +7,11 @@ Set Default Proof Using "Type".
 Import uPred.
 
 Class lrustG Σ := LRustG {
-  lrustG_invG : invG Σ;
-  lrustG_gen_heapG :> heapG Σ
+  lrustG_invG : invGS Σ;
+  lrustG_gen_heapG :> heapGS Σ
 }.
 
-Instance lrustG_irisG `{!lrustG Σ} : irisG lrust_lang Σ := {
+Instance lrustG_irisG `{!lrustG Σ} : irisGS lrust_lang Σ := {
   iris_invG := lrustG_invG;
   state_interp σ _ κs _ := heap_ctx σ;
   fork_post _ := True%I;

theories/lifetime/at_borrow.v

@@ -5,14 +5,14 @@ Set Default Proof Using "Type".
 
 (** Atomic persistent bors  *)
 (* TODO : update the TEX with the fact that we can choose the namespace. *)
-Definition at_bor `{!invG Σ, !lftG Σ userE} κ N (P : iProp Σ) :=
+Definition at_bor `{!invGS Σ, !lftG Σ userE} κ N (P : iProp Σ) :=
   (∃ i, &{κ,i}P ∗
     (⌜N ## lftN⌝ ∗ inv N (idx_bor_own 1 i) ∨
      ⌜N = lftN⌝ ∗ inv N (∃ q, idx_bor_own q i)))%I.
 Notation "&at{ κ , N }" := (at_bor κ N) (format "&at{ κ , N }") : bi_scope.
 
 Section atomic_bors.
-  Context `{!invG Σ, !lftG Σ userE} (P : iProp Σ) (N : namespace).
+  Context `{!invGS Σ, !lftG Σ userE} (P : iProp Σ) (N : namespace).
 
   Global Instance at_bor_ne κ n : Proper (dist n ==> dist n) (at_bor κ N).
   Proof. solve_proper. Qed.
@@ -97,7 +97,7 @@ Section atomic_bors.
   Qed.
 End atomic_bors.
 
-Lemma at_bor_acc_lftN `{!invG Σ, !lftG Σ userE} (P : iProp Σ) E κ :
+Lemma at_bor_acc_lftN `{!invGS Σ, !lftG Σ userE} (P : iProp Σ) E κ :
   ↑lftN ⊆ E →
   lft_ctx -∗ &at{κ,lftN}P ={E,E∖↑lftN}=∗ ▷P ∗ (▷P ={E∖↑lftN,E}=∗ True) ∨
              [†κ] ∗ |={E∖↑lftN,E}=> True.

theories/lifetime/frac_borrow.v

@@ -6,16 +6,16 @@ Set Default Proof Using "Type".
 
 Class frac_borG Σ := frac_borG_inG :> inG Σ fracR.
 
-Local Definition frac_bor_inv `{!invG Σ, !lftG Σ userE, !frac_borG Σ}
+Local Definition frac_bor_inv `{!invGS Σ, !lftG Σ userE, !frac_borG Σ}
                               (φ : Qp → iProp Σ) γ κ' :=
   (∃ q, φ q ∗ own γ q ∗ (⌜q = 1%Qp⌝ ∨ ∃ q', ⌜(q + q' = 1)%Qp⌝ ∗ q'.[κ']))%I.
 
-Definition frac_bor `{!invG Σ, !lftG Σ userE, !frac_borG Σ} κ (φ : Qp → iProp Σ) :=
+Definition frac_bor `{!invGS Σ, !lftG Σ userE, !frac_borG Σ} κ (φ : Qp → iProp Σ) :=
   (∃ γ κ', κ ⊑ κ' ∗ &at{κ',lftN} (frac_bor_inv φ γ κ'))%I.
 Notation "&frac{ κ }" := (frac_bor κ) (format "&frac{ κ }") : bi_scope.
 
 Section frac_bor.
-  Context `{!invG Σ, !lftG Σ userE, !frac_borG Σ} (φ : Qp → iProp Σ).
+  Context `{!invGS Σ, !lftG Σ userE, !frac_borG Σ} (φ : Qp → iProp Σ).
   Implicit Types E : coPset.
 
   Global Instance frac_bor_contractive κ n :
@@ -155,7 +155,7 @@ Section frac_bor.
   Qed.
 End frac_bor.
 
-Lemma frac_bor_lft_incl `{!invG Σ, !lftG Σ userE, !frac_borG Σ} κ κ' q:
+Lemma frac_bor_lft_incl `{!invGS Σ, !lftG Σ userE, !frac_borG Σ} κ κ' q:
   lft_ctx -∗ &frac{κ}(λ q', (q * q').[κ']) -∗ κ ⊑ κ'.
 Proof.
   iIntros "#LFT#Hbor". iApply lft_incl_intro. iModIntro. iSplitR.

theories/lifetime/lifetime.v

@@ -26,7 +26,7 @@ Definition lft_incl_syntactic (κ κ' : lft) : Prop := ∃ κ'', κ'' ⊓ κ' =
 Infix "⊑ˢʸⁿ" := lft_incl_syntactic (at level 40) : stdpp_scope.
 
 Section derived.
-Context `{!invG Σ, !lftG Σ userE}.
+Context `{!invGS Σ, !lftG Σ userE}.
 Implicit Types κ : lft.
 
 Lemma lft_create E :

theories/lifetime/lifetime_sig.v

@@ -25,17 +25,17 @@ Module Type lifetime_sig.
   Parameter static : lft.
   Declare Instance lft_intersect : Meet lft.
 
-  Parameter lft_ctx : ∀ `{!invG Σ, !lftG Σ userE}, iProp Σ.
+  Parameter lft_ctx : ∀ `{!invGS Σ, !lftG Σ userE}, iProp Σ.
 
   Parameter lft_tok : ∀ `{!lftG Σ userE} (q : Qp) (κ : lft), iProp Σ.
   Parameter lft_dead : ∀ `{!lftG Σ userE} (κ : lft), iProp Σ.
 
-  Parameter lft_incl : ∀ `{!invG Σ, !lftG Σ userE} (κ κ' : lft), iProp Σ.
-  Parameter bor : ∀ `{!invG Σ, !lftG Σ userE} (κ : lft) (P : iProp Σ), iProp Σ.
+  Parameter lft_incl : ∀ `{!invGS Σ, !lftG Σ userE} (κ κ' : lft), iProp Σ.
+  Parameter bor : ∀ `{!invGS Σ, !lftG Σ userE} (κ : lft) (P : iProp Σ), iProp Σ.
 
   Parameter bor_idx : Type.
   Parameter idx_bor_own : ∀ `{!lftG Σ userE} (q : frac) (i : bor_idx), iProp Σ.
-  Parameter idx_bor : ∀ `{!invG Σ, !lftG Σ userE} (κ : lft) (i : bor_idx) (P : iProp Σ), iProp Σ.
+  Parameter idx_bor : ∀ `{!invGS Σ, !lftG Σ userE} (κ : lft) (i : bor_idx) (P : iProp Σ), iProp Σ.
 
   (** Our lifetime creation lemma offers allocating a lifetime that is defined
   by a [positive] in some given infinite set. This operation converts the
@@ -53,7 +53,7 @@ Module Type lifetime_sig.
   Infix "⊑" := lft_incl (at level 70) : bi_scope.
 
   Section properties.
-  Context `{!invG Σ, !lftG Σ userE}.
+  Context `{!invGS Σ, !lftG Σ userE}.
 
   (** * Instances *)
   Global Declare Instance lft_inhabited : Inhabited lft.
@@ -172,7 +172,7 @@ Module Type lifetime_sig.
   Parameter lftΣ : gFunctors.
   Global Declare Instance subG_lftPreG Σ : subG lftΣ Σ → lftPreG Σ.
 
-  Parameter lft_init : ∀ `{!invG Σ, !lftPreG Σ} E userE,
+  Parameter lft_init : ∀ `{!invGS Σ, !lftPreG Σ} E userE,
     ↑lftN ⊆ E → ↑lftN ## userE →
     ⊢ |={E}=> ∃ _ : lftG Σ userE, lft_ctx.
 End lifetime_sig.

theories/lifetime/meta.v

@@ -26,7 +26,7 @@ Definition lft_meta `{!lftG Σ userE, lft_metaG Σ} (κ : lft) (γ : gname) : iP
     own lft_meta_gname (dyn_reservation_map_data p (to_agree γ)).
 
 Section lft_meta.
-  Context `{!invG Σ, !lftG Σ userE, lft_metaG Σ}.
+  Context `{!invGS Σ, !lftG Σ userE, lft_metaG Σ}.
 
   Global Instance lft_meta_timeless κ γ : Timeless (lft_meta κ γ).
   Proof. apply _. Qed.

theories/lifetime/model/accessors.v

@@ -5,7 +5,7 @@ From iris.base_logic.lib Require Import boxes.
 Set Default Proof Using "Type".
 
 Section accessors.
-Context `{!invG Σ, !lftG Σ userE}.
+Context `{!invGS Σ, !lftG Σ userE}.
 Implicit Types κ : lft.
 
 (* Helper internal lemmas *)

theories/lifetime/model/borrow.v

@@ -6,7 +6,7 @@ From iris.proofmode Require Import tactics.
 Set Default Proof Using "Type".
 
 Section borrow.
-Context `{!invG Σ, !lftG Σ userE}.
+Context `{!invGS Σ, !lftG Σ userE}.
 Implicit Types κ : lft.
 
 Lemma raw_bor_create E κ P :

theories/lifetime/model/borrow_sep.v

@@ -6,7 +6,7 @@ From iris.proofmode Require Import tactics.
 Set Default Proof Using "Type".
 
 Section borrow.
-Context `{!invG Σ, !lftG Σ userE}.
+Context `{!invGS Σ, !lftG Σ userE}.
 Implicit Types κ : lft.
 
 Lemma bor_sep E κ P Q :

theories/lifetime/model/creation.v

@@ -6,7 +6,7 @@ From iris.proofmode Require Import tactics.
 Set Default Proof Using "Type".
 
 Section creation.
-Context `{!invG Σ, !lftG Σ userE}.
+Context `{!invGS Σ, !lftG Σ userE}.
 Implicit Types κ : lft.
 
 Lemma lft_kill (I : gmap lft lft_names) (K K' : gset lft) (κ : lft) :

theories/lifetime/model/definitions.v

@@ -80,7 +80,7 @@ Definition to_ilftUR : gmap lft lft_names → ilftUR := fmap to_agree.
 Definition to_borUR : gmap slice_name bor_state → borUR := fmap ((1%Qp,.) ∘ to_agree).
 
 Section defs.
-  Context `{!invG Σ, !lftG Σ userE}.
+  Context `{!invGS Σ, !lftG Σ userE}.
 
   Definition lft_tok (q : Qp) (κ : lft) : iProp Σ :=
     ([∗ mset] Λ ∈ κ, own alft_name (◯ {[ Λ := Cinl q ]}))%I.
@@ -224,7 +224,7 @@ Typeclasses Opaque lft_tok lft_dead bor_cnt lft_bor_alive lft_bor_dead
   idx_bor_own idx_bor raw_bor bor.
 
 Section basic_properties.
-Context `{!invG Σ, !lftG Σ userE}.
+Context `{!invGS Σ, !lftG Σ userE}.
 Implicit Types κ : lft.
 
 (* Unfolding lemmas *)

theories/lifetime/model/faking.v

@@ -5,7 +5,7 @@ From iris.proofmode Require Import tactics.
 Set Default Proof Using "Type".
 
 Section faking.
-Context `{!invG Σ, !lftG Σ userE}.
+Context `{!invGS Σ, !lftG Σ userE}.
 Implicit Types κ : lft.
 
 Lemma ilft_create A I κ :

theories/lifetime/model/primitive.v

@@ -6,7 +6,7 @@ From iris.proofmode Require Import tactics.
 Set Default Proof Using "Type".
 Import uPred.
 
-Lemma lft_init `{!invG Σ, !lftPreG Σ} E userE :
+Lemma lft_init `{!invGS Σ, !lftPreG Σ} E userE :
   ↑lftN ⊆ E → ↑lftN ## userE → ⊢ |={E}=> ∃ _ : lftG Σ userE, lft_ctx.
 Proof.
   iIntros (? HuserE). rewrite /lft_ctx.
@@ -20,7 +20,7 @@ Proof.
 Qed.
 
 Section primitive.
-Context `{!invG Σ, !lftG Σ userE}.
+Context `{!invGS Σ, !lftG Σ userE}.
 Implicit Types κ : lft.
 
 Lemma to_borUR_included (B : gmap slice_name bor_state) i s q :

theories/lifetime/model/reborrow.v

@@ -5,7 +5,7 @@ From iris.proofmode Require Import tactics.
 Set Default Proof Using "Type".
 
 Section reborrow.
-Context `{!invG Σ, !lftG Σ userE}.
+Context `{!invGS Σ, !lftG Σ userE}.
 Implicit Types κ : lft.
 
 (* Notice that taking lft_inv for both κ and κ' already implies

theories/lifetime/na_borrow.v

@@ -3,7 +3,7 @@ From iris.base_logic.lib Require Export na_invariants.
 From iris.proofmode Require Import tactics.
 Set Default Proof Using "Type".
 
-Definition na_bor `{!invG Σ, !lftG Σ userE, !na_invG Σ}
+Definition na_bor `{!invGS Σ, !lftG Σ userE, !na_invG Σ}
            (κ : lft) (tid : na_inv_pool_name) (N : namespace) (P : iProp Σ) :=
   (∃ i, &{κ,i}P ∗ na_inv tid N (idx_bor_own 1 i))%I.
 
@@ -11,7 +11,7 @@ Notation "&na{ κ , tid , N }" := (na_bor κ tid N)
     (format "&na{ κ , tid , N }") : bi_scope.
 
 Section na_bor.
-  Context `{!invG Σ, !lftG Σ userE, !na_invG Σ}
+  Context `{!invGS Σ, !lftG Σ userE, !na_invG Σ}
           (tid : na_inv_pool_name) (N : namespace) (P : iProp Σ).
 
   Global Instance na_bor_ne κ n : Proper (dist n ==> dist n) (na_bor κ tid N).

theories/typing/lft_contexts.v

@@ -23,7 +23,7 @@ Notation llctx := (list llctx_elt).
 Notation "κ ⊑ₗ κl" := (@pair lft (list lft) κ κl) (at level 70).
 
 Section lft_contexts.
-  Context `{!invG Σ, !lftG Σ lft_userE}.
+  Context `{!invGS Σ, !lftG Σ lft_userE}.
   Implicit Type (κ : lft).
 
   (* External lifetime contexts. *)
@@ -415,7 +415,7 @@ Arguments lctx_lft_incl_incl_noend {_ _ _ _} _ _.
 Arguments lctx_lft_alive_tok {_ _ _ _ _} _ _ _.
 Arguments lctx_lft_alive_tok_noend {_ _ _ _ _} _ _ _.
 
-Lemma elctx_sat_submseteq `{!invG Σ, !lftG Σ lft_userE} E E' L :
+Lemma elctx_sat_submseteq `{!invGS Σ, !lftG Σ lft_userE} E E' L :
   E' ⊆+ E → elctx_sat E L E'.
 Proof. iIntros (HE' ??) "_ !> H". by iApply big_sepL_submseteq. Qed.