Prove WASM execution

Proof Generation of a signle execution

In the Proof Phase the web assembly interpreter (wasmi) outputs two traces; the web assembly bytecode as the execution trace & the host API call trace. These record the order of the host API calls and their output. The combination of the two traces ensures the host call trace is in the same order as the execution trace (including the same input arguments).

To generate a single proof using zkWasm using the wasm image generated from the C code above output.wasm, we simply run the ZKWASM VM with that image and provide a public input --public 2:i64 and a private input --private 2:i64 to it.

$ZKWASMBIN/zkwasm-cli --params ./params testwasm prove --output ./output --wasm ./pkg/output.wasm --public 1:i64 --private 1:i64

In the above command --host specifies the host api set we would like to use. Since our application does not relies on any special WASI functions, and --params tells the prover refer to /params folder for all circuit specific data. The --output argument specify the output folder for proof results (together with some intermediate files).

After executing the commnad, it should produce the following files in the output directory --output ./output.

.
├── Makefile
├── output.wasm
├── params
  ├── traces
    ├── external_host_table.json
    ├── jtable.json
    ├── itable.json
    └── testwasm.etable.0.json
  ├── K22.params
  ├── testwasm.circuit.finalized.data
  └── testwasm.zkwasm.data
├── output
  ├── traces
  ├── testwasm.loadinfo.json
  ├── testwasm.0.instance.data
  └── testwasm.0.transcript.data

The overall information of the proof is stored in the zkwasm.loadinfo.json which looks like the following

{
  "k": 22,
  "proofs": [
    {
      "circuit": "testwasm.circuit.finalized.data",
      "instance_size": 4,
      "witness": "testwasm.0.witness.json",
      "instance": "testwasm.0.instance.data",
      "transcript": "testwasm.0.transcript.data"
    }
  ],
  "param": "K22.params",
  "name": "testwasm",
  "hashtype": "Poseidon"
}

A few things in zkwasm.loadinfo.json are worth mentioning at this stage. First of all, the testwasm.circuit.finalized.data file contains all the information about the circuit (vkey, constraints, gate shape, etc). The testwasm.X.instance.data is the public instance for the proof, the testwasm.X.transcript.data is the execution proof generated for the output.wasm with given inputs. XXX.json files in the trace directory are execution trace for debugging purpose and the external_host_table is the trace of the host function calling info (In this example, we do not invoke any host apis thus the external_host_table is empty. Please refer to ZKWASM host circuits for more details).

The process of proof generation requires reading the vkey which is implied by the output.circuit.finalized data and K.params that is generated in the previous Setup Phase. These files in the params folder will be needed in the proof batching phase when we batch several proofs together to generate a single aggregated proof (Please refer to the proof batching phase for more details about proof arrangement and batching).

Proof Verification:

The verification of a proof generated by zkWasm is done using the verify command line arguement. In the below bash script which is execuated from within output_simple_program a single verification run can be done by:

$ZKWASMBIN/zkwasm-cli --params ./params testwasm verify --output ./output

where ZKWASMBIN is the directory of zkWasm.