digital-asset/daml
1
1
Fork 0
mirror of https://github.com/digital-asset/daml.git synced 2024-11-10 10:46:11 +03:00
Code Issues Projects Releases Wiki Activity
8582b04861
daml/daml-lf/spec/daml-lf-1.rst
Sofia Faro 8582b04861
ifaces: Add semantics for 'exercise_interface' in the LF spec (#13404) 
* ifaces: Add exercise interface semantics to spec

This is based on the semantics of 'exercise'.

Closes #11349 (for now). Also fixes a small bug in the semantics of 'exercise'.

changelog_begin
changelog_end

* Uniformize exercise syntax
2022-03-25 11:37:43 +00:00

5682 lines
299 KiB
ReStructuredText
Raw Blame History

This file contains ambiguous Unicode characters

This file contains Unicode characters that might be confused with other characters. If you think that this is intentional, you can safely ignore this warning. Use the Escape button to reveal them.

.. Copyright (c) 2022 Digital Asset (Switzerland) GmbH and/or its affiliates. All rights reserved.
.. SPDX-License-Identifier: Apache-2.0
Copyright © 2022, `Digital Asset (Switzerland) GmbH
<https://www.digitalasset.com/>`_ and/or its affiliates. All rights
reserved.
Daml-LF 1 specification
=======================
.. contents:: Contents
Introduction
^^^^^^^^^^^^
This document specifies version 1 of the Daml-LF language — the
language that Daml ledgers execute. Daml compiles to Daml-LF which
executes on Daml ledgers, similar to how Java compiles to JVM byte
code which executes on the JVM. “LF” in Daml-LF stands for “Ledger
Fragment”. Daml-LF is a small, strongly typed, functional language
with strict evaluation that includes native representations for core
Daml concepts such as templates, updates, and parties. It is primarily
intended as a compilation target.
How to view and edit this document
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
To view this document correctly, we recommend you install the `DejaVu
Sans family of fonts <https://dejavu-fonts.github.io/>`_, which is
free (as in freedom) and provide exceptional Unicode coverage. The
sphinx style sheets specify DejaVu Sans Mono as the font to use for
code, and if you want to view/edit this section you should use it
for your editor, too.
If you want to edit this section comfortably, we highly recommend using
either VS Code' ``latex-input`` extension or Emacs' TeX input mode.
In VS Code, you can start typing, say, ``\Gamma`` and the autocompleter
will suggest ``Γ``. Similarly ``\to``, ``\->`` and ``\rightarrow`` will
all lead to ``→``. You might need to explicitly trigger the
autocompleter using ``Ctrl+Space``. All autocompletions are triggered
by (one of) their LaTeX names. You can also trigger autocompletions for
subscripts by typing ``\_1`` for ``₁``, ``\_i`` for ``ᵢ``, etc. We have
have added a couple of extra symbols in
``.vscode/restructuredtext.code-snippets`` file. If you want to add
further symbols that's where they could go.
If you want to use Emacs' TeX input mode, , you can turn it on using ``M-x
set-input-method TeX``, and then you can input symbols as you would in
TeX, mostly using ``\symbol-name`` and ``_letter``. If you don't know
how to input a character, go over it with your cursor and ``M-x
describe-char``. Its TeX code will be listed under ``to input``.
Moreover, add the following to your ``~/.emacs`` to enable additional
symbols used in this doc::
(with-temp-buffer
(activate-input-method "TeX")
(let ((quail-current-package (assoc "TeX" quail-package-alist)))
(quail-defrule "\\limage" ?⦇ nil t)
(quail-defrule "\\rimage" ?⦈ nil t)
(quail-defrule "\\rwave" ?↝ nil t)
(quail-defrule "\\lwave" ?↜ nil t)
(quail-defrule "\\lwbrace" ?⦃ nil t)
(quail-defrule "\\rwbrace" ?⦄ nil t)))
Version history
~~~~~~~~~~~~~~~
The Daml-LF language is versioned using a major and minor component.
Increasing the major component allows us to drop features, change
the semantics of existing features, or update the serialization format.
Changes to the minor component cannot break backward compatibility,
and operate on the same major version of the serialization format in
a backward compatible way. This document describes Daml-LF major version
1, including all its minor versions.
Starting from SDK 1.0 release, Daml-LF versions older than 1.6 are
deprecated. An engine compliant with the present specification must handle
all versions newer than or equal to Daml-LF 1.6, no requirement is made on
handling older version.
Each Daml-LF program is accompanied by the version identifier of the
language it was serialized in. This number enables the Daml-LF engine
to interpret previous versions of the language in a backward
compatibility way.
In the following of this document, we will use annotations between
square brackets such as *[Available in version < x.y]*, *[Available in
versions >= x.y]*, and *[Changed in version x.y]* to emphasize that a
particular feature is concerned with a change introduced in Daml x.y
version. In addition, we will mark lines within inference rules with
annotations of the form ``[Daml-LF < x.y]`` and ``[Daml-LF ≥ x.y]`` to
make the respective line conditional upon the Daml-LF version.
A *preview* version is an snapshot of the next 1.x version to be
released. It is provided for beta testing purpose and may only be
changed to include bug fixes. On the other hand, the *development*
version is a special staging area for the development of upcoming
version 1.x version. It may be used for alpha testing, and can be
changed without notice. Compliant implementations are not required to
implement any features exclusive to development version, but should
take them under advisement as likely elements of the next 1.x version.
Below, we list the versions of Daml-LF 1.x that a Daml-LF engine
compliant with the present specification must handle, in ascending
order. The optional preview version is marked with the tag *(preview)*
while the development version is marked with the tag *(development)*.
Conventionally development version is call 1.dev. The list comes with
a brief description of the changes, and some links to help unfamiliar
readers learn about the features involved in the change. One can
refer also to the `Serialization` section which is particularly
concerned about versioning and backward compatibility.
Support for language versions 1.0 to 1.5 was dropped on 2020-11-30.
This breaking change does not impact ledgers created with SDK 1.0.0 or
later.
Version: 1.6
............
* Introduction date:
2019-07-01
* Description:
+ Initial version
Version: 1.7
............
* Introduction date:
2019-11-07
* Description:
+ **Add** Nat kind and Nat type.
- add `nat` kind
- add `nat` type
+ **Add** parametrically scaled Numeric type.
- add `NUMERIC` primitive type
- add `numeric` primitive literal
- add numeric builtins, namely `ADD_NUMERIC`, `SUB_NUMERIC`,
`MUL_NUMERIC`, `DIV_NUMERIC`, `ROUND_NUMERIC`, `CAST_NUMERIC`,
`SHIFT_NUMERIC`, `LEQ_NUMERIC`, `LESS_NUMERIC`, `GEQ_NUMERIC`,
`GREATER_NUMERIC`, `TEXT_TO_NUMERIC`, `NUMERIC_TO_TEXT`,
`INT64_TO_NUMERIC`, `NUMERIC_TO_INT64`, `EQUAL_NUMERIC`
+ **Drop** support for Decimal type. Use Numeric of scale 10 instead.
- drop `DECIMAL` primitive type
- drop `decimal` primitive literal
- drop decimal builtins, namely `ADD_DECIMAL`, `SUB_DECIMAL`,
`MUL_DECIMAL`, `DIV_DECIMAL`, `ROUND_DECIMAL`, `LEQ_DECIMAL`,
`LESS_DECIMAL`, `GEQ_DECIMAL`, `GREATER_DECIMAL`,
`TEXT_TO_DECIMAL`, `DECIMAL_TO_TEXT`, `INT64_TO_DECIMAL`,
`DECIMAL_TO_INT64`, `EQUAL_DECIMAL`
+ **Add** string interning in external package references.
+ **Add** name interning in external package references.
+ **Add** existential ``Any`` type
- add `'Any'` primitive type
- add `'to_any'` and `'from_any'` expression to convert from/to an
arbitrary ground type (i.e. a type with no free type variables)
to ``Any``.
+ **Add** for Type representation.
- add `'TypeRep'` primitive type
- add `type_rep` expression to reify a arbitrary ground type
(i.e. a type with no free type variables) to a value.
Version: 1.8
............
* Introduction date:
2020-03-02
* Description:
+ **Add** type synonyms.
+ **Add** package metadata.
+ **Rename** structural records from ``Tuple`` to ``Struct``.
+ **Rename** ``Map`` to ``TextMap``.
Version: 1.11
.............
* Introduction date:
2020-12-14
* Description:
+ **Add** generic equality builtin.
+ **Add** generic order builtin.
+ **Add** generic map type ``GenMap``.
+ **Add** ``CONTRACT_ID_TO_TEXT`` builtin.
+ **Add** `exercise_by_key` Update.
+ **Add** choice observers.
Version: 1.12
.............
* Introduction date:
2021-02-24
* Description:
+ Drop type constructor in serialized variant and enumeration
values. Drop type constructor and field names in serialized record
values. See value version 12 in value specification for more
details
Version: 1.13
.............
* Introduction date:
2021-04-06
* Description:
+ **Add** Add BigNumeric support (arbitrary precision decimals).
- add `BigNumeric` primitive type
- add `RoundingMode` primitive type and literals
- add `BigNumeric` builtins
Version: 1.14
.............
* Introduction date:
2021-06-22
* Description:
+ **Add** exception handling.
- Add `AnyException` primitive type
- Add `ToAnyException`, `FromAnyException`, and `Throw` expressions
- Add `TryCatch` update
- Add `ANY_EXCEPTION_MESSAGE` builtin functions,
Version: 1.dev (development)
............................
Abstract syntax
^^^^^^^^^^^^^^^
This section specifies the abstract syntax tree of a Daml-LF
package. We define identifiers, literals, types, expressions, and
definitions.
Notation
~~~~~~~~
Terminals are specified as such::
description:
symbols ∈ regexp -- Unique identifier
Where:
* The ``description`` describes the terminal being defined.
* The ``symbols`` define how we will refer of the terminal in type rules /
operational semantics / ....
* The ``regexp`` is a `Java regular expression
<https://docs.oracle.com/javase/8/docs/api/java/util/regex/Pattern.html>`_
describing the members of the terminal. In particular, we will use
the following conventions:
* ``\xhh`` matches the character with hexadecimal value ``0xhh``.
* ``\n`` matches the carriage return character ``\x0A``,
* ``\r`` matches the carriage return ``\x0D``,
* ``\"`` matches the double quote character ``\x22``.
* ``\$`` match the dollar character ``\x24``.
* ``\.`` matches the full stop character ``\x2e``.
* ``\\`` matches the backslash character ``\x5c``.
* ``\d`` to match a digit: ``[0-9]``.
* The ``Unique identifier`` is a string that uniquely identifies the
non-terminal.
Sometimes the symbol might be the same as the unique identifier, in
the instances where a short symbol is not needed because we do not
mention it very often.
Non-terminals are specified as such::
Description:
symbols
::= non-terminal alternative -- Unique identifier for alternative: description for alternative
| ⋮
Where description and symbols have the same meaning as in the terminal
rules, and:
* each non-terminal alternative is a piece of syntax describing the
alternative;
* each alternative has a unique identifier (think of them as
constructors of a datatype).
Note that the syntax defined by the non-terminals is not intended to
be parseable or non-ambiguous, rather it is intended to be read and
interpreted by humans. However, for the sake of clarity, we enclose
strings that are part of the syntax with single quotes. We do not
enclose symbols such as ``.`` or ``→`` in quotes for the sake of
brevity and readability.
Identifiers
~~~~~~~~~~~
In this section, we define the sorts of strings and identifiers that appear in
Daml-LF programs.
We first define two types of *strings*::
Strings:
Str ::= " " -- Str
| " StrChars "
Sequences of string characters:
StrChars ::= StrChar -- StrChars
| EscapedStrChar
| StrChar StrChars
| EscapedStrChar StrChars
String chars:
StrChar ∈ [^\n\r\"\\] -- StrChar
String character escape sequences:
EscapedStrChar ∈ \\\n|\\\r|\\\"|\\\\ -- EscapedStrChar
*Strings* are possibly empty sequences of legal `Unicode
<https://en.wikipedia.org/wiki/Unicode>`_ code points where the line
feed character ``\n``, the carriage return character ``\r``, the
double quote character ``\"``, and the backslash character ``\\`` must
be escaped with backslash ``\\``. Daml-LF considers legal `Unicode
code point <https://unicode.org/glossary/#code_point>`_ that is not a
`Surrogate Code Point
<https://unicode.org/glossary/#surrogate_code_point>`_, in other words
any code point with an integer value in the range from ``0x000000`` to
``0x00D7FF`` or in the range from ``0x00DFFF`` to ``0x10FFFF`` (bounds
included).
Then, we define the so-called *PackageId strings* and *PartyId
strings*. Those are non-empty strings built with a limited set of
US-ASCII characters (See the rules `PackageIdChar` and `PartyIdChar`
below for the exact sets of characters). We use those string in
instances when we want to avoid empty identifiers, escaping problems,
and other similar pitfalls. ::
PackageId strings
PackageIdString ::= [a-zA-Z0-9\-_ ]{1,64} -- PackageIdString
PartyId strings
PartyIdString ∈ [a-zA-Z0-9:\-_ ]{1,255} -- PartyIdString
PackageName strings
PackageNameString ∈ [a-zA-Z0-9:\-_]+ -- PackageNameString
PackageVersion strings
PackageVersionString ∈ (0|[1-9][0-9]*)(\.(0|[1-9][0-9]*))* – PackageVersionString
We can now define a generic notion of *identifier* and *name*::
identifiers:
Ident ∈ [a-zA-Z_\$][a-zA-Z0-9_\$]{0,999} -- Ident
names:
Name ::= Ident -- Name
| Name \. Ident
Identifiers are standard `Java identifiers
<https://docs.oracle.com/javase/specs/jls/se8/html/jls-3.html#jls-3.8>`_
restricted to US-ASCII with a length of at most 1000 characters.
Names are sequences of identifiers intercalated with dots with a total
length of at most 1000 characters.
The character ``%`` is reserved for external languages built on
Daml-LF as a "not an Ident" notation, so should not be considered for
future addition to allowed identifier characters.
In the following, we will use identifiers to represent *built-in
functions*, term and type *variable names*, record and struct *field
names*, *variant constructors* and *template choices*. On the other
hand, we will use names to represent *type constructors*, *type synonyms*, *value
references*, and *module names*. Finally, we will use PackageId
strings as *package identifiers*. ::
Expression variables
x, y, z ::= Ident -- VarExp
Type variables
α, β ::= Ident -- VarTy
Built-in function names
F ::= Ident -- Builtin
Record and struct field names
f ::= Ident -- Field
Variant data constructors
V ::= Ident -- VariantCon
Enum data constructors
E ::= Ident -- EnumCon
Template choice names
Ch ::= Ident -- ChoiceName
Value references
W ::= Name -- ValRef
Type constructors
T, I ::= Name -- TyCon
Type synonym
S ::= Name -- TySyn
Module names
ModName ::= Name -- ModName
Package identifiers
pid ::= PackageIdString -- PkgId
Package names
pname ::= PackageNameString -- PackageName
Package versions
pversion ::= PackageVersionString -- PackageVersion
V0 Contract identifiers:
cidV0 ∈ #[a-zA-Z0-9\._:-#/ ]{0,254} -- V0ContractId
V1 Contract identifiers:
cidV1 ∈ 00([0-9a-f][0-9a-f]){32,126} -- V1ContractId
Contract identifiers can be created dynamically through interactions
with the underlying ledger. See the `operation semantics of update
statements <Update Interpretation_>`_ for the formal specification of
those interactions. Depending on its configuration, a Daml-LF engine
can produce V0 or V1 contract identifiers. When configured to produce
V0 contract identifiers, a Daml-LF compliant engine must refuse to
load any Daml-LF >= 1.11 archives. On the contrary, when configured
to produce V1 contract IDs, a Daml-LF compliant engine must accept to
load any non-deprecated Daml-LF version. V1 Contract IDs allocation
scheme is described in the `V1 Contract ID allocation scheme
specification <./contract-id.rst>`_. In the following we will say that
a V1 contract identifier is *non-suffixed* if it is built from exactly
66 characters. Otherwise (meaning it has between 68 and 254 characters) we
will say it is *suffixed*.
Literals
~~~~~~~~
We now define all the literals that a program can handle::
Nat type literals: -- LitNatType
n ∈ \d+
64-bit integer literals:
LitInt64 ∈ (-?)\d+ -- LitInt64
Numeric literals:
LitNumeric ∈ ([+-]?)([1-9]\d+|0).\d* -- LitNumeric
Date literals:
LitDate ∈ \d{4}-\d{2}-\d{2} -- LitDate
UTC timestamp literals:
LitTimestamp ∈ \d{4}-\d{2}-\d{2}T\d{2}:\d{2}:\d{2}(.\d{1,3})?Z
-- LitTimestamp
UTF8 string literals:
t ::= Str -- LitText
Party literals:
LitParty ::= PartyIdString -- LitParty
Contract ID literals:
cid ::= cidV0 | cidV1 -- LitCid
Rounding Mode Literals: -- LitRoundingMode
LitRoundingMode ::=
| ROUNDING_UP
| ROUNDING_DOWN
| ROUNDING_CEILING
| ROUNDING_FLOOR
| ROUNDING_HALF_UP
| ROUNDING_HALF_DOWN
| ROUNDING_HALF_EVEN
| ROUNDING_UNNECESSARY
The literals represent actual Daml-LF values:
* A ``LitNatType`` represents a natural number between ``0`` and
``38``, bounds inclusive.
* A ``LitInt64`` represents a standard signed 64-bit integer (integer
between ``−2⁶³`` to ``2⁶³−1``).
* A decimal numbers is a signed number that can be represented as a
product `i * 10⁻ˢ` where `i` (the *unscaled value* of the number) is
a signed integer without trailing zeros and `s` (the *scale* of the
number) is a signed integer. The *precision* of a decimal numbers if
the number of digits of its unscaled value (ignoring possible
leading zeros). By convention the scale and the precision of zero
are 0. Daml-LF distinguishes two kinds of decimal numbers:
+ A ``LitNumeric`` represents those decimal numbers that have a
precision of at most 38 and a scale between ``0`` and ``37``
(bounds inclusive).
+ A ``LitBigNumeric`` represents those decimal numbers that have at
most 2¹⁵ significant digits at the right and the left of the
decimal point. Equivalently those are decimal numbers that respect
`scale ≤ 2¹⁵` and `precision - scale < 2¹⁵`.
* A ``LitDate`` represents the number of day since
``1970-01-01`` with allowed range from ``0001-01-01`` to
``9999-12-31`` and using a year-month-day format.
* A ``LitTimestamp`` represents the number of microseconds
since ``1970-01-01T00:00:00.000000Z`` with allowed range
``0001-01-01T00:00:00.000000Z`` to ``9999-12-31T23:59:59.999999Z``
using a
year-month-day-hour-minute-second-microsecond
format.
* A ``LitText`` represents a `UTF8 string
<https://en.wikipedia.org/wiki/UTF-8>`_.
* A ``LitParty`` represents a *party*.
* A ``LitRoundingMode`` represents a *rounding mode* used by numerical
operations.
.. note:: A literal which is not backed by an actual value is not
valid and is implicitly rejected by the syntax presented here.
For instance, the literal ``9223372036854775808`` is not a valid
``LitInt64`` since it cannot be encoded as a signed 64-bits
integer, i.e. it equals ``2⁶³``. Similarly,``2019-13-28`` is not a
valid ``LitDate`` because there are only 12 months in a year.
Number-like literals (``LitNatTyp``, ``LitInt64``, ``LitNumeric``,
``LitBigNumeric``, ``LitDate``, ``LitTimestamp``) are ordered by
natural ordering. Text-like literals (``LitText``, ``LitParty``, and
``Contract ID``) are ordered lexicographically. Note that in the ASCII
encoding, the character ``#`` comes before digits, meaning V0 Contract
ID are ordered before V1 Contract ID. In the following we will denote
the corresponding (non-strict) order by ``≤ₗ``. RoundingMode literals
are ordered as they appear in the definition of ``LitRoundingMode``,
e.g. ``ROUNDING_UP`` and ``ROUNDING_UNNECESSARY`` are the smallest and
greatest rounding mode.
Kinds, types, and expressions
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
.. TODO We might want to consider changing the syntax for ``Mod``,
since in our software we use the colon to separate the module name
from the definition name inside the module.
Then we can define our kinds, types, and expressions::
Kinds
k
::= 'nat' -- KindNat [Daml-LF ≥ 1.7]
| ek -- KindErasable
Erasable Kind
ek
::= ⋆ -- KindStar
| k → ek -- KindArrow
Module references
Mod
::= PkdId:ModName -- ModPackage: module from a package
Built-in types
BuiltinType
::= 'TArrow' -- BTArrow: Arrow type
| 'Int64' -- BTyInt64: 64-bit integer
| 'Numeric' -- BTyNumeric: numeric, precision 38, parametric scale between 0 and 37
| 'BigNumeric' -- BTyBigNumeric: arbitrary precision decimal
| 'RoundingMode' -- BTyRoundingMode: rounding mode to control BigNumeric operations.
| 'Text' -- BTyText: UTF-8 string
| 'Date' -- BTyDate
| 'Timestamp' -- BTyTime: UTC timestamp
| 'Party' -- BTyParty
| 'Date' -- BTyDate: year, month, date triple
| 'Unit' -- BTyUnit
| 'Bool' -- BTyBool
| 'List' -- BTyList
| 'Optional' -- BTyOptional
| 'TextMap' -- BTTextMap: map with string keys
| 'GenMap' -- BTGenMap: map with general value keys [Daml-LF ≥ 1.11]
| 'ContractId' -- BTyContractId
| 'Any' -- BTyAny [Daml-LF ≥ 1.7]
| 'TypeRep' -- BTTypeRep [Daml-LF ≥ 1.7]
| 'Update' -- BTyUpdate
| 'Scenario' -- BTyScenario
| 'AnyException' -- BTyAnyException [Daml-LF ≥ 1.14]
Types (mnemonic: tau for type)
τ, σ
::= α -- TyVar: Type variable
| n -- TyNat: Nat Type [Daml-LF ≥ 1.7]
| τ σ -- TyApp: Type application
| ∀ α : k . τ -- TyForall: Universal quantification
| BuiltinType -- TyBuiltin: Builtin type
| Mod:T -- TyCon: type constructor
| |Mod:S τ₁ … τₘ| -- TySyn: type synonym [Daml-LF ≥ 1.8]
| ⟨ f₁: τ₁, …, fₘ: τₘ ⟩ -- TyStruct: Structural record type
Expressions
e ::= x -- ExpVar: Local variable
| e₁ e₂ -- ExpApp: Application
| e @τ -- ExpTyApp: Type application
| λ x : τ . e -- ExpAbs: Abstraction
| Λ α : k . e -- ExpTyAbs: Type abstraction
| 'let' x : τ = e₁ 'in' e₂ -- ExpLet: Let
| 'case' e 'of' p₁ → e₁ '|' … '|' pₙ → eₙ -- ExpCase: Pattern matching
| () -- ExpUnit
| 'True' -- ExpTrue
| 'False' -- ExpFalse
| LitInt64 -- ExpLitInt64: 64-bit integer literal
| LitNumeric -- ExpLitNumeric: Numeric literal
| LitBigNumeric -- ExpLitBigNumeric: BigNumeric literal
| t -- ExpLitText: UTF-8 string literal
| LitDate -- ExpLitDate: Date literal
| LitTimestamp -- ExpLitTimestamp: UTC timestamp literal
| LitParty -- ExpLitParty: Party literal
| cid -- ExpLitContractId: Contract identifiers
| LitRoundingMode -- ExpLitRoundingMode: Rounding Mode
| F -- ExpBuiltin: Builtin function
| Mod:W -- ExpVal: Defined value
| Mod:T @τ₁ … @τₙ { f₁ = e₁, …, fₘ = eₘ } -- ExpRecCon: Record construction
| Mod:T @τ₁ … @τₙ {f} e -- ExpRecProj: Record projection
| Mod:T @τ₁ … @τₙ { e₁ 'with' f = e₂ } -- ExpRecUpdate: Record update
| Mod:T:V @τ₁ … @τₙ e -- ExpVariantCon: Variant construction
| Mod:T:E -- ExpEnumCon:Enum construction
| ⟨ f₁ = e₁, …, fₘ = eₘ ⟩ -- ExpStructCon: Struct construction
| e.f -- ExpStructProj: Struct projection
| ⟨ e₁ 'with' f = e₂ ⟩ -- ExpStructUpdate: Struct update
| 'Nil' @τ -- ExpListNil: Empty list
| 'Cons' @τ e₁ e₂ -- ExpListCons: Cons list
| 'None' @τ -- ExpOptionalNone: Empty Optional
| 'Some' @τ e -- ExpOptionalSome: Non-empty Optional
| [t₁ ↦ e₁; …; tₙ ↦ eₙ] -- ExpTextMap
| 〚e₁ ↦ e₁; …; eₙ ↦ eₙ'〛 -- ExpGenMap [Daml-LF ≥ 1.11]
| 'to_any' @τ e -- ExpToAny: Wrap a value of the given type in Any [Daml-LF ≥ 1.7]
| 'from_any' @τ e -- ExpToAny: Extract a value of the given from Any or return None [Daml-LF ≥ 1.7]
| 'type_rep' @τ -- ExpToTypeRep: A type representation [Daml-LF ≥ 1.7]
| u -- ExpUpdate: Update expression
| s -- ExpScenario: Scenario expression
| 'throw' @σ @τ e -- ExpThrow: throw exception [Daml-LF ≥ 1.14]
| 'to_any_exception' @τ e -- ExpToAnyException: Turn a concrete exception into an 'AnyException' [Daml-LF ≥ 1.14]
| 'from_any_exception' @τ e -- ExpFromAnyException: Extract a concrete exception from an 'AnyException' [Daml-LF ≥ 1.14]
| 'to_interface' @τ₁ @τ₂ e -- ExpToInterface: Turn a template value into an interface value [Daml-LF ≥ 1.dev]
| 'from_interface' @τ₁ @τ₂ e -- ExpFromInterface: Turn an interface value back into a template value (returns optional) [Daml-LF ≥ 1.dev]
| 'unsafe_from_interface' @τ₁ @τ₂ e₁ e₂ -- ExpUnsafeFromInterface: Turn an interface value back into a template value (throws fatal error) [Daml-LF ≥ 1.dev]
| 'call_interface' @τ f e -- ExpCallInterface: Call a method on an interface value [Daml-LF ≥ 1.dev]
| 'to_required_interface' @τ₁ @τ₂ e -- ExpToRequiredInterface: Upcast an interface value to an interface it requires [Daml-LF ≥ 1.dev]
| 'from_required_interface' @τ₁ @τ₂ e -- ExpFromRequiredInterface: Downcast an interface value to an interface that requires it (returns optional) [Daml-LF ≥ 1.dev]
| 'unsafe_from_required_interface' @τ₁ @τ₂ e₁ e₂ -- ExpUnsafeFromRequiredInterface: Downcast an interface value to an interface that requires it (throws fatal error) [Daml-LF ≥ 1.dev]
| 'interface_typerep' @τ e -- ExpInterfaceTyperep: Get the typerep associated with the template inside the interface value [Daml-LF ≥ 1.dev]
| 'interface_signatory' @τ e -- ExpInterfaceSignatory: Get the signatories of the template inside the interface value [Daml-LF ≥ 1.dev]
| 'interface_observer' @τ e -- ExpInterfaceObserver: Get the observers of the template inside the interface value [Daml-LF ≥ 1.dev]
Patterns
p
::= Mod:T:V x -- PatternVariant
| Mod:T:E -- PatternEnum
| 'Nil' -- PatternNil
| 'Cons' xₕ xₜ -- PatternCons
| 'None' -- PatternNone
| 'Some' x -- PatternSome
| 'True' -- PatternTrue
| 'False' -- PatternFalse
| () -- PatternUnit
| _ -- PatternDefault
Updates
u ::= 'pure' @τ e -- UpdatePure
| 'bind' x₁ : τ₁ ← e₁ 'in' e₂ -- UpdateBlock
| 'create' @Mod:T e -- UpdateCreate
| 'create_interface' @Mod:I e -- UpdateCreateInterface [Daml-LF ≥ 1.dev]
| 'fetch' @Mod:T e -- UpdateFetch
| 'fetch_interface' @Mod:I e -- UpdateFetchInterface [Daml-LF ≥ 1.dev]
| 'exercise' @Mod:T Ch e₁ e₂ -- UpdateExercise
| 'exercise_by_key' @Mod:T Ch e₁ e₂ -- UpdateExerciseByKey [Daml-LF ≥ 1.11]
| 'exercise_interface' @Mod:I Ch e₁ e₂ e₃ -- UpdateExerciseInterface [Daml-LF ≥ 1.dev]
| 'get_time' -- UpdateGetTime
| 'fetch_by_key' @τ e -- UpdateFecthByKey
| 'lookup_by_key' @τ e -- UpdateLookUpByKey
| 'embed_expr' @τ e -- UpdateEmbedExpr
| 'try' @τ e₁ 'catch' x. e₂ -- UpdateTryCatch [Daml-LF ≥ 1.14]
Scenario
s ::= 'spure' @τ e -- ScenarioPure
| 'sbind' x₁ : τ₁ ← e₁ 'in' e₂ -- ScenarioBlock
| 'commit' @τ e u -- ScenarioCommit
| 'must_fail_at' @τ e u -- ScenarioMustFailAt
| 'pass' e -- ScenarioPass
| 'sget_time' -- ScenarioGetTime
| 'sget_party' e -- ScenarioGetParty
| 'sembed_expr' @τ e -- ScenarioEmbedExpr
.. note:: The explicit syntax for maps (cases ``ExpTextMap`` and
``ExpGenMap``) is forbidden in serialized programs. It is specified
here to ease the definition of `values`_, `operational semantics`_
and `value comparison <Generic comparison functions_>`_. In practice,
`text map functions`_ and `generic map functions`_ are the only way
to create and handle those objects.
.. note:: The order of entries in maps (cases ``ExpTextMap`` and
``ExpGenMap``) is always significant. For text maps, the entries
should be always ordered by keys. On the other hand, the order of
entries in generic maps indicate the order in which the keys have
been inserted into the map.
.. note:: The distinction between kinds and erasable kinds is significant,
because erasable kinds have no runtime representation. This affects the
operational semantics. The right hand side of an arrow is always erasable.
.. note:: The explicit syntax for BigNumeric literal (case
``ExpLitBigNumeric``) is forbidden in serialized programs. It is
specified here to ease the definition of `values`_, `operational
semantics`_ and `value comparison <Generic comparison
functions_>`_. In practice, `BigNumeric functions`_ are the only way
to create and handle those objects.
In the following, we will use ``τ₁ → τ₂`` as syntactic sugar for the
type application ``('TArrow' τ₁ τ₂)`` where ``τ₁`` and ``τ₂`` are
types.
Definitions
~~~~~~~~~~~
Expressions and types contain references to definitions in packages
available for usage::
Template choice kind
ChKind
::= 'consuming' -- ChKindConsuming
| 'non-consuming' -- ChKindNonConsuming
Template key definition
KeyDef
::= 'no_key'
| 'key' τ eₖ eₘ
Template choice definition
ChDef ::= 'choice' ChKind Ch (y : 'ContractId' Mod:T) (z : τ) : σ 'by' eₚ 'observers' eₒ ↦ e
-- ChDef
Interface implementation definition
ImplDef ::= 'implements' Mod:I -- ImplDef [Daml-LF ≥ 1.dev]
{ 'methods { f₁ = e₁, …, fₙ = eₙ }
, 'choices' { Ch₁, …, Chₘ }
}
Definitions
Def
::=
| 'record' T (α₁: k₁)… (αₙ: kₙ) ↦ { f₁ : τ₁, …, fₘ : τₘ }
-- DefRecord: Nominal record type
| 'variant' T (α₁: k₁)… (αₙ: kₙ) ↦ V₁ : τ₁ | … | Vₘ : τₘ
-- DefVariant
| 'enum' T ↦ E₁ | … | Eₘ -- DefEnum
| 'synonym' S (α₁: k₁)… (αₙ: kₙ) ↦ τ -- DefTypeSynonym
| 'val' W : τ ↦ e -- DefValue
| 'tpl' (x : T) ↦ -- DefTemplate
{ 'precondition' e₁
, 'signatories' e₂
, 'observers' e₃
, 'agreement' e₄
, 'choices' { ChDef₁, …, ChDefₘ }
, KeyDef
, ImplDef₁, …, ImplDefₖ
}
| 'exception' T ↦ { 'message' e } -- DefException [Daml-LF ≥ 1.14]
| 'interface' (x : I) ↦ -- DefInterface [Daml-LF ≥ 1.dev]
{ 'requires' { Mod₁:I₁, …, Modₖ:Iₖ }
, 'precondition' e
, 'methods' { f₁ : τ₁, …, fₙ : τₙ }
, 'choices' { ChDef₁, …, ChDefₘ }
}
Module (mnemonic: delta for definitions)
Δ ::= ε -- DefCtxEmpty
| Def · Δ -- DefCtxCons
PackageMetadata
PackageMetadata ::= 'metadata' PackageNameString PackageVersionString -- PackageMetadata
PackageModules
PackageModules ∈ ModName ↦ Δ -- PackageModules
Package
Package ::= Package PackageModules PackageMetadata – since Daml-LF 1.8
Package ::= Package PackageModules -- until Daml-LF 1.8
Package collection
Ξ ∈ pid ↦ Package -- Packages
Feature flags
~~~~~~~~~~~~~
Modules are annotated with a set of feature flags. Those flags enables
syntactical restrictions and semantics changes on the annotated
module. The following feature flags are available:
+-------------------------------------------+----------------------------------------------------------+
| Flag | Semantic meaning |
+===========================================+==========================================================+
| ForbidPartyLiterals | Party literals are not allowed in a Daml-LF module. |
| | (See `Party Literal restriction`_ for more details) |
+-------------------------------------------+----------------------------------------------------------+
| DontDivulgeContractIdsInCreateArguments | contract IDs captured in ``create`` arguments are not |
| | divulged, ``fetch`` is authorized if and only if the |
| | authorizing parties contain at least one stakeholder of |
| | the fetched contract ID. |
| | The contract ID on which a choice is exercised |
| | is divulged to all parties that witness the choice. |
+-------------------------------------------+----------------------------------------------------------+
| DontDiscloseNonConsumingChoicesToObservers| When a non-consuming choice of a contract is exercised, |
| | the resulting sub-transaction is not disclosed to the |
| | observers of the contract. |
+-------------------------------------------+----------------------------------------------------------+
Well-formed programs
^^^^^^^^^^^^^^^^^^^^
The section describes the type system of language and introduces some
other restrictions over programs that are statically verified at
loading.
Type system
~~~~~~~~~~~
In all the type checking rules, we will carry around the packages
available for usage ``Ξ``. Given a module reference ``Mod`` equals to
``('Package' pid ModName)``, we will denote the corresponding
definitions as ``〚Ξ〛Mod`` where ``ModName`` is looked up in package
``Ξ(pid)``;
Expressions do also contain references to built-in functions. Any
built-in function ``F`` comes with a fixed type, which we will denote
as ``𝕋(F)``. See the `Built-in functions`_ section for the complete
list of built-in functions and their respective types.
Type normalization
..................
First, we define the type normalization relation ``↠`` over types,
which inlines type synonym definitions, and normalizes struct types
to remove dependence on the order of fields ::
——————————————————————————————————————————————— RewriteVar
α ↠ α
——————————————————————————————————————————————— RewriteNat
n ↠ n
——————————————————————————————————————————————— RewriteBuiltin
BuiltinType ↠ BuiltinType
———————————————————————————————————————————————— RewriteTyCon
Mod:T ↠ Mod:T
'synonym' S (α₁:k₁) … (αₙ:kₙ) ↦ τ ∈ 〚Ξ〛Mod
τ ↠ σ τ₁ ↠ σ₁ ⋯ τₙ ↠ σₙ
——————————————————————————————————————————————— RewriteSynonym
|Mod:S τ₁ … τₙ| ↠ σ[α₁ ↦ σ₁, …, αₙ ↦ σₙ]
τ₁ ↠ σ₁ ⋯ τₙ ↠ σₙ
[f₁, …, fₘ] sorts lexicographically to [fⱼ₁, …, fⱼₘ]
———————————————————————————————————————————————— RewriteStruct
⟨ f₁: τ₁, …, fₘ: τₘ ⟩ ↠ ⟨ fⱼ₁: σⱼ₁, …, fⱼₘ: σⱼₘ ⟩
τ₁ ↠ σ₁ τ₂ ↠ σ₂
———————————————————————————————————————————————— RewriteApp
τ₁ τ₂ ↠ σ₁ σ₂
τ ↠ σ
———————————————————————————————————————————————— RewriteForall
∀ α : k . τ ↠ ∀ α : k . σ
Note that the relation ``↠`` defines a partial normalization function
over types as soon as:
1. there is at most one definition for a type synonym ``S`` in each
module
2. there is no cycles between type synonym definitions.
These two properties will be enforced by the notion of
`well-formedness <Well-formed packages_>`_ defined below.
Note ``↠`` is undefined on type contains an undefined type synonym or
a type synonym applied to a wrong number. Such types are assumed non
well-formed and will be rejected by the Daml-LF type checker.
Well-formed types
.................
We now formally define *well-formed types*. ::
Type context:
Γ ::= ε -- CtxEmpty
| α : k · Γ -- CtxVarTyKind
| x : τ · Γ -- CtxVarExpType
┌───────────────┐
Well-formed types │ Γ ⊢ τ : k │
└───────────────┘
α : k ∈ Γ
————————————————————————————————————————————— TyVar
Γ ⊢ α : k
————————————————————————————————————————————— TyNat
Γ ⊢ n : 'nat'
Γ ⊢ τ : k₁ → k₂ Γ ⊢ σ : k₁
————————————————————————————————————————————— TyApp
Γ ⊢ τ σ : k₂
α : k · Γ ⊢ τ : ⋆
————————————————————————————————————————————— TyForall
Γ ⊢ ∀ α : k . τ : ⋆
————————————————————————————————————————————— TyArrow
Γ ⊢ 'TArrow' : ⋆ → ⋆ → ⋆
————————————————————————————————————————————— TyUnit
Γ ⊢ 'Unit' : ⋆
————————————————————————————————————————————— TyBool
Γ ⊢ 'Bool' : ⋆
————————————————————————————————————————————— TyInt64
Γ ⊢ 'Int64' : ⋆
————————————————————————————————————————————— TyNumeric
Γ ⊢ 'Numeric' : 'nat' → ⋆
————————————————————————————————————————————— TyBigNumeric
Γ ⊢ 'BigNumeric' : ⋆
————————————————————————————————————————————— TyRoundingMode
Γ ⊢ 'RoundingMode' : ⋆
————————————————————————————————————————————— TyText
Γ ⊢ 'Text' : ⋆
————————————————————————————————————————————— TyDate
Γ ⊢ 'Date' : ⋆
————————————————————————————————————————————— TyTimestamp
Γ ⊢ 'Timestamp' : ⋆
————————————————————————————————————————————— TyParty
Γ ⊢ 'Party' : ⋆
————————————————————————————————————————————— TyList
Γ ⊢ 'List' : ⋆ → ⋆
————————————————————————————————————————————— TyOptional
Γ ⊢ 'Optional' : ⋆ → ⋆
————————————————————————————————————————————— TyTextMap
Γ ⊢ 'TextMap' : ⋆ → ⋆
————————————————————————————————————————————— TyGenMap
Γ ⊢ 'GenMap' : ⋆ → ⋆ → ⋆
————————————————————————————————————————————— TyContractId
Γ ⊢ 'ContractId' : ⋆ → ⋆
————————————————————————————————————————————— TyAny
Γ ⊢ 'Any' : ⋆
————————————————————————————————————————————— TyTypeRep
Γ ⊢ 'TypeRep' : ⋆
'record' T (α₁:k₁) … (αₙ:kₙ) ↦ … ∈ 〚Ξ〛Mod
————————————————————————————————————————————— TyRecordCon
Γ ⊢ Mod:T : k₁ → … → kₙ → ⋆
'variant' T (α₁:k₁) … (αₙ:kₙ) ↦ … ∈ 〚Ξ〛Mod
————————————————————————————————————————————— TyVariantCon
Γ ⊢ Mod:T : k₁ → … → kₙ → ⋆
'enum' T ↦ … ∈ 〚Ξ〛Mod
————————————————————————————————————————————— TyEnumCon
Γ ⊢ Mod:T : ⋆
'interface' (x : I) ↦ … ∈ 〚Ξ〛Mod
————————————————————————————————————————————— TyInterfaceCon
Γ ⊢ Mod:I : ⋆
Γ ⊢ τ₁ : ⋆ … Γ ⊢ τₙ : ⋆
f₁ < … < fₙ lexicographically
————————————————————————————————————————————— TyStruct
Γ ⊢ ⟨ f₁: τ₁, …, fₙ: τₙ ⟩ : ⋆
————————————————————————————————————————————— TyUpdate
Γ ⊢ 'Update' : ⋆ → ⋆
————————————————————————————————————————————— TyScenario
Γ ⊢ 'Scenario' : ⋆ → ⋆
————————————————————————————————————————————— TyAnyException [Daml-LF ≥ 1.14]
Γ ⊢ 'AnyException' : ⋆
Exception types
...............
To state the typing rules related to exception handling, we need the notion of
*exception types*. As the name suggests, values of these types are the ones that
can be thrown and caught by the exception handling mechanism. ::
┌────────┐
Exception types │ ⊢ₑ τ │
└────────┘
'exception' T ↦ … ∈ 〚Ξ〛Mod
———————————————————————————————————————————————————————————————— ExnTyDefException
⊢ₑ Mod:T
Note that ``'AnyException'`` is not an exception type in order to avoid having
``'AnyException'`` wrapped into ``'AnyException'``.
Well-formed expression
......................
Then we define *well-formed expressions*. ::
┌───────────────┐
Well-formed expressions │ Γ ⊢ e : τ │
└───────────────┘
x : τ ∈ Γ
——————————————————————————————————————————————————————————————— ExpDefVar
Γ ⊢ x : τ
Γ ⊢ e₁ : τ₁ → τ₂ Γ ⊢ e₂ : τ₁
——————————————————————————————————————————————————————————————— ExpApp
Γ ⊢ e₁ e₂ : τ₂
τ ↠ τ' Γ ⊢ τ' : k Γ ⊢ e : ∀ α : k . σ
——————————————————————————————————————————————————————————————— ExpTyApp
Γ ⊢ e @τ : σ[α ↦ τ']
τ ↠ τ' x : τ' · Γ ⊢ e : σ Γ ⊢ τ' : ⋆
——————————————————————————————————————————————————————————————— ExpAbs
Γ ⊢ λ x : τ . e : τ' → σ
α : k · Γ ⊢ e : τ
——————————————————————————————————————————————————————————————— ExpTyAbs
Γ ⊢ Λ α : k . e : ∀ α : k . τ
τ ↠ τ' Γ ⊢ e₁ : τ' Γ ⊢ τ' : ⋆
x : τ' · Γ ⊢ e₂ : σ
——————————————————————————————————————————————————————————————— ExpLet
Γ ⊢ 'let' x : τ = e₁ 'in' e₂ : σ
——————————————————————————————————————————————————————————————— ExpUnit
Γ ⊢ () : 'Unit'
——————————————————————————————————————————————————————————————— ExpTrue
Γ ⊢ 'True' : 'Bool'
——————————————————————————————————————————————————————————————— ExpFalse
Γ ⊢ 'False' : 'Bool'
τ ↠ τ' Γ ⊢ τ' : ⋆
——————————————————————————————————————————————————————————————— ExpListNil
Γ ⊢ 'Nil' @τ : 'List' τ'
τ ↠ τ'
Γ ⊢ τ' : ⋆ Γ ⊢ eₕ : τ' Γ ⊢ eₜ : 'List' τ'
——————————————————————————————————————————————————————————————— ExpListCons
Γ ⊢ 'Cons' @τ eₕ eₜ : 'List' τ'
τ ↠ τ' Γ ⊢ τ' : ⋆
—————————————————————————————————————————————————————————————— ExpOptionalNone
Γ ⊢ 'None' @τ : 'Optional' τ'
τ ↠ τ' Γ ⊢ τ' : ⋆ Γ ⊢ e : τ'
——————————————————————————————————————————————————————————————— ExpOptionalSome
Γ ⊢ 'Some' @τ e : 'Optional' τ'
∀ i,j ∈ 1, …, n i > j ∨ tᵢ ≤ tⱼ
Γ ⊢ e₁ : τ Γ ⊢ eₙ : τ
——————————————————————————————————————————————————————————————— ExpTextMap
Γ ⊢ [t₁ ↦ e₁; …; tₙ ↦ eₙ] : 'TextMap' τ
Γ ⊢ e₁ : σ Γ ⊢ eₙ : σ
Γ ⊢ e₁' : τ Γ ⊢ eₙ' : τ
——————————————————————————————————————————————————————————————— ExpGenMap (*)
Γ ⊢ 〚e₁ ↦ e₁'; …; eₙ ↦ eₙ'〛: GenMap σ τ
τ contains no quantifiers and no type synonyms
ε ⊢ τ : ⋆ Γ ⊢ e : τ
——————————————————————————————————————————————————————————————— ExpToAny
Γ ⊢ 'to_any' @τ e : 'Any'
τ contains no quantifiers and no type synonyms
ε ⊢ τ : ⋆ Γ ⊢ e : 'Any'
——————————————————————————————————————————————————————————————— ExpFromAny
Γ ⊢ 'from_any' @τ e : 'Optional' τ
τ contains no quantifiers and no type synonyms
ε ⊢ τ : ⋆
——————————————————————————————————————————————————————————————— ExpTypeRep
Γ ⊢ 'type_rep' @τ : 'TypeRep'
——————————————————————————————————————————————————————————————— ExpBuiltin
Γ ⊢ F : 𝕋(F)
——————————————————————————————————————————————————————————————— ExpLitInt64
Γ ⊢ LitInt64 : 'Int64'
n = scale(LitNumeric)
——————————————————————————————————————————————————————————————— ExpLitNumeric
Γ ⊢ LitNumeric : 'Numeric' n
——————————————————————————————————————————————————————————————— ExpBigNumeric
Γ ⊢ LitBigNumeric : 'BigNumeric'
——————————————————————————————————————————————————————————————— ExpLitText
Γ ⊢ t : 'Text'
——————————————————————————————————————————————————————————————— ExpLitDate
Γ ⊢ LitDate : 'Date'
——————————————————————————————————————————————————————————————— ExpLitTimestamp
Γ ⊢ LitTimestamp : 'Timestamp'
——————————————————————————————————————————————————————————————— ExpLitParty
Γ ⊢ LitParty : 'Party'
'tpl' (x : T) ↦ { … } ∈ 〚Ξ〛Mod
——————————————————————————————————————————————————————————————— ExpLitContractId
Γ ⊢ cid : 'ContractId' Mod:T
——————————————————————————————————————————————————————————————— ExpLitRoundingMode
Γ ⊢ LitRoundingMode : 'RoundingMode'
τ ↠ τ' 'val' W : τ ↦ … ∈ 〚Ξ〛Mod
——————————————————————————————————————————————————————————————— ExpVal
Γ ⊢ Mod:W : τ'
'record' T (α₁:k₁) … (αₙ:kₙ) ↦ { f₁:τ₁, …, fₘ:τₘ } ∈ 〚Ξ〛Mod
σ₁ ↠ σ₁' ⋯ σₙ ↠ σₙ'
Γ ⊢ σ₁' : k₁ ⋯ Γ ⊢ σₙ' : kₙ
τ₁ ↠ τ₁' Γ ⊢ e₁ : τ₁'[α₁ ↦ σ₁', …, αₙ ↦ σₙ']
⋮
τₘ ↠ τₘ' Γ ⊢ eₘ : τₘ'[α₁ ↦ σ₁', …, αₙ ↦ σₙ']
———————————————————————————————————————————————————————————————— ExpRecCon
Γ ⊢
Mod:T @σ₁ … @σₙ { f₁ = e₁, …, fₘ = eₘ } : Mod:T σ₁' … σₙ'
'record' T (α₁:k₁) … (αₙ:kₙ) ↦ { …, fᵢ : τᵢ, … } ∈ 〚Ξ〛Mod
τᵢ ↠ τᵢ' σ₁ ↠ σ₁' ⋯ σₙ ↠ σₙ'
Γ ⊢ σ₁' : k₁ ⋯ Γ ⊢ σₙ' : kₙ
Γ ⊢ e : Mod:T σ₁' … σₙ'
——————————————————————————————————————————————————————————————— ExpRecProj
Γ ⊢ Mod:T @σ₁ … @σₙ {f} e : τᵢ'[α₁ ↦ σ₁', …, αₙ ↦ σₙ']
'record' T (α₁:k₁) … (αₙ:kₙ) ↦ { …, fᵢ : τᵢ, … } ∈ 〚Ξ〛Mod
τᵢ ↠ τᵢ' σ₁ ↠ σ₁' ⋯ σₙ ↠ σₙ'
Γ ⊢ σ₁' : k₁ ⋯ Γ ⊢ σₙ' : kₙ
Γ ⊢ e : Mod:T σ₁' ⋯ σₙ'
Γ ⊢ eᵢ : τᵢ'[α₁ ↦ σ₁', …, αₙ ↦ σₙ']
———————————————————————————————————————————————————————————————– ExpRecUpdate
Γ ⊢
Mod:T @σ₁ … @σₙ { e 'with' fᵢ = eᵢ } : Mod:T σ₁' … σₙ'
'variant' T (α₁:k₁) … (αₙ:kₙ) ↦ … | Vᵢ : τᵢ | … ∈ 〚Ξ〛Mod
τᵢ ↠ τᵢ' σ₁ ↠ σ₁' ⋯ σₙ ↠ σₙ'
Γ ⊢ σ₁' : k₁ ⋯ Γ ⊢ σₙ' : kₙ
Γ ⊢ e : τᵢ'[α₁ ↦ σ₁', …, αₙ ↦ σₙ']
——————————————————————————————————————————————————————————————— ExpVarCon
Γ ⊢ Mod:T:Vᵢ @σ₁ … @σₙ e : Mod:T σ₁' … σₙ'
'enum' T ↦ … | Eᵢ | … ∈ 〚Ξ〛Mod
——————————————————————————————————————————————————————————————— ExpEnumCon
Γ ⊢ Mod:T:Eᵢ : Mod:T
⟨ f₁: τ₁, …, fₘ: τₘ ⟩ ↠ σ
Γ ⊢ σ : ⋆
Γ ⊢ e₁ : τ₁ ⋯ Γ ⊢ eₘ : τₘ
——————————————————————————————————————————————————————————————— ExpStructCon
Γ ⊢ ⟨ f₁ = e₁, …, fₘ = eₘ ⟩ : σ
Γ ⊢ e : ⟨ …, fᵢ: τᵢ, … ⟩
——————————————————————————————————————————————————————————————— ExpStructProj
Γ ⊢ e.fᵢ : τᵢ
Γ ⊢ e : ⟨ f₁: τ₁, …, fᵢ: τᵢ, …, fₙ: τₙ ⟩
Γ ⊢ eᵢ : τᵢ
——————————————————————————————————————————————————————————————— ExpStructUpdate
Γ ⊢ ⟨ e 'with' fᵢ = eᵢ ⟩ : ⟨ f₁: τ₁, …, fₙ: τₙ ⟩
n ≥ 1
Γ ⊢ e : τ
Γ ⊢ τ // alt₁ : σ
⋮
Γ ⊢ τ // altₙ : σ
τ ⊲ alt₁, …, altₙ
——————————————————————————————————————————————————————————————— ExpCase
Γ ⊢ 'case' e 'of' alt₁ | … | altₙ : σ
Γ ⊢ σ : ⋆
⊢ₑ τ
Γ ⊢ e : τ
——————————————————————————————————————————————————————————————— ExpThrow [Daml-LF ≥ 1.14]
Γ ⊢ 'throw' @σ @τ @e : σ
⊢ₑ τ
Γ ⊢ e : τ
——————————————————————————————————————————————————————————————— ExpToAnyException [Daml-LF ≥ 1.14]
Γ ⊢ 'to_any_exception' @τ e : 'AnyException'
⊢ₑ τ
Γ ⊢ e : 'AnyException'
——————————————————————————————————————————————————————————————— ExpFromAnyException [Daml-LF ≥ 1.14]
Γ ⊢ 'from_any_exception' @τ e : 'Optional' τ
'interface' (x : I) ↦ … ∈ 〚Ξ〛Mod
'tpl' (x : T) ↦ { …, 'implements' Mod:I { … }, … } ∈ 〚Ξ〛Mod'
Γ ⊢ e : Mod':T
———————————————————————————————————————————————————————————————— ExpToInterface [Daml-LF ≥ 1.dev]
Γ ⊢ 'to_interface' @Mod:I @Mod':T e : Mod:I
'interface' (x : I) ↦ … ∈ 〚Ξ〛Mod
'tpl' (x : T) ↦ { …, 'implements' Mod:I { … }, … } ∈ 〚Ξ〛Mod'
Γ ⊢ e : Mod:I
———————————————————————————————————————————————————————————————— ExpFromInterface [Daml-LF ≥ 1.dev]
Γ ⊢ 'from_interface' @Mod:I @Mod':T e : 'Optional' Mod':T
'interface' (x : I) ↦ … ∈ 〚Ξ〛Mod
'tpl' (x : T) ↦ { …, 'implements' Mod:I { … }, … } ∈ 〚Ξ〛Mod'
Γ ⊢ e₁ : 'ContractId' Mod:I
Γ ⊢ e₂ : Mod:I
———————————————————————————————————————————————————————————————— ExpUnsafeFromInterface [Daml-LF ≥ 1.dev]
Γ ⊢ 'unsafe_from_interface' @Mod:I @Mod':T e₁ e₂ : Mod':T
'interface' (x : I) ↦ { …, 'methods' { …, f: τ, … }, … } ∈ 〚Ξ〛Mod
Γ ⊢ e : Mod:I
———————————————————————————————————————————————————————————————— ExpCallInterface [Daml-LF ≥ 1.dev]
Γ ⊢ 'call_interface' @Mod:I f e : τ
'interface' (x : I₁) ↦ … ∈ 〚Ξ〛Mod₁
'interface' (x : I₂) ↦ { …, 'requires' { …, Mod₁:I₁, … }, … } ∈ 〚Ξ〛Mod₂
Γ ⊢ e : Mod₂:I₂
———————————————————————————————————————————————————————————————— ExpToRequiredInterface [Daml-LF ≥ 1.dev]
Γ ⊢ 'to_required_interface' @Mod₁:I₁ @Mod₂:I₂ e : Mod₁:I₁
'interface' (x : I₁) ↦ … ∈ 〚Ξ〛Mod₁
'interface' (x : I₂) ↦ { …, 'requires' { …, Mod₁:I₁, … }, … } ∈ 〚Ξ〛Mod₂
Γ ⊢ e : Mod₁:I₁
———————————————————————————————————————————————————————————————— ExpFromRequiredInterface [Daml-LF ≥ 1.dev]
Γ ⊢ 'from_required_interface' @Mod₁:I₁ @Mod₂:I₂ e : 'Optional' Mod₂:I₂
'interface' (x : I₁) ↦ … ∈ 〚Ξ〛Mod₁
'interface' (x : I₂) ↦ { …, 'requires' { …, Mod₁:I₁, … }, … } ∈ 〚Ξ〛Mod₂
Γ ⊢ e₁ : 'ContractId' Mod₁:I₁
Γ ⊢ e₂ : Mod₁:I₁
———————————————————————————————————————————————————————————————— ExpUnsafeFromRequiredInterface [Daml-LF ≥ 1.dev]
Γ ⊢ 'unsafe_from_required_interface' @Mod₁:I₁ @Mod₂:I₂ e₁ e₂ : Mod₂:I₂
'interface' (x : I) ↦ … ∈ 〚Ξ〛Mod
Γ ⊢ e : Mod:I
———————————————————————————————————————————————————————————————— ExpInterfaceTypeRep [Daml-LF ≥ 1.dev]
Γ ⊢ 'interface_typerep' @Mod:I e : 'TypeRep'
'interface' (x : I) ↦ … ∈ 〚Ξ〛Mod
Γ ⊢ e : Mod:I
———————————————————————————————————————————————————————————————— ExpInterfaceSignatory [Daml-LF ≥ 1.dev]
Γ ⊢ 'interface_signatory' @Mod:I e : 'List' 'Party'
'interface' (x : I) ↦ … ∈ 〚Ξ〛Mod
Γ ⊢ e : Mod:I
———————————————————————————————————————————————————————————————— ExpInterfaceObserver [Daml-LF ≥ 1.dev]
Γ ⊢ 'interface_observer' @Mod:I e : 'List' 'Party'
τ ↠ τ' Γ ⊢ τ' : ⋆ Γ ⊢ e : τ'
——————————————————————————————————————————————————————————————— UpdPure
Γ ⊢ 'pure' @τ e : 'Update' τ'
τ₁ ↠ τ₁' Γ ⊢ τ₁' : ⋆ Γ ⊢ e₁ : 'Update' τ₁'
x₁ : τ₁' · Γ ⊢ e₂ : 'Update' τ₂
——————————————————————————————————————————————————————————————— UpdBlock
Γ ⊢ 'bind' x₁ : τ₁ ← e₁ 'in' e₂ : 'Update' τ₂
'tpl' (x : T) ↦ … ∈ 〚Ξ〛Mod Γ ⊢ e : Mod:T
——————————————————————————————————————————————————————————————— UpdCreate
Γ ⊢ 'create' @Mod:T e : 'Update' ('ContractId' Mod:T)
'interface' (x : I) ↦ … ∈ 〚Ξ〛Mod
Γ ⊢ e : Mod:I
——————————————————————————————————————————————————————————————— UpdCreateInterface [Daml-LF ≥ 1.dev]
Γ ⊢ 'create_interface' @Mod:I e : 'Update' ('ContractId' Mod:I)
'tpl' (x : T)
↦ { …, 'choices' { …, 'choice' ChKind Ch (y : 'ContractId' Mod:T) (z : τ) : σ 'by' … ↦ …, … } }
∈ 〚Ξ〛Mod
Γ ⊢ e₁ : 'ContractId' Mod:T
Γ ⊢ e₂ : τ
——————————————————————————————————————————————————————————————— UpdExercise
Γ ⊢ 'exercise' @Mod:T Ch e₁ e₂ : 'Update' σ
'tpl' (x : T)
↦ { …, 'choices' { …, 'choice' ChKind Ch (y : 'ContractId' Mod:T) (z : τ) : σ 'by' … ↦ …, … }, 'key' τₖ … }
∈ 〚Ξ〛Mod
Γ ⊢ e₁ : τₖ
Γ ⊢ e₂ : τ
——————————————————————————————————————————————————————————————— UpdExerciseByKey
Γ ⊢ 'exercise_by_key' @Mod:T Ch e₁ e₂ : 'Update' σ
'interface' (x : I)
↦ { …, 'choices' { …, 'choice' ChKind Ch (y : 'ContractId' Mod:I) (z : τ) : σ 'by' … ↦ …, … } }
∈ 〚Ξ〛Mod
Γ ⊢ e₁ : 'ContractId' Mod:I
Γ ⊢ e₂ : τ
Γ ⊢ e₃ : 'Optional' (Mod:I -> 'Bool')
——————————————————————————————————————————————————————————————— UpdExerciseInterface [Daml-LF ≥ 1.dev]
Γ ⊢ 'exercise_interface' @Mod:I Ch e₁ e₂ e₃ : 'Update' σ
'tpl' (x : T) ↦ … ∈ 〚Ξ〛Mod
Γ ⊢ e : 'ContractId' Mod:T
——————————————————————————————————————————————————————————————— UpdFetch
Γ ⊢ 'fetch' @Mod:T e : 'Update' Mod:T
'interface' (x : I) ↦ … ∈ 〚Ξ〛Mod
Γ ⊢ e : 'ContractId' Mod:I
——————————————————————————————————————————————————————————————— UpdFetchInterface [Daml-LF ≥ 1.dev]
Γ ⊢ 'fetch_interface' @Mod:I e : 'Update' Mod:I
——————————————————————————————————————————————————————————————— UpdGetTime
Γ ⊢ 'get_time' : 'Update' 'Timestamp'
'tpl' (x : T) ↦ { …, 'key' τ …, … } ∈ 〚Ξ〛Mod
Γ ⊢ e : τ
——————————————————————————————————————————————————————————————— UpdFetchByKey
Γ ⊢ 'fetch_by_key' @Mod:T e
:
'Update' ⟨
'contractId' : 'ContractId' @Mod:T
'contract' : Mod:T
⟩
'tpl' (x : T) ↦ { …, 'key' τ …, … } ∈ 〚Ξ〛Mod
Γ ⊢ e : τ
——————————————————————————————————————————————————————————————— UpdLookupByKey
Γ ⊢ 'lookup_by_key' @Mod:T e
:
'Update' ('Optional' (ContractId Mod:T))
τ ↠ τ' Γ ⊢ e : 'Update' τ'
——————————————————————————————————————————————————————————————— UpdEmbedExpr
Γ ⊢ 'embed_expr' @τ e : 'Update' τ'
τ ↠ τ'
Γ ⊢ e₁ : 'Update' τ'
x : 'AnyException' · Γ ⊢ e₂ : 'Optional' ('Update' τ')
——————————————————————————————————————————————————————————————— UpdTryCatch [Daml-LF ≥ 1.14]
Γ ⊢ 'try' @τ e₁ 'catch' x. e₂ : 'Update' τ'
Γ ⊢ τ : ⋆ Γ ⊢ e : τ
——————————————————————————————————————————————————————————————— ScnPure
Γ ⊢ 'spure' @τ e : 'Scenario' τ
τ₁ ↠ τ₁' Γ ⊢ τ₁' : ⋆ Γ ⊢ e₁ : 'Scenario' τ₁'
x₁ : τ₁' · Γ ⊢ e₂ : 'Scenario' τ₂
——————————————————————————————————————————————————————————————— ScnBlock
Γ ⊢ 'sbind' x₁ : τ₁ ← e₁ 'in' e₂ : 'Scenario' τ₂
Γ ⊢ e : 'Party'
τ ↠ τ' Γ ⊢ τ' : ⋆ Γ ⊢ u : 'Uptate' τ
——————————————————————————————————————————————————————————————— ScnCommit
Γ ⊢ 'commit' @τ e u : 'Scenario' τ
Γ ⊢ e : 'Party'
τ ↠ τ' Γ ⊢ τ' : ⋆ Γ ⊢ u : 'Uptate' τ
——————————————————————————————————————————————————————————————— ScnMustFailAt
Γ ⊢ 'must_fail_at' @τ e u : 'Scenario' 'Unit'
Γ ⊢ e : 'Int64'
——————————————————————————————————————————————————————————————— ScnPass
Γ ⊢ 'pass' e : 'Scenario' 'Timestamp'
Γ ⊢ e : 'Text'
——————————————————————————————————————————————————————————————— ScnGetParty
Γ ⊢ 'get_party' e : 'Scenario' 'Party'
τ ↠ τ' Γ ⊢ e : 'Scenario' τ'
——————————————————————————————————————————————————————————————— ScnEmbedExpr
Γ ⊢ 'sembed_expr' @τ e : 'Scenario' τ'
.. note :: Unlike ``ExpTextMap``, the ``ExpGenMap`` rule does not
enforce uniqueness of key. In practice, the uniqueness is enforced
by the `builtin functions <Generic Map functions>`_ that are the
only way to handle generic maps in a serialized program, the
explicit syntax for maps being forbidden in serialized programs.
Well-formed case alternatives
.............................
Case expressions ``Γ ⊢ 'case' e 'of' alt₁ | … | altₙ : σ`` require the
notion of well-formed case alternatives ``Γ ⊢ τ // alt : σ`` defined here.
To simplify the presentation, we omit the assumption that the scrutinee
type ``τ`` is well-formed, in the rules below. ::
┌──────────────────┐
Well-formed case alternatives │ Γ ⊢ τ // alt : σ │
└──────────────────┘
'variant' T (α₁:k₁) … (αₙ:kₙ) ↦ … | V : τ | … ∈ 〚Ξ〛Mod
τ ↠ τ'
x : τ'[α₁ ↦ τ₁, …, αₙ ↦ τₙ] · Γ ⊢ e : σ
——————————————————————————————————————————————————————————————— AltVariant
Γ ⊢ Mod:T τ₁ … τₙ // Mod:T:V x → e : σ
'enum' T ↦ … | E | … ∈ 〚Ξ〛Mod
Γ ⊢ e : σ
——————————————————————————————————————————————————————————————— AltEnum
Γ ⊢ Mod:T // Mod:T:E → e : σ
Γ ⊢ e : σ
——————————————————————————————————————————————————————————————— AltNil
Γ ⊢ 'List' τ // 'Nil' → e : σ
xₕ ≠ xₜ
xₕ : τ · xₜ : 'List' τ · Γ ⊢ e : σ
——————————————————————————————————————————————————————————————— AltCons
Γ ⊢ 'List' τ // 'Cons' xₕ xₜ → e : σ
Γ ⊢ e : σ
——————————————————————————————————————————————————————————————— AltNone
Γ ⊢ 'Optional' τ // 'None' → e : σ
x : τ · Γ ⊢ e : σ
——————————————————————————————————————————————————————————————— AltSome
Γ ⊢ 'Optional' τ // 'Some' x → e : σ
Γ ⊢ e : σ
——————————————————————————————————————————————————————————————— AltTrue
Γ ⊢ 'Bool' // 'True' → e : σ
Γ ⊢ e : σ
——————————————————————————————————————————————————————————————— AltFalse
Γ ⊢ 'Bool' // 'False' → e : σ
Γ ⊢ e : σ
——————————————————————————————————————————————————————————————— AltUnit
Γ ⊢ 'Unit' // () → e : σ
Γ ⊢ e : σ
——————————————————————————————————————————————————————————————— AltDefault
Γ ⊢ τ // _ → e : σ
Pattern match exhaustiveness
............................
Case expressions ``Γ ⊢ 'case' e 'of' alt₁ | … | altₙ : σ`` also require
their patterns to be exhaustive, which is defined here. ::
┌─────────────────────┐
Pattern match exhaustiveness │ τ ⊲ alt₁, …, altₙ │
└─────────────────────┘
'variant' T (α₁:k₁) … (αᵣ:kᵣ) ↦ V₁ : σ₁ | … | Vₘ : σₘ ∈ 〚Ξ〛Mod
i₁, i₂, …, iₘ ∈ {1, …, n}
altᵢ₁ = Mod:T:V₁ x₁ → e₁
altᵢ₂ = Mod:T:V₂ x₂ → e₂
⋮
altᵢₘ = Mod:T:Vₘ xₘ → eₘ
——————————————————————————————————————————————————————————————— ExhaustVariant
Mod:T τ₁ … τᵣ ⊲ alt₁, …, altₙ
'enum' T ↦ E₁ | … | Eₘ ∈ 〚Ξ〛Mod
i₁, i₂, …, iₘ ∈ {1, …, n}
altᵢ₁ = Mod:T:E₁ → e₁
altᵢ₂ = Mod:T:E₂ → e₂
⋮
altᵢₘ = Mod:T:Eₘ → eₘ
——————————————————————————————————————————————————————————————— ExhaustEnum
Mod:T ⊲ alt₁, …, altₙ
i, j ∈ {1, …, n}
altᵢ = 'Nil' → e₁
altⱼ = 'Cons' xₕ xₜ → e₂
——————————————————————————————————————————————————————————————— ExhaustList
'List' τ ⊲ alt₁, …, altₙ
i, j ∈ {1, …, n}
altᵢ = 'None' → e₁
altⱼ = 'Some' x → e₂
——————————————————————————————————————————————————————————————— ExhaustOptional
'Optional' τ ⊲ alt₁, …, altₙ
i, j ∈ {1, …, n}
altᵢ = 'True' → e₁
altⱼ = 'False' → e₂
——————————————————————————————————————————————————————————————— ExhaustBool
'Bool' ⊲ alt₁, …, altₙ
i ∈ {1, …, n}
altᵢ = () → e
——————————————————————————————————————————————————————————————— ExhaustUnit
'Unit' ⊲ alt₁, …, altₙ
i ∈ {1, …, n}
altᵢ = _ → e
——————————————————————————————————————————————————————————————— ExhaustDefault
τ ⊲ alt₁, …, altₙ
Serializable types
..................
To define the validity of definitions, modules, and packages, we need to
first define *serializable* types. As the name suggests, serializable
types are the types whose values can be persisted on the ledger. ::
┌────────┐
Serializable types │ ⊢ₛ τ │
└────────┘
———————————————————————————————————————————————————————————————— STyUnit
⊢ₛ 'Unit'
———————————————————————————————————————————————————————————————— STyBool
⊢ₛ 'Bool'
⊢ₛ τ
———————————————————————————————————————————————————————————————— STyList
⊢ₛ 'List' τ
⊢ₛ τ
———————————————————————————————————————————————————————————————— STyOptional
⊢ₛ 'Optional' τ
———————————————————————————————————————————————————————————————— STyInt64
⊢ₛ 'Int64'
———————————————————————————————————————————————————————————————— STyNumeric
⊢ₛ 'Numeric' n
———————————————————————————————————————————————————————————————— STyText
⊢ₛ 'Text'
———————————————————————————————————————————————————————————————— STyDate
⊢ₛ 'Date'
———————————————————————————————————————————————————————————————— STyTimestamp
⊢ₛ 'Timestamp'
———————————————————————————————————————————————————————————————— STyParty
⊢ₛ 'Party'
⊢ₛ τ
———————————————————————————————————————————————————————————————— STyCid
⊢ₛ 'ContractId' τ
'interface' (x : I) ↦ … ∈ 〚Ξ〛Mod
———————————————————————————————————————————————————————————————— STyCidInterface
⊢ₛ 'ContractId' Mod:I
'record' T α₁ … αₙ ↦ { f₁: σ₁, …, fₘ: σₘ } ∈ 〚Ξ〛Mod
⊢ₛ σ₁[α₁ ↦ τ₁, …, αₙ ↦ τₙ]
⋮
⊢ₛ σₘ[α₁ ↦ τ₁, …, αₙ ↦ τₙ]
⊢ₛ τ₁
⋮
⊢ₛ τₙ
———————————————————————————————————————————————————————————————— STyRecConf
⊢ₛ Mod:T τ₁ … τₙ
'variant' T α₁ … αₙ ↦ V₁: σ₁ | … | Vₘ: σₘ ∈ 〚Ξ〛Mod m ≥ 1
⊢ₛ σ₁[α₁ ↦ τ₁, …, αₙ ↦ τₙ]
⋮
⊢ₛ σₘ[α₁ ↦ τ₁, …, αₙ ↦ τₙ]
⊢ₛ τ₁
⋮
⊢ₛ τₙ
———————————————————————————————————————————————————————————————— STyVariantCon
⊢ₛ Mod:T τ₁ … τₙ
'enum' T ↦ E₁: σ₁ | … | Eₘ: σₘ ∈ 〚Ξ〛Mod m ≥ 1
———————————————————————————————————————————————————————————————— STyEnumCon
⊢ₛ Mod:T
Note that
1. Structs are *not* serializable.
2. Type synonyms are *not* serializable.
3. Uninhabited variant and enum types are *not* serializable.
4. For a data type to be serializable, *all* type
parameters must be instantiated with serializable types, even
phantom ones.
5. Interface types are not serializable, but interface contract ids
are serializable.
Well-formed-definitions
.......................
Finally, we specify well-formed definitions. Note that these rules
work also under a set of packages available for usage ``Ξ``. Moreover,
they also have the current module name, ``ModName``, in scope (needed
for the ``DefTemplate`` rule). ::
┌────────┐
Well-formed definitions │ ⊢ Def │
└────────┘
τ₁ ↠ τ₁' αₙ : kₙ · … · α₁ : k₁ ⊢ τ₁' : ⋆
⋮
τₘ ↠ τₘ' αₙ : kₙ · … · α₁ : k₁ ⊢ τₘ' : ⋆
——————————————————————————————————————————————————————————————— DefRec
⊢ 'record' T (α₁: k₁) … (αₙ: kₙ) ↦ { f₁: τ₁, …, fₘ: τₘ }
τ₁ ↠ τ₁' αₙ : kₙ · … · α₁ : k₁ ⊢ τ₁' : ⋆
⋮
τₘ ↠ τₘ' αₙ : kₙ · … · α₁ : k₁ ⊢ τₘ' : ⋆
——————————————————————————————————————————————————————————————— DefVariant
⊢ 'record' T (α₁: k₁) … (αₙ: kₙ) ↦ V₁: τ₁ | … | Vₘ: τₘ
——————————————————————————————————————————————————————————————— DefEnum
⊢ 'enum' T ↦ E₁ | … | Eₘ
τ ↠ τ' (α₁:k₁) … (αₙ:kₙ) · Γ ⊢ τ' : ⋆
——————————————————————————————————————————————————————————————— DefTypeSynonym
⊢ 'synonym' S (α₁: k₁) … (αₙ: kₙ) ↦ τ
τ ↠ τ' ε ⊢ e : τ'
——————————————————————————————————————————————————————————————— DefValue
⊢ 'val' W : τ ↦ e
'record' T ↦ { f₁ : τ₁, …, fₙ : τₙ } ∈ 〚Ξ〛Mod
⊢ₛ Mod:T
x : Mod:T ⊢ eₚ : 'Bool'
x : Mod:T ⊢ eₛ : 'List' 'Party'
x : Mod:T ⊢ eₒ : 'List' 'Party'
x : Mod:T ⊢ eₐ : 'Text'
x : Mod:T ⊢ ChDef₁ ⋯ x : Mod:T ⊢ ChDefₘ
x : Mod:T ⊢ KeyDef
x : Mod:T ⊢ ImplDef₁ ⋯ x : Mod:T ⊢ ImplDefₖ
——————————————————————————————————————————————————————————————— DefTemplate
⊢ 'tpl' (x : T) ↦
{ 'precondition' eₚ
, 'signatories' eₛ
, 'observers' eₒ
, 'agreement' eₐ
, 'choices' { ChDef₁, …, ChDefₘ }
, KeyDef
, ImplDef₁, …, ImplDefₖ
}
'record' T ↦ { f₁ : τ₁, …, fₙ : τₙ } ∈ 〚Ξ〛Mod
⊢ₛ Mod:T
⊢ e : Mod:T → 'Text'
——————————————————————————————————————————————————————————————— DefException [Daml-LF ≥ 1.14]
⊢ 'exception' T ↦ { 'message' e }
Mod:I ∉ { Mod₁:I₁, …, Modₖ:Iₖ }
'interface' (x₁ : I₁) ↦ { 'requires' R₁ , … } ∈ 〚Ξ〛Mod₁ R₁ ⊆ { Mod₁:I₁, …, Modₖ:Iₖ }
⋮
'interface' (xₖ : Iₖ) ↦ { 'requires' Rₖ , … } ∈ 〚Ξ〛Modₖ Rₖ ⊆ { Mod₁:I₁, …, Modₖ:Iₖ }
x : Mod:I ⊢ eₚ : 'Bool'
τ₁ ↠ τ₁' ⊢ τ₁' : ⋆
⋮
τₙ ↠ τₙ' ⊢ τₙ' : ⋆
x : Mod:I ⊢ ChDef₁ ⋯ x : Mod:I ⊢ ChDefₘ
——————————————————————————————————————————————————————————————— DefInterface [Daml-LF ≥ 1.dev]
⊢ 'interface' (x : I) ↦
{ 'requires' { Mod₁:I₁, …, Modₖ:Iₖ }
, 'precondition' eₚ
, 'methods' { f₁ : τ₁, …, fₙ : τₙ }
, 'choices' { ChDef₁, …, ChDefₘ }
}
┌───────────────────┐
Well-formed choices │ x : Mod:T ⊢ ChDef │
└───────────────────┘
⊢ₛ τ
⊢ₛ σ
y : 'ContractId' Mod:T · z : τ · x : Mod:T ⊢ e : 'Update' σ
z : τ · x : Mod:T ⊢ eₚ : 'List' 'Party'
z : τ · x : Mod:T ⊢ eₒ : 'List' 'Party'
——————————————————————————————————————————————————————————————— ChDef
x : Mod:T ⊢ 'choice' ChKind Ch (y : 'ContractId' Mod:T) (z : τ) : σ 'by' eₚ 'observers' eₒ ↦ e
┌─────────────────────┐
Well-formed interface implementations │ x : Mod:T ⊢ ImplDef │
└─────────────────────┘
'interface' (y : I) ↦
{ 'requires' R
, 'precondition' eₚ
, 'methods' { f₁ : τ₁, …, fₘ = τₘ }
, 'choices' { 'choice' ChKind₁ Ch₁ …, …, 'choice' ChKindₘ Chₘ … }
} ∈ 〚Ξ〛Mod'
'tpl' (x : T) ↦ { …, 'implements' Mod₁:I₁ { … }, …, 'implements' Modₖ:Iₖ { … } } ∈ 〚Ξ〛Mod
R ⊆ { Mod₁:I₁, …, Modₖ:Iₖ }
τ₁ ↠ τ₁' x : Mod:T ⊢ e₁ : τ₁'
⋮
τₘ ↠ τₘ' x : Mod:T ⊢ eₘ : τₘ'
——————————————————————————————————————————————————————————————— ImplDef
x : Mod:T ⊢ 'implements' Mod':I
{ 'methods' { f₁ = e₁, …, fₙ = eₙ }
, 'choices' { Ch₁, …, Chₘ }
}
┌────────────┐
Valid key │ ⊢ₖ e : τ │
└────────────┘
——————————————————————————————————————————————————————————————— ExpRecProj
⊢ₖ x
⊢ₖ e
——————————————————————————————————————————————————————————————— ExpRecProj
⊢ₖ Mod:T @τ₁ … @τₙ {f} e
⊢ₖ e₁ ⋯ ⊢ₖ eₘ
———————————————————————————————————————————————————————————————— ExpRecCon
⊢ₖ Mod:T @σ₁ … @σₙ { f₁ = e₁, …, fₘ = eₘ }
┌────────────┐
Well-formed keys │ Γ ⊢ KeyDef │
└────────────┘
——————————————————————————————————————————————————————————————— KeyDefNone
Γ ⊢ 'no_key'
⊢ₛ τ Γ ⊢ eₖ : τ
⊢ₖ eₖ [Daml-LF = 1.3]
ε ⊢ eₘ : τ → 'List' 'Party'
——————————————————————————————————————————————————————————————— KeyDefSome
Γ ⊢ 'key' τ eₖ eₘ
Naturally, we will say that modules and packages are well-formed if
all the definitions they contain are well-formed.
Template coherence
~~~~~~~~~~~~~~~~~~
Each template definition is paired to a record ``T`` with no type
arguments (see ``DefTemplate`` rule). To avoid ambiguities, we want to
make sure that each record type ``T`` has at most one template
definition associated to it. We term this restriction *template
coherence* since it's a requirement reminiscent of the coherence
requirement of Haskell type classes.
Specifically, a template definition is *coherent* if:
* Its argument data type is defined in the same module that the
template is defined in;
* Its argument data type is not an argument to any other template.
Exception coherence
~~~~~~~~~~~~~~~~~~~
The *exception coherence* condition is literally the same as the template
coherence condition with "template" replaced by "exception". We further require
that no type has both a template definition and an exception definition associated to
it.
Party literal restriction
~~~~~~~~~~~~~~~~~~~~~~~~~
.. TODO I think this is incorrect, and actually before the
``ForbidPartyLiterals`` feature flag party literals were
allowed everywhere.
The usage of party literals is restricted in Daml-LF. By default,
party literals are neither allowed in templates nor in values used in
templates directly or indirectly. In practice, this restricted the
usage of party literals to test cases written in Daml-LF. Usage of
party literals can be completely forbidden thanks to the `feature flag
<Feature flags_>`_ ``ForbidPartyLiterals``. If this flag is on, any
occurrence of a party literal anywhere in the module makes the module
not well-formed.
Name collision restriction
~~~~~~~~~~~~~~~~~~~~~~~~~~
Daml-LF relies on `names and identifiers <Identifiers_>`_ to refer to
different kinds of constructs such as modules, type constructors,
variants constructor, and fields. These are relative; type names are
relative to modules; field names are relative to type record and so
one. They live in different namespaces. For example, the space names
for module and type is different.
Fully resolved name
...................
Daml-LF restricts the way names and identifiers are used within a
package. This restriction relies on the notion of *fully resolved
name* construct as follows:
* The *fully resolved name* of the module ``Mod`` is ``Mod``.
* The *fully resolved name* of a record type constructor ``T`` defined
in the module ``Mod`` is ``Mod.T``.
* The *fully resolved name* of a variant type constructor ``T``
defined in the module ``Mod`` is ``Mod.T``.
* The *fully resolved name* of a enum type constructor ``T`` defined
in the module ``Mod`` is ``Mod.T``.
* The *fully resolved name* of a type synonym ``S`` defined in the
module ``Mod`` is ``Mod.S``.
* The *fully resolved name* of a field ``fᵢ`` of a record type
definition ``'record' T … ↦ { …, fᵢ: τᵢ, … }`` defined in the
module ``Mod`` is ``Mod.T.fᵢ``
* The *fully resolved name* of a variant constructor ``Vᵢ`` of a
variant type definition ``'variant' T … ↦ … | Vᵢ: τᵢ | …`` defined
in the module ``Mod`` is ``Mod.T.Vᵢ``.
* The *fully resolved name* of a enum constructor ``Eᵢ`` of a enum
type definition ``'enum' T ↦ … | Eᵢ | …`` defined in the module
``Mod`` is ``Mod.T.Eᵢ``.
* The *fully resolved name* of a choice ``Ch`` of a template
definition ``'tpl' (x : T) ↦ { …, 'choices' { …, 'choice' ChKind Ch
… ↦ …, … } }`` defined in the module ``Mod`` is ``Mod.T.Ch``.
* The *fully resolved name* of an inherited choice ``Ch`` of a template
definition ``'tpl' (x : T) ↦ { …, 'implements' { …, 'choices' { …, Ch,
… } } }`` defined in the module ``Mod`` is ``Mod.T.Ch``.
* The *fully resolved name* of a choice ``Ch`` of an interface
definition ``'interface' (x : I) ↦ { …, 'choices' { …, 'choice' ChKind Ch
… ↦ …, … } }`` defined in the module ``Mod`` is ``Mod.I.Ch``.
* The *fully resolved name* of a method ``fᵢ`` of an interface
definition ``'interface' (x : I) ↦ { …, 'methods' { …, fᵢ: τᵢ, … } }``
defined in the module ``Mod`` is ``Mod.I.fᵢ``.
Name collisions
...............
A so-called *name collision* occurs if two fully resolved names in a
package are equal *ignoring case*. The following are examples of
collisions:
* A package contains two modules with the same name;
* A module defines two types with the same name, one lowercase and the
other one uppercase;
* A record contains two fields with the same name;
* A package contains a module ``A.B`` and a module ``A`` that defines
the type ``B``;
* A package contains a module ``A.B`` that defines the type ``C``
together with a module ``A`` that defines the type ``B.C``.
Note that templates do not have names, and therefore can not cause
collisions. Note also that value references are not concerned with
collisions as defined here.
Also note that while the collision is case-insensitive, name resolution
is *not* case-insensitive in Daml-LF. In other words, to refer to a
name, one must refer to it with the same case that it was defined with.
The case-insensitivity for collisions is in place since we often generate
files from Daml-LF packages, and we want to make sure for things to work
smoothly when operating in case-insensitive file systems, while at the
same time preserving case sensitivity in the language.
Name collision condition
........................
In Daml-LF, the only permitted name collisions are those occurring
between variant constructors and record types defined in the same
module. Every other collision makes the module (and thus the package)
not well-formed. For example, a module ``Mod`` can contain the following
definitions::
'variant' Tree (α : ⋆) ↦ Node : Mod:Tree.Node @α | Leaf : Unit
'record' Tree.Node (α : ⋆) ↦ { value: α, left: Mod:Tree α, right: Mod:Tree α }
The variant constructor ``Node`` (within the definition of the
variant type ``Tree``) and the record type ``Tree.Node`` (within the
first record type definition) have the same fully resolved name
``Mod.Tree.Node``. However this package is well-formed.
Note that name collisions between a record definition and a variant
constructor from different modules are prohibited.
We will say that the *name collision condition* holds for a package if
the only name collisions within this package are those occurring
between variant constructors and record types, as described above.
Well-formed packages
~~~~~~~~~~~~~~~~~~~~
Then, a collection of packages ``Ξ`` is well-formed if:
* Each definition in ``Ξ`` is `well-formed <well-formed-definitions_>`_;
* Each template in ``Ξ`` is `coherent <Template coherence_>`_;
* Each exception in ``Ξ`` is `coherent <Exception coherence_>`_;
* The `party literal restriction`_ is respected for
every module in ``Ξ`` -- taking the ``ForbidPartyLiterals`` flag into
account.
* The `name collision condition`_ holds for every
package of ``Ξ``.
* There are no cycles between type synonym definitions, modules, and
packages references.
* Each package ``p`` only depends on packages whose LF version is older
than or the same as the LF version of ``p`` itself.
Operational semantics
^^^^^^^^^^^^^^^^^^^^^
The section presents a big-step call-by value operation semantics of
the language.
Similarly to the type system, every rule for expression evaluation and
update interpretation operates on the packages available for
usage ``Ξ``.
Values
~~~~~~
To define any call-by-value semantics for Daml-LF expression, we need
first to define the notion of *values*, the expressions which do not
need to be evaluated further. ::
┌───────┐
Values │ ⊢ᵥ e │
└───────┘
——————————————————————————————————————————————————— ValExpAbs
⊢ᵥ λ x : τ . e
——————————————————————————————————————————————————— ValExpTyAbsNat
⊢ᵥ Λ α : 'nat' . e
⊢ᵥ e
——————————————————————————————————————————————————— ValExpTyAbsErasable
⊢ᵥ Λ α : ek . e
——————————————————————————————————————————————————— ValExpLitInt64
⊢ᵥ LitInt64
——————————————————————————————————————————————————— ValExpLitNumeric
⊢ᵥ LitNumeric
——————————————————————————————————————————————————— ValExpLitBigNumeric
⊢ᵥ LitBigNumeric
——————————————————————————————————————————————————— ValExpLitText
⊢ᵥ t
——————————————————————————————————————————————————— ValExpLitDate
⊢ᵥ LitDate
——————————————————————————————————————————————————— ValExpLitTimestamp
⊢ᵥ LitTimestamp
——————————————————————————————————————————————————— ValExpLitContractId
⊢ᵥ cid
——————————————————————————————————————————————————— ValExpUnit
⊢ᵥ ()
——————————————————————————————————————————————————— ValExpTrue
⊢ᵥ 'True'
——————————————————————————————————————————————————— ValExpFalse
⊢ᵥ 'False'
——————————————————————————————————————————————————— ValExpListNil
⊢ᵥ 'Nil' @τ
⊢ᵥ eₕ ⊢ᵥ eₜ
——————————————————————————————————————————————————— ValExpListCons
⊢ᵥ 'Cons' @τ eₕ eₜ
——————————————————————————————————————————————————— ValExpOptionalNone
⊢ᵥ 'None' @τ
⊢ᵥ e
——————————————————————————————————————————————————— ValExpOptionalSome
⊢ᵥ 'Some' @τ e
⊢ᵥ e₁ ⋯ ⊢ᵥ eₙ
——————————————————————————————————————————————————— ValExpTextMap
⊢ᵥ [t₁ ↦ e₁; … ; tₙ ↦ eₙ]
⊢ᵥ e₁ ⋯ ⊢ᵥ eₙ
⊢ᵥ e₁' ⋯ ⊢ᵥ eₙ'
——————————————————————————————————————————————————— ValExpGenMap
⊢ᵥ 〚e₁ ↦ e₁'; … ; eₙ ↦ eₙ'〛
0 ≤ k < m
𝕋(F) = ∀ (α₁: k₁) … ∀ (αₘ: kₘ). σ₁ → … → σₙ → σ
——————————————————————————————————————————————————— ValExpBuiltin₁
⊢ᵥ F @τ₁ … @τₖ
0 ≤ k < n
𝕋(F) = ∀ (α₁: k₁) … ∀ (αₘ: kₘ). σ₁ → … → σₙ → σ
⊢ᵥ e₁ … ⊢ᵥ eₖ
——————————————————————————————————————————————————— ValExpBuiltin₂
⊢ᵥ F @τ₁ … @τₘ e₁ … eₖ
⊢ᵥ e₁ … ⊢ᵥ eₙ
——————————————————————————————————————————————————— ValExpRecCon
⊢ᵥ Mod:T @τ₁ … @τₙ { f₁ = e₁, …, fₙ = eₙ }
⊢ᵥ e
——————————————————————————————————————————————————— ValExpVariantCon
⊢ᵥ Mod:T:V @τ₁ … @τₙ e
——————————————————————————————————————————————————— ValExpEnumCon
⊢ᵥ Mod:T:E
⊢ᵥ e₁ ⋯ ⊢ᵥ eₘ
f₁ < f₂ < … < fₘ lexicographically
——————————————————————————————————————————————————— ValExpStructCon
⊢ᵥ ⟨ f₁ = e₁, …, fₘ = eₘ ⟩
⊢ᵥ e
——————————————————————————————————————————————————— ValExpToAny
⊢ᵥ 'to_any' @τ e
——————————————————————————————————————————————————— ValExpTypeRep
⊢ᵥ 'type_rep' @τ
⊢ₑ τ ⊢ᵥ e
——————————————————————————————————————————————————— ValToAnyException
⊢ᵥ 'to_any_exception' @τ e
'interface' (x : I) ↦ … ∈ 〚Ξ〛Mod
'tpl' (x : T) ↦ { …, 'implements' Mod:I { … }, … } ∈ 〚Ξ〛Mod'
⊢ᵥ e
——————————————————————————————————————————————————— ValToInterface
⊢ᵥ 'to_interface' @Mod:I @Mod':T e
⊢ᵥᵤ u
——————————————————————————————————————————————————— ValUpdate
⊢ᵥ u
⊢ᵥₛ s
——————————————————————————————————————————————————— ValScenario
⊢ᵥ s
——————————————————————————————————————————————————— ValUnboundedMathContext
⊢ᵥ LitRoundingMode
┌────────┐
Update Values │ ⊢ᵥᵤ u │
└────────┘
⊢ᵥ e
——————————————————————————————————————————————————— ValUpdatePure
⊢ᵥᵤ 'pure' @τ e
⊢ᵥᵤ e₁
——————————————————————————————————————————————————— ValUpdateBind
⊢ᵥᵤ 'bind' x₁ : τ₁ ← e₁ 'in' e₂
⊢ᵥ e
——————————————————————————————————————————————————— ValUpdateCreate
⊢ᵥᵤ 'create' @Mod:T e
⊢ᵥ e
——————————————————————————————————————————————————— ValUpdateFetch
⊢ᵥᵤ 'fetch' @Mod:T e
⊢ᵥ e₁
⊢ᵥ e₂
——————————————————————————————————————————————————— ValUpdateExercise
⊢ᵥᵤ 'exercise' @Mod:T Ch e₁ e₂
⊢ᵥ e₁
⊢ᵥ e₂
——————————————————————————————————————————————————— ValUpdateExerciseByKey
⊢ᵥᵤ 'exercise_by_key' @Mod:T Ch e₁ e₂
⊢ᵥ e
——————————————————————————————————————————————————— ValUpdateFetchByKey
⊢ᵥᵤ 'fetch_by_key' @Mod:T e
⊢ᵥ e
——————————————————————————————————————————————————— ValUpdateLookupByKey
⊢ᵥᵤ 'lookup_by_key' @Mod:T e
——————————————————————————————————————————————————— ValUpdateEmbedExpr
⊢ᵥᵤ 'embed_expr' @τ e
——————————————————————————————————————————————————— ValUpdateTryCatch
⊢ᵥᵤ 'try' @τ e₁ 'catch' x. e₂
┌────────┐
Scenario Values │ ⊢ᵥₛ s │
└────────┘
⊢ᵥ e
——————————————————————————————————————————————————— ValScenarioPure
⊢ᵥₛ 'spure' @τ e
⊢ᵥ e₁
——————————————————————————————————————————————————— ValScenarioBind
⊢ᵥₛ 'sbind' x₁ : τ₁ ← e₁ 'in' e₂
⊢ᵥ e
⊢ᵥᵤ u
——————————————————————————————————————————————————— ValScenarioCommit
⊢ᵥₛ 'commit' @τ e u
⊢ᵥ e
⊢ᵥᵤ u
——————————————————————————————————————————————————— ValScenarioMustFailAt
⊢ᵥₛ 'must_fail_at' @τ e u
⊢ᵥ e
——————————————————————————————————————————————————— ValScenarioPass
⊢ᵥₛ 'pass' e
——————————————————————————————————————————————————— ValScenarioGetTime
⊢ᵥₛ 'sget_time'
⊢ᵥ e
——————————————————————————————————————————————————— ValScenarioGetParty
⊢ᵥₛ 'sget_party' e
——————————————————————————————————————————————————— ValScenarioEmbedExpr
⊢ᵥₛ 'sembed_expr' @τ e
Note that the argument of an embedded expression does not need to be a
value for the whole to be so. In the following, we will use the
symbol ``v`` or ``w`` to represent an expression which is a value.
Note that for type lambdas, the kind of the argument affects whether it
is considered a value. In particular, an erasable kind is handled as if
it were erased, so in this case, the expression is a value only if the
body of the lambda is already a value. Type lambdas where the type
parameter is not erasable (i.e. does not have an erasable kind) are
values. This is captured in the rules ``ValExpTyAbsNat`` and
``ValExpTyAbsErasable``.
Note that the fields of struct values are always ordered lexicographically
by field name, unlike the fields of struct expressions. The field order is
normalized during evaluation.
Value nesting
~~~~~~~~~~~~~
A value is serializable if it lives inside serializable type and its
nesting is lower or equal to 100. Formally, the nesting of a
serializable value ``v`` is noted ``|v|`` and is defined recursively
on ``v`` as follows (we omit values that do not have serialized type)::
| LitInt64 | = 0
| LitNumeric | = 0
| LitBigNumeric | = 0
| t | = 0
| LitDate | = 0
| LitTimestamp | = 0
| cid | = 0
| () | = 0
| 'True' | = 0
| 'False' | = 0
| 'Nil' @τ | = 0
| 'Cons' @τ eₕ eₜ | = max₂ (|eₕ| + 1) |eₜ|
| 'None' @τ | = 0
| 'Some' @τ e | = |e| + 1
| [t₁ ↦ e₁; … ; tₙ ↦ eₙ] | = (maxₙ |e₁| … |eₙ|) + 1
| 〚e₁ ↦ e₁'; … ; eₙ ↦ eₙ'〛 | = (max₂ₙ |e₁| |e₁'| … |eₙ| |eₙ'|) + 1
| Mod:T @τ₁ … @τₙ { f₁ = e₁, …, fₙ = eₙ } | = (maxₙ |e₁| … |eₙ|) + 1
| Mod:T:V @τ₁ … @τₙ e | = |e| + 1
| Mod:T:E | = 0
| LitRoundingMode | = 0
where ``maxₙ`` is the ``n``-ary function that returns the maximum of its arguments.
Pattern matching
~~~~~~~~~~~~~~~~
We now define how patterns *match* values. If a pattern match succeed,
it produces a *substitution*, which tells us how to instantiate variables
bound by pattern.
::
Substitution
θ ::= ε -- SubstEmpty
| x ↦ v · θ -- SubstExpVal
Pattern matching result
mr ::= Succ θ -- MatchSuccess
| Fail -- MatchFailure
┌─────────────────────┐
Pattern Matching │ v 'matches' p ⇝ mr │
└─────────────────────┘
—————————————————————————————————————————————————————————————————————— MatchVariant
Mod:T:V @τ₁ … @τₘ v 'matches' Mod:T:V x ⇝ Succ (x ↦ v · ε)
—————————————————————————————————————————————————————————————————————— MatchEnum
Mod:T:E 'matches' Mod:T:E ⇝ Succ ε
—————————————————————————————————————————————————————————————————————— MatchNil
'Nil' @τ 'matches' 'Nil' ⇝ Succ ε
—————————————————————————————————————————————————————————————————————— MatchCons
'Cons' @τ vₕ vₜ 'matches' 'Cons' xₕ xₜ
⇝
Succ (xₕ ↦ vₕ · xₜ ↦ vₜ · ε)
—————————————————————————————————————————————————————————————————————— MatchNone
'None' @τ 'matches' 'None' ⇝ Succ ε
—————————————————————————————————————————————————————————————————————— MatchSome
'Some' @τ v 'matches' 'Some' x ⇝ Succ (x ↦ v · ε)
—————————————————————————————————————————————————————————————————————— MatchTrue
'True' 'matches' 'True' ⇝ Succ ε
—————————————————————————————————————————————————————————————————————— MatchFalse
'False' 'matches' 'False' ⇝ Succ ε
—————————————————————————————————————————————————————————————————————— MatchUnit
'()' 'matches' '()' ⇝ Succ ε
—————————————————————————————————————————————————————————————————————— MatchDefault
v 'matches' _ ⇝ Succ ε
if none of the rules above apply
—————————————————————————————————————————————————————————————————————— MatchFail
v 'matches' p ⇝ Fail
Type ordering
~~~~~~~~~~~~~
In this section, we define a strict partial order relation ``<ₜ`` on
types. Formally, ``<ₜ`` is defined as the least binary relation on
types that satisfies the following rules::
σ₁ <ₜ τ τ <ₜ σ₂
——————————————————————————————————————————————————— TypeOrderTransitivity
σ₁ <ₜ σ₂
——————————————————————————————————————————————————— TypeOrderUnitBool
'Unit' <ₜ 'Bool'
——————————————————————————————————————————————————— TypeOrderBoolInt64
'Bool' <ₜ 'Int64'
——————————————————————————————————————————————————— TypeOrderInt64Text
'Int64' <ₜ 'Text'
—————————————————————————————————————————————————— TypeOrderTextTimestamp
'Text' <ₜ 'Timestamp'
——————————————————————————————————————————————————— TypeOrderTimestampPArty
'Timestamp' <ₜ 'Party'
——————————————————————————————————————————————————— TypeOrderPartyList
'Party' <ₜ 'List'
—————————————————————————————————————————————————— TypeOrderListUpdate
'List' <ₜ 'Update'
——————————————————————————————————————————————————— TypeOrderUpdateScenario
'Update' <ₜ 'Scenario'
——————————————————————————————————————————————————— TypeOrderScenarioDate
'Scenario' <ₜ 'Date'
——————————————————————————————————————————————————— TypeOrderDateContractId
'Date' <ₜ 'ContractId'
——————————————————————————————————————————————————— TypeOrderContractIdOptional
'ContractId' <ₜ 'Optional'
——————————————————————————————————————————————————— TypeOrderOptionalArrow
'Optional' <ₜ 'Arrow'
——————————————————————————————————————————————————— TypeOrderArrowTextMap
'Arrow' <ₜ 'TextMap'
——————————————————————————————————————————————————— TypeOrderTextMapNumeric
'TextMap' <ₜ 'Numeric'
——————————————————————————————————————————————————— TypeOrderNumericAny
'Numeric' <ₜ 'Any'
——————————————————————————————————————————————————— TypeOrderAnyTypeRep
'Any' <ₜ 'TypeRep'
——————————————————————————————————————————————————— TypeOrderTypeRepUpdate
'TypeRep' <ₜ 'GenMap'
——————————————————————————————————————————————————— TypeOrderGenMapBigNumeric
'GenMap' <ₜ 'BigNumeric'
——————————————————————————————————————————————————— TypeOrderBigNumericRoundingMode
'BigNumeric' <ₜ 'RoundingMode'
——————————————————————————————————————————————————— TypeOrderRoundingModeAnyException
'RoundingMode' <ₜ 'AnyException'
——————————————————————————————————————————————————— TypeOrderAnyExceptionTyCon
'AnyException' <ₜ Mod:T
PkgId₁ comes lexicographically before PkgId₂
——————————————————————————————————————————————————— TypeOrderTyConPackageId
(PkgId₁:ModName₁):T₁ <ₜ (PkgId₂:ModName₂):T₂
ModName₁ comes lexicographically before ModName₂
——————————————————————————————————————————————————— TypeOrderTyConModName
(PkgId:ModName₁):T₁ <ₜ (PkgId:ModName₂):T₂
T₁ comes lexicographically before T₂
—————————————————————————————————————————————————— TypeOrderTyConName
Mod:T₁ <ₜ Mod:T₂
—————————————————————————————————————————————————— TypeOrderTyConNat
Mod:T <ₜ n
n₁ is strictly less than n₂
—————————————————————————————————————————————————— TypeOrderNatNat
n₁ <ₜ n₂
—————————————————————————————————————————————————— TypeOrderNatStruct
n <ₜ ⟨ f₁ : τ₁, …, fₘ : τₘ ⟩
fᵢ comes lexicographically before gᵢ
——————————————————————————————————————————————————— TypeOrderStructFieldName
⟨ f₁ : τ₁, …, fₘ : τₘ ⟩ <ₜ
⟨ f₁ : σ₁, …, fᵢ₋1 : σᵢ₋₁, gᵢ : σᵢ, …, gₙ : σₙ ⟩
——————————————————————————————————————————————————— TypeOrderStructFieldNumber
⟨ f₁ : τ₁, …, fₘ : τₘ ⟩ <ₜ
⟨ f₁ : τ₁, …, fₘ : τₘ, fₘ₊₁ : τₘ₊₁ ⟩
τᵢ <ₜ σᵢ
——————————————————————————————————————————————————— TypeOrderStructFieldType
⟨ f₁ : τ₁, …, fₘ : τₘ ⟩ <ₜ
⟨ f₁ : τ₁, …, fᵢ₋₁ : τᵢ₋₁, fᵢ : σᵢ, …, fₘ : σₘ ⟩
——————————————————————————————————————————————————— TypeOrderStructTyApp
⟨ f₁ : τ₁, …, fₘ : τₘ ⟩ <ₜ τ σ
τ₁ <ₜ τ₂
——————————————————————————————————————————————————— TypeOrderTyAppLeft
τ₁ σ₁ <ₜ τ₂ σ₂
σ₁ <ₜ σ₂
——————————————————————————————————————————————————— TypeOrderTypeAppRight
τ σ₁ <ₜ τ σ₂
Note that ``<ₜ`` is undefined on types containing variables,
quantifiers or type synonymes. ``≤ₜ`` is defined as the reflexive
closure of ``<ₜ``.
Expression evaluation
~~~~~~~~~~~~~~~~~~~~~
Daml-LF evaluation is only defined on well-typed expressions that
contain no free term-level variables, and any type-level variables
must be of an erasable kind. For the sake of brevity, and the fact
that erasable kinds cannot affect evaluation results, we do not
include the variable context ``Γ`` in the rules below.
Note that the evaluation of the body of a value definition is lazy. It
happens only when needed. The evaluation semantics itself does not cache
values to avoid recomputations, but actual implementations may do so.
The output of any Daml-LF built-in function ``F`` fully applied to
types ``@τ₁ … @τₘ`` and values ``v₁ … vₙ`` is deterministic. In the
following rules, we abstract this output with the notation ``𝕆(F @τ₁ …
@τₘ v₁ … vₙ)``. Please refer to the `Built-in functions`_ section for the
exact output.
::
Evaluation result
r ::= Ok v -- ResOk
| Err E -- ResErr
E ::= Throw v -- ErrThrow, v is a value of AnyException type
| Fatal t -- ErrFatal, t is a text value
┌──────────┐
Big-step evaluation │ e ⇓ r │
└──────────┘
—————————————————————————————————————————————————————————————————————— EvValue
v ⇓ Ok v
e ⇓ Err E
—————————————————————————————————————————————————————————————————————— EvTyAbsErasableErr
Λ α : ek . e ⇓ Err E
e ⇓ Ok v
—————————————————————————————————————————————————————————————————————— EvTyAbsErasable
Λ α : ek . e ⇓ Ok (Λ α : ek . v)
e₁ ⇓ Err E
—————————————————————————————————————————————————————————————————————— EvExpAppErr1
e₁ e₂ ⇓ Err E
e₁ ⇓ Ok (λ x : τ . e)
e₂ ⇓ Err E
—————————————————————————————————————————————————————————————————————— EvExpAppErr2
e₁ e₂ ⇓ Err E
e₁ ⇓ Ok (λ x : τ . e)
e₂ ⇓ Ok v₂
e[x ↦ v₂] ⇓ r
—————————————————————————————————————————————————————————————————————— EvExpApp
e₁ e₂ ⇓ r
e₁ ⇓ Err E
—————————————————————————————————————————————————————————————————————— EvExpTyAppErr
e₁ @τ ⇓ Err E
e₁ ⇓ Ok (Λ α : k . e)
e[α ↦ τ] ⇓ r
—————————————————————————————————————————————————————————————————————— EvExpTyApp
e₁ @τ ⇓ r
e₁ ⇓ Err E
—————————————————————————————————————————————————————————————————————— EvExpLetErr
'let' x : τ = e₁ 'in' e₂ ⇓ Err E
e₁ ⇓ Ok v₁
e₂[x ↦ v₁] ⇓ r
—————————————————————————————————————————————————————————————————————— EvExpLet
'let' x : τ = e₁ 'in' e₂ ⇓ r
e ⇓ Err E
—————————————————————————————————————————————————————————————————————— EvExpToAnyErr
'to_any' @τ e ⇓ Err E
e ⇓ Ok v
—————————————————————————————————————————————————————————————————————— EvExpToAny
'to_any' @τ e ⇓ Ok ('to_any' @τ v)
e ⇓ Err E
—————————————————————————————————————————————————————————————————————— EvExpFromAnyErr
'from_any' @τ e ⇓ Err E
e ⇓ Ok ('to_any' @τ v)
—————————————————————————————————————————————————————————————————————— EvExpFromAnySucc
'from_any' @τ e ⇓ Ok ('Some' @τ v)
e ⇓ Ok ('to_any' @τ₁ v) τ₁ ≠ τ₂
—————————————————————————————————————————————————————————————————————— EvExpFromAnyFail
'from_any' @τ₂ e ⇓ Ok 'None'
e₁ ⇓ Err E
—————————————————————————————————————————————————————————————————————— EvExpCaseErr
'case' e₁ 'of' { p₁ → e₁ | … | pₙ → eₙ } ⇓ Err E
e₁ ⇓ Ok v₁
v 'matches' p₁ ⇝ Succ (x₁ ↦ v₁ · … · xₘ ↦ vₘ · ε)
e₁[x₁ ↦ v₁, …, xₘ ↦ vₘ] ⇓ r
—————————————————————————————————————————————————————————————————————— EvExpCaseSucc
'case' e₁ 'of' { p₁ → e₁ | … | pₙ → eₙ } ⇓ r
e₁ ⇓ Ok v₁ v₁ 'matches' p₁ ⇝ Fail
'case' v₁ 'of' { p₂ → e₂ … | pₙ → eₙ } ⇓ r
—————————————————————————————————————————————————————————————————————— EvExpCaseFail
'case' e₁ 'of' { p₁ → e₁ | p₂ → e₂ | … | pₙ → eₙ } ⇓ r
e₁ ⇓ Ok v₁ v 'matches' p ⇝ Fail
—————————————————————————————————————————————————————————————————————— EvExpCaseEmpty
'case' e₁ 'of' { p → e } ⇓ Err "match error"
eₕ ⇓ Err E
—————————————————————————————————————————————————————————————————————— EvExpConsErr1
'Cons' @τ eₕ eₜ ⇓ Err E
eₕ ⇓ Ok vₕ
eₜ ⇓ Err E
—————————————————————————————————————————————————————————————————————— EvExpConsErr2
'Cons' @τ eₕ eₜ ⇓ Err E
eₕ ⇓ Ok vₕ
eₜ ⇓ Ok vₜ
—————————————————————————————————————————————————————————————————————— EvExpCons
'Cons' @τ eₕ eₜ ⇓ Ok ('Cons' @τ vₕ vₜ)
e ⇓ Err E
—————————————————————————————————————————————————————————————————————— EvExpSomeErr
'Some' @τ e ⇓ Err E
e ⇓ Ok v
—————————————————————————————————————————————————————————————————————— EvExpSome
'Some' @τ e ⇓ Ok ('Some' @τ v)
𝕋(F) = ∀ (α₁: k₁) … ∀ (αₘ: kₘ). σ₁ → … → σₙ → σ
e₁ ⇓ Ok v₁
⋮
eᵢ₋₁ ⇓ Ok vᵢ₋₁
eᵢ ⇓ Err E
—————————————————————————————————————————————————————————————————————— EvExpBuiltinErr
F @τ₁ … @τₘ e₁ … eₙ ⇓ Err E
𝕋(F) = ∀ (α₁: k₁) … ∀ (αₘ: kₘ). σ₁ → … → σₙ → σ
e₁ ⇓ Ok v₁
⋮
eₙ ⇓ Ok vₙ
—————————————————————————————————————————————————————————————————————— EvExpBuiltin
F @τ₁ … @τₘ e₁ … eₙ ⇓ 𝕆(F @τ₁ … @τₘ v₁ … vₙ)
'val' W : τ ↦ e ∈ 〚Ξ〛Mod
e ⇓ r
—————————————————————————————————————————————————————————————————————— EvExpVal
Mod:W ⇓ r
e₁ ⇓ Ok v₁
⋮
eᵢ₋₁ ⇓ Ok vᵢ₋₁
eᵢ ⇓ Err E
—————————————————————————————————————————————————————————————————————— EvExpRecConErr
Mod:T @τ₁ … @τₘ {f₁ = e₁, …, fₙ = eₙ} ⇓ Err E
e₁ ⇓ Ok v₁
⋮
eₙ ⇓ Ok vₙ
—————————————————————————————————————————————————————————————————————— EvExpRecCon
Mod:T @τ₁ … @τₘ {f₁ = e₁, …, fₙ = eₙ}
⇓
Ok (Mod:T @τ₁ … @τₘ {f₁ = v₁, …, fₙ = ₙ})
e ⇓ Err E
—————————————————————————————————————————————————————————————————————— EvExpRecProjErr
Mod:T @τ₁ … @τₘ {fᵢ} e ⇓ Err E
e ⇓ Ok (Mod:T @τ₁ … @τₘ {f₁= v₁, …, fᵢ= vᵢ, …, fₙ= vₙ})
—————————————————————————————————————————————————————————————————————— EvExpRecProj
Mod:T @τ₁ … @τₘ {fᵢ} e ⇓ Ok vᵢ
e ⇓ Err E
—————————————————————————————————————————————————————————————————————— EvExpRecUpdErr1
Mod:T @τ₁ … @τₘ { e 'with' fᵢ = eᵢ } ⇓ Err E
e ⇓ Ok (Mod:T @τ₁ … @τₘ {f₁= v₁, …, fᵢ= vᵢ, …, fₙ= vₙ})
eᵢ ⇓ Err E
—————————————————————————————————————————————————————————————————————— EvExpRecUpdErr2
Mod:T @τ₁ … @τₘ { e 'with' fᵢ = eᵢ } ⇓ Err E
e ⇓ Ok (Mod:T @τ₁ … @τₘ {f₁= v₁, …, fᵢ= vᵢ, …, fₙ= vₙ})
eᵢ ⇓ Ok vᵢ'
—————————————————————————————————————————————————————————————————————— EvExpRecUpd
Mod:T @τ₁ … @τₘ { e 'with' fᵢ = eᵢ }
⇓
Ok (Mod:T @τ₁ … @τₘ {f₁= v₁, …, fᵢ= vᵢ', …, fₙ= vₙ})
e ⇓ Err E
—————————————————————————————————————————————————————————————————————— EvExpVarConErr
Mod:T:V @τ₁ … @τₙ e ⇓ Err E
e ⇓ Ok v
—————————————————————————————————————————————————————————————————————— EvExpVarCon
Mod:T:V @τ₁ … @τₙ e ⇓ Ok (Mod:T:V @τ₁ … @τₙ v)
e₁ ⇓ Ok v₁
⋮
eᵢ₋₁ ⇓ Ok vᵢ₋₁
eᵢ ⇓ Err E
—————————————————————————————————————————————————————————————————————— EvExpStructConErr
⟨f₁ = e₁, …, fₙ = eₙ⟩ ⇓ Err E
e₁ ⇓ Ok v₁
⋮
eₙ ⇓ Ok vₙ
[f₁, …, fₙ] sorts lexicographically to [fⱼ₁, …, fⱼₙ]
—————————————————————————————————————————————————————————————————————— EvExpStructCon
⟨f₁ = e₁, …, fₙ = eₙ⟩ ⇓ Ok ⟨fⱼ₁ = vⱼ₁, …, fⱼₙ = vⱼₙ⟩
e ⇓ Err E
—————————————————————————————————————————————————————————————————————— EvExpStructProj
e.fᵢ ⇓ Err E
e ⇓ Ok ⟨ f₁= v₁, …, fᵢ = vᵢ, …, fₙ = vₙ ⟩
—————————————————————————————————————————————————————————————————————— EvExpStructProj
e.fᵢ ⇓ Ok vᵢ
e ⇓ Err E
—————————————————————————————————————————————————————————————————————— EvExpStructUpdErr1
⟨ e 'with' fᵢ = eᵢ ⟩ ⇓ Err E
e ⇓ Ok ⟨ f₁= v₁, …, fᵢ = vᵢ, …, fₙ = vₙ ⟩
eᵢ ⇓ Err E
—————————————————————————————————————————————————————————————————————— EvExpStructUpdErr2
⟨ e 'with' fᵢ = eᵢ ⟩ ⇓ Err E
e ⇓ Ok ⟨ f₁= v₁, …, fᵢ = vᵢ, …, fₙ = vₙ ⟩
eᵢ ⇓ Ok vᵢ'
—————————————————————————————————————————————————————————————————————— EvExpStructUpd
⟨ e 'with' fᵢ = eᵢ ⟩
⇓
Ok ⟨ f₁= v₁, …, fᵢ= vᵢ', …, fₙ= vₙ ⟩
e ⇓ Err E
—————————————————————————————————————————————————————————————————————— EvExpThrowErr
'throw' @σ @τ e ⇓ Err E
e ⇓ Ok v
—————————————————————————————————————————————————————————————————————— EvExpThrow
'throw' @σ @τ e ⇓ Err (Throw ('to_any_exception' @τ v))
e ⇓ Err E
—————————————————————————————————————————————————————————————————————— EvExpToAnyExceptionErr
'to_any_exception' @τ e ⇓ Err E
e ⇓ Ok v
—————————————————————————————————————————————————————————————————————— EvExpToAnyException
'to_any_exception' @τ e ⇓ Ok ('to_any_exception' @τ v)
e ⇓ Err E
—————————————————————————————————————————————————————————————————————— EvExpFromAnyExceptionErr
'from_any_exception' @τ e ⇓ Err E
e ⇓ Ok ('to_any_exception' @σ v)
σ ≠ τ
—————————————————————————————————————————————————————————————————————— EvExpFromAnyExceptionNone
'from_any_exception' @τ e ⇓ Ok ('None' @τ)
e ⇓ Ok ('to_any_exception' @σ v)
σ = τ
—————————————————————————————————————————————————————————————————————— EvExpFromAnyExceptionSome
'from_any_exception' @τ e ⇓ Ok ('Some' @τ v)
e ⇓ Err E
—————————————————————————————————————————————————————————————————————— EvExpAnyExceptionMessageErr
'ANY_EXCEPTION_MESSAGE' e ⇓ Err E
e ⇓ Ok ('to_any_exception' @Mod:T v)
'exception' T ↦ { 'message' eₘ } ∈ 〚Ξ〛Mod
eₘ v ⇓ Err E
—————————————————————————————————————————————————————————————————————— EvExpAnyExceptionMessageRecordErr
'ANY_EXCEPTION_MESSAGE' e ⇓ Err E
e ⇓ Ok ('to_any_exception' @Mod:T v)
'exception' T ↦ { 'message' eₘ } ∈ 〚Ξ〛Mod
eₘ v ⇓ Ok vₘ
—————————————————————————————————————————————————————————————————————— EvExpAnyExceptionMessageRecord
'ANY_EXCEPTION_MESSAGE' e ⇓ Ok vₘ
e ⇓ Err E
—————————————————————————————————————————————————————————————————————— EvExpToInterfaceErr [Daml-LF ≥ 1.dev]
'to_interface' @Mod:I @Mod':T e ⇓ Err E
e ⇓ Ok v
—————————————————————————————————————————————————————————————————————— EvExpToInterface [Daml-LF ≥ 1.dev]
'to_interface' @Mod:I @Mod':T e ⇓ Ok ('to_interface' @Mod:I @Mod':T v)
e ⇓ Err E
—————————————————————————————————————————————————————————————————————— EvExpFromInterfaceErr [Daml-LF ≥ 1.dev]
'from_interface' @Mod:I @Mod':T e ⇓ Err E
e ⇓ Ok ('to_interface' @Mod:I @Mod'':T' v)
Mod':T ≠ Mod'':T'
—————————————————————————————————————————————————————————————————————— EvExpFromInterfaceNone [Daml-LF ≥ 1.dev]
'from_interface' @Mod:I @Mod':T e ⇓ Ok ('None' @Mod':T)
e ⇓ Ok ('to_interface' @Mod:I @Mod':T v)
—————————————————————————————————————————————————————————————————————— EvExpFromInterfaceSome [Daml-LF ≥ 1.dev]
'from_interface' @Mod:I @Mod':T e ⇓ Ok ('Some' @Mod':T v)
e₁ ⇓ Err E
—————————————————————————————————————————————————————————————————————— EvExpUnsafeFromInterfaceErr1 [Daml-LF ≥ 1.dev]
'unsafe_from_interface' @Mod:I @Mod':T e₁ e₂ ⇓ Err E
e₁ ⇓ Ok cid
e₂ ⇓ Err E
—————————————————————————————————————————————————————————————————————— EvExpUnsafeFromInterfaceErr2 [Daml-LF ≥ 1.dev]
'unsafe_from_interface' @Mod:I @Mod':T e₁ e₂ ⇓ Err E
e₁ ⇓ Ok cid
e₂ ⇓ Ok ('to_interface' @Mod:I @Mod'':T' v)
Mod':T ≠ Mod'':T'
—————————————————————————————————————————————————————————————————————— EvExpUnsafeFromInterfaceErr3 [Daml-LF ≥ 1.dev]
'unsafe_from_interface' @Mod:I @Mod':T e₁ e₂
⇓
Err (Fatal "wrongly typed contract {cid} expected {Mod':T} got {Mod'':T'}")
e₁ ⇓ Ok cid
e₂ ⇓ Ok ('to_interface' @Mod:I @Mod':T v)
—————————————————————————————————————————————————————————————————————— EvExpUnsafeFromInterface [Daml-LF ≥ 1.dev]
'unsafe_from_interface' @Mod:I @Mod':T e₁ e₂ ⇓ Ok v
e ⇓ Err E
—————————————————————————————————————————————————————————————————————— EvExpCallInterfaceErr [Daml-LF ≥ 1.dev]
'call_interface' @Mod:I f e ⇓ Err E
e ⇓ Ok ('to_interface' @Mod:I @Mod':T v)
'tpl' (x : T) ↦ { …, 'implements' Mod:I { 'methods' { …, f = eₘ, … }, … }, … } ∈ 〚Ξ〛Mod'
eₘ v ⇓ r
—————————————————————————————————————————————————————————————————————— EvExpCallInterface [Daml-LF ≥ 1.dev]
'call_interface' @Mod:I f e ⇓ r
e ⇓ Err E
—————————————————————————————————————————————————————————————————————— EvExpToRequiredInterfaceErr [Daml-LF ≥ 1.dev]
'to_required_interface' @Mod₁:I₁ @Mod₂:I₂ e ⇓ Err E
e ⇓ Ok ('to_interface' @Mod₂:I₂ @Mod':T v)
—————————————————————————————————————————————————————————————————————— EvExpToRequiredInterface [Daml-LF ≥ 1.dev]
'to_required_interface' @Mod₁:I₁ @Mod₂:I₂ e ⇓ Ok ('to_interface' @Mod₁:I₁ @Mod':T v)
e ⇓ Err E
—————————————————————————————————————————————————————————————————————— EvExpFromRequiredInterfaceErr [Daml-LF ≥ 1.dev]
'from_required_interface' @Mod₁:I₁ @Mod₂:I₂ e ⇓ Err E
e ⇓ Ok ('to_interface' @Mod₁:I₁ @Mod':T v)
Mod':T does not implement interface Mod₂:I₂
—————————————————————————————————————————————————————————————————————— EvExpFromRequiredInterfaceNone [Daml-LF ≥ 1.dev]
'from_required_interface' @Mod₁:I₁ @Mod₂:I₂ e ⇓ Ok ('None' @Mod₂:I₂)
e ⇓ Ok ('to_interface' @Mod₁:I₁ @Mod':T v)
'tpl' (x : T) ↦ { …, 'implements' Mod₂:I₂ { … }, … } ∈ 〚Ξ〛Mod'
—————————————————————————————————————————————————————————————————————— EvExpFromRequiredInterfaceSome [Daml-LF ≥ 1.dev]
'from_required_interface' @Mod₁:I₁ @Mod₂:I₂ e ⇓ Ok ('Some' @Mod₂:I₂ ('to_interface' @Mod₂:I₂ @Mod':T v))
e₁ ⇓ Err E
—————————————————————————————————————————————————————————————————————— EvExpUnsafeFromRequiredInterfaceErr1 [Daml-LF ≥ 1.dev]
'unsafe_from_required_interface' @Mod₁:I₁ @Mod₂:I₂ e₁ e₂ ⇓ Err E
e₁ ⇓ Ok cid
e₂ ⇓ Err E
—————————————————————————————————————————————————————————————————————— EvExpUnsafeFromRequiredInterfaceErr2 [Daml-LF ≥ 1.dev]
'unsafe_from_required_interface' @Mod₁:I₁ @Mod₂:I₂ e₁ e₂ ⇓ Err E
e₁ ⇓ Ok cid
e₂ ⇓ Ok ('to_interface' @Mod₁:I₁ @Mod':T v)
Mod':T does not implement interface Mod₂:I₂
—————————————————————————————————————————————————————————————————————— EvExpUnsafeFromRequiredInterfaceErr3 [Daml-LF ≥ 1.dev]
'unsafe_from_required_interface' @Mod₁:I₁ @Mod₂:I₂ e₁ e₂
⇓
Err (Fatal "wrongly typed contract {cid} expected {Mod₂:I₂} got {Mod':T}")
e₁ ⇓ Ok cid
e₂ ⇓ Ok ('to_interface' @Mod₁:I₁ @Mod':T v)
'tpl' (x : T) ↦ { …, 'implements' Mod₂:I₂ { … }, … } ∈ 〚Ξ〛Mod'
—————————————————————————————————————————————————————————————————————— EvExpUnsafeFromRequiredInterface [Daml-LF ≥ 1.dev]
'unsafe_from_required_interface' @Mod₁:I₁ @Mod₂:I₂ e₁ e₂ ⇓ Ok ('to_interface' @Mod₂:I₂ @Mod':T v)
e ⇓ Err E
—————————————————————————————————————————————————————————————————————— EvExpInterfaceTypeRepErr [Daml-LF ≥ 1.dev]
'interface_typerep' @Mod:I e ⇓ Err E
e ⇓ Ok ('to_interface' @Mod:I @Mod':T v)
—————————————————————————————————————————————————————————————————————— EvExpInterfaceTypeRep [Daml-LF ≥ 1.dev]
'interface_typerep' @Mod:I e ⇓ Ok ('type_rep' @Mod':T)
e ⇓ Err E
—————————————————————————————————————————————————————————————————————— EvExpInterfaceSignatoryErr [Daml-LF ≥ 1.dev]
'interface_signatory' @Mod:I e ⇓ Err E
e ⇓ Ok ('to_interface' @Mod:I @Mod':T v)
'tpl' (x : T) ↦ { …, 'signatories' e', … } ∈ 〚Ξ〛Mod'
e' [x ↦ v] ⇓ r
—————————————————————————————————————————————————————————————————————— EvExpInterfaceSignatory [Daml-LF ≥ 1.dev]
'interface_signatory' @Mod:I e ⇓ r
e ⇓ Err E
—————————————————————————————————————————————————————————————————————— EvExpInterfaceObserverErr [Daml-LF ≥ 1.dev]
'interface_observer' @Mod:I e ⇓ Err E
e ⇓ Ok ('to_interface' @Mod:I @Mod':T v)
'tpl' (x : T) ↦ { …, 'observers' e', … } ∈ 〚Ξ〛Mod'
e' [x ↦ v] ⇓ r
—————————————————————————————————————————————————————————————————————— EvExpInterfaceObserver [Daml-LF ≥ 1.dev]
'interface_observer' @Mod:I e ⇓ r
e ⇓ Err E
—————————————————————————————————————————————————————————————————————— EvExpUpPureErr
'pure' @τ e ⇓ Err E
e ⇓ Ok v
—————————————————————————————————————————————————————————————————————— EvExpUpPure
'pure' @τ e ⇓ Ok ('pure' @τ v)
e₁ ⇓ Err E
—————————————————————————————————————————————————————————————————————— EvExpUpBindErr
'bind' x₁ : τ₁ ← e₁ 'in' e₂ ⇓ Err E
e₁ ⇓ Ok v₁
—————————————————————————————————————————————————————————————————————— EvExpUpBind
'bind' x₁ : τ₁ ← e₁ 'in' e₂
⇓
Ok ('bind' x₁ : τ₁ ← v₁ 'in' e₂)
e ⇓ Err E
—————————————————————————————————————————————————————————————————————— EvExpUpCreateErr
'create' @Mod:T e ⇓ Err E
e ⇓ Ok v
—————————————————————————————————————————————————————————————————————— EvExpUpCreate
'create' @Mod:T e ⇓ Ok ('create' @Mod:T v)
e ⇓ Err E
—————————————————————————————————————————————————————————————————————— EvExpUpCreateInterfaceErr [Daml-LF ≥ 1.dev]
'create_interface' @Mod:I e ⇓ Err E
e ⇓ Ok v
—————————————————————————————————————————————————————————————————————— EvExpUpCreateInterface [Daml-LF ≥ 1.dev]
'create_interface' @Mod:I e ⇓ Ok ('create_interface' @Mod:I v)
e ⇓ Err E
—————————————————————————————————————————————————————————————————————— EvExpUpFetchErr
'fetch' @Mod:T e ⇓ Err E
e ⇓ Ok v
—————————————————————————————————————————————————————————————————————— EvExpUpFetch
'fetch' @Mod:T e ⇓ Ok ('fetch' @Mod:T v)
e ⇓ Err E
—————————————————————————————————————————————————————————————————————— EvExpUpFetchInterface [Daml-LF ≥ 1.dev]
'fetch_interface' @Mod:I e ⇓ Err E
e ⇓ Ok v
—————————————————————————————————————————————————————————————————————— EvExpUpFetchInterface [Daml-LF ≥ 1.dev]
'fetch_interface' @Mod:I e ⇓ Ok ('fetch_interface' @Mod:I v)
e₁ ⇓ Err E
—————————————————————————————————————————————————————————————————————— EvExpUpExerciseErr1
'exercise' @Mod:T Ch e₁ e₂ ⇓ Err E
e₁ ⇓ Ok v₁
e₂ ⇓ Err E
—————————————————————————————————————————————————————————————————————— EvExpUpExerciseErr2
'exercise' @Mod:T Ch e₁ e₂ ⇓ Err E
e₁ ⇓ Ok v₁
e₂ ⇓ Ok v₂
—————————————————————————————————————————————————————————————————————— EvExpUpExercise
'exercise' @Mod:T Ch e₁ e₂
⇓
Ok ('exercise' @Mod:T Ch v₁ v₂)
e₁ ⇓ Err E
—————————————————————————————————————————————————————————————————————— EvExpUpExerciseByKeyErr1
'exercise_by_key' @Mod:T Ch e₁ e₂ ⇓ Err E
e₁ ⇓ Ok v₁
e₂ ⇓ Err E
—————————————————————————————————————————————————————————————————————— EvExpUpExerciseByKeyErr2
'exercise_by_key' @Mod:T Ch e₁ e₂ ⇓ Err E
e₁ ⇓ Ok v₁
e₂ ⇓ Ok v₂
—————————————————————————————————————————————————————————————————————— EvExpUpExerciseByKey
'exercise_by_key' @Mod:T Ch e₁ e₂
⇓
Ok ('exercise_by_key' @Mod:T Ch v₁ v₂)
e₁ ⇓ Err E
—————————————————————————————————————————————————————————————————————— EvExpUpExerciseInterfaceErr1 [Daml-LF ≥ 1.dev]
'exercise_interface' @Mod:T Ch e₁ e₂ e₃ ⇓ Err E
e₁ ⇓ Ok v₁
e₂ ⇓ Err E
—————————————————————————————————————————————————————————————————————— EvExpUpExerciseInterfaceErr2 [Daml-LF ≥ 1.dev]
'exercise_interface' @Mod:T Ch e₁ e₂ e₃ ⇓ Err E
e₁ ⇓ Ok v₁
e₂ ⇓ Ok v₂
e₃ ⇓ Err E
—————————————————————————————————————————————————————————————————————— EvExpUpExerciseInterfaceErr3 [Daml-LF ≥ 1.dev]
'exercise_interface' @Mod:T Ch e₁ e₂ e₃ ⇓ Err E
e₁ ⇓ Ok v₁
e₂ ⇓ Ok v₂
e₃ ⇓ Ok v₃
—————————————————————————————————————————————————————————————————————— EvExpUpExerciseInterface [Daml-LF ≥ 1.dev]
'exercise_interface' @Mod:T Ch e₁ e₂ e₃ ⇓ Ok ('exercise_interface' @Mod:T Ch v₁ v₂ v₃)
e ⇓ Err E
—————————————————————————————————————————————————————————————————————— EvExpUpFetchByKeyErr
'fetch_by_key' @Mod:T e ⇓ Err E
e ⇓ Ok v
—————————————————————————————————————————————————————————————————————— EvExpUpFetchByKey
'fetch_by_key' @Mod:T e
⇓
Ok ('fetch_by_key' @Mod:T v)
e ⇓ Err E
—————————————————————————————————————————————————————————————————————— EvExpUpLookupByKeyErr
'lookup_by_key' @Mod:T e ⇓ Err E
e ⇓ Ok v
—————————————————————————————————————————————————————————————————————— EvExpUpLookupByKey
'lookup_by_key' @Mod:T e
⇓
Ok ('lookup_by_key' @Mod:T v)
—————————————————————————————————————————————————————————————————————— EvExpUpTryCatch
'try' @τ e₁ 'catch' x. e₂
⇓
Ok ('try' @τ e₁ 'catch' x. e₂)
e ⇓ Err E
—————————————————————————————————————————————————————————————————————— EvExpScenarioPureErr
'spure' @τ e ⇓ Err E
e ⇓ Ok v
—————————————————————————————————————————————————————————————————————— EvExpScenarioPure
'spure' @τ e ⇓ Ok ('spure' @τ v)
e₁ ⇓ Err E
—————————————————————————————————————————————————————————————————————— EvExpScenarioBindErr
'sbind' x₁ : τ₁ ← e₁ 'in' e₂ ⇓ Err E
e₁ ⇓ Ok v₁
—————————————————————————————————————————————————————————————————————— EvExpScenarioBind
'sbind' x₁ : τ₁ ← e₁ 'in' e₂
⇓
Ok ('sbind' x₁ : τ₁ ← v₁ 'in' e₂)
e ⇓ Err E
—————————————————————————————————————————————————————————————————————— EvExpScenarioCommitErr1
'commit' @τ e u ⇓ Err E
e ⇓ Ok v₁
u ⇓ Err E
—————————————————————————————————————————————————————————————————————— EvExpScenarioCommitErr2
'commit' @τ e u ⇓ Err E
e ⇓ Ok v₁
u ⇓ Ok v₂
—————————————————————————————————————————————————————————————————————— EvExpScenarioCommit
'commit' @τ e u ⇓ Ok ('commit' @τ v₁ v₂)
e ⇓ Err E
—————————————————————————————————————————————————————————————————————— EvExpScenarioMustFailAtErr1
'must_fail_at' @τ e u ⇓ Err E
e ⇓ Ok v₁
u ⇓ Err E
—————————————————————————————————————————————————————————————————————— EvExpScenarioMustFailAtErr2
'must_fail_at' @τ e u ⇓ Err E
e ⇓ Ok v₁
u ⇓ Ok v₂
—————————————————————————————————————————————————————————————————————— EvExpScenarioMustFailAt
'must_fail_at' @τ e u ⇓ Ok ('must_fail_at' @τ v₁ v₂)
e ⇓ Err E
—————————————————————————————————————————————————————————————————————— EvExpScenarioPassErr
'pass' e ⇓ Err E
e ⇓ Ok v
—————————————————————————————————————————————————————————————————————— EvExpScenarioPass
'pass' e ⇓ Ok ('pass' v)
e ⇓ Err E
—————————————————————————————————————————————————————————————————————— EvExpScenarioGetPartyErr
'sget_party' e ⇓ Err E
e ⇓ Ok v
—————————————————————————————————————————————————————————————————————— EvExpScenarioGetParty
'sget_party' e ⇓ Ok ('sget_party' v)
Note that the rules are designed such that for every expression, there is at
most one possible outcome. In other words, results are deterministic. When
two or more derivations apply for the same expression, they yield the same result. For
example, the rules ``EvValue`` and ``EvExpUpPure`` both apply to the expression
``'pure' @Int64 10``, yielding the same result ``Ok ('pure' @Int64 10)``.
In addition, update expressions only evaluate to update values, and scenario
expressions only evaluate to scenario values.
Well-formed record construction expressions evaluate the fields in the order
they were defined in the type. This is implied by the type system, which forces
well-formed record construction expressions to specify the fields in the same
order as in the type definition, and the ``EvExpRecCon`` rules, which evaluate
fields in the order they are given.
These semantics do not require, nor forbid, the cacheing or memoization of
evaluation results for top-level values, or for any other value. This is
considered an implementation detail.
Update interpretation
~~~~~~~~~~~~~~~~~~~~~
We define the operational semantics of the update interpretation
against the ledger model described in the `Daml Ledger Model
<https://docs.daml.com/concepts/ledger-model/index.html>`_.
Update semantics use the predicate ``=ₛ`` to compare two lists of
party literals as if the lists were sets.
..
(RH) We probably do not need to be so explicit
Formally the predicate is defined as follows:::
—————————————————————————————————————— InHead
v in (Cons @Party v vₜ)
v in vₜ
—————————————————————————————————————— InTail
v in (Cons @Party vₕ vₜ)
—————————————————————————————————————— NilSubset
(Nil @Party) subset v
vₕ in v vₜ subset v
—————————————————————————————————————— ConsSubset
(Cons @Party vₕ vₜ) subset v
v₁ subset v₂ v₂ subset v₁
—————————————————————————————————————— SetEquality
v₁ =ₛ v₂
The operational semantics are restricted to update statements which
are values according to ``⊢ᵥᵤ``. In this section, all updates denoted
by the symbol ``u`` will be implicit values. In practice, what this
means is that an interpreter implementing these semantics will need to
evaluate the update expression first according to the operational
semantics for expressions, before interpreting the update.
The result of an update is a value accompanied by a ledger transaction
as described by the ledger model::
Contracts on the ledger
Contract
::= (cid, Mod:T, vₜ) -- vₜ must be of type Mod:T
Global contract Key
GlobalKey
::= (Mod:T, vₖ)
Ledger actions
act
::= 'create' Contract
| 'exercise' v Contract ChKind tr -- v must be of type 'List' 'Party'
Ledger transaction nodes
trnode
::= act
| 'rollback' tr
Ledger transactions
tr
::= trnode₁ · … · trnodeₙ
Contract states
ContractState
::= 'active'
| 'inactive'
Contract stores
st ∈ finite map from cid to (Mod:T, v, ContractState)
Contract key index
keys ∈ finite injective map from GlobalKey to cid
Contract state
S ::= (st, keys)
Update result
ur ::= (Ok v, tr) ‖ S
| (Err E, tr)
┌──────────────┐
Big-step update interpretation │ u ‖ S₀ ⇓ᵤ ur │ (u is an update value)
└──────────────┘
—————————————————————————————————————————————————————————————————————— EvUpdPure
'pure' @τ v ‖ (st, keys) ⇓ᵤ (Ok v, ε) ‖ (st, keys)
u₁ ‖ S₀ ⇓ᵤ (Err E, tr)
—————————————————————————————————————————————————————————————————————— EvUpdBindErr1
'bind' x : τ ← u₁ ; e₂ ‖ S₀ ⇓ᵤ (Err E, tr)
u₁ ‖ S₀ ⇓ᵤ (Ok v₁, tr₁) ‖ S₁
e₂[x ↦ v₁] ⇓ Err E
—————————————————————————————————————————————————————————————————————— EvUpdBindErr2
'bind' x : τ ← u₁ ; e₂ ‖ S₀ ⇓ᵤ (Err E, tr₁)
u₁ ‖ S₀ ⇓ᵤ (Ok v₁, tr₁) ‖ S₁
e₂[x ↦ v₁] ⇓ Ok u₂
u₂ ‖ S₁ ⇓ᵤ (Err E, tr₂)
—————————————————————————————————————————————————————————————————————— EvUpdBindErr3
'bind' x : τ ← u₁ ; e₂ ‖ S₀ ⇓ᵤ (Err E, tr₁ ⋅ tr₂)
u₁ ‖ S₀ ⇓ᵤ Ok (v₁, tr₁) ‖ S₁
e₂[x ↦ v₁] ⇓ Ok u₂
u₂ ‖ S₁ ⇓ᵤ Ok (v₂, tr₂) ‖ S₂
—————————————————————————————————————————————————————————————————————— EvUpdBind
'bind' x : τ ← u₁ ; e₂ ‖ S₀
⇓ᵤ
(Ok v₂, tr₁ · tr₂) ‖ S₂
'tpl' (x : T) ↦ { 'precondition' eₚ, … } ∈ 〚Ξ〛Mod
eₚ[x ↦ vₜ] ⇓ Err E
—————————————————————————————————————————————————————————————————————— EvUpdCreateErr1a
'create' @Mod:T vₜ ‖ S₀ ⇓ᵤ (Err E, ε)
'tpl' (x : T) ↦ { 'precondition' eₚ, … } ∈ 〚Ξ〛Mod
eₚ[x ↦ vₜ] ⇓ Ok 'False'
—————————————————————————————————————————————————————————————————————— EvUpdCreateFail1a
'create' @Mod:T vₜ ‖ S₀
⇓ᵤ
(Err (Fatal "Precondition failed on {Mod:T}."), ε)
'tpl' (x : T) ↦ { 'precondition' eₚ, …,
'implements' Mod₁:I₁ { … }, …, 'implements' Modᵢ:Iᵢ { … }, … } ∈ 〚Ξ〛Mod
eₚ[x ↦ vₜ] ⇓ Ok 'True'
'interface' (x₁ : I₁) ↦ { …, 'precondition' e₁ₚ, … } ∈ 〚Ξ〛Mod₁
e₁ₚ[x₁ ↦ 'to_interface' @Mod₁:I₁ @Mod:T vₜ] ⇓ Ok 'True'
'interface' (x₂ : I₂) ↦ { …, 'precondition' e₂ₚ, … } ∈ 〚Ξ〛Mod₂
e₂ₚ[x₂ ↦ 'to_interface' @Mod₂:I₂ @Mod:T vₜ] ⇓ Ok 'True'
…
'interface' (xᵢ : Iᵢ) ↦ { …, 'precondition' eᵢₚ, … } ∈ 〚Ξ〛Modᵢ
eᵢₚ[x₂ ↦ 'to_interface' @Modᵢ:Iᵢ @Mod:T vₜ] ⇓ Err E
—————————————————————————————————————————————————————————————————————— EvUpdCreateErr1b
'create' @Mod:T vₜ ‖ S₀ ⇓ᵤ (Err E, ε)
'tpl' (x : T) ↦ { 'precondition' eₚ, …,
'implements' Mod₁:I₁ { … }, …, 'implements' Modᵢ:Iᵢ { … }, … } ∈ 〚Ξ〛Mod
eₚ[x ↦ vₜ] ⇓ Ok 'True'
'interface' (x₁ : I₁) ↦ { …, 'precondition' e₁ₚ, … } ∈ 〚Ξ〛Mod₁
e₁ₚ[x₁ ↦ 'to_interface' @Mod₁:I₁ @Mod:T vₜ] ⇓ Ok 'True'
'interface' (x₂ : I₂) ↦ { …, 'precondition' e₂ₚ, … } ∈ 〚Ξ〛Mod₂
e₂ₚ[x₂ ↦ 'to_interface' @Mod₂:I₂ @Mod:T vₜ] ⇓ Ok 'True'
…
'interface' (xᵢ : Iᵢ) ↦ { …, 'precondition' eᵢₚ, … } ∈ 〚Ξ〛Modᵢ
eᵢₚ[xᵢ ↦ 'to_interface' @Modᵢ:Iᵢ @Mod:T vₜ] ⇓ Ok 'False'
—————————————————————————————————————————————————————————————————————— EvUpdCreateFail1b
'create' @Mod:T vₜ ‖ S₀
⇓ᵤ
(Err (Fatal "Precondition failed on {Mod:T}."), ε)
'tpl' (x : T) ↦ { 'precondition' eₚ, 'agreement' eₐ, …
'implements' Mod₁:I₁ { … }, …, 'implements' Modₖ:Iₖ { … } } ∈ 〚Ξ〛Mod
eₚ[x ↦ vₜ] ⇓ Ok 'True'
'interface' (x₁ : I₁) ↦ { …, 'precondition' e₁ₚ, … } ∈ 〚Ξ〛Mod₁
e₁ₚ[x₁ ↦ 'to_interface' @Mod₁:I₁ @Mod:T vₜ] ⇓ Ok 'True'
…
'interface' (xₖ : Iₖ) ↦ { …, 'precondition' eₖₚ, … } ∈ 〚Ξ〛Modₖ
eₖₚ[xₖ ↦ 'to_interface' @Modₖ:Iₖ @Mod:T vₜ] ⇓ Ok 'True'
eₐ[x ↦ vₜ] ⇓ Err E
—————————————————————————————————————————————————————————————————————— EvUpdCreateErr2
'create' @Mod:T vₜ ‖ (st₀, keys₀) ⇓ᵤ (Err E, ε)
'tpl' (x : T) ↦ { 'precondition' eₚ, 'agreement' eₐ, 'signatories' eₛ, …
'implements' Mod₁:I₁ { … }, …, 'implements' Modₖ:Iₖ { … } } ∈ 〚Ξ〛Mod
eₚ[x ↦ vₜ] ⇓ Ok 'True'
'interface' (x₁ : I₁) ↦ { …, 'precondition' e₁ₚ, … } ∈ 〚Ξ〛Mod₁
e₁ₚ[x₁ ↦ 'to_interface' @Mod₁:I₁ @Mod:T vₜ] ⇓ Ok 'True'
…
'interface' (xₖ : Iₖ) ↦ { …, 'precondition' eₖₚ, … } ∈ 〚Ξ〛Modₖ
eₖₚ[xₖ ↦ 'to_interface' @Modₖ:Iₖ @Mod:T vₜ] ⇓ Ok 'True'
eₐ[x ↦ vₜ] ⇓ Ok vₐ
eₛ[x ↦ vₜ] ⇓ Err E
—————————————————————————————————————————————————————————————————————— EvUpdCreateErr3
'create' @Mod:T vₜ ‖ (st₀, keys₀) ⇓ᵤ (Err E, ε)
'tpl' (x : T) ↦ { 'precondition' eₚ, 'agreement' eₐ,
'signatories' eₛ, 'observers' eₒ, …,
'implements' Mod₁:I₁ { … }, …, 'implements' Modₖ:Iₖ { … } } ∈ 〚Ξ〛Mod
eₚ[x ↦ vₜ] ⇓ Ok 'True'
'interface' (x₁ : I₁) ↦ { …, 'precondition' e₁ₚ, … } ∈ 〚Ξ〛Mod₁
e₁ₚ[x₁ ↦ 'to_interface' @Mod₁:I₁ @Mod:T vₜ] ⇓ Ok 'True'
…
'interface' (xₖ : Iₖ) ↦ { …, 'precondition' eₖₚ, … } ∈ 〚Ξ〛Modₖ
eₖₚ[xₖ ↦ 'to_interface' @Modₖ:Iₖ @Mod:T vₜ] ⇓ Ok 'True'
eₐ[x ↦ vₜ] ⇓ Ok vₐ
eₛ[x ↦ vₜ] ⇓ Ok vₛ
eₒ[x ↦ vₜ] ⇓ Err E
—————————————————————————————————————————————————————————————————————— EvUpdCreateErr4
'create' @Mod:T vₜ ‖ (st₀, keys₀) ⇓ᵤ (Err E, ε)
'tpl' (x : T) ↦ { 'precondition' eₚ, 'agreement' eₐ,
'signatories' eₛ, 'observers' eₒ, …,
'implements' Mod₁:I₁ { … }, …, 'implements' Modₖ:Iₖ { … } } ∈ 〚Ξ〛Mod
eₚ[x ↦ vₜ] ⇓ Ok 'True'
'interface' (x₁ : I₁) ↦ { …, 'precondition' e₁ₚ, … } ∈ 〚Ξ〛Mod₁
e₁ₚ[x₁ ↦ 'to_interface' @Mod₁:I₁ @Mod:T vₜ] ⇓ Ok 'True'
…
'interface' (xₖ : Iₖ) ↦ { …, 'precondition' eₖₚ, … } ∈ 〚Ξ〛Modₖ
eₖₚ[xₖ ↦ 'to_interface' @Modₖ:Iₖ @Mod:T vₜ] ⇓ Ok 'True'
eₐ[x ↦ vₜ] ⇓ Ok vₐ
eₛ[x ↦ vₜ] ⇓ Ok vₛ
eₒ[x ↦ vₜ] ⇓ Ok vₒ
|vₜ| > 100
—————————————————————————————————————————————————————————————————————— EvUpdCreateNestingArgErr
'create' @Mod:T vₜ ‖ (st₀, keys₀)
⇓ᵤ
(Err (Fatal "Value exceeds maximum nesting value"), ε)
'tpl' (x : T) ↦ { 'precondition' eₚ, 'agreement' eₐ,
'signatories' eₛ, 'observers' eₒ, …, 'no_key',
'implements' Mod₁:I₁ { … }, …, 'implements' Modₖ:Iₖ { … } } ∈ 〚Ξ〛Mod
eₚ[x ↦ vₜ] ⇓ Ok 'True'
'interface' (x₁ : I₁) ↦ { …, 'precondition' e₁ₚ, … } ∈ 〚Ξ〛Mod₁
e₁ₚ[x₁ ↦ 'to_interface' @Mod₁:I₁ @Mod:T vₜ] ⇓ Ok 'True'
…
'interface' (xₖ : Iₖ) ↦ { …, 'precondition' eₖₚ, … } ∈ 〚Ξ〛Modₖ
eₖₚ[xₖ ↦ 'to_interface' @Modₖ:Iₖ @Mod:T vₜ] ⇓ Ok 'True'
eₐ[x ↦ vₜ] ⇓ Ok vₐ
eₛ[x ↦ vₜ] ⇓ Ok vₛ
eₒ[x ↦ vₜ] ⇓ Ok vₒ
|vₜ| ≤ 100
cid ∉ dom(st₀)
tr = 'create' (cid, Mod:T, vₜ, 'no_key')
st₁ = st₀[cid ↦ (Mod:T, vₜ, 'active')]
—————————————————————————————————————————————————————————————————————— EvUpdCreateWithoutKeySucceed
'create' @Mod:T vₜ ‖ (st₀, keys₀)
⇓ᵤ
Ok (cid, tr) ‖ (st₁, keys₀)
'tpl' (x : T) ↦ { 'precondition' eₚ, 'agreement' eₐ,
'signatories' eₛ, 'observers' eₒ, …, 'key' @σ eₖ eₘ,
'implements' Mod₁:I₁ { … }, …, 'implements' Modₖ:Iₖ { … } } ∈ 〚Ξ〛Mod
eₚ[x ↦ vₜ] ⇓ Ok 'True'
'interface' (x₁ : I₁) ↦ { …, 'precondition' e₁ₚ, … } ∈ 〚Ξ〛Mod₁
e₁ₚ[x₁ ↦ 'to_interface' @Mod₁:I₁ @Mod:T vₜ] ⇓ Ok 'True'
…
'interface' (xₖ : Iₖ) ↦ { …, 'precondition' eₖₚ, … } ∈ 〚Ξ〛Modₖ
eₖₚ[xₖ ↦ 'to_interface' @Modₖ:Iₖ @Mod:T vₜ] ⇓ Ok 'True'
eₐ[x ↦ vₜ] ⇓ Ok vₐ
eₛ[x ↦ vₜ] ⇓ Ok vₛ
eₒ[x ↦ vₜ] ⇓ Ok vₒ
eₖ[x ↦ vₜ] ⇓ Err E
—————————————————————————————————————————————————————————————————————— EvUpdCreateWithKeyErr1
'create' @Mod:T vₜ ‖ (st₀, keys₀) ⇓ᵤ (Err E, ε)
'tpl' (x : T) ↦ { 'precondition' eₚ, 'agreement' eₐ,
'signatories' eₛ, 'observers' eₒ, …, 'key' @σ eₖ eₘ,
'implements' Mod₁:I₁ { … }, …, 'implements' Modₖ:Iₖ { … } } ∈ 〚Ξ〛Mod
eₚ[x ↦ vₜ] ⇓ Ok 'True'
'interface' (x₁ : I₁) ↦ { …, 'precondition' e₁ₚ, … } ∈ 〚Ξ〛Mod₁
e₁ₚ[x₁ ↦ 'to_interface' @Mod₁:I₁ @Mod:T vₜ] ⇓ Ok 'True'
…
'interface' (xₖ : Iₖ) ↦ { …, 'precondition' eₖₚ, … } ∈ 〚Ξ〛Modₖ
eₖₚ[xₖ ↦ 'to_interface' @Modₖ:Iₖ @Mod:T vₜ] ⇓ Ok 'True'
eₐ[x ↦ vₜ] ⇓ Ok vₐ
eₛ[x ↦ vₜ] ⇓ Ok vₛ
eₒ[x ↦ vₜ] ⇓ Ok vₒ
eₖ[x ↦ vₜ] ⇓ Ok vₖ
eₘ vₖ ⇓ Err E
—————————————————————————————————————————————————————————————————————— EvUpdCreateWithKeyErr2
'create' @Mod:T vₜ ‖ (st₀, keys₀) ⇓ᵤ (Err E, ε)
'tpl' (x : T) ↦ { 'precondition' eₚ, 'agreement' eₐ,
'signatories' eₛ, 'observers' eₒ, …, 'key' @σ eₖ eₘ,
'implements' Mod₁:I₁ { … }, …, 'implements' Modₖ:Iₖ { … } } ∈ 〚Ξ〛Mod
eₚ[x ↦ vₜ] ⇓ Ok 'True'
'interface' (x₁ : I₁) ↦ { …, 'precondition' e₁ₚ, … } ∈ 〚Ξ〛Mod₁
e₁ₚ[x₁ ↦ 'to_interface' @Mod₁:I₁ @Mod:T vₜ] ⇓ Ok 'True'
…
'interface' (xₖ : Iₖ) ↦ { …, 'precondition' eₖₚ, … } ∈ 〚Ξ〛Modₖ
eₖₚ[xₖ ↦ 'to_interface' @Modₖ:Iₖ @Mod:T vₜ] ⇓ Ok 'True'
eₐ[x ↦ vₜ] ⇓ Ok vₐ
eₛ[x ↦ vₜ] ⇓ Ok vₛ
eₒ[x ↦ vₜ] ⇓ Ok vₒ
eₖ[x ↦ vₜ] ⇓ Ok vₖ
eₘ vₖ ⇓ Ok vₘ
|vₜ| > 100
—————————————————————————————————————————————————————————————————————— EvUpdCreateWithKeyNestingArgErr
'create' @Mod:T vₜ ‖ (st₀, keys₀)
⇓ᵤ
(Err (Fatal "Value exceeds maximum nesting value"), ε)
'tpl' (x : T) ↦ { 'precondition' eₚ, 'agreement' eₐ,
'signatories' eₛ, 'observers' eₒ, …, 'key' @σ eₖ eₘ,
'implements' Mod₁:I₁ { … }, …, 'implements' Modₖ:Iₖ { … } } ∈ 〚Ξ〛Mod
eₚ[x ↦ vₜ] ⇓ Ok 'True'
'interface' (x₁ : I₁) ↦ { …, 'precondition' e₁ₚ, … } ∈ 〚Ξ〛Mod₁
e₁ₚ[x₁ ↦ 'to_interface' @Mod₁:I₁ @Mod:T vₜ] ⇓ Ok 'True'
…
'interface' (xₖ : Iₖ) ↦ { …, 'precondition' eₖₚ, … } ∈ 〚Ξ〛Modₖ
eₖₚ[xₖ ↦ 'to_interface' @Modₖ:Iₖ @Mod:T vₜ] ⇓ Ok 'True'
eₐ[x ↦ vₜ] ⇓ Ok vₐ
eₛ[x ↦ vₜ] ⇓ Ok vₛ
eₒ[x ↦ vₜ] ⇓ Ok vₒ
eₖ[x ↦ vₜ] ⇓ Ok vₖ
eₘ vₖ ⇓ Ok vₘ
|vₜ| ≤ 100
|vₖ| > 100
—————————————————————————————————————————————————————————————————————— EvUpdCreateWithKeyNestingKeyErr
'create' @Mod:T vₜ ‖ (st₀, keys₀)
⇓ᵤ
(Err (Fatal "Value exceeds maximum nesting value"), ε)
'tpl' (x : T) ↦ { 'precondition' eₚ, 'agreement' eₐ,
'signatories' eₛ, 'observers' eₒ, …, 'key' @σ eₖ eₘ,
'implements' Mod₁:I₁ { … }, …, 'implements' Modₖ:Iₖ { … } } ∈ 〚Ξ〛Mod
eₚ[x ↦ vₜ] ⇓ Ok 'True'
'interface' (x₁ : I₁) ↦ { …, 'precondition' e₁ₚ, … } ∈ 〚Ξ〛Mod₁
e₁ₚ[x₁ ↦ 'to_interface' @Mod₁:I₁ @Mod:T vₜ] ⇓ Ok 'True'
…
'interface' (xₖ : Iₖ) ↦ { …, 'precondition' eₖₚ, … } ∈ 〚Ξ〛Modₖ
eₖₚ[xₖ ↦ 'to_interface' @Modₖ:Iₖ @Mod:T vₜ] ⇓ Ok 'True'
eₐ[x ↦ vₜ] ⇓ Ok vₐ
eₛ[x ↦ vₜ] ⇓ Ok vₛ
eₒ[x ↦ vₜ] ⇓ Ok vₒ
eₖ[x ↦ vₜ] ⇓ Ok vₖ
eₘ vₖ ⇓ Ok vₘ
|vₜ| ≤ 100 |vₖ| ≤ 100
(Mod:T, vₖ) ∈ dom(keys₀)
—————————————————————————————————————————————————————————————————————— EvUpdCreateWithKeyFail
'create' @Mod:T vₜ ‖ (st₀, keys₀)
⇓ᵤ
(Err (Fatal "Mod:T template key violation"), ε)
'tpl' (x : T) ↦ { 'precondition' eₚ, 'agreement' eₐ,
'signatories' eₛ, 'observers' eₒ, …, 'key' @σ eₖ eₘ,
'implements' Mod₁:I₁ { … }, …, 'implements' Modₖ:Iₖ { … } } ∈ 〚Ξ〛Mod
eₚ[x ↦ vₜ] ⇓ Ok 'True'
'interface' (x₁ : I₁) ↦ { …, 'precondition' e₁ₚ, … } ∈ 〚Ξ〛Mod₁
e₁ₚ[x₁ ↦ 'to_interface' @Mod₁:I₁ @Mod:T vₜ] ⇓ Ok 'True'
…
'interface' (xₖ : Iₖ) ↦ { …, 'precondition' eₖₚ, … } ∈ 〚Ξ〛Modₖ
eₖₚ[xₖ ↦ 'to_interface' @Modₖ:Iₖ @Mod:T vₜ] ⇓ Ok 'True'
eₐ[x ↦ vₜ] ⇓ Ok vₐ
eₛ[x ↦ vₜ] ⇓ Ok vₛ
eₒ[x ↦ vₜ] ⇓ Ok vₒ
eₖ[x ↦ vₜ] ⇓ Ok vₖ
eₘ vₖ ⇓ Ok vₘ
|vₜ| ≤ 100 |vₖ| ≤ 100
(Mod:T, vₖ) ∉ dom(keys₀)
cid ∉ dom(st₀)
tr = 'create' (cid, Mod:T, vₜ)
st₁ = st₀[cid ↦ (Mod:T, vₜ, 'active')]
keys₁ = keys₀[(Mod:T, vₖ) ↦ cid]
—————————————————————————————————————————————————————————————————————— EvUpdCreateWithKeySucceed
'create' @Mod:T vₜ ‖ (st₀, keys₀)
⇓ᵤ
Ok (cid, tr) ‖ (st₁, keys₁)
'create' @Mod':T v ‖ S ⇓ᵤ ur
—————————————————————————————————————————————————————————————————————— EvUpdCreateInterface [Daml-LF ≥ 1.dev]
'create_interface' @Mod:I ('to_interface' @Mod:I @Mod':T v) ‖ S ⇓ᵤ ur
cid ∉ dom(st)
—————————————————————————————————————————————————————————————————————— EvUpdExercMissing
'exercise' @Mod:T Ch cid v₁ ‖ (st; keys)
⇓ᵤ
(Err (Fatal "Exercise on unknown contract"), ε)
'tpl' (x : T)
↦ { 'choices' { …, 'choice' ChKind Ch (y : 'ContractId' Mod:T) (z : τ) : σ 'by' eₚ 'observers' eₒ ↦ eₐ, … }, … } ∈ 〚Ξ〛Mod
cid ∈ dom(st₀)
st₀(cid) = (Mod':T', vₜ, 'inactive')
—————————————————————————————————————————————————————————————————————— EvUpdExercInactive
'exercise' @Mod:T Ch cid v₁ ‖ (st₀; keys₀)
⇓ᵤ
(Err (Fatal "Exercise on inactive contract"), ε)
'tpl' (x : T)
↦ { 'choices' { …, 'choice' ChKind Ch (y : 'ContractId' Mod:T) (z : τ) : σ 'by' eₚ 'observers' eₒ ↦ eₐ, … }, … } ∈ 〚Ξ〛Mod
cid ∈ dom(st₀)
st₀(cid) = (Mod':T', vₜ, 'active')
Mod:T ≠ Mod':T'
—————————————————————————————————————————————————————————————————————— EvUpdExercWrongTemplate
'exercise' @Mod:T Ch cid v₁ ‖ (st; keys₀)
⇓ᵤ
(Err (Fatal "Exercise on contract of wrong template"), ε)
'tpl' (x : T)
↦ { 'choices' { …, 'choice' ChKind Ch (y : 'ContractId' Mod:T) (z : τ) : σ 'by' eₚ 'observers' eₒ ↦ eₐ, … }, … } ∈ 〚Ξ〛Mod
cid ∈ dom(st₀)
st₀(cid) = (Mod:T, vₜ, 'active')
eₚ[x ↦ vₜ, z ↦ v₁] ⇓ Err E
—————————————————————————————————————————————————————————————————————— EvUpdExercActorEvalErr
'exercise' @Mod:T Ch cid v₁ ‖ (st₀, keys₀)
⇓ᵤ
(Err (Fatal "Choice controller evaluation failed"), ε)
'tpl' (x : T)
↦ { 'choices' { …, 'choice' ChKind Ch (y : 'ContractId' Mod:T) (z : τ) : σ 'by' eₚ 'observers' eₒ ↦ …, … }, … } ∈ 〚Ξ〛Mod
cid ∈ dom(st₀)
st₀(cid) = (Mod:T, vₜ, 'active')
eₚ[x ↦ vₜ, z ↦ v₁] ⇓ Ok vₚ
eₒ[x ↦ vₜ, z ↦ v₁] ⇓ Err E
—————————————————————————————————————————————————————————————————————— EvUpdExercObserversErr
'exercise' @Mod:T Ch cid v₁ ‖ (st₀, keys₀)
⇓ᵤ
(Err (Fatal "Choice observer evaluation failed"), ε)
'tpl' (x : T)
↦ { 'choices' { …, 'choice' ChKind Ch (y : 'ContractId' Mod:T) (z : τ) : σ 'by' eₚ 'observers' eₒ ↦ eₐ, … }, … } ∈ 〚Ξ〛Mod
cid ∈ dom(st₀)
st₀(cid) = (Mod:T, vₜ, 'active')
eₚ[x ↦ vₜ, z ↦ v₁] ⇓ Ok vₚ
eₒ[x ↦ vₜ, z ↦ v₁] ⇓ Ok vₒ
|v₁| > 100
—————————————————————————————————————————————————————————————————————— EvUpdExercNestingArgErr
'exercise' @Mod:T Ch cid v₁ ‖ (st₀, keys₀)
⇓ᵤ
(Err (Fatal "Value exceeds maximum nesting value"), ε)
'tpl' (x : T)
↦ { 'choices' { …, 'choice' ChKind Ch (y : 'ContractId' Mod:T) (z : τ) : σ 'by' eₚ 'observers' eₒ ↦ eₐ, … }, … } ∈ 〚Ξ〛Mod
cid ∈ dom(st₀)
st₀(cid) = (Mod:T, vₜ, 'active')
eₚ[x ↦ vₜ, z ↦ v₁] ⇓ Ok vₚ
eₒ[x ↦ vₜ, z ↦ v₁] ⇓ Ok vₒ
|v₁| ≤ 100
eₐ[x ↦ vₜ, y ↦ cid, z ↦ v₁] ⇓ Err E
—————————————————————————————————————————————————————————————————————— EvUpdExercBodyEvalErr
'exercise' @Mod:T Ch cid v₁ ‖ (st₀, keys₀)
⇓ᵤ
(Err E, 'exercise' vₚ (cid, Mod:T, vₜ) ChKind ε)
'tpl' (x : T)
↦ { 'choices' { …, 'choice' 'consuming' Ch (y : 'ContractId' Mod:T) (z : τ) : σ 'by' eₚ 'observers' eₒ ↦ eₐ, … }, … } ∈ 〚Ξ〛Mod
cid ∈ dom(st₀)
st₀(cid) = (Mod:T, vₜ, 'active')
eₚ[x ↦ vₜ, z ↦ v₁] ⇓ Ok vₚ
eₒ[x ↦ vₜ, z ↦ v₁] ⇓ Ok vₒ
|v₁| ≤ 100
eₐ[x ↦ vₜ, y ↦ cid, z ↦ v₁] ⇓ Ok uₐ
keys₁ = keys₀ - keys₀⁻¹(cid)
st₁ = st₀[cid ↦ (Mod:T, vₜ, 'inactive')]
uₐ ‖ (st₁, keys₁) ⇓ᵤ (Err E, tr)
—————————————————————————————————————————————————————————————————————— EvUpdExercConsumErr
'exercise' @Mod:T Ch cid v₁ ‖ (st₀, keys₀)
⇓ᵤ
(Err E, 'exercise' vₚ (cid, Mod:T, vₜ) 'consuming' tr)
'tpl' (x : T)
↦ { 'choices' { …, 'choice' 'consuming' Ch (y : 'ContractId' Mod:T) (z : τ) : σ 'by' eₚ 'observers' eₒ ↦ eₐ, … }, … } ∈ 〚Ξ〛Mod
cid ∈ dom(st₀)
st₀(cid) = (Mod:T, vₜ, 'active')
eₚ[x ↦ vₜ, z ↦ v₁] ⇓ Ok vₚ
eₒ[x ↦ vₜ, z ↦ v₁] ⇓ Ok vₒ
|v₁| ≤ 100
eₐ[x ↦ vₜ, y ↦ cid, z ↦ v₁] ⇓ Ok uₐ
keys₁ = keys₀ - keys₀⁻¹(cid)
st₁ = st₀[cid ↦ (Mod:T, vₜ, 'inactive')]
uₐ ‖ (st₁, keys₁) ⇓ᵤ Ok (vₐ, trₐ) ‖ (st₂, keys₂)
|vₐ| > 100
—————————————————————————————————————————————————————————————————————— EvUpdExercConsumNestingOutErr
'exercise' @Mod:T Ch cid v₁ ‖ (st₀, keys₀)
⇓ᵤ
(Err (Fatal "Value exceeds maximum nesting value"), ε)
'tpl' (x : T)
↦ { 'choices' { …, 'choice' 'consuming' Ch (y : 'ContractId' Mod:T) (z : τ) : σ 'by' eₚ 'observers' eₒ ↦ eₐ, … }, … } ∈ 〚Ξ〛Mod
cid ∈ dom(st₀)
st₀(cid) = (Mod:T, vₜ, 'active')
eₚ[x ↦ vₜ, z ↦ v₁] ⇓ Ok vₚ
eₒ[x ↦ vₜ, z ↦ v₁] ⇓ Ok vₒ
|v₁| ≤ 100
eₐ[x ↦ vₜ, y ↦ cid, z ↦ v₁] ⇓ Ok uₐ
keys₁ = keys₀ - keys₀⁻¹(cid)
st₁ = st₀[cid ↦ (Mod:T, vₜ, 'inactive')]
uₐ ‖ (st₁, keys₁) ⇓ᵤ Ok (vₐ, trₐ) ‖ (st₂, keys₂)
|vₐ| ≤ 100
—————————————————————————————————————————————————————————————————————— EvUpdExercConsum
'exercise' @Mod:T Ch cid v₁ ‖ (st₀, keys₀)
⇓ᵤ
Ok (vₐ, 'exercise' vₚ (cid, Mod:T, vₜ) 'consuming' trₐ) ‖ (st₂, keys₂)
'tpl' (x : T)
↦ { 'choices' { …, 'choice' 'non-consuming' Ch (y : 'ContractId' Mod:T) (z : τ) : σ 'by' eₚ 'observers' eₒ ↦ eₐ, … }, … } ∈ 〚Ξ〛Mod
cid ∈ dom(st₀)
st₀(cid) = (Mod:T, vₜ, 'active')
eₚ[x ↦ vₜ, z ↦ v₁] ⇓ Ok vₚ
eₒ[x ↦ vₜ, z ↦ v₁] ⇓ Ok vₒ
|v₁| ≤ 100
eₐ[x ↦ vₜ, y ↦ cid, z ↦ v₁] ⇓ Ok uₐ
uₐ ‖ (st₀; keys₀) ⇓ᵤ (Err E, tr)
—————————————————————————————————————————————————————————————————————— EvUpdExercNonConsumErr
'exercise' @Mod:T Ch cid v₁ ‖ (st₀, keys₀)
⇓ᵤ
(Err E, 'exercise' vₚ (cid, Mod:T, vₜ) 'non-consuming' tr)
'tpl' (x : T)
↦ { 'choices' { …, 'choice' 'non-consuming' Ch (y : 'ContractId' Mod:T) (z : τ) : σ 'by' eₚ 'observers' eₒ ↦ eₐ, … }, … } ∈ 〚Ξ〛Mod
cid ∈ dom(st₀)
st₀(cid) = (Mod:T, vₜ, 'active')
eₚ[x ↦ vₜ, z ↦ v₁] ⇓ Ok vₚ
eₒ[x ↦ vₜ, z ↦ v₁] ⇓ Ok vₒ
|v₁| ≤ 100
eₐ[x ↦ vₜ, y ↦ cid, z ↦ v₁] ⇓ Ok uₐ
uₐ ‖ (st₀; keys₀) ⇓ᵤ Ok (vₐ, trₐ) ‖ (st₁, keys₁)
|vₐ| > 100
—————————————————————————————————————————————————————————————————————— EvUpdExercNonConsumNestingOutErr
'exercise' @Mod:T Ch cid v₁ ‖ (st₀, keys₀)
⇓ᵤ
(Err (Fatal "Value exceeds maximum nesting value"), ε)
'tpl' (x : T)
↦ { 'choices' { …, 'choice' 'non-consuming' Ch (y : 'ContractId' Mod:T) (z : τ) : σ 'by' eₚ 'observers' eₒ ↦ eₐ, … }, … } ∈ 〚Ξ〛Mod
cid ∈ dom(st₀)
st₀(cid) = (Mod:T, vₜ, 'active')
eₚ[x ↦ vₜ, z ↦ v₁] ⇓ Ok vₚ
eₒ[x ↦ vₜ, z ↦ v₁] ⇓ Ok vₒ
|v₁| ≤ 100
eₐ[x ↦ vₜ, y ↦ cid, z ↦ v₁] ⇓ Ok uₐ
uₐ ‖ (st₀; keys₀) ⇓ᵤ Ok (vₐ, trₐ) ‖ (st₁, keys₁)
|vₐ| ≤ 100
—————————————————————————————————————————————————————————————————————— EvUpdExercNonConsum
'exercise' @Mod:T Ch cid v₁ ‖ (st₀, keys₀)
⇓ᵤ
Ok (vₐ, 'exercise' vₚ (cid, Mod:T, vₜ) 'non-consuming' trₐ) ‖ (st₁, keys₁)
cid ∉ dom(st)
—————————————————————————————————————————————————————————————————————— EvUpdExercIfaceMissing
'exercise_interface' @Mod:I Ch cid v₁ v₂ ‖ (st; keys)
⇓ᵤ
(Err (Fatal "Exercise on unknown contract"), ε)
cid ∈ dom(st₀)
st₀(cid) = (Mod':T', vₜ, 'inactive')
—————————————————————————————————————————————————————————————————————— EvUpdExercIfaceInactive
'exercise_interface' @Mod:I Ch cid v₁ v₂ ‖ (st₀; keys₀)
⇓ᵤ
(Err (Fatal "Exercise on inactive contract"), ε)
cid ∈ dom(st₀)
st₀(cid) = (Mod':T', vₜ, 'active')
Mod':T' does not implement interface Mod:I
—————————————————————————————————————————————————————————————————————— EvUpdExercIfaceDoesntImplement
'exercise_interface' @Mod:I Ch cid v₁ v₂ ‖ (st; keys₀)
⇓ᵤ
(Err (Fatal "Exercise on contract that does not implement interface"), ε)
cid ∈ dom(st₀)
st₀(cid) = (Mod':T, vₜ, 'active')
'tpl' (x : T) ↦ { …,'implements' Mod:I {…}, …, } ∈ 〚Ξ〛Mod'
vᵢ = 'to_interface' @Mod:I @Mod':T vₜ
v₂ vᵢ ⇓ Err (Fatal t)
—————————————————————————————————————————————————————————————————————— EvUpdExercIfaceGuardFatal
'exercise_interface' @Mod:I Ch cid v₁ v₂ ‖ (st; keys₀)
⇓ᵤ
(Err (Fatal t), ε)
cid ∈ dom(st₀)
st₀(cid) = (Mod':T, vₜ, 'active')
'tpl' (x : T) ↦ { …,'implements' Mod:I {…}, …, } ∈ 〚Ξ〛Mod'
vᵢ = 'to_interface' @Mod:I @Mod':T vₜ
v₂ vᵢ ⇓ Err (Throw v)
—————————————————————————————————————————————————————————————————————— EvUpdExercIfaceGuardThrow
'exercise_interface' @Mod:I Ch cid v₁ v₂ ‖ (st; keys₀)
⇓ᵤ
(Err (Fatal "Exercise guard failed"), ε)
cid ∈ dom(st₀)
st₀(cid) = (Mod':T, vₜ, 'active')
'tpl' (x : T) ↦ { …,'implements' Mod:I {…}, …, } ∈ 〚Ξ〛Mod'
vᵢ = 'to_interface' @Mod:I @Mod':T vₜ
v₂ vᵢ ⇓ Ok 'False'
—————————————————————————————————————————————————————————————————————— EvUpdExercIfaceGuardFalse
'exercise_interface' @Mod:I Ch cid v₁ v₂ ‖ (st; keys₀)
⇓ᵤ
(Err (Fatal "Exercise guard failed"), ε)
cid ∈ dom(st₀)
st₀(cid) = (Mod':T, vₜ, 'active')
'tpl' (x' : T) ↦ { …,'implements' Mod:I {…}, …, } ∈ 〚Ξ〛Mod'
vᵢ = 'to_interface' @Mod:I @Mod':T vₜ
v₂ vᵢ ⇓ Ok 'True'
'interface' (x : I) ↦ { …, 'choices' { …,
'choice' ChKind Ch (y : 'ContractId' Mod:I) (z : τ) : σ 'by' eₚ 'observers' eₒ ↦ eₐ, …
} } ∈ 〚Ξ〛Mod
eₚ[x ↦ vᵢ, z ↦ v₁] ⇓ Err E
—————————————————————————————————————————————————————————————————————— EvUpdExercIfaceActorEvalErr
'exercise_interface' @Mod:I Ch cid v₁ v₂ ‖ (st; keys₀)
⇓ᵤ
(Err (Fatal "Choice controller evaluation failed"), ε)
cid ∈ dom(st₀)
st₀(cid) = (Mod':T, vₜ, 'active')
'tpl' (x' : T) ↦ { …,'implements' Mod:I {…}, …, } ∈ 〚Ξ〛Mod'
vᵢ = 'to_interface' @Mod:I @Mod':T vₜ
v₂ vᵢ ⇓ Ok 'True'
'interface' (x : I) ↦ { …, 'choices' { …,
'choice' ChKind Ch (y : 'ContractId' Mod:I) (z : τ) : σ 'by' eₚ 'observers' eₒ ↦ eₐ, …
} } ∈ 〚Ξ〛Mod
eₚ[x ↦ vᵢ, z ↦ v₁] ⇓ Ok vₚ
eₒ[x ↦ vᵢ, z ↦ v₁] ⇓ Err E
—————————————————————————————————————————————————————————————————————— EvUpdExercIfaceObserversErr
'exercise_interface' @Mod:I Ch cid v₁ v₂ ‖ (st₀, keys₀)
⇓ᵤ
(Err (Fatal "Choice observer evaluation failed"), ε)
cid ∈ dom(st₀)
st₀(cid) = (Mod':T, vₜ, 'active')
'tpl' (x' : T) ↦ { …,'implements' Mod:I {…}, …, } ∈ 〚Ξ〛Mod'
vᵢ = 'to_interface' @Mod:I @Mod':T vₜ
v₂ vᵢ ⇓ Ok 'True'
'interface' (x : I) ↦ { …, 'choices' { …,
'choice' ChKind Ch (y : 'ContractId' Mod:I) (z : τ) : σ 'by' eₚ 'observers' eₒ ↦ eₐ, …
} } ∈ 〚Ξ〛Mod
eₚ[x ↦ vᵢ, z ↦ v₁] ⇓ Ok vₚ
eₒ[x ↦ vᵢ, z ↦ v₁] ⇓ Ok vₒ
|v₁| > 100
—————————————————————————————————————————————————————————————————————— EvUpdExercIfaceNestingArgErr
'exercise_interface' @Mod:I Ch cid v₁ v₂ ‖ (st₀, keys₀)
⇓ᵤ
(Err (Fatal "Value exceeds maximum nesting value"), ε)
cid ∈ dom(st₀)
st₀(cid) = (Mod':T, vₜ, 'active')
'tpl' (x' : T) ↦ { …,'implements' Mod:I {…}, …, } ∈ 〚Ξ〛Mod'
vᵢ = 'to_interface' @Mod:I @Mod':T vₜ
v₂ vᵢ ⇓ Ok 'True'
'interface' (x : I) ↦ { …, 'choices' { …,
'choice' ChKind Ch (y : 'ContractId' Mod:I) (z : τ) : σ 'by' eₚ 'observers' eₒ ↦ eₐ, …
} } ∈ 〚Ξ〛Mod
eₚ[x ↦ vᵢ, z ↦ v₁] ⇓ Ok vₚ
eₒ[x ↦ vᵢ, z ↦ v₁] ⇓ Ok vₒ
|v₁| ≤ 100
eₐ[x ↦ vᵢ, y ↦ cid, z ↦ v₁] ⇓ Err E
—————————————————————————————————————————————————————————————————————— EvUpdExercIfaceBodyEvalErr
'exercise_interface' @Mod:I Ch cid v₁ v₂ ‖ (st₀, keys₀)
⇓ᵤ
(Err E, 'exercise' vₚ (cid, Mod:T, vₜ) ChKind ε)
cid ∈ dom(st₀)
st₀(cid) = (Mod':T, vₜ, 'active')
'tpl' (x' : T) ↦ { …,'implements' Mod:I {…}, …, } ∈ 〚Ξ〛Mod'
vᵢ = 'to_interface' @Mod:I @Mod':T vₜ
v₂ vᵢ ⇓ Ok 'True'
'interface' (x : I) ↦ { …, 'choices' { …,
'choice' 'consuming' Ch (y : 'ContractId' Mod:I) (z : τ) : σ 'by' eₚ 'observers' eₒ ↦ eₐ, …
} } ∈ 〚Ξ〛Mod
eₚ[x ↦ vᵢ, z ↦ v₁] ⇓ Ok vₚ
eₒ[x ↦ vᵢ, z ↦ v₁] ⇓ Ok vₒ
|v₁| ≤ 100
eₐ[x ↦ vᵢ, y ↦ cid, z ↦ v₁] ⇓ Ok uₐ
keys₁ = keys₀ - keys₀⁻¹(cid)
st₁ = st₀[cid ↦ (Mod:T, vₜ, 'inactive')]
uₐ ‖ (st₁, keys₁) ⇓ᵤ (Err E, tr)
—————————————————————————————————————————————————————————————————————— EvUpdExercIfaceConsumErr
'exercise_interface' @Mod:I Ch cid v₁ v₂ ‖ (st₀, keys₀)
⇓ᵤ
(Err E, 'exercise' vₚ (cid, Mod:T, vₜ) 'consuming' tr)
cid ∈ dom(st₀)
st₀(cid) = (Mod':T, vₜ, 'active')
'tpl' (x' : T) ↦ { …,'implements' Mod:I {…}, …, } ∈ 〚Ξ〛Mod'
vᵢ = 'to_interface' @Mod:I @Mod':T vₜ
v₂ vᵢ ⇓ Ok 'True'
'interface' (x : I) ↦ { …, 'choices' { …,
'choice' 'consuming' Ch (y : 'ContractId' Mod:I) (z : τ) : σ 'by' eₚ 'observers' eₒ ↦ eₐ, …
} } ∈ 〚Ξ〛Mod
eₚ[x ↦ vᵢ, z ↦ v₁] ⇓ Ok vₚ
eₒ[x ↦ vᵢ, z ↦ v₁] ⇓ Ok vₒ
|v₁| ≤ 100
eₐ[x ↦ vᵢ, y ↦ cid, z ↦ v₁] ⇓ Ok uₐ
keys₁ = keys₀ - keys₀⁻¹(cid)
st₁ = st₀[cid ↦ (Mod:T, vₜ, 'inactive')]
uₐ ‖ (st₁, keys₁) ⇓ᵤ Ok (vₐ, trₐ) ‖ (st₂, keys₂)
|vₐ| > 100
—————————————————————————————————————————————————————————————————————— EvUpdExercIfaceConsumNestingOutErr
'exercise_interface' @Mod:I Ch cid v₁ v₂ ‖ (st₀, keys₀)
⇓ᵤ
(Err (Fatal "Value exceeds maximum nesting value"), ε)
cid ∈ dom(st₀)
st₀(cid) = (Mod':T, vₜ, 'active')
'tpl' (x' : T) ↦ { …,'implements' Mod:I {…}, …, } ∈ 〚Ξ〛Mod'
vᵢ = 'to_interface' @Mod:I @Mod':T vₜ
v₂ vᵢ ⇓ Ok 'True'
'interface' (x : I) ↦ { …, 'choices' { …,
'choice' 'consuming' Ch (y : 'ContractId' Mod:I) (z : τ) : σ 'by' eₚ 'observers' eₒ ↦ eₐ, …
} } ∈ 〚Ξ〛Mod
eₚ[x ↦ vᵢ, z ↦ v₁] ⇓ Ok vₚ
eₒ[x ↦ vᵢ, z ↦ v₁] ⇓ Ok vₒ
|v₁| ≤ 100
eₐ[x ↦ vᵢ, y ↦ cid, z ↦ v₁] ⇓ Ok uₐ
keys₁ = keys₀ - keys₀⁻¹(cid)
st₁ = st₀[cid ↦ (Mod:T, vₜ, 'inactive')]
uₐ ‖ (st₁, keys₁) ⇓ᵤ Ok (vₐ, trₐ) ‖ (st₂, keys₂)
|vₐ| ≤ 100
—————————————————————————————————————————————————————————————————————— EvUpdExercIfaceConsum
'exercise_interface' @Mod:I Ch cid v₁ v₂ ‖ (st₀, keys₀)
⇓ᵤ
Ok (vₐ, 'exercise' vₚ (cid, Mod:T, vₜ) 'consuming' trₐ) ‖ (st₂, keys₂)
cid ∈ dom(st₀)
st₀(cid) = (Mod':T, vₜ, 'active')
'tpl' (x' : T) ↦ { …,'implements' Mod:I {…}, …, } ∈ 〚Ξ〛Mod'
vᵢ = 'to_interface' @Mod:I @Mod':T vₜ
v₂ vᵢ ⇓ Ok 'True'
'interface' (x : I) ↦ { …, 'choices' { …,
'choice' 'non-consuming' Ch (y : 'ContractId' Mod:I) (z : τ) : σ 'by' eₚ 'observers' eₒ ↦ eₐ, …
} } ∈ 〚Ξ〛Mod
eₚ[x ↦ vᵢ, z ↦ v₁] ⇓ Ok vₚ
eₒ[x ↦ vᵢ, z ↦ v₁] ⇓ Ok vₒ
|v₁| ≤ 100
eₐ[x ↦ vᵢ, y ↦ cid, z ↦ v₁] ⇓ Ok uₐ
uₐ ‖ (st₀; keys₀) ⇓ᵤ (Err E, tr)
—————————————————————————————————————————————————————————————————————— EvUpdExercIfaceNonConsumErr
'exercise_interface' @Mod:I Ch cid v₁ v₂ ‖ (st₀, keys₀)
⇓ᵤ
(Err E, 'exercise' vₚ (cid, Mod:T, vₜ) 'non-consuming' tr)
cid ∈ dom(st₀)
st₀(cid) = (Mod':T, vₜ, 'active')
'tpl' (x' : T) ↦ { …,'implements' Mod:I {…}, …, } ∈ 〚Ξ〛Mod'
vᵢ = 'to_interface' @Mod:I @Mod':T vₜ
v₂ vᵢ ⇓ Ok 'True'
'interface' (x : I) ↦ { …, 'choices' { …,
'choice' 'non-consuming' Ch (y : 'ContractId' Mod:I) (z : τ) : σ 'by' eₚ 'observers' eₒ ↦ eₐ, …
} } ∈ 〚Ξ〛Mod
eₚ[x ↦ vᵢ, z ↦ v₁] ⇓ Ok vₚ
eₒ[x ↦ vᵢ, z ↦ v₁] ⇓ Ok vₒ
|v₁| ≤ 100
eₐ[x ↦ vᵢ, y ↦ cid, z ↦ v₁] ⇓ Ok uₐ
uₐ ‖ (st₀; keys₀) ⇓ᵤ Ok (vₐ, trₐ) ‖ (st₁, keys₁)
|vₐ| > 100
—————————————————————————————————————————————————————————————————————— EvUpdExercIfaceNonConsumNestingOutErr
'exercise_interface' @Mod:I Ch cid v₁ v₂ ‖ (st₀, keys₀)
⇓ᵤ
(Err (Fatal "Value exceeds maximum nesting value"), ε)
cid ∈ dom(st₀)
st₀(cid) = (Mod':T, vₜ, 'active')
'tpl' (x' : T) ↦ { …,'implements' Mod:I {…}, …, } ∈ 〚Ξ〛Mod'
vᵢ = 'to_interface' @Mod:I @Mod':T vₜ
v₂ vᵢ ⇓ Ok 'True'
'interface' (x : I) ↦ { …, 'choices' { …,
'choice' 'non-consuming' Ch (y : 'ContractId' Mod:I) (z : τ) : σ 'by' eₚ 'observers' eₒ ↦ eₐ, …
} } ∈ 〚Ξ〛Mod
eₚ[x ↦ vᵢ, z ↦ v₁] ⇓ Ok vₚ
eₒ[x ↦ vᵢ, z ↦ v₁] ⇓ Ok vₒ
|v₁| ≤ 100
eₐ[x ↦ vᵢ, y ↦ cid, z ↦ v₁] ⇓ Ok uₐ
uₐ ‖ (st₀; keys₀) ⇓ᵤ Ok (vₐ, trₐ) ‖ (st₁, keys₁)
|vₐ| ≤ 100
—————————————————————————————————————————————————————————————————————— EvUpdExercIfaceNonConsum
'exercise_interface' @Mod:I Ch cid v₁ v₂ ‖ (st₀, keys₀)
⇓ᵤ
Ok (vₐ, 'exercise' vₚ (cid, Mod:T, vₜ) 'non-consuming' trₐ) ‖ (st₁, keys₁)
cid ∉ dom(st)
—————————————————————————————————————————————————————————————————————— EvUpdFetchMissing
'fetch' @Mod:T cid ‖ (st; keys)
⇓ᵤ
(Err (Fatal "Fetch on unknown contract"), ε)
'tpl' (x : T) ↦ … ∈ 〚Ξ〛Mod
cid ∈ dom(st)
st(cid) = (Mod:T', vₜ, 'inactive')
—————————————————————————————————————————————————————————————————————— EvUpdFetchInactive
'fetch' @Mod:T cid ‖ (st; keys)
⇓ᵤ
(Err (Fatal "Fetch on inactive contract"), ε)
'tpl' (x : T) ↦ … ∈ 〚Ξ〛Mod
cid ∈ dom(st)
st(cid) = (Mod':T', vₜ, 'active')
Mod:T ≠ Mod':T'
—————————————————————————————————————————————————————————————————————— EvUpdFetchWrongTemplate
'fetch' @Mod:T cid ‖ (st; keys)
⇓ᵤ
(Err (Fatal "Fetch on contract of wrong template"), ε)
'tpl' (x : T) ↦ … ∈ 〚Ξ〛Mod
cid ∈ dom(st)
st(cid) = (Mod:T, vₜ, 'active')
—————————————————————————————————————————————————————————————————————— EvUpdFetch
'fetch' @Mod:T cid ‖ (st; keys)
⇓ᵤ
(Ok vₜ, ε) ‖ (st; keys)
cid ∉ dom(st)
—————————————————————————————————————————————————————————————————————— EvUpdFetchInterfaceMissing [Daml-LF ≥ 1.dev]
'fetch_interface' @Mod:I cid ‖ (st; keys)
⇓ᵤ
(Err (Fatal "Fetch on unknown contract"), ε)
cid ∈ dom(st)
st(cid) = (Mod:T, vₜ, 'inactive')
—————————————————————————————————————————————————————————————————————— EvUpdFetchInterfaceInactive [Daml-LF ≥ 1.dev]
'fetch_interface' @Mod:I cid ‖ (st; keys)
⇓ᵤ
(Err (Fatal "Fetch on inactive contract"), ε)
cid ∈ dom(st)
st(cid) = (Mod':T, vₜ, 'active')
Mod':T does not implement interface Mod:I
—————————————————————————————————————————————————————————————————————— EvUpdFetchInterfaceDoesntImplement [Daml-LF ≥ 1.dev]
'fetch_interface' @Mod:I cid ‖ (st; keys)
⇓ᵤ
(Err (Fatal "Fetched contract does not implement interface"), ε)
cid ∈ dom(st)
st(cid) = (Mod':T, vₜ, 'active')
'tpl' (x : T) ↦ { …, 'implements' Mod:I { … }, … } ∈ 〚Ξ〛Mod'
—————————————————————————————————————————————————————————————————————— EvUpdFetchInterface [Daml-LF ≥ 1.dev]
'fetch_interface' @Mod:I cid ‖ (st; keys)
⇓ᵤ
(Ok ('to_interface @Mod:I @Mod':T vₜ), ε) ‖ (st; keys)
'tpl' (x : T) ↦ { …, 'key' @σ eₖ eₘ } ∈ 〚Ξ〛Mod
(eₘ vₖ) ⇓ Err E
—————————————————————————————————————————————————————————————————————— EvUpdFetchByKeyErr
'fetch_by_key' @Mod:T vₖ ‖ (st; keys) ⇓ᵤ (Err E, ε)
'tpl' (x : T) ↦ { …, 'key' @σ eₖ eₘ } ∈ 〚Ξ〛Mod
(eₘ vₖ) ⇓ Ok vₘ
|vₖ| > 100
—————————————————————————————————————————————————————————————————————— EvUpdFetchByKeyNestingErr
'fetch_by_key' @Mod:T vₖ ‖ (st; keys)
⇓ᵤ
(Err (Fatal "Value exceeds maximum nesting value"), ε)
'tpl' (x : T) ↦ { …, 'key' @σ eₖ eₘ } ∈ 〚Ξ〛Mod
(eₘ vₖ) ⇓ Ok vₘ
|vₖ| ≤ 100
(Mod:T, vₖ) ∉ dom(keys₀)
—————————————————————————————————————————————————————————————————————— EvUpdFetchByKeyNotFound
'fetch_by_key' @Mod:T vₖ ‖ (st; keys)
⇓ᵤ
(Err (Fatal "Lookup key not found"), ε)
'tpl' (x : T) ↦ { …, 'key' @σ eₖ eₘ } ∈ 〚Ξ〛Mod
(eₘ vₖ) ⇓ Ok vₘ
|vₖ| ≤ 100
(Mod:T, vₖ) ∈ dom(keys)
cid = keys((Mod:T, v))
st(cid) = (Mod:T, vₜ, 'inactive')
—————————————————————————————————————————————————————————————————————— EvUpdFetchByKeyInactive
'fetch_by_key' @Mod:T vₖ ‖ (st; keys)
⇓ᵤ
(Err (Fatal "Exercise on inactive contract"), ε)
'tpl' (x : T) ↦ { …, 'key' @σ eₖ eₘ } ∈ 〚Ξ〛Mod
(eₘ vₖ) ⇓ Ok vₘ
|vₖ| ≤ 100
(Mod:T, vₖ) ∈ dom(keys)
cid = keys((Mod:T, v))
st(cid) = (Mod:T, vₜ, 'active')
—————————————————————————————————————————————————————————————————————— EvUpdFetchByKeyFound
'fetch_by_key' @Mod:T vₖ ‖ (st; keys)
⇓ᵤ
(Ok ⟨'contractId': cid, 'contract': vₜ⟩, ε) ‖ (st; keys)
'tpl' (x : T) ↦ { …, 'key' @σ eₖ eₘ } ∈ 〚Ξ〛Mod
(eₘ vₖ) ⇓ Err E
—————————————————————————————————————————————————————————————————————— EvUpdLookupByKeyErr
'lookup_by_key' @Mod:T vₖ ‖ (st; keys) ⇓ᵤ (Err E, ε)
'tpl' (x : T) ↦ { …, 'key' @σ eₖ eₘ } ∈ 〚Ξ〛Mod
(eₘ vₖ) ⇓ vₘ
|vₖ| ≤ 100
—————————————————————————————————————————————————————————————————————— EvUpdLookupByKeyNestingErr
'lookup_by_key' @Mod:T vₖ ‖ (st; keys)
⇓ᵤ
(Err (Fatal "Value exceeds maximum nesting value"), ε)
'tpl' (x : T) ↦ { …, 'key' @σ eₖ eₘ } ∈ 〚Ξ〛Mod
(eₘ vₖ) ⇓ vₘ
|vₖ| ≤ 100
(Mod:T, vₖ) ∉ dom(keys)
—————————————————————————————————————————————————————————————————————— EvUpdLookupByKeyNotFound
'lookup_by_key' @Mod:T vₖ ‖ (st; keys)
⇓ᵤ
(Ok ('None' @('ContractId' Mod:T)), ε) ‖ (st; keys)
'tpl' (x : T) ↦ { …, 'key' @σ eₖ eₘ } ∈ 〚Ξ〛Mod
(eₘ vₖ) ⇓ vₘ
|vₖ| ≤ 100
(Mod:T, vₖ) ∈ dom(keys)
cid = keys((Mod:T, v))
—————————————————————————————————————————————————————————————————————— EvUpdLookupByKeyFound
'lookup_by_key' @Mod:T vₖ ‖ (st; keys)
⇓ᵤ
(Ok ('Some' @('ContractId' Mod:T) cid), ε) ‖ (st; keys)
'tpl' (x : T) ↦ { …, 'key' @σ eₖ eₘ } ∈ 〚Ξ〛Mod
'fetch_by_key' @Mod:T vₖ ‖ (st; keys) ⇓ᵤ (Err E, tr)
—————————————————————————————————————————————————————————————————————— EvUpdExercByKeyFetchErr
'exercise_by_key' @Mod:T Ch vₖ v₁ ‖ (st; keys) ⇓ᵤ (Err E, tr)
'tpl' (x : T) ↦ { …, 'key' @σ eₖ eₘ } ∈ 〚Ξ〛Mod
'fetch_by_key' @Mod:T vₖ ‖ (st; keys) ⇓ᵤ (Ok ⟨'contractId': cid, 'contract': vₜ⟩, ε) ‖ (st'; keys')
'exercise' @Mod:T Ch cid v₁ ‖ (st'; keys') ⇓ᵤ ur
—————————————————————————————————————————————————————————————————————— EvUpdExercByKeyExercise
'exercise_by_key' @Mod:T Ch vₖ v₁ ‖ (st; keys) ⇓ᵤ ur
LitTimestamp is the current ledger time
—————————————————————————————————————————————————————————————————————— EvUpdGetTime
'get_time' ‖ (st; keys)
⇓ᵤ
(Ok LitTimestamp, ε) ‖ (st; keys)
e ⇓ Err E
—————————————————————————————————————————————————————————————————————— EvUpdEmbedExprErr
'embed_expr' @τ e ‖ (st; keys) ⇓ᵤ (Err E, ε)
e ⇓ Ok u
u ‖ (st; keys) ⇓ᵤ ur
—————————————————————————————————————————————————————————————————————— EvUpdEmbedExpr
'embed_expr' @τ e ‖ (st; keys) ⇓ᵤ ur
e₁ ⇓ Ok u₁
u₁ ‖ S₀ ⇓ᵤ (Ok v₁, tr₁) ‖ S₁
—————————————————————————————————————————————————————————————————————— EvUpdTryCatchOk
'try' @τ e₁ 'catch' x. e₂ ‖ S₀
⇓ᵤ
(Ok v₁, tr₁) ‖ S₁
e₁ ⇓ Err (Fatal t)
—————————————————————————————————————————————————————————————————————— EvUpdTryCatchFatal1
'try' @τ e₁ 'catch' x. e₂ ‖ S₀ ⇓ᵤ (Err (Fatal t), ε)
e₁ ⇓ Ok u₁
u₁ ‖ S₀ ⇓ᵤ (Err (Fatal t), tr₁)
—————————————————————————————————————————————————————————————————————— EvUpdTryCatchFatal2
'try' @τ e₁ 'catch' x. e₂ ‖ S₀ ⇓ᵤ (Err (Fatal t), tr₁)
e₁ ⇓ Err (Throw v)
e₂[x ↦ v] ⇓ Ok ('None' @σ)
—————————————————————————————————————————————————————————————————————— EvUpdTryCatchThrow1_NoHandle
'try' @τ e₁ 'catch' x. e₂ ‖ S₀ ⇓ᵤ (Err (Throw v), ε)
e₁ ⇓ Ok u₁
u₁ ‖ S₀ ⇓ᵤ (Err (Throw v), tr₁)
e₂[x ↦ v] ⇓ Ok ('None' @σ)
—————————————————————————————————————————————————————————————————————— EvUpdTryCatchThrow2_NoHandle
'try' @τ e₁ 'catch' x. e₂ ‖ S₀ ⇓ᵤ (Err (Throw v), tr₁)
e₁ ⇓ Err (Throw v₁)
e₂[x ↦ v₁] ⇓ Ok ('Some' @σ u₂)
u2 ‖ S₀ ⇓ᵤ (Ok v₂, tr₂) ‖ S₂
—————————————————————————————————————————————————————————————————————— EvUpdTryCatchThrow1_OkHandle_Ok
'try' @τ e₁ 'catch' x. e₂ ‖ S₀
⇓ᵤ
(Ok v₂, ('rollback' ε) ⋅ tr₂) ‖ S₂
e₁ ⇓ Ok u₁
u₁ ‖ S₀ ⇓ᵤ (Err (Throw v₁), tr₁)
e₂[x ↦ v₁] ⇓ Ok ('Some' @σ u₂)
u2 ‖ S₀ ⇓ᵤ (Ok v₂, tr₂) ‖ S₂
—————————————————————————————————————————————————————————————————————— EvUpdTryCatchThrow2_OkHandle_Ok
'try' @τ e₁ 'catch' x. e₂ ‖ S₀
⇓ᵤ
(Ok v₂, ('rollback' tr₁) ⋅ tr₂) ‖ S₂
e₁ ⇓ Err (Throw v₁)
e₂[x ↦ v₁] ⇓ Ok ('Some' @σ u₂)
u2 ‖ S₀ ⇓ᵤ (Err E, tr₂)
—————————————————————————————————————————————————————————————————————— EvUpdTryCatchThrow1_OkHandle_Err
'try' @τ e₁ 'catch' x. e₂ ‖ S₀
⇓ᵤ
(Err E, ('rollback' ε) ⋅ tr₂)
e₁ ⇓ Ok u₁
u₁ ‖ S₀ ⇓ᵤ (Err (Throw v₁), tr₁)
e₂[x ↦ v₁] ⇓ Ok ('Some' @σ u₂)
u2 ‖ S₀ ⇓ᵤ (Err E, tr₂)
—————————————————————————————————————————————————————————————————————— EvUpdTryCatchThrow2_OkHandle_Err
'try' @τ e₁ 'catch' x. e₂ ‖ S₀
⇓ᵤ
(Err E, ('rollback' tr₁) ⋅ tr₂)
e₁ ⇓ Err (Throw v₁)
e₂[x ↦ v₁] ⇓ Err E
—————————————————————————————————————————————————————————————————————— EvUpdTryCatchThrow1_ErrHandle
'try' @τ e₁ 'catch' x. e₂ ‖ S₀
⇓ᵤ
(Err E, ('rollback' ε))
e₁ ⇓ Ok u₁
u₁ ‖ S₀ ⇓ᵤ (Err (Throw v₁), tr₁)
e₂[x ↦ v₁] ⇓ Err E
—————————————————————————————————————————————————————————————————————— EvUpdTryCatchThrow2_ErrHandle
'try' @τ e₁ 'catch' x. e₂ ‖ S₀
⇓ᵤ
(Err E, ('rollback' tr₁))
Transaction normalization
~~~~~~~~~~~~~~~~~~~~~~~~~
After a transaction is generated through update interpretation, it is normalized.
Normalized transactions do not include empty rollback nodes, nor any rollback
node that starts or ends with another rollback node.
To define normalization, we need a helper function. This function takes a
normalized transaction and tries to wrap it in a rollback node, while preserving
normalization. This function is defined recursively by the following rules::
┌───────────────┐
Normalized Rollback Wrapping │ ℝ (tr₁) = tr₂ │
└───────────────┘
—————————————————————————————————————————————————————————————————————— RollbackEmpty
ℝ (ε) = ε
ℝ (tr₂) = tr₃
—————————————————————————————————————————————————————————————————————— RollbackPrefix
ℝ (('rollback' tr₁) ⋅ tr₂) = ('rollback' tr₁) ⋅ tr₃
—————————————————————————————————————————————————————————————————————— RollbackSuffix
ℝ (act ⋅ tr₁ ⋅ ('rollback' tr₂)) = 'rollback' (act ⋅ tr₁ ⋅ tr₂)
—————————————————————————————————————————————————————————————————————— RollbackSingle
ℝ (act) = 'rollback' act
—————————————————————————————————————————————————————————————————————— RollbackMultiple
ℝ (act₁ ⋅ tr ⋅ act₂) = 'rollback' (act₁ ⋅ tr ⋅ act₂)
Normalization of a transaction is then defined according to the following rules,
where `ntr` ranges over normalized transactions::
┌───────────┐
Transaction Normalization │ tr ⇓ₜ ntr │
└───────────┘
—————————————————————————————————————————————————————————————————————— TransNormEmpty
ε ⇓ₜ ε
tr₁ ⇓ₜ ntr₁
tr₂ ⇓ₜ ntr₂
—————————————————————————————————————————————————————————————————————— TransNormConcat
tr₁ ⋅ tr₂ ⇓ₜ ntr₁ ⋅ ntr₂
—————————————————————————————————————————————————————————————————————— TransNormCreate
'create' Contract ⇓ₜ 'create' Contract
tr ⇓ₜ ntr
—————————————————————————————————————————————————————————————————————— TransNormExercise
'exercise' v Contract ChKind tr
⇓ₜ
'exercise' v Contract ChKind ntr
tr ⇓ₜ ntr₁
ℝ (ntr₁) = ntr₂
—————————————————————————————————————————————————————————————————————— TransNormRollback
'rollback' tr ⇓ₜ ntr₂
About scenario interpretation
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
The interpretation of scenarios is a feature an engine can provide to
test business logic within a Daml-LF archive. Nevertheless, the
present specification does not define how scenarios should be actually
interpreted. An engine compliant with this specification does not have
to provide support for scenario interpretation. It must however accept
loading any `valid <Validation_>`_ archive that contains scenario
expressions, and must handle update statements that actually
manipulate expressions of type `Scenario τ`. Note that the semantics
of `Update interpretation`_ (including evaluation of `expression
<expression evaluation_>`_ and `built-in functions`_) guarantee that
values of type `'Scenario' τ` cannot be scrutinized and can only be
"moved around" as black box arguments by the different functions
evaluated during the interpretation of an update.
Built-in functions
^^^^^^^^^^^^^^^^^^
This section lists the built-in functions supported by Daml-LF 1.
The functions come with their types and a description of their
behavior.
About Exceptions
~~~~~~~~~~~~~~~~
Some builtin functions can throw non-fatal exceptions, i.e. exceptions
catchable by the ``TryCatch`` update expression. Those exceptions are
not built in the language but are standard exceptions defined in user
land. The builtin functions from an engine compliant with the current
specification should be able to produce and handle (notably the
``ANY_EXCEPTION_MESSAGE`` builtin function) such exceptions even if
the package they are defined in has not been loaded. Any other usage
on the exception payload, like construction, projection, update or
conversion from/back `'AnyException'`, requires the definition
packages to be loaded.
As of LF 1.14 the only non-fatal exceptions that a builtin function
can throw is the ``ArithmeticError`` record defined in the module
``DA.Exception.ArithmeticError`` of the package
``'cb0552debf219cc909f51cbb5c3b41e9981d39f8f645b1f35e2ef5be2e0b858a'``
whose content is as follow::
package cb0552debf219cc909f51cbb5c3b41e9981d39f8f645b1f35e2ef5be2e0b858a
daml-lf 1.14
metadata daml-prim-DA-Exception-ArithmeticError-1.0.0
module DA.Exception.ArithmeticError {
record @serializable ArithmeticError = { message : Text } ;
val $WArithmeticError :Text -> DA.Exception.ArithmeticError:ArithmeticError =
λ message : Text .
DA.Exception.ArithmeticError:ArithmeticError { message = message };
exception ArithmeticError = {
'message' λ x : DA.Exception.ArithmeticError:ArithmeticError.
DA.Exception.ArithmeticError:ArithmeticError { message } x
} ;
}
.. The package can be produced in a stable way by Daml SDK 1.14 or
latter with the command
``bazel build //compiler/damlc/stable-packages:stable-packages``
In the following, we will say that the call of a built-in function
``F : ∀ (α₁ … αₘ : nat) . τ₁ → … → τ₂ → τ`` "throws an
``ArithmeticError`` exception" to mean its evaluation is equivalent to
the evaluation of::
Throw cb0552debf219cc909f51cbb5c3b41e9981d39f8f645b1f35e2ef5be2e0b858a:DA.Exception.ArithmeticError:ArithmeticError {
message = "ArithmeticError while evaluating (F @n₁ … @nₘ v₁ … vₙ)."
}
where ``n₁ … nₘ v₁ … vₙ`` are the string representations of the
arguments passed to the function.
Generic comparison functions
~~~~~~~~~~~~~~~~~~~~~~~~~~~~
The following builtin functions defines an order on the so-called
`comparable` values. Comparable values are LF values except type
abstractions, functions, partially applied builtin functions, and
updates.
Note that as described in the `V1 Contract ID allocation scheme
specification <./contract-id.rst>`_ the comparison of two V1 contract
identifiers may fail at run time. For the purpose of this
specification, we will say that two contract identifiers are *not
comparable* if (i) both of them are V1 contract identifiers, (ii) one
of them is ``non-suffixed``, and (iii) is a strict prefixed of the
other one.
* ``LESS_EQ : ∀ (α:*). α → α → 'Bool'``
The builtin function ``LESS_EQ`` returns ``'True'`` if the first
argument is smaller than or equal to the second argument,
``'False'`` otherwise. The function raises a runtime error if the
arguments are incomparable.
[*Available in version >= 1.11*]
Formally the builtin function ``LESS_EQ`` semantics is defined by
the following rules. Note the rules assume ``LESS_EQ`` is fully
applied and well-typed, in particular ``LESS_EQ`` always compared
value of the same type.::
—————————————————————————————————————————————————————————————————————— EvLessEqUnit
𝕆('LESS_EQ' @σ () ()) = Ok 'True'
—————————————————————————————————————————————————————————————————————— EvLessEqBool
𝕆('LESS_EQ' @σ b₁ b₂) = Ok (¬b₁ ∨ b₂)
—————————————————————————————————————————————————————————————————————— EvLessEqInt64
𝕆('LESS_EQ' @σ LitInt64₁ LitInt64₂) = Ok (LitInt64₁ ≤ₗ LitInt64₂)
—————————————————————————————————————————————————————————————————————— EvLessEqDate
𝕆('LESS_EQ' @σ LitDate₁ LitDate₂) = Ok (LitDate₁ ≤ₗ LitDate₂)
—————————————————————————————————————————————————————————————————————— EvLessEqTimestamp
𝕆('LESS_EQ' @σ LitTimestamp₁ LitTimestamp₂) =
Ok (LitTimestamp₁ ≤ₗ LitTimestamp₂)
—————————————————————————————————————————————————————————————————————— EvLessEqText
𝕆('LESS_EQ' @σ LitText₁ LitText₂) = Ok (LitText₁ ≤ₗ LitText₂)
—————————————————————————————————————————————————————————————————————— EvLessEqParty
𝕆('LESS_EQ' @σ LitParty₁ LitParty₂) = Ok (LitParty₁ ≤ₗ LitParty₂)
—————————————————————————————————————————————————————————————————————— EvLessEqNumeric
𝕆('LESS_EQ' @σ LitNumeric₁ LitNumeric₂) =
Ok (LitNumeric₁ ≤ₗ LitNumeric₂)
—————————————————————————————————————————————————————————————————————— EvLessEqBigNumeric
𝕆('LESS_EQ' @σ LitBigNumeric₁ LitBigNumeric₂) =
Ok (LitBigNumeric₁ ≤ₗ LitBigNumeric₂)
—————————————————————————————————————————————————————————————————————— EvLessEqRoundingMode
𝕆('LESS_EQ' @σ LitRoundingMode₁ LitRoundingMode₂) =
Ok (LitRoundingMode₁ ≤ₗ LitRoundingMode₂)
cid₁ and cid₂ are not comparable
—————————————————————————————————————————————————————————————————————— EvLessEqNonComparableContractId
𝕆('LESS_EQ' @σ cid₁ cid₂) = Err 'ContractIdComparability'
cid₁ and cid₂ are comparable
—————————————————————————————————————————————————————————————————————— EvLessEqComparableContractId
𝕆('LESS_EQ' @σ cid₁ cid₂) = Ok (cid₁ ≤ₗ cid₂)
—————————————————————————————————————————————————————————————————————— EvLessEqStructEmpty
𝕆('LESS_EQ' @⟨ ⟩ ⟨ ⟩ ⟨ ⟩) = Ok 'True'
𝕆('LESS_EQ' @τ₀ v₀ v₀') = Err t
—————————————————————————————————————————————————————————————————————— EvLessEqStructNonEmptyHeadErr
𝕆('LESS_EQ' @⟨ f₀: τ₀, f₁: τ₁, …, fₙ: τₙ ⟩
⟨ f₀= v₀, f₁= v₁, …, fₘ= vₘ ⟩
⟨ f₀= v₀', f₁= v₁', …, fₘ= vₘ' ⟩) = Err t
𝕆('LESS_EQ' @τ₁ v₀ v₀') = Ok 'False'
————————————————————————————————————————————————————————————————————— EvLessEqStructNonEmptyHeadBigger
𝕆('LESS_EQ' @⟨ f₀: τ₀, f₁: τ₁, …, fₙ: τₙ ⟩
⟨ f₀= v₀, f₁= v₁, …, fₘ= vₘ ⟩
⟨ f₀= v₀', f₁= v₁', …, fₘ= vₘ' ⟩) = Ok 'False'
𝕆('LESS_EQ' @τ₀ v₀ v₀') = Ok 'True'
𝕆('LESS_EQ' @τ₀ v₀' v₀) = Ok 'False'
————————————————————————————————————————————————————————————————————— EvLessEqStructNonEmptyHeadSmaller
𝕆('LESS_EQ' @⟨ f₀: τ₀, f₁: τ₁, …, fₙ: τₙ ⟩
⟨ f₀= v₀, f₁= v₁, …, fₘ= vₘ ⟩
⟨ f₀= v₀', f₁= v₁', …, fₘ= vₘ' ⟩) = Ok 'True'
𝕆('LESS_EQ' @τ₀ v₀ v₀') = Ok 'True'
𝕆('LESS_EQ' @τ₀ v₀' v₀) = Ok 'True'
𝕆('LESS_EQ' @⟨ f₁: τ₁, …, fₙ: τₙ ⟩
⟨ f₁= v₁, …, fₘ= vₘ ⟩
⟨ f₁= v₁', …, fₘ= vₘ' ⟩) = r
—————————————————————————————————————————————————————————————————————— EvLessEqStructNonEmptyTail
𝕆('LESS_EQ' @⟨ f₀: τ₀, f₁: τ₁, …, fₙ: τₙ ⟩
⟨ f₀= v₀, f₁= v₁, …, fₘ= vₘ ⟩
⟨ f₀= v₀', f₁= v₁', …, fₘ= vₘ' ⟩) = r
'enum' T ↦ E₁: σ₁ | … | Eₘ: σₘ ∈ 〚Ξ〛Mod
—————————————————————————————————————————————————————————————————————— EvLessEqEnum
𝕆('LESS_EQ' @σ Mod:T:Eᵢ Mod:T:Eⱼ) = OK (i ≤ j)
'variant' T α₁ … αₙ ↦ V₁: σ₁ | … | Vₘ: σₘ ∈ 〚Ξ〛Mod i ≠ j
—————————————————————————————————————————————————————————————————————— EvLessEqVariantConstructor
𝕆('LESS_EQ' @σ (Mod:T:Vᵢ @σ₁ … @σₙ v) (Mod:T:Vⱼ @σ₁' … @σₙ' v') =
OK (i ≤ j)
'variant' T α₁ … αₙ ↦ V₁: τ₁ | … | Vₘ: τₘ ∈ 〚Ξ〛Mod
τᵢ ↠ τᵢ' 𝕆('LESS_EQ' @(τᵢ'[α₁ ↦ σ₁, …, αₙ ↦ σₙ]) v v') = r
—————————————————————————————————————————————————————————————————————— EvLessEqVariantValue
𝕆('LESS_EQ' @σ (Mod:T:Vᵢ @σ₁ … @σₙ v) (Mod:T:Vᵢ @σ₁' … @σₙ' v')) = r
'record' T (α₁:k₁) … (αₙ:kₙ) ↦ { f₁:τ₁, …, fₘ:τₘ } ∈ 〚Ξ〛Mod
'τ₁ ↠ τ₁' … τᵢ ↠ τᵢ'
𝕆('LESS_EQ' @⟨ f₁: τ₁'[α₁ ↦ σ₁, …, αₙ ↦ σₙ],
…, fₙ: τₙ'[α₁ ↦ σ₁, …, αₙ ↦ σₙ]⟩
⟨ f₁= v₁, …, fₘ = vₘ ⟩
⟨ f₁= v₁', …, fₘ = vₘ' ⟩) = r
—————————————————————————————————————————————————————————————————————— EvLessEqRecord
𝕆('LESS_EQ' @σ (Mod:T @σ₁ … @σₙ { f₁ = v₁ , …, fₘ = vₘ })
(Mod:T @σ₁' … @σₙ' { f₁ = v₁', …, fₘ = vₘ' })) = r
—————————————————————————————————————————————————————————————————————— EvLessEqListNil
𝕆('LESS_EQ' @σ (Nil @τ) v) = Ok 'True'
—————————————————————————————————————————————————————————————————————— EvLessEqListConsNil
𝕆('LESS_EQ' @σ (Cons @τ vₕ vₜ) (Nil @τ')) = Ok 'False'
𝕆('LESS_EQ' @⟨ h:τ, t: 'List' τ ⟩
⟨ h= vₕ, t= vₜ ⟩
⟨ h= vₕ', t= vₜ' ⟩) = r
—————————————————————————————————————————————————————————————————————— EvLessEqListConsCons
𝕆('LESS_EQ' @σ (Cons @τ vₕ vₜ) (Cons @τ' vₕ vₜ)) = r
—————————————————————————————————————————————————————————————————————— EvLessEqOptionNoneAny
𝕆('LESS_EQ' @σ (None @τ) v) = Ok 'True'
—————————————————————————————————————————————————————————————————————— EvLessEqOptionSomeNone
𝕆('LESS_EQ' @σ (Some @τ v) (None @τ')) = Ok 'False'
𝕆('LESS_EQ' @τ v v') = r
—————————————————————————————————————————————————————————————————————— EvLessEqOptionSomeSome
𝕆('LESS_EQ' @σ (Some @τ v) (Some @τ' v')) = r
—————————————————————————————————————————————————————————————————————— EvLessEqGenMapEmptyAny
𝕆('LESS_EQ' σ 〚〛v) = Ok 'True'
n > 0
—————————————————————————————————————————————————————————————————————— EvLessEqGenMapNonEmptyEmpty
𝕆('LESS_EQ' σ 〚v₁ ↦ w₁; …; vₙ ↦ wₙ〛〚〛) = Ok 'FALSE'
𝕆('LESS_EQ' @⟨ hₖ: σₖ, hᵥ: σᵥ, t: 'GenMap' σₖ σᵥ ⟩
⟨ hₖ= v₀, hᵥ= wₒ , t= 〚v₁ ↦ w₁ ; …; vₙ ↦ wₙ 〛⟩
⟨ hₖ= v₀', hᵥ= wₒ', t= 〚v₁' ↦ w₁'; …; vₙ' ↦ wₙ'〛⟩ = r
—————————————————————————————————————————————————————————————————————— EvLessEqGenMapNonEmptyNonEmpty
𝕆('LESS_EQ' @('GenMap' σₖ σᵥ)
〚v₀ ↦ w₀ ; v₁ ↦ w₁ ; …; vₙ ↦ wₙ 〛
〚v₀' ↦ w₀'; v₁' ↦ w₁'; …; vₙ' ↦ wₙ'〛) = r
𝕆('LESS_EQ' @('GenMap' 'Text' σ)
〚t₁ ↦ v₁ ; …; tₙ ↦ vₙ 〛
〚t₁' ↦ v₁'; …; tₙ' ↦ vₙ'〛) = r
—————————————————————————————————————————————————————————————————————— EvLessEqTextMap
𝕆('LESS_EQ' @('TextMap' σ)
[t₁ ↦ v₁ ; …; tₙ ↦ vₙ ]
[t₁' ↦ v₁'; …; tₙ' ↦ vₙ']) = r
—————————————————————————————————————————————————————————————————————— EvLessEqTypeRep
𝕆('LESS_EQ' @σ ('type_rep' @σ₁) ('type_rep' @σ₂)) = Ok (σ₁ ≤ₜ σ₂)
τ <ₜ τ'
—————————————————————————————————————————————————————————————————————— EvLessEqAnyTypeSmaller
𝕆('LESS_EQ' @σ ('to_any' @τ v) ('to_any' @τ' v')) = OK 'True'
τ' <ₜ τ
—————————————————————————————————————————————————————————————————————— EvLessEqAnyTypeGreater
𝕆('LESS_EQ' @σ ('to_any' @τ v) ('to_any' @τ' v')) = OK 'False'
𝕆('LESS_EQ' @τ v v') = r
—————————————————————————————————————————————————————————————————————— EvLessEqAnyValue
𝕆('LESS_EQ' @σ ('to_any' @τ v) ('to_any' @τ v')) = r
—————————————————————————————————————————————————————————————————————— EvLessEqAbs
𝕆('LESS_EQ' @(σ → τ) v v' = Err 'Try to compare functions'
—————————————————————————————————————————————————————————————————————— EvLessEqTyAbs
𝕆('LESS_EQ' @(∀ α : k . σ) v v' = Err 'Try to compare functions'
—————————————————————————————————————————————————————————————————————— EvLessEqUpdate
𝕆('LESS_EQ' @('Update' σ) v v' = Err 'Try to compare functions'
—————————————————————————————————————————————————————————————————————— EvLessEqScenario
𝕆('LESS_EQ' @('Scenario' σ) v v' = Err 'Try to compare functions'
.. FIXME: https://github.com/digital-asset/daml/issues/2256
Handle contract IDs
* ``GREATER_EQ : ∀ (α:*). α → α → 'Bool'``
The builtin function ``GREATER_EQ`` returns ``'True'`` if the first
argument is greater than or equal to the second argument,
``'False'`` otherwise. The function raises a runtime error if the
arguments are incomparable.
[*Available in version >= 1.11*]
Formally the function is defined as a shortcut for the function::
'GREATER_EQ' ≡
Λ α : ⋆. λ x : α . λ y : b.
'LESS_EQ' @α y x
* ``EQUAL : ∀ (α:*). α → α → 'Bool'``
The builtin function ``EQUAL`` returns ``'True'`` if the first
argument is equal to the second argument, ``'False'`` otherwise. The
function raises a runtime error if the arguments are incomparable.
[*Available in version >= 1.11*]
Formally the function is defined as a shortcut for the function::
'EQUAL' ≡
Λ α : ⋆. λ x : α . λ y : b.
'case' 'LESS_EQ' @α x y 'of'
'True' → 'GREATER_EQ' @α x y
'|' 'False' → 'False'
[*Available in version >= 1.11*]
* ``LESS : ∀ (α:*). α → α → 'Bool'``
The builtin function ``LESS`` returns ``'True'`` if the first
argument is strictly less that the second argument, ``'False'``
otherwise. The function raises a runtime error if the arguments are
incomparable.
[*Available in version >= 1.11*]
Formally the function is defined as a shortcut for the function::
'LESS' ≡
Λ α : ⋆. λ x : α . λ y : b.
'case' 'EQUAL' @α x y 'of'
'True' → 'False'
'|' 'False' → 'LESS_EQ' α x y
* ``GREATER : ∀ (α:*). α → α → 'Bool'``
The builtin function ``LESS`` returns ``'True'`` if the first
argument is strictly greater that the second argument, ``'False'``
otherwise. The function raises a runtime error if the arguments are
incomparable.
[*Available in version >= 1.11*]
Formally the function is defined as a shortcut for the function::
'GREATER' ≡
Λ α : ⋆. λ x : α . λ y : b.
'case' 'EQUAL' @α x y 'of'
'True' → 'False'
'|' 'False' → 'GREATER_EQ' α x y
Boolean functions
~~~~~~~~~~~~~~~~~
* ``EQUAL_BOOL : 'Bool' → 'Bool' → 'Bool'``
Returns ``'True'`` if the two booleans are syntactically equal,
``False`` otherwise.
[*Available in version < 1.11*]
Int64 functions
~~~~~~~~~~~~~~~
* ``ADD_INT64 : 'Int64' → 'Int64' → 'Int64'``
Adds the two integers. Throws an ``ArithmeticError`` exception in
case of overflow.
* ``SUB_INT64 : 'Int64' → 'Int64' → 'Int64'``
Subtracts the second integer from the first one. Throws an
``ArithmeticError`` exception in case of overflow.
* ``MUL_INT64 : 'Int64' → 'Int64' → 'Int64'``
Multiplies the two integers. Throws an ``ArithmeticError`` exception
in case of overflow.
* ``DIV_INT64 : 'Int64' → 'Int64' → 'Int64'``
Returns the quotient of division of the first integer by the second
one. Rounds toward 0 if the real quotient is not an integer.
Throws an ``ArithmeticError`` exception
- if the second argument is ``0``, or
- if the first argument is ``−2⁶³`` and the second one is ``-1``.
* ``MOD_INT64 : 'Int64' → 'Int64' → 'Int64'``
Returns the remainder of the division of the first integer by the
second one. Throws an ``ArithmeticError`` exception if the second
argument is ``0``.
* ``EXP_INT64 : 'Int64' → 'Int64' → 'Int64'``
Returns the exponentiation of the first integer by the second one.
Throws an ``ArithmeticError`` exception in case of overflow.
* ``LESS_EQ_INT64 : 'Int64' → 'Int64' → 'Bool'``
Returns ``'True'`` if the first integer is less or equal than the
second, ``'False'`` otherwise.
* ``GREATER_EQ_INT64 : 'Int64' → 'Int64' → 'Bool'``
Returns ``'True'`` if the first integer is greater or equal than the
second, ``'False'`` otherwise.
* ``LESS_INT64 : 'Int64' → 'Int64' → 'Bool'``
Returns ``'True'`` if the first integer is strictly less than the
second, ``'False'`` otherwise.
* ``GREATER_INT64 : 'Int64' → 'Int64' → 'Bool'``
Returns ``'True'`` if the first integer is strictly greater than
the second, ``'False'`` otherwise.
* ``EQUAL_INT64 : 'Int64' → 'Int64' → 'Bool'``
Returns ``'True'`` if the first integer is equal to the second,
``'False'`` otherwise.
[*Available in version < 1.11*]
* ``INT64_TO_TEXT : 'Int64' → 'Text'``
Returns the decimal representation of the integer as a string.
* ``TEXT_TO_INT64 : 'Text' → 'Optional' 'Int64'``
Given a string representation of an integer returns the integer wrapped
in ``Some``. If the input does not match the regexp ``[+-]?\d+`` or
if the result of the conversion overflows, returns ``None``.
Numeric functions
~~~~~~~~~~~~~~~~~
* ``ADD_NUMERIC : ∀ (α : nat) . 'Numeric' α → 'Numeric' α → 'Numeric' α``
Adds the two decimals. The scale of the inputs and the output is
given by the type parameter `α`. Throws an ``ArithmeticError``
exception in case of overflow.
* ``SUB_NUMERIC : ∀ (α : nat) . 'Numeric' α → 'Numeric' α → 'Numeric' α``
Subtracts the second decimal from the first one. The scale of the
inputs and the output is given by the type parameter `α`. Throws an
``ArithmeticError`` exception in case of overflow.
* ``MUL_NUMERIC : ∀ (α₁ α₂ α : nat) . 'Numeric' α₁ → 'Numeric' α₂ → 'Numeric' α``
Multiplies the two numerics and rounds the result to the closest
multiple of ``10⁻ᵅ`` using `banker's rounding convention
<https://en.wikipedia.org/wiki/Rounding#Round_half_to_even>`_. The
type parameters `α₁`, `α₂`, `α` define the scale of the first input,
the second input, and the output, respectively. Throws an
``ArithmeticError`` exception in case of overflow.
* ``DIV_NUMERIC : ∀ (α₁ α₂ α : nat) . 'Numeric' α₁ → 'Numeric' α₂ → 'Numeric' α``
Divides the first decimal by the second one and rounds the result to
the closest multiple of ``10⁻ᵅ`` using `banker's rounding convention
<https://en.wikipedia.org/wiki/Rounding#Round_half_to_even>`_ (where
`n` is given as the type parameter). The type parameters `α₁`,
`α₂`, `α` define the scale of the first input, the second input, and
the output, respectively. Throws an ``ArithmeticError`` exception
if the second argument is ``0.0`` or if the computation overflow.
* ``CAST_NUMERIC : ∀ (α₁, α₂: nat) . 'Numeric' α₁ → 'Numeric' α₂``
Converts a decimal of scale `α₁` to a decimal scale `α₂` while
keeping the value the same. Throws an ``ArithmeticError`` exception
in case of overflow or precision loss.
* ``SHIFT_NUMERIC : ∀ (α₁, α₂: nat) . 'Numeric' α₁ → 'Numeric' α₂``
Converts a decimal of scale `α₁` to a decimal scale `α₂` to another
by shifting the decimal point. Thus the output will be equal to the input
multiplied by `1E(α₁-α₂)`.
* ``LESS_EQ_NUMERIC : ∀ (α : nat) . 'Numeric' α → 'Numeric' α → 'Bool'``
Returns ``'True'`` if the first numeric is less or equal than the
second, ``'False'`` otherwise. The scale of the inputs is given by
the type parameter `α`.
* ``GREATER_EQ_NUMERIC : ∀ (α : nat) . 'Numeric' α → 'Numeric' α → 'Bool'``
Returns ``'True'`` if the first numeric is greater or equal than the
second, ``'False'`` otherwise. The scale of the inputs is given by
the type parameter `α`.
* ``LESS_NUMERIC : ∀ (α : nat) . 'Numeric' α → 'Numeric' α → 'Bool'``
Returns ``'True'`` if the first numeric is strictly less than the
second, ``'False'`` otherwise. The scale of the inputs is given by
the type parameter `α`.
* ``GREATER_NUMERIC : ∀ (α : nat) . 'Numeric' α → 'Numeric' α → 'Bool'``
Returns ``'True'`` if the first numeric is strictly greater than the
second, ``'False'`` otherwise. The scale of the inputs is given by
the type parameter `α`.
* ``EQUAL_NUMERIC : ∀ (α : nat) . 'Numeric' α → 'Numeric' α → 'Bool'``
Returns ``'True'`` if the first numeric is equal to the second,
``'False'`` otherwise. The scale of the inputs is given by the type
parameter `α`.
[*Available in version < 1.11*]
* ``NUMERIC_TO_TEXT : ∀ (α : nat) . 'Numeric' α → 'Text'``
Returns the numeric string representation of the numeric. The scale
of the input is given by the type parameter `α`.
* ``TEXT_TO_NUMERIC : ∀ (α : nat) .'Text' → 'Optional' 'Numeric' α``
Given a string representation of a numeric returns the numeric
wrapped in ``Some``. If the input does not match the regexp
``[+-]?\d+(\.d+)?`` or if the result of the conversion cannot
be mapped into a decimal without loss of precision, returns
``None``. The scale of the output is given by the type parameter
`α`.
BigNumeric functions
~~~~~~~~~~~~~~~~~~~~
* ``ADD_BIGNUMERIC : 'BigNumeric' → 'BigNumeric' → 'BigNumeric'``
Adds the two decimals. Throws an ``ArithmeticError`` if the output
is not a valid BigNumeric.
[*Available in version ≥ 1.13*]
* ``SUB_BIGNUMERIC : 'BigNumeric' → 'BigNumeric' → 'BigNumeric'``
Subtracts the two decimals. Throws an ``ArithmeticError`` if the
output is not a valid BigNumeric.
[*Available in version ≥ 1.13*]
* ``MUL_BIGNUMERIC : 'BigNumeric' → 'BigNumeric' → 'BigNumeric'``
Multiplies the two numerics. Throws an ``ArithmeticError`` if the
output is not a valid BigNumeric.
[*Available in version ≥ 1.13*]
* ``DIV_BIGNUMERIC : 'RoundingMode' → 'Int' → 'BigNumeric' → 'BigNumeric' → 'BigNumeric'``
Divides the first decimal by the second one and rounds the result
according the rounding mode. The scale of the output is given by
the second argument. If the result cannot be represented exactly at
the given scale, the result is rounded accordingly the
``roundingMode`` as follows:
- ``'ROUNDING_UP'`` : Round away from zero
- ``'ROUNDING_DOWN'`` : Round towards zero
- ``'ROUNDING_CEILING'`` : Round towards positive infinity.
- ``'ROUNDING_FLOOR'`` : Round towards negative infinity
- ``'ROUNDING_HALF_UP'`` : Round towards the nearest neighbor unless
both neighbors are equidistant, in which case round away from
zero.
- ``'ROUNDING_HALF_DOWN'`` : Round towards the nearest neighbor
unless both neighbors are equidistant, in which case round towards
zero.
- ``'ROUNDING_HALF_EVEN'`` : Round towards the nearest neighbor
unless both neighbors are equidistant, in which case round towards
the even neighbor.
- ``'ROUNDING_UNNECESSARY'`` : Throw an ``ArithmeticError``
exception if the exact result cannot be represented.
Throws an ``ArithmeticError``` if the output is not a valid
BigNumeric.
[*Available in version ≥ 1.13*]
* ``SCALE_BIGNUMERIC : 'BigNumeric' → 'Int64'``
Returns the scale of the BigNumeric
[*Available in version ≥ 1.13*]
* ``PRECISION_BIGNUMERIC : 'BigNumeric' → 'Int64'``
Returns the precision of the BigNumeric
[*Available in version ≥ 1.13*]
* ``SHIFT_RIGHT_BIGNUMERIC : 'Int64' → 'BigNumeric' → 'BigNumeric'``
Multiply the second argument by 10 to the negative power of the
first argument. Throws an ``ArithmeticError`` in case the result
cannot be represented without loss of precision.
[*Available in version ≥ 1.13*]
* ``BIGNUMERIC_TO_TEXT : 'BigNumeric' → 'Text'``
Returns the numeric string representation of the BigNumeric. The
result will be returned at the smallest precision that can represent
the result exactly, i.e., without any trailing zeroes.
[*Available in version ≥ 1.13*]
* ``'BIGNUMERIC_TO_NUMERIC' : ∀ (α : nat). 'BigNumeric' → 'Numeric' α``
Converts the ``BigNumeric`` to a ``Numeric α`` value with scale
``α``. Throws an ``ArithmeticError`` in case the result cannot be
represented without loss of precision.
[*Available in version ≥ 1.13*]
* ``'NUMERIC_TO_BIGNUMERIC' : ∀ (α : nat). 'Numeric' α → 'BigNumeric'``
Converts the ``Numeric`` to a ``BigNumeric``. This is always exact.
[*Available in version ≥ 1.13*]
String functions
~~~~~~~~~~~~~~~~
* ``APPEND_TEXT : 'Text' → 'Text' → 'Text'``
Appends the second string at the end of the first one.
* ``EXPLODE_TEXT : 'Text' → List 'Text'``
Returns the list of the individual `codepoint
<https://en.wikipedia.org/wiki/Code_point>`_ of the string. Note the
codepoints of the string are still of type ``'Text'``.
* ``IMPLODE_TEXT : 'List' 'Text' → 'Text'``
Appends all the strings in the list.
* ``SHA256_TEXT : 'Text' → 'Text'``
Performs the `SHA-256 <https://en.wikipedia.org/wiki/SHA-2>`_
hashing of the UTF-8 string and returns it encoded as a Hexadecimal
string (lower-case).
* ``LESS_EQ_TEXT : 'Text' → 'Text' → 'Bool'``
Returns ``'True'`` if the first string is lexicographically less
or equal than the second, ``'False'`` otherwise.
* ``GREATER_EQ_TEXT : 'Text' → 'Text' → 'Bool'``
Returns ``'True'`` if the first string is lexicographically
greater or equal than the second, ``'False'`` otherwise.
* ``LESS_TEXT : 'Text' → 'Text' → 'Bool'``
Returns ``'True'`` if the first string is lexicographically
strictly less than the second, ``'False'`` otherwise.
* ``GREATER_TEXT : 'Text' → 'Text' → 'Bool'``
Returns ``'True'`` if the first string is lexicographically
strictly greater than the second, ``'False'`` otherwise.
* ``EQUAL_TEXT : 'Text' → 'Text' → 'Bool'``
Returns ``'True'`` if the first string is equal to the second,
``'False'`` otherwise.
[*Available in version < 1.11*]
* ``TEXT_TO_TEXT : 'Text' → 'Text'``
Returns string such as.
* ``TEXT_TO_CODE_POINTS``: 'Text' → 'List' 'Int64'
Returns the list of the Unicode `codepoints
<https://en.wikipedia.org/wiki/Code_point>`_ of the input
string represented as integers.
* ``CODE_POINTS_TO_TEXT``: 'List' 'Int64' → 'Text'
Given a list of integer representations of Unicode codepoints,
return the string built from those codepoints. Throws an error
if one of the elements of the input list is not in the range
from `0x000000` to `0x00D7FF` or in the range from `0x00DFFF`
to `0x10FFFF` (bounds included).
Timestamp functions
~~~~~~~~~~~~~~~~~~~
* ``LESS_EQ_TIMESTAMP : 'Timestamp' → 'Timestamp' → 'Bool'``
Returns ``'True'`` if the first timestamp is less or equal than the
second, ``'False'`` otherwise.
* ``GREATER_EQ_TIMESTAMP : 'Timestamp' → 'Timestamp' → 'Bool'``
Returns ``'True'`` if the first timestamp is greater or equal than
the second, ``'False'`` otherwise.
* ``LESS_TIMESTAMP : 'Timestamp' → 'Timestamp' → 'Bool'``
Returns ``'True'`` if the first timestamp is strictly less than the
second, ``'False'`` otherwise.
* ``GREATER_TIMESTAMP : 'Timestamp' → 'Timestamp' → 'Bool'``
Returns ``'True'`` if the first timestamp is strictly greater than
the second, ``'False'`` otherwise.
* ``EQUAL_TIMESTAMP : 'Timestamp' → 'Timestamp' → 'Bool'``
Returns ``'True'`` if the first timestamp is equal to the second,
``'False'`` otherwise.
[*Available in version < 1.11*]
* ``TIMESTAMP_TO_TEXT : 'Timestamp' → 'Text'``
Returns an `ISO 8601 <https://en.wikipedia.org/wiki/ISO_8601>`_
compliant string representation of the timestamp. The actual format
is as follows. Note that both "``T``" and "``Z``" appear literally
in the string. On the one hand "``T``" separates the date part from
time part, while on the other hand, "``Z``" indicates the zero UTC
offset. ::
YYYY-MM-DDThh:mm:ss.SZ
where:
* ``YYYY`` = four-digit year
* ``MM`` = two-digit month (01=January, etc.)
* ``DD`` = two-digit day of month (01 through 31)
* ``hh`` = two digits of hour (00 through 23)
* ``mm`` = two digits of minute (00 through 59)
* ``ss`` = two digits of second (00 through 59)
* ``S`` = zero to six digits representing a decimal fraction of a
second. In case of zero digits the preceding full stop ("``.``")
is omitted.
Note the exact number of digits used to represent the decimal fraction of
a second is not specified, however, it is guaranteed:
* The output uses at least as many digits as necessary but may be
padded on the right with an unspecified number of "``0``".
* The output will not change within minor version of Daml-LF 1.
Date functions
~~~~~~~~~~~~~~
* ``LESS_EQ_DATE : 'Date' → 'Date' → 'Bool'``
Returns ``'True'`` if the first date is less or equal than the
second, ``'False'`` otherwise.
* ``GREATER_EQ_DATE : 'Date' → 'Date' → 'Bool'``
Returns ``'True'`` if the first date is greater or equal than the
second, ``'False'`` otherwise.
* ``LESS_DATE : 'Date' → 'Date' → 'Bool'``
Returns ``'True'`` if the first date is strictly less than the
second, ``'False'`` otherwise.
* ``GREATER_DATE : 'Date' → 'Date' → 'Bool'``
Returns ``'True'`` if the first date is strictly greater than the
second, ``'False'`` otherwise.
* ``EQUAL_DATE : 'Date' → 'Date' → 'Bool'``
Returns ``'True'`` if the first date is equal to the second,
``'False'`` otherwise.
[*Available in version < 1.11*]
* ``DATE_TO_TEXT : 'Date' → 'Text'``
Returns an `ISO 8601 <https://en.wikipedia.org/wiki/ISO_8601>`_
compliant string representation of the timestamp date. The actual
format is as follows. ::
YYYY-MM-DD
where:
* ``YYYY`` = four-digit year
* ``MM`` = two-digit month (01=January, etc.)
* ``DD`` = two-digit day of month (01 through 31)
Party functions
~~~~~~~~~~~~~~~
* ``LESS_EQ_PARTY : 'Party' → 'Party' → 'Bool'``
Returns ``'True'`` if the first party is less or equal than the
second, ``'False'`` otherwise.
* ``GREATER_EQ_PARTY : 'Party' → 'Party' → 'Bool'``
Returns ``'True'`` if the first party is greater or equal than the
second, ``'False'`` otherwise.
* ``LESS_PARTY : 'Party' → 'Party' → 'Bool'``
Returns ``'True'`` if the first party is strictly less than the
second, ``'False'`` otherwise.
* ``GREATER_PARTY : 'Party' → 'Party' → 'Bool'``
Returns ``'True'`` if the first party is strictly greater than the
second, ``'False'`` otherwise.
* ``EQUAL_PARTY : 'Party' → 'Party' → 'Bool'``
Returns ``'True'`` if the first party is equal to the second,
``'False'`` otherwise.
[*Available in version < 1.11*]
* ``PARTY_TO_QUOTED_TEXT : 'Party' → 'Text'``
Returns a single-quoted ``Text`` representation of the party. It
is equivalent to a call to ``PARTY_TO_TEXT``, followed by quoting
the resulting ``Text`` with single quotes.
[*Available in version < 1.dev*]
* ``PARTY_TO_TEXT : 'Party' → 'Text'``
Returns the string representation of the party. This function,
together with ``TEXT_TO_PARTY``, forms an isomorphism between
`PartyId strings <Literals_>`_ and parties. In other words,
the following equations hold::
∀ p. TEXT_TO_PARTY (PARTY_TO_TEXT p) = 'Some' p
∀ txt p. TEXT_TO_PARTY txt = 'Some' p → PARTY_TO_TEXT p = txt
* ``TEXT_TO_PARTY : 'Text' → 'Optional' 'Party'``
Given the string representation of the party, returns the party,
if the input string is a `PartyId strings <Literals_>`_.
ContractId functions
~~~~~~~~~~~~~~~~~~~~
* ``EQUAL_CONTRACT_ID : ∀ (α : ⋆) . 'ContractId' α → 'ContractId' α → 'Bool'``
Returns ``'True'`` if the first contact id is equal to the second,
``'False'`` otherwise.
* ``COERCE_CONTRACT_ID : ∀ (α : ⋆) (β : ⋆) . 'ContractId' α → 'ContractId' β``
Returns the given contract ID unchanged at a different type.
* ``CONTRACT_ID_TO_TEXT : ∀ (α : ⋆) . 'ContractId' α -> 'Optional' 'Text'``
Always returns ``None`` in ledger code. This function is only useful
for off-ledger code which is not covered by this specification.
[*Available in versions >= 1.11*]
List functions
~~~~~~~~~~~~~~
* ``FOLDL : ∀ (α : ⋆) . ∀ (β : ⋆) . (β → α → β) → β → 'List' α → β``
Left-associative fold of a list.
* ``FOLDR : ∀ (α : ⋆) . ∀ (β : ⋆) . (α → β → β) → β → 'List' α → β``
Right-associative fold of a list.
* ``EQUAL_LIST : ∀ (α : ⋆) . (α → α → 'Bool') → 'List' α → 'List' α → 'Bool'``
Returns ``'False'`` if the two lists have different length or the
elements of the two lists are not pairwise equal according to the
predicate give as first argument.
Text map functions
~~~~~~~~~~~~~~~~~~
**Entry order**: The operations below always return a map with entries
ordered by keys.
* ``TEXTMAP_EMPTY : ∀ α. 'TextMap' α``
Returns the empty TextMap.
* ``TEXTMAP_INSERT : ∀ α. 'Text' → α → 'TextMap' α → 'TextMap' α``
Inserts a new key and value in the map. If the key is already
present in the map, the associated value is replaced with the
supplied value.
* ``TEXTMAP_LOOKUP : ∀ α. 'Text' → 'TextMap' α → 'Optional' α``
Looks up the value at a key in the map.
* ``TEXTMAP_DELETE : ∀ α. 'Text' → 'TextMap' α → 'TextMap' α``
Deletes a key and its value from the map. When the key is not a
member of the map, the original map is returned.
* ``TEXTMAP_TO_LIST : ∀ α. 'TextMap' α → 'List' ⟨ key: 'Text', value: α ⟩``
Converts to a list of key/value pairs. The output list is guaranteed to be
sorted according to the ordering of its keys.
* ``TEXTMAP_SIZE : ∀ α. 'TextMap' α → 'Int64'``
Return the number of elements in the map.
Generic map functions
~~~~~~~~~~~~~~~~~~~~~
**Validity of Keys:** A key is valid if and only if it is equivalent
to itself according to the builtin function ``EQUAL``. Attempts to
use an invalid key in the operations listed under always result
in a runtime error.
Of particular note, the following values are never valid keys:
* Lambda expressions ``λ x : τ . e``
* Type abstractions ``Λ α : k . e``
* (Partially applied) built-in functions
* Update statement
* Any value containing an invalid key
**Entry order**: The operations below always return a map with entries
ordered by keys according to the comparison function ``LESS``.
* ``GENMAP_EMPTY : ∀ α. ∀ β. 'GenMap' α β``
Returns an empty generic map.
[*Available in versions >= 1.11*]
* ``GENMAP_INSERT : ∀ α. ∀ β. α → β → 'GenMap' α β → 'GenMap' α β``
Inserts a new key and value in the map. If the key is already
present according the builtin function ``EQUAL``, the associated
value is replaced with the supplied value, otherwise the key/value
is inserted in order according to the builtin function ``LESS`` applied
on keys. This raises a runtime error if it tries to compare
incomparable values.
[*Available in versions >= 1.11*]
Formally the builtin function ``GENMAP_INSERT`` semantics is defined
by the following rules. ::
𝕆('EQUAL' @σ v v) = Err t
—————————————————————————————————————————————————————————————————————— EvGenMapInsertReplaceErr
𝕆('GENMAP_INSERT' @σ @τ 〚v₁ ↦ w₁; … ; vₙ ↦ wₙ〛 v w) = Err t
—————————————————————————————————————————————————————————————————————— EvGenMapInsertEmpty
𝕆('GENMAP_INSERT' @σ @τ 〚〛 v w) = 〚v ↦ w〛
𝕆('EQUAL' @σ vᵢ v) = Ok 'True' for some i ∈ 1, …, n
—————————————————————————————————————————————————————————————————————— EvGenMapInsertReplace
𝕆('GENMAP_INSERT' @σ @τ 〚v₁ ↦ w₁; …; vₙ ↦ wₙ〛 v w) =
'Ok' 〚v₁ ↦ w₁; …; vᵢ₋₁ ↦ wᵢ₋₁; vᵢ ↦ w; vᵢ₊₁ ↦ wᵢ₊₁; …; vₙ ↦ wₙ〛
𝕆('LESS' @σ v v₁) = Ok 'True'
—————————————————————————————————————————————————————————————————————— EvGenMapInsertInsertFirst
𝕆('GENMAP_INSERT' @σ @τ 〚v₁ ↦ w₁; …; vₙ ↦ wₙ〛 v w) =
'Ok' 〚v ↦ w; v₁ ↦ w₁; …; vₙ ↦ wₙ〛
𝕆('LESS' @σ vᵢ₋₁ v) = Ok 'True'
𝕆('LESS' @σ v vᵢ) = Ok 'True'
for some i ∈ 2, …, n-1
—————————————————————————————————————————————————————————————————————— EvGenMapInsertInsertMiddle
𝕆('GENMAP_INSERT' @σ @τ 〚v₁ ↦ w₁; … ; vₙ ↦ wₙ〛 v w) =
'Ok' 〚v₁ ↦ w₁; … ; vᵢ₋₁ ↦ wᵢ₋₁; v ↦ w; vᵢ ↦ wᵢ; … ; vₙ ↦ wₙ〛
𝕆('LESS' @σ vₙ v) = Ok 'True'
—————————————————————————————————————————————————————————————————————— EvGenMapInsertInsertLast
𝕆('GENMAP_INSERT' @σ @τ 〚v₁ ↦ w₁; …; vₙ ↦ wₙ〛 v w) =
'Ok' 〚v₁ ↦ w₁; …; vₙ ↦ wₙ; v ↦ w〛
* ``GENMAP_LOOKUP : ∀ α. ∀ β. α → 'GenMap' α β → 'Optional' α``
Looks up the value at a key in the map using the builtin function
``EQUAL`` to test key equality. This raises a runtime error if it
try to compare incomparable values.
[*Available in versions >= 1.11*]
Formally the builtin function ``GENMAP_LOOKUP`` semantics is defined
by the following rules. ::
𝕆('EQUAL' @σ v v) = Err t
—————————————————————————————————————————————————————————————————————— EvGenMapInsertReplaceErr
𝕆('GENMAP_LOOKUP' @σ @τ 〚v₁ ↦ w₁; … ; vₙ ↦ wₙ〛 v) = Err t
—————————————————————————————————————————————————————————————————————— EvGenMapLookupErr
𝕆('GENMAP_LOOKUP' @σ @τ 〚v₁ ↦ w₁; … ; vₙ ↦ wₙ〛 v) = Err t
𝕆('EQUAL' @σ vᵢ v) = Ok 'True' for some i ∈ 1, …, n
—————————————————————————————————————————————————————————————————————— EvGenMapLookupPresent
𝕆('GENMAP_LOOKUP' @σ @τ 〚v₁ ↦ w₁; … ; vₙ ↦ wₙ〛 v) =
'Ok' (Some wᵢ)
𝕆('EQUAL' @σ vᵢ v) = Ok 'False' for all i ∈ 1, …, n
—————————————————————————————————————————————————————————————————————— EvGenMapLookupAbsent
𝕆('GENMAP_LOOKUP' @σ @τ 〚v₁ ↦ w₁; … ; vₙ ↦ wₙ〛 v) =
'Ok' None
* ``GENMAP_DELETE : ∀ α. ∀ β. α → 'GenMap' α β → 'GenMap' α β``
Deletes a key and its value from the map, using the builtin function
``EQUAL`` to test key equality. When the key is not a member of the
map, the original map is returned. This raises a runtime error if it
try to compare incomparable values.
[*Available in versions >= 1.11*]
Formally the builtin function ``GENMAP_DELETE`` semantics is defined
by the following rules. ::
𝕆('EQUAL' @σ v v) = Err t
—————————————————————————————————————————————————————————————————————— EvGenMapDeleteErr
𝕆('GENMAP_DELETE' @σ @τ 〚v₁ ↦ w₁; … ; vₙ ↦ wₙ〛 v) = Err t
𝕆('EQUAL' @σ vᵢ v) = Ok 'True' for some i ∈ 1, …, n
—————————————————————————————————————————————————————————————————————— EvGenMapDeletePresent
𝕆('GENMAP_DELETE' @σ @τ 〚v₁ ↦ w₁; … ; vₙ ↦ wₙ〛 v) =
Ok' 〚v₁ ↦ w₁; … ; vᵢ₋₁ ↦ wᵢ₋₁; vᵢ₊₁ ↦ wᵢ₊₁; … ; vₙ ↦ wₙ〛
𝕆('EQUAL' @σ vᵢ v) = Ok 'False' for all i ∈ 1, …, n
—————————————————————————————————————————————————————————————————————— EvGenMapDeleteAbsent
𝕆('GENMAP_DELETE' @σ @τ 〚v₁ ↦ w₁; … ; vₙ ↦ wₙ〛 v) =
'Ok' 〚v₁ ↦ w₁; … ; vₙ ↦ wₙ〛
* ``GENMAP_KEYS : ∀ α. ∀ β. 'GenMap' α β → 'List' α``
Get the list of keys in the map. The keys are returned in the order
they appear in the map.
[*Available in versions >= 1.11*]
Formally the builtin function ``GENMAP_KEYS`` semantics is defined
by the following rules. ::
—————————————————————————————————————————————————————————————————————— EvGenMapKeysEmpty
𝕆('GENMAP_KEYS' @σ @τ 〚〛) = 'Ok' (Nil @σ)
𝕆('GENMAP_KEYS' @σ @τ 〚v₁ ↦ w₁; … ; vₙ ↦ wₙ〛) = 'Ok' vₗ
—————————————————————————————————————————————————————————————————————— EvGenMapKeysNonEmpty
𝕆('GENMAP_KEYS' @σ @τ 〚v₀ ↦ w₀; v₁ ↦ w₁; … ; vₙ ↦ wₙ〛) =
'Ok' (Cons @σ v₀ vₗ)
* ``GENMAP_VALUES : ∀ α. ∀ β. 'GenMap' α β → 'List' β``
Get the list of values in the map. The values are returned in the
order they appear in the map (i.e. sorted by key).
[*Available in versions >= 1.11*]
Formally the builtin function ``GENMAP_VALUES`` semantics is defined
by the following rules. ::
—————————————————————————————————————————————————————————————————————— EvGenMapValuesEmpty
𝕆('GENMAP_VALUES' @σ @τ 〚〛) = 'Ok' (Nil @τ)
𝕆('GENMAP_VALUES' @σ @τ 〚v₁ ↦ w₁; … ; vₙ ↦ wₙ〛) = 'Ok' wₗ
—————————————————————————————————————————————————————————————————————— EvGenMapValuesNonEmpty
𝕆('GENMAP_KEYS' @σ @τ 〚v₀ ↦ w₀; v₁ ↦ w₁; … ; vₙ ↦ wₙ〛) =
'Ok' (Cons @τ w₀ wₗ)
* ``GENMAP_SIZE : ∀ α. ∀ β. 'GenMap' α β → 'Int64'``
Return the number of elements in the map.
[*Available in versions >= 1.11*]
Type Representation function
~~~~~~~~~~~~~~~~~~~~~~~~~~~~
* ``EQUAL_TYPE_REP`` : 'TypeRep' → 'TypeRep' → 'Bool'``
Returns ``'True'`` if the first type representation is syntactically equal to
the second one, ``'False'`` otherwise.
[*Available in versions >= 1.7*]
Conversions functions
~~~~~~~~~~~~~~~~~~~~~
* ``INT64_TO_NUMERIC : ∀ (α : nat) . 'Int64' → 'Numeric' α``
Returns a numeric representation of the integer. The scale of the
output and the output is given by the type parameter `α`. Throws an
``ArithmeticError`` exception in case of overflow.
* ``NUMERIC_TO_INT64 : ∀ (α : nat) . 'Numeric' α → 'Int64'``
Returns the integral part of the given numeric -- in other words,
rounds towards 0. The scale of the input and the output is given by
the type parameter `α`. Throws an ``ArithmeticError`` exception in
case of overflow.
* ``TIMESTAMP_TO_UNIX_MICROSECONDS : 'Timestamp' → 'Int64'``
Converts the timestamp in integer.
* ``UNIX_MICROSECONDS_TO_TIMESTAMP : 'Int64' → 'Date'``
Converts the integer in a timestamp. Throws an ``ArithmeticError``
exception in case of overflow.
* ``DATE_TO_UNIX_DAYS : 'Date' → 'Int64'``
Converts the date in integer.
* ``UNIX_DAYS_TO_DATE : 'Int64' → 'Date'``
Converts the integer in date. Throws an ``ArithmeticError``
exception in case of overflow.
Error functions
~~~~~~~~~~~~~~~
** ``ERROR : ∀ (α : ⋆) . 'Text' → α``
Throws a fatal error with the string as message.
* ``ANY_EXCEPTION_MESSAGE : 'AnyException' → 'Text'``
[*Available in version >= 1.14*]
Extract the error message from an ``'AnyException'``.
Debugging functions
~~~~~~~~~~~~~~~~~~~
* ``TRACE : ∀ (α : ⋆) . 'Text' → α → α``
Returns the second argument as is. This function is intended to be
used for debugging purposes, but note that we do not specify how
ledger implementations make use of it.
Program serialization
^^^^^^^^^^^^^^^^^^^^^
Daml-LF programs are serialized using `Protocol Buffers
<https://developers.google.com/protocol-buffers/>`_. The
machine-readable definition of the serialization for Daml-LF major
version 1 can be found in the `daml_lf_1.proto
<../archive/src/main/protobuf/com/daml/daml_lf_dev/daml_lf_1.proto>`_
file.
For the sake of brevity, we do no exhaustively describe how Daml-LF
programs are (un)serialized into protocol buffer. In the rest of this
section, we describe the particularities of the encoding and how
Daml-LF version impacts it.
Specificities of Daml-LF serialization
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Required fields
...............
As a rule of the thumb, all non `oneof fields
<https://developers.google.com/protocol-buffers/docs/proto3#oneof>`_
are required in the serialization. Similarly among fields within the
same oneof definition at least one must be defined. Exceptions are
exhaustively indicated in the `daml_lf_1.proto
<../archive/src/main/protobuf/com/daml/daml_lf_dev/daml_lf_1.proto>`_
file with comment::
// *Optional*
The deserialization process will reject any message in which a required
field is missing.
Package hash
............
In order to guarantee the integrity when stored on the drive or
communicated through the network, a package is paired with the hash of
its contents. The function used to produce the hash is specified
explicitly. Currently only SHA256 is supported. Software consuming the
serialized package must recompute the hash and make sure that it
matches with the serialized hash.
Package reference
.................
As commented in the `Identifiers`_ section, the package identifier is
actually the hash of the serialized package's AST. To circumvent the
circular dependency problem when computing the hash, package
identifiers are replaced by the so-called *package references* in
serialized AST. Those references are encoded by the following
message::
message PackageRef {
oneof Sum {
Unit self = 1;
string package_id_str = 2;
}
}
One should use either the field ``self`` to refer the current package or
``package_id_str`` to refer to an external package. During deserialization
``self`` references are replaced by the actual digest of the package in
which it appears.
Template precondition
.....................
The precondition of a template is serialized by an optional field in
the corresponding Protocol buffer message. If this field is undefined,
then the deserialization process will use the expression ``True`` as
default.
Data structure compression
..........................
In order to save space and to limit recursion depth, the serialization
generally “compresses” structures that are often repeated, such as
applications, let bindings, abstractions, list constructors, etc.
However, for the sake of simplicity, the specification presented here
uses a normal binary form.
For example, consider the following message that encodes expression
application ::
message App {
Expr fun = 1;
repeated Expr args = 2;
}
The message is interpreted as n applications ``(e e₁ … eₙ)`` where
``eᵢ`` is the interpretation of the ``iᵗʰ`` elements of ``args``
(whenever ``1 ≤ i ≤ n``) and ``e`` is the interpretation of ``fun``.
Note that the Daml-LF deserialization process verifies the repeated
fields of those compressed structures are non-empty. For instance, the
previous message can be used only if it encodes at least one
application.
Message fields of compressed structure that should not be empty - such
as the ``args`` field of the ``App`` message - are annotated in the
`daml_lf_1.proto
<../archive/src/main/protobuf/com/daml/daml_lf_dev/daml_lf_1.proto>`_
file with the comments::
// * must be non empty *
Maps
....
The program serialization format does not provide any direct way to
encode either `TextMap` or `GenMap`. Daml-LF programs can create such
objects only dynamically using the builtin functions prefixed by
`TEXTMAP_` or `'GENMAP_'`
Validation
~~~~~~~~~~
To prevent the engine from running buggy, damaged, or malicious
programs, serialized packages must be validated before execution. Two
validation phases can be distinguished.
* The first phase happens during deserialization itself. It is
responsible for checking the following points:
* The declared `hash <Package hash_>`_ of the package matches
the recomputed hash of its serialization.
* The format of `identifiers`_ and `literals`_ follow this
specification.
* Repeated fields of `Compressed structures <Data structure
compression_>`_ are non-empty.
* The encoding complies with the declared `version <version
history_>`_. For example, optional values are only used in version
1.1 or later.
The reader may refer to the `daml_lf_1.proto
<../archive/src/main/protobuf/com/daml/daml_lf_dev/daml_lf_1.proto>`_
file where those requirements are exhaustively described as comments
between asterisks (``*``).
* The second phase occurs after the deserialization, on the complete
abstract syntax tree of the package. It is concerned with the
`well-formedness <Well-formed packages_>`_ of the package.
An engine compliant with the present specification must accept loading a
package if and only if the latter of these two validation passes.
Serialization changes since version 1.6
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
As explained in `Version history`_ section, Daml-LF programs are
accompanied by a number version. This enables the Daml-LF
deserialization process to interpret different versions of the
language in a backward compatibility way. During deserialization, any
encoding that does not follow the minor version provided is rejected.
Below we list, in chronological order, all the changes that have been
introduced to the serialization format since version 1.6
String Interning
................
To provide string sharing, the so-called *string interning* mechanism
allows the strings within messages to be stored in a global table and
referenced by their index.
The field ``Package.interned_strings`` is a list of strings. A
so-called `interned string` is a valid zero-based index of this
list. An `interned string` is interpreted as the string it points to
in ``Package.interned_strings``.
+ An `interned package id` is an `interned string` that can be
interpreted as a valid `PackageId string`.
+ An `interned party` is an `interned string` that can be interpreted
as a valid `Party string`.
+ An `interned numeric id` is an `interned string` that can be
interpreted as a valid `numeric` literal.
+ An `interned text` is an `interned string` interpreted as a text
literal
+ An `interned identifier` is an `interned string` that can be
interpreted as a valid `identifier`
Starting from Daml-LF 1.7, all ``string`` (or ``repeated string``)
fields with the suffix ``_str`` are forbidden. Alternative fields of
type ``int32`` (or ``repeated int32``) with the suffix
``_interned_str`` must be used instead. Except
``PackageRef.package_id_interned_str`` which is [*Available in
versions >= 1.6*], all fields with suffix ``_interned_str`` are
[*Available in versions >= 1.7*]. The deserialization process will
reject any Daml-LF 1.7 (or later) that does not comply with this
restriction.
Name Interning
..............
[*Available in versions >= 1.7*]
To provide sharing of `names <Identifiers_>`_, the so-called *name
interning* mechanism allows the *names* within messages to be stored
in a global table and be referenced by their index.
``InternedDottedName`` is a non-empty list of valid interned
identifiers. Such message is interpreted as the name built from the
sequence the interned identifiers it contains. The field
``Package.interned_dotted_names`` is a list of such messages. A
so-called `interned name` is a valid zero-based index of this list. An
`interned name` is interpreted as the name built form the `name` it
points to in ``Package.interned_dotted_names``.
Starting from Daml-LF 1.7, all ``DottedName`` (or ``repeated
string``) fields with the suffix ``_dname`` are forbidden. Alternative
fields of type ``int32`` with the suffix ``_interned_dname``
[*Available in versions >= 1.7*] must be used instead. The
deserialization process will reject any Daml-LF 1.7 (or later) that
that does not comply this restriction.
Nat kind and Nat types
......................
[*Available in versions >= 1.7*]
The deserialization process will reject any Daml-LF 1.6 (or earlier)
that uses ``nat`` field in ``Kind`` or ``Type`` messages.
Starting from Daml-LF 1.7 those messages are deserialized to ``nat``
kind and ``nat`` type respectively. The field ``nat`` of ``Type``
message must be a positive integer.
Note that despite there being no concrete way to build Nat types in a
Daml-LF 1.6 (or earlier) program, those are implicitly generated when
reading as Numeric type and Numeric builtin as described in the next
section.
Parametric scaled Decimals
..........................
[*Available in versions >= 1.7*]
Daml-LF 1.7 is the first version that supports parametric scaled
decimals. Prior versions have decimal number with a fixed scale of 10
called Decimal. Backward compatibility with the current specification
is achieved as follows:
On the one hand, in case of Daml-LF 1.6 archive:
- The ``decimal`` field of the ``PrimLit`` message must match the
regexp::
``[+-]?\d{1,28}(.[0-9]\d{1-10})?``
The deserialization process will silently convert any message that
contains such field to a numeric literal of scale 10. The
deserialization process will reject any non-compliant program.
- ``PrimType`` message with a field ``decimal`` set are translated to
``(Numeric 10)`` type when deserialized.
- Decimal ``BuiltinFunction`` messages are translated as follows :
+ ``ADD_DECIMAL`` message is translated to ``(ADD_NUMERIC @10)``
+ ``SUB_DECIMAL`` message is translated to ``(SUB_NUMERIC @10)``
+ ``MUL_DECIMAL`` message is translated to ``(MUL_NUMERIC @10)``
+ ``DIV_DECIMAL`` message is translated to ``(DIV_NUMERIC @10)``
+ ``ROUND_DECIMAL`` message is translated to ``(ROUND_NUMERIC @10)``
+ ``LESS_EQ_DECIMAL`` message is translated to ``(LESS_EQ_NUMERIC @10)``
+ ``GREATER_EQ_DECIMAL`` message is translated to ``(GREATER_EQ_NUMERIC @10)``
+ ``LESS_DECIMAL`` message is translated to ``(LESS_NUMERIC @10)``
+ ``GREATER_DECIMAL`` message is translated to ``(GREATER_NUMERIC @10)``
+ ``GREATER_DECIMAL`` message is translated to ``(GREATER_NUMERIC @10)``
+ ``EQUAL_DECIMAL`` message is translated to ``(EQUAL_NUMERIC @10)``
+ ``DECIMAL_TO_TEXT`` message is translated to ``(NUMERIC_TO_TEXT @10)``
+ ``TEXT_TO_DECIMAL`` message is translated to ``(TEXT_TO_NUMERIC @10)`` [*Available in versions >= 1.5*]
+ ``INT64_TO_DECIMAL`` message is translated to ``(INT64_TO_NUMERIC @10)``
+ ``DECIMAL_TO_INT64`` message is translated to ``(NUMERIC_TO_INT64 @10)``
- Numeric types, literals and builtins cannot be referred directly.
In other words ``numeric`` fields in ``PrimLit`` and ``PrimType``
messages must remain unset and Numeric ``BuiltinFunction`` (those
containing ``NUMERIC`` in their name) are forbidden. The
deserialization process will reject any Daml-LF 1.6 (or earlier)
that does not comply those restrictions.
On the other hand, starting from Daml-LF 1.7:
- The ``numeric`` field of the ``PrimLit`` message must match the
regexp:
``[-]?([1-9]\d*|0).\d*``
with the addition constrains that it contains at most 38 digits
(ignoring a possibly leading ``0``). The deserialization process
will use the number of digits on the right of the decimal dot
as scale when converting the message to numeric literals. The
deserialization process will reject any non-compliant program.
- Decimal types, literals and builtins cannot be referred directly.
In other words ``decimal`` fields in ``PrimLit`` and ``PrimType``
messages must remain unset and Decimal ``BuiltinFunction`` (those
containing ``DECIMAL`` in their name are forbidden). The
deserialization process will reject any Daml-LF 1.7 (or later)
that does not comply those restrictions.
Any type and type representation
................................
Daml-LF 1.7 is the first version that supports any type and
type representation.
The deserialization process will reject any Daml-LF 1.6 program using
this data structure.
Generic Equality/Order
......................
[*Available in versions >= 1.11*]
The deserialization process will reject any Daml-LF 1.8 (or earlier)
program using the following builtin functions ``EQUAL``, ``LESS_EQ``,
``LESS``, ``GREATER_EQ``, ``GREATER``
The deserialization process will reject any Daml-LF 1.11 (or latter)
program using the following builtin functions , ``EQUAL_INT64``,
``EQUAL_NUMERIC``, ``EQUAL_TEXT``, ``EQUAL_TIMESTAMP``,
``EQUAL_DATE``, ``EQUAL_PARTY``, ``EQUAL_BOOL``,
``EQUAL_CONTRACT_ID``, ``EQUAL_TYPE_REP`` ``LEQ_INT64``,
``LEQ_NUMERIC``, ``LEQ_TEXT``, ``LEQ_TIMESTAMP``, ``LEQ_DATE``,
``LEQ_PARTY``, ``LESS_INT64``, ``LESS_NUMERIC``, ``LESS_TEXT``,
``LESS_TIMESTAMP``, ``LESS_DATE``, ``LESS_PARTY``, ``GEQ_INT64``,
``GEQ_NUMERIC``, ``GEQ_TEXT``, ``GEQ_TIMESTAMP``, ``GEQ_DATE``,
``GEQ_PARTY``, ``GREATER_INT64``, ``GREATER_NUMERIC``,
``GREATER_TEXT``, ``GREATER_TIMESTAMP``, ``GREATER_DATE``,
``GREATER_PARTY``.
Generic Map
............
[*Available in versions >= 1.11*]
The deserialization process will reject any Daml-LF 1.8 (or earlier)
program using the builtin type ``GENMAP`` or the builtin functions
``GENMAP_EMPTY``, ``GENMAP_INSERT``, ``GENMAP_LOOKUP``,
``GENMAP_DELETE``, ``GENMAP_KEYS``, ``GENMAP_VALUES``,
``GENMAP_SIZE``.
exercise_by_key
...............
[*Available in versions >= 1.11*]
The deserialization process will reject any Daml-LF 1.8 (or earlier)
program using the field ``exercise_by_key`` in the ``Update`` message.
CONTRACT_ID_TO_TEXT
...................
[*Available in versions >= 1.11*]
The deserialization process will reject any Daml-LF 1.8 (or earlier)
program using the builtin function ``CONTRACT_ID_TO_TEXT``.
Choice observers
................
[*Available in versions >= 1.11*]
An optional `observer` expression may be attached to a flexible
choice. This allows the specification of additional parties to whom
the sub-transaction is disclosed.
The deserialization process will reject any Daml-LF 1.8 (or earlier)
program using the field ``observers`` in the ``TemplateChoice``
message. The missing ``observers`` field is interpreted as an
empty list of observers.
BigNumeric
..........
[*Available in versions >= 1.13*]
The deserialization process will reject any Daml-LF 1.12 (or earlier)
program using:
- ``BigNumeric`` primitive type,
- ``RoundingMode`` primitive type,
- any of the literals ``ROUNDING_UP``, ``ROUNDING_DOWN``,
``ROUNDING_CEILING``, ``ROUNDING_FLOOR``, ``ROUNDING_HALF_UP``,
``ROUNDING_HALF_DOWN``, ``ROUNDING_HALF_EVEN``,
``ROUNDING_UNNECESSARY``,
- any of the builtins ``SCALE_BIGNUMERIC``, ``PRECISION_BIGNUMERIC``,
``ADD_BIGNUMERIC``, ``SUB_BIGNUMERIC``, ``MUL_BIGNUMERIC``,
``DIV_BIGNUMERIC``, ``SHIFT_RIGHT_BIGNUMERIC``,
``BIGNUMERIC_TO_NUMERIC``, ``NUMERIC_TO_BIGNUMERIC``,
``BIGNUMERIC_TO_TEXT``.
Exception
..........
[*Available in versions >= 1.14*]
Daml-LF 1.14 is the first version that supports Exceptions.
The deserialization process will reject any Daml-LF 1.13 (or earlier)
program exception using:
- ``AnyException`` primitive type,
- ``ToAnyException``, ``FromAnyException``, and ``Throw`` expressions,
- ``TryCatch`` update,
- ``ANY_EXCEPTION_MESSAGE`` builtin functions.
.. Local Variables:
.. eval: (flyspell-mode 1)
.. eval: (set-input-method "TeX")
.. End:
Reference in New Issue View Git Blame Copy Permalink