[Dijkstra] CIP-159-11b: Prove UTxO and UTxOW preservation of value (#1186) by williamdemeo · Pull Request #1189 · IntersectMBO/formal-ledger-specifications

williamdemeo · 2026-05-07T20:03:45Z

Description

Closes #1186. Base: master. First PR of the Dijkstra PoV stack (#1189, #1210, #1278).

Proves the UTxO-side value-accounting facts and rewires LEDGER-PoV to import them, deleting eight module parameters and adding the two batch-threading hypotheses.

What lands

Utxo.Properties.Base: the balance algebra (balance-∪, split-balance, outs-disjoint, newTxid⇒disj).
Utxo.Properties.PoV: the batch-balance coin projection and the mechanical state-change lemmas.
Utxow.Properties.PoV: the UTXOW⇒UTXO/SUBUTXOW⇒SUBUTXO extractors and the UTXOW-PoV/SUBUTXOW-PoV modules whose statements match the LEDGER-PoV parameters verbatim.
Ledger.Properties.PoV rewiring: utxow-pov-invalid, UTXOW-V-mechanical, UTXOW-batch-balance-coin and subutxow-step-coin are now imported instead of assumed; the unused balance-∪, split-balance, outs-disjoint and noMintTx parameters are dropped; noMintingSubTxs has a single home in Utxo.Properties.PoV.
Property catalog: dijkstra-utxo-pov and dijkstra-utxow-pov derive as proved.

Key points for review

subutxow-step-coin is proved conditionally on two batch-threading hypotheses (subtx-fresh-txid, subtx-spend-agree); they surface as new LEDGER-PoV parameters in the same family as utxo₁-tx-spend-eq/fresh-top-tx-id ([Dijkstra] Batch-threading UTxO invariants for LEDGER-pov #1274).
The batch balance is stated in the spec's closed form: cert deposits as refundCertDeposits/newCertDeposits over allDCerts tx against the pre-batch pool set, and gov deposits on the produced side.
Deliberately no UTXO-pov theorem: LEDGER-pov does not consume one, and none is provable at this level (see [Dijkstra] UTxO and UTxOW PoV #1186).
No CHANGELOG entry: property modules and parameter cleanup only, no semantic spec change.

Verification

The rewired Ledger.Properties.PoV typechecks with the parameters deleted, which verifies the discharge by construction.
agda src/Ledger.lagda.md and scan_properties.py --check both green.

Checklist

Commit sequence broadly makes sense and commits have useful messages
Any semantic changes to the specifications are documented in CHANGELOG.md (none in this PR)
Code is formatted according to CONTRIBUTING.md
Self-reviewed the diff

🤖 AI-assisted development: Claude Fable 5 (Anthropic)

Records the precise, ordered steps to make this PR faithful to the top-down plan: delete the Certs-PoV provider modules (Certs/Properties/PoV and PoVLemmas, which are #1210's work), drop their imports from Certs/Properties, and lift the facts they provide (CERTS-pov, and later CERTS-coinFromDeposits-updateCertDeposits) to module parameters in Entities.Properties.PoV and the LEDGER-PoV module. Notes that Utxo/Utxow-PoV are already absent (deferred to #1189) and already parameterized, flags the Conway-side touches to re-check, and cross-references the separate coinFromGovDeposit re-derivation. Prose only; to be executed in a session with the Agda toolchain so each step can be typechecked. https://claude.ai/code/session_0174ZBS1RKAGSbBXDsESUwoA

…mas (#1186) First piece of the utxo/utxow-pov work that discharges #1187/#1203's UTxO-side module parameters. Ported verbatim from the stale #1189 branch (1186-dijkstra-utxo-and-utxow-pov); typechecks unchanged against the current spec (Agda 2.8.0 via the Nix flake), since these lemmas are era-independent: - ∙-homo-Coin : coin (x + y) ≡ coin x + coin y (coin monoid homomorphism) - coin-∑ˡ : coin distributes over a list-indexed ∑ˡ - newTxid⇒disj : TxId freshness ⇒ disjointness of dom utxo and dom (outs tx) - outs-disjoint : the (utxo ∣ SpendInputs ᶜ) / outs specialisation used by PoV balance-∪ / split-balance remain module parameters of Utxo.Properties.PoV (the set-theoretic balance-arithmetic port is tracked separately). Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01We2YdXX2ozJAdAbCrRwi6r

Records the precise, ordered steps to make this PR faithful to the top-down plan: delete the Certs-PoV provider modules (Certs/Properties/PoV and PoVLemmas, which are #1210's work), drop their imports from Certs/Properties, and lift the facts they provide (CERTS-pov, and later CERTS-coinFromDeposits-updateCertDeposits) to module parameters in Entities.Properties.PoV and the LEDGER-PoV module. Notes that Utxo/Utxow-PoV are already absent (deferred to #1189) and already parameterized, flags the Conway-side touches to re-check, and cross-references the separate coinFromGovDeposit re-derivation. Prose only; to be executed in a session with the Agda toolchain so each step can be typechecked. https://claude.ai/code/session_0174ZBS1RKAGSbBXDsESUwoA

Copilot

🟡 Changes recommended

The property catalog makes unsupported preservation claims and must be corrected before approval.

Once you've addressed the issues Copilot identified, you can request another Copilot review.

Review details

Suppressed comments (3)

src/Ledger/Dijkstra/Specification/Ledger/Properties/PoV.lagda.md:188

The UTXO rule currently has no TxId-freshness premise, so this comment incorrectly states that the rule establishes freshness at batch level. This is still an assumption pending #1274 and should be documented as such.

  -- Batch-wide invariants on the post-SUBLEDGERS UTxO state.  Both follow from
  -- batch-wide input disjointness and TxId freshness, which the outer UTXO rule
  -- establishes at batch level, not per-step.

src/Ledger/Dijkstra/Specification/Utxo/Properties/PoV.lagda.md:139

This says the consumer discharges noMintingSubTxs, but LEDGER-PoV still accepts noMintSubTx as a module parameter (lines 183–184); discharge from SUBLEDGERS is deferred to #1274. Please describe it as a currently threaded hypothesis rather than an accomplished discharge.

steps.  The batch-balance lemmas below therefore take the following
per-transaction fact as a hypothesis; the `LEDGER`{.AgdaDatatype}-level consumer
discharges it from the `SUBLEDGERS`{.AgdaDatatype} derivation.

src/Ledger/Dijkstra/Specification/Utxo/Properties/PoV.lagda.md:53

The current UTXO rule has no batch TxId-freshness premise (see Utxo.lagda.md:507-527), and #1274 explicitly leaves open whether such a premise must be added. Claiming here that the rule already establishes fresh TxIds is therefore inaccurate; describe freshness as a required batch-threading hypothesis instead.

The `UTXO`{.AgdaDatatype} rule establishes this batch-wide (spend inputs are mutually
disjoint across the batch, TxIds are fresh) but does not expose it per step.

Files reviewed: 10/10 changed files
Comments generated: 3
Review effort level: Balanced

williamdemeo · 2026-09-09T03:53:43Z

+    notes: "Covers both thm:CERT-PoV and thm:CERTS-PoV."
+
+  - id: dijkstra-utxo-pov
+    title: "UTXO preserves value"


Indeed, the new property tracker is not immune to human error. I need to fix the properties.yaml catalog entries.

+    notes: ""
+
+  - id: dijkstra-utxow-pov
+    title: "UTXOW preserves value"


…s.Base Port the Conway balance lemmas to Dijkstra: balance-cong, balance-cong-coin, balance-∪ (additivity on disjoint unions) and split-balance (partition along a key-set restriction), plus the freshness lemmas newTxid⇒disj / outs-disjoint, the coin homomorphism law ∙-homo-Coin, and coin-∑ˡ (coin distributes over list-indexed Value sums). The Conway indexedSumᵐ proofs now port directly because the Dijkstra balance is again an indexed sum over a finite map of transaction outputs (∑[ x ← mapValues txOutToValue utxo ] x); the earlier ∑ˢ-over-ℙ-Value definition that blocked this port is gone. balance-∪, split-balance and outs-disjoint match the corresponding module parameters of Ledger.Properties.PoV (#1203), which they discharge (#1186). AI-assisted: Claude Fable 5 (Anthropic)

…te change Add Utxo.Properties.PoV with the UTXO-level preservation-of-value facts (#1186): * Layered coin projection of the batch balance premise consumedBatch ≡ producedBatch (premise 8 of the UTXO rule): per-transaction (coin-consumedTx, coin-producedTx), sums over sub-transactions (coin-∑-consumedTx-sub, coin-∑-producedTx-sub), and batch level (coin-consumedBatch, coin-producedBatch), in the closed form consumed by LEDGER-pov — cert deposits as refundCertDeposits/newCertDeposits over allDCerts tx against the pre-batch pool set, gov-action deposits collected into a trailing group. Minted terms drop by premise 7 (top level) and the noMintingSubTxs hypothesis (sub level). * module UTXO-PoV (tx) (noMintSubTx): UTXO-pov-invalid (collateral collection preserves getCoin), UTXO-V-mechanical (valid-case state change given TxId freshness), UTXO-batch-balance-coin. * subutxo-step-coin: the per-step SUBUTXO coin equation, with the two batch-threading facts it needs (sub-tx TxId freshness in the running UTxO, running-vs-snapshot spend-input balance agreement) as explicit hypotheses. Pure +-rearrangements are discharged with the reflective ring solver, stated over raw ℕ addition (_+ᴺ_) per the established pattern in Ledger.Properties.PoV. Register Base and PoV in the Utxo.Properties aggregator. AI-assisted: Claude Fable 5 (Anthropic)

Add Utxow.Properties.PoV (#1186). Both UTXOW constructors (and SUBUTXOW) embed their state-changing UTXO (SUBUTXO) derivation as the final premise, so a pair of extractors (UTXOW⇒UTXO, SUBUTXOW⇒SUBUTXO) reduces every statement to its Utxo.Properties.PoV counterpart: * module UTXOW-PoV (tx) (noMintSubTx): utxow-pov-invalid, UTXOW-V-mechanical, and UTXOW-batch-balance-coin, with statements matching the corresponding module parameters of Ledger.Properties.PoV (#1203) verbatim. * module SUBUTXOW-PoV: subutxow-step-coin, given the two batch-threading invariants (per-sub-tx TxId freshness and running-vs-snapshot spend-input agreement) as module parameters — the SUBUTXOW premises do not provide them; they belong to the same follow-up family as the utxo₁-tx-spend-eq and fresh-top-tx-id parameters of LEDGER-pov. Instantiating LEDGER-PoV with these lemmas (balance-∪/split-balance/ outs-disjoint from Utxo.Properties.Base with the η-wrappers from the PR #1203 design notes, subutxow-step-coin from SUBUTXOW-PoV, and the three UTXOW facts from UTXOW-PoV) has been verified to elaborate LEDGER-pov end-to-end. Register the module in the Utxow.Properties aggregator. AI-assisted: Claude Fable 5 (Anthropic)

Per the review policy established on the base PR: issue numbers and follow-up prose move to the PR description; the ring-solver/HasAdd explanation duplicated from Ledger.Properties.PoV becomes a cross-reference; open module parameters are described in present tense. AI-assisted: Claude Fable 5 (Anthropic)

Per review feedback: open with the theorem and argument in plain terms, then a dedicated section answering why the proof splits into the mechanical and batch-balance pieces (different UTxOs: running state vs pre-batch snapshot) and why the batch-balance statement mentions no states, then the Conway differences and the detailed proof map. Echo the running-vs-snapshot point locally at UTXO-V-mechanical and UTXO-batch-balance-coin. Final polish: + general improvements + add mkdocs nav entries AI-assisted: Claude Fable 5 (Anthropic)

…eir parameters The UTxO-side obligations of LEDGER-PoV are theorems on this branch, so the module now imports them instead of assuming them: utxow-pov-invalid, UTXOW-V-mechanical and UTXOW-batch-balance-coin from UTXOW-PoV, and subutxow-step-coin from SUBUTXOW-PoV. The unused balance-∪, split-balance, outs-disjoint and noMintTx parameters are dropped outright. SUBUTXOW-PoV's two batch-threading hypotheses (subtx-fresh-txid, subtx-spend-agree) surface as new parameters, in the same family as utxo₁-tx-spend-eq/fresh-top-tx-id. noMintingSubTxs now has a single home in Utxo.Properties.PoV. AI-assisted development: Claude Fable 5 (Anthropic)

Co-authored-by: Copilot Autofix powered by AI <175728472+Copilot@users.noreply.github.com>

williamdemeo self-assigned this May 7, 2026

williamdemeo linked an issue May 7, 2026 that may be closed by this pull request

[Dijkstra] UTxO and UTxOW PoV #1186

Open

3 tasks

williamdemeo force-pushed the 1186-dijkstra-utxo-and-utxow-pov branch from 6763664 to ca99121 Compare May 7, 2026 20:23

williamdemeo changed the base branch from master to 1185-dijkstra-certs-pov May 7, 2026 20:28

williamdemeo force-pushed the 1186-dijkstra-utxo-and-utxow-pov branch 4 times, most recently from f34dd7b to ed32fcc Compare May 8, 2026 22:32

williamdemeo mentioned this pull request May 11, 2026

[Dijkstra] CIP-159-11: PoV property proofs (#1123) #1169

Closed

4 tasks

williamdemeo force-pushed the 1186-dijkstra-utxo-and-utxow-pov branch from ed32fcc to 60167ea Compare May 12, 2026 05:25

williamdemeo marked this pull request as ready for review May 12, 2026 05:45

williamdemeo marked this pull request as draft May 14, 2026 04:28

williamdemeo force-pushed the 1186-dijkstra-utxo-and-utxow-pov branch 2 times, most recently from cf7a86b to e494a2e Compare May 14, 2026 19:51

williamdemeo force-pushed the 1186-dijkstra-utxo-and-utxow-pov branch 3 times, most recently from 91db883 to ac0e814 Compare May 20, 2026 01:13

williamdemeo mentioned this pull request May 21, 2026

[Dijkstra] CIP-159-11c: Prove LEDGER preservation of value (#1187) #1203

Merged

4 tasks

williamdemeo mentioned this pull request Jun 23, 2026

[Dijkstra] LEDGER-pov: complete the proof — gov re-derivation; Certs/Utxo/Utxow facts as parameters #1223

Merged

4 tasks

williamdemeo changed the title ~~[Dijkstra] CIP-159-11b: Prove UTxO and UTxOW preservation of value (#1186)~~ WIP -- [Dijkstra] CIP-159-11b: Prove UTxO and UTxOW preservation of value (#1186) Jun 23, 2026

williamdemeo force-pushed the 1186-dijkstra-utxo-and-utxow-pov branch 2 times, most recently from 562929d to 23691f0 Compare August 13, 2026 02:47

williamdemeo added property Ledger property (tracked in the catalog) era: dijkstra labels Aug 13, 2026

williamdemeo force-pushed the 1186-dijkstra-utxo-and-utxow-pov branch 2 times, most recently from ef59a39 to c600099 Compare August 18, 2026 03:47

williamdemeo force-pushed the 1186-dijkstra-utxo-and-utxow-pov branch from c600099 to 1701aa1 Compare September 3, 2026 02:08

williamdemeo force-pushed the 1186-dijkstra-utxo-and-utxow-pov branch from 1701aa1 to 51c8463 Compare September 3, 2026 02:10

Base automatically changed from 1187-dijkstra-NEW-ENTITIES-ledger-pov to master September 4, 2026 03:21

williamdemeo force-pushed the 1186-dijkstra-utxo-and-utxow-pov branch 2 times, most recently from 35a5f55 to cf3a26d Compare September 8, 2026 19:08

williamdemeo requested review from carlostome and a balanced review from Copilot September 9, 2026 03:43

Copilot started reviewing on behalf of williamdemeo September 9, 2026 03:43 View session

Copilot AI reviewed Sep 9, 2026

View reviewed changes

williamdemeo and others added 10 commits September 9, 2026 14:01

update properties catalog file

1cd3bec

update properties dashboard

db8b8f8

simplifications and other improvements

b7c5b42

Fix HTML entity encoding in documentation

2c05ac6

Co-authored-by: Copilot Autofix powered by AI <175728472+Copilot@users.noreply.github.com>

williamdemeo force-pushed the 1186-dijkstra-utxo-and-utxow-pov branch from 1180e42 to 2c05ac6 Compare September 9, 2026 20:01

Navigation Menu

Uh oh!

[Dijkstra] CIP-159-11b: Prove UTxO and UTxOW preservation of value (#1186) - #1189

[Dijkstra] CIP-159-11b: Prove UTxO and UTxOW preservation of value (#1186)#1189
williamdemeo wants to merge 10 commits into
masterfrom
1186-dijkstra-utxo-and-utxow-pov

williamdemeo commented May 7, 2026 •

edited

Loading

Uh oh!

Copilot AI left a comment

Uh oh!

williamdemeo Sep 9, 2026

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants

Uh oh!

Conversation

williamdemeo commented May 7, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Description

What lands

Key points for review

Verification

Checklist

Uh oh!

Copilot AI left a comment

Choose a reason for hiding this comment

🟡 Changes recommended

Suppressed comments (3)

Uh oh!

williamdemeo Sep 9, 2026

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants

williamdemeo commented May 7, 2026 •

edited

Loading