structure EvmYul.EVM.Stateextends EvmYul.SharedState : Type

The EVM State (extends EvmYul.SharedState).

• pc pc
• stack s
• execLength - Length of execution.

• accountMap : AccountMap
• σ₀ : AccountMap
• totalGasUsedInBlock : ℕ
• transactionReceipts : Array TransactionReceipt
• substate : Substate
• executionEnv : ExecutionEnv
• blocks : ProcessedBlocks
• genesisBlockHeader : BlockHeader
• createdAccounts : Batteries.RBSet AccountAddress compare
• gasAvailable : UInt256
• activeWords : UInt256
• memory : ByteArray
• returnData : ByteArray
• H_return : ByteArray
• pc : UInt256
• stack : Stack UInt256
• execLength : ℕ

instance EvmYul.EVM.instInhabitedState : Inhabited State

Equations

• EvmYul.EVM.instInhabitedState = { default := { toSharedState := default, pc := default, stack := default, execLength := default } }

inductive EvmYul.EVM.ExecutionResult (S : Type) : Type

• success {S : Type} (state : S) (o : ByteArray) : ExecutionResult S
• revert {S : Type} (g : UInt256) (o : ByteArray) : ExecutionResult S