structure Event (t : Type) : Type

• id : OutputRef
• info : t

@[reducible, inline]

abbrev DepositId : Type

Equations

• DepositId = OutputRef

structure DepositInfo : Type

• l2_address : Address
• l2_datum : Option Data

@[reducible, inline]

abbrev Deposits : Type

Equations

• Deposits = List (DepositId × DepositInfo)

@[reducible, inline]

abbrev DepositEvent : Type

Equations

• DepositEvent = Event DepositInfo

@[reducible, inline]

abbrev WithdrawalId : Type

Equations

• WithdrawalId = OutputRef

structure WithdrawalInfo : Type

• l2_outref : OutputRef
• l2_value : Value
• l1_address : Address
• l1_datum : Option Data

def instBEqWithdrawalInfo.beq : WithdrawalInfo → WithdrawalInfo → Bool

Equations

• One or more equations did not get rendered due to their size.
• instBEqWithdrawalInfo.beq x✝¹ x✝ = false

instance instBEqWithdrawalInfo : BEq WithdrawalInfo

Equations

• instBEqWithdrawalInfo = { beq := instBEqWithdrawalInfo.beq }

@[reducible, inline]

abbrev Withdrawal : Type

Equations

• Withdrawal = (WithdrawalId × WithdrawalInfo)

@[reducible, inline]

abbrev Withdrawals : Type

Equations

• Withdrawals = List Withdrawal

@[reducible, inline]

abbrev WithdrawalEvent : Type

Equations

• WithdrawalEvent = Event WithdrawalInfo

@[reducible, inline]

abbrev MidgardTx : Type

Equations

• MidgardTx = FlattenTransaction

@[reducible, inline]

abbrev TxOrderId : Type

Equations

• TxOrderId = OutputRef

@[reducible, inline]

abbrev TxOrderEvent : Type

Equations

• TxOrderEvent = Event MidgardTx

@[reducible, inline]

abbrev TransactionOrderMap : Type

Equations

• TransactionOrderMap = List (TxOrderId × MidgardTx)

structure MidgardTxSet (hash : MidgardTx → Hash_32) : Type

• map : Hash_32 → Option MidgardTx
• prop (k : Hash_32) (t : MidgardTx) : self.map k = some t → k = hash t

structure BlockBody : Type

• utxos : List (OutputRef × Output)
• transactions : TransactionOrderMap
• deposits : Deposits
• withdrawals : Withdrawals

@[reducible, inline]

abbrev HeaderHash : Type

Equations

• HeaderHash = Hash_28

structure Header : Type

• prev_utxos_root : Hash_64
• utxos_root : Hash_64
• transactions_root : Hash_64
• deposits_root : Hash_64
• withdrawals_root : Hash_64
• start_time : PosixTime
• end_time : PosixTime
• prev_header_hash : HeaderHash
• protocol_version : ℤ

def Header.genesis : Header

Equations

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

structure Block : Type

• header_hash : HeaderHash
• header : Header
• block_body : BlockBody

@[reducible, inline]

abbrev BlockId : Type

Equations

• BlockId = ℕ

structure SimpleHeader : Type

• utxo_root : NHash
• transactions_root : NHash
• deposits_root : NHash
• withdrawals_root : NHash
• prev_header_hash : NHash
• start_time : PosixTime
• end_time : PosixTime
• operator_vkey : OperatorId
• protocol_version : ℕ

def SimpleHeader.genesis : SimpleHeader

Equations

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