Settlement State

We represent the settlement module as a collection of tokens.

Disclaimer! The spec has UTxOs and Tokens. Settlement UTxOs have data while tokens have no data. To simplify our spec, we unify them, and we have Tokens with the corresponding UTxO data.

There is a catch here tho. We are not modelling authentication, we simply leave that to abstractions closer to the actual smart contracts code. Since we do not need these tokens, and we unified them, we simply have a collection of settlement utxos represented as a map. Because of this, we do not implement Resolve.

structure Settlement.State.ResolutionClaim : Type

Settlement UTxO datum is composed of deposits, withdrawals and transaction hashes.

• time : PosixTime
• operator : VKeyHash

structure Settlement.State.Settlement : Type

• deposits_root : NHash
• withdrawals_root : NHash
• transactions_root : NHash
• resolution_claim : Option ResolutionClaim

@[reducible, inline]

abbrev Settlement.State.SettlementSt : Type

Equations

• Settlement.State.SettlementSt = Tokens.State.Tokens Settlement.State.Settlement

inductive Settlement.State.UnprocessedEvent : Type

• Deposit (dep_id : Tokens.Elem.TId) : UnprocessedEvent
• Withdrawal (with_id : Tokens.Elem.TId) : UnprocessedEvent
• TxOrder (txo_id : Tokens.Elem.TId) : UnprocessedEvent

inductive Settlement.State.Actions : Type

Actions in the Settlement Module. We are not modelling access control here, so I don't need to mint/burn access tokens. Without the need of tokens, actions Actions.Spawn and Actions.Resolve are a bit different. In particular, we do not need to have Actions.Resolve.

• Spawn (header : StateQueue.State.HashHeader) : Actions
• Remove (settlement_id : Tokens.Elem.TId) : Actions
• AttachResolutionClaim (settlement_id : Tokens.Elem.TId) (res_time : PosixTime) (operator : VKeyHash) : Actions
• DisproveResolutionClaim (sett_id : Tokens.Elem.TId) : Actions