1
Translation of Rust's core and alloc crates to Coq for formal verification
We continue our work on formal verification of Rust programs with our tool coq-of-rust, to translate Rust code to the formal proof system Coq. One of the limitation we had was the handling of primitive constructs from the standard library of Rust, like Option::unwrapordefault or all other primitive functions. For each…