Split headers: libcrux-iot additions

[jschneider-bensch]

These are the glue additions that make all the extractions build using the upstream glue only.

[protz]

Looks great! I only have a few minor changes but other than that looks good.

Were you able to package libcrux with only some of the headers you need, using this new modular approach?

[protz]

if this function can be called with x1 == 32 (and I think it can), then your implementation exercises undefined behavior in C (which is bad)

for instance, a well-defined Rust program such as fn main () { assert_eq!(1u32.rotate_left(64), 1) } will generate undefined behavior here

[jschneider-bensch]

Oh, is it because of the <<? Would it help to assert(x1 < 32)?

And the same would apply to core_num__u64__rotate_left as well, I assume (where x1 should be less than 64).

[protz]

Oh, is it because of the <<?

yes, shifting by widths greater or equal than the bit width of the type is undefined behavior in C

consider the following Rust program:

fn main() {
    assert_eq!(1u32.rotate_left(32), 1);
}

if you compile and run it in Rust, you get a successful execution

Would it help to assert(x1 < 32)?

Unfortunately no, because if you compile the program above to C via Eurydice, using your suggestion of adding an assert, the program will start crashing.

And the same would apply to core_num__u64__rotate_left as well, I assume (where x1 should be less than 64).

You cannot assume that x1 is < 64 because callers are legally allowed to pick x1 == 64; instead, the implementation must be able to deal with any x1 (because Rust's rotate_left behaves that way).

There are way to implement a rotate macro efficiently for cryptographic libraries. I think there's one called rotl in OpenSSL. Let's see what they do.

[protz]

There's also an intrinsic apparently on some toolchains/platforms: https://learn.microsoft.com/en-us/cpp/c-runtime-library/reference/rotl-rotl64-rotr-rotr64?view=msvc-170

[protz]

Error: the new charon pin does not have the old one as its ancestor. The pin must only move forward.

@Nadrieril did someone rebase or something?

[Nadrieril]

Weird, but I think this will get fixed when new commits get pushed to the branch.

[protz]

Just to recap. I'm waiting on my comment to be fixed: #363 (comment) so that we don't merge something with undefined behavior