@[reducible, inline]

abbrev MloadSummary.mloadEVM : EvmYul.Operation EvmYul.OperationType.EVM

Equations

• MloadSummary.mloadEVM = EvmYul.Operation.MLOAD

@[reducible, inline]

abbrev MloadSummary.mload_instr : Option (EvmYul.Operation EvmYul.OperationType.EVM × Option (EvmYul.UInt256 × ℕ))

Equations

• MloadSummary.mload_instr = some (MloadSummary.mloadEVM, none)

@[reducible, inline]

abbrev MloadSummary.EVM.step_mload (gas gasCost : ℕ) : EvmYul.EVM.Transformer

Equations

• MloadSummary.EVM.step_mload gas gasCost = EvmYul.EVM.step gas gasCost MloadSummary.mload_instr

@[reducible, inline]

abbrev MloadSummary.EvmYul.step_mload : EvmYul.EVM.Transformer

Equations

• MloadSummary.EvmYul.step_mload = EvmYul.step MloadSummary.mloadEVM

@[reducible, inline]

abbrev MloadSummary.activeWords_comp (offset symActiveWords : EvmYul.UInt256) (l : ℕ) : EvmYul.UInt256

Equations

• MloadSummary.activeWords_comp = MstoreSummary.activeWords_comp

theorem MloadSummary.EvmYul.step_mload_summary (symGasPrice symTimestamp symNumber symGaslimit : ℕ) (symStack : EvmYul.Stack EvmYul.UInt256) (symPc symGasAvailable symRefund offset 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 := offset :: symStack, execLength := symExecLength }; step_mload ss = Except.ok { toState := ss.toState, gasAvailable := ss.gasAvailable, activeWords := activeWords_comp offset symActiveWords 32, memory := ss.memory, returnData := ss.returnData, H_return := ss.H_return, pc := symPc + EvmYul.UInt256.ofNat 1, stack := ss.lookupMemory offset :: symStack, execLength := ss.execLength }

theorem MloadSummary.EVM.step_mload_summary (gas gasCost symGasPrice symTimestamp symNumber symGaslimit : ℕ) (symStack : EvmYul.Stack EvmYul.UInt256) (symPc symGasAvailable symRefund offset 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 := offset :: symStack, execLength := symExecLength }; step_mload gas gasCost ss = Except.ok { toState := ss.toState, gasAvailable := symGasAvailable - EvmYul.UInt256.ofNat gasCost, activeWords := activeWords_comp offset symActiveWords 32, memory := ss.memory, returnData := ss.returnData, H_return := ss.H_return, pc := symPc + EvmYul.UInt256.ofNat 1, stack := ss.lookupMemory offset :: symStack, execLength := symExecLength + 1 }

@[simp]

theorem MloadSummary.decode_singleton_mload : EvmYul.EVM.decode { data := #[81] } (EvmYul.UInt256.ofNat 0) = some (mloadEVM, none)

def MloadSummary.value_and_activeWords_gas (symActiveWords : EvmYul.UInt256) (s : EvmYul.EVM.State) : EvmYul.UInt256

Equations

• MloadSummary.value_and_activeWords_gas symActiveWords s = EvmYul.UInt256.ofNat (EvmYul.MachineState.M symActiveWords.toNat s.stack[0]!.toNat 32)

@[simp]

theorem MloadSummary.memoryExpansionCost_mload (symActiveWords : EvmYul.UInt256) (symState : EvmYul.EVM.State) (symWords_ok : symState.activeWords = symActiveWords) : EvmYul.EVM.memoryExpansionCost symState mloadEVM = EvmYul.EVM.Cₘ (value_and_activeWords_gas symActiveWords symState) - EvmYul.EVM.Cₘ symActiveWords

theorem MloadSummary.X_mload_summary (symGasPrice symTimestamp symNumber symGaslimit : ℕ) (symStack : EvmYul.Stack EvmYul.UInt256) (symGasAvailable symRefund offset 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 := #[81] }, 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 := offset :: symStack, execLength := symExecLength }; GasConstants.Gverylow < symGasAvailable.toNat - EvmYul.EVM.memoryExpansionCost ss EvmYul.Operation.MLOAD → EvmYul.EVM.memoryExpansionCost ss EvmYul.Operation.MLOAD < EvmYul.UInt256.size → EvmYul.EVM.X symGasAvailable.toNat symValidJumps ss = Except.ok (EvmYul.EVM.ExecutionResult.success { toState := ss.toState, gasAvailable := symGasAvailable - EvmYul.UInt256.ofNat (EvmYul.EVM.memoryExpansionCost ss mloadEVM) - EvmYul.UInt256.ofNat GasConstants.Gverylow, activeWords := activeWords_comp offset symActiveWords 32, memory := ss.memory, returnData := ByteArray.empty, H_return := ss.H_return, pc := EvmYul.UInt256.ofNat 1, stack := ss.lookupMemory offset :: symStack, execLength := symExecLength + 2 } ByteArray.empty)