Begining of experiment to verify mulmuladdX_fullgen_b4

formal-land · Sep 16, 2024 · 5ddc286 · 5ddc286
1 parent f24242a
commit 5ddc286
Show file tree

Hide file tree

Showing 5 changed files with 19,929 additions and 7 deletions.
diff --git a/CoqOfSolidity/CoqOfSolidity.v b/CoqOfSolidity/CoqOfSolidity.v
@@ -370,6 +370,8 @@ Module M.
       end in
     LowM.Loop loop_body break_with LowM.Pure.
 
+  Parameter for_unit : t U256.t -> t unit -> t unit -> t unit.
+
   Definition break : t BlockUnit.t :=
     pure BlockUnit.Break.