3 posts tagged with "Move"

This is the last article of a series of blog post presenting our formal verification effort in  Rocq/Coq to ensure the correctness of the type-checker of the Move language for Sui.

Here we show how the formal proof works to check that the type-checker is correct on a particular instruction, for any possible initial states. The general idea is to symbolically execute the code step by step on the type-checker side, accumulating properties about the stack assuming the type-checker succeeds, and then to show that the interpreter will produce a stack of the expected type as a result.

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 🧑‍🏫.

In this blog post, we present our project to formally verify the implementation of the type checker for smart contracts of the 💧 Sui blockchain. The Sui blockchain uses the Move language to express smart contracts. This language is implemented in 🦀 Rust and compiles down to the Move bytecode that is loaded in memory when executing the smart contracts.

We will formally verify the part that checks that the bytecode is well-typed, so that when a smart contract is executed it cannot encounter critical errors. The type checker itself is also written in Rust, and we will verify it using the proof assistant Coq 🐓 and our tool coq-of-rust that translates Rust programs to Coq.