See presentation article:
The contract declares two assets:
asset ledger identified by holder to big_map {holder : address;tokens : nat = 0;} initialized by {{ holder = caller; tokens = totalsupply }}
The ledger
asset is the cap table: it holds the number of tokens for each token holder. totalsupply
is the initial number of tokens held by the originator of the contract.
asset allowance identified by addr_owner addr_spender to big_map {addr_owner : address;addr_spender : address;amount : nat;}
The allowance
asset stores the amount of tokens that can be spent by addr_spender
on the behalf of addr_owner
.
ledger.sum(tokens) = totalsupply
No token is minted: the total number of tokens is equal to the initial
totalsupply
number of tokens, regardless of the state of the storage.
Archetype implementation:
entry %transfer (%from : address, %to : address, value : nat) {require {r1 otherwise "NotEnoughBalance" : ledger[%from].tokens >= value;}effect {if caller <> %from then (var current = allowance[(%from, caller)].amount;dofailif(current < value, ("NotEnoughAllowance", ((value, current))));allowance.update((%from, caller), { amount -= value }););ledger.update(%from, { tokens -= value });ledger.addupdate(%to, { tokens += value });}}
%from <> %to ->let some before_ledger_from = before.ledger[%from] inlet some after_ledger_from = ledger[%from] inafter_ledger_from = { before_ledger_from withtokens = abs (before_ledger_from.tokens - value)}otherwise falseotherwise false
When the
%to
address is different from the%from
address, the number of tokens%to
possesses is decread byvalue
.
%from <> %to ->let some after_ledger_to = ledger[%to] inlet some before_ledger_to = before.ledger[%to] inafter_ledger_to = { before_ledger_to withtokens = (before_ledger_to.tokens + value)}otherwiseafter_ledger_to = { holder = %to; tokens = value }otherwise false
When the
%to
address is different from the%from
address, the number of tokens%to
possesses is increased byvalue
when%to
is already registered in the ledger, and set tovalue
otherwise. Anyway,%to
is registered in ledger.
%from = %to -> ledger = before.ledger
No effect on ledger when
%from
is equal to%to
.
forall tokenholder in ledger,tokenholder.holder <> %from ->tokenholder.holder <> %to ->before.ledger[tokenholder.holder] = some(tokenholder)
Tokenholders other than
%from
and%to
, are not modified nor added toledger
.
removed.ledger.isempty()
No record is removed from
ledger
.
let some before_to = before.ledger[%to] inadded.ledger.isempty()otherwiseadded.ledger = [ { holder = %to; tokens = value } ]
The added record in 'ledger', if any, is the
%to
record.
caller <> %from ->let some before_from_caller = before.allowance[(%from,caller)] inlet some after_from_caller = allowance[(%from,caller)] inbefore_from_caller.amount > value ->after_from_caller = { before_from_caller withamount = abs (before_from_caller.amount - value)}otherwise falseotherwise true
When
caller
is different from%from
, the amountcaller
is authorised to spend on the behalf of%from
is decreased byvalue
ifvalue
is striclty greated than the authorized amount.
caller = %from -> allowance = before.allowance
No effect on
allowance
whencaller
is equal to%from
.
forall a in allowance,a.addr_owner <> %from and a.addr_spender <> caller ->before.allowance[(a.addr_owner,a.addr_spender)] = some(a)
Allowed amounts other than those associated to
%from
andcaller
are identical.
removed.allowance.isempty() and added.allowance.isempty()
No allowance record is added or removed.
fails with (msg : string) :let some after_ledger_from = ledger[%from] inmsg = "NotEnoughBalance" andafter_ledger_from.tokens < valueotherwise true
When the entry fails with message "NotEnoughBalance",
value
is stricly greater than the number of tokens of%to
. Cannot spend more than you own.
fails with (msg : string * (nat * nat)) :let some after_allowance_from_caller = allowance[(%from,caller)] inmsg = ("NotEnoughAllowance", (value, after_allowance_from_caller.amount)) andcaller <> %from andafter_allowance_from_caller.amount < valueotherwise false
When the entry fails with message "NotEnoughAllowance",
caller
is different from%from
andvalue
is stricly greater than the allowed amount for%from
andcaller
. A spender cannot spend more than allowed.
length (operations) = 0
No operation generated.
Archetype implementation:
entry approve(spender : address, value : nat) {var k = (caller, spender);if allowance.contains(k) then (var previous = allowance[k].amount;dofailif(previous > 0 and value > 0, (("UnsafeAllowanceChange", previous))););allowance.addupdate( k, { amount = value });}
ledger = before.ledger
No effect on
ledger
.
let some after_allowance_caller_spender = allowance[(caller,spender)] inlet some before_allowance_caller_spender = before.allowance[(caller,spender)] inafter_allowance_caller_spender = { before_allowance_caller_spender withamount = value}otherwiseafter_allowance_caller_spender = {addr_owner = caller;addr_spender = spender;amount = value}otherwise false
Allowed amount of tokens spendable by
spender
on the behalf ofcaller
is set tovalue
.
forall a in allowance,(a.addr_owner, a.addr_spender) <> (caller, spender) ->before.allowance[(a.addr_owner, a.addr_spender)] = some(a)
Other allowed amounts than the allowed amount of tokens spendable by
spender
on the behalf ofcaller
, are unchanged.
let some allowance_caller_spender = before.allowance[(caller, spender)] inadded.allowance.isempty()otherwiseadded.allowance = [ { addr_owner = caller; addr_spender = spender; amount = value } ]
The added
allowance
record, if any, is thecaller
andspender
one.
removed.allowance.isempty()
No record is removed from
allowance
.
fails with (msg : (string * nat)) :let some allowance_caller_spender = allowance[(caller,spender)] inmsg = ("UnsafeAllowanceChange", allowance_caller_spender.amount) andvalue > 0 andallowance_caller_spender.amount > 0otherwise false
When the entry fails with message "UnsafeAllowanceChange",
value
is strictly greater than 0 and the allowed amount of tokens spendable byspender
on the behalf ofcaller
is not equal to zero.
Note that in that case, it may be set back to 0 by having spender
call the transfer
entry to transfer a number of tokens equal to the remaining allowed amount, from the approver address (ie caller
above) to the approver address (ie to itself).
Indeed, according to properties 1.3 and 2.1 of the transfer
entry, this has no effect on ledger
and sets allowance record to 0.
length (operations) = 0
No operation generated.
Archetype implementation:
getter getAllowance (owner : address, spender : address) : nat {return (allowance[(owner, spender)].amount)}
ledger = before.ledger
No effect on
ledger
.
allowance = before.allowance
No effect on
allowance
.
No explicit fail. The entry implicitely fails though if the provided callback is invalid.
length (operations) = 1
Creates one callback operation.
Archetype implementation:
getter getBalance (owner : address) : nat {return (ledger[owner].tokens)}
ledger = before.ledger
No effect on
ledger
.
allowance = before.allowance
No effect on
allowance
.
No explicit fail. The entry implicitely fails though if the provided callback is invalid.
length (operations) = 1
Creates one callback operation.
Archetype implementation:
getter getTotalSupply () : nat {return totalsupply}
ledger = before.ledger
No effect on
ledger
.
allowance = before.allowance
No effect on
allowance
.
No explicit fail. The entry implicitely fails though if the provided callback is invalid.
length (operations) = 1
Creates one callback operation.