zkProver debugging

zkProver debugging

Repositories involved

zkproverjs: prover reference implementation writen in javascript
zkproverc: prover implementation writen in C
zkasm: compiles .zkasm to a json ready for the zkproverjs
zkpil: Polynomial Identity Language
zkvmpil: PIL source code for the zkVM (state-machines)
zkrom: zkasm source code of the zkEVM
zkevmdoc: docs zkevm

Setup environment

ideal repository structure:

github
    --> zkrom
    --> zkvmpil
    --> zkproverjs

Next steps are required to run the zkprover:executor:

git clone https://github.com/hermeznetwork/zkrom.git
cd zkrom
npm i && npm run build
cd ..
git clone https://github.com/hermeznetwork/zkvmpil.git
cd zkvmpil
npm i && npm run build
git clone https://github.com/hermeznetwork/zkproverjs.git
cd zkproverjs
npm i

Detailed explanation:
- repository zkrom
  - main/* : contains assembly code
  - build: compiled assembly. code ready to the executor
- repository zkvmpil
  - src: state-machines
  - build: compiled state-machines. code ready to the executor
- repository zkproverjs
  - src/main_executor.js: cli to run executor easily
    - executor needs files fenerated from zkrom/build & zkvm pil/build
    - it also needs an input.json
    - Examples:
Run executor (in zkproverjs repository)

to just test the executor, the output is not needed

node src/main_executor.js ./testvectors/input.json -r ../zkrom/build/rom.json -p ../zkvmpil/build/zkevm.pil.json -o ./testvectors/poly.bin

Executor insights

Basically, the executor runs the program that is specified by the ROM.
The program can be seen in the rom.json file, which includes some debugging information.
Let's see an example of assembly code builded into the rom.json:

ASSEMBLY: 1 => B
JSON FILE:
{
  "CONST": 1,
  "neg": 0,
  "setB": 1,
  "line": 51,
  "fileName": "../zkrom/main/main.zkasm"
 }

All operations are defined in the JSON file, plus line & fileName where the assembly code is.
This JSON file is ready to be interpreted by the executor

VSCode debugging

In the zkproverjs repository you can find an example of launch.json to debug the executor code: https://github.com/hermeznetwork/zkproverjs/blob/main/.vscode/launch.json#L8

Debugging tips

Main executor code to debug: https://github.com/hermeznetwork/zkproverjs/blob/main/src/executor.js#L12
variable l is the rom.json that is going to be executed: https://github.com/hermeznetwork/zkproverjs/blob/main/src/executor.js#L61
debug helpers
- print registers
By monioring ctx(context), registers and op you will see all the states changes made by the executor
ctx.input contins all the variables loaded from input.json
storage makes refrence to the merkle-tree
transactions places at input.json are pre-processed and store it on ctx.pTxs. Besides, globalHash is computed given all the inputs.json according to specification (TO_BE_UPDATED)

Table rom assembly instructions

NAME	DESCRIPTION	EXECUTION
MLOAD	memory load	op = mem(addr)
MSTORE	memory storage	mem(addr) = op
SLOAD	storage load	op = `storage.get(SR, H[A0 , A1 , A2 , B0 , C0 , C1 , C2 , C3, 0...0]))` where `storage.get(root, key) -> value`
SSTORE	storage store	op = `storage.set(SR, (H[A0 , A1 , A2 , B0 , C0 , C1 , C2 , C3, 0...0], D0 + D1 * 2^64 + D2 * 2^128 + D3 * 2^192 )` where `storage.set(oldRoot, key, newValue) -> newRoot`
HASHW	hash write bytes	hash[addr].push(op[0..D-1])
HASHE	hash end	hash[addr].end()
HASHR	hash read	op = hash[addr].result
ARITH	arithmetic operation	AB + C = D OR op
SHL	shift left	op = A << D
SHR	shift right	op = A >> D
ECRECOVER	signature recover	op = ECRECOVER( A: HASH, B: R, C:S, D: V)
ASSERT	assertion	A = op

Examples assembly

MSTORE

assembly


A                       :MSTORE(sequencerAddr)

rom.json










{
  "inA": 1,
  "neg": 0,
  "offset": 4,
  "mWR": 1,
  "line": 9,
  "offsetLabel": "sequencerAddr",
  "useCTX": 0,
  "fileName": ".../zkrom/main/main.zkasm"
 }

description:
load A register in op, write in memory position 4 (offset) the op value

MREAD

assembly:


$ => A          : MLOAD(pendingTxs)

rom.json














{
  "freeInTag": {
   "op": ""
  },
  "inFREE": 1,
  "neg": 0,
  "setA": 1,
  "offset": 1,
  "mRD": 1,
  "line": 25,
  "offsetLabel": "pendingTxs",
  "useCTX": 0,
  "fileName": ".../zkrom/main/main.zkasm"
 }

description:
load a memory value from position 1 (offset) into op (action marked by inFREE), set op in A register

LOAD FROM STORAGE

assembly



$ => A                          :MLOAD(sequencerAddr)
0 => B,C
$ => A                          :SLOAD

rom.json

































 {
  "freeInTag": {
   "op": ""
  },
  "inFREE": 1,
  "neg": 0,
  "setA": 1,
  "offset": 4,
  "mRD": 1,
  "line": 47,
  "offsetLabel": "sequencerAddr",
  "useCTX": 0,
  "fileName": ".../zkrom/main/main.zkasm"
 },
 {
  "CONST": 0,
  "neg": 0,
  "setB": 1,
  "setC": 1,
  "line": 48,
  "fileName": ".../zkrom/main/main.zkasm"
 },
 {
  "freeInTag": {
   "op": ""
  },
  "inFREE": 1,
  "neg": 0,
  "setA": 1,
  "sRD": 1,
  "line": 49,
  "fileName": ".../zkrom/main/main.zkasm"
 }

description
- load from memory position 5 (sequencerAccValue) into op, store op on D register
- load from memory position 4 (sequencerAddr) into op, store op on A register
- load CONST in op, store it in registers B and C
- Perform SLOAD (reading from merkle-tree) with the follwing key: storage.get(SR, H[A0 , A1 , A2 , B0 , C0 , C1 , C2 , C3, 0...0]))
  - SR is the current state-root saved in register SR
  - A0, A1, A2 has the sequencer address
  - B0 is set to 0 pointing out that the balance is going to be read
  - C0,C1,C2,C3 are set to 0 since they are not used when reading balance from merkle-tree
- merkle-tree value is store in op (marked by inFREE tag), set op to register A

WRITE TO STORAGE

assembly



$ => A                          :MLOAD(sequencerAddr)
0 => B,C
$ => SR                         :SSTORE

rom.json

































{
  "freeInTag": {
   "op": ""
  },
  "inFREE": 1,
  "neg": 0,
  "setA": 1,
  "offset": 4,
  "mRD": 1,
  "line": 56,
  "offsetLabel": "sequencerAddr",
  "useCTX": 0,
  "fileName": ".../zkrom/main/main.zkasm"
 },
 {
  "CONST": 0,
  "neg": 0,
  "setB": 1,
  "setC": 1,
  "line": 57,
  "fileName": ".../zkrom/main/main.zkasm"
 },
 {
  "freeInTag": {
   "op": ""
  },
  "inFREE": 1,
  "neg": 0,
  "setSR": 1,
  "sWR": 1,
  "line": 58,
  "fileName": ".../zkrom/main/main.zkasm"
 }

description
- read from memory position 4 (sequencerAddr) and store it on op, set op to register A
- set CONST to op, store op in registers B and C
- Perform SWRITE (write to merkle-tree) according: storage.set(SR, (H[A0 , A1 , A2 , B0 , C0 , C1 , C2 , C3, 0...0], D0 + D1 * 2^64 + D2 * 2^128 + D3 * 2^192 )
  - SR is the current state-root saved in register SR
  - A0, A1, A2 has the sequencer address
  - B0 is set to 0 pointing out that the balance is going to be read
  - C0,C1,C2,C3 are set to 0 since they are not used when reading balance from merkle-tree
  - D0, D1, D2, D3 is the value writen in the merkle-tree pointed out by H[A0 , A1 , A2 , B0 , C0 , C1 , C2 , C3, 0...0] –> in this example register D has the balance of the seqAddr
- write merkle-tree state root in SR register

Syntax	Example	Reference
# Header	Header	基本排版
- Unordered List	Unordered List
1. Ordered List	Ordered List
- [ ] Todo List	Todo List
> Blockquote	Blockquote
Bold font	Bold font
Italics font	Italics font
~~Strikethrough~~	~~Strikethrough~~
19^th^	19^th
H~2~O	H₂O
++Inserted text++	Inserted text
==Marked text==	Marked text
[link text](https:// "title")	Link
![image alt](https:// "title")	Image
`Code`	`Code`	在筆記中貼入程式碼
```javascript var i = 0; ```	`var i = 0;`	在筆記中貼入程式碼
:smile:		Emoji list
{%youtube youtube_id %}	Externals
$L^aT_eX$	L^aT_eX
:::info This is a alert area. :::	This is a alert area.