structure EvmYul.ExecutionEnv : Type

The execution envorinment I ExecutionEnv. Section 9.3.

• codeOwner Iₐ
• sender Iₒ
• source Iₛ
• weiValue Iᵥ
• inputData I_d
• code I_b
• gasPrice Iₚ
• header I_H
• depth Iₑ
• perm I_w

• codeOwner : AccountAddress
• sender : AccountAddress
• source : AccountAddress
• weiValue : UInt256
• inputData : ByteArray
• code : ByteArray
• gasPrice : ℕ
• header : BlockHeader
• depth : ℕ
• perm : Bool
• blobVersionedHashes : List ByteArray

instance EvmYul.instDecidableEqExecutionEnv : DecidableEq ExecutionEnv

Equations

• EvmYul.instDecidableEqExecutionEnv = EvmYul.decEqExecutionEnv✝

instance EvmYul.instInhabitedExecutionEnv : Inhabited ExecutionEnv

Equations

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

instance EvmYul.instReprExecutionEnv : Repr ExecutionEnv

Equations

• EvmYul.instReprExecutionEnv = { reprPrec := EvmYul.reprExecutionEnv✝ }

def EvmYul.prevRandao (e : ExecutionEnv) : UInt256

Equations

• EvmYul.prevRandao e = e.header.prevRandao

def EvmYul.basefee (e : ExecutionEnv) : UInt256

Equations

• EvmYul.basefee e = EvmYul.UInt256.ofNat e.header.baseFeePerGas

def EvmYul.ExecutionEnv.getBlobGasprice (e : ExecutionEnv) : UInt256

Equations

• e.getBlobGasprice = EvmYul.UInt256.ofNat e.header.getBlobGasprice

def EvmYul.blobhash (e : ExecutionEnv) (i : UInt256) : UInt256

Equations

• EvmYul.blobhash e i = Option.option { val := 0 } (EvmYul.UInt256.ofNat ∘ EvmYul.fromByteArrayBigEndian) e.blobVersionedHashes[i.toNat]?