lazy-auction.md

Lazy

{% code title="auction_lazy.arl" %}

archetype auction_lazy

asset bid identified by incumbent {
  incumbent : address;
  val : tez;
}

variable deadline : date = 2019-01-01T00:00:00

entry 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*)
entry reclaim (witness : address) {
  require {
    c2 : now < deadline;
    c3 : (let bc = bid[caller].val in
          let bw = bid[witness].val in
          bc < bw);
  }
  effect {
    transfer bid[caller].val to caller
  }
}

specification {
  contract invariant s1 {
    forall b in bid, balance > b.val
  }
}

{% endcode %}