FA 1.2
Fungible token for Tezos
FA 1.2 is the fungible token specification for Tezos :
Getting started with FA1.2 · Digital Assets on Tezos
Below is the archetype implementation:
1
archetype fa12
2
3
constant totalsupply : nat = 10_000_000
4
5
asset allowance identified by addr_owner addr_spender to big_map {
6
addr_owner : address;
7
addr_spender : address;
8
amount : nat;
9
}
10
11
asset ledger identified by holder to big_map {
12
holder : address;
13
tokens : nat = 0;
14
} initialized by {
15
{ holder = caller; tokens = totalsupply }
16
}
17
18
entry %transfer (%from : address, %to : address, value : nat) {
19
require {
20
r1 otherwise "NotEnoughBalance" : ledger[%from].tokens >= value;
21
}
22
effect {
23
if caller <> %from then (
24
var current = allowance[(%from, caller)].amount;
25
dofailif(current < value, ("NotEnoughAllowance", ((value, current))));
26
allowance.update((%from, caller), { amount -= value });
27
);
28
ledger.update(%from, { tokens -= value });
29
ledger.addupdate(%to, { tokens += value });
30
}
31
}
32
33
entry approve(spender : address, value : nat) {
34
var k = (caller, spender);
35
if allowance.contains(k) then (
36
var previous = allowance[k].amount;
37
dofailif(previous > 0 and value > 0, (("UnsafeAllowanceChange", previous)));
38
);
39
allowance.addupdate( k, { amount = value });
40
}
41
42
getter getAllowance (owner : address, spender : address) : nat {
43
return (allowance[(owner, spender)].amount)
44
}
45
46
getter getBalance (owner : address) : nat {
47
return (if (ledger.contains(owner)) then ledger[owner].tokens else 0)
48
}
49
50
getter getTotalSupply () : nat {
51
return totalsupply
52
}
53
54
///////////////////////////////////////////////////////////////////////////////
55
// SPECIFICATION
56
///////////////////////////////////////////////////////////////////////////////
57
58
specification {
59
s1: ledger.sum(tokens) = totalsupply;
60
}
61
62
specification entry %transfer (%from : address, %to : address, value : nat) {
63
fails {
64
f0 with (msg : string) :
65
let some after_ledger_from = ledger[%from] in
66
msg = "NotEnoughBalance" and
67
after_ledger_from.tokens < value
68
otherwise true;
69
f1 with (msg : string * (nat * nat)) :
70
let some after_allowance_from_caller = allowance[(%from,caller)] in
71
msg = ("NotEnoughAllowance", ((value, after_allowance_from_caller.amount))) and
72
caller <> %from and
73
after_allowance_from_caller.amount < value
74
otherwise false;
75
}
76
// LEDGER ASSET
77
postcondition transfer_p1 { // effect on %from nbtokens
78
%from <> %to ->
79
let some before_ledger_from = before.ledger[%from] in
80
let some after_ledger_from = ledger[%from] in
81
after_ledger_from = { before_ledger_from with
82
tokens = abs (before_ledger_from.tokens - value)
83
}
84
otherwise false otherwise false
85
}
86
postcondition transfer_p2 { // effect on %to nbtokens
87
%from <> %to ->
88
let some after_ledger_to = ledger[%to] in
89
let some before_ledger_to = before.ledger[%to] in
90
after_ledger_to = { before_ledger_to with
91
tokens = (before_ledger_to.tokens + value)
92
}
93
otherwise
94
after_ledger_to = { holder = %to; tokens = value }
95
otherwise false // %to ledger asset exists after transfer
96
}
97
postcondition transfer_p3 {
98
%from = %to -> ledger = before.ledger
99
}
100
postcondition transfer_p4 { // other ledger assets are unchanged
101
forall tokenholder in ledger,
102
tokenholder.holder <> %from ->
103
tokenholder.holder <> %to ->
104
before.ledger[tokenholder.holder] = some(tokenholder)
105
}
106
postcondition transfer_p5 { // no ledger asset is removed
107
removed.ledger.isempty()
108
}
109
postcondition transfer_p6 { // number of added asset may be one
110
let some before_to = before.ledger[%to] in
111
added.ledger.isempty()
112
otherwise
113
added.ledger = [ { holder = %to; tokens = value } ]
114
}
115
// ALLOWANCE ASSET
116
postcondition transfer_p7 { // effect on allowance
117
caller <> %from ->
118
let some before_from_caller = before.allowance[(%from,caller)] in
119
let some after_from_caller = allowance[(%from,caller)] in
120
before_from_caller.amount > value ->
121
after_from_caller = { before_from_caller with
122
amount = abs (before_from_caller.amount - value)
123
}
124
otherwise false
125
otherwise true
126
}
127
postcondition transfer_p8 { // effect on allowance
128
caller = %from -> allowance = before.allowance
129
}
130
postcondition transfer_p9 { // other allowance assets are unchanged
131
forall a in allowance,
132
a.addr_owner <> %from and a.addr_spender <> caller ->
133
before.allowance[(a.addr_owner, a.addr_spender)] = some(a)
134
}
135
postcondition transfer_p10 { // no allowance is added or removed
136
removed.allowance.isempty() and added.allowance.isempty()
137
}
138
139
postcondition transfer_p11 { // no operation generated
140
length (operations) = 0
141
}
142
}
143
144
specification entry approve(spender : address, value : nat) {
145
fails {
146
f2 with (msg : (string * nat)) :
147
let some allowance_caller_spender = allowance[(caller, spender)] in
148
msg = ("UnsafeAllowanceChange", allowance_caller_spender.amount) and
149
value > 0 and
150
allowance_caller_spender.amount > 0
151
otherwise false;
152
}
153
postcondition approve_p1 { // effect on allowance asset
154
let some after_allowance_caller_spender = allowance[(caller,spender)] in
155
let some before_allowance_caller_spender = before.allowance[(caller,spender)] in
156
after_allowance_caller_spender = { before_allowance_caller_spender with
157
amount = value
158
}
159
otherwise
160
after_allowance_caller_spender = { addr_owner = caller; addr_spender = spender; amount = value }
161
otherwise false
162
}
163
164
postcondition approve_p2 { // other allowance assets are unchanged
165
forall a in allowance,
166
(a.addr_owner, a.addr_spender) <> (caller, spender) ->
167
before.allowance[(a.addr_owner, a.addr_spender)] = some(a)
168
}
169
170
postcondition approve_p3 { // added allowance
171
let some allowance_caller_spender = before.allowance[(caller, spender)] in
172
added.allowance.isempty()
173
otherwise
174
added.allowance = [ { addr_owner = caller; addr_spender = spender; amount = value } ]
175
}
176
177
postcondition approve_p4 { // no allowance asset is removed
178
removed.allowance.isempty()
179
}
180
181
postcondition approve_p5 {
182
ledger = before.ledger
183
}
184
185
postcondition approve_p6 { // no operation generated
186
length (operations) = 0
187
}
188
}
189
190
specification getter getAllowance (owner : address, spender : address) {
191
postcondition getallowance_p1 { // creates one op
192
length (operations) = 1
193
}
194
postcondition getallowance_p2 { // assets are unchanged
195
ledger = before.ledger and allowance = before.allowance
196
}
197
}
198
199
specification getter getBalance (owner : address) {
200
postcondition getbalance_p1 { // creates one op
201
length (operations) = 1
202
}
203
postcondition getbalance_p2 { // assets are unchanged
204
ledger = before.ledger and allowance = before.allowance
205
}
206
}
207
208
specification getter getTotalSupply () {
209
postcondition gettotalsupply_p1 { // creates one op
210
length (operations) = 1
211
}
212
postcondition gettotalsupply_p2 { // assets are unchanged
213
ledger = before.ledger and allowance = before.allowance
214
}
215
}
216
217
Copied!
Last modified 7mo ago
Export as PDF
Copy link