How do we compute the constant for scmul?

[JasonGross]

We were asked over email by @huitseeker:

I'm wondering if there is a reason why fiat is not generating the scalar arithmetic files by default, since every standard parameter set has an associated group order, and most ECC applications build scalar and point arithmetic on top of the field's operations anyway.

We have this for curve25519:

fiat-crypto/fiat-c/src/curve25519_64.c

Lines 572 to 615 in e525793

	/*
	* The function fiat_25519_carry_scmul_121666 multiplies a field element by 121666 and reduces the result.
	* Postconditions:
	* eval out1 mod m = (121666 * eval arg1) mod m
	*
	* Input Bounds:
	* arg1: [[0x0 ~> 0x1a666666666664], [0x0 ~> 0x1a666666666664], [0x0 ~> 0x1a666666666664], [0x0 ~> 0x1a666666666664], [0x0 ~> 0x1a666666666664]]
	* Output Bounds:
	* out1: [[0x0 ~> 0x8cccccccccccc], [0x0 ~> 0x8cccccccccccc], [0x0 ~> 0x8cccccccccccc], [0x0 ~> 0x8cccccccccccc], [0x0 ~> 0x8cccccccccccc]]
	*/
	static void fiat_25519_carry_scmul_121666(uint64_t out1[5], const uint64_t arg1[5]) {
	fiat_25519_uint128 x1 = ((fiat_25519_uint128)UINT32_C(0x1db42) * (arg1[4]));
	fiat_25519_uint128 x2 = ((fiat_25519_uint128)UINT32_C(0x1db42) * (arg1[3]));
	fiat_25519_uint128 x3 = ((fiat_25519_uint128)UINT32_C(0x1db42) * (arg1[2]));
	fiat_25519_uint128 x4 = ((fiat_25519_uint128)UINT32_C(0x1db42) * (arg1[1]));
	fiat_25519_uint128 x5 = ((fiat_25519_uint128)UINT32_C(0x1db42) * (arg1[0]));
	uint64_t x6 = (uint64_t)(x5 >> 51);
	uint64_t x7 = (uint64_t)(x5 & UINT64_C(0x7ffffffffffff));
	fiat_25519_uint128 x8 = (x6 + x4);
	uint64_t x9 = (uint64_t)(x8 >> 51);
	uint64_t x10 = (uint64_t)(x8 & UINT64_C(0x7ffffffffffff));
	fiat_25519_uint128 x11 = (x9 + x3);
	uint64_t x12 = (uint64_t)(x11 >> 51);
	uint64_t x13 = (uint64_t)(x11 & UINT64_C(0x7ffffffffffff));
	fiat_25519_uint128 x14 = (x12 + x2);
	uint64_t x15 = (uint64_t)(x14 >> 51);
	uint64_t x16 = (uint64_t)(x14 & UINT64_C(0x7ffffffffffff));
	fiat_25519_uint128 x17 = (x15 + x1);
	uint64_t x18 = (uint64_t)(x17 >> 51);
	uint64_t x19 = (uint64_t)(x17 & UINT64_C(0x7ffffffffffff));
	uint64_t x20 = (x18 * UINT8_C(0x13));
	uint64_t x21 = (x7 + x20);
	fiat_25519_uint1 x22 = (fiat_25519_uint1)(x21 >> 51);
	uint64_t x23 = (x21 & UINT64_C(0x7ffffffffffff));
	uint64_t x24 = (x22 + x10);
	fiat_25519_uint1 x25 = (fiat_25519_uint1)(x24 >> 51);
	uint64_t x26 = (x24 & UINT64_C(0x7ffffffffffff));
	uint64_t x27 = (x25 + x13);
	out1[0] = x23;
	out1[1] = x26;
	out1[2] = x27;
	out1[3] = x16;
	out1[4] = x19;
	}

However, the number 121666 is a magic constant to me (according to the internet, it's (d + 2) / 4....). What are the equivalent numbers for the other unsaturated solinas curves? Is there a table of these numbers somewhere? Can they be computed somehow?

cc @andres-erbsen

[jadephilipoom]

I'm not sure that's what is meant by "the scalar arithmetic files". Our carry_scmul multiplies a field element (in the field used by curve point coordinates) by a scalar value. However, at the group level of abstraction, you often want to multiply a curve point by a scalar, and you want that scalar to be in a specific (different!) field. In a lot of code developments the elements of this field are referred to simply as "scalars", as differentiated from group elements. (The modulus of this field for ed25519 is called l, to cite a possibly familiar example -- see code at [0])

@huitseeker is that indeed what you meant? If so, the answer I vaguely recall from years ago is "the scalar arithmetic isn't performance-critical or particularly complicated so it's lower priority than field arithmetic", but perhaps that's worth revisiting now that the field arithmetic is taken care of.

[0] /~https://github.com/floodyberry/supercop/blob/a351f2c29235512a042d4b6989d241a67e86ad23/crypto_sign/ed25519/ref/sc25519.c

[briansmith]

@huitseeker is that indeed what you meant? If so, the answer I vaguely recall from years ago is "the scalar arithmetic isn't performance-critical

That's pretty true. If you implement scalar inversion by Fermat's Little Theorem then the scalar multiplication and (especially) squaring performance matters a lot for that operation.

"or particularly complicated"

It is no simpler than the field arithmetic.

It would be nice for Fiat to synthesize size-optimized (e.g. using loops) code for scalar operations instead of speed-optimized code, or at least have the option to do so.

[FiloSottile]

I also was looking for generated operations modulo 2^252 + 27742317777372353535851937790883648493 (the order of the prime-order subgroup of Curve25519), which in implementations we usually refer to as the "scalar field" (because it's the field of the scalars that you perform scalar multiplication of group elements with) as opposed to the "base field" (integers modulo 2^255 - 19).

Almost everyone copy-pasted the same implementation of muladd (a + b * c) in that field (affectiously called the Christmas tree, because of how the multiplication step looks like, see below), and replacing it would be a great starting point for integrating fiat-crypto. I also think it's actually more complicated than the base field, because the prime doesn't have a nice shape.

Indeed, performance is not critical, except for inversion as @briansmith said, which we have a custom implementation for in filippo.io/edwards25519 (by @hdevalence).

(I think this has nothing to do with 121666, which is the denominator of the curve constant, is an element of the base field, and is apparently used in the implementation of group-level point scalar multiplication, so either we are off-topic or the issue should be retitled.)

[hdevalence]

Just to close the circle on that archaeology, if I recall correctly the scalar inversion implementation I added to filippo.io/edwards25519 uses a ladder found by @briansmith :)

[bambers936]

@JasonGross