-
Notifications
You must be signed in to change notification settings - Fork 7
/
Copy patherc777.dl
125 lines (101 loc) · 5.25 KB
/
erc777.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
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
// parameters
.decl *owner(p: address)
// views
.decl *totalSupply(n: uint)
.decl balanceOf(p: address, n: uint)[0]
.decl constructor()
// 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)
// 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)
// Rules
owner(s) :- constructor(), msgSender(s).
totalSupply(0) :- constructor().
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.
.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.
// ERC777 functionalities
.decl recv_approveOperator(o: address)
.decl recv_revokeDefaultOperator(o: address)
.decl operators(p:address , o:address, b: bool)[0,1]
.decl revokedDefaultOperator(p:address , o:address, b: bool)[0,1]
.decl defaultOperator(p:address, b:bool)[0]
.public recv_revokeDefaultOperator
.public recv_approveOperator
.public operators(2)
.public revokedDefaultOperator(2)
.public defaultOperator(1)
operators(p,o,true) :- recv_approveOperator(o), msgSender(p), defaultOperator(o, false), p!=o.
revokedDefaultOperator(o,p,false) :- recv_approveOperator(o), msgSender(p), defaultOperator(o,true), p!=o.
revokedDefaultOperator(p,o,true) :- recv_revokeDefaultOperator(o), msgSender(p), defaultOperator(o,true), p!=o.
operators(p,o,false) :- recv_revokeDefaultOperator(o), msgSender(p), defaultOperator(o,false), p!=o.
.decl recv_operatorSend(o:address,r:address,n:uint,data:uint,operatorData:uint)
.decl recv_operatorBurn(p:address,n:uint,data:uint,operatorData:uint)
.decl operatorSend(o:address,r:address,s:address,n:uint,data:uint,operatorData:uint)
.decl operatorBurn(p:address,s:address,n:uint,data:uint,operatorData:uint)
operatorSend(o,r,s,n,data,operatorData) :- recv_operatorSend(o,r,n,data,operatorData), msgSender(s), operators(o,s,true),
balanceOf(o,m), m >= n, r!=0, n>0.
operatorSend(o,r,o,n,data,operatorData) :- recv_operatorSend(o,r,n,data,operatorData), msgSender(o),
balanceOf(o,m), m >= n, r!=0, n>0.
operatorSend(o,r,s,n,data,operatorData) :- recv_operatorSend(o,r,n,data,operatorData), msgSender(s),
defaultOperator(s,true), revokedDefaultOperator(o,s,false),
balanceOf(o,m), m >= n, r!=0, n>0.
transfer(o,r,n) :- operatorSend(o,r,_,n,_,_).
operatorBurn(p,s,n,data,operatorData) :- recv_operatorBurn(p,n,data,operatorData), msgSender(s), operators(p,s,true),
balanceOf(p,m), m >= n, p!=0 , n>0.
operatorBurn(p,s,n,data,operatorData) :- recv_operatorBurn(p,n,data,operatorData), msgSender(p),
balanceOf(p,m), m >= n, p!=0, n>0.
operatorBurn(p,s,n,data,operatorData) :- recv_operatorBurn(p,n,data,operatorData), msgSender(s),
defaultOperator(s,true), revokedDefaultOperator(p,s,false),
balanceOf(p,m), m >= n, p!=0, n>0.
burn(p,n) :- operatorBurn(p,_,n,_,_).
// Properties
.decl inconsistentOperator(p:address, o:address)[0,1]
.violation inconsistentOperator
// inconsistentOperator(p,o) :- revokedDefaultOperator(p,o,true), defaultOperator(o,true), operators(p,o,true).
inconsistentOperator(p,o) :- defaultOperator(o,true), operators(p,o,true).