FA 1.2

Search…
FA 1.2
Fungible token for Tezos
FA 1.2 is the fungible token specification for 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!
Contract library - Previous
Digital Assets
Formal properties
Last modified 11mo ago
Export as PDF
Copy link
Edit on GitHub