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