diff options
author | Jason Gross <jgross@mit.edu> | 2017-04-28 13:31:55 -0400 |
---|---|---|
committer | Jason Gross <jasongross9@gmail.com> | 2017-05-01 15:02:58 -0400 |
commit | cb9f74654f2cf377277e0368bed935ef85b7be6e (patch) | |
tree | 476a18df2b3a151d06d5056639711a6f7b5b24a7 /src/Arithmetic/MontgomeryReduction/WordByWord/Definition.v | |
parent | ee9016bcdb77a89e2cbbe539ccfd4d3412d523e2 (diff) |
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.
Diffstat (limited to 'src/Arithmetic/MontgomeryReduction/WordByWord/Definition.v')
-rw-r--r-- | src/Arithmetic/MontgomeryReduction/WordByWord/Definition.v | 63 |
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. |