Basic
auction_basic.arl
1
archetype auction
2
3
variable max_bid : tez = 0tz
4
5
asset bid identified by incumbent {
6
incumbent : address;
7
value : tez;
8
}
9
10
variable deadline : date = 2019-01-01T00:00:00
11
12
13
entry place_bid () {
14
15
require {
16
c1 : now < deadline
17
}
18
19
effect {
20
bid.add({ incumbent = caller; value = transferred });
21
max_bid := max (transferred, max_bid)
22
}
23
}
24
25
26
(* Users need to exhibit proof they are not the winner to reclaim their bid *)
27
entry reclaim () {
28
29
require {
30
c2 : now < deadline;
31
c3 : bid[caller].value < max_bid;
32
}
33
34
effect {
35
transfer bid[caller].value to caller
36
}
37
}
38
39
specification {
40
contract invariant s1 {
41
forall b in bid, balance > b.value
42
}
43
}
44
Copied!
Last modified 1yr ago
Export as PDF
Copy link