Types for `strict` and `loose` field elements should prevent misuse

[pornin]

Context is related to this issue in another Rust crate that uses fiat-crypto: https://github.com/crate-crypto/Ed448-Goldilocks/issues/28

In a nutshell: some code is using the p448 field (for implementing computations in the edwards448 elliptic curve). The p448_solinas_64 fiat-crypto backend is used; in that backend, there are two internal representations of integers, called "tight" and "loose", that differ in the allowed range for the value limbs. In the generated Rust code, two distinct type names are defined: https://github.com/mit-plv/fiat-crypto/blob/63a6ba42f418d2031342cf8e63d3e4428c88473d/fiat-rust/src/p448_solinas_64.rs#L23-L29

However, the two names are defined as type aliases to [u64; 8], i.e. from the Rust compiler point of view, these are the same type. In particular, this means that the following code compiles without any error or warning:

pub fn bad_code(z: &mut fiat_p448_tight_field_element,
                x: &fiat_p448_tight_field_element,
                y: &fiat_p448_tight_field_element)
{
    fiat_p448_add(z, x, y);
}

fiat_p448_add() expects the output (first parameter) to be a "loose" value, and here I pass a reference to a variable with the "tight" type, and the compiler sees nothing wrong since these are the same type. The result is a "loose" value disguised as a "tight" value.

In practice, a lot of the routines accept a larger range than what is formally proven correct, so much misuse can be absorbed with no exploitable consequence; this is the case with the Ed448-Goldilocks crate referenced above. But it still means that the formal proof of correctness is lost.

Such misuse would be easier to catch if the "tight" and "loose" types were actually distinct, and not two aliases on the same type. The Rust definition would look like this:

pub struct fiat_p448_loose_field_element(pub [u64; 8]);
pub struct fiat_p448_tight_field_element(pub [u64; 8]);

i.e. simple wrappers which have no actual extra runtime overhead. This would have some source-level impact, though:

• References to limbs would have to be modified, e.g. x[3] becoming x.0[3]. I suppose this would be something to change in the code generator that produced the p448_solinas_64.rs file.
• Callers who instantiate values directly (by providing the limb values) would need to use the appropriate syntax (e.g. fiat_p448_tight_field_element([0u64; 8]) instead of [0u64; 8]). I expect such direct instantiation to be used for tables of precomputed constants (in an elliptic curve context, you would do that for precomputed small multiples of the base point, to speed up point multiplication by a scalar).

The second point means that the suggested change would break source compatibility with some external code that uses this crate.

Here I use the p448 field as example, but a cursory look shows that the same applies to other fields with tight/loose representation duality, and, arguably, also to fields with a Montgomery/non-Montgomery duality.

[andres-erbsen]

I agree that a safer interface seems desirable. I figure an unsurprising code-generator change around here and here would likely do the trick. We don't have a maintainer listed for the Rust backend but based on git history I'll ping @JasonGross, @zoep anyway in case they feel like chiming in. I see two users of our Rust code in the list and both would be affected, but neither seems to use the fiat-crypto types on the upper interface. So it looks like changing this would be feasible and probably feasible for anyone who speaks Rust and can deal with fiat-crypto's Coq code enough to edit the stringification and regenerate fiat-rust. Patches welcome, I am not sure whether/when I would get to it myself.

The C backend could benefit from a similar improvement. It would probably be possible now, but if we do manage to replace the unverified C backend with an improved version of the Bedrock2 backend, the unverified wrappers should totally use structs instead of typedefs.