[WIP] Mutable Style for ML-KEM

[karthikbhargavan]

WIP: tranforming ML-KEM to use &muts everywhere.

#947

[karthikbhargavan]

@franziskuskiefer @jschneider-bensch

This branch needs some fixes in order to extract F*, and then lax and typecheck it.
To test the current status run hax.py_extract &> res and inspect the errors in res.
We will be handling these errors incrementally.

In commit 29899aa
I fixed hash_functions.rs to lax-check as an example, so now the first error you will see is in ind_cpa.rs.

The general rules for the transformation are as follows.
For each function in a module:

• if an argument has been turned from an array (e.g. [u8; LEN]) to a slice (&[u8] or &mut [u8]), then we need a pre-condition stating what its length is: #[hax_lib::requires(input.len() == LEN)]
• if an output (e.g. [u8; LEN]) has been turned into a mutable slice input (out:&mut [u8]), then we need both a pre-condition as described above and a post-condition saying that the length did not change (unfortunate to have to do this, but needed for now): #[hax_lib::ensures(|_| fstar!("Seq.length ${out}_future == Seq.length ${out}"))]
• if an output has been turned into a mutable input, and if the function already has a post-condition stated in term of the result (e.g. ensures(| result | fstar!("... result ...."))) then we need to change each reference to result to refer to the future version of the output: ensures(| _ | fstar!("... ${output}_future ...."))

You can see some of these patterns in hash_functions.rs already.
Once you fix these, then hax.py_extract will no longer show errors for your module (even if there are errors in other modules). You can then open the extracted file in proofs/fstar/extraction and try to lax-check it.

Sometimes, the specs will have to be changed more substantially, in which case, comment them out, leave a note for the proofs team, and just try to make sure that the extraction works, and if possible that the output lax-checks.

[karthikbhargavan]

In a follow-up commit fa5d435 I fixed the spec for Spec.Utils.fsti to match the new signature of these functions.

Now all the post-conditions of hash-functions are also fixed for the new style.

[github-actions]

This PR has been marked as stale due to a lack of activity for 60 days. If you believe this pull request is still relevant, please provide an update or comment to keep it open. Otherwise, it will be closed in 7 days.

[jschneider-bensch]

Still relevant, proofs still need to be adapted.

[jschneider-bensch]

In lieu of a full rebase, I locally fixed the hax_lib dependency version and worked through all errors given by hax.py extract, changing |result| ... closures and adding length pre- & postconditions as described above.

Now that this is done we get further into the extraction pipeline and hit large number of different hax errors.

[jschneider-bensch]

Kyber APIs need fixing still.

[karthikbhargavan]

I'll take a look at this later today.

[karthikbhargavan]

I investigated the weird error about DirectAndMut. In these cases, what is happening is that the precondition (or postcondition) is referring to a function like ${Vector::montgomery_multiply_by_constant} which used to be a pure function but is now a function that takes an &mut argument. This kind of function (with mutable inputs) cannot be used in this form in pre- or post-conditions, so we'd need to edit these function calls. I'll think about a good style to do these preconditions and experiment with them.

[karthikbhargavan]

I took this branch further. Now there are some issues in avx2 which are "real" errors, and I am happy to guide on fixes.

[karthikbhargavan]

After a bunch of edits I got this back to laxing mode for ml-kem.
I don't have the energy to try full verification right now, so will set this aside till early next week.