EvmEquivalence.Summaries.StackOperationsSummary

StackOpsSummary.stackOps_op.iszero.stack word₁ word₂ word₃ symStack = word₁ :: symStack
StackOpsSummary.stackOps_op.not.stack word₁ word₂ word₃ symStack = word₁ :: symStack
StackOpsSummary.stackOps_op.addmod.stack word₁ word₂ word₃ symStack = word₁ :: word₂ :: word₃ :: symStack
StackOpsSummary.stackOps_op.mulmod.stack word₁ word₂ word₃ symStack = word₁ :: word₂ :: word₃ :: symStack
op.stack word₁ word₂ word₃ symStack = word₁ :: word₂ :: symStack

Instances For

source

theorem StackOpsSummary.EvmYul.step_op_summary (op : stackOps_op) (word₁ word₂ word₃ : EvmYul.UInt256) (symStack : EvmYul.Stack EvmYul.UInt256) (symPc : EvmYul.UInt256) (symState : EvmYul.EVM.State) :

step_stackOps op { toSharedState := symState.toSharedState, pc := symPc, stack := op.stack word₁ word₂ word₃ symStack, execLength := symState.execLength } = Except.ok { toSharedState := symState.toSharedState, pc := symPc + EvmYul.UInt256.ofNat 1, stack := op.do word₁ word₂ word₃ :: symStack, execLength := symState.execLength }

source

theorem StackOpsSummary.EVM.step_add_to_step_add (op : stackOps_op) (word₁ word₂ word₃ : EvmYul.UInt256) (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 := op.stack word₁ word₂ word₃ symStack, execLength := symExecLength }; step_stackOps op gas gasCost ss = EvmYul.step_stackOps 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 := symPc, stack := op.stack word₁ word₂ word₃ symStack, execLength := symExecLength + 1 }

source

theorem StackOpsSummary.EVM.step_add_summary (op : stackOps_op) (word₁ word₂ word₃ : EvmYul.UInt256) (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 := op.stack word₁ word₂ word₃ symStack, execLength := symExecLength }; step_stackOps 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 word₁ word₂ word₃ :: symStack, execLength := symExecLength + 1 }

source

def StackOpsSummary.stackOps_op.to_bin (op : stackOps_op) :

ByteArray

Equations

StackOpsSummary.stackOps_op.add.to_bin = { data := #[1] }
StackOpsSummary.stackOps_op.sub.to_bin = { data := #[3] }
StackOpsSummary.stackOps_op.div.to_bin = { data := #[4] }
StackOpsSummary.stackOps_op.sdiv.to_bin = { data := #[5] }
StackOpsSummary.stackOps_op.mod.to_bin = { data := #[6] }
StackOpsSummary.stackOps_op.smod.to_bin = { data := #[7] }
StackOpsSummary.stackOps_op.addmod.to_bin = { data := #[8] }
StackOpsSummary.stackOps_op.mulmod.to_bin = { data := #[9] }
StackOpsSummary.stackOps_op.exp.to_bin = { data := #[10] }
StackOpsSummary.stackOps_op.signextend.to_bin = { data := #[11] }
StackOpsSummary.stackOps_op.lt.to_bin = { data := #[16] }
StackOpsSummary.stackOps_op.gt.to_bin = { data := #[17] }
StackOpsSummary.stackOps_op.slt.to_bin = { data := #[18] }
StackOpsSummary.stackOps_op.sgt.to_bin = { data := #[19] }
StackOpsSummary.stackOps_op.eq.to_bin = { data := #[20] }
StackOpsSummary.stackOps_op.iszero.to_bin = { data := #[21] }
StackOpsSummary.stackOps_op.and.to_bin = { data := #[22] }
StackOpsSummary.stackOps_op.or.to_bin = { data := #[23] }
StackOpsSummary.stackOps_op.xor.to_bin = { data := #[24] }
StackOpsSummary.stackOps_op.not.to_bin = { data := #[25] }
StackOpsSummary.stackOps_op.byte.to_bin = { data := #[26] }
StackOpsSummary.stackOps_op.shl.to_bin = { data := #[27] }
StackOpsSummary.stackOps_op.shr.to_bin = { data := #[28] }
StackOpsSummary.stackOps_op.sar.to_bin = { data := #[29] }

Instances For

source

@[simp]

theorem StackOpsSummary.decode_singleton_add :

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

source

@[simp]

theorem StackOpsSummary.decode_singleton_sub :

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

source

@[simp]

theorem StackOpsSummary.decode_singleton_div :

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

source

@[simp]

theorem StackOpsSummary.decode_singleton_sdiv :

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

source

@[simp]

theorem StackOpsSummary.decode_singleton_mod :

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

source

@[simp]

theorem StackOpsSummary.decode_singleton_smod :

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

source

@[simp]

theorem StackOpsSummary.decode_singleton_addmod :

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

source

@[simp]

theorem StackOpsSummary.decode_singleton_mulmod :

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

source

@[simp]

theorem StackOpsSummary.decode_singleton_exp :

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

source

@[simp]

theorem StackOpsSummary.decode_singleton_signextend :

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

source

@[simp]

theorem StackOpsSummary.decode_singleton_lt :

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

source

@[simp]

theorem StackOpsSummary.decode_singleton_gt :

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

source

@[simp]

theorem StackOpsSummary.decode_singleton_slt :

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

source

@[simp]

theorem StackOpsSummary.decode_singleton_sgt :

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

source

@[simp]

theorem StackOpsSummary.decode_singleton_eq :

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

source

@[simp]

theorem StackOpsSummary.decode_singleton_iszero :

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

source

@[simp]

theorem StackOpsSummary.decode_singleton_and :

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

source

@[simp]

theorem StackOpsSummary.decode_singleton_or :

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

source

@[simp]

theorem StackOpsSummary.decode_singleton_xor :

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

source

@[simp]

theorem StackOpsSummary.decode_singleton_not :

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

source

@[simp]

theorem StackOpsSummary.decode_singleton_byte :

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

source

@[simp]

theorem StackOpsSummary.decode_singleton_shl :

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

source

@[simp]

theorem StackOpsSummary.decode_singleton_shr :

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

source

@[simp]

theorem StackOpsSummary.decode_singleton_sar :

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

source

@[simp]

theorem StackOpsSummary.decode_singleton_stackOps (op : stackOps_op) :

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

source

@[simp]

theorem StackOpsSummary.memoryExpansionCost_stackOps (op : stackOps_op) (symState : EvmYul.EVM.State) :

EvmYul.EVM.memoryExpansionCost symState op.t = 0

source

def StackOpsSummary.C'_exp (symState : EvmYul.EVM.State) :

ℕ

Equations

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

Instances For

source

def StackOpsSummary.stackOps_op.C'_comp (op : stackOps_op) (symState : EvmYul.EVM.State) :

ℕ

Equations

StackOpsSummary.stackOps_op.exp.C'_comp symState = StackOpsSummary.C'_exp symState
op.C'_comp symState = op.C'_noexp

Instances For

source

@[simp]

theorem StackOpsSummary.C'_stackOps (op : stackOps_op) (symState : EvmYul.EVM.State) :

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

source

def StackOpsSummary.stackOps_op.to_stack_length (op : stackOps_op) :

ℕ

Equations

StackOpsSummary.stackOps_op.iszero.to_stack_length = 1024
StackOpsSummary.stackOps_op.not.to_stack_length = 1024
StackOpsSummary.stackOps_op.addmod.to_stack_length = 1022
StackOpsSummary.stackOps_op.mulmod.to_stack_length = 1022
op.to_stack_length = 1023

Instances For

source

theorem StackOpsSummary.X_stackOps_summary (op : stackOps_op) (word₁ word₂ word₃ : EvmYul.UInt256) (symGasPrice symTimestamp symNumber symGaslimit : ℕ) (symStack : EvmYul.Stack EvmYul.UInt256) (symGasAvailable symRefund 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) (symStack_ok : List.length symStack < op.to_stack_length) (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 := 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 := op.stack word₁ word₂ word₃ symStack, execLength := symExecLength }; op.C'_comp ss < symGasAvailable.toNat → EvmYul.EVM.X symGasAvailable.toNat symValidJumps ss = Except.ok (EvmYul.EVM.ExecutionResult.success { toState := ss.toState, gasAvailable := symGasAvailable - EvmYul.UInt256.ofNat (op.C'_comp ss), activeWords := ss.activeWords, memory := ss.memory, returnData := ByteArray.empty, H_return := ss.H_return, pc := EvmYul.UInt256.ofNat 1, stack := op.do word₁ word₂ word₃ :: symStack, execLength := symExecLength + 2 } ByteArray.empty)