diff options
| -rw-r--r-- | _CoqProject | 1 | ||||
| -rw-r--r-- | src/Util/ZUtil/AddModulo.v | 9 | ||||
| -rw-r--r-- | src/Util/ZUtil/Definitions.v | 3 |
3 files changed, 13 insertions, 0 deletions
diff --git a/_CoqProject b/_CoqProject index d34d5214d..4d8765bd7 100644 --- a/_CoqProject +++ b/_CoqProject @@ -6558,6 +6558,7 @@ src/Util/ZRange/BasicLemmas.v src/Util/ZRange/CornersMonotoneBounds.v src/Util/ZRange/Operations.v src/Util/ZUtil/AddGetCarry.v +src/Util/ZUtil/AddModulo.v src/Util/ZUtil/CPS.v src/Util/ZUtil/Definitions.v src/Util/ZUtil/Div.v 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 |