diff options
| -rw-r--r-- | _CoqProject | 1 | ||||
| -rw-r--r-- | src/Util/ZUtil/Definitions.v | 2 | ||||
| -rw-r--r-- | src/Util/ZUtil/MulSplit.v | 10 |
3 files changed, 13 insertions, 0 deletions
diff --git a/_CoqProject b/_CoqProject index 8556a6120..5c11bee09 100644 --- a/_CoqProject +++ b/_CoqProject @@ -329,6 +329,7 @@ src/Util/ZUtil/Hints.v src/Util/ZUtil/Land.v src/Util/ZUtil/Modulo.v src/Util/ZUtil/Morphisms.v +src/Util/ZUtil/MulSplit.v src/Util/ZUtil/Notations.v src/Util/ZUtil/Pow2Mod.v src/Util/ZUtil/Quot.v diff --git a/src/Util/ZUtil/Definitions.v b/src/Util/ZUtil/Definitions.v index 6fc969dfd..ff15dc83c 100644 --- a/src/Util/ZUtil/Definitions.v +++ b/src/Util/ZUtil/Definitions.v @@ -35,4 +35,6 @@ Module Z. then add_get_carry (Z.log2 bound) x y else ((x + y) mod bound, (x + y) / bound). + Definition mul_split (s x y : Z) : Z * Z + := ((x * y) mod s, (x * y) / s). End Z. diff --git a/src/Util/ZUtil/MulSplit.v b/src/Util/ZUtil/MulSplit.v new file mode 100644 index 000000000..e0448fe69 --- /dev/null +++ b/src/Util/ZUtil/MulSplit.v @@ -0,0 +1,10 @@ +Require Import Coq.ZArith.ZArith. +Require Import Crypto.Util.ZUtil.Definitions. +Local Open Scope Z_scope. + +Module Z. + Lemma mul_split_mod s x y : fst (Z.mul_split s x y) = (x * y) mod s. + Proof. reflexivity. Qed. + Lemma mul_split_div s x y : snd (Z.mul_split s x y) = (x * y) / s. + Proof. reflexivity. Qed. +End Z. |