owned this note
owned this note
Published
Linked with GitHub
# plookup for execution transcript creation in zkevm
## Intro
Byte code is hard to move to snark. one reason is jumps because each opcode can jump to any other there needs to be a way to follow these jumps in the circuit. One approch requies adding opcdoes for proving an opocde is in an accumulator. This costs alot of constriatns with 1000s requried per step for this.
To over come this we use plookup to allow the prover to select any order of opcodes they want. Then we check each opcode against a program counter in the evm proof to ensure the selected order is correct.
plookup lets you prove that the elements of f are also containted in t. For example if `t = [1,2,3,4]` and `f = [1,2,3]` this will pass a plookup check but
`t = [1,2,3,4]` and `f = [1,2,5]` would not because 5 is not in t.
This can be tought of as a way of doing
``` python
for element in f:
assert(element in t)
```
Repeats are allowed and it costs ~ 1 constirant per check once you do enough checks to overcome the constant cost.
## Deployment time
At deployment time a user supplies
```
opcodes = [add, mul, jump, add , mul, jumpdest, term]
```
We take these opcodes , add an index to each and this is our table t we call this `t_opcodes`.
```
t_opcodes = [0add, 1mul, 2jump, 3add, 4mul, 5jumpdest, 6term]
```
## State proof
During our state proof stage we allow the prover to select any opcodes from our t_opcodes. We don't check validity here but will check later.
So we have selected opcodes
execution_opcodes = [0add, 1mul, 2jump, 5jumpdest, 6term]
## execution proof
In our execution proof we require that the index of the first opcode is 0. This is to ensure that we don't jump into the middle of the byte code skipping some checks.
Then each time we incrament our program counter we check that the index of the next opcode matches it. This way we can jumpt forward or backwards and repeat opcodes.
```python=
def execution_proof(execution_opcodes):
program_counter = 0
for i, opcode in execution_opcodes:
assert(program_counter == i)
# execute the current opcode and get the next one to execute
next_opcode = execute(opcode)
program_counter = next_opcode
```
## Why is this secure
This is secure because even tho they prover can select any opcode they can only select one opcode for any index. This means that they cannot skip an opcode because the index will not match the program counter. Also they cannot add an opcode that does not belong there because then the program counter will be less than the index of that opcode.
## Repeat opcodes
Lets say we have a while loop defined in bytecode
t_opcodes = [0add, 1mul, 2jump, 3jumpdest, 4mul, 5jumpi, 6term, 7jumpdest, 8add, 9jump]
Where we do 0add, 1mul, 2jump (to index 7), add, jump to index 3 ,mul if stack[0] == 1 jump to index 6 else term.
This is a kind of while loop where we continue multiplying the first two stack elements until stack[0] == 0 then we exit.
So how does this work with plookup. Our prover calculates how many times our while loop needs to be executed and contructs our execution trace based upon this many iterations. This can be variable depending upon how many iterations are required. For example lets say we do for 4 iteraction
execution_opcodes = [0add, 1mul, 2jump, 7jumpdest, 8add, 9jump, 3jumpdest, 4mul , 5jumpi, 3jumpdest, 4mul , 5jumpi, 3jumpdest, 4mul , 5jumpi, 3jumpdest, 4mul , 5jumpi, term ]
This works really well in our evm proof. The opcodes for our execution proof get turned on and we only need to worry about the ones that are turned on. Our prover helps by giving these opocdes in order. But they can't cheat because we check every index and opcode in the evm proof.
## Can we do this on the opcode level?
Some opcodes are actually multiple opcodes. For example add is 4 opcodes really
1. pop first element from stack
2. pop second element from stack
3. add the elements together
4. push the result onto the stack.
t_opcodes= [0add,1term]
We then add a concept of opcode_counter (similar to program_counter) to our constrataint selector polynomial.
execution_opcodes = [0add, 0add, 0add, 0add]
```python=
def execution_proof(execution_opcodes):
program_counter = 0
opcode_counter = 0
for i, opcode in execution_opcodes:
assert(program_counter == i)
# execute the current opcode and get the next one to execute
next_opcode, opcode_counter = execute(opcode, opcode_counter)
program_counter = next_opcode
```
Then during our execute add we update opcode_counter 3 times and then finally update program_counter when we execute the final step of addition.
### Another example: returndatacopy
returndatacopy is a difficult opcode to support because the number of iteractions depends upon the size of the return data which is variable. to support this we use a similar trick that we do with add but have a variable check rather than a constarnt 4 repeats.
```python=
def execution_proof(execution_opcodes):
program_counter = 0
opcode_counter = 0
for i, opcode in execution_opcodes:
assert(program_counter == i)
# execute the current opcode and get the next one to execute
next_opcode, opcode_counter = execute(opcode, opcode_counter)
if (opcode_counter == returndatasize):
program_counter += 1
```
Now we can repeat returndatacopy until all of the data has been copied onto the stack. We have the prover provide the number of repeats we need and the evm proof just verifies this was enough to copy all the data.
### Another example : hash function
A very annoying thing about hash functions is that they take many more constraints in zkp than any of our other opcodes. So if we were to include them we would have to add constant overhead to every other opcodes. We can avoid this by using a similar trick that we use with add. Just repeat the round of the hash function until everything has been executed.