Extracting Execution Trace from WebAssembly Runtime

NOTE: From Chrio (Orochi Network), appendix to ZK VM spec.

To prove arbitrary computation we need to extract the execution trace and prove that every step of the computation is correct. In our case, we want to prove the execution trace of WebAssembly run-time. We pick the wasmi - WebAssembly (Wasm) Interpreter a light weight and deterministic Wasm run-time to start with.

Method

• We created two new structures namely, Predator, Trace. Predator will record every single Trace to a vector of Trace.
• Inject the Predator instance to Executor of wasmi and start extracting before the opcode is executed (wasmi have some engineering turning so we might need to transform to the necessary format of the Trace).
• Passing a single reference of Predator from the construction of Engine to the EngineExecutor.

Format of the trace

After executing a Wasm program we have a Vec<Trace> with this structure:

• iaddr: Address of instruction in the memory
• program_counter: Number of instructions have been executed
• opcode: Opcode has been executed
• stack: The stack of Wasm run-time
• stack_depth: The depth of the above stack
• local: Local variables which can be accessed by using local.get <index>
• local_depth: The depth of local
• calling_frame: Calling frame of Wasm run-time
• calling_frame_depth: The depth of calling frame
• action: Memory access action
• memory_address: Memory address
• memory: Memory chunks

Trace {
    iaddr: InstructionPtr {
        ptr: 0x0000000131607800,
    },
    program_counter: 4,
    opcode: Return(
        DropKeep {
            drop: 2,
            keep: 1,
        },
    ),
    stack: [
        UntypedValue {
            bits: 9,
        },
    ],
    stack_depth: 1,
    local: [
        UntypedValue {
            bits: 4,
        },
        UntypedValue {
            bits: 5,
        },
    ],
    local_depth: 2,
    calling_frame: [],
    calling_frame_depth: 0,
    action: None,
    memory_address: 0,
    memory: [],
}

To test

The source code is available here https://github.com/orochi-network/wasmi

Mul example:

RUST_BACKTRACE=1 cargo run --bin example -- --mul

Add example:

RUST_BACKTRACE=1 cargo run --bin example

A very simple WebAssembly program:

(module
    (func (export "add_values") (param i64 i64) (result i64)
      local.get 0
      local.get 1
      i64.add))

This program takes two parameters and calculates the sum of them.