We are continuing our formal verification work for the implementation of the type-checker of the Move language in the π§Β Sui blockchain. We verify a manual translation in the proof system πΒ Coq of the π¦Β Rust code of the Move checker as available on GitHub.
In this blog post, we present in detail the verification of a particular function AbstractStack::pop_eq_n
that manipulates πΒ stacks of types to show that it is equivalent to its naive implementation.
All the code presented here is on our GitHub at github.com/formal-land/coq-of-rust π§βπ«.