p521: Update fiat-crypto + fiat-constify

[MasterAwesome]

The fiat-crypto version is v0.0.24 and the fiat-constify from RustCrypto/utils#978 was used

[tarcieri]

Seems like some updates to the macros in primeorder will be required.

I'm also curious if there were some sort of loose/tight-related type errors in the previous implementation which the newtypes can catch, since something is amiss with p521 but I never figured out what (it uses fiat-crypto's Solinas prime codegen for the base field, which is different from everything else)

[MasterAwesome]

Seems like some updates to the macros in primeorder will be required.

I'm also curious if there were some sort of loose/tight-related type errors in the previous implementation which the newtypes can catch, since something is amiss with p521 but I never figured out what (it uses fiat-crypto's Solinas prime codegen for the base field, which is different from everything else)

Yep the type errors were what I was going to look into first. I should really make this PR into a draft. If we update primeorder, since it's not versioned and used from path it might require an update to all dependents.

I just put it up here for analysis. The change ready for review is fiat-constify and this contains the generated code for now.

Alternatively we can find the problem possibly using this for p521 and then just use the old generated code, but I'm guessing this change has to happen at some point, might as well do it now. What do you think?

[tarcieri]

If we update primeorder, since it's not versioned and used from path it might require an update to all dependents.

You can remove the path directive from the other crates so they use the released crate.

[MasterAwesome]

If we update primeorder, since it's not versioned and used from path it might require an update to all dependents.

You can remove the path directive from the other crates so they use the released crate.

Sounds good I'll bump up the major version then since this will be a breaking change.

[MasterAwesome]

@tarcieri doesn't look like an issue related to types, although I noticed something incorrect with the U576 array constructed for GENERATOR, EQUATION_A and EQUATION_B. The bigint generated U576 for the incorrect array (Below for GENERATOR):

[
    17977945514697932134,
    3695401138005885595,
    18311004035940853982,
    11622487132578732328,
    17881735149126499770,
    11269274249489003809,
    11402774946092790850,
    9623636836853541325,
    198,
]

Expected

[
    107662193291804006,
    156764387973048062,
    5200896066446132,
    135037196563642487,
    30202750027516766,
    94555012806093784,
    97746763129557904,
    263238996462508174,
    55878890433217540,
]

Dumping the limbs makes the problem a little more evident:

Got

[
    Limb(0xF97E7E31C2E5BD66),
    Limb(0x3348B3C1856A429B),
    Limb(0xFE1DC127A2FFA8DE),
    Limb(0xA14B5E77EFE75928),
    Limb(0xF828AF606B4D3DBA),
    Limb(0x9C648139053FB521),
    Limb(0x9E3ECB662395B442),
    Limb(0x858E06B70404E9CD),
    Limb(0x00000000000000C6),
]

Expected

[
    Limb(0x017E7E31C2E5BD66),
    Limb(0x022CF0615A90A6FE),
    Limb(0x00127A2FFA8DE334),
    Limb(0x01DFBF9D64A3F877),
    Limb(0x006B4D3DBAA14B5E),
    Limb(0x014FED487E0A2BD8),
    Limb(0x015B4429C6481390),
    Limb(0x03A73678FB2D988E),
    Limb(0x00C6858E06B70404),
]

My guess is that the from_hex function forces the extra padding zeroes causing something to be done incorrectly per limb.

Correcting the generator point multiplication no longer overflows and scalar multiplication of G works as expected:

    let l = (FieldElement::from_u64(3) * (x1.square()) + NistP521::EQUATION_A)
        * (y1.double()).invert().unwrap();
    let l2 = l.square();
    let x3 = l2 - x1.double();
    let y3 = l * (x1 - &x3) - y1;

I'm guessing the issue when U576 is constructed from hex since it takes the first 8 bytes which is 00000000000000c6 as a single limb

This also means we can avoid all changes and just fix this part and add all the arithmetic tests needed. I'm confused about the usage of U576 here why not U528

[tarcieri]

This also means we can avoid all changes and just fix this part and add all the arithmetic tests needed. I'm confused about the usage of U576 here why not U528

There is no U528 because 528 does not evenly divide by 64. 9 * 64 = 576, which is the smallest number of 64-bit integers that a P-521 field element can be represented with (i.e. on a 64-bit machine where we want to use integers which match the native word size). It also matches the number of limbs the generated fiat-crypto code uses.

That said, fiat-crypto appears to be using an unsaturated limb size smaller than 64-bits for efficiency purposes:

/// The type fiat_p521_tight_field_element is a field element with tight bounds.
/// Bounds: [[0x0 ~> 0x400000000000000], [0x0 ~> 0x400000000000000], [0x0 ~> 0x400000000000000], [0x0 ~> 0x400000000000000], [0x0 ~> 0x400000000000000], [0x0 ~> 0x400000000000000], [0x0 ~> 0x400000000000000], [0x0 ~> 0x400000000000000], [0x0 ~> 0x200000000000000]]

If I'm reading that right, tight field elements use 59-bit unsaturated limbs, except for the last which is 58-bit.

Loose field elements appear to use 56-bit limbs.

crypto-bigint uses 64-bit saturated limbs, which is an incompatible representation, and that indeed appears to be the bug.

The best way to fix it would probably be to change FieldElement::from_uint_unchecked to convert from the saturated to unsaturated form. As a quick hack you could probably encode the provided Uint to bytes, and use the generated from_bytes function in p521_64.rs to decode to the unsaturated representation.

[MasterAwesome]

crypto-bigint uses 64-bit saturated limbs

Ah that makes sense. Ok the fix seems straightforward, let me make it so I don't need to touch any of the other files. I could also fixup from_hex to discard the first few bytes and do a from_bytes with it so the values match although this side effect seems have a consequence on readability. I think we should remove from_hex from FieldElement and LooseFieldElement. What do you think?

I'm guessing the only few things required to move it from wip-arithmetic are tests. I can add that in a separate PR when I get time.

For future fiat-crypto using crates should we still merge the change for fiat-constify? I think the new-type would definitely help ease up a few issues down the line.

[tarcieri]

Upgrading all of the crates sounds good, although I was hoping to see at least one POC of the updated fiat-constify working before merging since otherwise we don't have any tests for it.

[MasterAwesome]

Upgrading all of the crates sounds good, although I was hoping to see at least one POC of the updated fiat-constify working before merging since otherwise we don't have any tests for it.

Yeah sounds good, I'll do the upgrading as a part of another patch to unblock whoever wants to work with the wip-arithmetiv. I can start another PR with a POC for a working arithmetic nist curve which has existing tests like P256.

EDIT: This patch already has the groundwork for fiat-constify POC. Let me create another PR for the from_hex fixing

[tarcieri]

p256 has handwritten field impls which are faster than the ones generated by fiat-crypto. p192, p224, or p384 are good choices, however.

[MasterAwesome]

The best way to fix it would probably be to change FieldElement::from_uint_unchecked to convert from the saturated to unsaturated form.

How does the carry look for this to work? The hack works as expected but, without the hack I'm guessing we get a [u64; 9] of saturated limbs that we need to convert to unsaturated 59-bit, I mask the lower 59-bits and then I'm guessing I use the upper 5 bits as carry although I'm not quite sure on how to write this transformation, could you guide me through it?

[tarcieri]

You can use fiat_p521_from_bytes to decode to a fiat_p521_tight_field_element.

Everything that touches fiat_p521_tight_field_element should really be mediated through one of the functions exposed from the fiat-crypto generated code, so e.g. all carry propagation is handled by the formally verified arithmetic.

Likewise the encoding needs to be changed to fiat_p521_to_bytes to convert out of fiat_p521_tight_field_element

[MasterAwesome]

Implemented this here: #945

[tarcieri]

I opened a tracking issue for the current issues with p521 field arithmetic: #947

#946 adds some basic tests which are currently failing.