Named Token Tutorial

Search…
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):
1
module NamedToken
Copied!
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:
1
module NamedToken
2
​
3
open Zen.Base
4
open Zen.Cost
5
open Zen.Data
Copied!
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:
1
main
2
    ( txSkel      : Zen.Types.txSkeleton  )
3
    ( context     : Zen.Types.context     )
4
    ( contractId  : Zen.Types.contractId  )
5
    ( command     : string                )
6
    ( sender      : Zen.Types.sender      )
7
    ( messageBody : option Zen.Types.data )
8
    ( wallet      : Zen.Types.wallet      )
9
    ( state       : option Zen.Types.data )
10
    : Zen.Types.contractResult `Zen.Cost.t` n
Copied!
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:
1
let main txSkel context contractId command sender messageBody wallet state =
2
    ...
Copied!
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:
1
tryDict: data -> option (Dict.t data) `cost` 4
Copied!
Recall that the data type is a discriminated union of the following:
1
type data =
2
    | I64 of I64.t
3
    | Byte of U8.t
4
    | ByteArray: A.t U8.t -> data
5
    | U32 of U32.t
6
    | U64 of U64.t
7
    | String of string
8
    | Hash of hash
9
    | Lock of lock
10
    | Signature of signature
11
    | PublicKey of publicKey
12
    | Collection of dataCollection
13
​
14
and dataCollection =
15
    | Array of A.t data
16
    | Dict of dictionary data
17
    | List of list data
Copied!
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:
1
(>!=) : option a -> (a -> cost (option b) n) -> cost (option b) n
Copied!
The dictionary extraction should look like this:
1
messageBody >!= tryDict
Copied!
Let's name the result as dict, using a let expression, so the main function should now look like this:
1
let main txSkel context contractId command sender messageBody wallet state =
2
​
3
    let dict = messageBody >!= tryDict in
4
​
5
    ...
Copied!
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:
1
tryFind : string -> dictionary a -> option a `cost` 64
Copied!
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:
1
(>?=) : option a `cost` m -> (a -> option b `cost` n) -> option b `cost` (m+n)
Copied!
To extract the value of the "returnAddress" key, we'll do:
1
dict
2
>?= Zen.Dictionary.tryFind "returnAddress"
Copied!
(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):
1
dict
2
>?= Zen.Dictionary.tryFind "returnAddress"
3
>?= tryLock
Copied!
Let's give a name to the extracted lock, using a let! expression.
1
let! returnAddress =
2
    dict
3
    >?= Zen.Dictionary.tryFind "returnAddress"
4
    >?= tryLock
5
in
Copied!
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:
1
let main txSkel context contractId command sender messageBody wallet state =
2
​
3
    let dict = messageBody >!= tryDict in
4
​
5
    let! returnAddress =
6
        dict
7
        >?= Zen.Dictionary.tryFind "returnAddress"
8
        >?= tryLock
9
    in
10
​
11
    ...
Copied!
To extract the "amount" and "name" keys we'll do something similar (using tryU64 and tryString, respectively, instead of tryLock):
1
let main txSkel context contractId command sender messageBody wallet state =
2
​
3
    let dict = messageBody >!= tryDict in
4
​
5
    let! returnAddress =
6
        dict
7
        >?= Zen.Dictionary.tryFind "returnAddress"
8
        >?= tryLock
9
    in
10
​
11
    let! amount =
12
        dict
13
        >?= Zen.Dictionary.tryFind "amount"
14
        >?= tryU64
15
    in
16
​
17
    let! name =
18
        dict
19
        >?= Zen.Dictionary.tryFind "name"
20
        >?= tryString
21
    in
22
​
23
    ...
Copied!
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:
1
match returnAddress,amount,name with
2
| Some returnAddress, Some amount, Some name ->
3
    ...
4
| _ ->
5
    ...
Copied!
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.
1
match returnAddress,amount,name with
2
| Some returnAddress, Some amount, Some name ->
3
    ...
4
| _ ->
5
    Zen.ResultT.autoFailw "parameters are missing"
Copied!
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:
1
match returnAddress,amount,name with
2
| Some returnAddress, Some amount, Some name ->
3
    if FStar.String.length name <= 32 then
4
        ...
5
    else
6
        Zen.ResultT.autoFailw "name is too long"
7
| _ ->
8
    Zen.ResultT.autoFailw "parameters are missing"
Copied!
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):
1
match returnAddress,amount,name with
2
| Some returnAddress, Some amount, Some name ->
3
    if FStar.String.length name <= 32 then
4
        begin
5
          let! token = Zen.Asset.fromSubtypeString contractId name in
6
          ...
7
        end
8
    else
9
        Zen.ResultT.autoFailw "name is too long"
10
| _ ->
11
    Zen.ResultT.autoFailw "parameters are missing"
Copied!
(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):
1
match returnAddress,amount,name with
2
| Some returnAddress, Some amount, Some name ->
3
    if FStar.String.length name <= 32 then
4
        begin
5
          let! token = Zen.Asset.fromSubtypeString contractId name in
6
​
7
          let! txSkel =
8
            Zen.TxSkeleton.mint amount token txSkel
9
            >>= Zen.TxSkeleton.lockToAddress token amount returnAddress in
10
​
11
          ...
12
        end
13
    else
14
        Zen.ResultT.autoFailw "name is too long"
15
| _ ->
16
    Zen.ResultT.autoFailw "parameters are missing"
Copied!
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:
1
match returnAddress,amount,name with
2
| Some returnAddress, Some amount, Some name ->
3
    if FStar.String.length name <= 32 then
4
        begin
5
          let! token = Zen.Asset.fromSubtypeString contractId name in
6
​
7
          let! txSkel =
8
            Zen.TxSkeleton.mint amount token txSkel
9
            >>= Zen.TxSkeleton.lockToAddress token amount returnAddress in
10
​
11
          Zen.ContractResult.ofTxSkel txSkel
12
        end
13
    else
14
        Zen.ResultT.autoFailw "name is too long"
15
| _ ->
16
    Zen.ResultT.autoFailw "parameters are missing"
Copied!
The whole file should now look like this:
1
module NamedToken
2
​
3
open Zen.Base
4
open Zen.Cost
5
open Zen.Data
6
​
7
let main txSkel context contractId command sender messageBody wallet state =
8
​
9
    let dict = messageBody >!= tryDict in
10
​
11
    let! returnAddress =
12
        dict
13
        >?= Zen.Dictionary.tryFind "returnAddress"
14
        >?= tryLock
15
    in
16
​
17
    let! amount =
18
        dict
19
        >?= Zen.Dictionary.tryFind "amount"
20
        >?= tryU64
21
    in
22
​
23
    let! name =
24
        dict
25
        >?= Zen.Dictionary.tryFind "name"
26
        >?= tryString
27
    in
28
​
29
    match returnAddress,amount,name with
30
    | Some returnAddress, Some amount, Some name ->
31
        if FStar.String.length name <= 32 then
32
            begin
33
              let! token = Zen.Asset.fromSubtypeString contractId name in
34
​
35
              let! txSkel =
36
                Zen.TxSkeleton.mint amount token txSkel
37
                >>= Zen.TxSkeleton.lockToAddress token amount returnAddress in
38
​
39
              Zen.ContractResult.ofTxSkel txSkel
40
            end
41
        else
42
            Zen.ResultT.autoFailw "name is too long"
43
    | _ ->
44
        Zen.ResultT.autoFailw "parameters are missing"
Copied!
Now we can verify the validity of this file with:
1
zebra -v NamedToken.fst
Copied!
It should verify successfully, returning:
1
zebra -v NamedToken.fst SDK: Verified
Copied!
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:
1
cf
2
    ( txSkel      : Zen.Types.txSkeleton  )
3
    ( context     : Zen.Types.context     )
4
    ( command     : string                )
5
    ( sender      : Zen.Types.sender      )
6
    ( messageBody : option Zen.Types.data )
7
    ( wallet      : Zen.Types.wallet      )
8
    ( state       : option Zen.Types.data )
9
    : nat `cost` n
Copied!
So we should add the cf function to the end of the file, like this:
1
let cf txSkel context command sender messageBody wallet state =
Copied!
To start - let's give it to the value of 0 and then lift it into the cost monad with Zen.Cost.ret:
1
let cf txSkel context command sender messageBody wallet state =
2
    0
3
    |> Zen.Cost.ret
Copied!
Let's try to elaborate the contract, to make sure the cost is correct.
1
zebra -e NamedToken.fst
Copied!
You should get the following error:
1
(Error 19) Subtyping check failed; expected type
2
_: Zen.Types.Realized.txSkeleton ->
3
context: Zen.Types.Main.context ->
4
command: Prims.string ->
5
_: Zen.Types.Main.sender ->
6
messageBody: FStar.Pervasives.Native.option Zen.Types.Data.data ->
7
_: Zen.Types.Realized.wallet ->
8
state: FStar.Pervasives.Native.option Zen.Types.Data.data ->
9
Prims.Tot (Zen.Cost.Realized.cost Prims.nat (0 + 2)); got type
10
txSkel: Zen.Types.Realized.txSkeleton ->
11
context: Zen.Types.Main.context ->
12
command: Prims.string ->
13
sender: Zen.Types.Main.sender ->
14
messageBody: FStar.Pervasives.Native.option Zen.Types.Data.data ->
15
wallet: Zen.Types.Realized.wallet ->
16
state: FStar.Pervasives.Native.option Zen.Types.Data.data ->
17
Prims.Tot (Zen.Cost.Realized.cost Prims.int (0 + 2))
Copied!
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:
1
let cf txSkel context command sender messageBody wallet state =
2
    0
3
    |> cast nat
4
    |> Zen.Cost.ret
Copied!
Let's elaborate it again, now we get the following error:
1
(Error 19) Subtyping check failed; expected type
2
txSkel: Zen.Types.Realized.txSkeleton ->
3
context: Zen.Types.Main.context ->
4
_: Zen.Types.Extracted.contractId ->
5
command: Prims.string ->
6
sender: Zen.Types.Main.sender ->
7
messageBody: FStar.Pervasives.Native.option Zen.Types.Data.data ->
8
wallet: Zen.Types.Realized.wallet ->
9
state: FStar.Pervasives.Native.option Zen.Types.Data.data ->
10
Prims.Tot
11
(Zen.Cost.Realized.cost Zen.Types.Main.contractResult
12
  (Zen.Cost.Realized.force (CostFunc?.f (Zen.Types.Main.CostFunc NamedToken.cf)
13
          txSkel
14
          context
15
          command
16
          sender
17
          messageBody
18
          wallet
19
          state))); got type
20
txSkel: Zen.Types.Realized.txSkeleton ->
21
context: Zen.Types.Main.context ->
22
contractId: Zen.Types.Extracted.contractId ->
23
command: Prims.string ->
24
sender: Zen.Types.Main.sender ->
25
messageBody: FStar.Pervasives.Native.option Zen.Types.Data.data ->
26
wallet: Zen.Types.Realized.wallet ->
27
state: FStar.Pervasives.Native.option Zen.Types.Data.data ->
28
Prims.Tot
29
(Zen.Cost.Realized.cost Zen.Types.Main.contractResult
30
  (4 + 64 + 2 + (4 + 64 + 2 + (4 + 64 + 2 + (64 + (64 + 64 + 3)))) + 54))
Copied!
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:
1
let cf txSkel context command sender messageBody wallet state =
2
    (4 + 64 + 2 + (4 + 64 + 2 + (4 + 64 + 2 + (64 + (64 + 64 + 3)))) + 54)
3
    |> cast nat
4
    |> Zen.Cost.ret
Copied!
Let's try to elaborate again:
1
zebra -e NamedToken.fst SDK: Elaborating NamedToken.fst ... 
2
SDK: Wrote elaborated source to NamedToken.fst SDK: Verified
Copied!
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 1yr ago
Copy link