instance EvmYul.instReprFinsetBlockHeader : Repr (Finset BlockHeader)

Equations

• EvmYul.instReprFinsetBlockHeader = { reprPrec := fun (x : Finset EvmYul.BlockHeader) (x : ℕ) => Std.Format.text "Dummy Repr for ommers. TODO - change this :)." }

structure EvmYul.Transactions : Type

• trieRoot : ByteArray
• array : Array Transaction

instance EvmYul.instBEqTransactions : BEq Transactions

Equations

• EvmYul.instBEqTransactions = { beq := EvmYul.beqTransactions✝ }

instance EvmYul.instInhabitedTransactions : Inhabited Transactions

Equations

• EvmYul.instInhabitedTransactions = { default := { trieRoot := default, array := default } }

instance EvmYul.instReprTransactions : Repr Transactions

Equations

• EvmYul.instReprTransactions = { reprPrec := EvmYul.reprTransactions✝ }

structure EvmYul.Withdrawals : Type

• trieRoot : ByteArray
• array : Array Withdrawal

instance EvmYul.instBEqWithdrawals : BEq Withdrawals

Equations

• EvmYul.instBEqWithdrawals = { beq := EvmYul.beqWithdrawals✝ }

instance EvmYul.instInhabitedWithdrawals : Inhabited Withdrawals

Equations

• EvmYul.instInhabitedWithdrawals = { default := { trieRoot := default, array := default } }

instance EvmYul.instReprWithdrawals : Repr Withdrawals

Equations

• EvmYul.instReprWithdrawals = { reprPrec := EvmYul.reprWithdrawals✝ }

structure EvmYul.RawBlock : Type

• rlp : ByteArray
• exception : List String

instance EvmYul.instBEqRawBlock : BEq RawBlock

Equations

• EvmYul.instBEqRawBlock = { beq := EvmYul.beqRawBlock✝ }

instance EvmYul.instInhabitedRawBlock : Inhabited RawBlock

Equations

• EvmYul.instInhabitedRawBlock = { default := { rlp := default, exception := default } }

instance EvmYul.instReprRawBlock : Repr RawBlock

Equations

• EvmYul.instReprRawBlock = { reprPrec := EvmYul.reprRawBlock✝ }

@[reducible, inline]

abbrev EvmYul.RawBlocks : Type

Equations

• EvmYul.RawBlocks = Array EvmYul.RawBlock

structure EvmYul.DeserializedBlock : Type

• hash : UInt256
• blockHeader : BlockHeader
• transactions : Transactions
• withdrawals : Withdrawals
• exception : List String

instance EvmYul.instBEqDeserializedBlock : BEq DeserializedBlock

Equations

• EvmYul.instBEqDeserializedBlock = { beq := EvmYul.beqDeserializedBlock✝ }

instance EvmYul.instInhabitedDeserializedBlock : Inhabited DeserializedBlock

Equations

• EvmYul.instInhabitedDeserializedBlock = { default := { hash := default, blockHeader := default, transactions := default, withdrawals := default, exception := default } }

instance EvmYul.instReprDeserializedBlock : Repr DeserializedBlock

Equations

• EvmYul.instReprDeserializedBlock = { reprPrec := EvmYul.reprDeserializedBlock✝ }

@[reducible, inline]

abbrev EvmYul.DeserializedBlocks : Type

Equations

• EvmYul.DeserializedBlocks = Array EvmYul.DeserializedBlock

structure EvmYul.ProcessedBlock : Type

• hash : UInt256
• blockHeader : BlockHeader
• σ : AccountMap

instance EvmYul.instBEqProcessedBlock : BEq ProcessedBlock

Equations

• EvmYul.instBEqProcessedBlock = { beq := EvmYul.beqProcessedBlock✝ }

instance EvmYul.instInhabitedProcessedBlock : Inhabited ProcessedBlock

Equations

• EvmYul.instInhabitedProcessedBlock = { default := { hash := default, blockHeader := default, σ := default } }

instance EvmYul.instReprProcessedBlock : Repr ProcessedBlock

Equations

• EvmYul.instReprProcessedBlock = { reprPrec := EvmYul.reprProcessedBlock✝ }

@[reducible, inline]

abbrev EvmYul.ProcessedBlocks : Type

Equations

• EvmYul.ProcessedBlocks = Array EvmYul.ProcessedBlock

def EvmYul.validateUInt256 (b : ByteArray) (e : EVM.Exception) : Except EVM.Exception UInt256

Equations

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

def EvmYul.validateUInt64 (b : ByteArray) (e : EVM.Exception) : Except EVM.Exception UInt64

Equations

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

def EvmYul.validateAccountAddress (a : ByteArray) (e : EVM.Exception) : Except EVM.Exception AccountAddress

Equations

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

def EvmYul.deserializeBlock (rlp : ByteArray) : Except EVM.Exception (UInt256 × BlockHeader × Transactions × Withdrawals)

Equations

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

def EvmYul.deserializeBlock.parseWithdrawal : 𝕋 → Except EVM.Exception Withdrawal

Equations

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

def EvmYul.deserializeBlock.parseWithdrawals : 𝕋 → Except EVM.Exception (List Withdrawal)

Equations

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

def EvmYul.deserializeBlock.parseStorageKey : 𝕋 → Except EVM.Exception UInt256

Equations

• One or more equations did not get rendered due to their size.
• EvmYul.deserializeBlock.parseStorageKey (𝕋.𝔹 key) = pure (EvmYul.UInt256.ofNat (EvmYul.fromByteArrayBigEndian key))

def EvmYul.deserializeBlock.parseAccessListEntry : 𝕋 → Except EVM.Exception (AccountAddress × Array UInt256)

Equations

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

def EvmYul.deserializeBlock.parseBlobVersionHash : 𝕋 → Except EVM.Exception ByteArray

Equations

• One or more equations did not get rendered due to their size.
• EvmYul.deserializeBlock.parseBlobVersionHash (𝕋.𝔹 key) = pure key

def EvmYul.deserializeBlock.parseTransaction : 𝕋 → Except EVM.Exception Transaction

Equations

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

def EvmYul.deserializeBlock.parseTransactions : 𝕋 → Except EVM.Exception (List Transaction)

Equations

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

def EvmYul.deserializeBlock.parseHeader : 𝕋 → Except EVM.Exception BlockHeader