Auction (from Zilliqa)

auction_zilliqa.arl
archetype auction_zilliqa
​
variable highest_bid : tez = 0tz
variable highest_bidder : address = @tz1Lc2qBKEWCBeDU8npG6zCeCqpmaegRi6Jg
​
variable beneficiary : address = @tz1bfVgcJC4ukaQSHUe1EbrUd5SekXeP9CWk
​
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 {
  contract invariant highest_is_not_pending {
    not (pending_return.contains(highest_bidder))
  }
  contract invariant highest_is_highest {
    forall pr in pending_return,
      pr.val <= highest_bid and pr.incumbent <> highest_bidder
  }
}
​
entry place_bid () {
​
  require {
    c1 : auction_start <= now <= auction_end;
  }
​
  effect {
    if pending_return.contains(caller)
    then (
      var bid = pending_return[caller].val;
      var new_bid = bid + transferred;
      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 *)
entry withdraw () {
  specification {
    variable call_count : int = 0
    shadow effect {
      call_count += 1
    }
    postcondition o1 {
      pending_return.contains(caller) -> call_count = 0
    }
    postcondition o2 {
      call_count <= 1
    }
  }
  require {
    c2 : pending_return.contains(caller);
  }
  effect {
    transfer pending_return[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
  }
}
​