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 successfully completed contract and
the breached contract.

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 four ways to compose contracts:

expecting the occurrence of an event before another contract;
putting two contracts in sequence;
composing two contracts concurrently;
making a choice between two contracts;

We use the contract or template keywords to define names for contracts. These constructs are explained in more detail in these sections:

defining contracts;
wrapping contracts in templates; and
recursive 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 ...
contract 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:

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

success

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

Prefix guards

For more complex contracts, the where clause of a prefix-contract might become quite involved. For example, consider following definitions:

type Receipt {
  gross: Float,
  tax: Float,
  receiver: Agent,
  payee: Agent,
  store: String
}
type StorePayment : Event {
  amount: Float,
  receipt: Maybe Receipt,
  receiver: Agent,
  store: Maybe String
}

To write a contract that

accepts a payment event only if there is a receipt where - the receiver matches the receiver specified on the event - the payee is the agent that submitted the event - the gross plus the tax matches the total amount on the event - the store that got the payment is also the store on the receipt
then allows the receipt to be cleared by the bookkeeper

we end up with

// Just a stub to illustrate the example
contract clearReceipt = \(_: Receipt) -> success

contract acceptPaymentFrom = \(payee: Agent) ->
  <payee> e: StorePayment where
    e.agent = payee &&
    match e.receipt with {
      | (Some receipt : Maybe Receipt) ->
        receipt.gross + receipt.tax = e.amount &&
        receipt.payee = payee &&
        receipt.receiver = e.receiver && (
          match e.store with {
            | Some store -> receipt.store = store
            | None -> False
          }
        )
      | None -> False
    }
  then match e.receipt with {
    | Some receipt -> clearReceipt receipt
    | None -> failure
  }

This where clause is quite unwieldy. Note that one must write a pattern matching expression in the where clause, which continues with a boolean expression in the Some branch. Because store is also a Maybe type, a nested pattern match is required. In the continuation, one must pattern match once again to reveal the receipt, even though it is obvious that this point could only have been reached if there indeed was a receipt.

To aid in such scenarios, the prefix-contract also supports a guard clause, which consists of a list of qualifiers that must match. Syntactically, the guard is introduced by the matching keyword, as such:

<AGENT> x:EVENTTYPE matching { P1 <- E1, ..., Pn <- En } where PREDICATE

Within the guard, there are a comma-separated list of qualifiers. Each qualifier is a pattern, a left-arrow and an expression. To accept an event, all patterns in all qualifiers must match their associated expression. The names bound in the patterns are available in the following where clause, and also in the continuation of the contract. We can now rewrite the above contract using prefix guards:

contract acceptPaymentFrom2 = \(payee: Agent) ->
  <payee> e: StorePayment matching {
    Some receipt <- e.receipt,
    Some store <- e.store
  } where
    e.agent = payee &&
    receipt.gross + receipt.tax = e.amount &&
    receipt.payee = payee &&
    receipt.receiver = e.receiver &&
    receipt.store = store
  then clearReceipt receipt

The end result is both shorter, clearer and more maintainable.

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:

then binds tighter than
and, which binds tighter than
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:

contract alicePays = \alice -> \bob ->
  <alice> p: Payment where p.receiver = bob

contract 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.
contract alicePaysThenBobDelivers = \alice -> \bob ->
   alicePays alice bob then bobDelivers alice bob

// Equivalent formulation:
contract 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 of 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:

contract 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#

contract payBeforeOrAfterChristmas0 = \alice ->
  <alice> p: Payment where p.timestamp <= deadline0 && p.amount = 100
  or
  <alice> p: Payment where p.timestamp > deadline0 && p.amount = 200

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#

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

contract 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 {}

contract optionalChoice = \alice -> \bob -> \charlie ->
    <alice> Option1
    then
    <bob> Action
  or
    <alice> Option2
    then
    <charlie> Action
  or
    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 functions

Contract functions are anonymous functions that, when given an expression as argument, produce a contract. They work analogously to the value-level lambda-functions and are written using similar syntax. A contract function that takes an Int and produces the successful contract is written:

\(x : Int) -> success

Typically, the parameters given to the contract are useful in a where clause, e.g.:

type E : Event { x : Int }
contract onlyAcceptNumber = \x -> <*> e: E where e.x = x

Contract functions are applied using juxtaposition, similarly to value-level functions:

contract onlyAccept42 = onlyAcceptNumber 42

Contract functions can only take 1 parameter, so to specify multiple parameters you nest them:

contract twoParams = \x -> \y -> <*> e: E where e.x = x + y

Alternatively, you can use a tuple and its corresponding pattern to model multiple arguments:

contract tupleParams = \(x, y) -> <*> e: E where e.x = x + y

Just like value-level functions, contract functions can pattern match on their arguments, e.g:

contract successOrFailure =
  \ True -> success
  | False -> success

Direct pattern matching

You can also pattern match directly on values in contract definitions, analogously to value definitions. See the relevant section in the expression reference.

Contract definitions

A contract definition with the name definitionName has the form:

contract [rec] [entrypoint] definitionName = DEFINITIONBODY

This binds the contract DEFINITIONBODY to a contract identifier with the name definitionName. They are distinguished from templates in that it is not possible to specify any contract parameters, but are otherwise identical.

CSL allows local definitions that are only visible within contracts. The syntax for a local contract definition is

// ... inside some contract definition
let
    contract [rec] definitionName1 = DEFINITIONBODY1
    contract [rec] definitionName2 = DEFINITIONBODY2
    ...
    contract [rec] definitionNameN = DEFINITIONBODYN
in
    BODY

Inside BODY we may use definitionName1, definitionName2, …, definitionNameN as contract variables, but they are not visible from the outside. Furthermore, each DEFINITIONBODYi may use the previously defined definitions definitionName1, definitionName2, ..., definitionName(i-1).

You should in general use contract definitions over template definitions unless you need contract parameters.

Entrypoints

Contracts that you intend to use as “entrypoints” by instantiating them from the outside using, e.g., the sic interfaces must be marked with the entrypoint keyword. This adds the following constraints to the contract’s types:

The contract can only have a single parameter.

The contract’s value parameter types must be monomorphic – that is, each of the parameters must have a type that does not contain any type variables.

The contract’s value parameter types must not contain any occurrence of a function type (e.g., Int -> Int).

Warning

CSL currently also supports template entrypoints* of the form template entrypoint Foo x = ... but this is deprecated and will be removed in a future version.

Entrypoints with more or fewer parameters than 1

It’s common to have entrypoints where you want to provide either 0 parameters or more than one. This is easily done. For zero parameters, contract entrypoint t = \() -> ... solves the use case by taking 1 parameter of type Unit, which is the type that has only one value. For more than one parameter, you can specify a tuple parameter as e.g contract entrypoint t = \(x, y, z) -> ....

Together, these restrictions ensure that it’s possible to instantiate the contract externally through, e.g., the REST api. A CSL contract may contain multiple entrypoints. The entrypoint keyword is only available on top-level contracts; local contracts cannot be entrypoints.

Recursive contract definitions

A recursive contract definition with the name contractName has the form

contract rec contractName = CONTRACTBODY

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

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

contract rec contractName-0 = CONTRACTBODY-0
        with contractName-1 = CONTRACTBODY-1
        with ...
        with contractName-n = CONTRACTBODY-n

All contract names contractName-0, …, contractName-n can be used recursively in all bodies CONTRACTBODY-0 … CONTRACTBODY-n. The same restrictions regarding guardedness apply.

Examples

Here is a contrived example of a recursive contract that is also an entrypoint and which performs pattern matching on its integer argument:

type Count : Event { current: Int }
contract rec entrypoint countFrom =
    \ 0 -> success
    | i -> <*> c: Count where c.current = i then countFrom (i - 1)

The countFrom contract will accept a sequence of events counting down from the initial i given at instantiation time.

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 express that part of the contract by itself in a local let-binding and refer to it with the identifier driveCar:

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

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

contract entrypoint drive = \agent ->
  let
    contract driveCar =
      <agent> TurnOnCar then
      <agent> DriveCar then
      <agent> TurnOffCar
    contract borrow = <agent> BorrowCar then driveCar then <agent> ReturnCar
    contract buy = <agent> BuyCar then driveCar
  in borrow or buy

Because the drive contract is marked as entrypoint we can instantiate it from client code (such as the REST api).

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 {}
contract entrypoint house = \agent ->
  let contract 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 contracts locally inside a non-recursive contract 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.

Contract templates

A contract template with the name TemplateName has the form:

template [rec] [c0, ..., cn] [entrypoint] TemplateName p0 ... pm = BODY

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

template [rec] [entrypoint] 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 of 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

Warning

Templates that do not take any contract arguments are completely equivalent to plain contract functions and will be deprecated in future versions of CSL.

Contract parameters

The contract parameters of a template range over any valid type of contract. The following is expressible in CSL:

template [f] Apply x = f x
contract c = Apply[\x -> <*> Event where x = 42] 42

Here, the contract parameter f of Apply is inferred to have the polymorphic contract type a -> b and x to have the value type a. Therefore, in c we can call Apply with any contract lambda as its contract argument, and a will be specialized accordingly when we give the value parameter x. We can see that type inference for contracts works exactly the same as type inference for values.

A typical use case is to define reusable templates that accept some specific events and then continue with a given contract, e.g:

type E : Event { i: Int }
template [f : Int -> Contract] OnlyFactorsOf (factor : Int) =
  <*> e : E where e.i / factor = 0 then f e.i

The template OnlyFactorsOf defines a prefix that will only accept factors of a given integer. Once an event is accepted, the residual contract will be f applied to the accepted integer.

Syntactically, contract parameters are a subset of value patterns which only includes wildcards, variables, and type annotations.

Recursive contract templates

A recursive contract template with the name TemplateName has the form

template rec [entrypoint] TemplateName p0 ... pm = TEMPLATEBODY

where p0, …, pm are value parameters and the keyword entrypoint is optional. Unlike non-recursive contract templates, recursive contract templates are not allowed to have any contract parameters.

You can define mutually recursive contract templates using the same with syntax as applies for contract definitions

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

Recursive contract templates are subject to the same guardnedness condition as recursive contracts.

Warning

Recursive contract templates are equivalent to recursive contract defintions and will be deprecated in future versions of CSL.

Examples

We might often need to express that some contract is 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 [continueWithContract] SignAndContinue agent =
  <agent> Signature then continueWithContract

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 {}
contract 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 ...
contract helloHelloGoodbye = \agent ->
  <agent> SayHello then
  <agent> SayHello then
  (
    <agent> SayGoodbye
    or
    <agent> SayHello
  )

Guardedness

One has to take care that a (mutually) recursive contract 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 definition is unguarded whenever it is possible for it to call itself without first consuming an event. For example, the following recursive contract does nothing but call itself, and so is clearly unguarded:

contract rec unguarded = unguarded

Unguarded recursive contracts are problematic because they can be used to express contracts which have 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 }

contract 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):

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

contract nullable = <*> Count or success
contract 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.