Your first CSL contract

In this section we will guide you through the formulation of your first contract specification. Our goal is to describe a scenario in which the participant “Bob” sells one bicycle to “Alice” for 100 euros.

Specifying events

The first step in specifying our contract is to understand exactly what the scenario we want to describe actually contains:

• Is the bicycle delivered to Alice or must she pick it up?
• If it is delivered, is there a time limit for how long Alice wants to wait?
• If a third party, “Eve”, comes along and offers 200 USD for the bicycle, will she get it instead of Alice?
• Is there one single bicycle, or will Bob be able to sell more bicycles?
• When does payment occur?

One could come up with many more considerations than the above for a real-world scenario. For didactic purposes we shall limit ourselves to a simplified bike shop:

• Alice orders – and pays for – a bicycle, and then it is delivered to her with no time constraints;
• No other parties than Alice and Bob exist;
• Bob has one bicycle and when he sells it he closes down his shop.

Our idealized transaction thus boils down to the following:

1. Alice orders a bicycle by transferring 100 euros to Bob;
2. Bob delivers one bicycle to Alice.

Encoding events

In the preceding section we have established that our contract considers two separate types of events: a BikeOrder event and a BikeDelivery event. The BikeOrder event encodes the order that Alice places for a bicycle, and it should therefore include the price she is willing to pay and whom she orders a bike from. We specify this in CSL as follows:

type BikeOrder : Event {
  amount : Int, // The amount of euros that Alice will pay for a bicycle.
  recipient : Agent // The recipient of the order.
}

This CSL code specifies that a BikeOrder is a type of event which has the two fields amount and recipient in addition to the standard fields of events (which we shall see in a bit). Note that everything on a line that comes after // is treated as a comment and is ignored by CSL. CSL is not whitespace-sensitive, so we are free to layout the code as we please.

The BikeDelivery event represents the delivery of an item to a receiver. Hence, we include as extra fields in this event the recipient of the bicycle:

type BikeDelivery : Event {
  recipient : Agent // The recipient of the bicycle
}

Both BikeOrder and BikeDelivery are specified as a subtype of an event type called Event in CSL. This means that our newly defined types are events that we can use in contracts. Any event type we want to use in contracts has to be declared as a subtype of Event like this. In CSL we refer to this relationship as inheritance: our BikeOrder/BikeDelivery event inherits the properties of Event. An event is a subtype of another event if there is a so-called “is-a relationship” between them: A BikeOrder is an Event and a BikeDelivery is an Event.

Being an Event means that it has two fields agent and timestamp next to whatever else you specify. The Event type is defined as follows:

type Event {
  agent : Agent,
  timestamp : DateTime
}

Notice that Event does not inherit from any other events. Event is the root of the event hierarchy.

Specifying the desired behaviour

To specify the basic structure of our sales contract, we define a contract template named BikeSale with the template keyword. For now, we just encode the order in which the events must occur: One BikeOrder event followed by one BikeDelivery event.

template BikeSale0() =
  <*> BikeOrder // Someone sends a BikeOrder
  then
  <*> BikeDelivery // Someone sends a BikeDelivery
  // The contract is done

The syntax used here needs a bit of elaboration. A prefix contract is a contract that requires some given event to occur. Prefixes are written using the syntax <*> Event. The initial <*> means that the event may come from anyone, and the following Event is the actual type of the expected event. Combining a prefix contract with another contract with then results in a contract that requires the specified event to occur, followed by whatever the other contract requires.

Clearly, this contract is too generic. The only thing we have specified so far is the order of events and the fact that the contract is finished once the order and delivery has taken place. It therefore allows many sequences of events that should not be accepted: it is for instance quite possible for Bob to send a BikeOrder event and for Alice (or even Bob himself) to send the BikeDelivery event. To address this, we write the agents next to the events. In principle, we want the BikeOrder to come from Alice, and BikeDelivery to come from Bob – but this can be naturally generalised to any buyer and seller, respectively. In fact, in CSL we do not hardcode names of agents in contract templates. Instead, we make the buyer and the seller abstract in the contract, which is quite easily done by adding two parameters, buyer and seller to the contract template:

template BikeSale1(buyer, seller) =
  <buyer> BikeOrder // Buyer places a bike order
  then
  <seller> BikeDelivery // Seller delivers a bicycle
  // The contract is done

These parameters are bound to concrete values once the contract template is instantiated.

We have now used a different format for the prefix construct. If one writes <buyer> instead of <*> it means that the event must originate from an agent given by the template argument buyer. Hence, our contract now specifies that it is the buyer that must issue the BikeOrder event which must be followed by a BikeDelivery event from the seller. This is still too general: Our informal contract specification states that Alice places an order to Bob worth 100 euros and that Bob delivers a bicycle to Alice. Since we declared the BikeOrder and BikeDelivery events to include information about price, receiver, etc., we may use these properties to place restrictions on allowed events in our contract:

template BikeSale2(buyer, seller) =
  // Buyer sends an order worth 100 euros to seller
  <buyer> order: BikeOrder where
      order.amount = 100 &&
      order.recipient = seller
  then
  // Seller delivers a bicycle to buyer
  <seller> delivery: BikeDelivery where
      delivery.recipient = buyer

The prefix format is extended here to associate a name for a particular received event, making it possible to formulate a predicate on it. This predicate follows the keyword where, and the event is only accepted if it evaluates to True. The BikeOrder event is bound to a variable named order, and we use the where clause to check that the fields of order have the desired values, using the connective && which is the logical “and” operator. In this case, the event order is accepted only if the field order.price is set to 100 and the field order.recipient is set to seller. Likewise, the BikeDelivery event is bound to the variable delivery and is only accepted if delivery.recipient is buyer.

Generalizing the contract

Our contract template can now be instantiated to a specification of what we described at the beginning of this section: The sale of a bicycle for 100 euros from Bob to Alice – by setting the buyer parameter to alice and the seller parameter to bob. The contract is still quite limited, though, as it only models this particular idealized sale of one single bicycle for a fixed price. In this section we will demonstrate how to generalize the contract to handle a wider range of scenarios.

We currently have a contract template that specifies the sale of one bicycle from some seller to some buyer. Now, what if it was not a bicycle but a hammer that was the transaction’s object? Clearly, there is no substantial difference between a sales transaction that involves one object or the other, safe for the price. However, our way of modeling a transaction with BikeOrder and BikeDelivery events fixates the objects to be a bicycle. We must therefore extend our events a bit to be able to account for orders and deliveries of other items:

type Order : Event {
  amount : Int, // The amount of euros is offered for the item.
  recipient : Agent, // The recipient of the order.
  item : String // The item that is ordered
}
type Delivery : Event {
  recipient : Agent, // The recipient of the item
  item : String // The item that is delivered
}

Now we can formulate a more general sales contract template (call it Sale), by abstracting the item and the price out as parameters of the contract template:

template Sale0(buyer, seller, amount, item) =
  // Some buyer orders an item for some price from a seller
  <buyer> order: Order where
      order.amount = amount &&
      order.recipient = seller &&
      order.item = item
  then
  // The seller delivers that item
  <seller> delivery: Delivery where
      delivery.item = item &&
      delivery.recipient = buyer

Exercise: Pay on delivery

Write a variant of the Sale0 contract where the payment comes after the delivery (solution).

There is glaring problem with our new contract specification: Nowhere is it specified that certain items have certain prices! According to the contract in its current formulation, a buyer just has to offer any amount of euros for any item, including even a negative amount or zero, and she will receive it! This is not a desirable state of affairs: we must model some basic notion of an inventory that associates prices to items.

// Accept offer if the item and offered price fit.
val acceptOffer =
  \ "Bike" -> (\p -> p >= 100)
  | "Hammer" -> (\p -> p >= 30)
  | "Saw" -> (\p -> p >= 40)
  | _ -> \p -> False // Seller does not have this item; reject.

template Sale1(buyer, seller, amount, item) =
  // Some buyer orders an item for some price from a seller
  <buyer> order: Order where
      order.amount = amount &&
      order.recipient = seller &&
      order.item = item
  then
  // The seller delivers that item
  <seller> delivery: Delivery where
      acceptOffer order.item order.amount &&
      delivery.item = order.item &&
      delivery.recipient = buyer

This version of the contract template introduces a new concept of CSL: functions. The basic idea with this addition to our contract is to specify an “inventory function” acceptOffer that takes an item and a price and returns either True or False depending on whether the offered price for the item is acceptable. The notation used here deserves some elaboration: A function has the form \arg -> body where arg is a name that can be used inside of body as the value that was given when the function was called. In CSL, functions always take one single argument. How do we handle the case where we need more than one argument to a function then, like adding two numbers? We use a technique called currying, where we write our function such that it return another function that takes the remaining argument: \arg1 -> \arg2 -> body. Functions may have separate bodies for separate kinds of input. This is written in CSL as \form1 -> body1 | form2 -> body2. We call this pattern matching, and this is what we have used in the acceptOffer above where each body is a new function that takes the price p and checks that is above some threshold. In fact, the simple form \p -> body also uses pattern matching: the name p is a pattern that matches any value and binds it to the name p inside of body where it can then be used. Note that when pattern matching, the symbol _ is a special pattern that behaves like a name but does not result in a new binding in the function’s body, so \_ -> body is like above except that body cannot refer to the value that the function was called with. Functions are an important part of the CSL language, and they are discussed in much more detail in the detailed description in the value language reference.

Our new version of the contract allows three items to be sold at three different minimum prices (the buyer is free to offer more), and it protects the seller from accidentally selling items at an unacceptable discount. However, the contract is once again restricted to a certain set of items! What we really should do here is to abstract away the shop’s inventory.

First, how will an arbitrary shop’s inventory be represented? We can either create a separate checking function for every shop, or use some data structure to represent any shop’s inventory, and provide a function which, given an inventory, a name of an item, and the price that the buyer is offering, either accepts or rejects the offer. Here we show the latter of the two approaches.

What data structure should we use to represent the shop’s inventory? It can simply be a dictionary: a list of tuples containing the name of the item and a minimal acceptable price. For example, the bike shop’s inventory can be represented as:

val bikeShopInventory =
  [("Bike", 100),
   ("Brakes", 20),
   ("Helmet", 30)]

Next, we need to write a function which decides if an offer can be accepted. It should search the inventory for the given item and check that the price is acceptable. This is one possibility of an implementation:

val checkOffer = \inventory -> \(item  : String) -> \(price : Int) ->
  // If the item is listed in the inventory and the price is right,
  // then accept the offer
  // 'List::any' returns True if there is an element of the list
  // that satisfies the predicate
  List::any
    (\(name, acceptPrice) -> name = item  && price >= acceptPrice)
    inventory

We use a standard library function List::any, which traverses a list, looking for an element which satisfies the given predicate. It returns True if it finds one and False otherwise. In our case, the list in question is the inventory, and the predicate states that the item is in the inventory, and the proposed price is accepted. Notice that we need to explicitly say that the item argument is of String type and that price is an Int. This is because not all types in CSL are comparable using = or <= operators.

Now we can finish writing the Sale template:

// The 'inventory' parameter is a list of items available in
// the store, together with their prices.
template Sale2(buyer, seller, amount, item, inventory) =
  // Some buyer orders an item for some price from a seller
  <buyer> order: Order where
      order.amount = amount &&
      order.recipient = seller &&
      order.item = item
  then
  // The seller delivers that item
  <seller> delivery: Delivery where
      // Use the provided inventory to determine whether
      // the seller has the item.
      checkOffer inventory order.item order.amount &&
      delivery.item = order.item &&
      delivery.recipient = buyer

With this formulation of the contract template, we could instantiate it to be bikeshop-specific, bookshop-specific, etc., by defining different inventories for each shop:

// Items in a bike shop are bicycles or other gear.
val bikeShopInventory =
  [ ("Bike", 100),
    ("Brakes", 20),
    ("Helmet",30)] // It's a small bike shop.

// Items in our book shop are just the authors.
val bookShopInventory =
  [ ("Joyce", 10),
    ("Proust", 2),
    ("Hugo", 13)] // We just sell three books

// Items in this shop are the allowed ingredients in brunch.
val brunchShopInventory =
  [ ("Pancake", 1),
    ("Bacon", 2),
    ("Egg", 1)] // Nothing else goes in a brunch.

Providing fail-safe mechanisms

In CSL, sending an unexpected event to a contract does not cause this contract to fail. Instead, the contract simply waits for another event to arrive. This means that if the seller sends a Delivery event containing a different item than the one ordered, such an event is simply ignored by the contract, and the seller can try again.

Sometimes we want to react to a situation where something wrong happened, and have the contract fail, as it has been breached. For instance, if we ordered a bike and paid enough for it, we expect the seller to not try sending us a hammer instead. To account for the possibility of a contract failing, we use the contract combinator or and the primitive contract failure:

template Sale3(buyer, seller, amount, item, inventory) =
  // Some buyer orders an item for some price from a seller
  <buyer> order: Order where
      order.amount = amount &&
      order.recipient = seller &&
      order.item = item
  then (
    // The seller delivers that item
    <seller> delivery: Delivery where
        checkOffer inventory order.item order.amount &&
        delivery.item = order.item &&
        delivery.recipient = buyer
  or
    // The seller tries to cheat
    <seller> delivery: Delivery where
        // The order was accepted
        checkOffer inventory order.item order.amount &&
        // But something isn't right with the delivery
        (not (delivery.item = order.item) ||
         not (delivery.recipient = buyer))
    then failure
  )

We only want the contract to fail if the seller tries to deliver the wrong item, or deliver it to the wrong person. To express those two possibilities in the where clause, we use the connective ||, which is the logical “or” operator, and the negation operator not. Combining two different events with an or combinator gives us two possibilities of how the contract can evolve. In both cases we wait for a Delivery event, we also expect that the order was accepted (inventoryFunction returning true). Whether the contract results in failure or not, depends then on the correctness of the delivery details.

Exercise: Pay or return

Continue the pay on delivery exercise by allowing a return of unwanted items.

Create an inventoryPrice function, which, for each item, returns its price. For simplification, you can assume that for items which are not explicitly listed, the price is some arbitrary large number. The seller should now include the price of the item in the Delivery event, based on what the inventoryPrice function returns. The buyer then has two options: either pay what is asked of them, or return the item to the seller (solution).

Exercise: You need a bike and a helmet!

Write a contract in which the buyer orders both "Bike" and "Helmet", in any order. You can write it using only or and then, but it is easier if you use the and combinator instead (solution).

Adding time constraints

By now we have reached a fairly advanced contract, describing in an accurate way a number of sales-related scenarios. There is one serious omission in the contract formulation which we must address: The concept of time does not occur in the contract at all and therefore does not influence which events are allowed or not. Currently, it is perfectly legal behaviour for, e.g., Alice to place an order and then for Bob to wait ten years before delivering the ordered item.

What needs to be done is clear in light of the above sections. All events already have a timestamp field, simply by virtue of being an Event. We will use this timestamp to specify a maximum time period between when an order is placed and when the delivery takes place, i.e., the difference in the timestamp fields on the Order and Delivery events must not exceed some amount of days:

template Sale(buyer, seller, amount, item, inventory, maxDays) =
  // Some buyer orders an item for some price from a seller
  <buyer> order: Order where
    order.amount = amount &&
    order.recipient = seller &&
    order.item = item
  then (
    // The seller delivers that item
    <seller> delivery: Delivery where
      checkOffer inventory order.item order.amount &&
      delivery.item = order.item &&
      delivery.recipient = buyer &&
      // 'DateTime::addDays t d' creates a new timestamp that
      // is 'd' days after timestamp 't'.
      delivery.timestamp <= DateTime::addDays order.timestamp maxDays
    or
    // The seller tries to cheat
    <seller> delivery: Delivery where
        checkOffer inventory order.item order.amount &&
        (not (delivery.item = order.item) ||
         not (delivery.recipient = buyer))
    then failure
  )

The new clause that has been added on line 15 states that the Delivery must occur before maxDays has passed since the Order event occurred. We achieve this with a simple comparison of timestamps: The timestamp on the received Delivery event must be no later than a timestamp that is exactly maxDays in the future from the time of the Order event. The function DateTime::addDays takes a timestamp and an integer denoting a number of days and creates a new timestamp that is exactly the specified number of days removed from the input timestamp. This is another example of usage of a function from the standard library.

Exercise: Late payment

Extend the pay on delivery exercise again, this time by giving a time limit of 3 days to pay for the delivered item. In case the payment is not received in time, the price increases by a fine, which is as a parameter to the contract template (solution).