From 56bf29e5a4244d665f231b5a2602694a7414c762 Mon Sep 17 00:00:00 2001
From: Jade Philipoom <jadep@google.com>
Date: Fri, 16 Feb 2018 10:51:43 +0100
Subject: Add new modular addition operation on Z

---
 src/Util/ZUtil/AddModulo.v   | 9 +++++++++
 src/Util/ZUtil/Definitions.v | 3 +++
 2 files changed, 12 insertions(+)
 create mode 100644 src/Util/ZUtil/AddModulo.v

(limited to 'src/Util/ZUtil')

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
-- 
cgit v1.2.3