Auction (from Zilliqa)

Retranscription of zilliqa’s auction contract:
​https://github.com/Zilliqa/scilla/blob/master/tests/contracts/auction.scilla​
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!

Basic

Next - Contract library

Finance

Last modified 1mo ago

Export as PDF

Copy link

Edit on GitHub