Implement barrett reduction for ed25519 exponent field

[andres-erbsen]

modulus m = 2^252 + 27742317777372353535851937790883648493, length k = 256, (precomputed mu = 1852673427797059126777135760139006525645217721299241702126143248052143860224795,) input a < 2^512. As in https://github.com/floodyberry/supercop/blob/master/crypto_sign/ed25519/ref/sc25519.c#L41.

[andres-erbsen]

Or maybe we are mistaken to assume base b=2. Following HAC 14.42 as the code suggests, b=256, k=32 would make sense as well, and satisfy b^(k-1) < n < b^k.

[JasonGross]

Oh, hrm, interesting. I don't think I have anything that relies on b = 2, so it should be easy to generalize to any b > 1. The computation is q = (mu * (a >> (256 - 32)) >> (256 + 32)?

[andres-erbsen]

The guess I have with b=256=2^8 would give 256^(32-1) = 2^(256-8) and 256^(32+1) = 2^(256+8), so q = (mu * (a >> (256 - 8)) >> (256 + 8).

[JasonGross]

Ugh, why are there so many variations on Barrett Reduction. Not only does this version split apart the shifts, it also does reduction modulo b^(k+1) early (which might be where the possibility of negative values comes from).

[JasonGross]

@andres-erbsen Is it acceptable to replace

(3) If r < 0 then r ← r + bᵏ⁺¹

with

(3) r ← r mod bᵏ⁺¹

? I think this would make the proofs much easier, and it seems like, by choosing k and b carefully with respect to the machine word size, you get this for free.

[JasonGross]

What needs to be done to complete this, on top of #69?

[JasonGross]

Closed by #77.