Coase

The Coase smart contract enables the trading (buy and sell) of digital collectible card games:

The smart contract version we are considering here is the one that comes as a Ligo example:

The smart contract version we are considering here is the one that comes as a Ligo example (Copyright Coase, Inc 2019):

The Archetype version:

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 of 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 of 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 of 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 of 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;
failif (price > transferred);
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)
}

The Archetype contract defines two assets: card_pattern which holds the number of cards in stock and card which hods its owner and its pattern.

We note that the concept of asset collection makes the code very straightforward compared to lower-level code: for example, the transfer_single entry point sets the card_owner field of the card with id card_to_transfer.

Below the LIGO version:

const cards : cards = s.cards ;
const card : card = get_force(action.card_to_transfer , cards) ;
if (card.card_owner =/= source)
then failwith ("This card doesn't belong to you")
else skip ;
card.card_owner := action.destination ;
cards[action.card_to_transfer] := card ;
s.cards := cards ;

Below the Archetype version:

require {
ts1: caller = card.get(card_to_transfer).card_owner;
}
effect {
card.update(card_to_transfer, {card_owner = destination})
}

We note that, in Archetype, it is possible for example to provide the formula of the balance of the contract:

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

which writes mathematically as:

where sellcount is the number of times a card has been sold. Note that sellcount is not computed in the original contract. It is defined in Archetype as a shadow field (see “Asset shadow field” section below).

This property makes the contract’s business model explicit: each time a card is sold, the contract earns the value of the card’s coefficient; when every card has been sold (∀c,quantity(c)=0), the following relation stands:

We see that a high-level non-trivial property is a very powerful way to convey information about the contract.

Edit on GitHub