structure EvmYul.State : Type

The State. Section 9.3.

• accountMap σ
• substate A
• executionEnv I
• totalGasUsedInBlock Υᵍ

• accountMap : AccountMap
• σ₀ : AccountMap
• totalGasUsedInBlock : ℕ
• transactionReceipts : Array TransactionReceipt
• substate : Substate
• executionEnv : ExecutionEnv
• blocks : ProcessedBlocks
• genesisBlockHeader : BlockHeader
• createdAccounts : Batteries.RBSet AccountAddress compare

instance EvmYul.instBEqState : BEq State

Equations

• EvmYul.instBEqState = { beq := EvmYul.beqState✝ }

instance EvmYul.instInhabitedState : Inhabited State

Equations

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

instance EvmYul.instReprState : Repr State

Equations

• EvmYul.instReprState = { reprPrec := EvmYul.reprState✝ }

def EvmYul.State.blockHashes (self : State) : Array UInt256

Equations

• self.blockHashes = Array.map EvmYul.ProcessedBlock.hash self.blocks