FStarLang / karamel

KaRaMeL is a tool for extracting low-level F* programs to readable C code
Apache License 2.0
394 stars 58 forks source link

A new option for short names -- could potentially be useful generally #457

Closed msprotz closed 1 month ago

msprotz commented 1 month ago

This adds support for short names in monomorphized instances. For code that relies heavily on those (such as the code produced by the Eurydice frontend), this replaces a deterministic, pretty-printed name, such as libcrux_ml_kem_ind_cca_generate_keypair_unpacked__libcrux_ml_kem_vector_neon_vector_type_SIMD128Vector_libcrux_ml_kem_hash_functions_neon_Simd128Hash_3size_t_1152size_t_2400size_t_1184size_t_1152size_t_2size_t_128size_t, by the name of the generic function, followed by a hashcode of the instantiation function's type- and expression-level arguments, and produces this instead:

/**
A monomorphic instance of libcrux_ml_kem.ind_cca.generate_keypair_unpacked with
types libcrux_ml_kem_vector_neon_vector_type_SIMD128Vector,
libcrux_ml_kem_hash_functions_neon_Simd128Hash and with const generics:
- K = 2
- CPA_PRIVATE_KEY_SIZE = 768
- PRIVATE_KEY_SIZE = 1632
- PUBLIC_KEY_SIZE = 800
- BYTES_PER_RING_ELEMENT = 768
- ETA1 = 3
- ETA1_RANDOMNESS_SIZE = 192
*/
libcrux_ml_kem_ind_cca_unpacked_MlKemKeyPairUnpacked__libcrux_ml_kem_vector_neon_vector_type_SIMD128Vector__2size_t
libcrux_ml_kem_ind_cca_generate_keypair_unpacked_32

There could probably be similar improvements for type names.

msprotz commented 1 month ago

This PR now does the same for type names, provided the short names option is activated. There's also a bonus feature in which tuples of a repeated single type t get pretty-printed as t_xN where N is the size of the tuple.

msprotz commented 1 month ago

(Got an everest green locally, which is not surprising since this is off by default)