Rewrite ledger model integrity page #22506

andreaslochbihler-da · 2025-12-08T10:34:48Z

No description provided.

meiersi-da

Wow! That's a big whopper to review. I've made a first read-through but skipped over detailed checking of the examples.

Submitting the review now so you have the comments. Overall it looks good (as expected).

Let me know if you'd like me to do a full deep dive pass to double-check the examples in full.

sdk/docs/manually-written/overview/explanations/ledger-model/ledger-integrity.rst

meiersi-da · 2026-01-07T16:35:59Z

sdk/docs/manually-written/overview/explanations/ledger-model/ledger-integrity.rst

+Not every such projection can be expressed as a set of commands on the Ledger API, though, for two reasons.
+First, a projection may contain a Fetch node at the root, like the :ref:`projection of the DvP <da-dvp-acceptandsettle-projection>` ``AcceptAndSettle`` choice for Bank 2.
+Yet, there is no Ledger API command to fetch a contract, as there are only commands for creating and exercising contracts.
+Second, the Ledger API command language does not support feeding the result of an Exercise as an argument to a subsequent command.


We plan to change that don't we. Consider adding a comment explaining that, so that readers don't assume that this is a hard constraint.

We plan to change that don't we

I guess you're referring to the idea of constructing a submission interactively. By the letter, that's a different thing than the language of LAPI commands, where I honestly don't believe that we'll make this possible. But I get your point that we should emphasize that these restrictions are artificial and may be lifted in the future.

sdk/docs/manually-written/overview/explanations/ledger-model/ledger-integrity.rst

andreaslochbihler-da · 2026-01-08T16:14:58Z

Submitting the review now so you have the comments. Overall it looks good (as expected).

Thanks for the quick review.

Let me know if you'd like me to do a full deep dive pass to double-check the examples in full.

Yes please. Also, could you comment on whether the overall structure makes sense? Should this page be split up into multiple ones? I'm a bit worried that with the examples coming first, the reader cannot actually follow the arguments why some validity condition is violated given that those conditions have not yet been defined. And conversely, when the examples are discussed in detail later in the text, I wonder whether the reader has to keep scrolling up and down and whether it's always clear what example is being discussed where. Do you have any suggestions in this regard?

roger-bosman-da

I've not been able to render this as part of the full docs-website, so I have been using the ./ci/live-docs-preview.sh script of this repo.

In general, I appreciate the difficulty of broadcasting the formal information without overloading the reader. If we would be writing for a PL conference we could be a lot more efficient/precise by using notation, but that won't fly here, at least not without accompanying clarifications. I've made some individual comments that I think are improvements.

Here I will write my thoughts, but these are not necessarily suggestions, just thoughts.

Typically, I think I would introduce properties like this as follows.

Describe them on a high, but imprecise level ("a X that is consistent does not contain any Y")
Give context
Mathematical/precise definition

For all, I'm not really sure what the description in the first section is doing. "The parties who may request a particular change are restricted" to me reads more as a consequence of the property rather than the property itself. If the intent is to give an informal version of the properties (that would be item (0) in the above order), I would extend each section with the formal high-level description (item (1) above). If the descriptions in the first section are already intended to represent step item (1) above, I think they can be made more formal. In particular, they should be about the thing they are about, no? A thing that is X should be/have/adhere to/...?

Second, whilst reading, I found that only consistency has a nice precise definition (item (3)). However, I don't think we ever get to a full definition of consistency? Just the sub-definitions. If we were writing a paper, I would give a range of consistency definitions, split on argument type, ordered in terms of usage (e.g. "Consistency (action)", "Consistency (transaction)", "Consistency (ledger)" etc.

For conformance, I appreciate that this property is a bit more vague and does not have a nice mathematical definition (right?). That being said, I wonder if we can make it more formal by defining some things separately. For example, could we define what it means for a model to contain an action? Would this definition be helped by being split by target (e.g. "Conformance (transaction)", "Conformance (ledger)")? I doubt it.

For authorization AFAIC there is some recursive property in the sense that if you authorize some root action you also authorize its children (right?). This aspect right now does not really come out of the description, and would probably become quite clear with a bit more formality. However, this is not a PL paper, so I have no idea if this is to be desired or not.

sdk/docs/manually-written/overview/explanations/ledger-model/ledger-integrity.rst

roger-bosman-da · 2026-01-08T15:28:43Z

sdk/docs/manually-written/overview/explanations/ledger-model/ledger-integrity.rst

-   :align: center
-   :alt: Described in the caption.
+Later sections add further validity conditions as they increase the expressivity of the ledger model.
+Intuitively, the :ref:`running example of the DvP workflow <da-dvp-ledger>` should be and actually is valid.


What does this mean?

Rephrased. Can you take another look whether it's clearer now?

sdk/docs/manually-written/overview/explanations/ledger-model/ledger-integrity.rst

roger-bosman-da · 2026-01-08T15:58:02Z

sdk/docs/manually-written/overview/explanations/ledger-model/ledger-integrity.rst

 ====================

-Contract consistency ensures that contracts are used after they have been created and before they are consumed.
+Internal consistency ensures that if several nodes act on a contract within an action, transaction, or ledger,


It is not fully clear to me what differentiates internal consistency from the (overall) consistency properties, other than the internal one seems a mathematical definition, and the other more vague. I think this section best contrasts the two, even if only briefly

I've reshuffled some sentences and added another example to highlight the difference maybe a bit better.

I don't follow your statement about vagueness though. To me, internal consistency and consistency are both equally formal. Can you elaborate where the definition of consistency is "vague"?

roger-bosman-da · 2026-01-08T16:05:13Z

sdk/docs/manually-written/overview/explanations/ledger-model/ledger-integrity.rst

+For example, Alice's :ref:`projection of the DvP workflow <da-dvp-ledger-projections>` is not consistent
+because it lacks ``TX 1`` and therefore the creation of contract #2 used in ``TX 3``.
+
+Fortunately, consistency behaves well under projections if we look only at contracts the parties are stakeholders of.


What I would have expected here is something along the lines of "since every contract has at least one stakeholder, we can be sure that if every party concludes consistency on the contracts they are stakeholder of, we can be sure the entire ledger is consistent" or something like that

I've added a small subsection to "validity" that discusses why we're looking at both directions of projection (preservation and reflection). Hopefully that's enough of a signpost for the readers.

roger-bosman-da · 2026-01-08T16:06:58Z

sdk/docs/manually-written/overview/explanations/ledger-model/ledger-integrity.rst

+The :ref:`causality section <local-ledger>` relaxes the ordering requirement, but makes sure
+that projections continue to preserve (internal) consistency for the parties' contracts.
+
+From Canton's perspective, the dual property is at least as important:


Ah, I guess here is the "since every contract has at least one stakeholder, we can be sure that if every party concludes consistency on the contracts they are stakeholder of, we can be sure the entire ledger is consistent"

Indeed. Interactiion with projection usualy goes both ways: identifying the conditions for preservationand for the reflection. Would you say that we should first look at reflection and only later at preservation?

roger-bosman-da · 2026-01-08T16:10:47Z

sdk/docs/manually-written/overview/explanations/ledger-model/ledger-integrity.rst

-Key Consistency
-===============
+With signatories instead of stakeholders, this problem does not appear:
+A signatory is an informee of all nodes on the contract and therefore any node relevant for consistency for the contract is present in the signatory's projection.


So if I understand correctly, this section is essentially describing what situation we need to have to, from canton's side, be able to conclude consistency. So that begs the question: does this situation always occur, and if not, what happens if we cannot conclude consistency? I guess for the ledger we know that if we have all parties we must also have all stakeholders and therefore are never in the situation that we cannot determine consistency? And for transactions, perhaps it doesn't matter to not always be able to? This can be interpreted as either my confusion or as a suggestion for improvement

As discussed offline, Canton does not provide global consistency. The section of the VGL actually already explained this. I'll leave it as is for now and see whether I find some more time in the future to discuss this in more detail.

meiersi-da

@andreaslochbihler-da : here you go. I've done a full review pass over the preview of the ledger-integrity.rst page. I have not looked at any of the other .rst files though. Let me know if I should do so too.

sdk/docs/manually-written/overview/explanations/ledger-model/ledger-integrity.rst

meiersi-da · 2026-01-12T15:08:59Z

sdk/docs/manually-written/overview/explanations/ledger-model/ledger-integrity.rst

+The restriction to a set of parties `P` comes from privacy.
+As discussed above, consistency and well-authorization are not common knowledge.
+The Canton protocol therefore relies on the relevant parties to check these conditions.
+Accordingly, the protocol only ensures these properties for the parties that follow the protocol.


Add another reference to the DvP example to illustrate a non-trivial valid ledger

Added. It also serves as an example of why the ledger materializes nowhere as a whole.

sdk/docs/manually-written/overview/explanations/ledger-model/ledger-integrity.rst

andreaslochbihler-da · 2026-01-15T13:18:12Z

@roger-bosman-da Thanks for the detailed feedback.

In general, I appreciate the difficulty of broadcasting the formal information without overloading the reader. If we would be writing for a PL conference we could be a lot more efficient/precise by using notation, but that won't fly here, at least not without accompanying clarifications.

Correct. A scientific paper would need a lot more mathematical notation.

For all, I'm not really sure what the description in the first section is doing. "The parties who may request a particular change are restricted" to me reads more as a consequence of the property rather than the property itself. If the intent is to give an informal version of the properties (that would be item (0) in the above order), I would extend each section with the formal high-level description (item (1) above). If the descriptions in the first section are already intended to represent step item (1) above, I think they can be made more formal. In particular, they should be about the thing they are about, no? A thing that is X should be/have/adhere to/...?

I see what you mean. I've tried to rephrase the conditions more explicitly in terms of the Ledger they're about.

Second, whilst reading, I found that only consistency has a nice precise definition (item (3)). However, I don't think we ever get to a full definition of consistency?

We do. Contract consistency is the full definition.

If we were writing a paper, I would give a range of consistency definitions, split on argument type, ordered in terms of usage (e.g. "Consistency (action)", "Consistency (transaction)", "Consistency (ledger)" etc.

So you're saying that I should copy the box contract consistency three times, once for actions, once for transactions and once for the ledger?

For conformance, I appreciate that this property is a bit more vague and does not have a nice mathematical definition (right?). That being said, I wonder if we can make it more formal by defining some things separately. For example, could we define what it means for a model to contain an action?

Well, that's the abstraction layer that these definitions build on. I've added a sentence to hopefully make this clearer.

For authorization AFAIC there is some recursive property in the sense that if you authorize some root action you also authorize its children (right?).

Somewhat. The controllers of a choice authorize the direct consequences of the choice. But they do not authorize the consequences of the direct consequences. So it's not really recursive. Of course, if they happen to be controllers of a direct consequence, the authorization flow continues.

andreaslochbihler-da · 2026-01-16T09:05:51Z

@andreaslochbihler-da : here you go. I've done a full review pass over the preview of the ledger-integrity.rst page. I have not looked at any of the other .rst files though. Let me know if I should do so too.

Thank you for the extensive feedback. I think it's fine to not look at the other rst files at the moment; the changes there are cosmetic.

andreaslochbihler-da added 11 commits December 4, 2025 10:56

update integrity examples

ac493df

define execution order

caa0976

rework consistency section of ledger model

fdef38f

rewrite conformance section

45d28c4

first draft of authorization

6cd09c6

Merge branch 'main' into ledger-model-integrity

c6685be

finish authorization section

83a4e3a

remove obsolete diagrams

053f139

synchronize docs

c4f60dc

update snippet markers

cdfc36b

fix label

eb998ba

andreaslochbihler-da marked this pull request as ready for review January 7, 2026 13:57

andreaslochbihler-da requested review from cristina-da and meiersi-da January 7, 2026 14:04

meiersi-da reviewed Jan 7, 2026

View reviewed changes

address Simon's comments

3f64a76

roger-bosman-da reviewed Jan 9, 2026

View reviewed changes

meiersi-da reviewed Jan 12, 2026

View reviewed changes

andreaslochbihler-da added 2 commits January 15, 2026 14:19

address Roger's comments

e155219

address Simon's second round of feedback

834476b

Rewrite ledger model integrity page #22506

Are you sure you want to change the base?

Rewrite ledger model integrity page #22506

Uh oh!

Conversation

andreaslochbihler-da commented Dec 8, 2025

Uh oh!

meiersi-da left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

andreaslochbihler-da commented Jan 8, 2026

Uh oh!

roger-bosman-da left a comment • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

meiersi-da left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

andreaslochbihler-da commented Jan 15, 2026

Uh oh!

andreaslochbihler-da commented Jan 16, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

roger-bosman-da left a comment •

edited

Loading