Opsem for attestation instructions and skeleton for WP of EStoreId (#24)

* First draft of opsem of attestation instructions * Continue EInit: modify sweep * WIP: opsem of EInit * Some more thoughts on EInit * Finish opsem (needs cleanup) * WIP fixing opsem... * Finish opsem, lemmas missing * Prove atomicity of opsem * Fix proofs * Comment out WP proofs of einstrs * Update comments * Opsem simplification * Fix opsem IsUnique * Fix opsem TEE * Fix compilation * Hash function as machines parameters WIP * Change fresh_eid * Fix measure function * Update TIndex and ENum to be Nat, simplify ETable: TIndex -> EId only * WIP WP rule for EStoreId * WIP state interp * Cleanup * memG,regG,enclaveG -> ceriseG + fix compilation up-to fundamental + fix wp estoreid * einit: Uncomment writing seal/unseal pair to b' * einit: no W perm for code cap, no X perm for data cap * Cleanup: remove spurious comments * Rename EId -> EIdentity * Fix build * Fix the rule EStoreId --------- Co-authored-by: June Rousseau <[email protected]>
logsem · Dec 20, 2024 · eea2296 · eea2296
1 parent c90774e
commit eea2296
Show file tree

Hide file tree

Showing 106 changed files with 754 additions and 398 deletions.
diff --git a/tests/proofmode_focus_block.v b/tests/proofmode_focus_block.v
@@ -6,7 +6,7 @@ Definition i1 `{MP: MachineParameters} := encodeInstrsW [ Mov r_t2 1; Mov r_t2 0
 Definition i2 `{MP: MachineParameters} := encodeInstrsW [ Mov r_t3 1; Mov r_t3 0 ].
 Definition l2 `{MP: MachineParameters} := i1 ++ i2.
 
-Lemma foo {Σ:gFunctors} {memg:memG Σ} {regg:regG Σ} `{MP: MachineParameters} p b e a :
+Lemma foo {Σ:gFunctors} {ceriseg:ceriseG Σ} `{MP: MachineParameters} p b e a :
   {{{ ⌜ExecPCPerm p ∧ SubBounds b e a (a ^+ length (l1 ++ l2))%a⌝
       ∗ codefrag a (l1 ++ l2)
       ∗ PC ↦ᵣ WCap (p,b,e,(a ^+ length l1)%a) }}}

diff --git a/theories/cap_lang.v b/theories/cap_lang.v
diff --git a/theories/examples/adder.v b/theories/examples/adder.v
@@ -5,7 +5,7 @@ From cap_machine Require Import rules logrel macros fundamental.
 From cap_machine.proofmode Require Import tactics_helpers.
 
 Section adder.
-  Context {Σ:gFunctors} {memg:memG Σ} {regg:regG Σ} {sealsg: sealStoreG Σ}
+  Context {Σ:gFunctors} {ceriseg:ceriseG Σ} {sealsg: sealStoreG Σ}
           {nainv: logrel_na_invs Σ}
           `{MP: MachineParameters}.
 

diff --git a/theories/examples/arch_sealing.v b/theories/examples/arch_sealing.v
@@ -10,7 +10,7 @@ Import uPred. (* exist_persistent *)
 
 (* Architectural variant of the sealing/unsealing functionality in the dynamic_sealing file. *)
 Section sealing.
-  Context {Σ:gFunctors} {memg:memG Σ} {regg:regG Σ} {seals:sealStoreG Σ}
+  Context {Σ:gFunctors} {ceriseg:ceriseG Σ} {seals:sealStoreG Σ}
           {nainv: logrel_na_invs Σ}
           `{MP: MachineParameters} .
 

diff --git a/theories/examples/assert.v b/theories/examples/assert.v
@@ -7,7 +7,7 @@ From cap_machine Require Import logrel addr_reg_sample fundamental rules proofmo
 (* Maintains a flag storing whether an assert has failed. *)
 
 Section Assert.
-  Context {Σ:gFunctors} {memg:memG Σ} {regg:regG Σ}
+  Context {Σ:gFunctors} {ceriseg:ceriseG Σ}
           {nainv: logrel_na_invs Σ}
           `{MP: MachineParameters}.
 

diff --git a/theories/examples/buffer.v b/theories/examples/buffer.v
@@ -8,7 +8,7 @@ From cap_machine Require Import proofmode.
 Open Scope Z_scope.
 
 Section buffer.
-  Context {Σ:gFunctors} {memg:memG Σ} {regg:regG Σ} {seals:sealStoreG Σ}
+  Context {Σ:gFunctors} {ceriseg:ceriseG Σ} {seals:sealStoreG Σ}
           `{MP: MachineParameters}.
 
   Definition buffer_code (off: Z) : list LWord :=

diff --git a/theories/examples/call.v b/theories/examples/call.v
@@ -4,7 +4,7 @@ From cap_machine Require Import logrel macros rules.
 From cap_machine.proofmode Require Import tactics_helpers proofmode.
 
 Section call.
-  Context {Σ:gFunctors} {memg:memG Σ} {regg:regG Σ}
+  Context {Σ:gFunctors} {ceriseg:ceriseG Σ}
           {nainv: logrel_na_invs Σ}
           `{MP: MachineParameters}.
 

diff --git a/theories/examples/callback.v b/theories/examples/callback.v
@@ -5,7 +5,7 @@ From cap_machine Require Import rules logrel macros call.
 From cap_machine.proofmode Require Import tactics_helpers.
 
 Section callback.
-  Context {Σ:gFunctors} {memg:memG Σ} {regg:regG Σ} {sealsg: sealStoreG Σ}
+  Context {Σ:gFunctors} {ceriseg:ceriseG Σ} {sealsg: sealStoreG Σ}
           {nainv: logrel_na_invs Σ}
           `{MP: MachineParameters}.
 

diff --git a/theories/examples/counter/counter.v b/theories/examples/counter/counter.v
@@ -5,7 +5,7 @@ From cap_machine Require Import rules logrel macros fundamental.
 From cap_machine.proofmode Require Import tactics_helpers.
 
 Section counter.
-  Context {Σ:gFunctors} {memg:memG Σ} {regg:regG Σ} {sealsg: sealStoreG Σ}
+  Context {Σ:gFunctors} {ceriseg:ceriseG Σ} {sealsg: sealStoreG Σ}
           {nainv: logrel_na_invs Σ}
           `{MP: MachineParameters}.
 

diff --git a/theories/examples/counter/counter_preamble.v b/theories/examples/counter/counter_preamble.v
@@ -9,7 +9,7 @@ From cap_machine.proofmode Require Import tactics_helpers.
 From stdpp Require Import countable.
 
 Section counter_example_preamble.
-  Context {Σ:gFunctors} {memg:memG Σ} {regg:regG Σ} {sealsg: sealStoreG Σ}
+  Context {Σ:gFunctors} {ceriseg:ceriseG Σ} {sealsg: sealStoreG Σ}
           {nainv: logrel_na_invs Σ}
           `{MP: MachineParameters}.
 

diff --git a/theories/examples/counter_binary/counter_binary.v b/theories/examples/counter_binary/counter_binary.v
@@ -7,7 +7,7 @@ From cap_machine.proofmode Require Import tactics_helpers.
 
 
 Section counter.
-  Context {Σ:gFunctors} {memg:memG Σ} {regg:regG Σ}
+  Context {Σ:gFunctors} {ceriseg:ceriseG Σ}
           {nainv: logrel_na_invs Σ} {cfg : cfgSG Σ}
           `{MP: MachineParameters}.
 

diff --git a/theories/examples/counter_binary/counter_binary_preamble.v b/theories/examples/counter_binary/counter_binary_preamble.v
@@ -9,7 +9,7 @@ From cap_machine.examples.counter_binary Require Import counter_binary counter_b
 From stdpp Require Import countable.
 
 Section counter_example_preamble.
-  Context {Σ:gFunctors} {memg:memG Σ} {regg:regG Σ}
+  Context {Σ:gFunctors} {ceriseg:ceriseG Σ}
           {nainv: logrel_na_invs Σ} {cfg : cfgSG Σ}
           `{MP: MachineParameters}.
 

diff --git a/theories/examples/counter_binary/counter_binary_preamble_def.v b/theories/examples/counter_binary/counter_binary_preamble_def.v
@@ -9,7 +9,7 @@ From cap_machine.examples.counter_binary Require Import counter_binary.
 From stdpp Require Import countable.
 
 Section counter_example_preamble.
-  Context {Σ:gFunctors} {memg:memG Σ} {regg:regG Σ}
+  Context {Σ:gFunctors} {ceriseg:ceriseG Σ}
           {nainv: logrel_na_invs Σ} {cfg : cfgSG Σ}
           `{MP: MachineParameters}.
 

diff --git a/theories/examples/counter_binary/counter_binary_preamble_left.v b/theories/examples/counter_binary/counter_binary_preamble_left.v
@@ -9,7 +9,7 @@ From cap_machine.examples.counter_binary Require Import counter_binary counter_b
 From stdpp Require Import countable.
 
 Section counter_example_preamble.
-  Context {Σ:gFunctors} {memg:memG Σ} {regg:regG Σ}
+  Context {Σ:gFunctors} {ceriseg:ceriseG Σ}
           {nainv: logrel_na_invs Σ} {cfg : cfgSG Σ}
           `{MP: MachineParameters}.
 

diff --git a/theories/examples/dynamic_sealing.v b/theories/examples/dynamic_sealing.v
@@ -8,7 +8,7 @@ From cap_machine.proofmode Require Import tactics_helpers solve_pure proofmode c
 
 Section sealing.
 
-  Context {Σ:gFunctors} {memg:memG Σ} {regg:regG Σ}
+  Context {Σ:gFunctors} {ceriseg:ceriseG Σ}
           {nainv: logrel_na_invs Σ}
           `{MP: MachineParameters}
           {seals:sealStoreG Σ}

diff --git a/theories/examples/enclaves/trusted_compute.v b/theories/examples/enclaves/trusted_compute.v
@@ -8,7 +8,7 @@ From cap_machine Require Import macros_new.
 Open Scope Z_scope.
 
 Section trusted_compute_example.
-  Context {Σ:gFunctors} {memg:memG Σ} {regg:regG Σ} {sealsg : sealStoreG Σ} `{MP: MachineParameters}.
+  Context {Σ:gFunctors} {ceriseg:ceriseG Σ} {sealsg : sealStoreG Σ} `{MP: MachineParameters}.
 
   (* Data part, following the directly the main code *)
   Definition trusted_compute_data (linking_table_cap : LWord) : list LWord :=

diff --git a/theories/examples/interval/interval.v b/theories/examples/interval/interval.v
@@ -11,7 +11,7 @@ Notation "a ↪ₐ w" := (mapsto (L:=Addr) (V:=Word) a DfracDiscarded w) (at lev
 
 Section interval.
 
-  Context {Σ:gFunctors} {memg:memG Σ} {regg:regG Σ} {seals:sealStoreG Σ}
+  Context {Σ:gFunctors} {ceriseg:ceriseG Σ} {seals:sealStoreG Σ}
           {nainv: logrel_na_invs Σ} (* `{intg: intervalG Σ} *)
           `{MP: MachineParameters}
           {mono : sealLLG Σ}.

diff --git a/theories/examples/interval/interval_client.v b/theories/examples/interval/interval_client.v
@@ -8,7 +8,7 @@ From cap_machine.examples.interval Require Import interval interval_closure.
 From cap_machine Require Import contiguous tactics_helpers solve_pure proofmode map_simpl.
 
 Section interval_client.
-  Context {Σ:gFunctors} {memg:memG Σ} {regg:regG Σ} {sealg: sealStoreG Σ}
+  Context {Σ:gFunctors} {ceriseg:ceriseG Σ} {sealg: sealStoreG Σ}
           {nainv: logrel_na_invs Σ} {sealG: sealLLG Σ}
           `{MP: MachineParameters}.
 

diff --git a/theories/examples/interval/interval_client_adequacy.v b/theories/examples/interval/interval_client_adequacy.v
@@ -355,7 +355,7 @@ Proof.
 Qed.
 
 Section int_client_adequacy.
-  Context {Σ:gFunctors} {memg:memG Σ} {regg:regG Σ} {sealg:sealStoreG Σ}
+  Context {Σ:gFunctors} {ceriseg:ceriseG Σ} {sealg:sealStoreG Σ}
           {nainv: logrel_na_invs Σ} {sealLLG: keylist.sealLLG Σ}
           `{memlayout: memory_layout}.
 

diff --git a/theories/examples/interval/interval_client_closure.v b/theories/examples/interval/interval_client_closure.v
@@ -9,7 +9,7 @@ From cap_machine.proofmode Require Import
   contiguous tactics_helpers solve_pure proofmode map_simpl.
 
 Section interval_client.
-  Context {Σ:gFunctors} {memg:memG Σ} {regg:regG Σ} {sealg : sealStoreG Σ}
+  Context {Σ:gFunctors} {ceriseg:ceriseG Σ} {sealg : sealStoreG Σ}
           {nainv: logrel_na_invs Σ} {sealG: sealLLG Σ}
           `{MP: MachineParameters}.
 

diff --git a/theories/examples/interval/interval_closure.v b/theories/examples/interval/interval_closure.v
@@ -8,7 +8,7 @@ From cap_machine.examples Require Import dynamic_sealing keylist malloc.
 From cap_machine.examples.interval Require Import interval.
 
 Section interval_closure.
-  Context {Σ:gFunctors} {memg:memG Σ} {regg:regG Σ}
+  Context {Σ:gFunctors} {ceriseg:ceriseG Σ}
           {nainv: logrel_na_invs Σ} {sealG: sealLLG Σ}
           `{MP: MachineParameters}.
 

diff --git a/theories/examples/interval_arch/interval_arch.v b/theories/examples/interval_arch/interval_arch.v
@@ -11,7 +11,7 @@ Notation "a ↪ₐ w" := (mapsto (L:=Addr) (V:=Word) a DfracDiscarded w) (at lev
 
 Section interval.
 
-  Context {Σ:gFunctors} {memg:memG Σ} {regg:regG Σ} {seals:sealStoreG Σ}
+  Context {Σ:gFunctors} {ceriseg:ceriseG Σ} {seals:sealStoreG Σ}
           {nainv: logrel_na_invs Σ} (* `{intg: intervalG Σ} *)
           `{MP: MachineParameters}.
 

diff --git a/theories/examples/interval_arch/interval_client_adequacy_arch.v b/theories/examples/interval_arch/interval_client_adequacy_arch.v
@@ -395,7 +395,7 @@ Proof.
 Qed.
 
 Section int_client_adequacy.
-  Context {Σ:gFunctors} {memg:memG Σ} {regg:regG Σ} {sealg:sealStoreG Σ}
+  Context {Σ:gFunctors} {ceriseg:ceriseG Σ} {sealg:sealStoreG Σ}
           {nainv: logrel_na_invs Σ}
           `{memlayout: memory_layout}.
 

diff --git a/theories/examples/interval_arch/interval_client_arch.v b/theories/examples/interval_arch/interval_client_arch.v
@@ -9,7 +9,7 @@ From cap_machine.examples Require Import arch_sealing malloc.
 From cap_machine.examples.interval_arch Require Import interval_arch interval_closure_arch.
 
 Section interval_client.
-  Context {Σ:gFunctors} {memg:memG Σ} {regg:regG Σ} {sealg: sealStoreG Σ}
+  Context {Σ:gFunctors} {ceriseg:ceriseG Σ} {sealg: sealStoreG Σ}
           {nainv: logrel_na_invs Σ}
           `{MP: MachineParameters}.
 

diff --git a/theories/examples/interval_arch/interval_client_closure_arch.v b/theories/examples/interval_arch/interval_client_closure_arch.v
@@ -9,7 +9,7 @@ From cap_machine.examples Require Import arch_sealing malloc.
 From cap_machine.examples.interval_arch Require Import interval_arch interval_closure_arch interval_client_arch.
 
 Section interval_client.
-  Context {Σ:gFunctors} {memg:memG Σ} {regg:regG Σ} {sealg : sealStoreG Σ}
+  Context {Σ:gFunctors} {ceriseg:ceriseG Σ} {sealg : sealStoreG Σ}
           {nainv: logrel_na_invs Σ}
           `{MP: MachineParameters}.
 

diff --git a/theories/examples/interval_arch/interval_closure_arch.v b/theories/examples/interval_arch/interval_closure_arch.v
@@ -9,7 +9,7 @@ From cap_machine.examples Require Import arch_sealing malloc.
 From cap_machine.examples.interval_arch Require Import interval_arch.
 
 Section interval_closure.
-  Context {Σ:gFunctors} {memg:memG Σ} {regg:regG Σ} {seals:sealStoreG Σ}
+  Context {Σ:gFunctors} {ceriseg:ceriseG Σ} {seals:sealStoreG Σ}
           {nainv: logrel_na_invs Σ}
           `{MP: MachineParameters}.
 

diff --git a/theories/examples/isunique_example.v b/theories/examples/isunique_example.v
@@ -7,7 +7,7 @@ From cap_machine Require Import proofmode.
 Open Scope Z_scope.
 
 Section reclaim_buffer_example.
-  Context {Σ:gFunctors} {memg:memG Σ} {regg:regG Σ} {seals:sealStoreG Σ}
+  Context {Σ:gFunctors} {ceriseg:ceriseG Σ} {seals:sealStoreG Σ}
           `{MP: MachineParameters}.
 
   Definition reclaim_buffer_code : list LWord :=

diff --git a/theories/examples/keylist.v b/theories/examples/keylist.v
@@ -10,7 +10,7 @@ Definition prefR (al al' : addrwordLO) := al `prefix_of` al'.
 Class sealLLG Σ := CCounterG { ccounter_inG :: inG Σ (authUR (monotoneUR prefR)) }.
 
 Section list.
-  Context {Σ:gFunctors} {memg:memG Σ} {regg:regG Σ} {seals:sealStoreG Σ}
+  Context {Σ:gFunctors} {ceriseg:ceriseG Σ} {seals:sealStoreG Σ}
           {nainv: logrel_na_invs Σ}
           `{MP: MachineParameters}
           {mono : sealLLG Σ}.

diff --git a/theories/examples/lse.v b/theories/examples/lse.v
@@ -4,7 +4,7 @@ From cap_machine Require Import rules logrel macros fundamental call callback.
 From cap_machine.proofmode Require Import tactics_helpers.
 
 Section roe.
-  Context {Σ:gFunctors} {memg:memG Σ} {regg:regG Σ} {sealsg: sealStoreG Σ}
+  Context {Σ:gFunctors} {ceriseg:ceriseG Σ} {sealsg: sealStoreG Σ}
           {nainv: logrel_na_invs Σ}
           `{MP: MachineParameters}.
 

diff --git a/theories/examples/lse_adequacy.v b/theories/examples/lse_adequacy.v
@@ -163,7 +163,7 @@ Next Obligation.
 Qed.
 
 Section roe_adequacy.
-  Context {Σ:gFunctors} {memg:memG Σ} {regg:regG Σ} {sealsg: sealStoreG Σ}
+  Context {Σ:gFunctors} {ceriseg:ceriseG Σ} {sealsg: sealStoreG Σ}
           {nainv: logrel_na_invs Σ}
           `{memlayout: memory_layout}.
 

diff --git a/theories/examples/macros.v b/theories/examples/macros.v
@@ -6,7 +6,7 @@ From cap_machine.proofmode Require Import tactics_helpers map_simpl solve_pure.
 From cap_machine Require Export iris_extra addr_reg_sample contiguous malloc assert.
 
 Section macros.
-  Context {Σ:gFunctors} {memg:memG Σ} {regg:regG Σ}
+  Context {Σ:gFunctors} {ceriseg:ceriseG Σ}
           {nainv: logrel_na_invs Σ}
           `{MP: MachineParameters}.
 

diff --git a/theories/examples/macros_binary.v b/theories/examples/macros_binary.v
@@ -20,7 +20,7 @@ Ltac iEpilogue_s :=
    iSimpl in "Hj".
 
 Section macros.
-  Context {Σ:gFunctors} {memg:memG Σ} {regg:regG Σ}
+  Context {Σ:gFunctors} {ceriseg:ceriseG Σ}
           {nainv: logrel_na_invs Σ} {cfg : cfgSG Σ}
           `{MP: MachineParameters}.
 

diff --git a/theories/examples/macros_new.v b/theories/examples/macros_new.v
@@ -6,7 +6,7 @@ From cap_machine Require Export iris_extra addr_reg_sample contiguous malloc sal
 From cap_machine.proofmode Require Import classes tactics_helpers solve_pure proofmode map_simpl.
 
 Section macros.
-  Context {Σ:gFunctors} {memg:memG Σ} {regg:regG Σ} {seals:sealStoreG Σ}
+  Context {Σ:gFunctors} {ceriseg:ceriseG Σ} {seals:sealStoreG Σ}
           {nainv: logrel_na_invs Σ}
           `{MP: MachineParameters}.
 

diff --git a/theories/examples/malloc.v b/theories/examples/malloc.v
@@ -17,7 +17,7 @@ From cap_machine Require Import logrel addr_reg_sample fundamental rules proofmo
    studies. *)
 
 Section SimpleMalloc.
-  Context {Σ:gFunctors} {memg:memG Σ} {regg:regG Σ} {sealsg: sealStoreG Σ}
+  Context {Σ:gFunctors} {ceriseg:ceriseG Σ} {sealsg: sealStoreG Σ}
           {nainv: logrel_na_invs Σ}
           `{MP: MachineParameters}.
 

diff --git a/theories/examples/malloc_binary.v b/theories/examples/malloc_binary.v
@@ -7,7 +7,7 @@ From cap_machine Require Import iris_extra logrel_binary fundamental_binary.
 From cap_machine.rules Require Import rules_base.
 
 Section SimpleMalloc.
-  Context {Σ:gFunctors} {memg:memG Σ} {regg:regG Σ}
+  Context {Σ:gFunctors} {ceriseg:ceriseG Σ}
           {nainv: logrel_na_invs Σ} {cfg : cfgSG Σ}
           `{MP: MachineParameters}.
 

diff --git a/theories/examples/minimal_counter.v b/theories/examples/minimal_counter.v
@@ -7,7 +7,7 @@ From cap_machine Require Import proofmode.
 Open Scope Z_scope.
 
 Section counter.
-  Context {Σ:gFunctors} {memg:memG Σ} {regg:regG Σ} {sealg:sealStoreG Σ}
+  Context {Σ:gFunctors} {ceriseg:ceriseG Σ} {sealg:sealStoreG Σ}
           {nainv: logrel_na_invs Σ}
           `{MP: MachineParameters}.
 

diff --git a/theories/examples/ocpl_lowval_like.v b/theories/examples/ocpl_lowval_like.v
@@ -16,7 +16,7 @@ From cap_machine.proofmode Require Import tactics_helpers.
 *)
 
 Section rules.
-  Context {Σ:gFunctors} {memg:memG Σ} {regg:regG Σ} {sealg:sealStoreG Σ}
+  Context {Σ:gFunctors} {ceriseg:ceriseG Σ} {sealg:sealStoreG Σ}
           {nainv: logrel_na_invs Σ}
           `{MP: MachineParameters}.
 

diff --git a/theories/examples/salloc.v b/theories/examples/salloc.v
@@ -17,7 +17,7 @@ From cap_machine Require Import logrel addr_reg_sample fundamental rules proofmo
    studies. *)
 
 Section SimpleSalloc.
-  Context {Σ:gFunctors} {memg:memG Σ} {regg:regG Σ} {sealsg: sealStoreG Σ}
+  Context {Σ:gFunctors} {ceriseg:ceriseG Σ} {sealsg: sealStoreG Σ}
           {nainv: logrel_na_invs Σ}
           `{MP: MachineParameters}.
 

diff --git a/theories/exercises/cerise_modularity.v b/theories/exercises/cerise_modularity.v
@@ -14,7 +14,7 @@ From cap_machine.proofmode Require Import
 Open Scope Z_scope.
 
 Section increment_macro.
-  Context {Σ:gFunctors} {memg:memG Σ} {regg:regG Σ}
+  Context {Σ:gFunctors} {ceriseg:ceriseG Σ}
           `{MP: MachineParameters}.
 
   (** The increment macro is a macro that takes a register r (r ≠ r_env), which
@@ -159,7 +159,7 @@ Section increment_macro.
 End increment_macro.
 
 Section rclear_macro.
-  Context {Σ:gFunctors} {memg:memG Σ} {regg:regG Σ}
+  Context {Σ:gFunctors} {ceriseg:ceriseG Σ}
           `{MP: MachineParameters}.
 
   (** In this section, we will use a pre-defined macro in Cerise, `rclear`.
@@ -205,7 +205,7 @@ Section rclear_macro.
 End rclear_macro.
 
 Section linking_table.
-  Context {Σ:gFunctors} {memg:memG Σ} {regg:regG Σ}
+  Context {Σ:gFunctors} {ceriseg:ceriseG Σ}
           `{MP: MachineParameters}.
 
   (* Demo with incr_macro for the setup *)

diff --git a/theories/exercises/cerise_modularity_solutions.v b/theories/exercises/cerise_modularity_solutions.v
@@ -13,7 +13,7 @@ From cap_machine.proofmode Require Import proofmode tactics_helpers register_tac
 Open Scope Z_scope.
 
 Section increment_macro.
-  Context {Σ:gFunctors} {memg:memG Σ} {regg:regG Σ}
+  Context {Σ:gFunctors} {ceriseg:ceriseG Σ}
           `{MP: MachineParameters}.
 
   (** The increment macro is a macro that takes a register r (r ≠ r_env), which
@@ -184,7 +184,7 @@ Section increment_macro.
 End increment_macro.
 
 Section rclear_macro.
-  Context {Σ:gFunctors} {memg:memG Σ} {regg:regG Σ}
+  Context {Σ:gFunctors} {ceriseg:ceriseG Σ}
           `{MP: MachineParameters}.
 
   (** In this section, we will use a pre-defined macro in Cerise, `rclear`.
@@ -330,7 +330,7 @@ Section rclear_macro.
 End rclear_macro.
 
 Section linking_table.
-  Context {Σ:gFunctors} {memg:memG Σ} {regg:regG Σ}
+  Context {Σ:gFunctors} {ceriseg:ceriseG Σ}
           `{MP: MachineParameters}.
 
   (* Demo with incr_macro for the setup *)

diff --git a/theories/exercises/cerise_tutorial.v b/theories/exercises/cerise_tutorial.v
@@ -26,7 +26,7 @@ Section base_program.
       are the registers and the memory. Moreover, we need the machine parameters
       in the context, which abstract the encoding and the decoding function
       (for instance, to encode the instructions). *)
-  Context {Σ:gFunctors} {memg:memG Σ} {regg:regG Σ}
+  Context {Σ:gFunctors} {ceriseg:ceriseG Σ}
           `{MP: MachineParameters}.
 
   (** The program is a list of instructions. As the machine has a Von Neumann