-
Notifications
You must be signed in to change notification settings - Fork 6
/
theta.dl
106 lines (84 loc) · 3.48 KB
/
theta.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
// Adopted from: https://etherscan.io/token/0x3883f5e181fccaf8410fa61e12b59bad963fb645#code
// parameters
.decl *owner(p: address)
// views
.decl *totalSupply(n: uint)
.decl balanceOf(p: address, n: uint)[0]
.decl constructor(t:uint)
// New views
.decl allowance(p: address, s: address, n:uint)[0,1]
.decl precirculated(p:address, b:bool)[0]
.decl canTransfer(p:address,q:address)
.function canTransfer
.decl *unlockTime(t: uint)
canTransfer(p,q) :- now(t), unlockTime(ut), t >= ut.
canTransfer(p,q) :- precirculated(p,true), precirculated(q,true).
.decl recv_allowPrecirculation(p:address)
.decl recv_disallowPrecirculation(p:address)
precirculated(p,true) :- recv_allowPrecirculation(p), msgSender(s), owner(s).
precirculated(p,false) :- recv_disallowPrecirculation(p), msgSender(s), owner(s).
.public recv_allowPrecirculation
.public recv_disallowPrecirculation
// 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(_).
unlockTime(t) :- constructor(t).
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,
canTransfer(s,r).
.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,
canTransfer(o,r).
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.