[Dijkstra] CIP-159-11c: Prove LEDGER preservation of value (#1187) by williamdemeo · Pull Request #1203 · IntersectMBO/formal-ledger-specifications

williamdemeo · 2026-05-21T02:02:43Z

Description

Property proved

The Dijkstra LEDGER rule preserves value.

getCoin s ≡ getCoin s', assuming PoolDepositsRegistered (CertStateOf s)

where getCoin (LedgerState) sums UTxO coin, the rewards balance, the cert-deposit pots, and the gov-action deposits.

New hypothesis

POOL-reg adds the pool deposit with a left-biased union.

At a state holding a stale pot entry for an unregistered pool, registering that pool destroys the deposit of the batch balance; preservation is genuinely false there, not merely unprovable.

PoolDepositsRegistered asserts that every pool-deposit entry belongs to a registered pool, defined in Certs.

This precludes a state holding a stale pot entry for an unregistered pool. Moreover, this condition holds on-chain by construction, so a chain-level reachability argument discharges it.

Shape of the proof

There are no per-rule PoV theorems to compose here: Dijkstra's only balance premise is batch-wide.

So LEDGER-V is a single LedgerState-level equational chain, resting on three cancellations:

total direct-deposit value cancels between the UTxO side (producedBatch) and the CertState side (applyDirectDeposits in ENTITIES);
the batch-wide cert-deposit accounting (SUBLEDGERS-deposits, telescoping the per-step closed forms) reconciles the deposit pots against the batch balance;
gov-deposit growth is matched against the produced-side govProposalsDeposits.

Everything below LEDGER is left as a module parameter, so this PR proves exactly what LEDGER-pov needs and the parameter list is a frozen contract for the follow-ups.

What lands

Ledger/Properties/PoV.lagda.md: LEDGER-pov, the four SUBLEDGERS inductions, posNeg-deposits;
Entities/Properties/PoV.lagda.md: per-transaction accounting for the post-[Dijkstra] Refactor ENTITIES and add SUBENTITIES #1256 tx-signal rules, split by getCoin (CertState) component, combining to coin in + direct deposits + new deposits ≡ coin out + withdrawals + refunds;
Entities/Properties/ApplyToRewardsPoV.lagda.md: the withdrawal / direct-deposit fold lemmas.

Spec changes, each forced by the accounting.

Ledger.lagda.md: getCoin (LedgerState) gains coinFromGovDeposit; Gov-action deposits live in GovActionState.deposit, not GState.deposits, yet the UTXO batch balance charges govProposalsDeposits on the produced side; without this summand the total is not preserved.
Certs.lagda.md: getCoin (CertState) is now total (rewards balance plus the three deposit pots), with coinFromRewards/coinFromDeposits projections, and the new PoolDepositsRegistered invariant.
Prelude.lagda.md: era-independent sum lemmas (+-interleave, sum-map-+).

Assumptions: module parameters left open

Group	Issue	PR	Parameters
Certs-PoV	#1185	#1210	`CERTS-rewards-pov`, `CERTS-deposits-pov`, `CERTS-deposits-registered`, `CERTS-new-thread`, `refundCertDeposits-++`
Utxo/Utxow-PoV	#1186	#1189	`UTXOW-batch-balance-coin`, `UTXOW-V-mechanical`, `utxow-pov-invalid`, `subutxow-step-coin`, `balance-∪`, `split-balance`, `outs-disjoint`, `noMintTx`, `noMintSubTx`, `utxo₁-tx-spend-eq`, `fresh-top-tx-id`
Gov-PoV	#1276	#1278	`GOVS-coinFromGovDeposit`, `rmOrphanDRepVotes-coinFromGovDeposit`
Withdrawal bounds	#1275	`*`	`ENTITIES-wdrls-bounded`, `SUBENTITIES-wdrls-bounded`
Reachability	`*`	`*`	`PoolDepositsRegistered` for on-chain initial states
Set/map identities	`*`	`*`	`∪ˡ-lookup-preserve`, `sum-map-proj₂≡getCoin`, `setToList-Unique` (`agda-sets` candidates)

* = TODO (nothing filed yet)

Three of these deserve a word on why they are shaped the way they are.

CERTS-deposits-pov states the deposit accounting in closed form, D + newCertDeposits (dom pools) certs ≡ D' + refundCertDeposits certs, under a PoolDepositsRegistered premise, without which POOL-reg's left-biased update falsifies it. CERTS-new-thread splits newCertDeposits over xs ++ ys at a run boundary with the ys half against the run's final pool set; that is precisely what lets per-run accounting compose across a batch.
The whole-batch composition of the Certs facts is not assumed; SUBLEDGERS-deposits derives it.
UTXOW-batch-balance-coin keeps cert deposits in the spec's closed form, so it stays a pure UTxO obligation with no post-batch cert states in it.
The withdrawal bounds are assumed rather than derived because of a real spec gap: the premises bound withdrawals only against the pre-batch rewards₀ (except top-level legacy mode), which does not bound them against the input state of a later step in the batch; the phantom-withdrawal gap flagged in the [Dijkstra] Refactor ENTITIES and add SUBENTITIES #1256 review. Needs a spec-side premise or a batch-threading invariant.

Checklist

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

🤖 Generated with Claude Code
🧑 Curated and revised by @williamdemeo

Split out of the LEDGER-pov work (#1203): this Conway-era properties cleanup is independent of the Dijkstra PoV proof and belongs in its own PR. - Add reusable coin/map lemmas to `Ledger.Prelude`: `getCoin-singleton`, `getCoin-cong`, `indexedSumᵛ'-∪`, `res-decomp`, `∪ˡsingleton∈dom`, `∪ˡsingleton∉dom`, `∪ˡsingleton0≡`, `sumConstZero`, `indexedSumL-proj₂-zero`, `setToList-∈`; relocate `≡ᵉ-getCoin` into the `⦃ DecEq A ⦄` module. - Drop the now-provable assumption parameters from the Conway PoV proofs, using the Prelude lemmas instead: - `Certs/Properties/PoV`: keep only `≡ᵉ-getCoinˢ'`. - `Certs/Properties/PoVLemmas`: remove the local `∪ˡsingleton*`/`getCoin-singleton` helpers and the `indexedSumᵛ'-∪` assumption module; qualify `IsEquivalence` as `Eq`. - `Ledger/Properties/PoV`: keep only `≡ᵉ-getCoinˢ`. - `Conformance/Properties`: drop the `indexedSum-∪⁺-hom` parameter. - `Utxo/Properties/GenMinSpend`: use the hoisted `getCoin-singleton`. No spec-semantic change (proof refactor only), so no CHANGELOG entry. `Ledger.Prelude` typechecks under Agda 2.8.0 via the project flake; the Conway files are their 1187 versions (which typecheck) and depend only on the hoisted lemmas. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01We2YdXX2ozJAdAbCrRwi6r

Copilot

Pull request overview

This PR adds Dijkstra-era preservation-of-value (PoV) proofs for the top-level LEDGER rule (parameterising lower-layer PoV facts for follow-up PRs), and fixes specification accounting so governance-action deposits and cert/governance deposit flows are counted on the correct sides of the batch-balance equations.

Changes:

Introduces new Dijkstra PoV proof modules for LEDGER and ENTITIES, plus supporting applyToRewards PoV lemmas.
Fixes Dijkstra spec accounting: moves deposit terms to the correct produced/consumed sides in Utxo, and extends getCoin (LedgerState) to include coinFromGovDeposit.
Centralises reusable getCoin/map-sum lemmas in Ledger.Prelude and updates Conway call sites accordingly; adds .claude/ tooling docs/hooks for Agda typechecking via Nix.

Reviewed changes

Copilot reviewed 18 out of 18 changed files in this pull request and generated 1 comment.

Show a summary per file

File	Description
`src/Ledger/Prelude.lagda.md`	Adds reusable `getCoin`/map-sum and union/singleton coin lemmas used by PoV proofs.
`src/Ledger/Dijkstra/Specification/Utxo.lagda.md`	Fixes deposit term placement in consumed/produced accounting (new deposits on produced, refunds on consumed).
`src/Ledger/Dijkstra/Specification/Transaction.lagda.md`	Relocates `HasDirectDeposits` interface out of `Transaction` (record removed here).
`src/Ledger/Dijkstra/Specification/Ledger/Properties/PoV.lagda.md`	New: top-level Dijkstra `LEDGER-pov` proof (parameterised over lower-layer lemmas).
`src/Ledger/Dijkstra/Specification/Ledger.lagda.md`	Extends `getCoin (LedgerState)` with `coinFromGovDeposit` and documents the 4-summand accounting.
`src/Ledger/Dijkstra/Specification/Entities/Properties/PoV.lagda.md`	New: PoV for `ENTITIES` bridging withdrawals/direct-deposits around `CERTS`.
`src/Ledger/Dijkstra/Specification/Entities/Properties/ApplyToRewardsPoV.lagda.md`	New: PoV lemmas for `applyWithdrawals` and `applyDirectDeposits` fold structure.
`src/Ledger/Dijkstra/Specification/Certs.lagda.md`	Adds `HasDirectDeposits` instance for `CertEnv`.
`src/Ledger/Dijkstra/Specification/Account.lagda.md`	Adds/hosts the `HasDirectDeposits` interface next to `DirectDeposits`.
`src/Ledger/Conway/Specification/Utxo/Properties/GenMinSpend.lagda.md`	Adapts to `getCoin-singleton` being provided by `Ledger.Prelude`.
`src/Ledger/Conway/Specification/Ledger/Properties/PoV.lagda.md`	Simplifies assumptions and updates to the new Prelude lemma surface.
`src/Ledger/Conway/Specification/Certs/Properties/PoVLemmas.lagda.md`	Refactors imports/assumptions to rely on Prelude-provided coin lemmas.
`src/Ledger/Conway/Specification/Certs/Properties/PoV.lagda.md`	Updates `Certs-PoV` module assumptions accordingly.
`src/Ledger/Conway/Conformance/Properties.lagda.md`	Removes now-unneeded indexed-sum homomorphism assumption.
`CHANGELOG.md`	Documents the semantic spec fixes (deposit-side swap; governance deposits counted in ledger total).
`.claude/skills/agda-typecheck/SKILL.md`	Adds developer guidance for typechecking Agda via the project Nix flake.
`.claude/settings.json`	Registers a `SessionStart` hook for Claude Code sessions.
`.claude/hooks/session-start.sh`	Adds a hook to provision Nix + warm the dev shell for Agda typechecking.

💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.

…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

Split out of the LEDGER-pov work (#1203): this Conway-era properties cleanup is independent of the Dijkstra PoV proof and belongs in its own PR. - Add reusable coin/map lemmas to `Ledger.Prelude`: `getCoin-singleton`, `getCoin-cong`, `indexedSumᵛ'-∪`, `res-decomp`, `∪ˡsingleton∈dom`, `∪ˡsingleton∉dom`, `∪ˡsingleton0≡`, `sumConstZero`, `indexedSumL-proj₂-zero`, `setToList-∈`; relocate `≡ᵉ-getCoin` into the `⦃ DecEq A ⦄` module. - Drop the now-provable assumption parameters from the Conway PoV proofs, using the Prelude lemmas instead: - `Certs/Properties/PoV`: keep only `≡ᵉ-getCoinˢ'`. - `Certs/Properties/PoVLemmas`: remove the local `∪ˡsingleton*`/`getCoin-singleton` helpers and the `indexedSumᵛ'-∪` assumption module; qualify `IsEquivalence` as `Eq`. - `Ledger/Properties/PoV`: keep only `≡ᵉ-getCoinˢ`. - `Conformance/Properties`: drop the `indexedSum-∪⁺-hom` parameter. - `Utxo/Properties/GenMinSpend`: use the hoisted `getCoin-singleton`. No spec-semantic change (proof refactor only), so no CHANGELOG entry. `Ledger.Prelude` typechecks under Agda 2.8.0 via the project flake; the Conway files are their 1187 versions (which typecheck) and depend only on the hoisted lemmas. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01We2YdXX2ozJAdAbCrRwi6r

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. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>

…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). Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>

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. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>

…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). Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>

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. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>

…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). Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>

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. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>

…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)

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)

…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)

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)

carlostome · 2026-09-01T12:27:29Z

+- Add `PoolDepositsRegistered` (every pool-deposit entry belongs to a registered
+  pool) to `Certs`; the deposit accounting genuinely fails without it, since
+  `POOL-reg` adds its deposit with a left-biased union.
+- Count governance-action deposits in `getCoin LedgerState` via a new
+  `coinFromGovDeposit : GovState → Coin` (sum of `GovActionState.deposit`).  These
+  deposits live in `GovActionState.deposit`, not `GState.deposits`, so the three
+  `CertState` deposit pots alone do not account for them.
+- Make `getCoin` on `CertState` total (rewards balance plus the three deposit pots) and
+  add the `coinFromRewards`/`coinFromDeposits` projections in `Certs`.


We should really think through the policy about a CHANGELOG on something that is WIP

I'll remove the changelog entries from this PR.

williamdemeo · 2026-09-03T02:07:43Z

@carlostome thanks for the review. I cleaned up the prose and removed the paragraph you suggested looked out-of-place. I think this PR is finally ready!

…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)

carlostome

LGTM! I left a couple of small nitpicks but it looks great

carlostome · 2026-09-03T10:25:01Z

+- Add `PoolDepositsRegistered` (every pool-deposit entry belongs to a registered
+  pool) to `Certs`; the deposit accounting genuinely fails without it, since
+  `POOL-reg` adds its deposit with a left-biased union.
+- Count governance-action deposits in `getCoin LedgerState` via a new
+  `coinFromGovDeposit : GovState → Coin` (sum of `GovActionState.deposit`).  These
+  deposits live in `GovActionState.deposit`, not `GState.deposits`, so the three
+  `CertState` deposit pots alone do not account for them.
+- Make `getCoin` on `CertState` total (rewards balance plus the three deposit pots) and
+  add the `coinFromRewards`/`coinFromDeposits` projections in `Certs`.


Prove `LEDGER-pov` for the Dijkstra LEDGER rule: getCoin s ≡ getCoin s', where getCoin (LedgerState) sums UTxO coin, the rewards balance, the three cert-deposit pots, and the gov-action deposits. Typechecks under --safe with no postulates or holes. Top-down plan: the supporting Certs / UTxO / Gov facts are module parameters of `Ledger.Properties.PoV`, forming the frozen contract for the follow-up PRs (#1186 utxo/utxow, #1210 certs, and a future Gov PoV). New modules: - Ledger/Properties/PoV: LEDGER-pov. The LEDGER-V case is a single LedgerState-level equational chain; direct-deposit value cancels between the UTxO and CertState sides, gov-deposit growth is matched against the produced-side govProposalsDeposits, and `bat'` converts the closed-form batch balance (#1186 shape) to the chain's two-level posPart/negPart deposit form via the batch-cert-deposits-bridge (#1210 shape) and net-arith. - Entities/Properties/PoV: ENTITIES-pov and SUBENTITIES-pov, the value-flow equations for the post-#1256 tx-signal rules. NetworkId and domain facts come from the rules' own premises; the no-truncation bound (withdrawal amount ≤ input-state balance) is an explicit hypothesis — the phantom-withdrawal gap flagged in the #1256 review, provided at the LEDGER level by the ENTITIES/SUBENTITIES-wdrls-bounded parameters. - Entities/Properties/ApplyToRewardsPoV: applyWithdrawals-pov and applyDirectDeposits-pov fold lemmas. Spec changes: - Ledger: getCoin (LedgerState) gains a coinFromGovDeposit summand (gov-action deposits live in GovActionState.deposit, not GState.deposits, yet the UTXO batch balance charges govProposalsDeposits on the produced side). - Certs: getCoin (CertState) is now total (rewards + deposit pots), with coinFromRewards / coinFromDeposits projections. - Prelude: era-independent sum lemmas (+-interleave, sum-map-+). Squash of the pre-rebase branch (13 WIP commits, head f677e1b), rebased onto master and adapted to #1250 (explicit cert deposits, closed-form newCertDeposits/refundCertDeposits), #1253/#1256 (EntitiesEnv, SUBENTITIES, tx-signal ENTITIES), #1262 (legacyMode threading), and deposit sign-swap fix in #1250, so it is no longer part of the diff. AI-assisted: Claude Fable 5 (Anthropic)

… solver Replace the hand-written equational chains of the pure +-rearrangement helpers (swap-right, abcd-to-acdb, mid-extract, rearr3, outer-rearr, arithmetic-1..5, net-arith's rearr-X/Y/Z, reshuffle-to-DD's core) with the reflective ring solver over the ℕ commutative semiring (Data.Nat.Tactic.RingSolver): solve-∀ for closed all-visible ∀-goals, in-context solve where trailing variables are implicit. The solver matches the ring's operations syntactically, so the solver-facing statements use the raw Data.Nat._+_ (imported as _+ᴺ_) rather than the Ledger.Prelude HasAdd overload, which only *reduces* to it; the two are definitionally equal, so all call sites are unchanged. reshuffle-to-DD generalises its where-bound abbreviations to a closed ∀-goal first, since syntactic atom matching cannot see through them. Also drop unused integer imports (0ℤ, _-_, +ℤ-comm). Net: 133 lines of tedious associativity/commutativity shuffling deleted; statements and chain structure unchanged. Typechecks under --safe (full src/Ledger root green). AI-assisted: Claude Fable 5 (Anthropic)

…batch bridge Per review: the Certs-level parameters now state the complete value accounting of a CERTS run, and the ENTITIES PoV module surfaces it per transaction: - CERTS-rewards-pov (rewards preserved), CERTS-deposits-pov (closed-form deposit accounting D + new ≡ D' + refunds), CERTS-deposits-registered (invariant preservation), CERTS-new-thread (newCertDeposits split at a run boundary), refundCertDeposits-++ (fold algebra). - Entities.Properties.PoV adds SUBENTITIES/ENTITIES-deposits-pov, -deposits-registered, SUBENTITIES-new-thread (all definitional transports of the CERTS facts), and the combined full-CertState-coin identities SUBENTITIES/ENTITIES-pov-total: coin in + direct deposits + new deposits ≡ coin out + withdrawals + refunds. - Ledger.Properties.PoV now *derives* the batch-wide deposit accounting (SUBLEDGERS-deposits, telescoping per-step closed forms across the batch, with SUBLEDGERS-registered threading the invariant and refund-concatMap recombining refunds); the batch-cert-deposits-bridge parameter is gone. Its premises mentioned SUBLEDGERS, so it was not statable at the Certs level anyway. Restating the per-run accounting exposed a genuine soundness condition: POOL-reg adds its deposit with a left-biased union, so at a state with a stale pot entry for an unregistered pool, registering that pool destroys the deposit the batch balance charges, and value preservation is false. New PoolDepositsRegistered invariant in Certs (every pool-deposit entry belongs to a registered pool; preserved by CERTS, holds on-chain by construction); LEDGER-pov now takes it as a hypothesis on the initial state. The old bridge parameter silently baked in the same assumption and would have been undischargeable as stated. Also apply the review's prose policy: status/roadmap/issue-number prose moved from module documentation to the PR description; explanations deduplicated across modules (stated once, referenced elsewhere). Final touches: + general improvements + remove unnecessary CHANGELOG entry + add mkdocs nav entries AI-assisted: Claude Fable 5 (Anthropic)

Co-authored-by: Carlos Tomé Cortiñas <carlos.tome-cortinas@iohk.io>

williamdemeo self-assigned this May 21, 2026

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

[Dijkstra] LEDGER PoV #1187

Closed

3 tasks

williamdemeo mentioned this pull request May 21, 2026

[Dijkstra] (DEPRECATED) CIP-159-11c: Prove LEDGER PoV #1190

Closed

4 tasks

williamdemeo force-pushed the 1187-dijkstra-NEW-ENTITIES-ledger-pov branch 4 times, most recently from a723193 to e5190e8 Compare May 27, 2026 20:42

williamdemeo force-pushed the 1187-dijkstra-NEW-ENTITIES-ledger-pov branch 2 times, most recently from 5d054ab to e24b1b0 Compare June 2, 2026 04:33

williamdemeo force-pushed the 1187-dijkstra-NEW-ENTITIES-ledger-pov branch 2 times, most recently from c167cba to 3cc8b70 Compare June 15, 2026 22:34

williamdemeo changed the title ~~[Dijkstra] CIP-159-11c: Prove LEDGER preservation of value (#1187)~~ WIP -- [Dijkstra] CIP-159-11c: Prove LEDGER preservation of value (#1187) Jun 23, 2026

williamdemeo force-pushed the 1187-dijkstra-NEW-ENTITIES-ledger-pov branch from a1f3738 to 54853be Compare June 25, 2026 03:54

williamdemeo changed the title ~~WIP -- [Dijkstra] CIP-159-11c: Prove LEDGER preservation of value (#1187)~~ [Dijkstra] CIP-159-11c: Prove LEDGER preservation of value (#1187) Jun 25, 2026

williamdemeo marked this pull request as ready for review June 25, 2026 04:10

williamdemeo requested a review from Copilot June 25, 2026 04:10

Copilot started reviewing on behalf of williamdemeo June 25, 2026 04:11 View session

Copilot AI reviewed Jun 25, 2026

View reviewed changes

Comment thread .claude/hooks/session-start.sh Outdated

williamdemeo changed the base branch from master to claude/conway-pov-cleanup June 25, 2026 04:21

williamdemeo changed the base branch from claude/conway-pov-cleanup to master June 25, 2026 04:21

williamdemeo force-pushed the 1187-dijkstra-NEW-ENTITIES-ledger-pov branch from 04cf4c7 to a651f09 Compare August 10, 2026 19:58

williamdemeo force-pushed the 1187-dijkstra-NEW-ENTITIES-ledger-pov branch 3 times, most recently from b277131 to 6bea3e8 Compare August 12, 2026 05:42

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

williamdemeo force-pushed the 1187-dijkstra-NEW-ENTITIES-ledger-pov branch from 6718d6a to 164f116 Compare August 18, 2026 03:18

carlostome reviewed Sep 1, 2026

View reviewed changes

williamdemeo force-pushed the 1187-dijkstra-NEW-ENTITIES-ledger-pov branch from e3b7d4a to 3d69937 Compare September 3, 2026 02:06

carlostome approved these changes Sep 3, 2026

View reviewed changes

williamdemeo and others added 7 commits September 3, 2026 19:25

address Copilot review + minor improvements

8659c9f

Update src/Ledger/Dijkstra/Specification/Ledger/Properties/PoV.lagda.md

5375c72

Co-authored-by: Carlos Tomé Cortiñas <carlos.tome-cortinas@iohk.io>

clean up prose and remove out-of-place comment on POOL-reg.

c19d82c

remove CHANGELOG additions since we're not tracking changes to WIP

91ed08e

Navigation Menu

Uh oh!

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

[Dijkstra] CIP-159-11c: Prove LEDGER preservation of value (#1187)#1203
williamdemeo merged 7 commits into
masterfrom
1187-dijkstra-NEW-ENTITIES-ledger-pov

williamdemeo commented May 21, 2026 •

edited

Loading

Uh oh!

Copilot AI left a comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

carlostome Sep 1, 2026

Uh oh!

williamdemeo Sep 3, 2026

Uh oh!

carlostome Sep 3, 2026

Uh oh!

Uh oh!

williamdemeo commented Sep 3, 2026

Uh oh!

carlostome left a comment

Uh oh!

carlostome Sep 3, 2026

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

Uh oh!

Conversation

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

Uh oh!

Description

Property proved

New hypothesis

Shape of the proof

What lands

Assumptions: module parameters left open

Checklist

Uh oh!

Copilot AI left a comment

Choose a reason for hiding this comment

Pull request overview

Reviewed changes

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

carlostome Sep 1, 2026

Choose a reason for hiding this comment

Uh oh!

williamdemeo Sep 3, 2026

Choose a reason for hiding this comment

Uh oh!

carlostome Sep 3, 2026

Choose a reason for hiding this comment

Uh oh!

Uh oh!

williamdemeo commented Sep 3, 2026

Uh oh!

carlostome left a comment

Choose a reason for hiding this comment

Uh oh!

carlostome Sep 3, 2026

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

williamdemeo commented May 21, 2026 •

edited

Loading