use invGS_gen

secure-foundations · Feb 12, 2025 · 68d7971 · 68d7971
1 parent 5eb5f70
commit 68d7971
Show file tree

Hide file tree

Showing 11 changed files with 14 additions and 14 deletions.
diff --git a/src/examples/counting.v b/src/examples/counting.v
@@ -107,7 +107,7 @@ Section Counting.
 
 Context {Σ: gFunctors}.
 Context `{co_in_Σ: !@co_logicG Σ}.
-Context `{!invGS Σ}.
+Context `{!invGS_gen hlc Σ}.
 
 Fixpoint sep_pow (n: nat) (P: iProp Σ) : iProp Σ :=
   match n with

diff --git a/src/examples/forever.v b/src/examples/forever.v
@@ -147,7 +147,7 @@ Section Forever.
 
 Context {Σ: gFunctors}.
 Context `{f_in_Σ: @forever_logicG Σ}.
-Context `{!invGS Σ}.
+Context `{!invGS_gen hlc Σ}.
 
 Definition family (Q: iProp Σ) (e: Exc ()) : iProp Σ :=
   match e with

diff --git a/src/examples/fractional.v b/src/examples/fractional.v
@@ -348,7 +348,7 @@ Proof. solve_inG. Qed.
 Section Frac.
   Context {Σ: gFunctors}.
   Context `{@frac_logicG Σ}.
-  Context `{!invGS Σ}.
+  Context `{!invGS_gen hlc Σ}.
 
   Definition sto_frac (γ: gname) (Q: iProp Σ) := sp_sto (sp_i := frac_sp_inG) γ (family Q).
   Definition own_frac (γ: gname) (qp: Qp) := sp_own (sp_i := frac_sp_inG) γ (Some qp).

diff --git a/src/examples/hash_table_logic.v b/src/examples/hash_table_logic.v
@@ -66,7 +66,7 @@ Section HashTableLogic.
 
 Context {Σ: gFunctors}.
 Context {htl: ht_logicG Σ}.
-Context `{!invGS Σ}. 
+Context `{!invGS_gen hlc Σ}.
 
 Lemma ht_Init (n: nat) :
   ⊢ |==> (∃ γ , own γ (mseq n) ∗ own γ (sseq ht_fixed_size))%I.

diff --git a/src/guarding/guard_later_pers.v b/src/guarding/guard_later_pers.v
@@ -72,7 +72,7 @@ Proof.
 Qed.
 
 Context {Σ: gFunctors}.
-Context `{!invGS Σ}. 
+Context `{!invGS_gen hlc Σ}. 
 
 (* Later-Pers-Guard *)
 

diff --git a/src/guarding/lib/cancellable.v b/src/guarding/lib/cancellable.v
@@ -29,7 +29,7 @@ Section CancellableInvariants.
 
   Context {Σ: gFunctors}.
   Context `{!ecInv_logicG Σ}.
-  Context `{!invGS Σ}.
+  Context `{!invGS_gen hlc Σ}.
 
   Definition Active (γ: gname) : iProp Σ := own γ (Excl ()).
 

diff --git a/src/guarding/lib/lifetime.v b/src/guarding/lib/lifetime.v
@@ -147,7 +147,7 @@ Qed.
 Section LlftHelperResources.
   Context {Σ: gFunctors}.
   Context `{!llft_logicGpreS Σ}.
-  Context `{!invGS Σ}.
+  Context `{!invGS_gen hlc Σ}.
 
   (* begin hide *)
 
@@ -538,7 +538,7 @@ End LlftHelperResources.
 Section LlftLogic.
   Context {Σ: gFunctors}.
   Context `{!llft_logicGS Σ}.
-  Context `{!invGS Σ}.
+  Context `{!invGS_gen hlc Σ}.
 
   (*** Lifetime logic ***)
 
@@ -867,7 +867,7 @@ Section LlftLogic.
   Qed.
 End LlftLogic.
 
-Lemma llft_alloc {Σ: gFunctors} `{!llft_logicGpreS Σ} `{!invGS Σ} E
+Lemma llft_alloc {Σ: gFunctors} `{!llft_logicGpreS Σ} `{!invGS_gen hlc Σ} E
   : ⊢ |={E}=> ∃ _ : llft_logicGS Σ, llft_ctx.
 Proof.
   iIntros. iMod lt_alloc as (γ) "J".

diff --git a/src/guarding/lib/non_atomic_map.v b/src/guarding/lib/non_atomic_map.v
@@ -285,7 +285,7 @@ Section NonAtomicMap.
 
   Context {Σ: gFunctors}.
   Context `{!na_logicG L V Σ}.
-  Context `{!invGS Σ}. 
+  Context `{!invGS_gen hlc Σ}. 
 
   Implicit Types (γ: gname) (l: L) (v: V).
   Implicit Types (G: iProp Σ).

diff --git a/src/guarding/lib/rwlock.v b/src/guarding/lib/rwlock.v
@@ -354,7 +354,7 @@ Context {eqdec: EqDecision S}.
 
 Context {Σ: gFunctors}.
 Context `{@rwlock_logicG S _ Σ}.
-Context `{!invGS Σ}.
+Context `{!invGS_gen hlc Σ}.
 
 Definition fields γ (e: bool) (r: Z) (x: S) : iProp Σ
     := sp_own (sp_i := rwlock_sp_inG) γ (Central e r x).

diff --git a/src/guarding/storage_protocol/protocol.v b/src/guarding/storage_protocol/protocol.v
@@ -366,7 +366,7 @@ Section StorageLogic.
 
   Context {Σ: gFunctors}.
   Context `{sp_i: !sp_logicG storage_mixin Σ}.
-  Context `{!invGS Σ}.
+  Context `{!invGS_gen hlc Σ}.
 
   Definition sp_sto (γ: gname) (f: B → iProp Σ) : iProp Σ :=
       ⌜ wf_prop_map f ⌝ ∗

diff --git a/src/guarding/tactics.v b/src/guarding/tactics.v
@@ -4,7 +4,7 @@ From iris.prelude Require Import options.
 Section TacticsHelpers.
 
 Context {Σ: gFunctors}.
-Context `{!invGS_gen hlc Σ}. 
+Context `{!invGS_gen hlc Σ}.
 
 Local Lemma guard_weaken_helper_right (A B C : iProp Σ) (E: coPset) (n: nat)
     : (A &&{E; n}&&> B) -∗ (B &&{E}&&> C) -∗ (A &&{E; n}&&> C).
@@ -133,7 +133,7 @@ Tactic Notation "leaf_open_laters" constr(g) "with" constr(sel) "as" constr(pat)
 Section TacticsTests.
 
 Context {Σ: gFunctors}.
-Context `{!invGS Σ}. 
+Context `{!invGS_gen hlc Σ}.
 
 Local Lemma test_leaf_hyp (A B C D : iProp Σ) E
     : (A &&{∅ ; 3}&&> B ∗ C) ⊢ (A ∗ D &&{E ; 20}&&> B).