Lazy

auction_lazy.arl
archetype auction_lazy
asset bid identified by incumbent = {
incumbent : address;
val : mtez;
}
variable deadline date = 2019-01-01T00:00:00
action place_bid = {
require {
c1 : now < deadline;
}
effect {
bid.add({ incumbent = caller; val = transferred })
}
}
(*Users need to exhibit proof they are not the winner to reclaim their bid*)
action reclaim (witness : address) = {
require {
c2 : now < deadline;
c3 : (let bc = bid.get(caller).val in
let bw = bid.get(witness).val in
bc < bw);
}
effect {
transfer bid.get(caller).val to caller
}
}
specification {
postcondition s1 = {
forall a in address,
bid.contains(a) -> balance > bid.get(a).val
}
}