@[reducible, inline]

abbrev SloadSummary.sloadEVM : EvmYul.Operation EvmYul.OperationType.EVM

Equations

• SloadSummary.sloadEVM = EvmYul.Operation.SLOAD

@[reducible, inline]

abbrev SloadSummary.sload_instr : Option (EvmYul.Operation EvmYul.OperationType.EVM × Option (EvmYul.UInt256 × ℕ))

Equations

• SloadSummary.sload_instr = some (SloadSummary.sloadEVM, none)

@[reducible, inline]

abbrev SloadSummary.EVM.step_sload (gas gasCost : ℕ) : EvmYul.EVM.Transformer

Equations

• SloadSummary.EVM.step_sload gas gasCost = EvmYul.EVM.step gas gasCost SloadSummary.sload_instr

@[reducible, inline]

abbrev SloadSummary.EvmYul.step_sload : EvmYul.EVM.Transformer

Equations

• SloadSummary.EvmYul.step_sload = EvmYul.step SloadSummary.sloadEVM

def SloadSummary.lookupStorage_sload (symState : EvmYul.State) (key : EvmYul.UInt256) : EvmYul.UInt256

Equations

• SloadSummary.lookupStorage_sload symState key = match symState.lookupAccount symState.executionEnv.codeOwner with | none => { val := 0 } | some acc => acc.lookupStorage key

theorem SloadSummary.sload_summary (symGasPrice symTimestamp symNumber symGaslimit : ℕ) (symRefund symPrevrandao : EvmYul.UInt256) (symCode : ByteArray) (symAccessedStorageKeys : Batteries.RBSet (EvmYul.AccountAddress × EvmYul.UInt256) EvmYul.Substate.storageKeysCmp) (symAccounts : EvmYul.AccountMap) (symCodeOwner symSender symSource symCoinbase : EvmYul.AccountAddress) (symPerm : Bool) (symState : EvmYul.State) (key : EvmYul.UInt256) : let ss := { accountMap := symAccounts, σ₀ := symState.σ₀, totalGasUsedInBlock := symState.totalGasUsedInBlock, transactionReceipts := symState.transactionReceipts, substate := let __src := symState.substate; { selfDestructSet := __src.selfDestructSet, touchedAccounts := __src.touchedAccounts, refundBalance := symRefund, accessedAccounts := __src.accessedAccounts, accessedStorageKeys := symAccessedStorageKeys, logSeries := __src.logSeries }, executionEnv := let __src := symState.executionEnv; { codeOwner := symCodeOwner, sender := symSender, source := symSource, weiValue := __src.weiValue, inputData := __src.inputData, code := symCode, gasPrice := symGasPrice, header := let __src := symState.executionEnv.header; { parentHash := __src.parentHash, ommersHash := __src.ommersHash, beneficiary := symCoinbase, stateRoot := __src.stateRoot, transRoot := __src.transRoot, receiptRoot := __src.receiptRoot, logsBloom := __src.logsBloom, difficulty := __src.difficulty, number := symNumber, gasLimit := symGaslimit, gasUsed := __src.gasUsed, timestamp := symTimestamp, extraData := __src.extraData, nonce := __src.nonce, prevRandao := symPrevrandao, baseFeePerGas := __src.baseFeePerGas, parentBeaconBlockRoot := __src.parentBeaconBlockRoot, withdrawalsRoot := __src.withdrawalsRoot, blobGasUsed := __src.blobGasUsed, excessBlobGas := __src.excessBlobGas }, depth := __src.depth, perm := symPerm, blobVersionedHashes := __src.blobVersionedHashes }, blocks := symState.blocks, genesisBlockHeader := symState.genesisBlockHeader, createdAccounts := symState.createdAccounts }; ss.sload key = (ss.addAccessedStorageKey (symCodeOwner, key), lookupStorage_sload ss key)

theorem SloadSummary.sload_bypass_private (symGasPrice symTimestamp symNumber symGaslimit : ℕ) (symStack : EvmYul.Stack EvmYul.UInt256) (symPc symGasAvailable symRefund symActiveWords symPrevrandao : EvmYul.UInt256) (symExecLength : ℕ) (symReturnData symCode symMemory : ByteArray) (symAccessedStorageKeys : Batteries.RBSet (EvmYul.AccountAddress × EvmYul.UInt256) EvmYul.Substate.storageKeysCmp) (symAccounts : EvmYul.AccountMap) (symCodeOwner symSender symSource symCoinbase : EvmYul.AccountAddress) (symPerm : Bool) (symState : EvmYul.EVM.State) : let ss := { accountMap := symAccounts, σ₀ := symState.σ₀, totalGasUsedInBlock := symState.totalGasUsedInBlock, transactionReceipts := symState.transactionReceipts, substate := let __src := symState.substate; { selfDestructSet := __src.selfDestructSet, touchedAccounts := __src.touchedAccounts, refundBalance := symRefund, accessedAccounts := __src.accessedAccounts, accessedStorageKeys := symAccessedStorageKeys, logSeries := __src.logSeries }, executionEnv := let __src := symState.executionEnv; { codeOwner := symCodeOwner, sender := symSender, source := symSource, weiValue := __src.weiValue, inputData := __src.inputData, code := symCode, gasPrice := symGasPrice, header := let __src := symState.executionEnv.header; { parentHash := __src.parentHash, ommersHash := __src.ommersHash, beneficiary := symCoinbase, stateRoot := __src.stateRoot, transRoot := __src.transRoot, receiptRoot := __src.receiptRoot, logsBloom := __src.logsBloom, difficulty := __src.difficulty, number := symNumber, gasLimit := symGaslimit, gasUsed := __src.gasUsed, timestamp := symTimestamp, extraData := __src.extraData, nonce := __src.nonce, prevRandao := symPrevrandao, baseFeePerGas := __src.baseFeePerGas, parentBeaconBlockRoot := __src.parentBeaconBlockRoot, withdrawalsRoot := __src.withdrawalsRoot, blobGasUsed := __src.blobGasUsed, excessBlobGas := __src.excessBlobGas }, depth := __src.depth, perm := symPerm, blobVersionedHashes := __src.blobVersionedHashes }, blocks := symState.blocks, genesisBlockHeader := symState.genesisBlockHeader, createdAccounts := symState.createdAccounts, gasAvailable := symGasAvailable, activeWords := symActiveWords, memory := symMemory, returnData := symReturnData, H_return := symState.H_return, pc := symPc, stack := symStack, execLength := symExecLength }; EvmYul.step_sload ss = EvmYul.EVM.unaryStateOp EvmYul.State.sload ss

Theorem needed to bypass the private attribute of EVM.dispatchBinaryStateOp

theorem SloadSummary.EvmYul.step_sload_summary (symGasPrice symTimestamp symNumber symGaslimit : ℕ) (symStack : EvmYul.Stack EvmYul.UInt256) (symPc symGasAvailable symRefund key symActiveWords symPrevrandao : EvmYul.UInt256) (symExecLength : ℕ) (symReturnData symCode symMemory : ByteArray) (symAccessedStorageKeys : Batteries.RBSet (EvmYul.AccountAddress × EvmYul.UInt256) EvmYul.Substate.storageKeysCmp) (symAccounts : EvmYul.AccountMap) (symCodeOwner symSender symSource symCoinbase : EvmYul.AccountAddress) (symPerm : Bool) (symState : EvmYul.EVM.State) : let ss := { accountMap := symAccounts, σ₀ := symState.σ₀, totalGasUsedInBlock := symState.totalGasUsedInBlock, transactionReceipts := symState.transactionReceipts, substate := let __src := symState.substate; { selfDestructSet := __src.selfDestructSet, touchedAccounts := __src.touchedAccounts, refundBalance := symRefund, accessedAccounts := __src.accessedAccounts, accessedStorageKeys := symAccessedStorageKeys, logSeries := __src.logSeries }, executionEnv := let __src := symState.executionEnv; { codeOwner := symCodeOwner, sender := symSender, source := symSource, weiValue := __src.weiValue, inputData := __src.inputData, code := symCode, gasPrice := symGasPrice, header := let __src := symState.executionEnv.header; { parentHash := __src.parentHash, ommersHash := __src.ommersHash, beneficiary := symCoinbase, stateRoot := __src.stateRoot, transRoot := __src.transRoot, receiptRoot := __src.receiptRoot, logsBloom := __src.logsBloom, difficulty := __src.difficulty, number := symNumber, gasLimit := symGaslimit, gasUsed := __src.gasUsed, timestamp := symTimestamp, extraData := __src.extraData, nonce := __src.nonce, prevRandao := symPrevrandao, baseFeePerGas := __src.baseFeePerGas, parentBeaconBlockRoot := __src.parentBeaconBlockRoot, withdrawalsRoot := __src.withdrawalsRoot, blobGasUsed := __src.blobGasUsed, excessBlobGas := __src.excessBlobGas }, depth := __src.depth, perm := symPerm, blobVersionedHashes := __src.blobVersionedHashes }, blocks := symState.blocks, genesisBlockHeader := symState.genesisBlockHeader, createdAccounts := symState.createdAccounts, gasAvailable := symGasAvailable, activeWords := symActiveWords, memory := symMemory, returnData := symReturnData, H_return := symState.H_return, pc := symPc, stack := key :: symStack, execLength := symExecLength }; step_sload ss = Except.ok { accountMap := ss.accountMap, σ₀ := ss.σ₀, totalGasUsedInBlock := ss.totalGasUsedInBlock, transactionReceipts := ss.transactionReceipts, substate := let __src := ss.substate; { selfDestructSet := __src.selfDestructSet, touchedAccounts := __src.touchedAccounts, refundBalance := __src.refundBalance, accessedAccounts := __src.accessedAccounts, accessedStorageKeys := ss.substate.accessedStorageKeys.insert (ss.executionEnv.codeOwner, key), logSeries := __src.logSeries }, executionEnv := ss.executionEnv, blocks := ss.blocks, genesisBlockHeader := ss.genesisBlockHeader, createdAccounts := ss.createdAccounts, toMachineState := ss.toMachineState, pc := symPc + EvmYul.UInt256.ofNat 1, stack := lookupStorage_sload ss.toState key :: symStack, execLength := ss.execLength }

theorem SloadSummary.EVM.step_sload_summary (gas gasCost symGasPrice symTimestamp symNumber symGaslimit : ℕ) (symStack : EvmYul.Stack EvmYul.UInt256) (symPc symGasAvailable symRefund key symActiveWords symPrevrandao : EvmYul.UInt256) (symExecLength : ℕ) (symReturnData symCode symMemory : ByteArray) (symAccessedStorageKeys : Batteries.RBSet (EvmYul.AccountAddress × EvmYul.UInt256) EvmYul.Substate.storageKeysCmp) (symAccounts : EvmYul.AccountMap) (symCodeOwner symSender symSource symCoinbase : EvmYul.AccountAddress) (symPerm : Bool) (gas_pos : 0 < gas) (symState : EvmYul.EVM.State) : let ss := { accountMap := symAccounts, σ₀ := symState.σ₀, totalGasUsedInBlock := symState.totalGasUsedInBlock, transactionReceipts := symState.transactionReceipts, substate := let __src := symState.substate; { selfDestructSet := __src.selfDestructSet, touchedAccounts := __src.touchedAccounts, refundBalance := symRefund, accessedAccounts := __src.accessedAccounts, accessedStorageKeys := symAccessedStorageKeys, logSeries := __src.logSeries }, executionEnv := let __src := symState.executionEnv; { codeOwner := symCodeOwner, sender := symSender, source := symSource, weiValue := __src.weiValue, inputData := __src.inputData, code := symCode, gasPrice := symGasPrice, header := let __src := symState.executionEnv.header; { parentHash := __src.parentHash, ommersHash := __src.ommersHash, beneficiary := symCoinbase, stateRoot := __src.stateRoot, transRoot := __src.transRoot, receiptRoot := __src.receiptRoot, logsBloom := __src.logsBloom, difficulty := __src.difficulty, number := symNumber, gasLimit := symGaslimit, gasUsed := __src.gasUsed, timestamp := symTimestamp, extraData := __src.extraData, nonce := __src.nonce, prevRandao := symPrevrandao, baseFeePerGas := __src.baseFeePerGas, parentBeaconBlockRoot := __src.parentBeaconBlockRoot, withdrawalsRoot := __src.withdrawalsRoot, blobGasUsed := __src.blobGasUsed, excessBlobGas := __src.excessBlobGas }, depth := __src.depth, perm := symPerm, blobVersionedHashes := __src.blobVersionedHashes }, blocks := symState.blocks, genesisBlockHeader := symState.genesisBlockHeader, createdAccounts := symState.createdAccounts, gasAvailable := symGasAvailable, activeWords := symActiveWords, memory := symMemory, returnData := symReturnData, H_return := symState.H_return, pc := symPc, stack := key :: symStack, execLength := symExecLength }; step_sload gas gasCost ss = Except.ok { accountMap := ss.accountMap, σ₀ := ss.σ₀, totalGasUsedInBlock := ss.totalGasUsedInBlock, transactionReceipts := ss.transactionReceipts, substate := let __src := ss.substate; { selfDestructSet := __src.selfDestructSet, touchedAccounts := __src.touchedAccounts, refundBalance := __src.refundBalance, accessedAccounts := __src.accessedAccounts, accessedStorageKeys := ss.substate.accessedStorageKeys.insert (ss.executionEnv.codeOwner, key), logSeries := __src.logSeries }, executionEnv := ss.executionEnv, blocks := ss.blocks, genesisBlockHeader := ss.genesisBlockHeader, createdAccounts := ss.createdAccounts, gasAvailable := symGasAvailable - EvmYul.UInt256.ofNat gasCost, activeWords := ss.activeWords, memory := ss.memory, returnData := ss.returnData, H_return := ss.H_return, pc := symPc + EvmYul.UInt256.ofNat 1, stack := lookupStorage_sload ss.toState key :: symStack, execLength := symExecLength + 1 }

@[simp]

theorem SloadSummary.decode_singleton_sload : EvmYul.EVM.decode { data := #[84] } (EvmYul.UInt256.ofNat 0) = some (sloadEVM, none)

@[simp]

theorem SloadSummary.memoryExpansionCost_sload (symState : EvmYul.EVM.State) : EvmYul.EVM.memoryExpansionCost symState sloadEVM = 0

theorem SloadSummary.Csload_pos (symState : EvmYul.EVM.State) : 99 < EvmYul.EVM.Csload symState.stack symState.substate symState.executionEnv

TODO: Generalize to C'

theorem SloadSummary.X_sload_summary (symGasPrice symTimestamp symNumber symGaslimit : ℕ) (symStack : EvmYul.Stack EvmYul.UInt256) (symGasAvailable symRefund key symActiveWords symPrevrandao : EvmYul.UInt256) (symExecLength : ℕ) (symReturnData symMemory : ByteArray) (symAccessedStorageKeys : Batteries.RBSet (EvmYul.AccountAddress × EvmYul.UInt256) EvmYul.Substate.storageKeysCmp) (symAccounts : EvmYul.AccountMap) (symCodeOwner symSender symSource symCoinbase : EvmYul.AccountAddress) (symPerm : Bool) (symValidJumps : Array EvmYul.UInt256) (symState : EvmYul.EVM.State) (symStack_ok : List.length symStack < 1024) : let ss := { accountMap := symAccounts, σ₀ := symState.σ₀, totalGasUsedInBlock := symState.totalGasUsedInBlock, transactionReceipts := symState.transactionReceipts, substate := let __src := symState.substate; { selfDestructSet := __src.selfDestructSet, touchedAccounts := __src.touchedAccounts, refundBalance := symRefund, accessedAccounts := __src.accessedAccounts, accessedStorageKeys := symAccessedStorageKeys, logSeries := __src.logSeries }, executionEnv := let __src := symState.executionEnv; { codeOwner := symCodeOwner, sender := symSender, source := symSource, weiValue := __src.weiValue, inputData := __src.inputData, code := { data := #[84] }, gasPrice := symGasPrice, header := let __src := symState.executionEnv.header; { parentHash := __src.parentHash, ommersHash := __src.ommersHash, beneficiary := symCoinbase, stateRoot := __src.stateRoot, transRoot := __src.transRoot, receiptRoot := __src.receiptRoot, logsBloom := __src.logsBloom, difficulty := __src.difficulty, number := symNumber, gasLimit := symGaslimit, gasUsed := __src.gasUsed, timestamp := symTimestamp, extraData := __src.extraData, nonce := __src.nonce, prevRandao := symPrevrandao, baseFeePerGas := __src.baseFeePerGas, parentBeaconBlockRoot := __src.parentBeaconBlockRoot, withdrawalsRoot := __src.withdrawalsRoot, blobGasUsed := __src.blobGasUsed, excessBlobGas := __src.excessBlobGas }, depth := __src.depth, perm := symPerm, blobVersionedHashes := __src.blobVersionedHashes }, blocks := symState.blocks, genesisBlockHeader := symState.genesisBlockHeader, createdAccounts := symState.createdAccounts, gasAvailable := symGasAvailable, activeWords := symActiveWords, memory := symMemory, returnData := symReturnData, H_return := symState.H_return, pc := EvmYul.UInt256.ofNat 0, stack := key :: symStack, execLength := symExecLength }; EvmYul.EVM.Csload ss.stack ss.substate ss.executionEnv < symGasAvailable.toNat → EvmYul.EVM.X symGasAvailable.toNat symValidJumps ss = Except.ok (EvmYul.EVM.ExecutionResult.success { accountMap := ss.accountMap, σ₀ := ss.σ₀, totalGasUsedInBlock := ss.totalGasUsedInBlock, transactionReceipts := ss.transactionReceipts, substate := let __src := ss.substate; { selfDestructSet := __src.selfDestructSet, touchedAccounts := __src.touchedAccounts, refundBalance := __src.refundBalance, accessedAccounts := __src.accessedAccounts, accessedStorageKeys := ss.substate.accessedStorageKeys.insert (ss.executionEnv.codeOwner, key), logSeries := __src.logSeries }, executionEnv := ss.executionEnv, blocks := ss.blocks, genesisBlockHeader := ss.genesisBlockHeader, createdAccounts := ss.createdAccounts, gasAvailable := symGasAvailable - EvmYul.UInt256.ofNat (EvmYul.EVM.Csload ss.stack ss.substate ss.executionEnv), activeWords := ss.activeWords, memory := ss.memory, returnData := ByteArray.empty, H_return := ss.H_return, pc := EvmYul.UInt256.ofNat 1, stack := lookupStorage_sload ss.toState key :: symStack, execLength := symExecLength + 2 } ByteArray.empty)