Mutable Style for ML-KEM

[karthikbhargavan]

Transforming ML-KEM to use &muts everywhere.

#947

[skip changelog]

[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.