HackMD
  • Beta
    Beta  Get a sneak peek of HackMD’s new design
    Turn on the feature preview and give us feedback.
    Go → Got it
      • Create new note
      • Create a note from template
    • Beta  Get a sneak peek of HackMD’s new design
      Beta  Get a sneak peek of HackMD’s new design
      Turn on the feature preview and give us feedback.
      Go → Got it
      • Sharing Link copied
      • /edit
      • View mode
        • Edit mode
        • View mode
        • Book mode
        • Slide mode
        Edit mode View mode Book mode Slide mode
      • 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
      • More (Comment, Invitee)
      • Publishing
        Please check the box to agree to the Community Guidelines.
        Everyone on the web can find and read all notes of this public team.
        After the note is published, everyone on the web can find and read this note.
        See all published notes on profile page.
      • Commenting Enable
        Disabled Forbidden Owners Signed-in users Everyone
      • Permission
        • Forbidden
        • Owners
        • Signed-in users
        • Everyone
      • Invitee
      • No invitee
      • Options
      • Versions and GitHub Sync
      • Transfer ownership
      • Delete this note
      • Template
      • Save as template
      • Insert from template
      • Export
      • Dropbox
      • Google Drive Export to Google Drive
      • Gist
      • Import
      • Dropbox
      • Google Drive Import from Google Drive
      • Gist
      • Clipboard
      • Download
      • Markdown
      • HTML
      • Raw HTML
    Menu Sharing Create Help
    Create Create new note Create a note from template
    Menu
    Options
    Versions and GitHub Sync Transfer ownership Delete this note
    Export
    Dropbox Google Drive Export to Google Drive Gist
    Import
    Dropbox Google Drive Import from Google Drive Gist Clipboard
    Download
    Markdown HTML Raw HTML
    Back
    Sharing
    Sharing Link copied
    /edit
    View mode
    • Edit mode
    • View mode
    • Book mode
    • Slide mode
    Edit mode View mode Book mode Slide mode
    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
    More (Comment, Invitee)
    Publishing
    Please check the box to agree to the Community Guidelines.
    Everyone on the web can find and read all notes of this public team.
    After the note is published, everyone on the web can find and read this note.
    See all published notes on profile page.
    More (Comment, Invitee)
    Commenting Enable
    Disabled Forbidden Owners Signed-in users Everyone
    Permission
    Owners
    • Forbidden
    • Owners
    • Signed-in users
    • Everyone
    Invitee
    No invitee
       owned this note    owned this note      
    Published Linked with GitHub
    Like9 BookmarkBookmarked
    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

    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 lost their connection.

    Create a note from template

    Create a note from template

    Oops...
    This template is not available.


    Upgrade

    All
    • All
    • Team
    No template found.

    Create custom template


    Upgrade

    Delete template

    Do you really want to delete this template?

    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

    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

    Tutorials

    Book Mode Tutorial

    Slide Mode Tutorial

    YAML Metadata

    Contacts

    Facebook

    Twitter

    Feedback

    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

    Versions and GitHub Sync

    Sign in to link this note to GitHub Learn more
    This note is not linked with GitHub Learn more
     
    Add badge Pull Push GitHub Link Settings
    Upgrade now

    Version named by    

    More Less
    • Edit
    • Delete

    Note content is identical to the latest version.
    Compare with
      Choose a version
      No search result
      Version not found

    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. Learn more

         Sign in to GitHub

        HackMD links with GitHub through a GitHub App. You can choose which repo to install our App.

        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
        Available push count

        Upgrade

        Pull from GitHub

         
        File from GitHub
        File from HackMD

        GitHub Link Settings

        File linked

        Linked by
        File path
        Last synced branch
        Available push count

        Upgrade

        Danger Zone

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

        Syncing

        Push failed

        Push successfully