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:
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.
Contracts Language ZF*
Common Goods Pool
Last modified 2yr ago