Adapt to #114

_CoqProject

@@ -1,7 +1,6 @@
 -Q src Perennial
 -arg -w -arg -ssr-search-moved
 -arg -w -arg +deprecated-instance-without-locality
--arg -w -arg -future-coercion-class-field
 # don't allow ambiguous coercions
 -arg -w -arg +ambiguous-paths
 -arg -w -arg +deprecated-hint-rewrite-without-locality

new/proof/asyncfile.v

@@ -18,12 +18,12 @@ Record af_names := mk_af_names {
 
 Class asyncfileG Σ :=
   AsyncFileG {
-    map_inG :> mapG Σ u64 ();
-    data_inG :> ghost_varG Σ (list u8);
-    tok_inG :> ghost_varG Σ ();
-    idx_ing :> ghost_varG Σ u64;
-    stagedG :> stagedG Σ ; (* for crash borrows? *)
-    syncG :> syncG Σ ;
+    #[global] map_inG :: mapG Σ u64 ();
+    #[global] data_inG :: ghost_varG Σ (list u8);
+    #[global] tok_inG :: ghost_varG Σ ();
+    #[global] idx_ing :: ghost_varG Σ u64;
+    #[global] stagedG :: stagedG Σ ; (* for crash borrows? *)
+    #[global] syncG :: syncG Σ ;
   }.
 
 Definition asyncfileΣ :=

new/proof/sync.v

@@ -12,8 +12,8 @@ From Perennial.algebra Require Import map.
 Set Default Proof Using "Type".
 
 Class syncG Σ := {
-    wg_tokG :> mapG Σ u64 unit;
-    wg_totalG :> ghost_varG Σ u64
+    #[global] wg_tokG :: mapG Σ u64 unit;
+    #[global] wg_totalG :: ghost_varG Σ u64
   }.
 
 Definition syncΣ := #[mapΣ u64 unit ; ghost_varΣ u64].

new/proof/vrsm/paxos/definitions.v

@@ -23,13 +23,13 @@ Implicit Type γ : paxos_system_names.
 Definition client_logR := dfrac_agreeR (leibnizO (list u8)).
 
 Class paxosG Σ := {
-    (* mp_ghostG :> mp_ghostG (EntryType:=(list u8 * iProp Σ)%type) Σ ; *)
-    paxos_ghostG :> mpaxosG (EntryType:=(list u8 * gname)%type) Σ ;
-    paxos_urpcG :> urpcregG Σ ;
-    paxos_wgG :> waitgroupG Σ ; (* for apply proof *)
-    paxos_logG :> inG Σ client_logR;
-    paxos_apply_escrow_tok :> ghost_varG Σ unit ;
-    paxos_asyncfile :> asyncfileG Σ ;
+    (* #[global] mp_ghostG :: mp_ghostG (EntryType:=(list u8 * iProp Σ)%type) Σ ; *)
+    #[global] paxos_ghostG :: mpaxosG (EntryType:=(list u8 * gname)%type) Σ ;
+    #[global] paxos_urpcG :: urpcregG Σ ;
+    #[global] paxos_wgG :: waitgroupG Σ ; (* for apply proof *)
+    #[global] paxos_logG :: inG Σ client_logR;
+    #[global] paxos_apply_escrow_tok :: ghost_varG Σ unit ;
+    #[global] paxos_asyncfile :: asyncfileG Σ ;
 }.
 
 Definition paxosΣ :=

src/algebra/append_list.v

@@ -11,7 +11,7 @@ Set Default Goal Selector "!".
 Set Default Proof Using "Type".
 
 Class alistG Σ A : Set :=
-  { alist_inG :> mapG Σ nat A; }.
+  { #[global] alist_inG :: mapG Σ nat A; }.
 
 Definition alistΣ A : gFunctors := #[ mapΣ nat A ].
 

src/algebra/async.v

@@ -10,8 +10,8 @@ From Perennial.algebra Require Import log_heap own_discrete.
 Set Default Proof Using "Type".
 
 Class asyncG Σ (K V: Type) `{Countable K, EqDecision V} := {
-  async_listG :> fmlistG (gmap K V) Σ;
-  async_mapG :> inG Σ (gmap_viewR K (agreeR natO));
+  #[global] async_listG :: fmlistG (gmap K V) Σ;
+  #[global] async_mapG :: inG Σ (gmap_viewR K (agreeR natO));
 }.
 
 Definition asyncΣ K V `{Countable K, EqDecision V} : gFunctors :=

src/algebra/atleast.v

@@ -305,7 +305,7 @@ Arguments MakeAtLeast {_} _ _%I _%I.
 #[global]
 Hint Mode MakeAtLeast + - - - : typeclass_instances.
 Class KnownMakeAtLeast {PROP : bi} k (P Q : PROP) :=
-  known_make_except_0 :> MakeAtLeast k P Q.
+  #[global] known_make_except_0 :: MakeAtLeast k P Q.
 Arguments KnownMakeAtLeast {_} _ _%I _%I.
 #[global]
 Hint Mode KnownMakeAtLeast + + ! - : typeclass_instances.

src/algebra/auth_map.v

@@ -36,7 +36,7 @@ Definition mapUR (K V: Type) `{Countable K}: ucmra :=
                   (agreeR (leibnizO V))).
 
 Class mapG Σ K V `{Countable K} :=
-  { map_inG :> inG Σ (authUR (mapUR K V)); }.
+  { #[global] map_inG :: inG Σ (authUR (mapUR K V)); }.
 
 Definition mapΣ K V `{Countable K} :=
   #[GFunctor (authR (mapUR K V))].

src/algebra/fmlist_map.v

@@ -7,7 +7,7 @@ From Perennial.program_proof Require Import proof_prelude.
 
 Section definitions.
 Class fmlist_mapG Σ K V `{Countable K} :=
-   { fmlist_map_inG :> inG Σ (gmapR K (mono_listR (leibnizO V))) }.
+   { #[global] fmlist_map_inG :: inG Σ (gmapR K (mono_listR (leibnizO V))) }.
 
 Definition fmlist_mapΣ K V `{Countable K} := #[GFunctor (gmapUR K (mono_listR (leibnizO V)))].
 

src/algebra/frac_count.v

@@ -17,7 +17,7 @@ Definition frac_countUR :=
   (optionUR (prodR fracR positiveR)).
 
 Class frac_countG Σ :=
-  { frac_count_inG :> inG Σ (authR frac_countUR) }.
+  { #[global] frac_count_inG :: inG Σ (authR frac_countUR) }.
 
 Definition frac_countΣ : gFunctors := #[GFunctor (authR frac_countUR)].
 #[global]

src/algebra/gen_dir.v

@@ -17,13 +17,13 @@ Definition to_gen_dir {L1 L2 V} `{Countable L1} `{Countable L2} :
 
 (** The CMRA we need. *)
 Class gen_dirG (L1 L2 V : Type) (Σ : gFunctors) `{Countable L1} `{Countable L2} := GenDirG {
-  gen_dir_inG :> inG Σ (authR (gen_dirUR L1 L2 V));
+  #[global] gen_dir_inG :: inG Σ (authR (gen_dirUR L1 L2 V));
   gen_dir_name : gname
 }.
 Arguments gen_dir_name {_ _ _ _ _ _ _ _} _ : assert.
 
 Class gen_dirPreG (L1 L2 V : Type) (Σ : gFunctors) `{Countable L1} `{Countable L2} :=
-  { gen_dir_preG_inG :> inG Σ (authR (gen_dirUR L1 L2 V)) }.
+  { #[global] gen_dir_preG_inG :: inG Σ (authR (gen_dirUR L1 L2 V)) }.
 
 Definition gen_dirΣ (L1 L2 V : Type) `{Countable L1} `{Countable L2} : gFunctors :=
   #[GFunctor (authR (gen_dirUR L1 L2 V))].

src/algebra/ghost_async_map.v

@@ -43,7 +43,7 @@ End async_rel.
 (** The CMRA we need. *)
 
 Class ghost_async_mapG Σ (K V : Type) `{Countable K, Countable V} := GhostMapG {
-  ghost_async_map_inG :> inG Σ (gmap_rel_viewR K (leibnizO (async V)) (leibnizO V) (gset V) async_rel);
+  #[global] ghost_async_map_inG :: inG Σ (gmap_rel_viewR K (leibnizO (async V)) (leibnizO V) (gset V) async_rel);
 }.
 Definition ghost_async_mapΣ (K V : Type) `{Countable K, Countable V} : gFunctors :=
   #[ GFunctor (gmap_rel_viewR K (leibnizO (async V)) _ _ async_rel) ].

src/algebra/map.v

@@ -5,7 +5,7 @@ From iris.proofmode Require Import proofmode.
 
 Section definitions.
 Class mapG Σ K V `{Countable K} :=
-  { map_inG:> inG Σ (gmapR K (dfrac_agreeR (leibnizO V)))} .
+  { #[global] map_inG :: inG Σ (gmapR K (dfrac_agreeR (leibnizO V)))} .
 
 Definition mapΣ K V `{Countable K} := #[GFunctor (gmapR K (dfrac_agreeR (leibnizO V)))].
 Global Instance subG_mapΣ K V `{Countable K} {Σ} : subG (mapΣ K V) Σ → (mapG Σ K V).

src/algebra/mlist.v

@@ -188,7 +188,7 @@ Global Arguments MList {_} _.
 
 Definition fmlistUR (A: Type) {Heq: EqDecision A} := authUR (mlistUR A).
 Class fmlistG (A: Type) {Heq: EqDecision A} Σ :=
-  { fmlist_inG :> inG Σ (fmlistUR A) }.
+  { #[global] fmlist_inG :: inG Σ (fmlistUR A) }.
 Definition fmlistΣ (A: Type) {Heq: EqDecision A} : gFunctors :=
   #[GFunctor (fmlistUR A)].
 

src/algebra/na_heap.v

@@ -33,10 +33,10 @@ Definition na_sizeUR (L: Type) `{Countable L} : ucmra :=
   gmapUR L (agreeR (leibnizO Z)).
 
 Class na_heapGS (L V: Type) Σ `{BlockAddr L} := Na_HeapG {
-  na_heap_inG :> inG Σ (na_heapUR L V);
-  na_size_inG :> inG Σ (authR (na_sizeUR Z));
-  na_meta_inG :> inG Σ (gmap_viewR L (agreeR gnameO));
-  na_meta_data_inG :> inG Σ (reservation_mapR (agreeR positiveO));
+  #[global] na_heap_inG :: inG Σ (na_heapUR L V);
+  #[global] na_size_inG :: inG Σ (authR (na_sizeUR Z));
+  #[global] na_meta_inG :: inG Σ (gmap_viewR L (agreeR gnameO));
+  #[global] na_meta_data_inG :: inG Σ (reservation_mapR (agreeR positiveO));
   na_heap_name : gname;
   na_size_name : gname;
   na_meta_name : gname
@@ -47,10 +47,10 @@ Arguments na_size_name {_ _ _ _ _ _} _ : assert.
 Arguments na_meta_name {_ _ _ _ _ _} _ : assert.
 
 Class na_heapGpreS (L V : Type) (Σ : gFunctors) `{BlockAddr L} := {
-  na_heap_preG_inG :> inG Σ (na_heapUR L V);
-  na_size_preG_inG :> inG Σ (authR (na_sizeUR Z));
-  na_meta_preG_inG :> inG Σ (gmap_viewR L (agreeR gnameO));
-  na_meta_data_preG_inG :> inG Σ (reservation_mapR (agreeR positiveO));
+  #[global] na_heap_preG_inG :: inG Σ (na_heapUR L V);
+  #[global] na_size_preG_inG :: inG Σ (authR (na_sizeUR Z));
+  #[global] na_meta_preG_inG :: inG Σ (gmap_viewR L (agreeR gnameO));
+  #[global] na_meta_data_preG_inG :: inG Σ (reservation_mapR (agreeR positiveO));
 }.
 
 Definition na_heapΣ (L V : Type) `{BlockAddr L} : gFunctors := #[

src/algebra/partition.v

@@ -7,11 +7,11 @@ Set Default Proof Using "Type".
 Import uPred.
 
 Class partitionG (L V: Type) (Σ: gFunctors) `{Countable L, Infinite L, Countable V, Infinite V} := {
-  partition_heap_inG :> gen_heapGS L (gset V) Σ;
+  #[global] partition_heap_inG :: gen_heapGS L (gset V) Σ;
 }.
 
 Class partition_preG (L V: Type) Σ `{Countable L, Infinite L, Countable V, Infinite V} := {
-  partition_heap_preG :> gen_heapGpreS L (gset V) Σ;
+  #[global] partition_heap_preG :: gen_heapGpreS L (gset V) Σ;
 }.
 
 

src/base_logic/lib/cancelable_invariants.v

@@ -5,7 +5,7 @@ From Perennial.base_logic.lib Require Export invariants.
 From iris.prelude Require Import options.
 Import uPred.
 
-Class cinvG Σ := cinv_inG :> inG Σ fracR.
+Class cinvG Σ := #[global] cinv_inG :: inG Σ fracR.
 Definition cinvΣ : gFunctors := #[GFunctor fracR].
 
 Global Instance subG_cinvΣ {Σ} : subG cinvΣ Σ → cinvG Σ.

src/base_logic/lib/crash_token.v

@@ -7,8 +7,8 @@ Definition crashR := csumR fracR (agreeR unitO).
 Definition NC_tok q : crashR := Cinl q.
 Definition C_tok : crashR := Cinr (to_agree ()).
 
-Class crashGS Σ := { crash_inG :> inG Σ crashR; crash_name : gname }.
-Class crashGpreS Σ := { crash_inPreG :> inG Σ crashR }.
+Class crashGS Σ := { #[global] crash_inG :: inG Σ crashR; crash_name : gname }.
+Class crashGpreS Σ := { #[global] crash_inPreG :: inG Σ crashR }.
 
 Definition crashΣ : gFunctors :=
     #[GFunctor (csumR fracR (agreeR unitO))].

src/base_logic/lib/frac_coPset.v

@@ -6,7 +6,7 @@ From Perennial.base_logic Require Export lib.own.
 From iris.proofmode Require Import tactics.
 
 Record frac_coPset :=
-  { fc_carrier :> @discrete_fun positive (fun _ => optionO fracR) }.
+  { #[global] fc_carrier :: @discrete_fun positive (fun _ => optionO fracR) }.
 
 Section ofe.
   Global Instance frac_coPset_equiv : Equiv (frac_coPset) := λ f g, (fc_carrier f) ≡ (fc_carrier g).

src/base_logic/lib/gmap_own.v

@@ -9,7 +9,7 @@ Set Default Proof Using "Type".
 Local Definition gmapR (K V : Type) `{Countable K} :=
   gmapUR K (prodR dfracR (agreeR (leibnizO V))).
 Class gmapG Σ (K V : Type) `{Countable K} :=
-   { gmap_inG :> inG Σ (gmapR K V) }.
+   { #[global] gmap_inG :: inG Σ (gmapR K V) }.
 Definition gmapΣ (K V : Type) `{Countable K} := #[GFunctor (gmapR K V)].
 
 Global Instance subG_gmapΣ {Σ} (K V  : Type) `{Countable K} :

src/base_logic/lib/wsat.v

@@ -41,18 +41,18 @@ Qed.
 
 Module invGS.
   Class invGpreS (Σ : gFunctors) : Set := WsatPreG {
-    inv_inPreG :> inG Σ (authR (gmapUR positive
+    #[global] inv_inPreG :: inG Σ (authR (gmapUR positive
                                     (prodR (agreeR (prodO (listO (laterO (iPropO Σ))) bi_schemaO))
                                            (optionR (prodR fracR (agreeR (listO (laterO (iPropO Σ)))))))));
-    enabled_inPreG :> inG Σ coPset_disjR;
-    disabled_inPreG :> inG Σ (gset_disjR positive);
-    mlist_inPreG :> fmlistG (invariant_level_names) Σ;
+    #[global] enabled_inPreG :: inG Σ coPset_disjR;
+    #[global] disabled_inPreG :: inG Σ (gset_disjR positive);
+    #[global] mlist_inPreG :: fmlistG (invariant_level_names) Σ;
     inv_lcPreG : lcGpreS Σ;
   }.
 
   Class invGS (Σ : gFunctors) : Set := WsatG {
-    inv_inG :> invGpreS Σ;
-    invGS_lc :> lcGS Σ;
+    #[global] inv_inG :: invGpreS Σ;
+    #[global] invGS_lc :: lcGS Σ;
     inv_list_name : gname;
     enabled_name : gname;
     disabled_name : gname;

src/goose_lang/adequacy.v

@@ -42,13 +42,13 @@ Hint Resolve subG_ffiPreG : typeclass_instances.
 Class gooseGpreS `{ext: ffi_syntax} `{EXT_SEM: !ffi_semantics ext ffi}
       `{INTERP: !ffi_interp ffi} `{!ffi_interp_adequacy} Σ
   := GooseGpreS {
-  goose_preG_iris :> invGpreS Σ;
-  goose_preG_crash :> crashGpreS Σ;
-  goose_preG_heap :> na_heapGpreS loc val Σ;
-  goose_preG_proph :> proph_mapGpreS proph_id val Σ;
-  goose_preG_ffi :> ffiGpreS Σ;
-  goose_preG_trace :> trace_preG Σ;
-  goose_preG_credit :> credit_preG Σ;
+  #[global] goose_preG_iris :: invGpreS Σ;
+  #[global] goose_preG_crash :: crashGpreS Σ;
+  #[global] goose_preG_heap :: na_heapGpreS loc val Σ;
+  #[global] goose_preG_proph :: proph_mapGpreS proph_id val Σ;
+  #[global] goose_preG_ffi :: ffiGpreS Σ;
+  #[global] goose_preG_trace :: trace_preG Σ;
+  #[global] goose_preG_credit :: credit_preG Σ;
 }.
 
 Ltac solve_inG_deep :=

src/goose_lang/ffi/append_log_ffi.v

@@ -189,15 +189,15 @@ Definition openR := csumR (prodR fracR (agreeR (leibnizO log_unopen_status))) (a
 Definition Log_Opened (l: loc) : openR := Cinr (to_agree l).
 
 Class logG Σ :=
-  { logG_open_inG :> inG Σ openR;
+  { #[gobal] logG_open_inG :: inG Σ openR;
     logG_open_name : gname;
-    logG_state_inG:> ghost_varG Σ (list disk.Block);
+    #[global] logG_state_inG :: ghost_varG Σ (list disk.Block);
     logG_state_name: gname;
   }.
 
 Class log_preG Σ :=
-  { logG_preG_open_inG :> inG Σ openR;
-    logG_preG_state_inG:> ghost_varG Σ (list disk.Block);
+  { #[global] logG_preG_open_inG :: inG Σ openR;
+    #[global] logG_preG_state_inG :: ghost_varG Σ (list disk.Block);
   }.
 
 Definition logΣ : gFunctors :=

src/goose_lang/ffi/async_disk.v

@@ -39,11 +39,11 @@ Lemma replicate_zero_to_block0 `{ext_ty: ext_types} :
 Proof. reflexivity. Qed.
 
 Class diskGS Σ : Set := DiskGS
-  { diskG_ghost_async_mapG :> ghost_async_mapG Σ Z Block ;
+  { #[global] diskG_ghost_async_mapG :: ghost_async_mapG Σ Z Block ;
     diskG_ghost_async_name : gname }.
 
 Class disk_preG Σ :=
-  { disk_preG_ghost_async_mapG :> ghost_async_mapG Σ Z Block }.
+  { #[global] disk_preG_ghost_async_mapG :: ghost_async_mapG Σ Z Block }.
 
 Definition diskΣ : gFunctors :=
   #[ghost_async_mapΣ Z Block].

src/goose_lang/ffi/async_disk_proph.v

@@ -48,10 +48,10 @@ Lemma replicate_zero_to_block0 `{ext_ty: ext_types} :
 Proof. reflexivity. Qed.
 
 Class diskGS Σ : Set := DiskGS
-  { diskG_gen_heapG :> gen_heap.gen_heapGS Z CrashBlock Σ; }.
+  { #[global] diskG_gen_heapG :: gen_heap.gen_heapGS Z CrashBlock Σ; }.
 
 Class disk_preG Σ :=
-  { disk_preG_gen_heapG :> gen_heap.gen_heapGpreS Z CrashBlock Σ; }.
+  { #[global] disk_preG_gen_heapG :: gen_heap.gen_heapGpreS Z CrashBlock Σ; }.
 
 Definition diskΣ : gFunctors :=
   #[gen_heapΣ Z CrashBlock].

src/goose_lang/ffi/disk_ffi/specs.v

@@ -18,11 +18,11 @@ usually written *)
 Set Printing Projections.
 
 Class diskGS Σ : Set := DiskGS
-  { diskG_gen_heapG :> gen_heap.gen_heapGS Z Block Σ; }.
+  { #[global] diskG_gen_heapG :: gen_heap.gen_heapGS Z Block Σ; }.
 
 
 Class disk_preG Σ : Set :=
-  { disk_preG_gen_heapG :> gen_heap.gen_heapGpreS Z Block Σ; }.
+  { #[global] disk_preG_gen_heapG :: gen_heap.gen_heapGpreS Z Block Σ; }.
 
 Definition diskΣ : gFunctors :=
   #[gen_heapΣ Z Block].

src/goose_lang/ffi/grove_ffi/grove_ffi.v

@@ -19,20 +19,20 @@ Set Printing Projections.
 
 (** * Grove semantic interpretation and lifting lemmas *)
 Class groveGS Σ : Set := GroveGS {
-  groveG_net_heapG :> gen_heap.gen_heapGS chan (gset message) Σ;
+  #[global] groveG_net_heapG :: gen_heap.gen_heapGS chan (gset message) Σ;
   grove_time_name : gname;
-  groveG_timeG :> mono_natG Σ;
+  #[global] groveG_timeG :: mono_natG Σ;
 }.
 
 Class groveGpreS Σ : Set := {
-  grove_preG_net_heapG :> gen_heap.gen_heapGpreS chan (gset message) Σ;
-  grove_preG_files_heapG :> gen_heap.gen_heapGpreS string (list byte) Σ;
-  grove_preG_tscG :> mono_natG Σ;
+  #[global] grove_preG_net_heapG :: gen_heap.gen_heapGpreS chan (gset message) Σ;
+  #[global] grove_preG_files_heapG :: gen_heap.gen_heapGpreS string (list byte) Σ;
+  #[global] grove_preG_tscG :: mono_natG Σ;
 }.
 Class groveNodeGS Σ : Set := GroveNodeGS {
-  groveG_preS :> groveGpreS Σ;
+  #[global] groveG_preS :: groveGpreS Σ;
   grove_tsc_name : gname;
-  groveG_files_heapG :> gen_heap.gen_heapGS string (list byte) Σ;
+  #[global] groveG_files_heapG :: gen_heap.gen_heapGS string (list byte) Σ;
 }.
 
 Definition groveΣ : gFunctors :=