Auction (from Zilliqa)
Archetype version of zilliqa auction contract
Retranscription of zilliqa’s auction contract:
auction_zilliqa.arl
1
archetype auction_zilliqa
2
3
variable highest_bid : tez = 0tz
4
variable highest_bidder : address = @tz1Lc2qBKEWCBeDU8npG6zCeCqpmaegRi6Jg
5
6
variable beneficiary : address = @tz1bfVgcJC4ukaQSHUe1EbrUd5SekXeP9CWk
7
8
asset pending_return identified by incumbent {
9
incumbent : address;
10
val : tez;
11
}
12
13
states =
14
| Open initial
15
| Closed
16
17
variable auction_start : date = 2019-01-01T00:00:00
18
variable auction_end : date = 2019-02-01T00:00:00
19
20
specification {
21
contract invariant highest_is_not_pending {
22
not (pending_return.contains(highest_bidder))
23
}
24
contract invariant highest_is_highest {
25
forall pr in pending_return,
26
pr.val <= highest_bid and pr.incumbent <> highest_bidder
27
}
28
}
29
30
entry place_bid () {
31
32
require {
33
c1 : auction_start <= now <= auction_end;
34
}
35
36
effect {
37
if pending_return.contains(caller)
38
then (
39
var bid = pending_return[caller].val;
40
var new_bid = bid + transferred;
41
if new_bid > highest_bid
42
then (
43
(* update pending_return *)
44
pending_return.add ({ incumbent = highest_bidder;
45
val = highest_bid });
46
pending_return.remove(caller);
47
(* update highest *)
48
highest_bid := new_bid;
49
highest_bidder := caller)
50
else
51
pending_return.update (caller, { val = new_bid })
52
)
53
else
54
if caller = highest_bidder
55
then
56
(* caller is highest_bidder! accumulate *)
57
highest_bid += transferred
58
else if transferred > highest_bid
59
then (
60
(* update pending_return *)
61
pending_return.add ({incumbent = highest_bidder;
62
val = highest_bid });
63
(* update highest *)
64
highest_bid := transferred;
65
highest_bidder := caller)
66
else fail ("no update") (* no need to add bidder since there will
67
be nothing to withdraw *)
68
}
69
}
70
71
(* onlyonce extension specifies that one cannot withdraw more than once *)
72
entry withdraw () {
73
specification {
74
variable call_count : int = 0
75
shadow effect {
76
call_count += 1
77
}
78
postcondition o1 {
79
pending_return.contains(caller) -> call_count = 0
80
}
81
postcondition o2 {
82
call_count <= 1
83
}
84
}
85
require {
86
c2 : pending_return.contains(caller);
87
}
88
effect {
89
transfer pending_return[caller].val to caller;
90
pending_return.remove(caller)
91
}
92
}
93
94
transition endAuction () {
95
from Open
96
to Closed
97
when { now > auction_end }
98
with effect {
99
transfer highest_bid to beneficiary
100
}
101
}
102
Copied!
Last modified 1yr ago
Export as PDF
Copy link