Split headers into logical units

[protz]

Following multiple conversations, this PR attempts to split headers into logical units to make downstream integration easier. The expected workflow is:

• power users like @keks and @franziskuskiefer use --no-default-include as a eurydice option
• then, in config.yaml, individual headers are added via the include_in_h field: https://github.com/AeneasVerif/eurydice/blob/main/test/libcrux/c.yaml#L64

Please provide feedback to make sure life can be easier for downstream consumers. Thank you.

[franziskuskiefer]

Looks like the handwritten glue files are missing?

[protz]

Classic...

[jschneider-bensch]

I gave this a try on libcrux-iot, where we have extractions for SHA3, ML-KEM and ML-DSA. Extractions go to the {sha3,ml-kem,ml-dsa}/extracted/ directories respectively.

I included the split glue files by symlinking eurydice/include to eurydice-include in the extraction directories, and adding the necessary include_in_h in the configs worked without problems. 👍

For SHA3 and ML-KEM there were some bits of glue missing from the upstream glue. For ML-DSA there were also missing bits, and I had to patch one of the upstream glue files as well. I put the necessary custom modifications into the custom_glue directory for each extraction. Here custom_glue/custom_glue.h are pure additions, and for the case where I had to patch one of the upstream headers (core.h) I put the patched version into custom_glue/core.h.

More detail on what I had to change:

• SHA3:
  • This version of SHA3 is internally different from the mainline libcrux version, so it needed a definition for core::num::u32::rotate_left
• ML-KEM, in addition to the SHA3 bit needed two macro definitions:
  • core_array___Array_T__N___as_mut_slice
  • Eurydice_slice_eq_shared (This one may have been dropped from the upstream glue on accident?)
• ML-DSA, in addition to the SHA3 bit needed a different macro and some things where the name might have changed
  • core_option__core__option__Option_T__TraitClause_0___is_some
  • core_ops_bit__core__ops__bit__BitAnd_u8__u8__for__0__u8___bitand and core_ops_bit__core__ops__bit__Shr_i32__u8__for__0__u8___shr (There are almost identically named functions in the upstream glue.)
  • This may be some cmake misconfiguration, but I had to define KRML_HOST_EPRINTF in the custom glue, since it was not picked up from the karamel includes for some reason.
  • As a patch to core.h I also had to make arguments of two glue functions into const uint8_t* here.

[protz]

I gave this a try on libcrux-iot, where we have extractions for SHA3, ML-KEM and ML-DSA. Extractions go to the {sha3,ml-kem,ml-dsa}/extracted/ directories respectively.

Excellent, thanks for the extensive testing!

I included the split glue files by symlinking eurydice/include to eurydice-include in the extraction directories, and adding the necessary include_in_h in the configs worked without problems. 👍

For SHA3 and ML-KEM there were some bits of glue missing from the upstream glue. For ML-DSA there were also missing bits, and I had to patch one of the upstream glue files as well. I put the necessary custom modifications into the custom_glue directory for each extraction. Here custom_glue/custom_glue.h are pure additions, and for the case where I had to patch one of the upstream headers (core.h) I put the patched version into custom_glue/core.h.

More detail on what I had to change:

* SHA3:
  
  * This version of SHA3 is internally different from the mainline libcrux version, so it needed a definition for [`core::num::u32::rotate_left`](https://github.com/cryspen/libcrux-iot/blob/34a7778be03e250fff932df62147cec2b85ec54b/c/sha3/extracted/custom_glue/custom_glue.h#L18-L20)

Can you upstream this?

* ML-KEM, in addition to the SHA3 bit needed two macro definitions:
  
  * [`core_array___Array_T__N___as_mut_slice`](https://github.com/cryspen/libcrux-iot/blob/34a7778be03e250fff932df62147cec2b85ec54b/c/ml-kem/extracted/custom_glue/custom_glue.h#L23-L25)
  * [`Eurydice_slice_eq_shared`](https://github.com/cryspen/libcrux-iot/blob/34a7778be03e250fff932df62147cec2b85ec54b/c/ml-kem/extracted/custom_glue/custom_glue.h#L27-L29) (This one may have been dropped from the upstream glue on accident?)

Sounds like it's worth upstreaming these as well

* ML-DSA, in addition to the SHA3 bit needed a different macro and some things where the name might have changed
  
  * [`core_option__core__option__Option_T__TraitClause_0___is_some`](https://github.com/cryspen/libcrux-iot/blob/34a7778be03e250fff932df62147cec2b85ec54b/c/ml-dsa/extracted/custom_glue/custom_glue.h#L21-L23)
  * [`core_ops_bit__core__ops__bit__BitAnd_u8__u8__for__0__u8___bitand` and `core_ops_bit__core__ops__bit__Shr_i32__u8__for__0__u8___shr`](https://github.com/cryspen/libcrux-iot/blob/34a7778be03e250fff932df62147cec2b85ec54b/c/ml-dsa/extracted/custom_glue/custom_glue.h#L26-L37) (There are almost identically named functions in the upstream glue.)

Sounds like the upstream name needs to be fixed.

  * This may be some cmake misconfiguration, but I had to define [`KRML_HOST_EPRINTF`](https://github.com/cryspen/libcrux-iot/blob/34a7778be03e250fff932df62147cec2b85ec54b/c/ml-dsa/extracted/custom_glue/custom_glue.h#L39-L43) in the custom glue, since it was not picked up from the karamel includes for some reason.

Are you perhaps compiling in C++ mode?

  * As a [patch to `core.h`](https://github.com/cryspen/libcrux-iot/blob/34a7778be03e250fff932df62147cec2b85ec54b/c/ml-dsa/extracted/custom_glue/core.h#L183-L188) I also had to make arguments of two glue functions into `const uint8_t*` here.

Also good to upstream.

It sounds like all the stuff you had to fix is generally useful. I think it would make your life easier if these fixes were upstreamed, so would you mind submitting a PR (to be merged into this branch) to incorporate your modifications? Thanks!

[jschneider-bensch]

Are you perhaps compiling in C++ mode?

Yes, it must be something like that. Updating the macro definition in krml/internal/target.h as follows solves the issue:

#if ((defined(__STDC_VERSION__) && __STDC_VERSION__ >= 199901L) || \
     (defined(__cplusplus) && __cplusplus > 199711L)) &&           \
    (!defined(KRML_HOST_EPRINTF))
#define KRML_HOST_EPRINTF(...) fprintf(stderr, __VA_ARGS__)
#elif !(defined KRML_HOST_EPRINTF) && defined(_MSC_VER)
#define KRML_HOST_EPRINTF(...) fprintf(stderr, __VA_ARGS__)
#endif

In this particular case (libcrux-iot) we'll eventually want to not include that header when building for embedded platforms, but thought you'd be interested anyway.

It sounds like all the stuff you had to fix is generally useful. I think it would make your life easier if these fixes were upstreamed, so would you mind submitting a PR (to be merged into this branch) to incorporate your modifications? Thanks!

Sure 👍 PR'd as #363.

[franziskuskiefer]

Would it make sense to also not include krml headers by default? For example base.h includes target.h. But that's not needed in many cases.

[protz]

Yes, I am open to moving the inclusion of target.h into eurydice.h itself, so that power users can just include base.h and then define KRML_FOR_XXX macros themselves (unless you are disabling static loop unrolling). That's a good suggestion. @jschneider-bensch if you want to do that on this PR go ahead.