From 68d7971acf3871d6a1eeb7372425f1b4b529fa0e Mon Sep 17 00:00:00 2001 From: Travis Hance Date: Wed, 12 Feb 2025 16:51:38 +0100 Subject: [PATCH] use invGS_gen --- src/examples/counting.v | 2 +- src/examples/forever.v | 2 +- src/examples/fractional.v | 2 +- src/examples/hash_table_logic.v | 2 +- src/guarding/guard_later_pers.v | 2 +- src/guarding/lib/cancellable.v | 2 +- src/guarding/lib/lifetime.v | 6 +++--- src/guarding/lib/non_atomic_map.v | 2 +- src/guarding/lib/rwlock.v | 2 +- src/guarding/storage_protocol/protocol.v | 2 +- src/guarding/tactics.v | 4 ++-- 11 files changed, 14 insertions(+), 14 deletions(-) diff --git a/src/examples/counting.v b/src/examples/counting.v index 65d6293..7373e42 100644 --- 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 index efd928e..bf2b7b9 100644 --- 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 index 2cabf00..f8ecd48 100644 --- 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 index 5b723c6..c73d4dd 100644 --- 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 index cd80cd5..3d5c667 100644 --- 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 index 238d015..452816f 100644 --- 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 index 0c11ba1..385930b 100644 --- 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 index e584131..42bc1e2 100644 --- 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 index b28f502..9cbfbdd 100644 --- 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 index 59bbce2..84e3451 100644 --- 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 index ec370bd..1d5fad1 100644 --- 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).