instance EvmYul.instDecidableEqByteArray_evmYul : DecidableEq ByteArray

Equations

• EvmYul.instDecidableEqByteArray_evmYul x✝¹ x✝ = match decEq x✝¹.data x✝.data with | isTrue h₁ => isTrue ⋯ | isFalse h₂ => isFalse ⋯

structure EvmYul.MachineState : Type

The partial shared MachineState μ. Section 9.4.1.

• gasAvailable g
• memory m
• activeWords i - # active words.
• returnData o - Data from the previous call from the current environment.

• gasAvailable : UInt256
• activeWords : UInt256
• memory : ByteArray
• returnData : ByteArray
• H_return : ByteArray

instance EvmYul.instInhabitedMachineState : Inhabited MachineState

Equations

• EvmYul.instInhabitedMachineState = { default := { gasAvailable := default, activeWords := default, memory := default, returnData := default, H_return := default } }