barryWhiteHat
    • Create new note
    • Create a note from template
      • Sharing URL Link copied
      • /edit
      • View mode
        • Edit mode
        • View mode
        • Book mode
        • Slide mode
        Edit mode View mode Book mode Slide mode
      • Customize slides
      • Note Permission
      • Read
        • Only me
        • Signed-in users
        • Everyone
        Only me Signed-in users Everyone
      • Write
        • Only me
        • Signed-in users
        • Everyone
        Only me Signed-in users Everyone
      • Engagement control Commenting, Suggest edit, Emoji Reply
      • Invitee
    • Publish Note

      Share your work with the world Congratulations! 🎉 Your note is out in the world Publish Note

      Your note will be visible on your profile and discoverable by anyone.
      Your note is now live.
      This note is visible on your profile and discoverable online.
      Everyone on the web can find and read all notes of this public team.
      See published notes
      Unpublish note
      Please check the box to agree to the Community Guidelines.
      View profile
    • Commenting
      Permission
      Disabled Forbidden Owners Signed-in users Everyone
    • Enable
    • Permission
      • Forbidden
      • Owners
      • Signed-in users
      • Everyone
    • Suggest edit
      Permission
      Disabled Forbidden Owners Signed-in users Everyone
    • Enable
    • Permission
      • Forbidden
      • Owners
      • Signed-in users
    • Emoji Reply
    • Enable
    • Versions and GitHub Sync
    • Note settings
    • Engagement control
    • Transfer ownership
    • Delete this note
    • Save as template
    • Insert from template
    • Import from
      • Dropbox
      • Google Drive
      • Gist
      • Clipboard
    • Export to
      • Dropbox
      • Google Drive
      • Gist
    • Download
      • Markdown
      • HTML
      • Raw HTML
Menu Note settings Sharing URL Create Help
Create Create new note Create a note from template
Menu
Options
Versions and GitHub Sync Engagement control Transfer ownership Delete this note
Import from
Dropbox Google Drive Gist Clipboard
Export to
Dropbox Google Drive Gist
Download
Markdown HTML Raw HTML
Back
Sharing URL Link copied
/edit
View mode
  • Edit mode
  • View mode
  • Book mode
  • Slide mode
Edit mode View mode Book mode Slide mode
Customize slides
Note Permission
Read
Only me
  • Only me
  • Signed-in users
  • Everyone
Only me Signed-in users Everyone
Write
Only me
  • Only me
  • Signed-in users
  • Everyone
Only me Signed-in users Everyone
Engagement control Commenting, Suggest edit, Emoji Reply
Invitee
Publish Note

Share your work with the world Congratulations! 🎉 Your note is out in the world Publish Note

Your note will be visible on your profile and discoverable by anyone.
Your note is now live.
This note is visible on your profile and discoverable online.
Everyone on the web can find and read all notes of this public team.
See published notes
Unpublish note
Please check the box to agree to the Community Guidelines.
View profile
Engagement control
Commenting
Permission
Disabled Forbidden Owners Signed-in users Everyone
Enable
Permission
  • Forbidden
  • Owners
  • Signed-in users
  • Everyone
Suggest edit
Permission
Disabled Forbidden Owners Signed-in users Everyone
Enable
Permission
  • Forbidden
  • Owners
  • Signed-in users
Emoji Reply
Enable
Import from Dropbox Google Drive Gist Clipboard
   owned this note    owned this note      
Published Linked with GitHub
12
Subscribed
  • Any changes
    Be notified of any changes
  • Mention me
    Be notified of mention me
  • Unsubscribe
Subscribe
# 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.

Import from clipboard

Paste your markdown or webpage here...

Advanced permission required

Your current role can only read. Ask the system administrator to acquire write and comment permission.

This team is disabled

Sorry, this team is disabled. You can't edit this note.

This note is locked

Sorry, only owner can edit this note.

Reach the limit

Sorry, you've reached the max length this note can be.
Please reduce the content or divide it to more notes, thank you!

Import from Gist

Import from Snippet

or

Export to Snippet

Are you sure?

Do you really want to delete this note?
All users will lose their connection.

Create a note from template

Create a note from template

Oops...
This template has been removed or transferred.
Upgrade
All
  • All
  • Team
No template.

Create a template

Upgrade

Delete template

Do you really want to delete this template?
Turn this template into a regular note and keep its content, versions, and comments.

This page need refresh

You have an incompatible client version.
Refresh to update.
New version available!
See releases notes here
Refresh to enjoy new features.
Your user state has changed.
Refresh to load new user state.

Sign in

Forgot password

or

By clicking below, you agree to our terms of service.

Sign in via Facebook Sign in via Twitter Sign in via GitHub Sign in via Dropbox Sign in with Wallet
Wallet ( )
Connect another wallet

New to HackMD? Sign up

Help

  • English
  • 中文
  • Français
  • Deutsch
  • 日本語
  • Español
  • Català
  • Ελληνικά
  • Português
  • italiano
  • Türkçe
  • Русский
  • Nederlands
  • hrvatski jezik
  • język polski
  • Українська
  • हिन्दी
  • svenska
  • Esperanto
  • dansk

Documents

Help & Tutorial

How to use Book mode

Slide Example

API Docs

Edit in VSCode

Install browser extension

Contacts

Feedback

Discord

Send us email

Resources

Releases

Pricing

Blog

Policy

Terms

Privacy

Cheatsheet

Syntax Example Reference
# Header Header 基本排版
- Unordered List
  • Unordered List
1. Ordered List
  1. Ordered List
- [ ] Todo List
  • Todo List
> Blockquote
Blockquote
**Bold font** Bold font
*Italics font* Italics font
~~Strikethrough~~ Strikethrough
19^th^ 19th
H~2~O H2O
++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: :smile: Emoji list
{%youtube youtube_id %} Externals
$L^aT_eX$ LaTeX
:::info
This is a alert area.
:::

This is a alert area.

Versions and GitHub Sync
Get Full History Access

  • Edit version name
  • Delete

revision author avatar     named on  

More Less

Note content is identical to the latest version.
Compare
    Choose a version
    No search result
    Version not found
Sign in to link this note to GitHub
Learn more
This note is not linked with GitHub
 

Feedback

Submission failed, please try again

Thanks for your support.

On a scale of 0-10, how likely is it that you would recommend HackMD to your friends, family or business associates?

Please give us some advice and help us improve HackMD.

 

Thanks for your feedback

Remove version name

Do you want to remove this version name and description?

Transfer ownership

Transfer to
    Warning: is a public team. If you transfer note to this team, everyone on the web can find and read this note.

      Link with GitHub

      Please authorize HackMD on GitHub
      • Please sign in to GitHub and install the HackMD app on your GitHub repo.
      • HackMD links with GitHub through a GitHub App. You can choose which repo to install our App.
      Learn more  Sign in to GitHub

      Push the note to GitHub Push to GitHub Pull a file from GitHub

        Authorize again
       

      Choose which file to push to

      Select repo
      Refresh Authorize more repos
      Select branch
      Select file
      Select branch
      Choose version(s) to push
      • Save a new version and push
      • Choose from existing versions
      Include title and tags
      Available push count

      Pull from GitHub

       
      File from GitHub
      File from HackMD

      GitHub Link Settings

      File linked

      Linked by
      File path
      Last synced branch
      Available push count

      Danger Zone

      Unlink
      You will no longer receive notification when GitHub file changes after unlink.

      Syncing

      Push failed

      Push successfully