State

We use our small implementation of Tokens as tokens to model this module. There are three different tokens, deposits, withdrawals, and transaction orders.

Since token names match l1_nonces from Cardano, they are unique. And linkable to L1.

structure Bridge.State.GenDatum (event_type : Type) : Type

Generic datum structure. The structure itself change a bit from the initial spec to the current one. Deposits and Transaction Orders still have this format

• event : event_type
• inclusion_time : PosixTime
• witness : NHash
• refund_address : Address
• refund_datum : Option Data

structure Bridge.State.DepositDatum : Type

• event : DepositEvent
• inclusion_time : PosixTime
• witness : NHash

@[reducible, inline]

abbrev Bridge.State.WithdrawalDatum : Type

Equations

• Bridge.State.WithdrawalDatum = Bridge.State.GenDatum WithdrawalEvent

@[reducible, inline]

abbrev Bridge.State.TransactionDatum : Type

Equations

• Bridge.State.TransactionDatum = Bridge.State.GenDatum TxOrderEvent

structure Bridge.State.Events (α : Type) : Type

• deposits : UTxO.UTxOMap α
• depositTokens : Tokens.State.Tokens Unit

instance Bridge.State.instEmptyCollectionEvents {α : Type} : EmptyCollection (Events α)

Equations

• Bridge.State.instEmptyCollectionEvents = { emptyCollection := { deposits := UTxO.UTxOMap.init, depositTokens := Tokens.State.Tokens.init } }

@[reducible, inline]

abbrev Bridge.State.Deposits : Type

Equations

• Bridge.State.Deposits = Bridge.State.Events Bridge.State.DepositDatum

@[reducible, inline]

abbrev Bridge.State.Withdrawals : Type

Equations

• Bridge.State.Withdrawals = Bridge.State.Events Bridge.State.WithdrawalDatum

@[reducible, inline]

abbrev Bridge.State.TxOrders : Type

Equations

• Bridge.State.TxOrders = Bridge.State.Events Bridge.State.TransactionDatum

structure Bridge.State.EventMap : Type

• deposits : Deposits
• withdrawals : Withdrawals
• txOrders : TxOrders

def Bridge.State.EventMap.init : EventMap

Equations

• Bridge.State.EventMap.init = { deposits := ∅, withdrawals := ∅, txOrders := ∅ }

Events

inductive Bridge.State.DepositActions : Type

• AuthDeposit : DepositActions
• BurnDeposit : DepositActions
• DepositSpend : DepositActions

inductive Bridge.State.WithdrawalActions : Type

inductive Bridge.State.TxOrderActions : Type

inductive Bridge.State.Actions : Type

• Deposit : DepositActions → Actions
• Withdrawal : WithdrawalActions → Actions
• TxOrder : TxOrderActions → Actions