Consensys / linea-arithmetization

17 stars 18 forks source link

Controls for targeted testing #812

Open OlivierBBB opened 1 week ago

OlivierBBB commented 1 week ago
# Control knobs In order to test the arithmetization of specific opcodes, in particular complex ones like CALL-type instructions, there are 4 components we would need to have precise control over: - world state $\sigma$ - machine state $\mu$ - accrued state $A$ - environment $I$ By this we mean: we want to be able to produce precise configurations of several parameters in each of the above at the point in time **T** which is typically the **instant before** triggering a particular opcode. In other words if the EVM executes a sequence of opcodes $$\begin{array}{ccccccc} &&&&\mathbf{T}&&\\ &&&&\downarrow&&\\ w_{0} & w_{1} & \cdots & w_{i-1} & & w_{i} & \cdots\end{array}$$ we would like to us to have control at the point in time **T** which is just after $w_{i-1}$ was executed (and its impact on $\sigma$, $\mu$ and $A$ has been accounted for) and just before $w_i$ is about to start its processing, with $w_i$ being the opcode which we want to test. **Note.** Initially we want to test single transactions so all the steering would have to happen in the same transaction. There will be scenarios where we will want to test several transactions in succession, typically when testing the effects of SELFDESTRUCT's on state or consistency conditions on storage and accounts. In this issue we are mostly concerned with the testing of **opcodes** and thus a single transaction should suffice. ## Control over the world state We need control over - for a specific account its **balance** $\sigma[a] _ \text{b}$, **nonce** $\sigma[a] _ \text{n}$ and **code** $\sigma[a] _ \text{c}$ - whether an address is **currently undergoing deployment** or not - whether this is, within the current transaction and for that address, a **first time a deployment or not** As a consequence we would have control over - whether the account $\sigma[a]$ associated with a given address $a$ **exists** or not - it does not exist **iff** it has [ zero balance and zero nonce and empty code ] - whether an address $a$ can be deployed at or not - you can only deploy at address $a$ if the underlying account $\sigma[a]$ has zero nonce and empty code - whether CALL's will lead to account creation or not (of the callee) - whether CALL's will be aborted due to insufficient balance (of the caller) **Note.** this control over accounts will be required for both the currently executing one and any account that may be touched/modified by the opcode in question. E.g. for caller/callee pairs for CALL-type instructions, creator/createe pairs for CREATE(2), but also when running opcodes that query other accounts (e.g. BALANCE, EXTCODEXXX) ## Control over the machine state For machine state everything should be under our control when we require it. - the top most elements of the **stack** $\mu_\textbf{s}$ (which are typically the inputs of the instruction $w_i$) - how much **gas** $\mu_\text{g}$ is available at that point in time - **memory size** (i.e. $\mu_\text{i}$) This would allow us to trigger certain exceptions at will - stackUnderflow / stackOverflow - memoryExpansionException (a subexception of the outOfGasException that was defined to simplify the arithmetization) - outOfGasException (in the sense of the arithmetization) **Note.** Control over the stack and its top items can "easily" be achieved through any of the following parameters - the **world state** - the currently executing **bytecode** (PUSH'ing items on the stack that are hardcoded in the bytecode) - **storage** (by SLOAD'ing items onto the stack in succession that are in storage) - **other accounts** (by having nonsense contracts in the state from which to EXTCODECOPY stuff that represents values we may then MLOAD onto the stack) - the **execution environment** and in particular the **call data** (by CALLDATALOAD'ing various values from call data or CALLDATACOPY'ing stuff and the MLOAD'ing onto the stack) ## Control over the accrued state - whether an address $a$ is warm or not (so whether $a \in A_\textbf{a}$ or not) - whether an storage key $k$ is warm or not (so whether $k \in A_\textbf{k}$ or not) - whether an address has been marked for SELFDESTRUCT or not (i.e. whether $a \in A_\textbf{s}$ or not) **Note.** - For warmth - requested account warmth can be achieved easily by either including that address in the transaction's access list or by carrying out a BALANCE operation ahead of time (or any other warmth impacting operation) - similar (access list or SSTORE/SLOAD ahead of time) - marking an address for SELFDESTRUCT requires that the address in question can selfdestruct - either through SELFDESTRUCT in its own bytecode - or through a CALLCODE or DELEGATECALL call to a smart contract that can SELFDESTRUCT. ## Control over select environment variables Among environment variables $I$ we mostly would require control over - the **call stack depth** $I_\text{e}$ in order to test aborting conditions of CALLs and CREATEs - whether the environment is **static** (i.e. is **write protected**) or not $I_\text{w}$ i.e. whether one of its ancestors (or itself) was spawned through a STATICCALL. ## Control over future events We further need to be able to decide ahead of time - if the current execution context will revert, either - on its own through a REVERT opcode or an exception or - by virtue of one of its ancestor context's reverting - when $w_i =$ some CALL or CREATE instruction, whether the call / deployment will be successful (i.e. exit with status code 1 or 0) # Goals The purpose of having this much control is to steer the EVM into very specific execution scenarios e.g. - various exceptions for CALL-type instructions, in particular conjunctions of exceptions (e.g. static exception + out of gas etc ...) - unexceptional CALL-type instructions that get aborted (insufficient balance and/or call stack depth limit reached) - (unexceptional, unaborted and necessarily successful) EOA call that - WILL be reverted - WON'T be reverted - (unexceptional, unaborted) SMC call that will be a - FAILURE and - WILL be reverted - WON'T be reverted - SUCCESS and - WILL be reverted - WON'T be reverted - same thing but with precompile calls and various ways of failure/success in the precompile - various exceptions for CREATE-type instructions - various aborting conditions for CREATE-type instructions - various failure conditions for CREATE-type instructions (deployment address already has nonzero nonce or nonempty code) - (unexceptional, unaborted, no failure condition and necessarily successful) deployment with empty initialization code - (unexceptional, unaborted, no failure condition) deployment with nonempty initialization code - FAILURE in deployment - WILL be reverted - WON'T be reverted - SUCCESS in deployment - WILL be reverted - WON'T be reverted - compatibility of all of the above with successive, reverted deployments