Examples of CSL 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 : DateTime
}

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”:

template entrypoint DeliveryDeadline(alice,bob) =
  <alice> p: Payment
  then
  <bob> d: Delivery where
    d.timestamp < DateTime::addDays p.timestamp 2

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.

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
template entrypoint LatePayment
  (paymentDeadline: DateTime, alice: Agent, bob: Agent) =
  <alice> p: Payment where
    p.amount = 100 &&
    p.timestamp <= paymentDeadline
  then
  <bob> d: Delivery where
    d.timestamp < DateTime::addDays p.timestamp 2 &&
    d.goods = "SomeBike"
  or
  <alice> p: Payment where
    p.amount = 110 &&
    p.timestamp >= paymentDeadline
  then
  <bob> d: Delivery where
    d.timestamp < DateTime::addDays p.timestamp 2 &&
    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:

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
20
21
template entrypoint PartialPayment(deadline,alice,bob) =
  let
    template 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 = DateTime::addDays deadline 2
  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 contract template called PayPartially which takes as its single value parameter the remaining amount of money that has to be paid. This template gets instantiated to a contract that is a combination (with or) of two contracts for the following scenarios:

  1. Alice pays an amount that is smaller than what is owed. The contract template 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:

template 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:

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
template 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:

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
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 : DateTime,
  rentalEnd : DateTime
}
// When does user stop having the rights to a car
type EndUsage
  | Ends DateTime // At this point in time.
  | Never // The user owns the car.

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

template CarUsage(user, start, endUsage) =
  <user> o: Open where
    o.timestamp > start &&
    mayStillUseCar o.timestamp endUsage
  then
  <user> Close

template rec CarRental(renter, rentalStart, rentalEnd) =
  CarUsage(renter, rentalStart, Ends rentalEnd)
  then CarRental(renter, rentalStart, rentalEnd)
  or
  <renter> Return

template 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 on line 29.

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 be the renter or the owner. We also introduced a convenience function mayStillUseCar that compares a timestamp to a value of type EndUsage on line 18. Either the EndUsage is an Ends d where d is a DateTime, 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:

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
// ... events 'Close', 'Return', etc. defined as before
// ... templates '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

template 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, DateTime::addDays t.timestamp 2)
  // 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 on line 6 with two template parameters to model the general pattern where two different things might happen depending on whether the user signs or not. In the CarOwnership template on line 16 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.