Make libcrux-ml-kem lax check in F*

[karthikbhargavan]

This PR addresses #301

It extracts F* code for libcrux-ml-kem and typechecks the resulting code in lax mode. Running ./hax.py extract generates F* code for portable, avx2, and neon versions. And all the code now lax typechecks by running make within proofs/fstar/extraction.

This PR depends on the corresponding hax PR that adds the necessary new library functions and types: cryspen/hax#769 (merged)

It also currently relies on one manual edit to the generated F*, which we need to resolve before merging this PR:
See 91b12cf
It relies on helping F* with typeclass inference using the hax-lib::fstar macro (see f77dc3b)

In the F* extraction driven by hax.py, one major change is that we now extract only the interface for hash_functions.rs and not the code, and this allows us to break the dependency on libcrux-sha3, significantly simplifying our task for verification. The advantage is that the F* code generated from libcrux-ml-kem no longer depends on any F* code or interfaces generated in libcrux-sha3. The drawback is that the code in libcrux-ml-kem/hash_functions.rs is no longer extracted to F*, only its interface is. In a future PR, we should separately aim to extract and check libcrux-sha3 and link it properly to hash_functions.rs (#395)

We also edited the Rust code in the following ways:

• The first change is that we rewrote the code in vector/portable/serialize.rs, vector/portable/ntt.rs, vector/avx2/serialize.rs, andvector/neon/serialize.rs to factor out the core functions and reduce redundancy. We primarily did this to help F* handle the generated code (it was running out of memory with the previous code) but this rewrite also reduces the size of the Rust code and we hope it makes the source code more readable.

• Second, we had to make some slightly annoying changes to the Rust code that were needed as a workaround for this issue: Double return bug hax#720 These changes can be reverted when the hax issue is resolved.

The generated C code (via c.sh and boring.sh) compiles and passes tests.

Review re-requested

[franziskuskiefer]

I made a couple changes to clean this up. We should change deserialize_4_int, then we can get this in.

[franziskuskiefer]

Let's get this merged and then incrementally get the modules to typecheck.