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.
Predator
, Trace
. Predator
will record every single Trace
to a vector of Trace
.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
).Predator
from the construction of Engine
to the EngineExecutor
.After executing a Wasm program we have a Vec<Trace>
with this structure:
local.get <index>
The source code is available here https://github.com/orochi-network/wasmi
Mul example:
Add example:
A very simple WebAssembly program:
This program takes two parameters and calculates the sum of them.