C extraction for ML-DSA

[franziskuskiefer]

This PR makes all necessary to extract C code from ML-DSA.

• It updates the F* code that still laxes.
• It includes a minimal self test.

To generate the C code, run

./c.sh --config cg.yaml --out cg --no-glue --no-unrolling --no-karamel_include --no-karamel_include --mldsa65

Follow ups

• The generated code right now needs to be edited to remove the empty structs (see Drop (empty) unused structs AeneasVerif/eurydice#107).
• The C boilerplate, tests, benchmarks need to be cleaned up in a follow up.
• The avx2 variant may still have issues.
• The stack size used by the C code is too large.

Note that this PR is on top of #707.
This works towards #706 but doesn't close it yet (see follow ups).

[keks]

Some of my comments are nits, some a questions, but I think by and large this isn't controversial :)

[keks]

Should these impls somehow prevent using this sponge in a duplex way (i.e. absorbing after squeezing)? My understanding is that a duplex is not an xof

[franziskuskiefer]

That's what it did before. But I don't think we should do that here. It's only creating more boilerplate when using it. This is not a general purpose sha3 implementation right now that people should be using (unless they know what they are doing).

[keks]

They did that on a type level, I was just thinking of setting a bit when squeezing and then panicking when trying to squeeze. But I hear you wrt. not a general purpose SHA3, so it should be fine, as long as we know that we use it correctly. Does that follow from our proofs?

[keks]

What's the difference betwen DsaXof and Xof?

[franziskuskiefer]

This (DsaXof) is not actually a full Xof implementation but opererates only on multiple of blocks. That's enough for the algorithm. But not enough to hash the messages. That's where we need a proper Xof. That's why we needed to add a proper Xof here for DSA. This needs to get cleaned up in sha3. As part of that we should clean up names here too.

[keks]

Got it. Can we add that as a comment?

Review re-requested