Complete interpreter instructions at the end - Githubissues

formal-land / coq-of-rust

Formal verification tool for Rust: check 100% of execution cases of your programs 🦀 to make applications with no bugs! ✈️ 🚀 ⚕️ 🏦

GNU Affero General Public License v3.0

418 stars 14 forks source link

Complete interpreter instructions at the end #616

Open clarus opened 2 weeks ago

clarus commented 2 weeks ago

The goal of this issue is to complete the definition of the interpreter for the following instructions:

[ ] PackGeneric
[x] Unpack
[x] UnpackGeneric
[ ] ReadRef
[ ] WriteRef
[x] CastU8
[x] CastU16
[x] CastU32
[x] CastU64
[x] CastU128
[x] CastU256
[x] Add
[x] Sub
[x] Mul
[x] Mod
[x] Div
[x] BitOr
[x] BitAnd
[x] Xor

The interpreter is defined in the file https://github.com/formal-land/coq-of-rust/blob/main/CoqOfRust/move_sui/simulations/move_vm_runtime/interpreter.v