Auction (from Zilliqa)

auction_zilliqa.arl
archetype auction_zilliqa
​
variable highest_bid : tez = 0tz
variable highest_bidder : address = @0
​
variable beneficiary : address = @tz1KmuhR6P52hw6xs5P69BXJYAURaznhvN1k
​
asset pending_return identified by incumbent {
  incumbent   : address;
  val         : tez;
}
​
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 pending_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 update") (* 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_return.contains(caller);
  }
  effect {
    transfer pending_return.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
  }
}
​