Contract language reference

This section presents an overview of the CSL language constructions for the composition of contracts.

The atomic contracts of CSL are the smallest building blocks:

The non-atomic contracts all specify behaviour relative to smaller sub-contracts. Herein lies the composability of CSL: We formulate general structures that we may re-use across several contracts. There are five ways to compose contracts:

Note that the code examples in the following sections will sometimes consist of snippets of CSL code, not entire CSL specifications that can be copy-pasted and run. We have attempted to add comments in the code snippets to make it clear which parts have been left out, so it should not be too much work to copy and reuse the example snippets.

The successfully completed contract

A successfully completed contract is written as:

success

Because it is completed, this contract accepts no events.

The breached contract

The failed, or breached, contract is written as:

failure

A breached contract is in a state of failure and therefore it accepts no events.

The prefixed-contract

A “prefix-contract” is a contract that expects an event satisfying some predicate and after receiving a matching event it becomes a new contract. The general format is:

<AGENT> x:EVENTTYPE where PREDICATE

The above general form should be read as:

The agent identified by the value AGENT must issue an event of the type EVENTTYPE. This event is called x, and the predicate PREDICATE must evaluate to True. If it does, consume the event and evolve to success. Otherwise, do nothing.

If the originator of the event is unimportant, we may write *, matching any agent. Likewise, we may completely omit the where-clause with the predicate. Doing so corresponds to matching any event with the given type.

Examples

The following example illustrates how one could match certain Foo events from Alice:

<alice> n: Foo where n.timestamp < #2017-08-31T23:00:00Z#

This is a specification of a contract that expects an event of type Foo from Alice where the timestamp field is before August 31st at eleven o’clock in the evening. After receipt of such an event, the reduced contract is success.

If we instead wanted to match just any event of type Foo, with no constraints on either the fields of the event or on the originating agent, we could write the following:

<*> Foo

This snippet is equivalent to writing

<*> Foo where True

which is again equivalent to

<*> f: Foo where True

We may chain together several prefix contracts using the then sequence combinator. For example, the following contract snippet specifies that first a payment event from Alice and then a delivery event from Bob must occur, after which no more events may occur:

type Payment : Event { receiver: Agent, amount: Int }
type Delivery : Event { receiver: Agent }

// ... definition of Payment and Delivery events ...
template C1(alice,bob) =
  <alice> p: Payment where
    p.receiver = bob &&
    p.timestamp = #2017-08-24T12:00:00Z#
  then
  <bob> d: Delivery where
    d.receiver = alice &&
    d.timestamp < #2017-08-26T12:00:00Z#

Now, assume that the agent Alice has input the following event:

Payment {
  agent = alice,
  timestamp = #2017-08-24T12:00:00Z#,
  receiver = bob
}

This event satisfies the first predicate, so our contract accepts it and evolves into its residual:

template C2(alice,bob) =
  <bob> d: Delivery where
    d.receiver = alice &&
    d.timestamp < #2017-08-26T12:00:00Z#

Bob now issues an event:

Delivery {
  agent = bob
  timestamp = #2017-08-25T12:00:00Z#,
  receiver = alice
}

The second predicate of the original contract (or the first predicate of the residual contract) is satisfied with this event, so the contract evolves into:

template C3() = success

No more events may be applied; the sequence of events that our contract specified was observed.

Sequentially composed contracts

Given two contracts c1 and c2, their sequential composition is the contract:

c1 then c2

A contract that is a sequential composition of two other contracts specifies that the left-hand contract must be completed before the events of the right-hand contract can be considered.

Precedence of binary operators

The precedence of the three binary contract operators is as follows:

  1. then binds tighter than
  2. and, which binds tighter than
  3. or.

This means that the following

a then b or c and d then e

is equivalent to

(a then b) or (c and (d then e))

When you write a contract and need a different structure than the default imposed by the operators’ precedence levels you can use parentheses to change it.

Examples

Consider the following example where we define the two contracts AlicePays and BobDelivers:

template AlicePays(alice,bob) =
  <alice> p: Payment where p.receiver = bob

template BobDelivers(alice,bob) =
  <bob> d: Delivery where d.receiver = alice

Given these definitions, the following two contracts are equivalent:

// Combine two smaller contracts into one.
template AlicePaysThenBobDelivers(alice,bob) =
  AlicePays(alice,bob) then BobDelivers(alice,bob)
// Equivalent formulation:
template AlicePaysThenBobDelivers2(alice,bob) =
  <alice> p: Payment where p.receiver = bob
  then
  <bob> d: Delivery where d.receiver = alice

Concurrently composed contracts

The concurrent composition of two contracts c1 and c2 is the contract:

c1 and c2

Composing contracts concurrently yields a contract that accepts all event sequences that are accepted by either the two constituent contracts, where the sequences might be interleaved. For any contract c, the contracts success and c and c and success are equivalent.

The precedence level is below then and above or.

Examples

Say we wanted to express a sales contract where the buyer was free to pay the seller before or after delivery of the goods. The following contract is a reformulation of our sales contract between Alice and Bob that allows for just that:

template SaleWithoutTemporalRestrictions(alice,bob) =
  <alice> p: Payment where p.receiver = bob
  and
  <bob> d: Delivery where d.receiver = alice

This contract specifies that Alice and Bob must issue Payment and Delivery events, but not that they must occur in any specific order. Both the event sequence “Payment-then-Delivery” and “Delivery-then-Payment” are valid according to this contract. After applying the event

Payment {
  agent = alice,
  timestamp = #2017-08-24T13:37:00Z#
  receiver = bob
}

the residual contract will be

success
and
<bob> d: Delivery where d.receiver = alice

This contract accepts just the Delivery event from Bob.

If we had instead applied a Delivery event first, the residual contract would have been

<alice> p: Payment where p.receiver = bob
and
success

Now the contract expects a Payment event from Alice next.

Choice between contracts

The choice between two contracts c1 and c2 is the contract:

c1 or c2

The choice-contract allows composition of two independent contracts into a new contract that expects exactly one of the two contracts to be completed. Depending on the shape of the two sub-contracts and the incoming event, one or the other will be picked as the residual contract.

The precedence level is below both then and and.

Examples

Consider a scenario in which we would like Alice to pay a sum of money and the sum depends on whether she pays before or after Christmas eve 2018. Each of the sub-scenarios can be modelled with a simple prefix-contract, and we can use or to combine them in the appropriate way:

val deadline0 = #2018-12-24T13:37:00Z#

template PayBeforeOrAfterChristmas0(alice) =
  <alice> p: Payment where p.timestamp <= deadline0
  or
  <alice> p: Payment where p.timestamp > deadline0

The contract can evolve in two different ways. Either Alice performs a Payment before the deadline of 2018-12-24T13:37:00 with an amount of 100, or Alice performs a Payment after the deadline and then the amount has to be 200. Exactly one of these two things has to occur in order for the entire contract to be satisfied. Applying a Payment event either before or after the deadline yields the residual contract

success

This is because the residual contract of the two individual prefix-contracts are both success.

Consider instead the following variation on the contract, where either Santa Claus or Bob sends a Delivery event depending on whether the Payment came before or after Christmas:

val deadline1 = #2018-12-24T13:37:00Z#

template PayBeforeOrAfterChristmas1(alice,bob,santaClaus) =
    <alice> p: Payment where p.timestamp <= deadline1
    then
    <santaClaus> Delivery
  or
    <alice> p: Payment where p.timestamp > deadline1
    then
    <bob> Delivery

Applying a Payment event before the deadline will now yield the residual contract

<santaClaus> Delivery

If the Payment came after the deadline, the residual would instead be

<bob> Delivery

The success contract denotes a contract that is considered to have been completed in a successful manner. If we combine that with some other contract c using or, we construct a contract where the events of c are permitted but not obligated. Suppose we construct a contract as follows:

template C(alice) = <alice> Payment or success

This is a contract where Alice may perform a Payment event if she chooses.

We can extend the permission contract to a contract where there is an optional choice to be made:

type Option1 : Event {}
type Option2 : Event {}
type Action : Event {}

template OptionalChoice(alice,bob,charlie) =
    <alice> Option1
    then
    <bob> Action
  or
    <alice> Option2
    then
    <charlie> Action then success

In this contract, Alice may choose to perform either of the events Option1 or Option2, resulting in either the residual contract where Bob can perform an Action or the contract where Charlie can perform an Action. She may also choose not to send any events; the final composition with the success contract allows that.

Contract templates

A contract template with the name TemplateName has the general form:

template [c0, ..., cn] TemplateName (p0, ..., pm) = BODY

where c0, …, cn are contract parameters and p0, …, pm are value parameters. In the special case where there are zero contract parameters, we may also use the equivalent shorthand:

template TemplateName (p0, ..., pm) = BODY

A contract template, either with or without contract parameters, is a name for a contract that can be re-used. Using a contract template means instantiating the contract and value parameters, if any, with contract arguments and value arguments, respectively. This means that we can capture general contract design patterns with contract templates and apply them whenever they are needed.

CSL allows the use of local contract templates: Templates that are only usable inside some other contract. This can be handy if we need some contract template that is too specific to be at the top-level but where we would still like the benefits from encapsulating a pattern. The syntax for a local contract template is:

// ... inside some contract definition
let template [c0, ..., cn] TemplateName (p0, ..., pm) = TEMPLATEBODY
in
    BODY

Inside of the contract body BODY we may now use the template TemplateName, but it is not visible from the outside nor is it visible inside TEMPLATEBODY. Earlier definitions are visible in later ones but not vice versa.

Examples

In its most basic form we can write

template JustSucceed() = success

which effectively serves as an alias for the success contract. This contract template takes no value parameters. Say we want to express that a Payment event from Alice for some not-yet-specified amount of money has to occur. There is just one (value) parameter to this contract template, namely the sum of money. We express it as follows:

// ... Payment event defined here
template AlicePaysAmount(amount,alice) =
<alice> p: Payment where p.amount = amount

If now want to express some sale where Alice pays 42 euros and then, for the sake of simplicity, nothing more happens, we write

template SomeSale(alice) = AlicePaysAmount(42,alice)

Note that this is itself a contract template (still with zero contract parameters). In the section about instantiating contracts it is explained how to get from “static” descriptions of contracts to something that actually lives and runs somewhere.

We might often need to express that some contract be dependent on a signature from an agent. This is a quite general pattern, so we formulate it as a contract template:

type Signature : Event {
 // ... Signature event defined here with appropriate fields
}
template [c] SignAndContinue(agent) =
  <agent> Signature then c

This contract template takes one contract parameter, c, and one value parameter, agent, and it constructs a prefix-contract requiring a Signature event from agent before it evolves into the contract c. We might want to refine this pattern by allowing some default contract to happen if the agent can’t issue a Signature. Our contract template just needs two contract parameters instead of one to achieve this:

// ... Signature event defined as above
template [cSigned, cUnsigned] SignOrDefault(agent) =
  (<agent> Signature then cSigned) or cUnsigned

Here we use the or combinator to choose between the contract where the agent signs which continues as cSigned, and the contract called cUnsigned where the agent does not sign. It could of course be generalized to handle different kinds of signatures, default cases, etc.

Templates themselves can be nested using the let ... in construct:

type SayHello : Event {}
type SayGoodbye : Event {}
template HelloHelloGoodbyeLocal(agent) =
  let
    // 'agent' says "hello" and the template evolves
    // into the contract given by 't'
    template [t] Hello() = <agent> SayHello then t
    // 'agent' says either "goodbye" and the contract
    // evolves into 't', or she says "hello" and the
    // contract evolves into 't'.
    template [t] Goodbye() =
        (<agent> SayGoodbye then t) or Hello[t]()
  in
    // 'agent' says "hello" twice before saying
    // either "goodbye" or "hello" once and then
    // the contract ends successfully.
    Hello[Hello[Goodbye[success]()]()]()

In this example we exploit the fact that the template Goodbye can use the template Hello. We could write the above without the use of local templates as follows:

// ... SayHello and SayGoodbye defined here ...
template HelloHelloGoodbye(agent) =
  <agent> SayHello then
  <agent> SayHello then
  (
    <agent> SayGoodbye
    or
    <agent> SayHello
  )

Recursive contract templates

A recursive contract template with the name TemplateName has the form

template rec TemplateName(p0, p1, ..., pm) = TEMPLATEBODY

where p0, …, pm are value parameters. Unlike non-recursive contract templates, recursive contract templates are not allowed to have any contract parameters.

Recursive contract templates work like normal contract templates, except that TEMPLATEBODY may call itself by calling TemplateName. All recursive calls must be guarded, which means that at least one event must be accepted by TEMPLATEBODY before a call to TemplateName has to be unfolded to determine what the possible next events of the residual contract is.

If multiple recursive contract templates will need to call each other, the following general form can be used:

template rec TemplateName-0( ... ) = TEMPLATEBODY-0
        with TemplateName-1( ... ) = TEMPLATEBODY-1
        with ...
        with TemplateName-n( ... ) = TEMPLATEBODY-n

All template names TemplateName-0, …, TemplateName-n can be used recursively in all bodies TEMPLATEBODY-0 … TEMPLATEBODY-n. The same restrictions regarding guardedness apply.

Recursive contract template examples

Consider the following recursive contract template PingPong:

type Ping : Event {}
type Pong : Event {}
template rec PingPong() =
  <*> ping:Ping then <ping.agent> Pong then PingPong()
  or
  success

Instantiating this template yields a contract which accepts the event Ping from any agent and then requires the same agent to generate an event Pong, after which it goes back to accepting another Ping event from another agent by calling PingPong(). The contract can be terminated as long as all Ping events have been matched by a corresponding Pong.

For example, if Alice applies Ping to PingPong(), then the residual contract is

<alice> Pong then PingPong()

The following example uses mutual recursion to model a house where a specified agent can move inside and outside and, depending on where the agent is, may perform tasks such as watching TV or mowing the lawn.

type WatchTv : Event {}
type GoOutside : Event {}
type GoInside : Event {}
type MowLawn : Event {}
template House(agent) =
  let template rec Inside() =
        <agent> WatchTv then Inside()
        or <agent> GoOutside then Outside()

      with Outside() =
        <agent> MowLawn then Outside()
        or <agent> GoInside then Inside()
        or success
  in
    Outside()

We have defined the mutually recursive templates as local templates inside a non-recursive contract template to ensure that a House contract can only be instantiated starting in the Outside state. In each of the states Inside and Outside, the agent may perform any number of WatchTv and MowLawn events, respectively, but the agent can only go outside if already inside, and vice versa. Note that the contract may only successfully terminate when the agent is outside.

Guardedness

One has to take care that a (mutually) recursive contract template definition is well-guarded, as unguarded contracts do not have a well-defined semantics. The CSL system will automatically check if a contract is well-guarded and reject it with a descriptive error message otherwise.

A recursive template definition is unguarded whenever it is possible for it to call itself without first consuming an event. For example, the following recursive template does nothing but call itself, and so is clearly unguarded:

template rec Unguarded() = Unguarded()

Unguarded recursive templates are problematic because they can be used to express contracts which has to be unfolded indefinitely before we can determine whether a given event can be applied or not. For example, consider the following unguarded contract template:

type Count : Event { n: Int }

template rec Unguarded(n) =
  <*> p:Count where p.n = n or Unguarded(n+1)

The instantiation Unguarded(0) can, without applying any events, be unfolded to any of the following:

<*> p:Count where p.n = 0 or Unguarded(1)
<*> p:Count where p.n = 0 or p:Count where p.n = 1 or Unguarded(2)
<*> p:Count where p.n = 0 or p:Count where p.n = 1 or
    p:Count where p.n = 2 or Unguarded(3)
...

and so on. In this case, if we are given the event Count { n = 42 }, then the system will have to figure out that it needs to do 42 unfoldings before it reveals a prefix matching the event. Given the event Count { n = -42 }, the system has to analyze the contract to determine that no number of unfoldings can reveal a matching prefix. In general, an unguarded unfolding can generate much more complicated mathematical sequences, and it can be shown that it is theoretically impossible to determine, in general, if there exists a number of unfoldings that reveals a matching prefix or not.

The above example becomes guarded if we change or to then (and add success to allow the contract to terminate):

template rec Guarded(n) =
  <*> p:Count where p.n = 1 then Guarded(n + 1)
  or success

While we can still unfold the recursive calls indefinitely, we do not have to do that in order to determine whether a given event can be accepted: any event must be matched by the prefix that is visible now, so unfolding Guarded(n+1) will not reveal any new information.

It is generally easy to spot unguarded contracts simply by checking that all recursive calls occur below a prefix. However, there is one common pitfall that may lead to accidental unguardedness. Consider the following example:

template Nullable() = <*> Count or success
template rec Unguarded() = Nullable() then Unguarded()

The call to Unguarded() is apparently below a then, making it appear guarded on cursory inspection. However, since it is possible to terminate Nullable() via the right alternative without consuming any events, the call to Unguarded() is exposed.

Contract abbreviations

A contract abbreviation with the name abbreviationName has the general form:

contract abbreviationName = ABBREVIATIONBODY

This defines an abbreviation for the contract ABBREVIATIONBODY and binds it to a contract variable with the name abbreviationName. Abbreviations are defined using the contract keyword with a lowercase name. They are distinguished from templates in that it is not possible to specify any contract or value parameters, and furthermore contract abbreviations cannot refer to themselves, which for the above example means that abbreviationName may not occur as a contract variable within ABBREVIATIONBODY.

CSL allows the definition of local abbreviations that are only visible within contracts. The syntax for a local contract abbreviation is

// ... inside some contract definition
let
    contract abbreviationName1 = ABBREVIATIONBODY1
    contract abbreviationName2 = ABBREVIATIONBODY2
    ...
    contract abbreviationNameN = ABBREVIATIONBODYN
in
    BODY

Inside BODY we may use abbreviationName1, abbreviationName2, …, abbreviationNameN as a contract variables, but they are not visible from the outside. Furthermore, each ABBREVIATIONBODYi may use the previously defined abbreviations abbreviationName1, abbreviationName2, ..., abbreviationName(i-1).

Abbreviations can be used to reformat a complex contract to make it more readable, but otherwise they add no expressive power to the language. It is generally preferable to use abbreviations when the full power of contract templates are not needed, since this communicates to the system that the abbreviations are intended to be used as such, and that any self-reference is accidental and should be flagged as an error.

Examples

In the following example, we express a contract where some agent may either borrow a car or buy it, after which the agent is allowed to drive it. If the car was only borrowed and not bought, then it must be returned again when the agent has finished driving it. To avoid repeating the specification of what it means to drive a car, we define that part of the contract using an abbreviation:

type BorrowCar : Event {}
type ReturnCar : Event {}
type BuyCar : Event {}

type DriveCar : Event {}
type TurnOnCar : Event {}
type TurnOffCar : Event{}

template Drive(agent) =
  let
    contract driveCar =
      <agent> TurnOnCar then
      <agent> DriveCar then
      <agent> TurnOffCar
  in
    (<agent> BorrowCar then
     driveCar then
     <agent> ReturnCar
    )
    or
    (<agent> BuyCar then
     driveCar
     )

We could also have defined a local template DriveCar() instead, but that would have been unnecessary since the driveCar contract never needs to call itself. In this way, readers of our contract can determine just by looking at the definition head of driveCar that it is truly just an abbreviation, and that its body cannot refer back to itself.