-
Notifications
You must be signed in to change notification settings - Fork 6
/
wbtc.dl
129 lines (105 loc) · 4.37 KB
/
wbtc.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
126
127
128
129
// Adopted from: https://etherscan.io/token/0x2260fac5e5542a773aa44fbcfedf7c193bc2c599#code
// 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(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 decreaseAllowance(p: address, s: address, n:uint)
.decl recv_approve(s: address, n:uint)
.decl recv_increaseApproval(p:address, n:uint)
.decl recv_decreaseApproval(p:address, n:uint)
.public recv_increaseApproval
.public recv_decreaseApproval
// 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)
.decl *paused(b: bool)
.decl *pendingOwner(p: address)
// .decl *mintingFinished(b: bool)
.decl recv_pause()
.decl recv_unpause()
paused(true) :- recv_pause(), msgSender(s), owner(s), paused(false).
paused(false) :- recv_unpause(), msgSender(s), owner(s), paused(true).
.decl recv_transferOwnership(p:address)
.decl recv_claimOwnership()
.decl claimOwnership(p:address)
pendingOwner(p) :- recv_transferOwnership(p), msgSender(s), owner(s), p!=0.
claimOwnership(s) :- recv_claimOwnership(), msgSender(s), pendingOwner(s).
owner(s) :- claimOwnership(s).
pendingOwner(0) :- claimOwnership(_).
.decl recv_reclaimToken()
.decl reclaimToken(t:address, s:address,n: uint)
reclaimToken(t,s,n) :- recv_reclaimToken(), msgSender(s), owner(s),
this(t), balanceOf(t,n).
send(s,n) :- reclaimToken(_,s,n).
transfer(t,s,n) :- reclaimToken(t,s,n).
.public recv_pause
.public recv_unpause
.public recv_transferOwnership
.public recv_claimOwnership
.public recv_reclaimToken
// 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(n), msgSender(p), balanceOf(p,m), n<=m.
transfer(s,r,n) :- recv_transfer(r,n), msgSender(s), balanceOf(s,m), n<=m,
paused(false).
.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,
paused(false).
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.
increaseAllowance(o,s,n) :- recv_increaseApproval(s,n), msgSender(o).
decreaseAllowance(o,s,n) :- recv_decreaseApproval(s,n), msgSender(o), allowance(o,s,m), m>=n.
.decl allowanceTotal(o:address, s:address, m:uint)[0,1]
.decl decreaseAllowanceTotal(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).
decreaseAllowanceTotal(o,s,m) :- decreaseAllowance(o,s,_), m = sum n: decreaseAllowance(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), decreaseAllowanceTotal(o,s,d), n := m-l-d.
// 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.