add wrapper for add_get_carry and proofs for add_get_carry and zselect

1 files changed, 9 insertions, 0 deletions

diff --git a/src/Util/ZUtil/Definitions.v b/src/Util/ZUtil/Definitions.v
index a74e4b8f4..4a5d3a0ab 100644
--- a/src/Util/ZUtil/Definitions.v
+++ b/src/Util/ZUtil/Definitions.v
@@ -1,4 +1,5 @@
 Require Import Coq.ZArith.ZArith.
+Require Import Crypto.Util.Decidable.
 Require Import Crypto.Util.ZUtil.Notations.
 Local Open Scope Z_scope.
 
@@ -16,4 +17,12 @@ Module Z.
     := get_carry bitwidth (add_with_carry c x y).
   Definition add_get_carry (bitwidth : Z) (x y : Z) : Z * Z
     := add_with_get_carry bitwidth 0 x y.
+
+  (* splits at [bound], not [2^bitwidth]; wrapper to make add_getcarry
+  work if input is not known to be a power of 2 *)
+  Definition add_get_carry_full (bound : Z) (x y : Z) : Z * Z
+    := if dec (2 ^ (Z.log2 bound) = bound)
+       then add_get_carry (Z.log2 bound) x y
+       else ((x + y) mod bound, (x + y) / bound).
+
 End Z.