(***************************************************)
(***************************************************)
let nil_msg = Nil {Message} in
Cons {Message} msg nil_msg
let msgs_tmp = one_msg msg2 in
Cons {Message} msg1 msgs_tmp
fun (some_bal: Option Uint256) =>
| CodeNotApprovedSpenderOrOperator
| CodeNotContractOwner => Int32 -1
| CodeTokenExists => Int32 -3
| CodeIsNotMinter => Int32 -4
| CodeNotApproved => Int32 -5
| CodeNotTokenOwner => Int32 -6
| CodeNotFound => Int32 -7
| CodeNotApprovedForAll => Int32 -8
| CodeNotOwnerOrOperator => Int32 -9
| CodeNotApprovedSpenderOrOperator => Int32 -10
{ _exception : "Error"; code : result_code }
(***************************************************)
(* The contract definition *)
(***************************************************)
contract NonfungibleToken
(* Mapping of minters available *)
field minters: Map ByStr20 Dummy =
let emp_map = Emp ByStr20 Dummy in
builtin put emp_map contract_owner verdad
(* Mapping between token_id to token_owner *)
field token_owners: Map Uint256 ByStr20 = Emp Uint256 ByStr20
(* Mapping from owner to number of owned tokens *)
field owned_token_count: Map ByStr20 Uint256 = Emp ByStr20 Uint256
(* Mapping between token_id to approved address *)
(* @dev: There can only be one approved address per token at any given time. *)
field token_approvals: Map Uint256 ByStr20 = Emp Uint256 ByStr20
(* Mapping of token_owner to operator *)
field operator_approvals: Map ByStr20 (Map ByStr20 Dummy)
= Emp ByStr20 (Map ByStr20 Dummy)
(* Mapping from token_id to token_uri *)
field token_uris: Map Uint256 String = Emp Uint256 String
field total_supply: Uint256 = Uint256 0
procedure ThrowError(err : Error)
procedure IsContractOwner()
is_contract_owner = builtin eq contract_owner _sender;
match is_contract_owner with
err = CodeNotContractOwner;
procedure IsSelf(address_a: ByStr20, address_b: ByStr20)
is_self = builtin eq address_a address_b;
procedure IsTokenExists(token_id: Uint256)
token_exist <- exists token_owners[token_id];
procedure IsMinter(address: ByStr20)
is_minter <- exists minters[_sender];
procedure IsTokenOwner(token_id: Uint256, address: ByStr20)
some_token_owner <- token_owners[token_id];
match some_token_owner with
is_token_owner = builtin eq addr address;
match is_token_owner with
procedure IsApprovedForAll(token_owner: ByStr20, operator: ByStr20)
is_operator_approved <- exists operator_approvals[token_owner][operator];
match is_operator_approved with
err = CodeNotApprovedForAll;
procedure IsOwnerOrOperator(token_owner: ByStr20)
is_owner = builtin eq _sender token_owner;
is_approved_for_all <- exists operator_approvals[token_owner][_sender];
is_authorised = orb is_owner is_approved_for_all;
err = CodeNotOwnerOrOperator;
procedure IsApprovedSpenderOrOperator(token_id: Uint256, token_owner: ByStr20)
some_token_approval <- token_approvals[token_id];
is_approved = match some_token_approval with
| Some approved_address =>
builtin eq _sender approved_address
is_operator <- exists operator_approvals[token_owner][_sender];
is_authorised = orb is_approved is_operator;
err = CodeNotApprovedSpenderOrOperator;
procedure UpdateTokenCount(operation: Operation, address: ByStr20)
some_to_count <- owned_token_count[address];
let current_count = get_bal some_to_count in
builtin add current_count one;
owned_token_count[address] := new_to_count
some_from_count <- owned_token_count[address];
let current_count = get_bal some_from_count in
let is_zero = builtin eq current_count zero in
| False => builtin sub current_count one
owned_token_count[address] := new_from_count
(* @dev: Get number of NFTs assigned to a token_owner *)
transition BalanceOf(address: ByStr20)
some_bal <- owned_token_count[address];
balance = get_bal some_bal;
msg_to_sender = { _tag : "BalanceOfCallBack"; _recipient : _sender; _amount : Uint128 0;
msgs = one_msg msg_to_sender;
(* @dev: Get total supply of NFTs minted *)
current_supply <- total_supply;
msg_to_sender = { _tag : "TotalSupplyCallBack"; _recipient : _sender; _amount : Uint128 0;
total_supply : current_supply};
msgs = one_msg msg_to_sender;
(* @dev: Get name of the NFTs *)
msg_to_sender = { _tag : "NameCallBack"; _recipient : _sender; _amount : Uint128 0;
msgs = one_msg msg_to_sender;
(* @dev: Get name of the NFTs *)
msg_to_sender = { _tag : "SymbolCallBack"; _recipient : _sender; _amount : Uint128 0;
msgs = one_msg msg_to_sender;
(* @dev: Get approved_addr for token_id *)
transition GetApproved(token_id: Uint256)
some_token_approval <- token_approvals[token_id];
match some_token_approval with
msg_to_sender = { _tag : "GetApprovedCallBack"; _recipient : _sender; _amount : Uint128 0;
approved_addr : addr; token_id : token_id};
msgs = one_msg msg_to_sender;
(* @dev: Get the token_uri of a certain token_id *)
transition GetTokenURI(token_id: Uint256)
some_token_uri <- token_uris[token_id];
match some_token_uri with
msg_to_sender = { _tag : "GetTokenURICallBack"; _recipient : _sender; _amount : Uint128 0;
msgs = one_msg msg_to_sender;
(* @dev: Check if a token_id is owned by a token_owner *)
transition CheckTokenOwner(token_id: Uint256, address: ByStr20)
IsTokenOwner token_id address;
msg_to_sender = { _tag : "IsOwnerCallBack"; _recipient : _sender; _amount : Uint128 0};
msgs = one_msg msg_to_sender;
(* @dev: Check if address is operator for token_owner *)
transition CheckApprovedForAll(token_owner: ByStr20, operator: ByStr20)
IsApprovedForAll token_owner operator;
msg_to_sender = { _tag : "IsApprovedForAllCallBack"; _recipient : _sender; _amount : Uint128 0};
msgs = one_msg msg_to_sender;
(* Interface transitions *)
(* @dev: Add or remove approved minters. Only contract_owner can approve minters. *)
(* @param: minter - Address of the minter to be approved or removed *)
transition ConfigureMinter(minter: ByStr20)
some_minter <- minters[minter];
e = {_eventname: "RemovedMinterSuccess"; minter: minter};
minters[minter] := verdad;
e = {_eventname: "AddMinterSuccess"; minter: minter};
(* @dev: Mint new tokens. Only minters can mint. *)
(* @param: to - Address of the token recipient *)
(* @param: token_uri - URI of the the new token to be minted *)
transition Mint(to: ByStr20, token_uri: String)
UpdateTokenCount add_operation to;
(* Add to total_supply *)
current_supply <- total_supply;
new_supply = builtin add current_supply one;
total_supply := new_supply;
(* Initiate token_id and check conditions *)
(* Mint new non-fungible token *)
token_owners[token_id] := to;
(* Add token_uri for token_id *)
token_uris[token_id] := token_uri;
token_approvals[token_id] := dex_address;
e = {_eventname: "AddApprovalSuccess"; initiator: _sender; approved_addr: dex_address; token: token_id};
e = {_eventname: "MintSuccess"; by: _sender; recipient: to;
token_id: token_id; token_uri: token_uri};
msg_to_recipient = { _tag : "RecipientAcceptMint"; _recipient : to; _amount : Uint128 0 };
msg_to_sender = { _tag : "MintCallBack"; _recipient : _sender; _amount : Uint128 0;
recipient : to; token_id : token_id; token_uri : token_uri };
msgs = two_msgs msg_to_recipient msg_to_sender;
(* @dev: Burn existing tokens. Only token_owner or an operator can burn a NFT. *)
(* @param: token_id - Unique ID of the NFT to be destroyed *)
transition Burn(token_id: Uint256)
(* Check if token exists *)
some_token_owner <- token_owners[token_id];
match some_token_owner with
IsOwnerOrOperator token_owner;
(* Destroy existing token *)
delete token_owners[token_id];
delete token_approvals[token_id];
delete token_uris[token_id];
(* Deduct from owned_token_count *)
UpdateTokenCount sub_operation token_owner;
(* Deduct from total_supply *)
current_supply <- total_supply;
new_supply = builtin sub current_supply one;
total_supply := new_supply;
e = {_eventname: "BurnSuccess"; initiator: _sender; burn_address: token_owner; token: token_id};
msg_to_sender = { _tag : "BurnCallBack"; _recipient : _sender; _amount : Uint128 0;
initiator : _sender; burn_address : token_owner; token_id : token_id };
msgs = one_msg msg_to_sender;
(* @dev: Approves OR remove an address ability to transfer a given token_id *)
(* There can only be one approved_spender per token at any given time *)
(* param: to - Address to be approved for the given token_id *)
(* param: token_id - Unique ID of the NFT to be approved *)
transition SetApprove(to: ByStr20, token_id: Uint256)
some_token_owner <- token_owners[token_id];
match some_token_owner with
IsOwnerOrOperator token_owner;
is_approved <- exists token_approvals[token_id];
(* Remove approved_spender *)
delete token_approvals[token_id];
e = {_eventname: "RemoveApprovalSuccess"; initiator: _sender; removed_spender: to; token_id: token_id};
msg_to_sender = { _tag : "RemoveApprovalSuccessCallBack"; _recipient : _sender; _amount : Uint128 0;
removed_spender : to; token_id : token_id };
msgs = one_msg msg_to_sender;
(* Add approved_spender *)
token_approvals[token_id] := to;
e = {_eventname: "AddApprovalSuccess"; initiator: _sender; approved_addr: to; token: token_id};
msg_to_sender = { _tag : "AddApprovalSuccessCallBack"; _recipient : _sender; _amount : Uint128 0;
approved_spender : to; token_id : token_id };
msgs = one_msg msg_to_sender;
(* @dev: Sets or unsets an operator for the _sender *)
(* @param: to - Address to be set or unset as an operator *)
transition SetApprovalForAll(to: ByStr20)
is_operator <- exists operator_approvals[_sender][to];
operator_approvals[_sender][to] := verdad;
e = {_eventname: "AddApprovalForAllSuccess"; initiator: _sender; operator: to};
delete operator_approvals[_sender][to];
e = {_eventname: "RemoveApprovalForAllSuccess"; initiator: _sender; operator: to};
new_status = negb is_operator;
msg_to_sender = { _tag : "SetApprovalForAllSuccessCallBack"; _recipient : _sender; _amount : Uint128 0;
operator : to; status : new_status};
msgs = one_msg msg_to_sender;
(* @dev: Transfer the ownership of a given token_id to another address. token_owner only transition. *)
(* @param: to - Recipient address for the token *)
(* @param: token_id - Unique ID of the NFT to be transferred *)
transition Transfer(to: ByStr20, token_id: Uint256)
IsTokenOwner token_id _sender;
(* Change token_owner for that token_id *)
token_owners[token_id] := to;
(* Delete tokenApproval entry for that token_id *)
delete token_approvals[token_id];
(* Subtract one from previous token owner count *)
UpdateTokenCount sub_operation _sender;
(* Add one to the new token owner count *)
UpdateTokenCount add_operation to;
e = {_eventname: "TransferSuccess"; from: _sender; recipient: to; token: token_id};
msg_to_recipient = { _tag : "RecipientAcceptTransfer"; _recipient : to; _amount : Uint128 0;
from : _sender; recipient : to; token_id : token_id };
msg_to_sender = { _tag : "TransferSuccessCallBack"; _recipient : _sender; _amount : Uint128 0;
from : _sender; recipient : to; token_id : token_id };
msgs = two_msgs msg_to_recipient msg_to_sender;
(* @dev: Transfer the ownership of a given token_id to another address. approved_spender or operator only transition. *)
(* @param: to - Recipient address for the NFT *)
(* @param: token_id - Unique ID of the NFT to be transferred *)
transition TransferFrom(to: ByStr20, token_id: Uint256)
some_token_owner <- token_owners[token_id];
match some_token_owner with
IsApprovedSpenderOrOperator token_id token_owner;
(* Change token_owner for that token_id *)
token_owners[token_id] := to;
(* Delete tokenApproval entry for that token_id *)
delete token_approvals[token_id];
(* Subtract one from previous token owner count *)
UpdateTokenCount sub_operation token_owner;
(* Add one to the new token owner count *)
UpdateTokenCount add_operation to;
e = {_eventname: "TransferFromSuccess"; from: token_owner; recipient: to; token: token_id};
msg_to_recipient = { _tag : "RecipientAcceptTransferFrom"; _recipient : to; _amount : Uint128 0;
from : token_owner; recipient : to; token_id : token_id };
msg_to_sender = { _tag : "TransferFromSuccessCallBack"; _recipient : _sender; _amount : Uint128 0;
from : token_owner; recipient : to; token_id : token_id };
msgs = two_msgs msg_to_recipient msg_to_sender;