inductive MstoreSummary.mstore_op : Type

• mstore : mstore_op
• mstore8 : mstore_op

@[reducible, inline]

abbrev MstoreSummary.mstoreEVM : EvmYul.Operation EvmYul.OperationType.EVM

Equations

• MstoreSummary.mstoreEVM = EvmYul.Operation.MSTORE

@[reducible, inline]

abbrev MstoreSummary.mstore8EVM : EvmYul.Operation EvmYul.OperationType.EVM

Equations

• MstoreSummary.mstore8EVM = EvmYul.Operation.MSTORE8

@[reducible, inline]

abbrev MstoreSummary.mstore_instr : Option (EvmYul.Operation EvmYul.OperationType.EVM × Option (EvmYul.UInt256 × ℕ))

Equations

• MstoreSummary.mstore_instr = some (MstoreSummary.mstoreEVM, none)

@[reducible, inline]

abbrev MstoreSummary.mstore8_instr : Option (EvmYul.Operation EvmYul.OperationType.EVM × Option (EvmYul.UInt256 × ℕ))

Equations

• MstoreSummary.mstore8_instr = some (MstoreSummary.mstore8EVM, none)

def MstoreSummary.mstore_op.get (op : mstore_op) : Option (EvmYul.Operation EvmYul.OperationType.EVM × Option (EvmYul.UInt256 × ℕ))

Equations

• MstoreSummary.mstore_op.mstore.get = MstoreSummary.mstore_instr
• MstoreSummary.mstore_op.mstore8.get = MstoreSummary.mstore8_instr

def MstoreSummary.mstore_op.t (op : mstore_op) : EvmYul.Operation EvmYul.OperationType.EVM

Equations

• MstoreSummary.mstore_op.mstore.t = (MstoreSummary.mstore_instr.get MstoreSummary.mstore_op.t.proof_1).1
• MstoreSummary.mstore_op.mstore8.t = (MstoreSummary.mstore8_instr.get MstoreSummary.mstore_op.t.proof_2).1

def MstoreSummary.mstore_op.to_mso (op : mstore_op) : EvmYul.MachineState → EvmYul.UInt256 → EvmYul.UInt256 → EvmYul.MachineState

Getter for the MachineStateOps.mstore* function

Equations

• MstoreSummary.mstore_op.mstore.to_mso = EvmYul.MachineState.mstore
• MstoreSummary.mstore_op.mstore8.to_mso = EvmYul.MachineState.mstore8

@[reducible, inline]

abbrev MstoreSummary.EVM.step_mstore (op : mstore_op) (gas gasCost : ℕ) : EvmYul.EVM.Transformer

Equations

• MstoreSummary.EVM.step_mstore op gas gasCost = EvmYul.EVM.step gas gasCost op.get

@[reducible, inline]

abbrev MstoreSummary.EvmYul.step_mstore (op : mstore_op) : EvmYul.EVM.Transformer

Equations

• MstoreSummary.EvmYul.step_mstore op = EvmYul.step op.t

def MstoreSummary.mstore_op.to_l (op : mstore_op) : ℕ

Different cases for the activeWords update

Equations

• MstoreSummary.mstore_op.mstore.to_l = 32
• MstoreSummary.mstore_op.mstore8.to_l = 1

theorem MstoreSummary.mstore_bypass_private (op : mstore_op) (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_mstore op ss = EvmYul.EVM.binaryMachineStateOp op.to_mso ss

Theorem needed to bypass the private attribute of EVM.dispatchBinaryMachineStateOp

def MstoreSummary.activeWords_comp (offset symActiveWords : EvmYul.UInt256) (l : ℕ) : EvmYul.UInt256

The new amount of activeWords based after running MSTORE with offset and currentAC amount of active words

Equations

• MstoreSummary.activeWords_comp offset symActiveWords l = EvmYul.UInt256.ofNat (symActiveWords.toNat ⊔ (offset.toNat + l + 31) / 32)

def MstoreSummary.mstore_memory_write (offset value : EvmYul.UInt256) (symMemory : ByteArray) : ByteArray

Writing value to symMemory starting at offset

Equations

• MstoreSummary.mstore_memory_write offset value symMemory = value.toByteArray.write 0 symMemory offset.toNat 32

def MstoreSummary.mstore8_memory_write (offset value : EvmYul.UInt256) (symMemory : ByteArray) : ByteArray

Writing value to symMemory starting at offset

Equations

• MstoreSummary.mstore8_memory_write offset value symMemory = { data := #[UInt8.ofNat value.toNat] }.write 0 symMemory offset.toNat 1

def MstoreSummary.mstore_op.to_write (op : mstore_op) : EvmYul.UInt256 → EvmYul.UInt256 → ByteArray → ByteArray

Different cases to write to memory depending on the mstore* opcode

Equations

• MstoreSummary.mstore_op.mstore.to_write = MstoreSummary.mstore_memory_write
• MstoreSummary.mstore_op.mstore8.to_write = MstoreSummary.mstore8_memory_write

theorem MstoreSummary.EvmYul.step_mstore_summary (op : mstore_op) (symGasPrice symTimestamp symNumber symGaslimit : ℕ) (symStack : EvmYul.Stack EvmYul.UInt256) (symPc symGasAvailable symRefund offset value 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 :: value :: symStack, execLength := symExecLength }; step_mstore op ss = Except.ok { toState := ss.toState, gasAvailable := ss.gasAvailable, activeWords := activeWords_comp offset symActiveWords op.to_l, memory := op.to_write offset value symMemory, returnData := ss.returnData, H_return := ss.H_return, pc := symPc + EvmYul.UInt256.ofNat 1, stack := symStack, execLength := ss.execLength }

theorem MstoreSummary.EVM.step_mstore_summary (op : mstore_op) (gas gasCost symGasPrice symTimestamp symNumber symGaslimit : ℕ) (symStack : EvmYul.Stack EvmYul.UInt256) (symPc symGasAvailable symRefund offset value 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 :: value :: symStack, execLength := symExecLength }; step_mstore op gas gasCost ss = Except.ok { toState := ss.toState, gasAvailable := symGasAvailable - EvmYul.UInt256.ofNat gasCost, activeWords := activeWords_comp offset symActiveWords op.to_l, memory := op.to_write offset value symMemory, returnData := ss.returnData, H_return := ss.H_return, pc := symPc + EvmYul.UInt256.ofNat 1, stack := symStack, execLength := symExecLength + 1 }

def MstoreSummary.mstore_op.to_bin (op : mstore_op) : ByteArray

Opcode map to binary

Equations

• MstoreSummary.mstore_op.mstore.to_bin = { data := #[82] }
• MstoreSummary.mstore_op.mstore8.to_bin = { data := #[83] }

@[simp]

theorem MstoreSummary.decode_singleton_mstore (op : mstore_op) : EvmYul.EVM.decode op.to_bin (EvmYul.UInt256.ofNat 0) = some (op.t, none)

def MstoreSummary.value_and_activeWords_gas (op : mstore_op) (value symActiveWords : EvmYul.UInt256) : EvmYul.UInt256

Equations

• MstoreSummary.value_and_activeWords_gas op value symActiveWords = EvmYul.UInt256.ofNat (EvmYul.MachineState.M symActiveWords.toNat value.toNat op.to_l)

@[simp]

theorem MstoreSummary.memoryExpansionCost_mstore (op : mstore_op) (symStack : EvmYul.Stack EvmYul.UInt256) (offset value symActiveWords : EvmYul.UInt256) (symState : EvmYul.EVM.State) (stack_ok : symState.stack = offset :: value :: symStack) (symWords_ok : symState.activeWords = symActiveWords) : EvmYul.EVM.memoryExpansionCost symState op.t = EvmYul.EVM.Cₘ (value_and_activeWords_gas op offset symActiveWords) - EvmYul.EVM.Cₘ symActiveWords

theorem MstoreSummary.X_mstore_summary (op : mstore_op) (symGasPrice symTimestamp symNumber symGaslimit : ℕ) (symStack : EvmYul.Stack EvmYul.UInt256) (symGasAvailable symRefund offset value 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 < match op with | mstore_op.mstore => 1024 | mstore_op.mstore8 => 1025) : 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 := op.to_bin, 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 :: value :: symStack, execLength := symExecLength }; GasConstants.Gverylow < symGasAvailable.toNat - EvmYul.EVM.memoryExpansionCost ss op.t → EvmYul.EVM.memoryExpansionCost ss op.t < 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 op.t) - EvmYul.UInt256.ofNat GasConstants.Gverylow, activeWords := activeWords_comp offset symActiveWords op.to_l, memory := op.to_write offset value symMemory, returnData := ByteArray.empty, H_return := ss.H_return, pc := EvmYul.UInt256.ofNat 1, stack := symStack, execLength := symExecLength + 2 } ByteArray.empty)