coase.arl

archetype coase

asset card_pattern identified by card_pattern_id {
  card_pattern_id: int;
  coefficient: tez;
  quantity: int;
} shadow {
  sellcount: int = 0;
} with {
  cp1: card_pattern_id >= 0;
  cp2: quantity >= 0;
}

asset card identified by card_id {
  card_id: int;
  card_owner: address;
  card_pattern_card: pkey<card_pattern>;
} with {
  c1: card_id >= 0;
}

variable next_id : int = 0
with {
  n1: next_id >= 0;
  n2: forall c in card, next_id <> c.card_id;
}

entry transfer_single (card_to_transfer : pkey<card>, destination : address) {
  require {
    ts1: caller = card[card_to_transfer].card_owner;
  }
  effect {
    card.update(card_to_transfer, {card_owner = destination})
  }
}

entry sell_single (card_to_sell : pkey<card>) {
  specification {
    shadow effect {
      card_pattern.update(card[card_to_sell].card_pattern_card, {sellcount += 1})
    }
  }
  require {
    ss1: caller = card[card_to_sell].card_owner;
  }
  effect {
    var cpc = card[card_to_sell].card_pattern_card;
    card_pattern.update(cpc, {quantity -= 1});
    card.remove(card_to_sell);
    var price : tez = card_pattern[cpc].quantity * card_pattern[cpc].coefficient;
    var receiver = caller;
    transfer price to receiver
  }
}

entry buy_single (card_to_buy : pkey<card_pattern>) {
  specification {
    postcondition bs1 {
      card.count() = before.card.count() + 1
    }
    postcondition bs2 {
      let some cp = card_pattern[card_to_buy] in
      balance = before.balance + cp.quantity * cp.coefficient
      otherwise true
    }
    postcondition bs3 {
      card.select(card_owner = caller).count() >= 1
    }
  }
  accept transfer
  effect {
    var price : tez = (card_pattern[card_to_buy].quantity + 1) * card_pattern[card_to_buy].coefficient;
    dofailif (price > transferred, "NotEnoughTransferred");
    card_pattern.update(card_to_buy, {quantity += 1});
    card.add({card_id = next_id; card_owner = caller; card_pattern_card = card_to_buy});
    next_id += 1
  }
}

specification {
  g1: balance = card_pattern.sum(((quantity * (quantity + 1)) / 2 + sellcount) * coefficient)
}