Rename EId -> EIdentity

logsem · Dec 19, 2024 · 1335450 · 1335450
1 parent 6f97b41
commit 1335450
Show file tree

Hide file tree

Showing 4 changed files with 13 additions and 13 deletions.
diff --git a/theories/cap_lang.v b/theories/cap_lang.v
@@ -25,7 +25,7 @@ Definition Conf: Type := ConfFlag * ExecConf.
 Definition update_regs (φ: ExecConf) (reg' : Reg) : ExecConf := MkExecConf reg' (mem φ) (etable φ) (enumcur φ).
 Definition update_reg (φ: ExecConf) (r: RegName) (w: Word): ExecConf := update_regs φ (<[ r := w ]> (reg φ)).
 Definition update_mem (φ: ExecConf) (a: Addr) (w: Word): ExecConf := MkExecConf (reg φ) (<[a:=w]>(mem φ)) (etable φ) (enumcur φ).
-Definition update_etable (φ: ExecConf) (i: TIndex) (eid : EId) : ExecConf := MkExecConf (reg φ) (mem φ) (<[i := eid]> (etable φ)) (enumcur φ).
+Definition update_etable (φ: ExecConf) (i: TIndex) (eid : EIdentity) : ExecConf := MkExecConf (reg φ) (mem φ) (<[i := eid]> (etable φ)) (enumcur φ).
 Definition remove_from_etable (φ : ExecConf) (i : TIndex) : ExecConf :=
    match φ with
    | {| reg := reg; mem := mem; etable := etable; enumcur := enumcur |} =>
@@ -440,7 +440,7 @@ Section opsem.
   Definition no_cap (mem : Mem) (b: Addr) (e : Addr) : bool :=
     bool_decide (not (contains_cap mem b e)).
 
-  Definition retrieve_eid (i : TIndex) (tb : ETable) : option EId :=
+  Definition retrieve_eid (i : TIndex) (tb : ETable) : option EIdentity :=
     match (tb !! i) with
     | Some p => Some p
     | None => None

diff --git a/theories/logical_mapsto.v b/theories/logical_mapsto.v
@@ -2356,9 +2356,9 @@ Class ceriseG Σ := CeriseG {
   (* Heap for registers *)
   reg_gen_regG :: gen_heapGS RegName LWord Σ;
   (* The ghost resource of all enclaves that have ever existed *)
-  enclaves_hist :: inG Σ (authR (gmapR TIndex (agreeR EId)));
+  enclaves_hist :: inG Σ (authR (gmapR TIndex (agreeR EIdentity)));
   (* The ghost resource of current, known alive enclaves *)
-  enclaves_live :: inG Σ (authR (gmapR TIndex (exclR EId)));
+  enclaves_live :: inG Σ (authR (gmapR TIndex (exclR EIdentity)));
   (* ghost names for the resources *)
   enclaves_name_prev : gname;
   enclaves_name_cur : gname;
@@ -2367,32 +2367,32 @@ Class ceriseG Σ := CeriseG {
 
  (* Assertions over enclaves *)
 
-Definition enclaves_cur (tbl : gmap TIndex EId) `{ceriseG Σ} :=
+Definition enclaves_cur (tbl : gmap TIndex EIdentity) `{ceriseG Σ} :=
   own (inG0 := enclaves_live) enclaves_name_cur (● (Excl <$> tbl)).
 
-Definition enclaves_prev (tbl : gmap TIndex EId) `{ceriseG Σ} :=
+Definition enclaves_prev (tbl : gmap TIndex EIdentity) `{ceriseG Σ} :=
   own (inG0 := enclaves_hist) enclaves_name_prev (● (to_agree <$> tbl)).
 
-Definition enclaves_all (tbl : gmap TIndex EId) `{ceriseG Σ} :=
+Definition enclaves_all (tbl : gmap TIndex EIdentity) `{ceriseG Σ} :=
   own (inG0 := enclaves_hist) enclaves_name_all (● (to_agree <$> tbl)).
 
 (* Fragmental resources *)
 
-Definition enclave_cur (eid : TIndex) (identity : EId) `{ceriseG Σ} :=
+Definition enclave_cur (eid : TIndex) (identity : EIdentity) `{ceriseG Σ} :=
   own (inG0 := enclaves_live) enclaves_name_cur (auth_frag {[eid := Excl identity]}).
 
 Definition enclave_prev (eid : TIndex) `{ceriseG Σ} : iProp Σ :=
   ∃ id ,
   own (inG0 := enclaves_hist) enclaves_name_prev (auth_frag {[eid := to_agree id]}).
 
-Definition enclave_all (eid : TIndex) (id : EId) `{ceriseG Σ} : iProp Σ :=
+Definition enclave_all (eid : TIndex) (id : EIdentity) `{ceriseG Σ} : iProp Σ :=
   own (inG0 := enclaves_hist) enclaves_name_all (auth_frag {[eid := to_agree id]}).
 
 (* Notations for fragmental resources *)
 (* @TODO: denis *)
 
 Definition state_interp_logical (σ : cap_lang.state) `{!ceriseG Σ} : iProp Σ :=
-  ∃ lr lm vmap (cur_tb prev_tb all_tb : gmap TIndex EId) ,
+  ∃ lr lm vmap (cur_tb prev_tb all_tb : gmap TIndex EIdentity) ,
     gen_heap_interp lr ∗
     gen_heap_interp lm ∗
     ⌜cur_tb = σ.(etable)⌝ ∗

diff --git a/theories/machine_base.v b/theories/machine_base.v
@@ -77,9 +77,9 @@ Definition Mem := gmap Addr Word.
 
 (* State involved in supporting enclaves *)
 Definition TIndex := nat.
-Definition EId := Z. (* For now, we assume the hash to be unbounded *)
+Definition EIdentity := Z. (* For now, we assume the hash to be unbounded *)
 Definition ENum := nat. (* The max # of supported enclaves *)
-Definition ETable := gmap TIndex EId. (* Check sail impl. of CHERi-TrEE for how to get table index ? They don't have a table but a distinct memory region *)
+Definition ETable := gmap TIndex EIdentity. (* Check sail impl. of CHERi-TrEE for how to get table index ? They don't have a table but a distinct memory region *)
 
 (* EqDecision instances *)
 

diff --git a/theories/rules/rules_EStoreId.v b/theories/rules/rules_EStoreId.v
@@ -42,7 +42,7 @@ Section cap_lang_rules.
         ∗ rs ↦ᵣ LWInt otype
         ∗ (
           ⌜ retv = NextIV ⌝
-          ∗ ∃ (id : EId), ∃ (enum : ENum),
+          ∗ ∃ (id : EIdentity), ∃ (enum : ENum),
               rd ↦ᵣ (LWInt id)
               ∗ (enclave_all enum id)
             ∗ ⌜ has_lseal otype enum ⌝