search

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

Move - Simulations - Verifier - call function #574

Closed clarus closed 2 months ago

clarus commented 4 months ago

Write a simulation for the call function in https://github.com/move-language/move-sui/blob/main/crates/move-bytecode-verifier/src/type_safety.rs

InfiniteEchoes commented 2 months ago

Done in #590 .This function looks like a mere helper function along with others to check the instructions are well-typed.