Causality and interoperability documentation (#6920)

CHANGELOG_BEGIN
Add documentation for the ordering guarantees on the Ledger API
and for causal consistency with interoperable ledgers
CHANGELOG_END

Co-authored-by: Ognjen Maric <ognjen.maric@digitalasset.com>
Co-authored-by: Bernhard Elsner <40762178+bame-da@users.noreply.github.com>

docs/source/app-dev/services.rst

@@ -1,6 +1,8 @@
 .. Copyright (c) 2020 Digital Asset (Switzerland) GmbH and/or its affiliates. All rights reserved.
 .. SPDX-License-Identifier: Apache-2.0
 
+.. _ledger-api-services:
+   
 The Ledger API services
 #######################
 
@@ -38,6 +40,8 @@ Glossary
 - A ``submission`` is a proposed transaction, consisting of a list of ``commands``, which correspond to the top-level ``actions`` in that transaction.
 - A ``completion`` indicates the success or failure of a ``submission``.
 
+.. _ledger-api-submission-services:
+  
 Submitting commands to the ledger
 *********************************
 
@@ -155,6 +159,8 @@ Verbosity
 
 See :ref:`verbosity` above.
 
+.. _ledger-api-utility-services:
+
 Utility services
 ****************
 
@@ -191,13 +197,15 @@ This configuration includes the maximum command deduplication time (see `Command
 
 For full details, see :ref:`the proto documentation for the service <com.daml.ledger.api.v1.LedgerConfigurationService>`.
 
-.. _time-service:
+.. _ledger-api-testing-services:
 
 Testing services
 ****************
 
 **These are only for use for testing with the Sandbox, not for on production ledgers.**
 
+.. _time-service:
+
 Time service
 ============
 

docs/source/concepts/interoperability.rst

@@ -0,0 +1,477 @@
+.. Copyright (c) 2020 Digital Asset (Switzerland) GmbH and/or its affiliates. All rights reserved.
+.. SPDX-License-Identifier: Apache-2.0
+   
+.. _interoperable-ledgers:
+
+Ledger Interoperability
+#######################
+
+Certain DAML ledgers can interoperate with other DAML ledgers.
+That is, the contracts created on one ledger can be used and archived in transactions on other ledgers.
+Some Participant Nodes can connect to multiple ledgers and provide their parties unified access to those ledgers via the :ref:`Ledger API <ledger-api-services>`.
+For example, when an organization initially deploys two workflows to two DAML ledgers, it can later compose those workflows into a larger workflow that spans both ledgers.
+
+Interoperability may limit the visibility a Participant Node has into a party's ledger projection, i.e., its :ref:`local ledger <local-ledger>`, when the party is hosted on multiple Participant Nodes.
+These limitations influence what parties can observe via the Ledger API of each Participant Node.
+In particular, interoperability affects which events a party observes and their order.
+This document explains the visibility limitations due to interoperability and their consequences for the Transaction Service, by :ref:`example <interop-limitation-examples>` and formally by introducing interoperable versions of :ref:`causality graphs <interop-causality-graph>` and :ref:`projections <ledger-aware-projection>`.
+
+The presentation assumes that you are familiar with the following concepts:
+
+* The :ref:`Ledger API <ledger-api-services>`
+
+* The :ref:`DAML Ledger Model <da-ledgers>`
+
+* :ref:`Local ledgers and causality graphs <local-ledger>`
+
+.. note::
+   Interoperability for DAML ledgers is under active development.
+   This document describes the vision for interoperability
+   and gives an idea of how the Ledger API services may change and what guarantees are provided.
+   The described services and guarantees may change without notice as the interoperability implementation proceeds.
+
+.. _interop-limitation-examples:
+   
+Interoperability examples
+*************************
+   
+.. _interoperable-topology:
+
+Topology
+========
+
+Participant Nodes connect to DAML ledgers and parties access projections of these ledgers via the Ledger API.
+The following picture shows such a setup.
+
+.. https://app.lucidchart.com/documents/edit/6b818d37-cf4c-4513-9d31-d68acddf4533
+
+.. figure:: ./images/multiple-domains.svg
+   :align: center
+   :name: multiple-ledgers
+
+   Example topology with three interoperable ledgers
+
+The components in this diagram are the following:
+
+* There is a set of interoperable **DAML ledgers**: Ledger 1 (green) and Ledger 2 (yellow).
+
+* Each **Participant Node** is connected to a subset of the DAML ledgers.
+  
+  - Participant Nodes 1 and 3 are connected to Ledger 1 and 2.
+  - Participant Node 2 is connected to Ledger 1 only.
+
+* Participant Nodes host parties on a subset of the DAML ledgers they are connected to.
+  A Participant Node provides a party access to the DAML ledgers that it hosts the party on.
+
+  - Participant Node 1 hosts Alice on Ledger 1 and 2.
+  - Participant Node 2 hosts Alice on Ledger 1.
+  - Participant Node 3 hosts the painter on Ledger 1 and 2.
+
+.. _interoperable-aggregation:
+
+Aggregation at the participant
+==============================
+
+The Participant Node assembles the updates from these ledgers and outputs them via the party's Transaction Service and Active Contract Service.
+When a Participant Node hosts a party only on a subset of the interoperable DAML ledgers,
+then the transaction and active contract services of the Participant Node are derived only from those ledgers.
+
+For example, in the :ref:`above topology <multiple-ledgers>`, when a transaction creates a contract with stakeholder Alice on Ledger 2,
+then `P1`\ 's transaction stream for Alice will emit this transaction and report the contract as active, but Alice's stream at `P2` will not.
+
+
+.. _enter-leave-event:
+
+Enter and Leave events
+======================
+
+With interoperability, a transaction can use a contract whose creation was recorded on a different ledger.
+In the :ref:`above topology <multiple-ledgers>`, e.g., one transaction creates a contract `c1` with stakeholder Alice on Ledger 1 and another archives the contract on Ledger 2.
+Then the Participant Node `P2` outputs the **Create** action as a ``CreatedEvent``, but not the **Exercise** in form of an ``ArchiveEvent`` on the transaction service
+because Ledger 2 can not notify `P2` as `P2` does not host Alice on Ledger 2.
+Conversely, when one transaction creates a contract `c2` with stakeholder Alice on Ledger 2 and another archives the contract on Ledger 1, then `P2` outputs the ``ArchivedEvent``, but not the ``CreatedEvent``.
+
+To keep the transaction stream consistent, `P2` additionally outputs a **Leave** `c1` action on Alice's transaction stream.
+This action signals that the Participant Node no longer outputs events concerning this contract;
+in particular not when the contract is archived.
+The contract is accordingly no longer reported in the active contract service and cannot be used by command submissions.
+
+Conversely, `P2` outputs an **Enter** `c2` action some time before the ``ArchivedEvent`` on the transaction stream.
+This action signals that the Participant Node starts outputting events concerning this contract.
+The contract is reported in the Active Contract Service and can be used by command submission.
+
+The actions **Enter** and **Leave** are similar to a **Create** and a consuming **Exercise** action, respectively, except that **Enter** and **Leave** may occur several times for the same contract whereas 
+there should be at most one **Create** action and at most one consuming **Exercise** action for each contract.
+
+These **Enter** and **Leave** events are generated by the underlying interoperability protocol.
+This may happen as part of command submission or for other reasons, e.g., load balancing.
+It is guaranteed that the **Enter** action precedes contract usage, subject to the trust assumptions of the underlying ledgers and the interoperability protocol.
+
+A contract may enter and leave the visibility of a Participant Node several times.
+For example, suppose that the painter submits the following commands and their commits end up on the given ledgers.
+
+#. Create a contract `c` with signatories Alice and the painter on Ledger 2
+#. Exercise a non-consuming choice `ch1` on `c` on Ledger 1.
+#. Exercise a non-consuming choice `ch2` on `c` on Ledger 2.
+#. Exercise a consuming choice `ch3` on `c` on Ledger 1.
+
+Then, the transaction tree stream that `P2` provides for `A` contains five actions involving contract `c`: **Enter**, non-consuming **Exercise**, **Leave**, **Enter**, consuming **Exercise**.
+Importantly, `P2` must not omit the **Leave** action and the subsequent **Enter**, even though they seem to cancel out.
+This is because their presence indicates that `P2`\ 's event stream for Alice may miss some events in between; in this example, exercising the choice `ch2`.
+
+The flat transaction stream by `P2` omits the non-consuming exercise choices.
+It nevertheless contains the three actions **Enter**, **Leave**, **Enter** before the consuming **Exercise**.
+This is because the Participant Node cannot know at the **Leave** action that there will be another **Enter** action coming.
+
+In contrast, `P1` need not output the **Enter** and **Leave** actions at all in this example because `P1` hosts Alice on both ledgers.
+
+.. _cross-ledger-transaction:
+
+Cross-ledger transactions
+=========================
+
+With interoperability, a cross-ledger transaction can be committed on several interoperable DAML ledgers simultaneously.
+Such a cross-ledger transaction avoids some of the synchronization overhead of **Enter** and **Leave** actions.
+When a cross-ledger transaction uses contracts from several DAML ledgers,
+stakeholders may witness actions on their contracts that are actually not visible on the Participant Node.
+
+For example, suppose that the :ref:`split paint counteroffer workflow <split-counteroffer-ledger>` from the causality examples is committed as follows:
+The actions on `CounterOffer` and `PaintAgree` contracts are committed on Ledger 1.
+All actions on `Iou`\ s are committed on Ledger 2, assuming that some Participant Node hosts the Bank on Ledger 2.
+The last transaction is a cross-ledger transaction because the archival of the `CounterOffer` and the creation of the `PaintAgree`\ ment commits on Ledger 1 simultaneously with the transfer of Alice's `Iou` to the painter on Ledger 2.
+
+For the last transaction, Participant Node 1 notifies Alice of the transaction tree, the two archivals and the `PaintAgree` creation via the Transaction Service as usual.
+Participant Node 2 also output's the whole transaction tree on Alice's transaction tree stream, which contains the consuming **Exercise** of Alice's `Iou`.
+However, it has not output the **Create** of Alice's `Iou` because `Iou` actions commit on Ledger 2, on which Participant Node 2 does not host Alice.
+So Alice merely *witnesses* the archival even though she is an :ref:`informee <def-informee>` of the exercise.
+The **Exercise** action is therefore marked as merely being witnessed on Participant Node 2's transaction tree stream.
+
+In general, an action is marked as **merely being witnessed** when a party is an informee of the action, but the action is not committed on a ledger on which the Participant Node hosts the party.
+Unlike **Enter** and **Leave**, such witnessed actions do not affect causality from the participant's point of view and therefore provide weaker ordering guarantees.
+Such witnessed actions show up neither in the flat transaction stream nor in the Active Contracts Service.
+
+For example, suppose that the **Create** `PaintAgree` action commits on Ledger 2 instead of Ledger 1, i.e., only the `CounterOffer` actions commit on Ledger 1.
+Then, Participant Node 2 marks the **Create** `PaintAgree` action also as merely being witnessed on the transaction tree stream.
+Accordingly, it does not report the contract as active nor can Alice use the contract in her submissions via Participant Node 2.
+
+.. _interop-causality-graph:
+
+Multi-ledger causality graphs
+*****************************
+
+This section generalizes :ref:`causality graphs <causality-graph>` to the interoperability setting.
+
+Every active DAML contract resides on at most one DAML ledger.
+Any use of a contract must be committed on the DAML ledger where it resides.
+Initially, when the contract is created, it takes up residence on the DAML ledger on which the **Create** action is committed.
+To use contracts residing on different DAML ledgers, cross-ledger transactions are committed on several DAML ledgers.
+
+However, cross-ledger transactions incur overheads and if a contract is frequently used on a DAML ledger that is not its residence, the interoperability protocol can migrate the contract to the other DAML ledger.
+The process of the contract giving up residence on the origin DAML ledger and taking up residence on the target DAML ledger is called a **contract transfer**.
+The **Enter** and **Leave** events on the transaction stream originate from such contract transfers, as will be explained below.
+Moreover, contract transfers are synchronization points between the origin and target DAML ledgers and therefore affect the ordering guarantees.
+We therefore generalize causality graphs for interoperability.
+
+Definition »Transfer action«
+  A **transfer action** on a contract `c` is written **Transfer** `c`.
+  The **informees** of the transfer actions are the stakeholders of `c`.
+
+In the following, the term *action* refers to transaction actions (**Create**, **Exercise**, **Fetch**, and **NoSuchKey**) as well as transfer actions.
+In particular, a transfer action on a contract `c` is an action on `c`.
+Transfer actions do not appear in transactions though.
+So a transaction action cannot have a transfer action as a consequence and transfer actions do not have consequences at all.
+
+Definition »Multi-Ledger causality graph«
+  A **multi-ledger causality graph** `G` for a set `Y` of DAML ledgers is a finite, transitively closed, directed acyclic graph.
+  The vertices are either transactions or transfer actions.
+  Every action is possibly annotated with an **incoming ledger** and an **outgoing ledger** from `Y` according to the following table:
+
+  +---------------+-----------------+-----------------+
+  | Action        | incoming ledger | outgoing ledger |
+  +===============+=================+=================+
+  | **Create**    | no              | yes             |
+  +---------------+-----------------+-----------------+
+  | consuming     |                 |                 |
+  | **Exercise**  | yes             | no              |
+  +---------------+-----------------+-----------------+
+  | non-consuming |                 |                 |
+  | **Exercise**  | yes             | yes             |
+  +---------------+-----------------+-----------------+
+  | **Fetch**     | yes             | yes             |
+  +---------------+-----------------+-----------------+
+  | **NoSuchKey** | no              | no              |
+  +---------------+-----------------+-----------------+
+  | **Transfer**  | maybe           | maybe           |
+  +---------------+-----------------+-----------------+
+
+  For non-consuming **Exercise** and **Fetch** actions, the incoming ledger must be the same as the outgoing ledger.
+  **Transfer** actions must have at least one of them.
+  A **transfer** action with both set represents a complete transfer.
+  If only the incoming ledger is set, it represents the partial information of an **Enter** event;
+  if only outgoing is set, it is the partial information of a **Leave** event.
+  **Transfer** actions with missing incoming or outgoing ledger annotations referred to as **Enter** or **Leave** actions, respectively.
+
+The :ref:`action order <def-action-order>` generalizes to multi-ledger causality graphs accordingly.
+
+In the :ref:`example for Enter and Leave events <enter-leave-event>` where the painter exercises three choices on contract `c` with signatories Alice and the painter, the four transactions yield the following multi-ledger causality graph.
+Incoming and outgoing ledgers are encoded as colors (green for Ledger 1 and yellow for Ledger 2).
+**Transfer** vertices are shown as circles, where the left half is colored with the incoming ledger and the right half with the outgoing ledger.
+
+.. https://app.lucidchart.com/documents/edit/ef1e60ac-fa1e-40be-b1e6-7b3197d4543b
+
+.. _interoperable-causality-graph-linear:
+   
+.. figure:: ./images/interoperable-causality-graph-linear.svg
+   :align: center
+   :width: 100%
+
+   Multi-Ledger causality graph with transfer actions
+
+.. note::
+   As for ordinary causality graphs, the diagrams for multi-ledger causality graphs omit transitive edges for readability.
+
+As an example for a cross-domain transaction, consider the :ref:`split paint counteroffer workflow with the cross-domain transaction <cross-ledger-transaction>`.
+The corresponding multi-ledger causality graph is shown below.
+The last transaction `tx4` is a cross-ledger transaction because its actions have more than one color.
+
+.. https://app.lucidchart.com/documents/edit/c3b120cf-1974-4ae8-8334-435642f94eed/
+
+.. _counteroffer-interoperable-causality-graph:
+   
+.. figure:: ./images/counteroffer-interoperable-causality-graph.svg
+   :align: center
+   :width: 100%
+
+   Multi-Ledger causality graph for the split paint counteroffer workflow on two DAML ledgers
+
+
+Consistency
+===========
+
+Definition »Ledger trace«
+  A **ledger trace** is a finite list of pairs `(a`:sub:`i`\ `, b`:sub:`i`\ `)`
+  such that `b`:sub:`i - 1` = `a`:sub:`i` for all `i` > 0.
+  Here `a`:sub:`i` and `b`:sub:`i` identify DAML ledgers or are the special value `NONE`,
+  which is different from all DAML ledger identifiers.
+
+ 
+Definition »Multi-Ledger causal consistency for a contract«
+  Let `G` be a multi-ledger causality graph and `X` be a set of actions from `G` on a contract in `c`.
+  The graph `G` is **multi-ledger consistent for the contract** `c` on `X` if all of the following hold:
+
+  #. If `X` is not empty, then `X` contains a **Create** or **Enter** action.
+     This action precedes all other actions in `X`.
+
+  #. `X` contains at most one **Create** action.
+     If so, this action precedes all other actions in `X`.
+
+  #. If `X` contains a consuming **Exercise** action `act`, then `act` follows all other actions in `X` in `G`\ 's action order.
+
+  #. All **Transfer** actions in `X` are ordered with all other actions in `X`.
+
+  #. For every maximal chain in `X` (i.e., maximal totally ordered subset of `X`), the sequence of `(`\ incoming ledger, outgoing ledger\ `)` pairs is a ledger trace, using `NONE` if the action does not have an incoming or outgoing ledger annotation.
+
+The first three conditions mimick the conditions of :ref:`causal consistency <def-causal-consistency-contract>` for ordinary causality graphs.
+They ensure that **Create** actions come first and consuming **Exercise** actions last.
+An **Enter** action takes the role of a **Create** if there is no **Create**.
+The fourth condition ensures that all transfer actions are synchronization points for a contract.
+The last condition about ledger traces ensures that contracts reside on only one DAML ledger and all usages happen on the ledger of residence.
+In particular, the next contract action after a **Leave** must be an **Enter**.
+
+For example, the above :ref:`multi-ledger causality graph with transfer actions <interoperable-causality-graph-linear>` is multi-ledger consistent for `c`.
+In particular, there is only one maximal chain in the actions on `c`, namely
+
+  **Create** `c` -> `tf1` -> **ExeN** `B` `c` `ch1` -> `tf2` -> **ExeN** `B` `c` `ch2` -> `tf3` -> **ExeN** `B` `c` `ch3`,
+
+and for each edge `act`:sub:`1` -> `act`:sub:`2`, the outgoing ledger color of `act`:sub:`1` is the same as the incoming ledger color of `act`:sub:`2`.
+The restriction to maximal chains ensures that no node is skipped.
+For example, the (non-maximal) chain
+
+  **Create** `c` -> **ExeN** `B` `c` `ch1` -> `tf2` -> **ExeN** `B` `c` `ch2` -> `tf3` -> **Exe** `B` `c` `ch3`
+
+is not a ledger trace because the outgoing ledger of the **Create** action (yellow) is not the same as the incoming ledger of the non-consuming **Exercise** action for `ch1` (green).
+Accordingly, the subgraph without the `tf1` vertex is not multi-ledger consistent for `c` even though it is a multi-ledger causality graph.
+
+Definition »Consistency for a multi-ledger causality graph«
+  Let `X` be a subset of actions in a multi-ledger causality graph `G`.
+  Then `G` is **multi-ledger consistent** for `X` (or `X`-**multi-ledger consistent**)
+  if `G` is multi-ledger consistent for all contracts `c` on the set of actions on `c` in `X`.
+  `G` is **multi-ledger consistent** if `G` is multi-ledger consistent on all the actions in `G`.
+
+.. note::
+   There is no multi-ledger consistency requirement for contract keys yet.
+   So interoperability does not provide consistency guarantees beyond those that come from the contracts they reference.
+   In particular, contract keys need not be unique and **NoSuchKey** actions do not check that the contract key is unassigned.
+
+The :ref:`multi-ledger causality graph for the split paint counteroffer workflow <counteroffer-interoperable-causality-graph>` is multi-ledger consistent.
+In particular all maximal chains of actions on a contract are ledger traces:
+
++-------------------------+-----------------------------------------+
+| contract                | maximal chains                          |
++=========================+=========================================+
+| `Iou Bank A`            | **Create** -> **Fetch** -> **Exercise** |
++-------------------------+-----------------------------------------+
+| `ShowIou A P Bank`      | **Create** -> **Exercise**              |
++-------------------------+-----------------------------------------+
+| `Counteroffer A P Bank` | **Create** -> **Exercise**              |
++-------------------------+-----------------------------------------+
+| `Iou Bank P`            | **Create**                              |
++-------------------------+-----------------------------------------+
+| `PaintAgree P A`        | **Create**                              |
++-------------------------+-----------------------------------------+
+   
+Minimality and reduction
+========================
+
+When edges are added to an `X`-multi-ledger consistent causality graph such that it remains acyclic and transitively closed,
+the resulting graph is again `X`-multi-ledger consistent.
+The notions :ref:`minimally consistent <minimal-consistent-causality-graph>` and :ref:`reduction <def-reduction-causality-graph>` therefore generalize from ordinary causality graphs accordingly.
+
+Definition »Minimal multi-ledger-consistent causality graph«
+  An `X`-multi-ledger consistent causality graph `G` is `X`\ -**minimal** if no strict subgraph of `G` (same vertices, fewer edges) is an `X`-multi-ledger consistent causality graph.
+  If `X` is the set of all actions in `G`, then `X` is omitted.
+
+Definition »Reduction of a multi-ledger consistent causality graph«
+  For an `X`\ -multi-ledger consistent causality graph `G`, there exists a unique minimal `X`\ -multi-ledger consistent causality graph `reduce`:sub:`X`\ `(G)` with the same vertices and the edges being a subset of `G`.
+  `reduce`:sub:`X`\ `(G)` is called the `X`\ -**reduction** of `G`.
+  As before, `X` is omitted if it contains all actions in `G`.
+
+Since multi-ledger causality graphs are acyclic, their vertices can be sorted topologically and the resulting list is again a causality graph, where every vertex has an outgoing edge to all later vertices.
+If the original causality graph is `X`\ -consistent, then so is the topological sort, as topological sorting merely adds edges.
+
+
+From multi-ledger causality graphs to ledgers
+=============================================
+
+Multi-Ledger causality graphs `G` are linked to ledgers `L` in the DAML Ledger Model via topological sort and reduction.
+
+* Given a multi-ledger causality graph `G`,
+  drop the incoming and outgoing ledger annotations and all transfer vertices,
+  topologically sort the transaction vertices,
+  and extend the resulting list of transactions with the requesters to obtain a sequence of commits `L`.
+
+* Given a sequence of commits `L`,
+  use the transactions as vertices and add an edge from `tx1` to `tx2` whenever `tx1`\ 's commit precedes `tx2`\ 's commit in the sequence.
+  Then add transfer vertices and incoming and outgoing ledger annotations as needed and connect them with edges to the transaction vertices.
+
+This link preserves consistency only to some extent.
+Namely, if a multi-ledger causality graph is multi-ledger consistent for a contract `c`, then the corresponding ledger is consistent for the contract `c`, too.
+However, a multi-ledger-consistent causality graph does not yield a consistent ledger because key consistency may be violated.
+Conversely, a consistent ledger does not talk about the incoming and outgoing ledger annotations and therefore cannot enforce that the annotations are consistent.
+
+.. _ledger-aware-projection:
+
+Ledger-aware projection
+***********************
+
+A Participant Node maintains a local ledger for each party it hosts and the Transaction Service outputs a topological sort of this local ledger.
+When the Participant Node hosts the party on several ledgers, this local ledger is an multi-ledger causality graph.
+This section defines the ledger-aware projection of an multi-ledger causality graph, which yields such a local ledger.
+
+Definition »Y-labelled action«
+  An action with incoming and outgoing ledger annotations is **Y-labelled** for a set `Y`
+  if its incoming or outgoing ledger annotation is an element of `Y`.
+
+Definition »Ledger-aware projection for transactions«
+  Let `Y` be a set of DAML ledgers and `tx` a transaction whose actions are annotated with incoming and outgoing ledgers.
+  Let `Act` be the set of `Y`\ -labelled subactions of `tx` that the party `P` is an informee of.
+  The **ledger-aware projection** of `tx` for `P` on `Y` (`P`-**projection on** `Y`) consists of all the maximal elements of `Act` (w.r.t. the subaction relation) in execution order.
+
+.. note::
+   Every action contains all its subactions.
+   So if `act` is included in the `P`\ -projection on `Y` of `tx`,
+   then all subactions of `act` are also part of the projection.
+   Such a subaction `act'` may not be `Y`\ -labelled itself though, i.e., belong to a different ledger.
+   If `P` is an informee of `act'`, the Participant Node will mark `act'` as merely being witnessed on `P`\ 's transaction stream, as explained below.
+
+The :ref:`cross-domain transaction in the split paint counteroffer workflow <counteroffer-interoperable-causality-graph>`, for example, has the following projections for Alice and the painter on the `Iou` ledger (yellow) and the painting ledger (green).
+Here, the projections on the green ledger include the actions of the yellow ledger because a projection includes the subactions.
+
+.. https://www.lucidchart.com/documents/edit/f8ec5741-7a37-4cf5-92a9-bf7b3132ba8e
+.. image:: ./images/projecting-transactions-paint-offer-ledger-aware.svg
+   :align: center
+   :width: 60%
+
+Definition »Projection for transfer actions«
+  Let `act` be a transfer action annotated with an incoming ledger and/or an outgoing ledger.
+  The **projection** of `act` on a set of ledgers `Y`
+  removes the annotations from `act` that are not in `Y`.
+  If the projection removes all annotations, it is empty.
+
+  The **projection** of `act` to a party `P` on `Y` (`P`\ -**projection** on `Y`)
+  is the projection of `act` on `Y` if `P` is a stakeholder of the contract, and empty otherwise.
+
+Definition »Multi-Ledger consistency for a party«
+  An multi-ledger causality graph `G` is **consistent for a party** `P` on a set of ledgers `Y` (`P`\ -**consistent** on `Y`)
+  if `G` is multi-ledger consistent on the set of `Y`\ -labelled actions in `G` of which `P` is an informee.
+
+The notions of `X`-minimality and `X`-reduction extend to a party `P` on a set `Y` of ledgers accordingly.
+
+Definition »Ledger-aware projection for multi-ledger causality graphs«
+  Let `G` be a multi-ledger consistent causality graph and `Y` be a set of DAML ledgers.
+  The **projection** of `G` to party `P` on `Y` (`P`\ -**projection** on `Y`) is the `P`\ -reduction on `Y` of the following causality graph `G'`, which is `P`\ -consistent on `Y`:
+
+  * The vertices of `G'` are the vertices of `G` projected to `P` on `Y`, excluding empty projections.
+
+  * There is an edge between two vertices `v`:sub:`1` and `v`:sub:`2` in `G'` if there is an edge from the `G`\ -vertex corresponding to `v`:sub:`1` to the `G`\ -vertex corresponding to `v`:sub:`2`.
+
+If `G` is a multi-ledger consistent causality graph, then the `P`\ -projection on `Y` is `P`\ -consistent on `Y`, too.
+
+For example, the :ref:`multi-ledger causality graph for the split paint counteroffer workflow <counteroffer-interoperable-causality-graph>` is projected as follows.
+
+.. https://app.lucidchart.com/documents/edit/d788b464-d670-4029-b2c0-d537c023052f
+   
+.. image:: ./images/counteroffer-causality-ledgeraware-projection.svg
+   :align: center
+   :width: 100%
+
+The following points are worth highlighting:
+
+* In Alice's projection on the green ledger, Alice witnesses the archival of her `Iou`.
+  As explained in the :ref:`interop-ordering-guarantees` below,
+  the **Exercise** action is marked as merely being witnessed
+  in the transaction stream of a Participant Node that hosts Alice on the green ledger but not on the yellow ledger.
+  Similarly, the Painter merely witnesses the **Create** of his `Iou` in the Painter's projection on the green ledger.
+
+* In the Painter's projections, the `ShowIou` transaction `tx3` is unordered w.r.t. to the `CounterOffer` acceptance in `tx4`
+  like in the :ref:`case of ordinary causality graphs <counteroffer-causality-projections>`.
+  The edge `tx3` -> `tx4` is removed by the reduction step during projection.
+
+The projection of transfer actions can be illustrated with the :ref:`interoperable-causality-graph-linear`.
+The `A`-projections on the yellow and green ledger look as follows.
+The white color indicates that a transfer action has no incoming or outgoing ledger annotation.
+That is, a **Leave** action is white on the right hand side and an **Enter** action is white on the left hand side.
+
+.. https://app.lucidchart.com/documents/edit/edbf9aaf-b7da-4e68-b9c9-9e631c3a87bb
+
+.. image:: ./images/transfer-projection.svg
+   :align: center
+   :width: 100%
+
+.. _interop-ordering-guarantees:
+
+Ledger API ordering guarantees
+******************************
+
+The Transaction Service and the Active Contract Service are derived from the local ledger that the Participant Node maintains for the party.
+Let `Y` be the set of ledgers on which the Participant Node hosts a party.
+The transaction tree stream outputs a topological sort of the party's local ledger on `Y`, with the following modifications:
+
+#. **Transfer** actions with either an incoming or an outgoing ledger annotation are output as **Enter** and **Leave** events.
+   **Transfer** actions with both incoming and outgoing ledger annotations are omitted.
+
+#. The incoming and outgoing ledger annotations are not output.
+   Transaction actions with an incoming or outgoing ledger annotation
+   that is not in `Y` are marked as merely being witnessed if the
+   party is an informee of the action.
+
+#. **Fetch** nodes and **NoSuchKey** are omitted.
+
+The flat transaction stream contains precisely the ``CreatedEvent``\ s, ``ArchivedEvent``\ s, and the **Enter** and **Leave** actions that correspond to **Create**, consuming **Exercise**, **Enter** and **Leave** actions in transaction trees on the transaction tree stream where the party is a stakeholder of the affected contract and that are not marked as merely being witnessed.
+
+Similarly, the active contract service provides the set of contracts that are active at the returned offset according to the flat transaction stream.
+That is, the contract state changes of all events from the transaction event stream are taken into account in the provided set of contracts.
+
+The :ref:`ordering guarantees <ordering-guarantees>` for single DAML ledgers extend accordingly.
+In particular, interoperability ensures that all local ledgers are projections of a virtual shared multi-ledger causality graph that connects to the DAML Ledger Model as described above.
+The ledger validity guarantees therefore extend via the local ledgers to the Ledger API.

docs/source/concepts/ledger-model/ledger-integrity.rst

@@ -194,6 +194,7 @@ It grants `P` the choice to perform such an assertion, which is needed for :ref:
 
 Key consistency extends to actions, transactions and lists of transactions just like the other consistency notions.
 
+.. _da-model-ledger-consistency:
 
 Ledger consistency
 ``````````````````
@@ -267,7 +268,7 @@ Definition »input key«
 In the :ref:`blacklisting example <paint-offer-blacklist>`, `P`\ 's transaction has two input keys: `(U, A)` due to the **NoSuchKey** action and `(P, P123)` as it creates a `PaintOffer` contract.
 
 
-.. _`da-model-conformance`:
+.. _da-model-conformance:
 
 Conformance
 +++++++++++

docs/source/concepts/ledger-model/ledger-privacy.rst

@@ -243,6 +243,7 @@ the painter:
 .. image:: ./images/divulgence-for-disclosure-counteroffer.svg
    :align: center
    :width: 100%
+   :name: da-paint-counteroffer-example
 
 In the example, the context is provided by consuming a `ShowIou` contract on which the painter is a stakeholder.
 This now requires an additional contract type, compared to the original paint offer example.

docs/source/concepts/ledger-model/ledger-structure.rst

@@ -1,6 +1,8 @@
 .. Copyright (c) 2020 Digital Asset (Switzerland) GmbH and/or its affiliates. All rights reserved.
 .. SPDX-License-Identifier: Apache-2.0
 
+.. _ledger-structure:
+
 Structure
 ---------
 

docs/source/concepts/local-ledger.rst

@@ -0,0 +1,454 @@
+.. Copyright (c) 2020 Digital Asset (Switzerland) GmbH and/or its affiliates. All rights reserved.
+.. SPDX-License-Identifier: Apache-2.0
+
+.. _local-ledger:
+
+Causality and Local Ledgers
+###########################
+
+DAML ledgers do not totally order all transactions.
+So different parties may observe two transactions on different Participant Nodes in different orders via the :ref:`Ledger API <ledger-api-services>`.
+Moreover, different Participant Nodes may output two transactions for the same party in different orders.
+This document explains the ordering guarantees that DAML ledgers do provide, by :ref:`example <causality-examples>` and formally via the concept of :ref:`causality graphs <causality-graph>` and :ref:`local ledgers <local-ledger-structure>`.
+
+The presentation assumes that you are familiar with the following concepts:
+
+* The :ref:`Ledger API <ledger-api-services>`
+
+* The :ref:`DAML Ledger Model <da-ledgers>`
+
+.. _causality-examples:
+
+Causality examples
+******************
+
+A DAML Ledger need not totally order all transaction, unlike ledgers in the DAML Ledger Model.
+The following examples illustrate these ordering guarantees of the Ledger API.
+They are based the paint counteroffer workflow from the DAML Ledger Model's :ref:`privacy section <da-model-privacy>`,
+ignoring the total ordering coming from the DAML Ledger Model.
+Recall that :ref:`the party projections <da-paint-counteroffer-example>` are as follows.
+
+.. https://www.lucidchart.com/documents/edit/c4df0455-13ab-415f-b457-f5654c2684be
+.. image:: ./ledger-model/images/divulgence-for-disclosure-counteroffer.svg
+   :align: center
+   :width: 100%
+
+
+.. _causality-example-create-archive:
+
+Stakeholders of a contract see creation and archival in the same order.
+=======================================================================
+
+Every DAML Ledger orders the creation of the `CounterOffer A P Bank` before the painter exercising the consuming choice on the `CounterOffer`.
+(If the **Create** was ordered after the **Exercise**, the resulting shared ledger would be inconsistent, which violates the validity guarantee of DAML ledgers.)
+Accordingly, Alice will see the creation before the archival on her transaction stream and so will the painter.
+This does not depend on whether they are hosted on the same Participant Node.
+
+.. _causality-example-create-use-archive:
+
+Signatories of a contract and stakeholder actors see usages after the creation and before the archival.
+=======================================================================================================
+
+The `Fetch A (Iou Bank A)` action comes after the creation of the `Iou Bank A` and before its archival,
+for both Alice and the Bank,
+because the Bank is a signatory of the `Iou Bank A` contract and Alice is a stakeholder of the `Iou Bank A` contract and an actor on the **Fetch** action.
+
+.. _causality-example-commit-atomic:
+
+Commits are atomic.
+===================
+
+Alice sees the **Create** of her `Iou` before the creation of the `CounterOffer`,
+because the `CounterOffer` is created in the same commit as the **Fetch** of the `Iou`
+and the **Fetch** commit comes after the **Create** of the `Iou`.
+
+.. _causality-example-non-consuming:
+
+Non-consuming usages in different commits may appear in different orders.
+=========================================================================
+
+Suppose that the Bank exercises a non-consuming choice on the `Iou Bank A` without consequences while Alice creates the `CounterOffer`.
+In the ledger shown below, the Bank's commit comes before Alice's commit.
+   
+.. https://app.lucidchart.com/documents/edit/1923969f-7bf2-45e0-a68d-6a0b2d308883/0_0
+   
+.. image:: ./images/counteroffer-double-fetch.svg
+   :align: center
+   :width: 100%
+
+The Bank's projection contains the nonconsuming **Exercise** and the **Fetch** action on the `Iou`.
+Yet, the **Fetch** may come before the non-consuming **Exercise** in the Bank's transaction tree stream.
+
+.. _causality-example-out-of-band:
+
+Out-of-band causality is not respected.
+=======================================
+
+The following examples assume that Alice splits up her commit into two as follows:
+
+.. https://www.lucidchart.com/documents/edit/05be08a6-7374-41f0-8b96-31276d2c5349/
+
+.. _split-counteroffer-ledger:
+   
+.. figure:: ./images/counteroffer-split-commit.svg
+   :align: center
+   :width: 100%
+
+   Counteroffer workflow with four commits.
+   
+Alice can specify in the `CounterOffer` the `Iou` that she wants to pay the painter with.
+In a deployed implementation, Alice's application first observes the created `Iou` contract via the transaction service or active contract service before she requests to create the `CounterOffer`.
+Such application logic does not induce an ordering between commits.
+So the creation of the `CounterOffer` need not come after the creation of the `Iou`.
+
+If Alice is hosted on several Participant Nodes, the Participant Nodes can therefore output the two creations in either order.
+   
+The rationale for this behaviour is that Alice could have learnt about the contract ID out of band or made it up.
+The Participant Nodes therefore cannot know whether there will ever be a **Create** event for the contract.
+So if Participant Nodes delayed outputting the **Create** action for the `CounterOffer` until a **Create** event for the `Iou` contract was published,
+this delay might last forever and liveness is lost.
+DAML ledgers therefore do not capture data flow through applications.
+
+.. _causality-divulgence-example:
+
+Divulged actions do not induce order.
+=====================================
+
+The painter witnesses the fetching of Alice's `Iou` when the `ShowIou` contract is consumed.
+The painter also witnesses the **Exercise** of the `Iou` when Alice exercises the transfer choice as a consequence of the painter accepting the `CounterOffer`.
+However, as the painter is not a stakeholder of Alice's `Iou` contract, he may observe Alice's `ShowIou` commit after the archival of the `Iou` as part of accepting the `CounterOffer`.
+
+In practice, this can happen in a setup where two Participant Nodes `N`:sub:`1` and `N`:sub:`2` host the painter.
+He sees the divulged `Iou` and the created `CounterOffer` through `N`:sub:`1`\ 's transaction tree stream
+and then submits the acceptance through `N`:sub:`1`.
+Like in the previous example, `N`:sub:`2` does not know about the dependence of the two commits.
+Accordingly, `N`:sub:`2` may output the accepting transaction *before* the `ShowIou` contract on the transaction stream.
+      
+Even though this may seem unexpected, it is in line with stakeholder-based ledgers:
+Since the painter is not a stakeholder of the `Iou` contract, he should not care about the archivals or creates of the contract.
+In fact, the divulged `Iou` contract shows up neither in the painter's active contract service nor in the flat transaction stream.
+Such witnessed events are included in the transaction tree stream as a convenience:
+They relieve the painter from computing the consequences of the choice and enable him to check that the action conforms to the DAML model.
+
+Similarly, being an actor of an **Exercise** action induces order with respect to other uses of the contract only if the actor is a contract stakeholder.
+This is because non-stakeholder actors of an **Exercise** action merely authorize the action, but they do not track whether the contract is active; this is what signatories and observers are for.
+
+.. _causality-example-depend-on-party:
+
+The ordering guarantees depend on the party.
+============================================
+
+By the previous example, for the painter, fetching the `Iou` is not ordered before transferring the `Iou`.
+For Alice, however, the **Fetch** must appear before the **Exercise** 
+because Alice is a stakeholder on the `Iou` contract.
+This shows that the ordering guarantees depend on the party.
+
+
+.. _causality-graph:
+   
+Causality graphs
+****************
+
+The above examples indicate that DAML ledgers order transactions only partially.
+DAML ledgers can be represented as finite directed acyclic graphs (DAG) of transactions.
+
+.. _def-causality-graph:
+
+Definition »causality graph«
+  A **causality graph** is a finite directed acyclic graph `G` of transactions that is transitively closed.
+  Transitively closed means that whenever `v`:sub:`1` -> `v`:sub:`2` and `v`:sub:`2` -> `v`:sub:`3` are edges in `G`,
+  then there is also an edge `v`:sub:`1` -> `v`:sub:`3` in `G`.
+
+.. _def-action-order:
+
+Definition »action order«
+  For a causality graph `G`,
+  the induced **action order** on the actions in the transactions combines the graph-induced order between transactions with the execution order of actions inside each transaction.
+  It is the least partial order that includes the following ordering relations between two actions `act`:sub:`1` and `act`:sub:`2`:
+  
+  * `act`:sub:`1` and `act`:sub:`2` belong to the same transaction and `act`:sub:`1` precedes `act`:sub:`2` in the transaction.
+  * `act`:sub:`1` and `act`:sub:`2` belong to different transactions in vertices `tx`:sub:`1` and `tx`:sub:`2` and there is a path in `G` from `tx`:sub:`1` to `tx`:sub:`2`.
+
+    .. note::
+       Checking for an *edge* instead of a *path* in `G` from `tx`:sub:`1` to `tx`:sub:`2` is equivalent
+       because causality graphs are transitively closed.
+       The definition uses *path* because the figures below omit transitive edges for readability.
+
+The action order is a partial order on the actions in a causality graph.
+For example, the following diagram shows such a causality graph for the ledger in the above :ref:`Out-of-band causality example <causality-example-out-of-band>`.
+Each grey box represents one transaction and the graph edges are the solid arrows between the boxes.
+Diagrams omit transitive edges for readability; in this graph the edge from `tx1` to `tx4` is not shown.
+The **Create** action of Alice's `Iou` is ordered before the **Create** action of the `ShowIou` contract because there is an edge from the transaction `tx1` with the `Iou` **Create** to the transaction `tx3` with the `ShowIou` **Create**.
+Moreover, the `ShowIou` **Create** action is ordered before the **Fetch** of Alice's `Iou` because the **Create** action precedes the **Fetch** action in the transaction.
+In contrast, the **Create** actions of the `CounterOffer` and Alice's `Iou` are unordered: neither precedes the other because they belong to different transaction and there is no directed path between them.
+
+.. https://app.lucidchart.com/documents/edit/44d97c43-1bb2-4d60-ac30-6b6048b5b5f5
+
+.. _causality-graph-couteroffer-split:
+
+.. figure:: ./images/counteroffer-split-action-order.svg
+   :align: center
+   :width: 100%
+
+   Causality graph for the :ref:`counteroffer workflow with four commits <split-counteroffer-ledger>`.
+
+.. _causality-graph-consistency:
+
+Consistency
+===========
+
+Consistency ensures that a causality graph sufficiently orders all the transactions.
+It generalizes :ref:`ledger consistency <da-model-consistency>` from the DAML Ledger Model as :ref:`explained below <causality-consistency-ledger-model>`.
+
+.. _def-causal-consistency-contract:
+
+Definition »Causal consistency for a contract«
+  Let `G` be a causality graph and `X` be a set of actions on a contract `c` that belong to transactions in `G`.
+  The graph `G` is **causally consistent for the contract** `c` on `X` if all of the following hold:
+
+  * If `X` is not empty, then `X` contains exactly one **Create** action.
+    This action precedes all other actions in `X` in `G`\ 's action order.
+
+  * If `X` contains a consuming **Exercise** action `act`, then `act` follows all actions in `X` other than `act` in `G`\ 's action order.
+
+Definition »Causal consistency for a key«
+  Let `G` be a causality graph and `X` be a set of actions on a key `k` that belong to transactions in `G`.
+  The graph `G` is **causally consistent for the key** `k` on `X` if all of the following hold:
+
+  * All **Create** and consuming **Exercise** actions in `X` are totally ordered in `G`\ 's action order
+    and **Create**\ s and consuming **Exercise**\ s alternate, starting with **Create**.
+    Every consecutive **Create**\ -**Exercise** pair acts on the same contract.
+
+  * All **NoSuchKey** actions in `X` are action-ordered with respect to all **Create** and consuming **Exercise** actions in `X`.
+    No **NoSuchKey** action is action-ordered between a **Create** action and its subsequent consuming **Exercise** action in `X`.
+
+.. _def-consistency-causality-graph:
+    
+Definition »Consistency for a causality graph«
+  Let `X` be a subset of the actions in a causality graph `G`.
+  Then `G` is **consistent** on `X` (or `X`-**consistent**) if `G` is causally consistent for all contracts `c` on the set of actions on `c` in `X` and for all keys `k` on the set of actions on `k` in `X`.
+  `G` is **consistent** if `G` is consistent on all the actions in `G`.
+
+When edges are added to an `X`-consistent causality graph such that it remains acyclic and transitively closed,
+the resulting graph is again `X`-consistent.
+So it makes sense to consider minimal consistent causality graphs.
+
+.. _minimal-consistent-causality-graph:
+
+Definition »Minimal consistent causality graph«
+  An `X`-consistent causality graph `G` is `X`\ -**minimal** if no strict subgraph of `G` (same vertices, fewer edges) is an `X`-consistent causality graph.
+  If `X` is the set of all actions in `G`, then `X` is omitted.
+
+For example, the :ref:`above causality graph for the split counteroffer workflow <causality-graph-couteroffer-split>` is consistent.
+This causality graph is minimal, as the following analysis shows:
+
++----------------+--------------------------------------------------------------------------------------+
+| Edge           | Justification                                                                        |
++================+======================================================================================+
+| `tx1` -> `tx3` | Alice's `Iou` **Create** action of  must precede the **Fetch** action.               |
++----------------+--------------------------------------------------------------------------------------+
+| `tx2` -> `tx4` | The `CounterOffer` **Create** action of  must precede the **Exercise** action.       |
++----------------+--------------------------------------------------------------------------------------+
+| `tx3` -> `tx4` | The consuming **Exercise** action on Alice's `Iou` must follow the **Fetch** action. |
++----------------+--------------------------------------------------------------------------------------+
+
+We can focus on parts of the causality graph by restricting the set `X`.
+If `X` consists of the actions on `Iou` contracts, this causality graph is `X`\ -consistent.
+Yet, it is not `X`\ -minimal since the edge `tx2` -> `tx4` can be removed without violating `X`\ -consistency: the edge is required only because of the `CounterOffer` actions, which are excluded from `X`.
+The `X`\ -minimal consistent causality graph looks as follows, where the actions in `X` are highlighted in red.
+
+.. https://app.lucidchart.com/documents/edit/4aa93018-bf32-42e1-98a1-3cc1943cdd36
+
+.. _causality-counteroffer-Iou-minimal:
+   
+.. figure:: ./images/causality-counteroffer-Iou-minimal.svg
+   :align: center
+   :width: 100%
+
+   Minimal consistent causality graph for the highlighted actions.
+
+Another example of a minimal causality graph is shown below.
+At the top, the transactions `tx1` to `tx4` create an `Iou` for Alice, exercise two non-consuming choices on it, and transfer the `Iou` to the painter.
+At the bottom, `tx5` asserts that there is no key for an Account contract for the painter.
+Then, `tx6` creates an such account with balance 0 and `tx7` deposits the painter's `Iou` from `tx4` into the account, updating the balance to 1.
+
+.. https://app.lucidchart.com/documents/edit/b9d84f0f-e459-427c-86b8-c767662af326
+   
+.. image:: ./images/causality-consistency-examples.svg
+   :align: center
+   :width: 100%
+
+Unlike in a linearly ordered ledger, the causality graph relates the transactions of the `Iou` transfer workflow with the `Account` creation workflow only at the end, when the `Iou` is deposited into the account.
+As will be formalized below, the Bank, Alice, and the painter therefore need not observe the transactions `tx1` to `tx7` in the same order.
+
+Moreover, transaction `tx2` and `tx3` are unordered in this causality graph even though they act on the same `Iou` contract.
+However, as both actions are non-consuming, they do not interfere with each other and could therefore be parallelized, too.
+Alice and the Bank accordingly may observe them in different orders.
+
+The **NoSuchKey** action in `tx5` must be ordered with respect to the two Account **Create** actions in `tx6` and `tx7` and the consuming **Exercise** on the Account contract in `tx7`, by the key consistency conditions.
+For this set of transactions, consistency allows only one such order: `tx5` comes before `tx6` because `tx7` is atomic: `tx5` cannot be interleaved with `tx7`, e.g., between the consuming **Exercise** of the `Acc Bank P P 0` and the **Create** of the updated account `Acc Bank P P 1`.
+
+**NoSuchKey** actions are similar to non-consuming **Exercise**\ s and **Fetch**\ es of contracts when it comes to causal ordering: If there were another transaction `tx5'` with a **NoSuchKey** `(Acc, Bank, P)` action, then `tx5` and `tx5'` need not be ordered, just like `tx2` and `tx3` are unordered.
+
+.. _causality-consistency-ledger-model:
+
+From causality graphs to ledgers
+================================
+
+Since causality graphs are acyclic, their vertices can be sorted topologically and the resulting list is again a causality graph, where every vertex has an outgoing edge to all later vertices.
+If the original causality graph is `X`\ -consistent, then so is the topological sort, as topological sorting merely adds edges.
+For example, the transactions on the :ref:`ledger <split-counteroffer-ledger>` in the :ref:`out-of-band causality example <causality-example-out-of-band>` are a topological sort of the :ref:`corresponding causality graph <causality-graph-couteroffer-split>`.
+
+Conversely, we can reduce an `X`\ -consistent causality graph to only the causal dependencies that `X`\ -consistency imposes.
+This gives a minimal `X`\ -consistent causality graph.
+
+.. _def-reduction-causality-graph:
+
+Definition »Reduction of a consistent causality graph«
+  For an `X`\ -consistent causality graph `G`, there exists a unique minimal `X`\ -consistent causality graph `reduce`:sub:`X`\ `(G)` with the same vertices and the edges being a subset of `G`.
+  `reduce`:sub:`X`\ `(G)` is called the `X`\ -**reduction** of `G`.
+  As before, `X` is omitted if it contains all actions in `G`.
+
+The causality graph for the split `CounterOffer` workflow is minimal and therefore its own reduction.
+It is also the reduction of the topological sort, i.e., the :ref:`ledger <split-counteroffer-ledger>` in the :ref:`out-of-band causality example <causality-example-out-of-band>`.
+
+.. note::
+   The reduction `reduce`:sub:`X`\ `(G)` of an `X`\ -consistent causality graph `G` can be computed as follows:
+   
+   #. Set the vertices of `G'` to the vertices of `G`.
+   #. The causal consistency conditions for contracts and keys demand that certain pairs of actions
+      `act`:sub:`1` and `act`:sub:`2` in `X` must be action-ordered.
+      For each such pair, determine the actions' ordering in `G` and add an edge to `G'` from the earlier action's transaction to the later action's transaction.
+   #. `reduce`:sub:`X`\ `(G)` is the transitive closure of `G'`.
+
+Topological sort and reduction link causality graphs `G` to the ledgers `L` from the DAML Ledger Model.
+Topological sort transforms a causality graph `G` into a sequence of transactions; extending them with the requesters gives a sequence of commits, i.e., a ledger in the DAML Ledger Model.
+Conversely, a sequence of commits `L` yields a causality graph `G`:sub:`L` by taking the transactions as vertices and adding an edge from `tx1` to `tx2` whenever `tx1`\ 's commit precedes `tx2`\ 's commit in the sequence.
+
+There are now two consistency definitions:
+
+* :ref:`Ledger Consistency <da-model-ledger-consistency>` according to DAML Ledger Model
+
+* :ref:`Consistency of causality graph <def-consistency-causality-graph>`
+
+Fortunately, the two definitions are equivalent:
+If `G` is a consistent causality graph, then the topological sort is ledger consistent.
+Conversely, if the sequence of commits `L` is ledger consistent, `G`:sub:`L` is a consistent causality graph, and so is the reduction `reduce(G`:sub:`L`\ `)`.
+
+.. _local-ledger-structure:
+   
+Local ledgers
+*************
+
+As explained in the DAML Ledger Model, parties see only a :ref:`projection <da-model-projections>` of the shared ledger for privacy reasons.
+Like consistency, projection extends to causality graphs as follows.
+
+Definition »Causal consistency for a party«
+  A causality graph `G` is **consistent for a party** `P` (`P`-consistent) if `G` is consistent on all the actions that `P` is an informee of.
+
+The notions of `X`\ -minimality and `X`\ -reduction extend to parties accordingly.
+
+For example, the :ref:`split counteroffer causality graph without the edge tx2 -> tx4 <causality-counteroffer-Iou-minimal>` is consistent for the Bank because the Bank is an informee of exactly the highlighted actions.
+It is also minimal Bank-consistent and the Bank-reduction of the :ref:`original split counteroffer causality graph <causality-graph-couteroffer-split>`.
+  
+Definition »Projection of a consistent causality graph«
+  The **projection** `proj`:sub:`P`\ `(G)` of a consistent causality graph `G` to a party `P` is the `P`\ -reduction of the following causality graph `G'`:
+
+  * The vertices of `G'` are the vertices of `G` projected to `P`, excluding empty projections.
+
+  * There is an edge between two vertices `v`:sub:`1` and `v`:sub:`2` in `G'` if there is an edge from the `G`\ -vertex corresponding to `v`:sub:`1` to the `G`\ -vertex corresponding to `v`:sub:`2`.
+
+For the :ref:`split counteroffer causality graph <causality-graph-couteroffer-split>`, the projections to Alice, the Bank, and the painter are as follows.
+
+.. https://app.lucidchart.com/documents/edit/65a83eba-9b09-4003-b824-8e7bec50ce10
+
+.. _counteroffer-causality-projections:
+   
+.. figure:: ./images/counteroffer-causality-projection.svg
+   :align: center
+   :width: 100%
+
+   Projections of the :ref:`split counteroffer causality graph <causality-graph-couteroffer-split>`.
+
+Alice's projection is the same as the original minimal causality graph.
+The Bank sees only actions on `Iou` contracts, so the causality graph projection does not contain `tx2` any more.
+Similarly, the painter is not aware of `tx1`, where Alice's `Iou` is created.
+Moreover, there is no longer an edge from `tx3` to `tx4` in the painter's local ledger.
+This is because the edge is induced by the **Fetch** of Alice's `Iou` preceding the consuming **Exercise**.
+However, the painter is not an informee of those two actions; he merely witnesses the **Fetch** and **Exercse** actions as part of divulgence.
+Therefore no ordering is required from the painter's point of view.
+This difference explains the :ref:`divulgence causality example <causality-divulgence-example>`.
+
+.. _ordering-guarantees:
+
+Ledger API ordering guarantees
+==============================
+
+The :ref:`Transaction Service <transaction-service>` provides the updates as a stream of DAML transactions
+and the :ref:`Active Contract Service <active-contract-service>` summarizes all the updates up to a given point
+by the contracts that are active at this point.
+Conceptually, both services are derived from the local ledger that the Participant Node manages for each hosted party.
+That is, the transaction tree stream for a party is a topological sort of the party's local ledger.
+The flat transaction stream contains precisely the ``CreatedEvent``\ s and ``ArchivedEvent``\ s
+that correspond to **Create** and consuming **Exercise** actions in transaction trees on the transaction tree stream where the party is a stakeholder of the affected contract.
+
+.. note::
+   The transaction trees of the :ref:`Transaction Service <transaction-service>` omit **Fetch** and **NoSuchKey** actions
+   that are part of the transactions in the local ledger.
+   The **Fetch** and **NoSuchKey** actions are thus removed before the :ref:`Transaction Service <transaction-service>` outputs the transaction trees.
+
+Similarly, the active contract service provides the set of contracts that are active at the returned offset according to the Transaction Service streams.
+That is, the contract state changes of all events from the transaction event stream are taken into account in the provided set of contracts.
+In particular, an application can process all subsequent events from the flat transaction stream or the transaction tree stream without having to take events before the snapshot into account.
+   
+Since the topological sort of a local ledger is not unique, different Participant Nodes may pick different orders for the transaction streams of the same party.
+Similarly, the transaction streams for different parties may order common transactions differently, as the party's local ledgers impose different ordering constraints.
+Nevertheless, DAML ledgers ensure that all local ledgers are projections of a virtual shared causality graph that connects to the DAML Ledger Model as described above.
+The ledger validity guarantees therefore extend via the local ledgers to the Ledger API.
+These guarantees are subject to the deployed DAML ledger's trust assumptions.
+
+.. note::
+   The virtual shared causality graph exists only as a concept, to reason about DAML ledger guarantees.
+   A deployed DAML ledger in general does not store or even construct such a shared causality graph.
+   The Participant Nodes merely maintain the local ledgers for their parties.
+   They synchronize these local ledgers to the extent that they remain consistent.
+   That is, all the local ledgers can in theory be combined into a consistent single causality graph of which they are projections.
+
+
+Explaining the causality examples
+=================================
+
+The :ref:`causality examples <causality-examples>` can be explained in terms of causality graphs and local ledgers as follows:
+
+#. :ref:`causality-example-create-archive`
+   Causal consistency for the contract requires that the **Create** comes before the consuming **Exercise** action on the contract.
+   As all stakeholders are informees on **Create** and consuming **Exercise** actions of their contracts,
+   the stakeholder's local ledgers impose this order on the actions.
+
+#. :ref:`causality-example-create-use-archive`
+   Causal consistency for the contract requires that the **Create** comes before the non-consuming **Exercise** and **Fetch** actions of a contract and that consuming **Exercise**\ s follow them.
+   Since signatories and stakeholder actors are informees of **Create**, **Exercise**, and **Fetch** actions,
+   the stakeholder's local ledgers impose this order on the actions.
+
+#. :ref:`causality-example-commit-atomic`
+   Local ledgers are DAGs of (projected) transactions.
+   Topologically sorting such a DAG cannot interleave one transaction with another, even if the transaction consists of several top-level actions.
+
+#. :ref:`causality-example-non-consuming`
+   Causal consistency does not require ordering between non-consuming usages of a contract.
+   As there is no other action in the transaction that would prescribe an ordering,
+   the Participant Nodes can output them in any order.
+
+#. :ref:`causality-example-out-of-band`
+   Out-of-band data flow is not captured by causal consistency and therefore does not induce ordering.
+
+#. :ref:`causality-divulgence-example`
+   The painter is not an informee of the **Fetch** and **Exercise** actions on Alice's `Iou`;
+   he merely witnesses them.
+   The :ref:`painter's local ledger <counteroffer-causality-projections>` therefore does not order `tx3` before `tx4`.
+   So the painter's transaction stream can output `tx4` before `tx3`.
+
+#. :ref:`causality-example-depend-on-party`
+   Alice is an informee of the **Fetch** and **Exercise** actions on her `Iou`.
+   Unlike for the painter, :ref:`her local ledger <counteroffer-causality-projections>` does order `tx3` before `tx4`,
+   so Alice is guaranteed to observe `tx3` before `tx4` on all Participant Nodes through which she is connect to the DAML ledger.

docs/source/index.rst

@@ -84,6 +84,7 @@ DAML SDK documentation
    concepts/ledger-model/index
    concepts/identity-and-package-management
    concepts/time
+   concepts/local-ledger
 
 .. toctree::
    :titlesonly:
@@ -105,6 +106,7 @@ DAML SDK documentation
    triggers/index
    tools/visual
    tools/trigger-service
+   concepts/interoperability
 
 .. toctree::
    :titlesonly: