EvmEquivalence.Summaries.StateGettersSummary

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 }; step_arith op gas gasCost ss = EvmYul.step_arith op { toState := ss.toState, gasAvailable := symGasAvailable - EvmYul.UInt256.ofNat gasCost, activeWords := ss.activeWords, memory := ss.memory, returnData := ss.returnData, H_return := ss.H_return, pc := ss.pc, stack := ss.stack, execLength := symExecLength + 1 }

source

theorem StateGettersSummary.EVM.step_getter_summary (op : stateGetter_op) (gas gasCost 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) (gpos : 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 := symStack, execLength := symExecLength }; step_arith op gas gasCost ss = Except.ok { toState := ss.toState, gasAvailable := symGasAvailable - EvmYul.UInt256.ofNat gasCost, activeWords := ss.activeWords, memory := ss.memory, returnData := ss.returnData, H_return := ss.H_return, pc := symPc.add (EvmYul.UInt256.ofNat 1), stack := op.do ss :: symStack, execLength := symExecLength + 1 }

source

def StateGettersSummary.stateGetter_op.to_bin (op : stateGetter_op) :

ByteArray

Equations

StateGettersSummary.stateGetter_op.address.to_bin = { data := #[48] }
StateGettersSummary.stateGetter_op.origin.to_bin = { data := #[50] }
StateGettersSummary.stateGetter_op.caller.to_bin = { data := #[51] }
StateGettersSummary.stateGetter_op.gasprice.to_bin = { data := #[58] }
StateGettersSummary.stateGetter_op.coinbase.to_bin = { data := #[65] }
StateGettersSummary.stateGetter_op.timestamp.to_bin = { data := #[66] }
StateGettersSummary.stateGetter_op.number.to_bin = { data := #[67] }
StateGettersSummary.stateGetter_op.prevrandao.to_bin = { data := #[68] }
StateGettersSummary.stateGetter_op.gaslimit.to_bin = { data := #[69] }
StateGettersSummary.stateGetter_op.chainid.to_bin = { data := #[70] }
StateGettersSummary.stateGetter_op.selfbalance.to_bin = { data := #[71] }
StateGettersSummary.stateGetter_op.pc.to_bin = { data := #[88] }

Instances For

source

@[simp]

theorem StateGettersSummary.decode_singleton_address :

EvmYul.EVM.decode { data := #[48] } (EvmYul.UInt256.ofNat 0) = some (addressEVM , none )

source

@[simp]

theorem StateGettersSummary.decode_singleton_origin :

EvmYul.EVM.decode { data := #[50] } (EvmYul.UInt256.ofNat 0) = some (originEVM , none )

source

@[simp]

theorem StateGettersSummary.decode_singleton_caller :

EvmYul.EVM.decode { data := #[51] } (EvmYul.UInt256.ofNat 0) = some (callerEVM , none )

source

@[simp]

theorem StateGettersSummary.decode_singleton_gasprice :

EvmYul.EVM.decode { data := #[58] } (EvmYul.UInt256.ofNat 0) = some (gaspriceEVM , none )

source

@[simp]

theorem StateGettersSummary.decode_singleton_coinbase :

EvmYul.EVM.decode { data := #[65] } (EvmYul.UInt256.ofNat 0) = some (coinbaseEVM , none )

source

@[simp]

theorem StateGettersSummary.decode_singleton_timestamp :

EvmYul.EVM.decode { data := #[66] } (EvmYul.UInt256.ofNat 0) = some (timestampEVM , none )

source

@[simp]

theorem StateGettersSummary.decode_singleton_number :

EvmYul.EVM.decode { data := #[67] } (EvmYul.UInt256.ofNat 0) = some (numberEVM , none )

source

@[simp]

theorem StateGettersSummary.decode_singleton_prevrandao :

EvmYul.EVM.decode { data := #[68] } (EvmYul.UInt256.ofNat 0) = some (prevrandaoEVM , none )

source

@[simp]

theorem StateGettersSummary.decode_singleton_gaslimit :

EvmYul.EVM.decode { data := #[69] } (EvmYul.UInt256.ofNat 0) = some (gaslimitEVM , none )

source

@[simp]

theorem StateGettersSummary.decode_singleton_chainid :

EvmYul.EVM.decode { data := #[70] } (EvmYul.UInt256.ofNat 0) = some (chainidEVM , none )

source

@[simp]

theorem StateGettersSummary.decode_singleton_selfbalance :

EvmYul.EVM.decode { data := #[71] } (EvmYul.UInt256.ofNat 0) = some (selfbalanceEVM , none )

source

@[simp]

theorem StateGettersSummary.decode_singleton_pc :

EvmYul.EVM.decode { data := #[88] } (EvmYul.UInt256.ofNat 0) = some (pcEVM , none )

source

@[simp]

theorem StateGettersSummary.decode_singleton (op : stateGetter_op) :

EvmYul.EVM.decode op.to_bin (EvmYul.UInt256.ofNat 0) = some (op.t, none )

source

@[simp]

theorem StateGettersSummary.memoryExpansionCost_arith (op : stateGetter_op) (symState : EvmYul.EVM.State) :

EvmYul.EVM.memoryExpansionCost symState op.t = 0

source

def StateGettersSummary.stateGetter_op.C'_comp (op : stateGetter_op) :

ℕ

Equations

Instances For

source

@[simp]

theorem StateGettersSummary.C'_arith (op : stateGetter_op) (symState : EvmYul.EVM.State) :

EvmYul.EVM.C' symState op.t = op.C'_comp

source

theorem StateGettersSummary.X_getter_summary (op : stateGetter_op) (symGasPrice symTimestamp symNumber symGaslimit : ℕ) (symStack : EvmYul.Stack EvmYul.UInt256) (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) (symValidJumps : Array EvmYul.UInt256) (enoughGas : op.C'_comp < symGasAvailable.toNat) (symStack_ok : List.length symStack < 1024) (code_h : symCode = op.to_bin) (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 := EvmYul.UInt256.ofNat 0, stack := symStack, execLength := symExecLength }; EvmYul.EVM.X symGasAvailable.toNat symValidJumps ss = Except.ok (EvmYul.EVM.ExecutionResult.success { toState := ss.toState, gasAvailable := symGasAvailable - EvmYul.UInt256.ofNat op.C'_comp, activeWords := ss.activeWords, memory := ss.memory, returnData := ByteArray.empty, H_return := ss.H_return, pc := EvmYul.UInt256.ofNat 1, stack := op.do ss :: symStack, execLength := symExecLength + 2 } ByteArray.empty)