Cleaning up the trusted compute file

logsem · Jan 7, 2025 · c161a17 · c161a17
1 parent 8ce4dd2
commit c161a17
Show file tree

Hide file tree

Showing 6 changed files with 241 additions and 225 deletions.
diff --git a/theories/cap_lang.v b/theories/cap_lang.v
@@ -445,6 +445,12 @@ Section opsem.
       then Some (Nat.div (Z.to_nat oa) 2)
       else Some (Nat.div (Z.to_nat (oa^-1)%f) 2).
 
+  Definition has_seal (ot : Z) (tid : TIndex) : Prop :=
+    match finz.of_z ot with
+    | Some ot => tid_of_otype ot = Some tid
+    | None => False
+    end.
+
   Definition measure (m : Mem) (b e: Addr) :=
     let instructions : list Word :=
       map snd