Initial stab at word-by-word montgomery

I think I got the loop itself wrong, though:
1. I'm worried that it'll overflow off the end of the positional
   representation, since I'm not actually dividing by 2^s
2. I'm not carrying/reducing anywhere, so the getting the nth value
   might be wrong
3. I'm not sure if I got indexing right.

But I want to submit this early version to get comments, before I put
more effort into it.

1 files changed, 63 insertions, 0 deletions

diff --git a/src/Arithmetic/MontgomeryReduction/WordByWord/Definition.v b/src/Arithmetic/MontgomeryReduction/WordByWord/Definition.v
new file mode 100644
index 000000000..5d10cbe74
--- /dev/null
+++ b/src/Arithmetic/MontgomeryReduction/WordByWord/Definition.v
@@ -0,0 +1,63 @@
+(*** Word-By-Word Montgomery Multiplication *)
+(** This file implements Montgomery Form, Montgomery Reduction, and
+    Montgomery Multiplication on [tuple ℤ].  We follow "Fast Prime
+    Field Elliptic Curve Cryptography with 256 Bit Primes",
+    https://eprint.iacr.org/2013/816.pdf. *)
+Require Import Coq.ZArith.ZArith.
+Require Import Crypto.Arithmetic.Core.
+Require Import Crypto.Arithmetic.MontgomeryReduction.Definition.
+Require Import Crypto.Util.Tuple.
+Require Import Crypto.Util.Notations.
+
+(** Quoting from page 7 of "Fast Prime
+    Field Elliptic Curve Cryptography with 256 Bit Primes",
+    https://eprint.iacr.org/2013/816.pdf: *)
+(** * Algorithm 1: Word-by-Word Montgomery Multiplication (WW-MM) *)
+(** Input: [p < 2ˡ] (odd modulus),
+           [0 ≤ a, b < p], [l = s×k]
+    Output: [a×b×2⁻ˡ mod p]
+    Pre-computed: [k0 = -p⁻¹ mod 2ˢ]
+    Flow
+<<
+1. T = a×b
+ For i = 1 to k do
+   2. T1 = T mod 2ˢ
+   3. Y = T1 × k0 mod 2ˢ
+   4. T2 = Y × p
+   5. T3 = (T + T2)
+   6. T = T3 / 2ˢ
+ End For
+7. If T ≥ p then X = T – p;
+      else X = T
+Return X
+>> *)
+Local Open Scope Z_scope.
+Section positional.
+  Local Notation "ts {{ i }}" := (@nth_default Z _ 0%Z i ts).
+  Context (k : nat)
+          (weight : nat -> Z)
+          (p : tuple Z k) (* the prime *)
+          (p' : Z) (* [-p⁻¹] *)
+          (modulo div : Z -> Z -> Z).
+  Local Notation encode := (@B.Positional.encode weight modulo div k).
+  Local Notation mul a b := (@B.Positional.mul_cps weight k k a b _ id).
+  Local Notation add a b := (@B.Positional.add_cps weight k a b _ id).
+
+  Section body.
+    Context (T : tuple Z k)
+            (i : nat).
+    Let k0 := p' mod (weight i).
+
+    Let T1 := T{{i}} mod (weight i).
+    Let Y := (T1 * k0) mod (weight i).
+    Let T2 := mul p (encode Y).
+    Let T3 := add T T2.
+    Definition redc_body := T3.
+  End body.
+
+  Fixpoint redc_from (T : tuple Z k) (count : nat) : tuple Z k
+    := match count with
+       | O => T
+       | S count' => redc_from (redc_body T (k - count)) count'
+       end.
+End positional.