Miles
This archetype is a very basic miles management system with add and consume transactions. It may be considered as a simplified version of ERC20.
miles.arl
1
archetype miles
2
3
variable validator : role = @tz1Lc2qBKEWCBeDU8npG6zCeCqpmaegRi6Jg
4
5
asset account identified by owner {
6
owner : role;
7
amount : int;
8
}
9
10
entry add (ow : role, value : int) {
11
called by validator
12
effect {
13
if account.contains(ow) then
14
account.update (ow, { amount += value })
15
else
16
account.add({ owner = ow; amount = 0 })
17
}
18
}
19
20
entry consume (ow : role, value : int) {
21
specification {
22
postcondition s1 {
23
let some ba = before.account[ow] in
24
let some a = account[ow] in
25
ba.amount = a.amount + value
26
otherwise true
27
otherwise true
28
}
29
}
30
31
called by validator
32
33
require {
34
c1 : account[ow].amount >= value;
35
}
36
37
effect {
38
account.update (ow, { amount -= value })
39
}
40
}
41
Copied!
Last modified 1yr ago
Export as PDF
Copy link