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 - Interpreter #593

Open clarus opened 2 months ago

clarus commented 2 months ago

Write a simulation for the evaluation function execute_instruction in https://github.com/move-language/move-sui/blob/main/crates/move-vm-runtime/src/interpreter.rs

There might be a lot of dependencies to this function, that can be cut into smaller pull requests!

InfiniteEchoes commented 2 months ago

With a check into the function signature of execute_instruction, I think the task can be divded based on the types appeared in the signature. I'm creating issues based on them:

    fn execute_instruction(
        pc: &mut u16,
        locals: &mut Locals,
        ty_args: &[Type],
        function: &Arc<Function>,
        resolver: &Resolver,
        interpreter: &mut Interpreter,
        gas_meter: &mut impl GasMeter,
        instruction: &Bytecode,
    ) -> PartialVMResult<InstrRet> { ... }
clarus commented 2 months ago

OK, good idea!