Auction (from Zilliqa)

auction_zilliqa.arl
archetype auction_zilliqa
​
variable highest_bid mtez = 0mtz
variable highest_bidder address = 0
​
variable beneficiary address = @tz1KmuhR6P52hw6xs5P69BXJYAURaznhvN1k
​
asset pending_returns identified by incumbent = {
  incumbent   : address;
  val         : mtez;
}
​
states =
| Open initial
| Closed
​
variable auction_start date = 2019-01-01T00:00:00
variable auction_end   date = 2019-02-01T00:00:00
​
specification {
  postcondition highest_is_not_pending = {
    not (pending_return.contains(highest_bidder))
  }
  postcondition highest_is_highest = {
    forall pr in prending_return,
      pr.val <= highest_bid and pr.incumbent <> highest_bidder
  }
}
​
action place_bid = {
​
  require {
    c1 : auction_start <= now <= auction_end;
  }
​
  effect {
    if pending_return.contains(caller)
    then
      let bid = pending_return.get(caller).val in
      let new_bid = bid + transferred in
      if new_bid > highest_bid
      then (
        (* update pending_return *)
        pending_return.add ({ incumbent = highest_bidder;
                              val       = highest_bid });
        pending_return.remove(caller);
        (* update highest *)
        highest_bid    := new_bid;
        highest_bidder := caller)
      else
        pending_return.update (caller, { val = new_bid })
    else
      if caller = highest_bidder
      then
        (* caller is highest_bidder! accumulate *)
        highest_bid += transferred
      else if transferred > highest_bid
      then (
        (* update pending_return *)
        pending_return.add ({incumbent = highest_bidder;
                             val       = highest_bid });
        (* update highest *)
        highest_bid := transferred;
        highest_bidder := caller)
      else fail (* no need to add bidder since there will
                           be nothing to withdraw *)
  }
}
​
(* onlyonce extension specifies that one cannot withdraw more than once *)
action[%onlyonce%] withdraw = {
  require {
    c2 : pending_returns.contains(caller);
  }
  effect {
    transfer pending_returns.get(caller).val to caller;
    pending_return.remove(caller)
  }
}
​
transition endAuction from Open = {
  to Closed
  when { now > auction_end }
  with effect {
    transfer highest_bid to beneficiary
  }
}