Contracts

In this section you can see a selection of example CSL contracts. Some of these will be directly copy-pasteable as-is while others assume that they occur in some context with the proper event types defined. It will be clear from the examples whether you need to insert the appropriate missing bits or not.

Many contracts use the recurring event types Payment and Delivery, defined as follows:

type Payment : Event {
  amount : Int, // Amount of money in euros
  receiver : Agent
}
type Delivery : Event {
  goods : String
}

Recall that the base Event type is defined as:

type Event {
  agent : Agent,
  timestamp : Instant
}

Delivery deadline relative to payment

In this example, a payment from Alice is required before a delivery from Bob. The delivery has a deadline of “two days after receiving payment”:

contract entrypoint deliveryDeadline = \(alice, bob) ->
  <alice> p: Payment
  then
  <bob> d: Delivery where
    d.timestamp < Instant::addDays 2 p.timestamp

The expression uses the strictly-less-than comparison operator < and as a consequence, the delivery cannot be exactly two days later than the payment but only until, but not including, two days later. Had we instead used the <= operator, the delivery would be allowed to occur two days after payment on the second.

Late payment

The following is a specification of a contract in which Alice must pay 100 euros before some deadline and once this has occurred, Bob has 2 days to perform a delivery of "SomeBike". If Alice pays after the deadline, she has to pay 110 euros in order to get Bob to deliver the "SomeBike". Bob still has to deliver "SomeBike" before two days after payment when Alice pays too late.

contract entrypoint latePayment =
  \(paymentDeadline: Instant, alice: Agent, bob: Agent) ->
  <alice> p: Payment where
    p.amount = 100 &&
    p.timestamp <= paymentDeadline
  then
  <bob> d: Delivery where
    d.timestamp < Instant::addDays 2 p.timestamp &&
    d.goods = "SomeBike"
  or
  <alice> p: Payment where
    p.amount = 110 &&
    p.timestamp >= paymentDeadline
  then
  <bob> d: Delivery where
    d.timestamp < Instant::addDays 2 p.timestamp &&
    d.goods = "SomeBike"

The contract uses the or combinator to combine the contracts for payment on time and late payment.

Partial payments

In the previous contracts, the full amount had to be paid in one go. It is possible to write a contract that allows payments to occur over several events:

contract entrypoint partialPayment = \(deadline,alice,bob) ->
  let
    contract rec payPartially = \remainingAmount ->
      <alice> p: Payment where
        p.timestamp < deadline &&
        p.amount < remainingAmount
      then
        // She paid only part of the amount, so await the remaining sum.
        payPartially (remainingAmount - p.amount)
      or
      <alice> p: Payment where
        p.timestamp < deadline &&
        p.amount = remainingAmount

    val deliveryDeadline = Instant::addDays 2 deadline
  in
    payPartially 100 // Alice must pay 100 euros in total
    then
    <bob> d: Delivery where
      d.timestamp < deliveryDeadline &&
      d.goods = "SomeBike"

In this example we make essential use of recursive contracts. We define a local recursive contract called payPartially which takes as its single parameter the remaining amount of money that has to be paid. The contract arising from this contract function uses an or-combination of a recursive call to the contract function itself and another prefix contract to handle the following to cases:

1. Alice pays an amount that is smaller than what is owed. The contract function is used to create a new contract that handles the remaining amount.

2. Alice pays the entire amount and the contract completes successfully.

When the payPartially-instantiated contract finishes it can only be because Alice has sent one or more events with payments of 100 euros. We omit the concept of change here, so the contract only supports exact payments. At that point, the “top-level” contract is simply:

// .. deliveryDeadline defined earlier ...
(
  success
)
then
<bob> d: Delivery where
  d.timestamp < deliveryDeadline &&
  d.goods = "SomeBike"

One can always simplify a contract success then c to just c, so the residual contract is:

// ... deliveryDeadline defined earlier ...
<bob> d: Delivery where
  d.timestamp < deliveryDeadline &&
  d.goods = "SomeBike"

Only a delivery is expected now.

Escrow

Below is a version of the standard sale-of-bike contract repeated for the sake of example:

contract entrypoint bikeSale = \(seller, buyer) ->
  <buyer> p: Payment where
    p.amount = 100 &&
    p.receiver = seller
  then
  <seller> d: Delivery where
    d.goods = "SomeBike" &&
    p.receiver = buyer

One could consider it problematic that the buyer is obligated to perform a payment before receiving the bike as maybe the bike was not in good condition upon arrival. However, requiring delivery before payment is also unreasonable because the seller would not like to deliver a bike without knowing that it will be paid for. Instead we introduce a trusted third-party agent to the contract:

contract entrypoint bikeSaleEscrow = \(trustedParty, seller, buyer, deliveryDeadline) ->
  <buyer> p: Payment where
    p.receiver = trustedParty &&
    p.amount = 100
  then (
    <seller> d: Delivery where
      p.receiver = buyer &&
      d.goods = "SomeBike" &&
      p.timestamp < deliveryDeadline
    then
    <trustedParty> tp: Payment where
      tp.receiver = seller &&
      tp.amount = 100
    or
    <trustedParty> bp: Payment where
      bp.receiver = buyer &&
      bp.amount = 100 &&
      bp.timestamp > deliveryDeadline
  )

The idea is that trustedParty is a third-party agent that both seller and buyer trusts enough to hold the payment in escrow. Initially, the buyer submits a Payment to the trustedParty of the expected amount. After that, either the seller will perform a Delivery after which the trustedParty is obliged to perform a Payment to the seller. If the seller does not perform a Delivery within the deadline, the trustedParty must to pay back the money to buyer.

An important thing to consider when entering into the escrow contract is that the resource-flows are as expected. After successful completion of the contract, either the seller has one SomeBike fewer than before and buyer has 100 fewer euros or no party in the contract have any change in resource holdings.

Transferable contract

The following is an example of a car-ownership/rental contract where the car can be rented out to other parties and where the owner may transfer ownership of the car completely:

type Open : Event {} // Open the car doors
type Close : Event {} // Close the car doors
type Return : Event {} // Return car to owner
type TransferOwnership : Event {
  newOwner : Agent
}
type ReserveCar : Event {
  renter : Agent,
  rentalStart : Instant,
  rentalEnd : Instant
}
// When does user stop having the rights to a car
type EndUsage
  | Ends Instant // At this point in time.
  | Never // The user owns the car.

val mayStillUseCar = \time ->
  \ Ends endTime -> time <= endTime
  | Never        -> True

contract carUsage = \user -> \start -> \endUsage ->
  <user> o: Open where
    o.timestamp > start &&
    mayStillUseCar o.timestamp endUsage
  then
  <user> Close

contract rec carRental = \renter -> \rentalStart -> \rentalEnd ->
  carUsage renter rentalStart (Ends rentalEnd)
  then carRental renter rentalStart rentalEnd
  or
  <renter> Return

contract rec entrypoint carOwnership = \(owner, start) ->
  <owner> t: TransferOwnership then carOwnership (t.newOwner, t.timestamp)
  or
  carUsage owner start Never then carOwnership (owner, start)
  or
  <owner> r: ReserveCar
  then
  carRental r.renter r.rentalStart r.rentalEnd
  then
  carOwnership (owner, start)

Ownership of the car is modeled by the contract carOwnership. An owner can do one of the following:

1. Give the car to someone else by issuing a TransferOwnership. This causes the next valid sequence of events to be modeled by a new instance of the carOwnership contract with a new owner.

2. Use the car. Car usage is modeled in a simplified way where a user can just open and close the car doors if she is allowed to at that point in time. The carOwnership contract makes sure that the owner of the car is always allowed to use the car by setting the endUsage to Never.

3. Rent out the car to someone else, temporarily giving the renter the rights to use the car but requiring that she returns it back again. The renter may only use the car until a certain point in time. This is achieved by setting the endUsage to Ends rentalEnd.

This contract also demonstrates the usefulness of sum types. EndUsage expresses that either there is an expiration date for the car or the car can be used as long as the user likes, reflecting the situations where the car is either used by the renter or the owner. We also introduced a convenience function mayStillUseCar that compares a timestamp to a value of type EndUsage. Either the EndUsage is an Ends d where d is an Instant, in which case we just compare the timestamps to see if the user may use the car, or the EndUsage is a Never, in which case the user may always use the car and the function returns True.

Signing contracts

In the car ownership/rental example above, the car owner basically gets to decide whether a new owner should have the car or not. This is unlikely to model a realistic transfer of ownership, as the recipient might want the chance to either accept or reject the offer. We can extend our contract from above with a notion of signing:

// ... events 'Close', 'Return', etc. defined as before
// ... contracts 'carUsage', 'carRental', defined as before
type Sign : Event {}
type Reject : Event {}

template [theContract, default] SignedContract party deadline =
<party> s: Sign where
  s.timestamp < deadline
then theContract
or
<party> Reject then default

contract rec entrypoint carOwnershipSigned = \(owner, start) ->
  <owner> t: TransferOwnership
  then
  SignedContract[
    // Transfer ownership if the new owner accepts the transfer and signs.
    carOwnershipSigned (t.newOwner, t.timestamp),
    // Keep ownership if the new owner rejects the transfer.
    carOwnershipSigned (owner, start)
  ] t.newOwner (Instant::addDays 2 t.timestamp)
  // New owner must sign before two days
  or
  carUsage owner start Never then carOwnershipSigned (owner, start)
  or
  <owner> r: ReserveCar
  then
  carRental (r.renter) (r.rentalStart) (r.rentalEnd)
  then
  carOwnershipSigned (owner, start)

After being offered a car with the TransferOwnership event, the recipient can choose to either accept or reject the offer with a Sign or Reject event, respectively. We use the contract template SignedContract with two contract parameters to model the general pattern where two different things might happen depending on whether the user signs or not. In the carOwnershipSigned contract we then simply instantiate the SignedContract with contracts reflecting the cases where the recipient accepts or rejects the car. For the purposes of this example, the only requirements that are checked on the signature is that it happened before a certain deadline.

Pattern matching contracts

Contract functions can pattern match on their argument. This allows you to write contract specifications that can change behaviour depending on their instantiation arguments or the value of events they accept.

Coupon Payments

With pattern matching and recursive contracts, you can dynamically construct a sequence of prefix-contracts from an input list. For example, many financial products have a list of coupon payments associated with them. Given a list of coupon payment dates and their values, we can use pattern matching and iteration to write a contract that accepts the coupon payments with the right criteria.

// Signifies a payment of a coupon.
type Payment : Event { amount: Float, recipient: Agent }

// Specification of a coupon payment by its date and value.
typealias CouponPaymentSpec = Tuple Instant Float

// Make multiple coupon payments.
// Assumes `couponPaymentDates` is sorted by the first component of the tuple.
contract entrypoint couponPayments = \(
  payingAgent: Agent,
  recipient: Agent,
  couponPaymentDates: List CouponPaymentSpec
) -> let
  // Pattern match on a list of CouponPaymentSpec.
  // If the list is empty, we're not expecting any more coupon payments.
  // If not, we create the contract that waits for a coupon payment
  // before continuing with the rest of the list.
  contract rec couponPaymentsHelper =
    \ Nil -> success
    | Cons (nextCouponDate, nextCouponAmount) restCoupons ->
      <payingAgent> p : Payment where
        p.timestamp = nextCouponDate &&
        p.amount = nextCouponAmount &&
        p.recipient = recipient
      then
      couponPaymentsHelper restCoupons
  in
    couponPaymentsHelper couponPaymentDates

Dynamic Bike Delivery

Pattern matching can also be used to alter the behaviour of a contract depending on its instantiation parameters. For example, when buying a bicycle, the customer might have a choice on how it is delivered. Depending on the customer’s choice, the contract can alter how it must be completed.

// A type modeling how the bike is to be delivered.
type DeliveryOptions
  | InPerson Instant // Pick up in store at a specified date.
  | DeliveryToHome String // Send to home address provided.
  | DeliveryToPackageShop String // Send to a selected package shop.

// Models that a customer has chosen a product and how it should be delivered.
type SelectProduct : Event {
  product : String,
  deliveryOption : DeliveryOptions
}

// These events each correspond to a constructor of DeliveryOptions above.
type PickUp : Event { product : String }
type Deliver : Event { address : String, product : String }
type DeliverToShop : Deliver {}

// Used to model notification of the recipient that they can pick up their bike.
type Notify : Event { recipient: Agent }

// Pattern matches on its fourth argument, which is of type DeliveryOptions.
// Depending on this value, the contract that is returned accepts a different type of event.
contract delivery = \seller -> \buyer -> \product ->
  \InPerson date ->
    <buyer> pu : PickUp where pu.timestamp = date && pu.product = product
  | DeliveryToHome address ->
    <seller> d: Deliver where d.address = address && d.product = product
  | DeliveryToPackageShop address ->
    <seller> d : DeliverToShop where d.address = address && d.product = product
    then
    <seller> n : Notify where n.recipient = buyer

// Models a customer selecting a product and their preferred delivery method.
// The contract dynamically accepts the correct delivery event depending on their choice.
contract entrypoint sale = \seller ->
  <*> sp : SelectProduct
  then
  delivery seller sp.agent sp.product sp.deliveryOption