{{ message }}

# Define Montgomery reduction / multiplication on Z #42

Merged
merged 6 commits into from Aug 5, 2016
Merged

# Define Montgomery reduction / multiplication on Z#42

merged 6 commits into from Aug 5, 2016

## Conversation

### JasonGross commented Aug 1, 2016 • edited

 This is partly done for my own benefit, to internalize how Montgomery multiplication works, and partly done as a template for word-based Montgomery multiplication when the carrying does not take advantage of the fact that we are using a pseudomersenne prime. (@agl @mschilder123 @andres-erbsen @jadephilipoom) I'm looking for feedback on style, as well as correctness of transcription for ECC.
``` Define Montgomery reduction / multiplication on Z ```
``` 3775274 ```
```This is partly done for my own benefit, to internalize how Montgomery
multiplication works, and partly done as a template for word-based
Montgomery multiplication when the carrying does not take advantage of
the fact that we are using a pseudomersenne prime.```
 Section redc. (** While the above algorithm is correct, it is slower than multiplication in the standard representation because of the need to multiply by [R′] and divide by [N]. Montgomery

#### andres-erbsen Aug 2, 2016 Contributor

divide? Are you assuming `(fun x => x mod m)` is implemented using division?

#### JasonGross Aug 2, 2016 Author Member

Is there a faster way for `m` not a power of two and `x` large? Maybe I should insert more instances of "I'm quoting Wikipedia"...

#### andres-erbsen Aug 2, 2016 Contributor

Nah, division is a very reasonable implementation. The edit I would have suggested would be "divide by [N]" -> "reduce modulo [N]", but reading this the third time now, I don't find it confusing anymore, so maybe nevermind.

 Let m := ((T mod R) * N') mod R. Let t := (T + m * N) / R. Definition reduce : montgomeryZ

#### andres-erbsen Aug 2, 2016 Contributor

It is quite hard to tell that reduce will have only one argument. Not sure whether we care.

#### JasonGross Aug 2, 2016 Author Member

Fixed non-obvious non-dependence on `T_in_range` by f9d5110. I suppose I could also separate out the algorithms and the proofs into separate files. Do you think I should?

#### andres-erbsen Aug 2, 2016 Contributor

No. I think there is value in keeping top-level specification as small as possible, but Montgomery reduction isn't that. I can't currently think of a case where I would want the definitions but not the proofs.

#### JasonGross Aug 2, 2016 Author Member

I think I want to separate out the proofs; @mschilder123 suggested a bunch of alternate bounds one might want, and the file is getting a bit unwieldy to read at this point.

added 2 commits Aug 2, 2016
``` Make it more obvious where T_in_range is used ```
``` f9d5110 ```
``` Work around broken [lia]/[omega] in Coq 8.4 ```
``` 64065fe ```

### andres-erbsen commented Aug 2, 2016

 I haven't implemented Montgomery reduction before, so I can't judge how closely this lines up with the code you would want to have when using a polynomial representation of Z. I think I would skim through https://golang.org/src/math/big/nat.go#L199 and https://golang.org/src/math/big/nat.go#L1056 (which have helpful comments) and maybe https://github.com/libtom/libtommath/blob/master/bn_mp_montgomery_reduce.c if I wanted to line this PR up with a polynomial-representation implementation, but I won't do this now. Does this PR mean that you will not be implementing polynomial-based Barrett reduction? The motivation on my part here is that I was hoping I could reuse the generic code for polynomial-representation Barrett reduction for the Ed25519 exponent scalars. In an ideal word we could have a somewhat generic recipe for changing between representations of Z, so it might be worth thinking about how different the `Barrett reduction on Z -> Barrett reduction on polynomials in Z` and `Montgomery reduction reduction on Z -> Montgomery reduction on polynomials in Z` transformations need to look like anyway.

### JasonGross commented Aug 2, 2016

 so I can't judge how closely this lines up with the code you would want to have when using a polynomial representation of Z. I plan to look at that next; I think it's better to have this version, and look at the polynomial version after, rather than trying to do them simultaneously. Wikipedia also has a section on the polynomial version Does this PR mean that you will not be implementing polynomial-based Barrett reduction? It turns out that some of the optimizations necessary for doing Barrett-reduction efficiently (namely, computing `q = (m * (a >> (k-1))) >> (k+1)` rather than `q = (m * a) >> k` and only works for 25519 (`k = 255`) by luck, and may or may not work for P256; this optimization only guarantees that `a - q * n < 3 * n`, and a brute-force search of around 700 cases shows that `a - q * n < 2 * n` for 25519. (P256 requires just over `2^256 - 2^254` cases using the method that works for 25519, so I'm still not sure if it works.) So I probably won't be implementing polynomial-based Barrett reduction, but I'm hopeful that I'll be able to port the proofs from integer-based Montgomery to polynomial-based Montgomery without much code, if not derive the algorithm itself, and I'm hopeful that the transformation will be similar for (unoptimized) Barrett reduction. I might even include this as a test-case that the machinery is modular enough.

### andres-erbsen commented Aug 2, 2016

 I assume your experiments were for the Curve25519 underlying field `F (2^255-19)`, not the exponent field `F (2^252 + 27742317777372353535851937790883648493)` ? I would want code for the latter. However, the corresponding Barrett reduction in `ed25519-ref` at https://github.com/floodyberry/supercop/blob/master/crypto_sign/ed25519/ref/sc25519.c#L88 performs two conditional subtractions, as HAC 14.44(ii) says, and so does https://github.com/floodyberry/supercop/blob/master/crypto_sign/ed25519/amd64-51-30k/sc25519_barrett.s#L1029.

### JasonGross commented Aug 2, 2016

 `F (2^255-19)` Yes, that's correct. performs two conditional subtractions Yes, this is safe regardless of the modulus, as long as it's sufficiently within bounds. I haven't pushed through / cleaned up the code that shows this (most of the content is there, excepting the part that shows that we're not negative), but I could probably do so (for `Z`) in a few hours to a day of work (unless it turns out that you can get something negative, and that something special has to be done in this case). Would that be useful to you?

 Yes.

### JasonGross commented Aug 2, 2016

 Okay, let me finish cleaning this up (I'm going to separate out the proofs and add a few alternate bounds), and then I'll add the `(m * (a >> (k-1))) >> (k+1)` version of Barrett. (Do you have a good name for it? I've been calling it `ZPaper.v` because it's what's in Barrett's original paper.)
``` Add more bounds proofs, move to ZProofs ```
``` c0b5a19 ```

### JasonGross commented Aug 2, 2016

 @andres-erbsen I've moved the proofs to `ZProofs.v` and added a number of alternate bounds.
``` Fixes for Coq 8.4 ```
``` 7dd7cd1 ```

### JasonGross commented Aug 3, 2016

 `F (2^252 + 27742317777372353535851937790883648493)` Do you take `k = 253` here? If not, I think you can be off by a lot more than 2. In particular, I need that `a mod 2^(k-1) < n` for `a` the input and `n` the modulus. https://github.com/floodyberry/supercop/blob/master/crypto_sign/ed25519/ref/sc25519.c#L88 ``` /* XXX: Can it really happen that r<0?, See HAC, Alg 14.42, Step 3 * If so: Handle it here! */``` Assuming they're implementing the same algorithm we are, the answer here is "no".

### andres-erbsen commented Aug 3, 2016

 Let's move the Barrett reduction discussion to #43 and leave this ticket for Montgomery form stuff.
``` Merge branch 'master' into montgomery-Z ```
``` 74c6d7c ```
 an integer [R′] such that [RR' ≡ 1 (mod N)], that is, by an [R′] whose residue class is the modular inverse of [R] mod [N]. Then, working modulo [N], *) (** [(aR mod N)(bR mod N)R' ≡ (aR)(bR)R⁻¹ ≡ (ab)R (mod N)]. *)

#### jadephilipoom Aug 5, 2016 • edited Collaborator

I think the R⁻¹ should be changed to R' here for consistency.

#### JasonGross Aug 5, 2016 Author Member

This is literally a quotation from Wikipedia. I think they mean `(aR)(bR) / R`, but just wanted to write that without the fraction.

 end if end function >> *) Context (N' : Z). (* N' is N⁻¹ mod R *)

#### jadephilipoom Aug 5, 2016 Collaborator

Above on line 89 it says "Integer `N′` in `[0, R − 1]` such that `NN′ ≡ −1 mod R`", so shouldn't `N'` be `-N⁻¹ mod R`?

#### JasonGross Aug 5, 2016 Author Member

Good catch. Fixed.

### jadephilipoom commented Aug 5, 2016

 Looks good.
merged commit `2be3fd6` into mit-plv:master Aug 5, 2016
1 check passed
1 check passed
continuous-integration/travis-ci/pr The Travis CI build passed
Details
deleted the JasonGross:montgomery-Z branch Aug 5, 2016