Curve25519 scalar field reduction

[jadephilipoom]

More of a discussion than an issue. I was talking with @FiloSottile at HACS about the possibility of generating code for curve25519's scalar field using fiat-crypto. My first answer was "I think it uses Barrett reduction, and we don't have the mainstream pipeline set up for it", based on the ref implementation [0]. But further discussion about the ref10 implementation sounded like pseudomersenne/unsaturated solinas reduction to me, so I said I would take a closer look. Here's what I found:

It does look like unsaturated solinas reduction, but a variant I've never seen before. In particular, the usual algorithm for unsaturated solinas is to take a modulus in the form 2^k-c, split the result of multiplication (usually a no-op because of a cleverly chosen representation) at the kth bit so you have (a + 2^kb) mod (2^k-c), and, since this is the same as (a + cb) mod (2^k-c), just multiply the high half by c and add it to a, then repeat the process. The ref10 implementation [1] does essentially this procedure, except that c is positive (the modulus is l = 2^252 + 27742317777372353535851937790883648493). These lines [2], repeated over and over again, subtract 27742317777372353535851937790883648493 from the first half of the number. Essentially they're doing (a + 2^kb) mod (2^k+c) = (a - cb) mod (2^k+c) -- note the change in sign. I think this is using signed integers; otherwise I can't see how a line like [3] wouldn't underflow (The crypto_int64 type is defined at [4], and I do believe this means signed).

Overall, I don't think we can support this exact algorithm right now without additional engineering, but it's still interesting to know about.

[0] https://github.com/floodyberry/supercop/blob/a351f2c29235512a042d4b6989d241a67e86ad23/crypto_sign/ed25519/ref/sc25519.c#L41 [1] https://github.com/floodyberry/supercop/blob/a351f2c29235512a042d4b6989d241a67e86ad23/crypto_sign/ed25519/ref10/sc_reduce.c#L35 [2] https://github.com/floodyberry/supercop/blob/a351f2c29235512a042d4b6989d241a67e86ad23/crypto_sign/ed25519/ref10/sc_reduce.c#L140-L146 [3] https://github.com/floodyberry/supercop/blob/a351f2c29235512a042d4b6989d241a67e86ad23/crypto_sign/ed25519/ref10/sc_reduce.c#L84 [4] https://github.com/floodyberry/supercop/blob/a351f2c29235512a042d4b6989d241a67e86ad23/inttypes/crypto_int64.c#L3

[JasonGross]

Overall, I don't think we can support this exact algorithm right now without additional engineering,

What engineering is needed?

The bounds analysis and backend code already basically supports signed integers (Java, for example, only has signed integers, so the bounds relaxation pass needs to deal with signed ranges). It's possible I'll need to add an option that says "use both signed and unsigned integers" or it's possible that everything in the bounds and backend pipeline will just work as-is.

[jadephilipoom]

Oh, cool, didn't realize we already have signed-integer support! In that case this might be pretty doable. Right now PushButtonSynthesis requires c to be positive (https://github.com/mit-plv/fiat-crypto/blob/a8ee5ece8ffdb4cfde20f81dd0cf40aef62b9d7c/src/PushButtonSynthesis/UnsaturatedSolinas.v#L190) but I don't see that requirement in the core arithmetic code, so maybe it can be removed and replaced with more nuanced requirements.

[jadephilipoom]

Looks like there's some balance being added after subtraction e.g. here https://github.com/floodyberry/supercop/blob/a351f2c29235512a042d4b6989d241a67e86ad23/crypto_sign/ed25519/ref10/sc_reduce.c#L127

[JasonGross]

but I don't see that requirement in the core arithmetic code, so maybe it can be removed and replaced with more nuanced requirements

I think we encode s for tight bounds. Maybe we should be encoding 2^Z.log2_up(s-c) instead?

[jadephilipoom]

I think that might be a more flexible encoding, yes.

[JasonGross]

@jadephilipoom Actually I was wrong about the source, we do require this assumption in Arithmetic/Freeze: https://github.com/mit-plv/fiat-crypto/blob/a416aabfa3e5ea531a882249213d3dd874b96587/src/Arithmetic/Freeze.v#L35 https://github.com/mit-plv/fiat-crypto/blob/a416aabfa3e5ea531a882249213d3dd874b96587/src/Arithmetic/Freeze.v#L94 Thoughts?

[JasonGross]

I think in fact https://github.com/mit-plv/fiat-crypto/blob/a416aabfa3e5ea531a882249213d3dd874b96587/src/Arithmetic/Freeze.v#L38-L39 does not hold for c < 0, and instead we need to use something like (dec (-((y - m) / m) = 0)) instead of (dec (-((y - m) / s) = 0))?

[JasonGross]

But that doesn't work either, so I'm not sure how to deal with freeze.

[jadephilipoom]

The sc_reduce function I linked to actually performs a full modular reduction, so we wouldn't need freeze. I think it's genuinely a slightly different algorithm, but if we already have signed-integer support it might be feasible to add it.

[JasonGross]

Indeed, we do already have signed integer support. See for example https://github.com/mit-plv/fiat-crypto/blob/98864bbde575242334b97e5a9059e6224e82be76/src/BoundsPipeline.v#L129-L131 where we decide whether to allow both signed and unsigned integer, or to only permit signed integers.

Note, however, that our special routines (addcarryx, subborrowx, zselect/cmovznz) only support unsigned integers right now, IIRC. It would not be too hard to make cmovznz have a variant supporting signed integers.

[andres-erbsen]

Looks like a clever solution that didn't need expanding fiat-crypto was found: https://words.filippo.io/dispatches/wide-reduction/ :)