search

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

Attempt to unify implicit and explicit lifetime declarations #441

Closed R1kM closed 2 months ago

R1kM commented 2 months ago

As part of the Rust extraction of HACL*, several functions are not extracted with messages such as the following:

translating Hacl.Streaming.Blake2b_32.reset_raw: Krml.Warn.Fatal("type mismatch;\n  e=(@7).fst\n  t=&'a mut [hacl::hash_blake2b::blake2_params <'a>]\n  t_ret=&mut [hacl::hash_blake2b::blake2_params]\n  x=@7.fst")

The reason is that there is a mismatch between the inferred and the expected type, as the inferred type includes explicit lifetime annotations. This PR aims to provide a best-effort workaround, by comparing types with lifetime annotations erased. The soundness of this comparison will be left to the Rust borrow-checker, in particular, incorrect cases where there would truly be a mismatch (e.g., because of different lifetimes in t and t_ret, or because of multiple lifetimes) will be extracted by karamel with this patch, but will fail Rust compilation.