Cardano Tokens

We use Cardano Tokens to contain element of a given datum. In particular, it is just parcial map from IDs to such datums. We do not check ownership, ownership here is expressed simply has knowing the correct id. In Cardano, ownership is by literally having/owning such tokens.

A main difference with UTxOs is that to everyone has access to UTxOs, but not anyone can authenticate to use it. We have Credentials. Another difference is that there is no creation checks when creating UTxOs, so the mere existence of UTxOs is not proof of anything. Tokens on the other side, when belonging to a given PolicyId P, their existence has attached the fact that the policyid P was triggered.

Since we avoid all this know, UTxOs and Tokens are quite similar.

@[reducible, inline]

abbrev Tokens.State.Tokens (α : Type) : Type

Tokens are a stateful list of maybe tokens. This is a map m: Tokens α ≃ (id : Nat) -> Option (TokenD α).

Equations

• Tokens.State.Tokens α = List (Option (Tokens.Elem.TokenD α))

def Tokens.State.Tokens.init {α : Type} : Tokens α

Initialization is just empty

Equations

• Tokens.State.Tokens.init = []

def Tokens.State.Tokens.get {α : Type} (tid : Elem.TId) (s : Tokens α) : Option (Elem.TokenD α)

We can get the value in a map, if it is in the map.

Equations

• Tokens.State.Tokens.get tid s = match Tokens.ListHelpers.split_at tid s with | some (fst, x, snd) => x | none => none

instance Tokens.State.instMembershipTIdTokens {α : Type} : Membership Elem.TId (Tokens α)

We define the notino of a member as if we can get the element

Equations

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

def Tokens.State.Tokens.get_proj {α β : Type} (tid : Elem.TId) (f : α → β) (s : Tokens α) : Option β

Simply helper function.

Equations

• Tokens.State.Tokens.get_proj tid f s = (f ∘ fun (x : Tokens.Elem.TokenD α) => x.data) <$> Tokens.State.Tokens.get tid s

def Tokens.State.Tokens.get_name {α : Type} (tkn : Elem.TId) (s : Tokens α) : Option String

Tokens have names.

Equations

• Tokens.State.Tokens.get_name tkn s = (fun (x : Tokens.Elem.TokenD α) => Nat.repr x.id) <$> Tokens.State.Tokens.get tkn s

def Tokens.State.Tokens.update {α : Type} (tid : Elem.TId) (fv : Elem.TokenD α → Option (Elem.TokenD α)) (s : Tokens α) : Option (Tokens α)

This is an interal update function. We can update the value of an existing tokens, and destroy it. This should be internal to tokens.

Equations

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

def Tokens.State.Tokens.update_data {α : Type} (tid : Elem.TId) (f : α → α) (s : Tokens α) : Option (Tokens α)

Update the data of an existing tokens, without destroying it.

Equations

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

def Tokens.State.Tokens.mint' {α : Type} (_nm : String) (d : α) (s : Tokens α) : Tokens α × Elem.TId

Internal token minting. Tokens know their ids. In a way, tokens know themselves internally too. Correct token instances are generated by exercising only the Token Api.

Equations

• Tokens.State.Tokens.mint' _nm d s = (List.concat s (some { name := (), data := d, id := List.length s }), List.length s)

def Tokens.State.Tokens.mint {α : Type} (nm : String) (d : α) (s : Tokens α) : Tokens α

A normal minting without exposing the id.

Equations

• Tokens.State.Tokens.mint nm d s = (Tokens.State.Tokens.mint' nm d s).fst

def Tokens.State.Tokens.burn {α : Type} (tid : Elem.TId) (s : Tokens α) : Option (Tokens α)

Burning a token (defined using update)

Equations

• Tokens.State.Tokens.burn tid s = Tokens.State.Tokens.update tid (fun (x : Tokens.Elem.TokenD α) => none) s

def Tokens.State.Tokens.last_id {α : Type} (s : Tokens α) : Elem.TId

This is useful to write properties and it is offchain information. We can program this operation by monitoring the evolution of smart contracts.

Equations

• s.last_id = (List.length s).pred

def Tokens.State.size {α : Type} : Tokens α → Nat

This is also internal and mesuares the tokens alive in a map.

Equations

• Tokens.State.size s = (List.filter (fun (x : Option (Tokens.Elem.TokenD α)) => x.isSome) s).length