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 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 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 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 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 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 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 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.

Past events

Events that are applied to a contract are available via the special self instantiation argument and the function getEvents. Let’s say we create an amusement park called Tivoli which can issue day passes to any guest and only guests with day passes can ride the roller coaster. For the sake of example, let’s also say that all day passes must have a unique id, and that a person can only carry one day pass:

 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
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
type Payment: Event {
  amount : Int
}

type DayPass: Event {
  receiver : Agent,
  id : Int
}

type Ride: Event {
  person : Agent
}

// Find the next available id by looking at the previously largest id
val nextDayPassId = \contractId -> let
  val dayPassId =
    \(e:Event) -> type x = e of { DayPass -> Some x.id; _ -> None }
  val dayPassEvents = List::mapMaybe dayPassId (getEvents contractId)
  val sorted = List::sort (flip compareInt) dayPassEvents
in
  fromMaybe 0 (List::head sorted) + 1


// Does the person have a daypass for today?
val hasDayPass =
  \contractId -> \person -> \timestamp -> List::any (\(e: Event) ->
  let
    val sameDay = \timestamp1 -> \timestamp2 ->
      let
        val cs1 = DateTime::components timestamp1
        val cs2 = DateTime::components timestamp2
      in
        cs1.year = cs2.year && cs1.month = cs2.month && cs1.day = cs2.day
  in
    type daypass = e of {
      DayPass ->
        daypass.receiver = person && sameDay daypass.timestamp timestamp;
      _ -> False
    }) (getEvents contractId)

// Only issue day passes if a customer pays
template rec IssueDayPass(self, tivoli) =
  <*> payment: Payment where payment.amount = 10
  then
  <tivoli> daypass: DayPass where
    daypass.receiver = payment.agent &&
    daypass.id = nextDayPassId self &&
    // A person can only carry one day pass
    not (hasDayPass self daypass.receiver daypass.timestamp)
  then IssueDayPass(self, tivoli)

template rec RideRollerCoaster(self) =
  <*> ride: Ride where hasDayPass self ride.person ride.timestamp
  then RideRollerCoaster(self)

template Tivoli(self, tivoli) =
  IssueDayPass(self, tivoli)
  and
  RideRollerCoaster(self)

Here we use the getEvents twice: To find the next available day pass id and to make sure that a customer has a day pass when requesting a ride on the roller coaster.

For nextDayPassId we iterate through all past events, considering only DayPass events using the type case construction. Next, we sort them by id and pick the first one.

For hasDayPass we check that there is a day pass issued to the person requesting a ride on the roller coaster on the same day. The year, month, and day of the timestamps are compared using the DateTime::components.

In this example, we use both List::mapMaybe and fromMaybe from the standard library. List::mapMaybe is used to do a filter and projection to extract only DayPass from Events and then transform the list to only contain the id fields.

For another example of using past events, see the Language guide.

Observe events on other contracts

To continue the Tivoli example, let’s model another amusement park, Bakken where day passes from Tivoli grant access to one free ride. We will need to access the running contract of Tivoli and find issued day passes, and make sure they are used only once in Bakken:

 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
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
type DayPass: Event {
  receiver: Agent,
  id: Int
} // From "Tivoli"

type Ride: Event {}

type TicketRide: Ride {
  ticketId: Int
}

// For tivoli day pass one time uses
type TivoliCampaignRide: Ride {
  person: Agent,
  ticketId: Int,
  tivoliContractId: ContractId
}

type Payment: Event {
  amount : Int
}

type Ticket: Event {
  id: Int
}

// Find the next available id by looking at the previously largest id
val nextTicketId = \contractId -> let
  val ticketId =
    \(e:Event) -> type x = e of { Ticket -> Some x.id; _ -> None }
  val ticketEvents = List::mapMaybe ticketId (getEvents contractId)
  val sorted = List::sort (flip compareInt) ticketEvents
  in fromMaybe 0 (List::head sorted) + 1

val isValidTicket = \contractId -> \(ride1: Ride) -> let
  val bakkenEvents = getEvents contractId
  in type ride = ride1 of {
    TicketRide ->
      // There exist a ticket with this id
      List::any (\(e:Event) ->
        type ticket = e of {
          Ticket -> ticket.id = ride.ticketId;
          _ -> False }
        ) bakkenEvents
      &&
      // And it's not already used
      not (List::any (\(e:Event) ->
        type x = e of {
          TicketRide -> x.ticketId = ride.ticketId;
          _ -> False }
        ) bakkenEvents);

    TivoliCampaignRide ->
      // There exist a tivoli day pass with this id
      List::any (\(e:Event) ->
        type daypass = e of {
          DayPass -> daypass.receiver = ride.person;
          _ -> False }
        )
        // Referencing the "Tivoli" contract
        (getEvents ride.tivoliContractId)
      &&
      // And it's not already used
      not (List::any (\(e:Event) ->
        type x = e of {
          TivoliCampaignRide -> x.ticketId = ride.ticketId;
          _ -> False }
        ) bakkenEvents);
    _ -> False
  }

template rec IssueTicket(self, bakken) =
  <*> payment: Payment where payment.amount = 2
  then
  <bakken> ticket: Ticket where
    ticket.id = nextTicketId self
  then IssueTicket(self, bakken)

template rec RideFerrisWheel(self) =
  <*> ride: Ride where isValidTicket self ride
    then RideFerrisWheel(self)

template Bakken(self, bakken) =
  IssueTicket(self, bakken)
  and
  RideFerrisWheel(self)

Here, line 60 holds the reference to the Tivoli amusement park contract events. Referencing other contracts requires the id of the instantiated contract, so if the Tivoli contract is instantiated with id 42, the TivoliCampaignRide.tivoliContractId field must be 42.

For another example of referencing other contracts, see the Language guide.

Modules

Modules provide a way to organize contract specifications for larger contracts. Many of the examples in the previous section includes references to the standard library, which contain several modules (see the source code). But it is also possible to create custom modules using the module notation.

We illustrate this with a area/circumference calculator for circles:

 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
module Constants {
  val pi = 3.14159
}

module Circle {
  type Circle: Event {
    name: String,
    r: Float
  }

  module Calc {
    val circumference = \r -> 2.0 * Constants::pi * r
    val area = \r -> Constants::pi * r * r
  }

  // Returns all Circle events where name matches
  val findCircle = \cid -> \name ->
    List::mapMaybe (\(e:Event) ->
      type c = e of {
        Circle::Circle -> if (c.name = name) Some c else None;
        _ -> None
      }) (getEvents cid)

  val area = \cid -> \name ->
    let
      // only consider the first
      val byId = List::head (Circle::findCircle cid name)
    in
      maybe 0.0 (\(c:Circle::Circle) -> Circle::Calc::area c.r) byId

  val circumference = \cid -> \name ->
    let
      // only consider the first
      val byId = List::head (Circle::findCircle cid name)
    in
      maybe 0.0
            (\(c:Circle::Circle) -> Circle::Calc::circumference c.r)
            byId
}

template rec C() =
  <*> c: Circle::Circle where c.r > 0.0
  then C()

This contract, accepts events of type Circle with a radius and a name.

Here, we have defined two modules, one for constants and one for functions to calculate the area and circumference. Notice that we use sub modules to define an internal module Circle::Calc to do calculations.

The area and circumference of a circle is available with the functions area and circumference after a Circle event has been applied:

// For the circle defined as
Circle::Circle {
  name = "my circle",
  r = 3.0
}

Circle::area "my circle"
// returns 28.27431

Circle::circumference "my circle"
// return 18.849

For more information about modules, see the language guide.