-
Notifications
You must be signed in to change notification settings - Fork 7
/
Copy pathcontrollable.dl
107 lines (86 loc) · 3.59 KB
/
controllable.dl
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
// The controllable token contract following ERC 1644 standard.
// parameters
.decl *owner(p: address)
.decl *controller(p: address)
// views
.decl *totalSupply(n: uint)
.decl balanceOf(p: address, n: uint)[0]
.decl constructor(p: address)
// New views
.decl allowance(p: address, s: address, n:uint)[0,1]
// Transactions
.decl mint(p: address, amount: uint)
.decl recv_mint(p: address, amount: uint)
.decl burn(p: address, amount: uint)
.decl recv_burn(p: address, amount: uint)
.decl transfer(from: address, to: address, amount: uint)
.decl recv_transfer(to: address, amount: uint)
// ERC 1644 interfaces
.decl recv_controllerTransfer(from: address, to: address, amount: uint)
.decl controllerTransfer(from: address, to: address, amount: uint)
.decl recv_controllerRedeem(p: address, amount: uint)
.decl controllerRedeem(p: address, amount: uint)
// New transactions
.decl recv_transferFrom(from: address, to: address, amount: uint)
.decl increaseAllowance(p: address, s: address, n:uint)
.decl recv_approve(s: address, n:uint)
// Interfaces
.public recv_mint
.public recv_burn
.public recv_transfer
.public balanceOf(1)
.public totalSupply(0)
// New interfaces
.public recv_approve
.public recv_transferFrom
.public allowance(2)
.public recv_controllerRedeem
// Rules
owner(s) :- constructor(_), msgSender(s).
totalSupply(0) :- constructor(_).
controller(p) :- constructor(p).
mint(p,n) :- recv_mint(p,n), msgSender(s), owner(s), p!=0.
burn(p,n) :- recv_burn(p,n), msgSender(s), owner(s), p!=0 ,balanceOf(p,m), n<=m.
transfer(s,r,n) :- recv_transfer(r,n), msgSender(s), balanceOf(s,m), n<=m.
// Controller transactions
controllerTransfer(s,r,n) :- recv_controllerTransfer(s,r,n),
msgSender(c), controller(c),
balanceOf(s,m), n<=m.
transfer(s,r,n) :- controllerTransfer(s,r,n).
controllerRedeem(p,n) :- recv_controllerRedeem(p,n),
msgSender(c), controller(c),
p!=0 ,balanceOf(p,m), n<=m.
burn(p,n) :- controllerRedeem(p,n).
.decl totalMint(p: address, n: uint)[0]
.decl totalBurn(p: address, n: uint)[0]
.decl totalOut(p: address, n: uint)[0]
.decl totalIn(p: address, n: uint)[0]
totalOut(p,s) :- transfer(p,_,_), s = sum n: transfer(p,_,n).
totalIn(p,s) :- transfer(_,p,_), s = sum n: transfer(_,p,n).
totalMint(p,s) :- mint(p,_), s = sum n: mint(p,n).
totalBurn(p,s) :- burn(p,_), s = sum n: burn(p,n).
balanceOf(p,s) :- totalMint(p,n), totalBurn(p,m), totalOut(p,o), totalIn(p,i), s:=n+i-m-o.
.decl *allMint(n: uint)
.decl *allBurn(n: uint)
allMint(s) :- s = sum n: mint(_,n).
allBurn(s) :- s = sum n: burn(_,n).
totalSupply(n) :- allMint(m), allBurn(b), n := m - b.
// New rules
.decl transferFrom(from: address, to: address, spender: address, amount: uint)
transferFrom(o,r,s,n) :- recv_transferFrom(o,r,n),
balanceOf(o,m), m>=n,
msgSender(s), allowance(o,s,k), k>=n.
transfer(o,r,n) :- transferFrom(o,r,_,n).
increaseAllowance(o,s,d) :- recv_approve(s,n), msgSender(o), allowance(o,s,m), d:=n-m.
.decl allowanceTotal(o:address, s:address, m:uint)[0,1]
.decl spentTotal(o:address, s:address, m:uint)[0,1]
allowanceTotal(o,s,m) :- increaseAllowance(o,s,_), m = sum n: increaseAllowance(o,s,n).
spentTotal(o,s,m) :- transferFrom(o,_,s,_), m = sum n: transferFrom(o,_,s,n).
allowance(o,s,n) :- allowanceTotal(o,s,m), spentTotal(o,s,l), n := m-l.
// Properties
.decl *totalBalances(m: uint)
.decl *unequalBalance(s: uint, n: uint)
.violation unequalBalance
totalBalances(0) :- constructor(_).
totalBalances(s) :- s = sum n: balanceOf(_,n).
unequalBalance(s,n) :- totalBalances(s), totalSupply(n), s!=n.