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