structure EvmYul.Transaction.Base : Type

BaseTransaction. Section 4.3.

• nonce n
• gasLimit g
• recipinet t
• value v
• r r
• s s
• data d/i

• nonce : UInt256
• gasLimit : UInt256
• recipient : Option AccountAddress
• value : UInt256
• r : ByteArray
• s : ByteArray
• data : ByteArray

instance EvmYul.Transaction.instBEqBase : BEq Base

Equations

• EvmYul.Transaction.instBEqBase = { beq := EvmYul.Transaction.beqBase✝ }

instance EvmYul.Transaction.instReprBase : Repr Base

Equations

• EvmYul.Transaction.instReprBase = { reprPrec := EvmYul.Transaction.reprBase✝ }

structure EvmYul.Transaction.WithAccessList : Type

AccessList. EIP-2930.

• chainId c
• accessList A
• yParity y

• chainId : UInt256
• accessList : List (AccountAddress × Array UInt256)
• yParity : UInt256

instance EvmYul.Transaction.instBEqWithAccessList : BEq WithAccessList

Equations

• EvmYul.Transaction.instBEqWithAccessList = { beq := EvmYul.Transaction.beqWithAccessList✝ }

instance EvmYul.Transaction.instReprWithAccessList : Repr WithAccessList

Equations

• EvmYul.Transaction.instReprWithAccessList = { reprPrec := EvmYul.Transaction.reprWithAccessList✝ }

structure EvmYul.Transaction.WithGasPrice : Type

WithGasPrice. Section 4.3.

• gasPrice p

• gasPrice : UInt256

instance EvmYul.Transaction.instBEqWithGasPrice : BEq WithGasPrice

Equations

• EvmYul.Transaction.instBEqWithGasPrice = { beq := EvmYul.Transaction.beqWithGasPrice✝ }

instance EvmYul.Transaction.instReprWithGasPrice : Repr WithGasPrice

Equations

• EvmYul.Transaction.instReprWithGasPrice = { reprPrec := EvmYul.Transaction.reprWithGasPrice✝ }

structure EvmYul.LegacyTransactionextends EvmYul.Transaction.Base, EvmYul.Transaction.WithGasPrice : Type

Type 0: LegacyTransaction. Section 4.3.

• nonce n
• gasLimit g
• recipinet t
• value v
• r r
• s s
• data d/i
• gasPrice p
• w w

• nonce : UInt256
• gasLimit : UInt256
• recipient : Option AccountAddress
• value : UInt256
• r : ByteArray
• s : ByteArray
• data : ByteArray
• gasPrice : UInt256
• w : UInt256

instance EvmYul.instBEqLegacyTransaction : BEq LegacyTransaction

Equations

• EvmYul.instBEqLegacyTransaction = { beq := EvmYul.beqLegacyTransaction✝ }

instance EvmYul.instReprLegacyTransaction : Repr LegacyTransaction

Equations

• EvmYul.instReprLegacyTransaction = { reprPrec := EvmYul.reprLegacyTransaction✝ }

structure EvmYul.AccessListTransactionextends EvmYul.Transaction.Base, EvmYul.Transaction.WithAccessList, EvmYul.Transaction.WithGasPrice : Type

Type 1: AccessListTransaction

• nonce n
• gasLimit g
• recipinet t
• value v
• r r
• s s
• data d/i
• chainId c
• accessList A
• yParity y
• gasPrice p

• nonce : UInt256
• gasLimit : UInt256
• recipient : Option AccountAddress
• value : UInt256
• r : ByteArray
• s : ByteArray
• data : ByteArray
• chainId : UInt256
• accessList : List (AccountAddress × Array UInt256)
• yParity : UInt256
• gasPrice : UInt256

instance EvmYul.instBEqAccessListTransaction : BEq AccessListTransaction

Equations

• EvmYul.instBEqAccessListTransaction = { beq := EvmYul.beqAccessListTransaction✝ }

instance EvmYul.instReprAccessListTransaction : Repr AccessListTransaction

Equations

• EvmYul.instReprAccessListTransaction = { reprPrec := EvmYul.reprAccessListTransaction✝ }

structure EvmYul.DynamicFeeTransactionextends EvmYul.Transaction.Base, EvmYul.Transaction.WithAccessList : Type

Type 2: DynamicFeeTransaction

• nonce n
• gasLimit g
• recipinet t
• value v
• r r
• s s
• data d/i
• chainId c
• accessList A
• yParity y
• maxFeePerGas m
• maxPriorityFeePerGas f

• nonce : UInt256
• gasLimit : UInt256
• recipient : Option AccountAddress
• value : UInt256
• r : ByteArray
• s : ByteArray
• data : ByteArray
• chainId : UInt256
• accessList : List (AccountAddress × Array UInt256)
• yParity : UInt256
• maxFeePerGas : UInt256
• maxPriorityFeePerGas : UInt256

instance EvmYul.instBEqDynamicFeeTransaction : BEq DynamicFeeTransaction

Equations

• EvmYul.instBEqDynamicFeeTransaction = { beq := EvmYul.beqDynamicFeeTransaction✝ }

instance EvmYul.instReprDynamicFeeTransaction : Repr DynamicFeeTransaction

Equations

• EvmYul.instReprDynamicFeeTransaction = { reprPrec := EvmYul.reprDynamicFeeTransaction✝ }

structure EvmYul.BlobTransactionextends EvmYul.DynamicFeeTransaction : Type

• nonce : UInt256
• gasLimit : UInt256
• recipient : Option AccountAddress
• value : UInt256
• r : ByteArray
• s : ByteArray
• data : ByteArray
• chainId : UInt256
• accessList : List (AccountAddress × Array UInt256)
• yParity : UInt256
• maxFeePerGas : UInt256
• maxPriorityFeePerGas : UInt256
• maxFeePerBlobGas : UInt256
• blobVersionedHashes : List ByteArray

instance EvmYul.instBEqBlobTransaction : BEq BlobTransaction

Equations

• EvmYul.instBEqBlobTransaction = { beq := EvmYul.beqBlobTransaction✝ }

instance EvmYul.instReprBlobTransaction : Repr BlobTransaction

Equations

• EvmYul.instReprBlobTransaction = { reprPrec := EvmYul.reprBlobTransaction✝ }

inductive EvmYul.Transaction : Type

• legacy : LegacyTransaction → Transaction
• access : AccessListTransaction → Transaction
• dynamic : DynamicFeeTransaction → Transaction
• blob : BlobTransaction → Transaction

instance EvmYul.instBEqTransaction : BEq Transaction

Equations

• EvmYul.instBEqTransaction = { beq := EvmYul.beqTransaction✝ }

instance EvmYul.instReprTransaction : Repr Transaction

Equations

• EvmYul.instReprTransaction = { reprPrec := EvmYul.reprTransaction✝ }

def EvmYul.Transaction.base : Transaction → Base

Equations

• (EvmYul.Transaction.legacy a).base = a.toBase
• (EvmYul.Transaction.access a).base = a.toBase
• (EvmYul.Transaction.dynamic a).base = a.toBase
• (EvmYul.Transaction.blob a).base = a.toBase

def EvmYul.Transaction.getAccessList : Transaction → List (AccountAddress × Array UInt256)

Equations

• (EvmYul.Transaction.legacy a).getAccessList = []
• (EvmYul.Transaction.access a).getAccessList = a.accessList
• (EvmYul.Transaction.dynamic a).getAccessList = a.accessList
• (EvmYul.Transaction.blob a).getAccessList = a.accessList

def EvmYul.Transaction.type : Transaction → UInt8

Equations

• (EvmYul.Transaction.legacy a).type = 0
• (EvmYul.Transaction.access a).type = 1
• (EvmYul.Transaction.dynamic a).type = 2
• (EvmYul.Transaction.blob a).type = 3

def EvmYul.Transaction.toBlobs (t : ℕ × ByteArray) : Option (String × String)

Equations

• EvmYul.Transaction.toBlobs t = do let rlpᵢ ← RLP (𝕋.𝔹 (BE t.1)) let rlp : ByteArray := t.2 pure (EvmYul.toHex rlpᵢ, EvmYul.toHex rlp)

def EvmYul.Transaction.computeTrieRoot (ts : Array ByteArray) : Option ByteArray

Equations

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

structure EvmYul.TransactionReceipt : Type

• type : UInt8
• statusCode : Bool
• cumulativeGasUsedInBlock : ℕ
• bloomFilter : ByteArray
• logSeries : LogSeries

instance EvmYul.instBEqTransactionReceipt : BEq TransactionReceipt

Equations

• EvmYul.instBEqTransactionReceipt = { beq := EvmYul.beqTransactionReceipt✝ }

instance EvmYul.instInhabitedTransactionReceipt : Inhabited TransactionReceipt

Equations

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

instance EvmYul.instReprTransactionReceipt : Repr TransactionReceipt

Equations

• EvmYul.instReprTransactionReceipt = { reprPrec := EvmYul.reprTransactionReceipt✝ }

def EvmYul.L_R : TransactionReceipt → 𝕋

Equations

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

def EvmYul.TransactionReceipt.toBlobs (w : ℕ × ByteArray) : Option (String × String)

Equations

• EvmYul.TransactionReceipt.toBlobs w = do let rlpᵢ ← RLP (𝕋.𝔹 (BE w.1)) let rlp ← some w.2 pure (EvmYul.toHex rlpᵢ, EvmYul.toHex rlp)

def EvmYul.TransactionReceipt.computeTrieRoot (ws : Array ByteArray) : Option ByteArray

Equations

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

def EvmYul.TransactionReceipt.toTrieValue (r : TransactionReceipt) : ByteArray

Equations

• r.toTrieValue = if r.type = 0 then (Option.get! ∘ RLP ∘ EvmYul.L_R) r else { data := #[r.type] } ++ (Option.get! ∘ RLP ∘ EvmYul.L_R) r