Translation of the Rust's core and alloc crates
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::unwrap_or_default or all other primitive functions. For each of these functions, we had to make a Coq definition to represent its behavior. This is both tedious and error prone.
To solve this issue, we worked on the translation of the core and alloc crates of Rust using coq-of-rust. These are very large code bases, with a lot of unsafe or advanced Rust code. We present what we did to have a "best effort" translation of these crates. The resulting translation is in the following folders:
This work is funded by the Aleph Zero crypto-currency to verify their Rust smart contracts. You can follow us on X to get our updates. We propose tools and services to make your codebase bug-free with formal verification.
