add wrapper for add_get_carry and proofs for add_get_carry and zselect

3 files changed, 46 insertions, 0 deletions

diff --git a/src/Util/ZUtil/AddGetCarry.v b/src/Util/ZUtil/AddGetCarry.v
index 7a38e4ba6..3c78ca280 100644
--- a/src/Util/ZUtil/AddGetCarry.v
+++ b/src/Util/ZUtil/AddGetCarry.v
@@ -1,6 +1,8 @@
 Require Import Coq.ZArith.ZArith Coq.micromega.Lia.
+Require Import Crypto.Util.ZUtil.
 Require Import Crypto.Util.ZUtil.Definitions.
 Require Import Crypto.Util.ZUtil.Hints.ZArith.
+Require Import Crypto.Util.Prod Crypto.Util.Tactics.
 Require Import Crypto.Util.ZUtil.Tactics.PullPush.Modulo.
 Require Import Crypto.Util.ZUtil.Tactics.DivModToQuotRem.
 Require Import Crypto.Util.LetIn.
@@ -49,4 +51,23 @@ Module Z.
       apply add_get_carry_to_add_with_get_carry_cps_gen.
     Qed.
   End with_bitwidth.
+  
+  Local Hint Unfold Z.add_get_carry_full Z.add_get_carry
+        Z.add_with_get_carry Z.get_carry Z.add_with_carry.
+  Lemma add_get_carry_full_mod s x y :
+    fst (Z.add_get_carry_full s x y)  = (x + y) mod s.
+  Proof.
+    repeat progress autounfold.
+    break_match; autorewrite with cancel_pair zsimplify;
+      reflexivity.
+  Qed.
+
+  Lemma add_get_carry_full_div s x y :
+    snd (Z.add_get_carry_full s x y)  = (x + y) / s.
+  Proof.
+    repeat progress autounfold.
+    break_match; autorewrite with cancel_pair zsimplify;
+      reflexivity.
+  Qed.
+  
 End Z.
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.
diff --git a/src/Util/ZUtil/Zselect.v b/src/Util/ZUtil/Zselect.v
new file mode 100644
index 000000000..0166ce6f4
--- /dev/null
+++ b/src/Util/ZUtil/Zselect.v
@@ -0,0 +1,16 @@
+Require Import Coq.ZArith.ZArith.
+Require Import Crypto.Util.Decidable.
+Require Import Crypto.Util.ZUtil.Definitions.
+Require Import Crypto.Util.Tactics.
+Local Open Scope Z_scope.
+
+Module Z.
+  Lemma zselect_correct cond zero_case nonzero_case :
+    Z.zselect cond zero_case nonzero_case =
+    if dec (cond = 0) then zero_case else nonzero_case.
+  Proof.
+    cbv [Z.zselect]; break_match;
+      try reflexivity; try discriminate.
+    rewrite <-Z.eqb_neq in *; congruence.
+  Qed.
+End Z.
\ No newline at end of file