Stable type names in C extractions

[djmdjm]

This is a feature request for stable type names in the C extraction.

For example, libcrux_ml_kem_mlkem768_portable_encapsulate has this sigature:

static inline tuple_f4 libcrux_ml_kem_mlkem768_portable_encapsulate(
    const Eurydice_arr_5f *public_key, Eurydice_arr_ec randomness) {

There are two problems here.

First the types Eurydice_arr_5f, Eurydice_arr_ec, etc do not obviously reflect the function of the type. Second, the types are not stable from release to release of libcrux.

This isn't a huge hassle to work around. OpenSSH has a block like this that renames the types that I fix up each time I update to a new libcrux release:

typedef Eurydice_arr_c7 libcrux_mlkem768_keypair_rnd;
typedef Eurydice_arr_ec libcrux_mlkem768_enc_rnd;
typedef libcrux_ml_kem_mlkem768_MlKem768KeyPair libcrux_mlkem768_keypair;
typedef Eurydice_arr_5f libcrux_mlkem768_pk;
typedef Eurydice_arr_7d libcrux_mlkem768_sk;
typedef Eurydice_arr_2b libcrux_mlkem768_ciphertext;
typedef tuple_f4 libcrux_mlkem768_enc_result;
typedef Eurydice_arr_ec libcrux_mlkem768_dec_result;

But it is a bit of a hassle 😃 - it would be great if this was maintained automatically by the extraction tools.

[jschneider-bensch]

I recall that we had at one point defined type aliases for the output array types in SHA3, e.g.:

pub type Sha3Digest256 = [u8; 32];

and those were translated to stable type aliases. But if I recall correctly these aliases would then also be used for any translation of [u8;32], not just those that use the alias on the Rust side.

@protz Do you have an idea here, perhaps?

[protz]

Yes, the issue is that the krml compiler first inlines away all type aliases before anything happens, so that subsequent passes do not have to be aware of type aliases.

The monomorphization phase tries to recover from that by seeing if there any type alias lying around that might provide a hint as to a suitable name for e.g. the monomorphized struct for [u8; 32]. But then if there are two, one is arbitrarily chosen, and the name might make sense for one occurrence of [u8; 32] but not all.

The nice solution would be to not do that, and have every phase do e.g. if is_foobar (resolve_aliases t) instead of if is_foobar t. This is quite a bit of feature work.