@[reducible, inline]

abbrev SstoreSummary.sstoreEVM : EvmYul.Operation EvmYul.OperationType.EVM

Equations

• SstoreSummary.sstoreEVM = EvmYul.Operation.SSTORE

@[reducible, inline]

abbrev SstoreSummary.sstore_instr : Option (EvmYul.Operation EvmYul.OperationType.EVM × Option (EvmYul.UInt256 × ℕ))

Equations

• SstoreSummary.sstore_instr = some (SstoreSummary.sstoreEVM, none)

@[reducible, inline]

abbrev SstoreSummary.EVM.step_sstore (gas gasCost : ℕ) : EvmYul.EVM.Transformer

Equations

• SstoreSummary.EVM.step_sstore gas gasCost = EvmYul.EVM.step gas gasCost SstoreSummary.sstore_instr

@[reducible, inline]

abbrev SstoreSummary.EvmYul.step_sstore : EvmYul.EVM.Transformer

Equations

• SstoreSummary.EvmYul.step_sstore = EvmYul.step SstoreSummary.sstoreEVM

theorem SstoreSummary.sstore_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_sstore ss = EvmYul.EVM.binaryStateOp EvmYul.State.sstore ss

Theorem needed to bypass the private attribute of EVM.dispatchBinaryStateOp

def SstoreSummary.accountMap_sstore (symState : EvmYul.State) (key value : EvmYul.UInt256) : EvmYul.AccountMap

Equations

• One or more equations did not get rendered due to their size.

def SstoreSummary.accessedStorageKeys_sstore (symState : EvmYul.State) (key : EvmYul.UInt256) : Batteries.RBSet (EvmYul.AccountAddress × EvmYul.UInt256) EvmYul.Substate.storageKeysCmp

Equations

• One or more equations did not get rendered due to their size.

def SstoreSummary.Aᵣ_sstore (symState : EvmYul.State) (key val : EvmYul.UInt256) : EvmYul.UInt256

Equations

• One or more equations did not get rendered due to their size.

theorem SstoreSummary.sstore_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 value : 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.sstore key value = { accountMap := accountMap_sstore ss key value, σ₀ := ss.σ₀, totalGasUsedInBlock := ss.totalGasUsedInBlock, transactionReceipts := ss.transactionReceipts, substate := let __src := ss.substate; { selfDestructSet := __src.selfDestructSet, touchedAccounts := __src.touchedAccounts, refundBalance := Aᵣ_sstore ss key value, accessedAccounts := __src.accessedAccounts, accessedStorageKeys := accessedStorageKeys_sstore ss key, logSeries := __src.logSeries }, executionEnv := ss.executionEnv, blocks := ss.blocks, genesisBlockHeader := ss.genesisBlockHeader, createdAccounts := ss.createdAccounts }

theorem SstoreSummary.EvmYul.step_sstore_summary (symGasPrice symTimestamp symNumber symGaslimit : ℕ) (symStack : EvmYul.Stack EvmYul.UInt256) (symPc symGasAvailable symRefund key 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 := key :: value :: symStack, execLength := symExecLength }; step_sstore ss = Except.ok { accountMap := accountMap_sstore ss.toState key value, σ₀ := ss.σ₀, totalGasUsedInBlock := ss.totalGasUsedInBlock, transactionReceipts := ss.transactionReceipts, substate := let __src := ss.substate; { selfDestructSet := __src.selfDestructSet, touchedAccounts := __src.touchedAccounts, refundBalance := Aᵣ_sstore ss.toState key value, accessedAccounts := __src.accessedAccounts, accessedStorageKeys := accessedStorageKeys_sstore ss.toState 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 := symStack, execLength := ss.execLength }

theorem SstoreSummary.EVM.step_sstore_summary (gas gasCost symGasPrice symTimestamp symNumber symGaslimit : ℕ) (symStack : EvmYul.Stack EvmYul.UInt256) (symPc symGasAvailable symRefund key 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) (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 := true, 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 :: value :: symStack, execLength := symExecLength }; step_sstore gas gasCost ss = Except.ok { accountMap := accountMap_sstore ss.toState key value, σ₀ := ss.σ₀, totalGasUsedInBlock := ss.totalGasUsedInBlock, transactionReceipts := ss.transactionReceipts, substate := let __src := ss.substate; { selfDestructSet := __src.selfDestructSet, touchedAccounts := __src.touchedAccounts, refundBalance := Aᵣ_sstore ss.toState key value, accessedAccounts := __src.accessedAccounts, accessedStorageKeys := accessedStorageKeys_sstore ss.toState 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 := symStack, execLength := symExecLength + 1 }

@[simp]

theorem SstoreSummary.decode_singleton_sstore : EvmYul.EVM.decode { data := #[85] } (EvmYul.UInt256.ofNat 0) = some (sstoreEVM, none)

@[simp]

theorem SstoreSummary.memoryExpansionCost_sstore (symState : EvmYul.EVM.State) : EvmYul.EVM.memoryExpansionCost symState sstoreEVM = 0

theorem SstoreSummary.Csstore_pos (symState : EvmYul.EVM.State) : 99 < EvmYul.EVM.Csstore symState

theorem SstoreSummary.X_sstore_summary (symGasPrice symTimestamp symNumber symGaslimit : ℕ) (symStack : EvmYul.Stack EvmYul.UInt256) (symGasAvailable symRefund key 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) (symValidJumps : Array EvmYul.UInt256) (symState : EvmYul.EVM.State) (symStack_ok : List.length symStack < 1024) (gasStippend : GasConstants.Gcallstipend < symGasAvailable.toNat) : 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 := #[85] }, 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 := true, 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 :: value :: symStack, execLength := symExecLength }; EvmYul.EVM.Csstore ss < symGasAvailable.toNat → EvmYul.EVM.X symGasAvailable.toNat symValidJumps ss = Except.ok (EvmYul.EVM.ExecutionResult.success { accountMap := accountMap_sstore ss.toState key value, σ₀ := ss.σ₀, totalGasUsedInBlock := ss.totalGasUsedInBlock, transactionReceipts := ss.transactionReceipts, substate := let __src := ss.substate; { selfDestructSet := __src.selfDestructSet, touchedAccounts := __src.touchedAccounts, refundBalance := Aᵣ_sstore ss.toState key value, accessedAccounts := __src.accessedAccounts, accessedStorageKeys := accessedStorageKeys_sstore ss.toState key, logSeries := __src.logSeries }, executionEnv := ss.executionEnv, blocks := ss.blocks, genesisBlockHeader := ss.genesisBlockHeader, createdAccounts := ss.createdAccounts, gasAvailable := symGasAvailable - EvmYul.UInt256.ofNat (EvmYul.EVM.Csstore ss), activeWords := ss.activeWords, memory := ss.memory, returnData := ByteArray.empty, H_return := ss.H_return, pc := EvmYul.UInt256.ofNat 1, stack := symStack, execLength := symExecLength + 2 } ByteArray.empty)