-
Notifications
You must be signed in to change notification settings - Fork 20
/
EnglishAuction_strict.spec
64 lines (52 loc) · 2.19 KB
/
EnglishAuction_strict.spec
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
/**
* # English auction spec - proving strict inequality
*/
methods
{
// Declaring getters as `envfree`
function highestBidder() external returns (address) envfree;
function highestBid() external returns (uint) envfree;
function bids(address) external returns (uint) envfree;
}
/** @title A ghost and hook identifying if any bid was placed
* There is no other way to detect if a bid was placed *unless we assume that
* `address(0)` cannot place a bid).
*/
ghost bool _hasAnyoneBid {
init_state axiom !_hasAnyoneBid;
}
hook Sstore bids[KEY address bidder] uint newAmount (uint oldAmount) {
_hasAnyoneBid = _hasAnyoneBid || (newAmount > 0);
}
/// @title `highestBid` is the maximal bid
invariant integrityOfHighestBid(address bidder)
bids(bidder) <= highestBid();
/// @title No bids implies all bids are zero and highest bidder is address zero
invariant noBidsIntegrity(address bidder)
!_hasAnyoneBid => (bids(bidder) == 0 && highestBidder() == 0);
/// @title There can be no tie in highest bid (if there is at least one bid)
invariant highestBidStrictlyHighest(address bidder)
(_hasAnyoneBid && bidder != highestBidder()) => (highestBid() > bids(bidder)) {
preserved {
requireInvariant integrityOfHighestBid(bidder);
}
preserved withdrawFor(address bidder2, uint amount) with (env e1) {
requireInvariant noBidsIntegrity(bidder2);
}
preserved withdrawAmount(address recipient, uint amount) with (env e2) {
requireInvariant noBidsIntegrity(e2.msg.sender);
}
}
// -----------------------------------------------------------------------------
// Here is the invariant "highest bidder has the highest bid" without assuming that
// `address(0)` cannot place a bid.
/// @title Highest bidder has the highest bid
invariant highestBidderHasHighestBid()
_hasAnyoneBid => (bids(highestBidder()) == highestBid()) {
preserved withdrawFor(address bidder, uint amount) with (env e1) {
requireInvariant noBidsIntegrity(bidder);
}
preserved withdrawAmount(address recipient, uint amount) with (env e2) {
requireInvariant noBidsIntegrity(e2.msg.sender);
}
}