Daml: Define Contract Models Compactly

As described in preceding sections, both the integrity and privacy notions depend on a contract model, and such a model must specify:

  1. a set of allowed actions on the contracts, and
  2. the signatories, contract observers, and
  3. an optional agreement text associated with each contract, and
  4. the optional key associated with each contract and its maintainers.

The sets of allowed actions can in general be infinite. For instance, the actions in the IOU contract model considered earlier can be instantiated for an arbitrary obligor and an arbitrary owner. As enumerating all possible actions from an infinite set is infeasible, a more compact way of representing models is needed.

Daml provides exactly that: a compact representation of a contract model. Intuitively, the allowed actions are:

  1. Create actions on all instances of templates such that the template arguments satisfy the ensure clause of the template

  2. Exercise actions on a contract corresponding to choices on that template, with given choice arguments, such that:

    1. The actors match the controllers of the choice. That is, the controllers define the required authorizers of the choice.
    2. The choice observers match the observers annotated in the choice.
    3. The exercise kind matches.
    4. All assertions in the update block hold for the given choice arguments.
    5. Create, exercise, fetch and key statements in the update block are represented as create, exercise and fetch actions and key assertions in the consequences of the exercise action.
  3. Fetch actions on a contract corresponding to a fetch of that instance inside of an update block. The actors must be a non-empty subset of the contract stakeholders. The actors are determined dynamically as follows: if the fetch appears in an update block of a choice ch on a contract c1, and the fetched contract ID resolves to a contract c2, then the actors are defined as the intersection of (1) the signatories of c1 union the controllers of ch with (2) the stakeholders of c2.

    A fetchByKey statement also produces a Fetch action with the actors determined in the same way. A lookupByKey statement that finds a contract also translates into a Fetch action, but all maintainers of the key are the actors.

  4. NoSuchKey assertions corresponding to a lookupByKey update statement for the given key that does not find a contract.

An instance of a Daml template, that is, a Daml contract, is a triple of:

  1. a contract identifier
  2. the template identifier
  3. the template arguments

The signatories of a Daml contract are derived from the template arguments and the explicit signatory annotations on the contract template. The contract observers are those explicitly defined in the template using the observer keyword.

For example, the following template exactly describes the contract model of a simple IOU with a unit amount, shown earlier.

template MustPay with
    obligor : Party
    owner : Party
    signatory obligor, owner
      show obligor <> " must pay " <>
      show owner <> " one unit of value"

template Iou with
    obligor : Party
    owner : Party
    signatory obligor
    observer owner

    choice Transfer
      : ContractId Iou
      with newOwner : Party
      controller owner
      do create Iou with obligor; owner = newOwner

    choice Settle
      : ContractId MustPay
      controller owner
      do create MustPay with obligor; owner

In this example, the owner is specified as an observer, since it must be able to see the contract to exercise the Transfer and Settle choices on it.

The template identifiers of contracts are created through a content-addressing scheme. This means every contract is self-describing in a sense: it constrains its stakeholder annotations and all Daml-conformant actions on itself. As a consequence, one can talk about “the” Daml contract model, as a single contract model encoding all possible instances of all possible templates. This model is subaction-closed; all exercise and create actions done within an update block are also always permissible as top-level actions.