The Deon Digital Contract Specification Language

Contract Specification Language

At Deon Digital we are working on a domain-specific language for specifying contracts.

In this blog post we will share details about the contract specification language (CSL henceforth) as well as details on how to get a technology preview version of our implementation. As the technology is being actively developed, expect changes in the future.

In future posts we will share more details about our technology and how to use it, so make sure to check back.

A formal language for contracts

A contract is an agreement between multiple parties stating obligations, permissions, and prohibitions of the parties to perform specific actions.

CSL is a domain specific language for specifying contracts using combinators, where larger contracts are formed by combining smaller contracts using various contract combinators.

A contract written in CSL formally denotes a set of traces of events where each event is in accordance with the conditions of the contract.

Here is a simple example contract:

c = <alice> p:Payment where p.amount = 100
    then
    <bob> d:Delivery where d.item = "Bike"

In the contract c defined above:

  1. First alice must perform a Payment event with an amount = 100, and then
  2. bob must perform a Delivery event with an item = "Bike".

No other sequences of actions would be in compliance with the contract. Using the and combinator, one could change the example contract c into a contract where the order of the Payment and Delivery is not important:

c' = <alice> p:Payment where p.amount = 100
     and
     <bob> d:Delivery where d.item = "Bike"

In the contract c':

  • alice must perform a Payment event with an amount = 100, and
  • bob must perform a Delivery event with an item = "Bike".

By saying that c is a contract specification, we mean that a contract is not a program that will perform any of the actions stated in it. Instead, CSL contracts describe only the expected future events.

Having contracts specified in a concise and mathematically precise language is beneficial in terms of communication between people but also allows automation. In particular, contracts can be subject to many kinds of analyses.

A few examples of contract analyses are:

  • Expected value in terms of resources gained or services rendered by participating in the contract.
  • Important deadlines in the contract where a choice should be made.
  • Does a given contract conform to the relevant laws?
  • Does a given trace of events comply with the obligations and permissions in a contract?

The last example mentioned could also be used in an iterative version, where a computer monitors a contract and incoming events for conformance one at a time.

Getting the technology preview

DISCLAIMER: Before using Deon Digital’s technology read our Terms and Conditions provided in the LICENSE file. It is available on the top right in the web app.

We distribute our technology as a Docker image. The image is available on Docker Hub. Simply do docker run to pull and start the image:

$ docker run -p 8080:8080 deondigital/vitznauerstock
 _____                         _____    _         _              _
(____ \                       (____ \  (_)       (_) _          | |
 _   \ \  ____  ___   ____     _   \ \  _   ____  _ | |_   ____ | |
| |   | |/ _  )/ _ \ |  _ \   | |   | || | / _  || ||  _) / _  || |
| |__/ /( (/ /| |_| || | | |  | |__/ / | |( ( | || || |__( ( | || |
|_____/  \____)\___/ |_| |_|  |_____/  |_| \_|| ||_| \___)\_||_||_|
https://deondigital.com                   (_____|
support@deondigital.com

Welcome to the Deon Digital technology preview image!

This container starts a web service and the necessary backend services
to get the Deon Digital technology stack up and running so you can
play around with it.

Go to http://localhost:8080 and start writing tomorrow's contracts
today!
[...]

After the container starts, the demo web app together with the associated web service should be running.

The web app can be accessed by pointing a browser at http://localhost:8080/. Usage of the web app is described at https://deondigital.com/docs/.

Using the webapp

Using the webapp, one can author contracts, instantiate contract templates, apply events to the running system, as well as query the state in various ways. A web service is also available on port 8080. Going to http://localhost:8080/swagger-ui.html#/ shows the Swagger UI presenting the OpenAPI specification for the web service. To make it a bit easier to interact with the web service, we have created a client library (in TypeScript). The client library is available at GitHub.

If you encounter any problems, please do not hesitate to contact us at support@deondigital.com.

Example specifications

As previously mentioned, the guide can be found at https://deondigital.com/docs/.

As a help for authoring contracts, there is also an extension for Visual Studio Code. The extension provides syntax highlighting, parsing, and type checking of CSL. To install it, search for “deon” in the Visual Studio Marketplace or go to https://marketplace.visualstudio.com/items?itemName=deondigital.csl-support.

Below, we give a few example contract specifications.

Full sources of examples are available at GitHub.

Example: Simple Zero-Coupon Bond

A simplified version of a so-called Zero-Coupon Bond, ZCB (investopedia) is a financial contract where an investor gains the right to some amount of money at a specified time in the future.

A very simple CSL contract template that models a ZCB is the following:

template ZCB(buyer, seller, faceValue, currency, maturity) =
  <seller> p: Payment where
    p.timestamp = maturity &&
    p.sender = seller && p.receiver = buyer &&
    expectedAmount p faceValue currency

Where expectedAmount is a function defined elsewhere that checks that a given Payment event specifies a transfer of the expected amount and the expected currency.

An instance of the ZCB contract template above c1 = ZCB(alice, bob, 1000, "USD", 2029-12-12) is a contract where bob is obliged to transfer 1000 USD to alice on 2029-12-12. As is, c1 is not a contract where both parties benefit because only one party stands to gain anything. We can create a new contract template so that it also models the purchase of the ZCB by extending the previous:

template BuyZCB(buyer, seller, discountValue, discountDate, faceValue, currency, maturity) =
  <buyer> p1: Payment where
    p1.sender = buyer &&
    p1.receiver = seller &&
    expectedAmount p1 discountValue currency &&
    p1.timestamp = discountDate
  then
  ZCB(buyer, seller, faceValue, currency, maturity)

An instance of c2 = BuyZCB(alice, bob, 614, 2019-02-15, 1000, "USD", 2029-12-12) is a contract where:

  1.  First alice is obligated to transfer (via Payment) 614 USD to bob on 2019-02-15.
  2. Then bob and alice enter the ZCB and bob is obligated to transfer 1000 USD to alice roughly 10 years later on the 2029-12-12.

The price of 614 USD corresponds to a yearly interest rate of about 5%.

Example: Sales contract

The Sale contract template below is a specification of a simple “delivery versus payment” sales contract between a buyer and seller. The specification allows delivery only after payment has been performed. Payment should occur before the given paymentDeadline. Finally, after delivery, the buyer has the right, but not the obligation, to make a “claim for damages” within 2 days after delivery. At that point the seller may either reimburse the buyer half the amount payed or deny the claim for damages. In case the seller denies the claim, a valid reason must be included. The function validRejectionReason (defined elsewhere) checks that the data submitted in the event corresponds to what would be considered valid reasons for rejecting the claim for damages.

template ClaimForDamages(seller, buyer, price, deliveryTime) =
  let val noticeDeadline = DateTime::addDays deliveryTime 2 in
  <buyer> n:DamageClaim where
    n.timestamp <= noticeDeadline
  then
  let val sellerDeadline = DateTime::addDays n.timestamp 2 in
  <seller> p:Payment where
    let val t = p :> Transfer in
    p.sender = seller && p.receiver buyer &&
    expectedAmount t (price / 2) "USD" &&
    p.timestamp <= sellerDeadline
  or
  <seller> d:DenyClaim where
    d.timestamp <= sellerDeadline &&
    validRejectionReason d

template Sale(seller, buyer, price, unit, qty, goods, paymentDeadline) =
  <buyer> p:Payment where
    p.sender = seller && p.receiver = buyer &&
    correctItem t1 price unit &&
    p.timestamp <= paymentDeadline
  then
  <seller> d:Delivery where
    d.sender = buyer && d.receiver = seller &&
    expectedAmount d qty goods &&
    d.timestamp <= DateTime::addDays p.timestamp 2
  then
  ( ClaimForDamages(seller, buyer, price, d.timestamp)
    or
    success )

References

CSL is based on research done at the University of Copenhagen over several years by several people. A brief list of papers that describe prior work is given below.

  • Contract Formalisation and Modular Implementation of Domain-Specific Languages (Ph.D. Dissertation, pdf)
  • POETS: Process-oriented event-driven transaction systems (doi)
  • Compositional specification of commercial contracts (doi)
  • Composing contracts: an adventure in financial engineering (link)
  • How to write a financial contract (pdf)