In this blog post we present how represent a proof of execution for translated 🦀 Rust programs in 
Rocq/Coq, to show that it is possible to type the values and resolve the names. Resolving the names amounts to finding the trait instances and an ordering for the function definitions.
We call these proofs of execution "links". They do not contain memory allocation strategies, which can be defined later in a second step called "simulation". From these links we have all the information to extract a typed execution that is equivalent to the translated code from coq-of-rust. The core of the work presented in this article is in the file CoqOfRust/links/M.v on GitHub.