AeneasVerif / eurydice

Eurydice compiles (a modest subset of) Rust to C. Verify programs in Rust, still get C code for legacy environments.
Apache License 2.0
21 stars 1 forks source link

Clean up config.yml for mlkem using charon#216 #16

Closed msprotz closed 2 months ago

msprotz commented 3 months ago

Once https://github.com/AeneasVerif/charon/pull/216 lands, we will gain the ability to extract type aliases to eurydice, and use that to guide monomorphization.

Right now, in Low*, if you write a type abbreviation whose body is the application of a generic type to concrete arguments (e.g. https://github.com/hacl-star/hacl-star/blob/main/code/streaming/Hacl.Streaming.MD.fst#L192), then you control two things:

I would like to have the same kind of support in Eurydice, once the upstream Charon fix lands.

This would allow us, for instance, to write in Rust the definition of these types: https://github.com/cryspen/libcrux/blob/lucas/extract-intrinsics/libcrux-ml-kem/c.yaml#L143-L151 in, say, libcrux_mlkem::types, and then we could get rid of those.

Generally speaking, we could do the same with every other entry of the form monomorphizations_exact in config.yml

msprotz commented 2 months ago

https://github.com/cryspen/libcrux/commit/3b31006037373a79c6b87de0b4bf00d5fd84e74c does this