Implement barrett reduction for ed25519 exponent field about fiat-crypto HOT 7 CLOSED

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.

from fiat-crypto.

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)?

from fiat-crypto.

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).

from fiat-crypto.

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).

from fiat-crypto.

@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.

from fiat-crypto.

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

from fiat-crypto.

Closed by #77.

from fiat-crypto.