At the moment every node on ethereum has to validate every transaction in the ethereum virtual machine. This means that every transaction adds work that everyone needs to do to verify Ethereum's history. Worse still is that each transaction needs to be verified by every new node. Which means the amount of work a new node needs to do the sync the network is growing constantly. We want to build a proof of validity for the Ethereum blocks to avoid this.
This means making a proof of validity for the EVM + state reads / writes + signatures.
To simplify we separate our proofs into two components.
Only after verifying both proofs are we confident that that Ethereum block is executed correctly.
TODO: high-level description of how these two circuits are connected, i.e. they consume the same bus mapping
ying tong
l1txl2txl2txs from users, verifies them, generates witness and proof, and sends it to the zkevm verifier. They use a l1tx to provide these proofs to the zkevm verifier.barryWhiteHat Possibly can remove slot if we can use custom constarints
note to self: "slot" = "number of rows"
ying tong
barryWhiteHat possibly can remove the notation of multislot opcodes as every opcode would be multiple slots.
slot_counter and don't increment the program counter.is it the case that each opcode uses one slot, and each slot uses a variable number of rows?
ying tong
I think it's NOT. From my point of view, Slot is one bundle of contraints to implement fixed functions. For normal opcode, one Slot is enough. For complicated opcode, possibly more slots should be composed.
Star.LI
would it be accurate to say that the Global Counter counts the number of reads and writes?
ying tong
Yes But it is also used to distinguis between where you are in a multi slot opcode. For call data copy you use global counter to move to the next step during that step.
I feel global counter is very important and used in many places to guarentee many things.
We use it in our arguments about security https://hackmd.io/Hy_nqH4yTOmjjS9nbOArgw#Proof
barryWhiteHat
TODO: types
ying tong
Similar to a bus in a traditional computer the bus_mapping is used to transfer information from storage, memory and stack ops to the EVM proof.
i
A global counter that increments for every slot of the EVM proof.
The id of the transaction/separate call context we are currently executing
Is the value of program_index to the opcode we need to verify.
The location of an opcode in the L2 contract's bytecode.
A Memory key-value mapping of global_counter -> index -> value
Defines the type of memory action this is. For example 0 is read , 1 is write.
A key-value mapping for storage reads/writes. global_counter -> index -> value
Defines what type of storage op to do.
A key-value mapping for each stack op.
Defines the type of stack op
This is the current opcode to execute.
One of the big challenges of building a snark to verify a VM is that you need to be able to read random values / opcodes at any time. To do this we use key-value mappings. Key value mappings are basically random linear combinations of all elements
In plookup you can build key-value mappings as follows
def build_mapping():
keys = [1,3,5]
values = [2,4,6]
randomness = hash(keys, values)
mappings = []
for key , value in zip(keys,values):
mappings.append(key + randomness*value)
return(mappings)
It can be opened at the cost of 3 plookups
def open_mapping(mappings, keys, values):
randomness = hash(keys,values)
index = 1
# Prover can chose any mapping, key , value
mapping = plookup(mappings)
key = plookup(keys)
value = plookup(values)
# But it has to satisfy this check
require(mappings[index] == key[index] + randomness*value[index])
# with overwhelming probability will not find an invalid mapping.
The bus mapping is consumed by both the EVM proof and the state proof.
bus_mapping[global_counter] = {
mem: [op, key, value],
stack: [op, index, value],
storage: [op, key, value],
index: opcode,
call_id: call_id,
prog_counter: prog_counter
}
The bus mapping is witnessed by the prover. In the EVM proof, we have to ensure the prover did not include extra variables. To do this, we limit its degree in the L1 EVM and then check every single element in the EVM proof.
The commitment to the bus mapping is a public input to both the state proof and EVM proof.
A block has a bunch of constants we create a mapping to support these.
This mapping can be looked up in our EVM proof for each of these opcodes.
block = [blockhash, coinbase, timestamp, number, difficiulty, gaslimit, chainID]
CPerezz If any of the block constants needs to be used as Public Input in any of the proofs, they should be all represented as Scalars I presume right? Which is fine for all of the elements except:
blockhashwhich repr IIRC will not fit inside a Scalar.
Any thoughts? Sould we compare it differently but keep it on this format? Use a different format to store that constant?
barryWhiteHat not sure which should be
This is created by the l1 evm and passed as a public input
OR
This is passed as a witness varaible from the prover and checked in the proofs
Want to wait for some gas cost estimates to find out
| opcode | Name | Description |
|---|---|---|
| 0x40 | BLOCKHASH | Get the hash of one of the 256 most recent complete blocks - 20 |
| 0x41 | COINBASE | Get the block's beneficiary address |
| 0x42 | TIMESTAMP | Get the block's timestamp |
| 0x43 | NUMBER | Get the block's number |
| 0x44 | DIFFICULTY | Get the block's difficulty |
| 0x45 | GASLIMIT | Get the block's gas limit |
| 0x46 | CHAINID | Returns the current chain’s EIP-155 unique identifier (EIP1344) |
A variable that defines which call we are currently executing
The current depth of our call stack current max is 1024 calls
The current caller of this contract
The address where this transaction originated
If this call/l2tx reverts we need to be able to undo all the storage writes. We store the storage_root_before so we can easily do this.
the gas price the user paid for gas
The amount of gas this program has
TODO: Add details about the constraints comprising the slot in the state proof.
^ e.g. finish condition
ying tong
There are a diverse set of opcodes that result in reading and writing the storage. They include
| Flag | Opcode | Description |
|---|---|---|
| 0x54 | SLOAD | Read a variable |
| 0x55 | SSTORE | Write a variable |
| 0xf0 | CREATE | Deploy a contract |
| 0x31 | BALANCE | Get a user's balance |
| 0xf1 | CALL | Call another account |
| 0xf2 | CALLCODE | Message call into this account with another account's code |
| 0xf4 | DELEGATECALL | Message call into this account with another account's code and persist changes. |
| 0xfa | STATICCALL | Similar to call but changes are not persistent |
| 0xfd | REVERT | Stop execution and revert storage changes |
| Get current storage root | Use this to enforce static calls and reverts |
We use the flag variable in our mapping to define which of these opcodes is being checked in the state proof.
A state-reading opcode copies an element from storage to the stack.
Storage operations happen in the state proof and are validated in the EVM proof. The prover is able to select any storage reads / writes they want in the state proof. They have to commit to the order of the reads and writes that have been done using the global_counter variable.
TODO: Add details about merkle proof.
Memory operations are performed in different orders in EVM proof and state proof. In the state proof, memory operations are performed ordered by index (location in memory) and then by global_counter. In the EVM proof they are checked ordered by global_counter.
We let our prover commit to any memory reads / writes they want to. We defer checking the correct ops were performed at the correct global_counter for our EVM proof.
| index | global_counter | value | memory_flag | Comment |
|---|---|---|---|---|
| 0 | 0 | 0 | 1 | init at 0 |
| 0 | 12 | 12 | 1 | write 12 |
| 0 | 24 | 12 | 0 | read 12 |
| 1 | 0 | 0 | 1 | init at 0 |
| 1 | 17 | 32 | 1 | write 32 |
| 1 | 89 | 32 | 0 | Read 32 |
Note: this is only partial bus mapping. In reality we will also have stack, storage and opcode details included in our bus mapping
| global_counter | memory_flag | memory_index | memory_value |
|---|---|---|---|
| 12 | 1 | 0 | 12 |
| 17 | 1 | 1 | 32 |
| 24 | 0 | 0 | 12 |
| 89 | 0 | 1 | 32 |
# rand is random number used to construct plookup key-value mappings
# It is a list of r, r**2 , r**3, r**4 .. r**n
def memory(rands):
bus_mapping = {{}}
index = [0,0,0,1,1,1]
value = [0,12,12,0,32,32]
memory_flag = [1,1,0,1,1,0]
global_counter = [0,12,24,0,27,89]
# set prev index to be value outside legal memory bounds
prev_index = p-1
# check 10000 mem ops
for i in range(10000):
# check the rest
for value, memory_flag, global_counter, index in
zip(value, memory_flag, global_counter, index):
# Binary constarint
require(memory_flag == 1 or memory_flag == 0)
# Check the value is correct
# if memory_flag == 0 its a read we check
# previous_value == current value read
if index != prev_index:
## init to zero
prev_index = index
require(value == 0)
require(memory_flag == 1)
if (memory_flag == 0):
require(current_value == value)
else (memory_flag == 1):
# if its a write we just set the current_value = new_value
current_value = value
# Check global_counter is ordered correctly
require(global_counter > previous_global_counter)
previous_global_counter = global_counter
if(global_counter!=0):
# add to bus mapping
global_counter = plookup(global_counter, valid_glbal_counters)
mapping = plookup(mapping, valid_mappings)
memory = "memory"
memory_flag = memory_flag
index = index
value = value
# check the key-value mapping
require(mapping == global_counter + rand[0]*memory
+ rand[1]*memory_flag + rand[2]* index)
Our stack has 16 elements that can be push, pop, dup, and swapped. But it also contains 1024 elements that must be stored. For example you can push 3 onto the stack 1024 times and then pop it 1024 times. So we need to be able to support these 1024 elements of storage.
In order to make a proof of validity about our stack we do the same that we have done for memory. We create a memory table with \(1024\) elements (indexed 0-1023). We also create a stack pointer (stack_pointer) which is initialized at 1024. This points to the index of the top of the stack.
Our EVM proof tracks stack_pointer and decrements it for every push, and increments it for every pop.
In our state proof our prover has to initialise each stack element at zero. Then they are able to perform any updates they want. They then commit this to our bus mapping.
In the EVM proof for every opcode that checks the stack we get the stack op that is associated with that from the bus mapping. We check that the index of push, pop matches the stack_pointer. Then we adjust the stack_pointer (++/--) based upon whether we popped or pushed.
Similar to the case of push/pop we can do this. But we have to check two indexes: the destination, and the source; and then push the value there onto the stack. This requires a single read and then a push.
Here we read twice the two indexes to swap and perform two writes of each index for the other value
Note: Note push pop dup swap outside the first 16 eleemnts in the stack is now allows. To avoid this we we have to perform a range proof on the stack_pointer - index is less than 16.
^ i.e. we have to check that
indexis a 4-bit value. this is definitely achievable with a 4-bit lookup table (and we'll likely have larger lookup tables in the circuit for other purposes anyway).
ying tong
barryWhiteHat Well its stack_pointer - index right ? Because if i push 1016 things on to the stack i can only push pop dup and swap elements 1016 to 1000.
TODO: Probably you don't need to have 1024 elements in the stack if you are only using a few. We can let the prover adjust htese
barryWhiteHat maybe we can remove slot in favor of just a list of checks each constraint must apply.
A slot can be defined as a single custom constraint. This constraint can be defined by the opcode programmer to perform that operation. Some things that will probably be done by most opcodes is
program_counterslot_counterOur opcodes can be more than one unique custom constraint we just need to ensure our selector uses slot_counter to select the correct custom constraint.
# global_counter input
# program_counter input
# slot_counter input
# fin_condition defined by the opcode
def slot():
opcode = plookup(t_opcodes)
mapping = plookup(t_mappings)
assert global_counter + program_counter * r + opcode * r**2 == mapping
# TODO we may have to include more elements in this plookup
# like stack storage and memory
# Do our actual opcode work
# TODO calculate fin_condition if required
# this means multiple slot opcode
# Several plookups
# Order 100 plookups
# Check if we are finished
if slot_counter == fin_condition:
slot_counter = 0
program_counter ++
else:
slot_counter ++
gas_used += gas_cost
if gas_used > gas_limit:
# Out of gas
oog = True
program_counter = oog_opcode
global_counter ++
The slot uses a bunch of variables to ensure it is looking at the correct element in the bus mapping. These variables are pass from the previous slot. Instead of using copy constraints to ensure these are correct we can just look at the wires of the previous circuit.
There variables include
This means our evm proof will have 5 wires entering each custom constraint and several advice wires also
(TODO?)
ying tong
barryWhiteHat TL;DR we use jump opcode to adjust hte program counter to what ever it is supposed to be this is how we handle loops and other things.
Our feild element size is 253 bits. So we cannot represent a word of 256 bit (evm word size) in a single feild element. All arithmatic is done modulo p ~ 253 bits which is also not compatible with the evm.
In order to make both compatible with the EVM encode our stack and memory elements as random linear combinations of the word decomposed into 8 bits.
w is our word and w[0:7] is the first 8 bits of our word.
word = w[0:7] + w[7:15]r + w[15:23] r^2 .. + w[247:255]r^31
note: r is calulated as the hash of all possible 8 bit words
barryWhiteHat are there some attacks here ? Seems like that is 2^8 possible elements and as we grow this to 32 element sum at some point there will be some "collisions"
barryWhiteHatit its a problem we can take r as being the list of all elements in that round.
If this is not a problem then we can place the encoded variale in storage.
This makes it very easy for us to do arithmatic by just looking up each word in a lookup table that maps to that operation.
Our stack and memory don't need to adjust to allow for this. but we need to apply this encoding / decoding when we get call data and read or write to storage.
Recall that the bus mapping is constructed as:
Take the three elements from bus mapping
value1 , value2 , value3 = bus_mapping[global_counter][call_id][prog_counter][stack][op_id][index]
^ does the
bus_mappinghere correspond to this one (copied from above)?bus_mapping[global_counter] = { mem: [op, key, value], stack: [op, index, value], storage: [op, key, value], index: opcode, call_id: call_id, prog_counter: prog_counter }should
value1, value2, value3each have a differentop_idandindex?ying tong
I was going to remove value2 , value 3 and rename value 1 to value. think we don't need multiple values here we can just include 3 stack ops inside our custom opcode.
I am asking Han about this feel he has been thinking about this some what so curious to hear what he thinks.
Do we have a cost to making the bus mapping have a non constant size?
barryWhiteHat
value1, value2 and value3 are defined as 32 8 bit words.
carry_bit = 0
for i in range(len(value1)):
result, carry_bit = plookup_add(value1[i], value2[i] carry_bit)
require(result == value2[i])
Take the two elements from bus mapping
value1 , value2 = bus_mapping[global_counter][call_id][prog_counter][stack][op_id][index]
value1, value2 are defined as 32 8 bit words.
carry_bit = 0
# Here we use carry_bit as a is check already true.
# ReverSE order from least significant first to most significant first.
for i in range(len(value1),0):
old_carry_bit = carry_bit
result, carry_bit = plookup_greater_than(value1[i], value2[i], carry_bit)
result == value3
A call should update the call_id in the evm proof. This will allow the prover to create a new memory and stack that have no elements in the state proof and use this for this call context.
We also track calldatacallid, calldata_start, calldatasize and returndatacallid, returndata_size, returndata_start. If calldatacopy or return data copy opcodes are used we require the prover to use the callid for data copy or returndatacopy to copy data into the memory of hte current call_id.
We set call_id equal to the random linear combination of everything we want to track about the call context
call_id -> rlc(calldata_callid, call_data_start_addr, call_data_size, return_data_callid, return_data_start_addr, return_data_size, origin, caller, call_value, call_stack_depth)
This mapping is updated for each call. But does not need to be tracked for every step. Instead it is pass as a elemnt of the bus mapping RLC.
| opcode | Name | Description |
|---|---|---|
| 0x32 | ORIGIN | Get execution origination address |
| 0x33 | CALLER | Get caller address |
| 0x34 | CALLVALUE | How much eth is sent with this tx |
| 0x36 | CALLDATASIZE | How much call data |
| 0x35 | CALLDATALOAD | What is the call data |
| 0x3d | RETURNDATASIZE | How much return data |
| return data | What is the return data | |
| Call stack depth | ||
| storage root before this call | Use this to revert and enforce static calls |
Until now we have dicussed opcodes that had constant amounts of work. For example \(\texttt{mul}\) takes two numbers and multiplies them. No matter what parameters are provided to \(\texttt{mul}\) at computation time it will still have the same amount of work to prove the \(\texttt{mul}\) was performed correctly.
There is another class of evm opcodes that have variable work associated with them. These opcodes tend to load variable length items from memory. For example calldatacopy copies call data onto the stack. The length of this call data is defined by the smart contract programmer and is variable.
This presents a difficult challenge. If we were to make our "opcode slots" long enough to support every possible calldatalength it would make our opcode slot very large and thus the rest of our opcode prohibitively expensive. Instead we separate these opcodes over multiple opcode slots so that we continue processing them until they have completed successfully.
These opcodes include
calldatacopy, returndatacopy
We arithmetise these opcodes by defining a condition that they must fulfil in order to increment the program_counter. We can then use multiple global_counters for the same opcode. For example calldatacopy must copy elements from call_details.calldata to the stack calldatalength times before we increment the program counter.
Similar approach can be taken for returndatacopy and return.
We have a key-value mapping that maps each opcode in a smart contract's bytecode to its byte offset (a.k.a program_index). This program_index is the program_counter value that is required to execute that opcode.
Our prover is able to select any opcode:program_index pair. We want to ensure that the prover is only able to select a valid execution branch. Doing things like changing the order of opcodes, adding opcodes or removing opcodes break this.
program_index list contains only unique values (no repeats).global_counter ie. global_counter \(0,1,2,3\)program_counter variable for a call_id is 0.program_counter variable for a call_id is opcode \(\texttt{stop}\) or \(\texttt{return}\)program_counter according to its rules: there is no way to update the program_counter other than executing the current opcode. For example, \(\texttt{mul}\) increments it by 1. \(\texttt{jump}\) pops an element from the stack and sets the program counter equal to that.TODO: add reasoning about deployment and loading the bytecode
program_counter = 0, which is the correct starting position for every smart contract.NOTE: This is more a proof about deployment.
program_index there is only one value.program_counter to move to the next opcodeWe use our bus mapping to transfer storage/memory and stack reads/writes to our EVM proof. We want to prove that
MLOAD contains a memory check and a stack push. This opcode should confirm both of these are happening AND that a storage read/write is not happening.bus_mapping is equal to max(global_counter).Because of \(\texttt{Global_counterUniqueness}\) assumption we know that we can have only a single element for each global_counter.
In the EVM proof we confirm that each of these is right.
The opcode correctness argument shows that we execute opcodes in the correct order up until we get to the storage read/write opcode.
\(\texttt{ProgramCounterTransition}\) assumes that for each opcode (including storage/stack/memory) we update the program counter correctly.
We also need to confirm that we do not execute any extra reads / writes in our state proof that are not checked in our EVM proof. To do this we use our \(\texttt{DegreeBound}\) assumption which limits the size of bus_mapping. We then ensure in our EVM proof that we check every value of global_counter up to our degreeBound.
It is still possible that a bus mapping contains a memory read, a storage write, and a stack push. This is invalid as no opcode requires these 3. Here an attacker is trying to hide a storage write inside a memory read opcode. We add the \(\texttt{OpcodeFidelity}\) assumption that makes sure that opcodes only contain mappings for the variables they care about and the rest are zero. For example \(\texttt{mul}\) opcode's bus mappings should only contain an element for stack.
-
Any changes
Be notified of any changes
-
Mention me
Be notified of mention me
-
Unsubscribe
Subscribe