From 8fb843d604989a073559b4811523c7b49a85e221 Mon Sep 17 00:00:00 2001
From: InfiniteEchoes <128528395+InfiniteEchoes@users.noreply.github.com>
Date: Wed, 12 Jun 2024 14:34:32 +0800
Subject: [PATCH] Update

---
 CoqOfPython/ethereum/utils/simulations/numeric.v | 10 +++++++++-
 1 file changed, 9 insertions(+), 1 deletion(-)

diff --git a/CoqOfPython/ethereum/utils/simulations/numeric.v b/CoqOfPython/ethereum/utils/simulations/numeric.v
index 776aa53..9f95f6e 100644
--- 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 *)
\ No newline at end of file
+        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.
\ No newline at end of file