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 = @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!

Basic

Next - Contract library

Finance

Last modified 1yr ago

Export as PDF

Copy link