Add new modular addition operation on Z

2 files changed, 12 insertions, 0 deletions

diff --git a/src/Util/ZUtil/AddModulo.v b/src/Util/ZUtil/AddModulo.v
new file mode 100644
index 000000000..0f80a75d9
--- /dev/null
+++ b/src/Util/ZUtil/AddModulo.v
@@ -0,0 +1,9 @@
+Require Import Coq.ZArith.ZArith.
+Require Import Crypto.Util.ZUtil.Definitions.
+Local Open Scope Z_scope.
+
+Module Z.
+  Lemma add_modulo_correct x y modulus :
+    Z.add_modulo x y modulus =  if (modulus <=? x + y) then (x + y) - modulus else (x + y).
+  Proof. reflexivity. Qed.
+End Z.
\ No newline at end of file
diff --git a/src/Util/ZUtil/Definitions.v b/src/Util/ZUtil/Definitions.v
index 760651a94..66fc7f558 100644
--- a/src/Util/ZUtil/Definitions.v
+++ b/src/Util/ZUtil/Definitions.v
@@ -10,6 +10,9 @@ Module Z.
   Definition zselect (cond zero_case nonzero_case : Z) :=
     if cond =? 0 then zero_case else nonzero_case.
 
+  Definition add_modulo x y modulus :=
+    if (modulus <=? x + y) then (x + y) - modulus else (x + y).
+
   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