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 = @0
5
6
variable beneficiary : address = @tz1KmuhR6P52hw6xs5P69BXJYAURaznhvN1k
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
postcondition highest_is_not_pending {
22
not (pending_return.contains(highest_bidder))
23
}
24
postcondition highest_is_highest {
25
forall pr in pending_return,
26
pr.val <= highest_bid and pr.incumbent <> highest_bidder
27
}
28
}
29
30
action 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
let bid = pending_return.get(caller).val in
40
let new_bid = bid + transferred in
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
else
53
if caller = highest_bidder
54
then
55
(* caller is highest_bidder! accumulate *)
56
highest_bid += transferred
57
else if transferred > highest_bid
58
then (
59
(* update pending_return *)
60
pending_return.add ({incumbent = highest_bidder;
61
val = highest_bid });
62
(* update highest *)
63
highest_bid := transferred;
64
highest_bidder := caller)
65
else fail ("no update") (* no need to add bidder since there will
66
be nothing to withdraw *)
67
}
68
}
69
70
(* onlyonce extension specifies that one cannot withdraw more than once *)
71
action[%onlyonce%] withdraw () {
72
require {
73
c2 : pending_return.contains(caller);
74
}
75
effect {
76
transfer pending_return.get(caller).val to caller;
77
pending_return.remove(caller)
78
}
79
}
80
81
transition endAuction () {
82
from Open
83
to Closed
84
when { now > auction_end }
85
with effect {
86
transfer highest_bid to beneficiary
87
}
88
}
Copied!
Last modified 1mo ago
Export as PDF
Copy link
Edit on GitHub