Auction (from Zilliqa)

Archetype version of zilliqa auction contract

Retranscription of zilliqa’s auction contract:

https://github.com/Zilliqa/scilla/blob/master/tests/contracts/auction.scilla

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
}
}
Edit on GitHub