Use fiat-crypto for Fp128 and other fields

[armfazh]

fiat-crypto code generator is currently used for Fp255, however it can also be used for other fields, such as Fp128.

[divergentdave]

I looked into this briefly a while back, and I found that the word-by-word Montgomery synthesis program had issues when the prime modulus fit in only one machine word. It appeared that the IR expressions were of an unexpected shape, or they were being split into statements incorrectly. This would be nice to do, but it'll require some upstream work first, I think.

[armfazh]

It is true that fiat-crypto has issues with single-word arithmetic, it only works with multi-precision. So, it's applicable in the case of Fp128 using 2 words of 64-bits, or Fp64 using 2 words of 32-bits.

[cjpatton]

I don't think I understand the situation: if we split the u128 into two u64s, would fiat-crypto generate faster code? Or is there something we'd need to fix in fiat-crypto in order to get fast code for our (relatively small) fields?

[armfazh]

fiat-crypto cannot produce is single-word implementations. For example, it cannot generate code for the Fp32 or Fp64 fields using (one) word of 64 bits.

On the other hand, fiat-crypto can produce code for 128-bit primes (internally numbers are split in two 64-words), and this is the case shown in #758.

[divergentdave]

As an example, running ./src/ExtractionOCaml/word_by_word_montgomery --lang Rust --inline field64 64 18446744069414584321 mul square add sub opp from_montgomery to_montgomery to_bytes from_bytes nonzero selectznz produces several typedefs, followed by a dump of fiat-crypto IR at various stages of the pipeline, and this error:

In fiat_field64_opp:
Stringification failed on the syntax tree:
(λ x1,
  let x2 := (uint64_t, uint1_t)(Z.sub_get_borrow((2^64), (0, (uint64_t)(x1[0])))) (* : uint64_t, uint1_t *) in
  let x3 := (uint64_t, uint1_t)(Z.add_get_carry((2^64), ((uint64_t)(uint64_t, uint1_t)x2₁, (uint64_t)((uint64_t)(Z.zselect((uint1_t)(uint64_t, uint1_t)x2₂, (0, (2^64-1)))) & 0xffffffff00000001)))) (* : uint64_t, uint1_t *) in
  (uint64_t)(uint64_t, uint1_t)x3₁ :: []
)
Which with some casts elided is:
(λ x1,
  let x2 := Z.sub_get_borrow((2^64), (0, (uint64_t)(x1[0]))) (* : uint64_t, uint1_t *) in
  let x3 := Z.add_get_carry((2^64), ((uint64_t)x2₁, (uint64_t)(Z.zselect((uint1_t)x2₂, (0, (2^64-1))) & 0xffffffff00000001))) (* : uint64_t, uint1_t *) in
  x3₁ :: []
)
Error in converting fiat_field64_opp to Rust:
Invalid identifier in arithmetic expression Z.zselect

Fatal error: exception Failure("Synthesis failed")

Note that 18446744069414584321 is a 64-bit modulus, and we specified 64 bits for "machine_wordsize".

[cjpatton]

@armfazh an incremental step we can take is to use fiat-crypto for Field64. We wouldn't have the same perfromance issue for a field that fits in a single word, right?

[divergentdave]

We can't implement Field64 with a 64-bit word size until some improvements are made to fiat-crypto, to plumb in a rewrite pass that fixes the above error. Until then, Field64 could only be implemented with smaller word sizes.

[cjpatton]

Ah so it's the same problem as for Field128?

[divergentdave]

Code generation for Field128 with a 64-bit word size works, it's just slower than the existing handwritten routines for a few reasons (see #758).