Add definitions for zselect and add_get_carry

In ZUtil/Definitions.v

1 files changed, 12 insertions, 0 deletions

diff --git a/src/Util/ZUtil/Definitions.v b/src/Util/ZUtil/Definitions.v
index 2753f5ff8..a8dbc5e96 100644
--- a/src/Util/ZUtil/Definitions.v
+++ b/src/Util/ZUtil/Definitions.v
@@ -4,4 +4,16 @@ Local Open Scope Z_scope.
 
 Module Z.
   Definition pow2_mod n i := (n &' (Z.ones i)).
+
+  Definition zselect (cond zero_case nonzero_case : Z) :=
+    if cond =? 0 then zero_case else nonzero_case.
+
+  Definition get_carry (bitwidth : Z) (v : Z) : Z * Z
+    := (v mod 2^bitwidth, v / 2^bitwidth).
+  Definition add_with_carry (c : Z) (x y : Z) : Z
+    := c + x + y.
+  Definition add_with_get_carry (bitwidth : Z) (c : Z) (x y : Z) : Z * Z
+    := get_carry bitwidth (add_with_carry c x y).
+  Definition add_get_carry (bitwidth : Z) (x y : Z) : Z * Z
+    := get_carry bitwidth (x + y).
 End Z.