cappedCrowdSale.dl

// 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.

///////////////////////////////////////////////////////////
.decl recv_finalize()
.public recv_finalize
.decl finalize()
.decl *finalized(b:bool)

.decl *start(time: uint)
.decl *end(time: uint)

.decl *rate(r: uint)
.decl recv_buyToken(p:address, amount: uint)
.decl buyToken(p:address, amount: uint)
.public recv_buyToken

buyToken(p,n) :- recv_buyToken(p,m), finalized(false), p!=0, m!=0, now(t), start(s), end(e), t>s, t<e, rate(r), n:=m*r.
mint(p,n) :- buyToken(p,n).

.decl *raised(n: uint)
raised(s) :- s = sum n: buyToken(_,n).
.decl *cap(n: uint)

finalize() :- recv_finalize(), msgSender(s), owner(s), finalized(false), now(t), end(e), t>e.
finalize() :- recv_finalize(), msgSender(s), owner(s), finalized(false), raised(m), cap(c), m>=c.
finalized(true) :- finalize().


//property
.decl *onceFinalize(b:bool)
onceFinalize(false) :- constructor().
onceFinalize(true) :- finalize().

.decl illegalFinalization()
.violation illegalFinalization
illegalFinalization() :- onceFinalize(true), now(t), end(e), t<e, raised(r), cap(c), r<c.

.decl buyAfterFinalize()
.violation buyAfterFinalize
buyAfterFinalize() :- onceFinalize(true), transaction(recv_buyToken).