[SHA3 / ML-KEM/ ML-DSA] C extraction

[jschneider-bensch]

This PR provides a C extraction for ML-DSA and updates the C extractions for SHA3 and ML-KEM to work with Eurydice revision cdf02f9d8ed0d73f88c0a495c5b79359a51398fc.

CI will fail at the moment, because the latest published libcrux-c docker image runs an older version of Eurydice. Should work once cryspen/libcrux#1237 is merged.

[jschneider-bensch]

At this point the extraction and build succeed, but the test fails.

[jschneider-bensch]

The failing test was due to an apparently incorrect translation of a .step_by(4) range loop in a cloop! macro. I've replaced that with manual indexing, and now the results are correct.

[keks]

The changes to the Rust code look good to me. There is a bunch of commented old code in the shell script, let's remove that. I like the new logic for handling dependencies, it's a lot cleaner. I expect it works just as well for distinguishing kebab-case and snake-case?

Otherwise I was not able to extract the ML-DSA code, but it looks like it worked for you. Maybe let's talk to see what I am doing wrong.

[keks]

I think this mostly looks pretty good! I just had the pleasure of doing a proper deep update of the glue in another project, so I had that on my mind when I reviewed this, and it looks like this is pretty out of date.

Here is the glue for our Eurydice version, but maybe it has too much stuff in it: https://github.com/AeneasVerif/eurydice/blob/cdf02f/include/eurydice_glue.h

I mostly commented on the one that was added to ML-DSA, but I suppose we might also have in ML-KEM and SHA3.

Otherwise I think this looks good!

[jschneider-bensch]

I removed a bunch of stuff from the glue that you pointed out 👍

Most of the glue will hopefully soon be upstream glue anyway. I tried the split header version of Eurydice and that seemed to work fine, for the most part.

[keks]

Thanks, this looks good to go now!