Update

formal-land · Jun 12, 2024 · 8fb843d · 8fb843d
1 parent 897e74d
commit 8fb843d
Showing 1 changed file with 9 additions and 1 deletion.
diff --git a/CoqOfPython/ethereum/utils/simulations/numeric.v b/CoqOfPython/ethereum/utils/simulations/numeric.v
@@ -19,4 +19,12 @@
     if remainder == Uint(0):
         return value
     else:
-        return value + ceiling - remainder *)
+        return value + ceiling - remainder *)
+
+(* TODO: Finish below *)
+Definition ceil32 (value : Uint) : Uint :=
+  let ceiling := Uint.Make 32 in
+  let remainder := value % ceiling in
+  if remainder =? Uint 0
+  then value
+  else value + ceiling - remainder.