Update Eurydice for combined header-only C extraction of ML-KEM & ML-DSA

[djmdjm]

Would it be possible to make a c_header_only extract for ML-DSA, similar to the existing one for ML-KEM.

AFAIK the existing libcrux-ml-dsa/cg extract targets C++, but I'd like to use libcrux' ML-DSA support in OpenSSH, which is a vanilla C project.

[jschneider-bensch]

I think it should be possible to get a C header only extraction and we're certainly open to it! It's more a question of when we can fit in the work at the moment.
We'll discuss what it would take and see when we could schedule it. I'll update here when we know more.

[jschneider-bensch]

We'll try to get this done within the next two weeks.

[djmdjm]

Thanks very much for doing this. However the extraction contains C++isms, e.g. the use of Result constructors, repeated named unions that collide in the namespace and a couple of other things.

For example https://github.com/cryspen/libcrux/blob/46cab2e6de2b364d02f89f4f0b62356d846b11a2/combined_extraction/generated/libcrux_mlkem768_portable.h#L69 uses a C++ constructor whereas the libcrux-ml-kem/extracts/c_header_only implementation uses the KRML_CLITERAL() to adapt between C and C++ depending on the compiler: https://github.com/cryspen/libcrux/blob/46cab2e6de2b364d02f89f4f0b62356d846b11a2/libcrux-ml-kem/extracts/c_header_only/generated/libcrux_mlkem768_portable.h#L113-L115

For now I've worked around them with a truly hideous hack in our import script, but would it be possible to get the extract done with the same settings as libcrux-ml-kem/extracts/c_header_only? Would you prefer I file a separate issue for this?

[jschneider-bensch]

Ah, I'm sorry about that. I'll re-open this issue and give it another try.

[jschneider-bensch]

Indeed, the extraction had a configuration flag set that forced it to C++17 compatible code.
Could you have a look at whether the code on this branch looks better? main...jonas/combined-extraction-fix

[djmdjm]

That's much better, thanks! I'll just ask one of the other developers who was having more trouble with an old gcc to test too, but this look like it will resolve the problem.

[djmdjm]

I noticed another problem. This code

https://github.com/cryspen/libcrux/blob/399ea12dd50814c6edca2b1f935809dcefc425c1/combined_extraction/generated/libcrux_mldsa65_portable.h#L4734-L4735

is undefined behaviour because it shifts a negative number. ubsan catches this. It looks like a total no-op and the shift could safely be removed AFAIK

[djmdjm]

Confirming that the new extract works with the old gcc too.

[jschneider-bensch]

I noticed another problem. This code

libcrux/combined_extraction/generated/libcrux_mldsa65_portable.h

Lines 4734 to 4735 in 399ea12

libcrux_ml_dsa_simd_portable_arithmetic_reduce_element(simd_unit->data[i0] <<
(uint32_t)(int32_t)0);
is undefined behaviour because it shifts a negative number. ubsan catches this. It looks like a total no-op and the shift could safely be removed AFAIK

I think this may be an issue in Eurydice, which we use for the extraction. Trying to find out if it's perhaps already addressed in a more recent revision.