ZKVM

Intro

We want to build a ZKP that validates an entire EVM block or as much of it as we can efficiently. Its okay to adjust the gas costs for every EVM opcode. Its also to exclude some opcodes for now if they are super expensive. Its okay to exclude precompiles.

This repo creates a sketch of how this can work as a way to explain but also to get the idea clear in my mind.
Arch

We have two proofs that we use to prove validity of the state transition

Proof 1: State proof

The goal of hte state proof is to remove the checking of reading and wirting to state/memory from the EVM proof. The state proof proves that all of these reads and writes have been done correctly and provides a list of memoryQue and stateQue. These lists are basically the list of things that go into or come off of state/memory. So inside the EVM proof we can have to do much less work when we do memory/state reads and writes.

Another advantage of this is that we are gathering together a group of similar operations state checking. This means we can prepare a proof that targets them specificlaly and saves overhead in the EVM circuit.

[barry] Signatures go here too ?

Proof 2: Execution

For each opcode in the stack we execute it and update the stack.

Each EVM opcode is a custom constraint. We select the custom constraint based upon the stack and execute that.

This means that every opcode is just a set number of custom constraints which allows us to "turn off" the opcodes we are not using.

State proof variables

Private inputs

​​​​StorageMap: An ordered list of the index (Opcodes) of all the opcodes that read/write from state or memory and signature veificaion checks. 

​​​​StateQue: An ordered list of all the State objects that get loaded from or written to the state.

​​​​MemoryQue: An ordered list of variables that get loaded from or written to memory.
​​​​
​​​​stateLocationQue: An ordered list of the location of every state read/write. 
​​​​
​​​​memoryLocationQue: An ordered list of the locaiton of every memory read/write
​​​​
​​​​helperStore[len(transactions)][len(StorageMap[len(transactions)])]: This variable provieds the vaules for sstore and mstore because state proof does not check them at proving time. This check is defered until evm proof. 

Public inputs

​​​​Transactions: A list of transactions that get included in this block. 
​​​​stateCommits: A commitment to ethereum State before and after executing these transactions. 
​​​​**A communitment to all the private variables described above.**

EVM proof variables

Private inputs

​​​​ExectionContext[]: This containts an opcodes instance, MemoryPage instance, stackCount instance , StorageMap and msg.sender.
​​​​
​​​​ExecutionContextIndex: This is the index of the currently exectued ExecutionContext.
​​​​
​​​​stackCount: The position in the stack that the next opcode to be read is from.

Public inputs

​​​​Transactions: A list of transactions that get included in this block. 
​​​​
​​​​StateCommits:
​​​​
​​​​**A commitment to all the private variables described above.**

State proof psudo code

def state_proof(transactions, stateCommitments, storageMap, helperStore): opcodes = [] memoryCommitmnet = [0]*1048 for tx_i, tx in enumerate(transactions): tx.opcodes.append(state_load(tx.to)) for storage_i, storageOpcode in enumerate(storageMap): i = tx.opcodes[storageOpcode] value = tx.opcodes[storageOpcode + 1] if i == sload: result = sload(state, value) stateQue.append(result) stateLocationQue.append(value) if i == sstore to_store = helperStore[tx_i][storage_i] state = sstore(state, location, to_store) stateQue.append(to_store) stateLocationQue.append(location) if i == mload: result = mload(memoryCommitment, value, location) stateQue.append(result) memoryLocationQue.append(location) if i == mstore: to_store = helperStore[tx_i][storage_i] memoryCommitment = mstore(memoryCommitment, location, to_store) stateQue.append(to_store) memoryLocationQue.append(location) # TODO: signature check. # TODO: Call # TODO: Delegate call # TODO all state read opcodes opcode_commitments.append () return(commitStateQue, commitMemoryQue, commitLocationQue)

EVM proof psudo code

def evm_proof(commitTransactions, commitMemoryQue, commitStateQue): memoryQue = commitToList(commitMemoryQue) memoryQueCounter = 0 stateQue = commitToList(commitStateQue) stateQueCounter = 0 storageCount = 0 programCounter = 0 transactions =commitToList(commitTransactions) for tx in transactions: stack = [] for opcode in tx.opcodes: if opcode in [sload, sstore, mload, mstore]: # make sure this opcode was checked in the state zkp assert(storageMap[storageCount] == counter) location = stack.pop() value = stack.pop() if opcode == sload: assert(stateLocationQue[stateQueCounter] == location) stack.push(stateQue[stateQueCounter]) stateQueCounter ++ programCounter += 1 if opcode == sstore: # check the location the storage happened at was correct assert(memoryLocationQue[stateQueCounter] == location) # check this is what was stored assert(stack[0] == value ) stack.pop() stateQueCounter ++ programCounter += 1 if opcode == jump: programCounter = stack[0] stack.pop() if opcode == add: a = stack.pop() b = stack.pop() stack.push(a+b) programCounter += 1 return (True)

Opcodes

state load

//TODO

comparion

Every comparison pops 2 elements from the stack and appends one. With the exception of Not and isZero which only pop 1 element.

https://github.com/ethereum/py-evm/blob/master/eth/vm/logic/comparison.py

Arith

Every Arith opcode pops 2 elements and pushes one with the exception of addmod and mulmod which pop 3.

https://github.com/ethereum/py-evm/blob/master/eth/vm/logic/arithmetic.py

Duplicaion

Dup just copies a stack value to position 0 on the stack. It takes not inputs.

Select a repo