# Named Token Tutorial

## Named Token

First we'll learn how to write a very simple contract, called the "Named Token" contract. The contract simply mints a token with an identifier specified by the issuer, and locks the specified amount of the token to the specified return address.

Let's specify the contract.

First - the issuer executes the contract, giving it the following data:

1. **name** `: string` The name of the issued token
2. **amount**`: uint64`: The issued amount of the token
3. **returnAddress**`: Zen.Types.lock`: The recipient of the token

Then - the contract mints the specified amount of the token using the given name as a subidentifier, and locks it to the specified return address.

The whole process looks like this:

![](https://743511345-files.gitbook.io/~/files/v0/b/gitbook-legacy-files/o/assets%2F-L9dN7pLc3A31eOxo1tu%2F-MQvYNrn03g-RwTIl6is%2F-MQve9fqACZW_2CcVaWZ%2FScreen%20Shot%202021-01-13%20at%2014.11.12.png?alt=media\&token=b3c2a1a4-0a03-4ce0-8bcc-143de14bae59)

Let's write the contract.

Create a text file called *"NamedToken.fst"*, the *"fst"* suffix is the standard suffix for **F\*** files.

At the top of the file put the module name - it should be identical to the file name (excluding the suffix):

```
module NamedToken
```

We should also load (using the `open` directive) a couple of useful modules (`Zen.Base`, `Zen.Cost`, and `Zen.Data`) into the namespace, which we'll use later on.

The file should now look like this:

```
module NamedToken

open Zen.Base
open Zen.Cost
open Zen.Data
```

Each contract should have at least 2 top-level functions: `main`, and `cf`.

The `main` function is the function which runs with each execution of the contract, and `cf` function is the function which describes the cost of the `main` function.

Let's write the `main` function, it should always have the following type signature:

```
main
    ( txSkel      : Zen.Types.txSkeleton  )
    ( context     : Zen.Types.context     )
    ( contractId  : Zen.Types.contractId  )
    ( command     : string                )
    ( sender      : Zen.Types.sender      )
    ( messageBody : option Zen.Types.data )
    ( wallet      : Zen.Types.wallet      )
    ( state       : option Zen.Types.data )
    : Zen.Types.contractResult `Zen.Cost.t` n
```

where `n` is the cost of the function and equal to `cf txSkel context command sender messageBody wallet state` \
(notice that `cf` doesn't take the `contractId` as an argument, since the cost shouldn't depend on it).

In practice we usually don't actually have to specify the types of the parameters, as they would be inferred by the compiler.

It should look like this:

```
let main txSkel context contractId command sender messageBody wallet state =
    ...
```

We haven't supplied the body of the function yet, which should go below that line (instead of the ellipsis).

The first thing we need to do is to parse the data - to extract the name, amount, and return address out of it.

The data should be sent to the contract through the `messageBody` parameter, in the form of a dictionary, which will contain the specified data as *(key, value)* pairs, where each key corresponds to one of the specified fields (**"name"**, **"amount"**, and **"returnAddress"**).

Since we assume `messageBody` is a dictionary, we need to try to extract a dictionary out of it - this is is done with the `tryDict` function, defined in `Zen.Data`.

The `tryDict` function has the following type signature:

```
tryDict: data -> option (Dict.t data) `cost` 4
```

Recall that the `data` type is a discriminated union of the following:

```
type data =
    | I64 of I64.t
    | Byte of U8.t
    | ByteArray: A.t U8.t -> data
    | U32 of U32.t
    | U64 of U64.t
    | String of string
    | Hash of hash
    | Lock of lock
    | Signature of signature
    | PublicKey of publicKey
    | Collection of dataCollection

and dataCollection =
    | Array of A.t data
    | Dict of dictionary data
    | List of list data
```

So what `tryDict` does, is taking a value of type `data`, and if that value is a `Collection(Dict(d))` - it returns `Some d`, and otherwise it returns `None`.

Now - since the `messageBody` is already an `option data`, we can't apply `tryDict` on it directly (since it expects a `data`), so instead we use the `(>!=)` operator from `Zen.Data` which have the following type signature:

```
(>!=) : option a -> (a -> cost (option b) n) -> cost (option b) n
```

The dictionary extraction should look like this:

```
messageBody >!= tryDict
```

Let's name the result as `dict`, using a `let` expression, so the `main` function should now look like this:

```
let main txSkel context contractId command sender messageBody wallet state =

    let dict = messageBody >!= tryDict in

    ...
```

`dict` will either contain a `Some d` (where `d` is a dictionary) or `None`.

Now that we have the dictionary, let's extract the required fields out of it, using the `tryFind` function (from `Zen.Dictionary`).

The `tryFind` function has the following type signature:

```
tryFind : string -> dictionary a -> option a `cost` 64
```

It takes a key name as an argument, and a dictionary, and if that dictionary has a value with the specified key name it returns it (within a `Some`), and otherwise returns `None`.

Since `dict` is an ``option (dictionary data) `cost` 64`` we can't use `tryFind` on it directly, so we'll use the `(>?=)` operator (defined in `Zen.Data`) instead.

The `(>?=)` operator has the following type signature:

```
(>?=) : option a `cost` m -> (a -> option b `cost` n) -> option b `cost` (m+n)
```

To extract the value of the **"returnAddress"** key, we'll do:

```
dict
>?= Zen.Dictionary.tryFind "returnAddress"
```

(notice we use the full qualified name here, since we didn't load the `Zen.Dictionary` module into the namespace with the `open` directive)

This will give us a (costed) `option data` value; to extract an actual lock out of that value we'll use the `tryLock` function (defined in `Zen.Data`):

```
dict
>?= Zen.Dictionary.tryFind "returnAddress"
>?= tryLock
```

Let's give a name to the extracted lock, using a `let!` expression.

```
let! returnAddress =
    dict
    >?= Zen.Dictionary.tryFind "returnAddress"
    >?= tryLock
in
```

The `let!` usage strips the cost out of the declared variable (using the cost monad), so it would be easier to work with - the type of `returnAddress` will be `option lock`, instead of ``option lock `cost` m``.

Now the whole `main` function should look like this:

```
let main txSkel context contractId command sender messageBody wallet state =

    let dict = messageBody >!= tryDict in

    let! returnAddress =
        dict
        >?= Zen.Dictionary.tryFind "returnAddress"
        >?= tryLock
    in

    ...
```

To extract the **"amount"** and **"name"** keys we'll do something similar (using `tryU64` and `tryString`, respectively, instead of `tryLock`):

```
let main txSkel context contractId command sender messageBody wallet state =

    let dict = messageBody >!= tryDict in

    let! returnAddress =
        dict
        >?= Zen.Dictionary.tryFind "returnAddress"
        >?= tryLock
    in

    let! amount =
        dict
        >?= Zen.Dictionary.tryFind "amount"
        >?= tryU64
    in

    let! name =
        dict
        >?= Zen.Dictionary.tryFind "name"
        >?= tryString
    in

    ...
```

Now that we have all of the data, we can use it assuming everything was provided by the issuer.

To consider both the case where the issuer has provided everything and the case where there is missing information, we pattern match on the data, like this:

```
match returnAddress,amount,name with
| Some returnAddress, Some amount, Some name ->
    ...
| _ ->
    ...
```

The 1st case will be executed when all the data was provided, and the 2nd case will be executed if any of the required parameters wasn't provided.

Let's throw an error when some of the parameters are missing.

```
match returnAddress,amount,name with
| Some returnAddress, Some amount, Some name ->
    ...
| _ ->
    Zen.ResultT.autoFailw "parameters are missing"
```

The function `autoFailw` in `Zen.ResultT` throws an error (within a `ResultT`) and infers the cost automatically.

If all the parameters were provided - we need to check that the provided name of the token is at most 32 characters, because that's the maximum size an asset subidentifier can have.

If the name is longer than 32 characters - we throw an error:

```
match returnAddress,amount,name with
| Some returnAddress, Some amount, Some name ->
    if FStar.String.length name <= 32 then
        ...
    else
        Zen.ResultT.autoFailw "name is too long"
| _ ->
    Zen.ResultT.autoFailw "parameters are missing"
```

In Zen Protocol assets are defined by 2 parts:

1. Main Identifier - The contract ID of the contract which have minted the asset.
2. Subidentifier - The unique ID of the asset, given by 32 bytes.

If the name is short enough to fit as an asset subidentifier - we can define a token with the given name as the subidentifier and the contract ID of this contract as the main identifier (using the `fromSubtypeString` function from `Zen.Asset`):

```
match returnAddress,amount,name with
| Some returnAddress, Some amount, Some name ->
    if FStar.String.length name <= 32 then
        begin
          let! token = Zen.Asset.fromSubtypeString contractId name in
          ...
        end
    else
        Zen.ResultT.autoFailw "name is too long"
| _ ->
    Zen.ResultT.autoFailw "parameters are missing"
```

(Notice that we're using `begin` and `end` here instead of parentheses, to make the code cleaner)

Now that we have defined the named token - we **mint** the specified amount of it, and then **lock** the minted tokens to the specified return address - this is done by modifying the supplied transaction (`txSkel`) with `mint`, and then modifying the result with `lockToAddress` (both are defined in `Zen.TxSkeleton`):

```
match returnAddress,amount,name with
| Some returnAddress, Some amount, Some name ->
    if FStar.String.length name <= 32 then
        begin
          let! token = Zen.Asset.fromSubtypeString contractId name in

          let! txSkel =
            Zen.TxSkeleton.mint amount token txSkel
            >>= Zen.TxSkeleton.lockToAddress token amount returnAddress in

          ...
        end
    else
        Zen.ResultT.autoFailw "name is too long"
| _ ->
    Zen.ResultT.autoFailw "parameters are missing"
```

Notice the syntax we're using here - both `mint` and `lockToAddress` return a costed `txSkeleton`, so to chain them we're using the `(>>=)` operator (bind) of the cost monad, and then we name the result using a `let!` so we can use it as a "pure" `txSkeleton` (instead of a **costed** `txSkeleton`).

Now that we've prepared the transaction - all that is left is to return it (using `ofTxSkel` from `Zen.ContractResult`), and the contract is done:

```
match returnAddress,amount,name with
| Some returnAddress, Some amount, Some name ->
    if FStar.String.length name <= 32 then
        begin
          let! token = Zen.Asset.fromSubtypeString contractId name in

          let! txSkel =
            Zen.TxSkeleton.mint amount token txSkel
            >>= Zen.TxSkeleton.lockToAddress token amount returnAddress in

          Zen.ContractResult.ofTxSkel txSkel
        end
    else
        Zen.ResultT.autoFailw "name is too long"
| _ ->
    Zen.ResultT.autoFailw "parameters are missing"
```

The whole file should now look like this:

```
module NamedToken

open Zen.Base
open Zen.Cost
open Zen.Data

let main txSkel context contractId command sender messageBody wallet state =

    let dict = messageBody >!= tryDict in

    let! returnAddress =
        dict
        >?= Zen.Dictionary.tryFind "returnAddress"
        >?= tryLock
    in

    let! amount =
        dict
        >?= Zen.Dictionary.tryFind "amount"
        >?= tryU64
    in

    let! name =
        dict
        >?= Zen.Dictionary.tryFind "name"
        >?= tryString
    in

    match returnAddress,amount,name with
    | Some returnAddress, Some amount, Some name ->
        if FStar.String.length name <= 32 then
            begin
              let! token = Zen.Asset.fromSubtypeString contractId name in

              let! txSkel =
                Zen.TxSkeleton.mint amount token txSkel
                >>= Zen.TxSkeleton.lockToAddress token amount returnAddress in

              Zen.ContractResult.ofTxSkel txSkel
            end
        else
            Zen.ResultT.autoFailw "name is too long"
    | _ ->
        Zen.ResultT.autoFailw "parameters are missing"
```

Now we can verify the validity of this file with:

```
zebra -v NamedToken.fst
```

It should verify successfully, returning:

```
zebra -v NamedToken.fst SDK: Verified
```

But hold on - **we aren't done yet!**

We have finished with the `main` function, but we still need to define the `cf` function.

The type signature of `cf` is:

```
cf
    ( txSkel      : Zen.Types.txSkeleton  )
    ( context     : Zen.Types.context     )
    ( command     : string                )
    ( sender      : Zen.Types.sender      )
    ( messageBody : option Zen.Types.data )
    ( wallet      : Zen.Types.wallet      )
    ( state       : option Zen.Types.data )
    : nat `cost` n
```

So we should add the `cf` function to the end of the file, like this:

```
let cf txSkel context command sender messageBody wallet state =
```

To start - let's give it to the value of `0` and then lift it into the cost monad with `Zen.Cost.ret`:

```
let cf txSkel context command sender messageBody wallet state =
    0
    |> Zen.Cost.ret
```

Let's try to **elaborate** the contract, to make sure the cost is correct.

```
zebra -e NamedToken.fst
```

You should get the following error:

```
(Error 19) Subtyping check failed; expected type
_: Zen.Types.Realized.txSkeleton ->
context: Zen.Types.Main.context ->
command: Prims.string ->
_: Zen.Types.Main.sender ->
messageBody: FStar.Pervasives.Native.option Zen.Types.Data.data ->
_: Zen.Types.Realized.wallet ->
state: FStar.Pervasives.Native.option Zen.Types.Data.data ->
Prims.Tot (Zen.Cost.Realized.cost Prims.nat (0 + 2)); got type
txSkel: Zen.Types.Realized.txSkeleton ->
context: Zen.Types.Main.context ->
command: Prims.string ->
sender: Zen.Types.Main.sender ->
messageBody: FStar.Pervasives.Native.option Zen.Types.Data.data ->
wallet: Zen.Types.Realized.wallet ->
state: FStar.Pervasives.Native.option Zen.Types.Data.data ->
Prims.Tot (Zen.Cost.Realized.cost Prims.int (0 + 2))
```

Notice how it infers that `cf` returns an `int`, while it should return a `nat`.

To solve it we need to **cast** the value of `cf` into a `nat`, using the `cast` function:

```
let cf txSkel context command sender messageBody wallet state =
    0
    |> cast nat
    |> Zen.Cost.ret
```

Let's elaborate it again, now we get the following error:

```
(Error 19) Subtyping check failed; expected type
txSkel: Zen.Types.Realized.txSkeleton ->
context: Zen.Types.Main.context ->
_: Zen.Types.Extracted.contractId ->
command: Prims.string ->
sender: Zen.Types.Main.sender ->
messageBody: FStar.Pervasives.Native.option Zen.Types.Data.data ->
wallet: Zen.Types.Realized.wallet ->
state: FStar.Pervasives.Native.option Zen.Types.Data.data ->
Prims.Tot
(Zen.Cost.Realized.cost Zen.Types.Main.contractResult
  (Zen.Cost.Realized.force (CostFunc?.f (Zen.Types.Main.CostFunc NamedToken.cf)
          txSkel
          context
          command
          sender
          messageBody
          wallet
          state))); got type
txSkel: Zen.Types.Realized.txSkeleton ->
context: Zen.Types.Main.context ->
contractId: Zen.Types.Extracted.contractId ->
command: Prims.string ->
sender: Zen.Types.Main.sender ->
messageBody: FStar.Pervasives.Native.option Zen.Types.Data.data ->
wallet: Zen.Types.Realized.wallet ->
state: FStar.Pervasives.Native.option Zen.Types.Data.data ->
Prims.Tot
(Zen.Cost.Realized.cost Zen.Types.Main.contractResult
  (4 + 64 + 2 + (4 + 64 + 2 + (4 + 64 + 2 + (64 + (64 + 64 + 3)))) + 54))
```

Look at the number at the bottom - this is the cost that was **inferred** by the compiler, so let's try to paste it into the function:

```
let cf txSkel context command sender messageBody wallet state =
    (4 + 64 + 2 + (4 + 64 + 2 + (4 + 64 + 2 + (64 + (64 + 64 + 3)))) + 54)
    |> cast nat
    |> Zen.Cost.ret
```

Let's try to elaborate again:

```
zebra -e NamedToken.fst SDK: Elaborating NamedToken.fst ... 
SDK: Wrote elaborated source to NamedToken.fst SDK: Verified
```

**Congratulations!**

You have written, elaborated, and verified your very first contract.

This time we were lucky - we didn't have to explicitly type our terms and the code was simple enough for the compiler to infer its cost.

With more complex contracts it might not be so easy - in many cases you'll have to explicitly type your terms to convince the compiler that the cost of the contract is what you claim it is.