Translation of the Rust's core and alloc crates | Formal Land

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.

[mukaken]

形式的検証のためのRustのコアとalloc cratesのCoqへの変換