Update WBW montgomery comments

As per https://github.com/mit-plv/fiat-crypto/commit/b4b711cba32a21806c6c0aae53be40c04af60cb3#commitcomment-22521097

2 files changed, 6 insertions, 29 deletions

diff --git a/src/Arithmetic/MontgomeryReduction/WordByWord/Abstract/Definition.v b/src/Arithmetic/MontgomeryReduction/WordByWord/Abstract/Definition.v
index c7bf317ec..9a6b089da 100644
--- a/src/Arithmetic/MontgomeryReduction/WordByWord/Abstract/Definition.v
+++ b/src/Arithmetic/MontgomeryReduction/WordByWord/Abstract/Definition.v
@@ -1,34 +1,13 @@
 (*** Word-By-Word Montgomery Multiplication *)
 (** This file implements Montgomery Form, Montgomery Reduction, and
-    Montgomery Multiplication on an abstract [T].  We follow "Fast Prime
-    Field Elliptic Curve Cryptography with 256 Bit Primes",
-    https://eprint.iacr.org/2013/816.pdf. *)
+    Montgomery Multiplication on an abstract [T].  See
+    https://github.com/mit-plv/fiat-crypto/issues/157 for a discussion
+    of the algorithm; note that it may be that none of the algorithms
+    there exactly match what we're doing here. *)
 Require Import Coq.ZArith.ZArith.
 Require Import Crypto.Util.Notations.
 Require Import Crypto.Util.LetIn.
 
-(** 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 WordByWordMontgomery.
diff --git a/src/Arithmetic/MontgomeryReduction/WordByWord/Definition.v b/src/Arithmetic/MontgomeryReduction/WordByWord/Definition.v
index d27336819..bc95d7091 100644
--- a/src/Arithmetic/MontgomeryReduction/WordByWord/Definition.v
+++ b/src/Arithmetic/MontgomeryReduction/WordByWord/Definition.v
@@ -1,14 +1,12 @@
 (*** Word-By-Word Montgomery Multiplication *)
 (** This file implements Montgomery Form, Montgomery Reduction, and
-    Montgomery Multiplication on an abstract [list ℤ].  We follow
-    "Fast Prime Field Elliptic Curve Cryptography with 256 Bit
-    Primes", https://eprint.iacr.org/2013/816.pdf. *)
+    Montgomery Multiplication on an abstract [list ℤ]. *)
 Require Import Coq.ZArith.BinInt.
 Require Import Crypto.Arithmetic.Saturated.
 Require Import Crypto.Arithmetic.MontgomeryReduction.WordByWord.Abstract.Definition.
 
 Section redc.
-  (** XXX TODO: pick better names for the arguments to this definition. *)
+  (** TODO: pick better names for the arguments to this definition. *)
   Definition redc {r : positive} {R_numlimbs : nat} (N A B : T) (k : Z) : T
     := @redc T numlimbs zero divmod r (@scmul (Z.pos r)) (@add (Z.pos r)) (@drop_high (S R_numlimbs)) N A B k.
 End redc.