def UTxO.UTxOMap (α : Type) : Type

UTxOMap is a map Nat -> α where elements can be:

• minted and burn once
• modify data arbitrarily

Equations

• UTxO.UTxOMap α = List (Option α)

def UTxO.UTxOMap.init {α : Type} : UTxOMap α

Equations

• UTxO.UTxOMap.init = []

def UTxO.UTxOMap.get {α : Type} (m : UTxOMap α) (id : Nat) : Option α

Main get operation. This get does not diff between burnt and not-minted utxos. This is similar to Cardano and that's why in the spec Anastasia went on and wrote staking credentials scripts.

Equations

• m.get id = match Tokens.ListHelpers.split_at id m with | some (fst, e, snd) => e | none => none

instance UTxO.instMembershipNatUTxOMap {α : Type} : Membership Nat (UTxOMap α)

Equations

• UTxO.instMembershipNatUTxOMap = { mem := fun (m : UTxO.UTxOMap α) (tid : Nat) => match m.get tid with | none => False | some val => True }

def UTxO.UTxOMap.mint {α : Type} (m : UTxOMap α) (v : α) : UTxOMap α

Mint is always possible just concat it at the end.

Equations

• m.mint v = List.concat m (some v)

def UTxO.UTxOMap.last_id {α : Type} (m : UTxOMap α) : Option Nat

Equations

• UTxO.UTxOMap.last_id [] = none
• UTxO.UTxOMap.last_id (head :: tail) = some (head :: tail).length.pred

def UTxO.UTxOMap.last_id' {α : Type} (m : UTxOMap α) (_mnz : 0 < List.length m) : Nat

Equations

• m.last_id' _mnz = (List.length m).pred