Named Token Tutorial
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.
Last modified 2yr ago