owned this note
owned this note
Published
Linked with GitHub
# ZKEVM
[TOC]
## Links
- State proof exploration: https://hackmd.io/Nwd0e5AgTVSBWRQlp-Ving
- State circuit spec: https://hackmd.io/oJT1kJjvQYWQlKZ1JEtmMQ
- Circuit implementation: https://github.com/appliedzkp/zkevm-circuits
- Test vectors: https://github.com/appliedzkp/zkevm-testing-vectors
## Introduction
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.
1. Make a zkrollup that supports smart contracts
2. Create a proof of validity for every Ethereum block
This means making a proof of validity for the EVM + state reads / writes + signatures.
To simplify we separate our proofs into two components.
1. **State proof**: State/memory/stack ops have been performed correctly. This does not check if the correct location has been read/written. We allow our prover to pick any location here and in the EVM proof confirm it is correct.
2. **EVM proof**: This checks that the correct opcode is called at the correct time. It checks the validity of these opcodes. It also confirms that for each of these opcodes the state proof performed the correct operation.
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
> [name=ying tong]
## Terminology
L1 contract
: is a contract deployed on mainnet Ethereum.
zkevm verifier
: is an L1 contract that verifies the zkevm proofs.
L2 contract
: is a contract that is deployed inside our zkrollup, i.e. it uses the zkevm verifier to prove that transactions calling that smart contract are correct.
`l1tx`
: is a transaction a user sends to interact with an L1 contract.
`l2tx`
: is a transaction a user sends to deploy or interact with an L2 contract
Coordinator
: a party that makes proof of validity for Ethereum blocks. The coordinator recives `l2tx`s 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.
User
: a party who deploys and/or interacts with smart contracts deployed on l2
Opcodes
: EVM opcodes
> [name=barryWhiteHat] Possibly can remove slot if we can use custom constarints
Slot
: This is a number of constraints we assign to prove validity of every EVM opcode. For example we can have a slot of 100 constraints. This means that we will use 100 constraints that we use to prove Mul opcode but also Add , Jump, Sload. Each opcode costs 100 constraints even if it uses less than 100 constraints.
> note to self: "slot" = "number of rows"
> [name=ying tong]
> [name=barryWhiteHat] possibly can remove the notation of multislot opcodes as every opcode would be multiple slots.
MultiSlot opcodes
: Some opcodes can use multiple slots. This means that we just increment the `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?
> [name=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.
> [name=Star.LI]
Program Counter
: The location of the current opcode to execute in the EVM. This is updated after each opcode; in the case of $\texttt{JUMP}$ it is set to the location of the $\texttt{JUMP}$. For every new contract call it is initialised to zero.
Slot Counter
: For multislot opcodes we use the slot counter to track how many executions have taken place. This is incremented after each slot. This variable is used to track when a multislot opcode has terminated.
Global Counter
: A counter that is incremented for every opcode.
> would it be accurate to say that the Global Counter counts the number of reads and writes?
> [name=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
> [name=barryWhiteHat]
Bus Mapping
: In traditional computers a Bus is used to transfer data from memory and storage to the CPU. Here we reuse that paradigm to transfer data from our state proof to our EVM proof.
## Variables
> TODO: types
> [name=ying tong]
#### bus_mapping
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
#### global_counter
A global counter that increments for every slot of the EVM proof.
#### call_id
The id of the transaction/separate call context we are currently executing
#### program_counter
Is the value of `program_index` to the opcode we need to verify.
#### program_index
The location of an opcode in the L2 contract's bytecode.
#### mem
A Memory key-value mapping of `global_counter` -> `index` -> `value`
##### memory_op
Defines the type of memory action this is. For example 0 is read , 1 is write.
#### Storage
A key-value mapping for storage reads/writes. `global_counter` -> `index` -> `value`
##### storage_op
Defines what type of storage op to do.
#### Stack
A key-value mapping for each stack op.
##### stack_op
Defines the type of stack op
#### opcode
This is the current opcode to execute.
## Bus mappings
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
### Plookup key-value mappings
In plookup you can build key-value mappings as follows
``` python
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
``` python
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.
```
### Bus 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.
#### Block Constants
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]
```
>[name=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: `blockhash` which 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?
>[name=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
##### Opcodes that get block constants
| 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) |
### block details
#### call_id
A variable that defines which call we are currently executing
#### call_stack_depth
The current depth of our call stack current max is 1024 calls
#### msg.sender
The current caller of this contract
#### tx.origin
The address where this transaction originated
#### storage_root_before
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.
#### gas price
the gas price the user paid for gas
#### gas
The amount of gas this program has
## State Proof
### Slot
TODO: Add details about the constraints comprising the slot in the state proof.
> ^ e.g. finish condition
> [name=ying tong]
### Storage
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
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.
#### Memory reads / writes
| 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 |
#### Bus mapping produced
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 |
#### Pseudocode
``` python
# 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)
```
### Stack
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.
#### Push/Pop
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.
#### Dup
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.
#### Swap
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 `index` is 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).
> [name=ying tong]
> [name=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
## EVM proof
>[name=barryWhiteHat] maybe we can remove slot in favor of just a list of checks each constraint must apply.
### Slot
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
1. Gets the current opcode we are executing
2. Gets the stack and memory/storage variables the state proof provided via the memory bus.
3. Ensure only memory OR storage values have been provided. If two are provided fail.
4. Check that the correct bus mapping variables have been provided. E.g. for add we have to have 3 stack elements (two pops and one push). All performed at index 0.
5. Several plookup constaints used for arith / binary ops/ comparators
6. Check result of 3 matches what the opcode requires.
7. Check the finish condition of that opcode.
* If: true increment `program_counter`
* Else: Use another slot for this opcode and increment the `slot_counter`
Our 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.
#### pseudo code
``` python
# 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 ++
```
## slot variables
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
1. Global Counter
2. Slot counter
3. Program counter
4. call_id
5. stack pointer
6. several advice wires.
7. Intermediate variable wires
This means our evm proof will have 5 wires entering each custom constraint and several advice wires also
## Flow Control
> (TODO?)
> [name=ying tong]
> [name=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.
## Data encoding
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
>[name=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"
>[name=barryWhiteHat]it 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.
### Arithmetic
Recall that the bus mapping is constructed as:
#### Add
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_mapping` here 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, value3` each have a different `op_id` and `index`?
>
> [name=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?
> [name=barryWhiteHat]
`value1`, `value2` and `value3` are defined as 32 8 bit words.
``` python
carry_bit = 0
for i in range(len(value1)):
result, carry_bit = plookup_add(value1[i], value2[i] carry_bit)
require(result == value2[i])
```
### Binary Ops
### Comparators
#### Greater than
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.
``` python
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
```
## call / static call
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.
### 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.
### Call details related opcodes
| 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 |
## Opcodes with variable work
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`
### 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`.
## Proof of Security Properties
### Flow Control
#### Preliminaries
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.
#### Assumptions
IndexUniqueness
: `program_index` list contains only unique values (no repeats).
GlobalCounterUniqueness
: In EVM proof the opcodes are executed in increasing values of `global_counter` ie. global_counter $0,1,2,3$
StartZero
: The first `program_counter` variable for a `call_id` is 0.
StopAtTermination
: The last `program_counter` variable for a `call_id` is opcode $\texttt{stop}$ or $\texttt{return}$
ProgramCounterTransition
: Each opcode adjusts the `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.
#### 2.1 Opcodes are executed in the correct order
TODO: add reasoning about deployment and loading the bytecode
* $\texttt{StartZero}$ assumption says we have to start at `program_counter` = 0, which is the correct starting position for every smart contract.
* $\texttt{ProgramCounterTransition}$ assumption says we have to update our program counter correctly based upon the opcode we are executing.
* Because we update the program counter correctly we get to the correct second storage root.
* By induction n is valid , n+1 is valid therefore we must continue this until termination.
* $\texttt{StopAtTermination}$ assumption says we continue this until we reach an opcode that terminates that call.
#### 2.2: You can't insert an extra opcode
NOTE: This is more a proof about deployment.
* $\texttt{IndexUniqueness}$ says that for each `program_index` there is only one value.
* If you insert an extra opcode this breaks this assumption therefore it's false.
#### 2.3: You can't skip an opcode
* You need to update your `program_counter` to move to the next opcode
* The only way to do this is by executing the current opcode
* If you skip an opcode this will violate the $\texttt{ProgramCounterTransition}$ assumption.
### Bus mapping proof
#### Preliminaries
We use our bus mapping to transfer storage/memory and stack reads/writes to our EVM proof. We want to prove that
* You can't skip any reads / writes
* You can't add an extra read/write that is not required in the bytecode
#### Assumptions
OpcodeFidelity
: Some of our opcodes contain multiple memory / storage ops. For example `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.
DegreeBound
: We assume the degree of the `bus_mapping` is equal to max(global_counter).
#### Proof
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](#21-Opcodes-are-executed-in-the-correct-order) 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.