[Dijkstra] CIP-159-11: PoV property proofs (#1123) by williamdemeo · Pull Request #1169 · IntersectMBO/formal-ledger-specifications

williamdemeo · 2026-04-14T06:07:50Z

Description

Closes #1123.

Summary

This PR adds preservation-of-value (PoV) property modules for the Dijkstra era, adapted from the Conway PoV proof structure to account for CIP-159's partial withdrawals and direct deposits.

Modules

Module	Purpose	Status
`Certs.Properties.PoVLemmas`	`CERT-pov`, `POST-CERT-pov`, `sts-pov`, `PRE-CERT-pov`	Skeleton with Claims
`Certs.Properties.PoV`	`CERTS-pov` top-level theorem	Proved (modulo assumptions)
`Certs.Properties.ApplyWithdrawalsPov`	`applyWithdrawals-pov` fold induction	Skeleton with Claims
`Utxo.Properties.Base` (new)	`∙-homo-Coin`, `newTxid⇒disj`, `outs-disjoint`, `coin-∑ˡ`	Proved
`Utxo.Properties.PoV` (new)	UTXO-level PoV building blocks	Mostly proved
`Utxow.Properties.PoV` (new)	`UTXOW⇒UTXO` extractor + delegated wrappers	Proved
`Ledger.Properties.PoV`	`HasCoin` instances, `LEDGER-pov`	Proved modulo module parameters

UTXO / UTXOW PoV — what's proved

The Dijkstra UTXO PoV proof decomposes into two orthogonal pieces, matching the batch structure of the rule:

Mechanical state change. UTXO-I-getCoin (invalid case: collateral collection preserves getCoin) and UTXO-V-mechanical (valid case: additive rearrangement relating getCoin s₀ to getCoin s₁ via split-balance + balance-∪). Both proved.
Batch coin balance. batch-balance-coin — the coin projection of the consumedBatch ≡ producedBatch premise (premise p₇ of the UTXO rule). Proved, via a three-layer structure:
1. Per-transaction (coin-producedTx, coin-consumedTx): unfold producedTx / consumedTx and peel coin through each + inject _ layer using ∙-homo-Coin + coin∘inject≗id. The consumed version uses coin (MintedValueOf t) ≡ 0 (from UTXO premise p₆ / SUBUTXO premise) to cancel the mint term.
2. Sum-over-sub-transactions (coin-∑-producedTx-sub, coin-∑-consumedTx-sub): push coin through the ∑ˡ-indexed sum using the new coin-∑ˡ lemma (a ~4-line monoid-homomorphism induction in Utxo.Properties.Base), then apply the per-transaction equations pointwise. The consumed version threads a noMintingSubTxs tx hypothesis through the sub-tx list induction.
3. Batch-level (coin-of-consumedBatch, coin-of-producedBatch): peel the outer + inject _ layers, substitute Layer 1 for the top-level summand and Layer 2 for the sub-transaction sum, and finish with a small associative-commutative shuffle using a swap-right helper.

The UTXOW-level proofs (UTXOW-I-getCoin, UTXOW-V-mechanical, UTXOW-batch-balance-coin, utxow-pov-invalid) are thin wrappers: both UTXOW-normal and UTXOW-legacy embed a UTXO derivation as their final premise, so a single UTXOW⇒UTXO extractor reduces every statement to its UTXO-level counterpart.

The combined UTXO-pov theorem is stated but left as a placeholder ({!!}) — its exact form depends on how the LEDGER-pov proof's BatchUtxoAccounting consumer threads sub-transaction state. All three of its building blocks (UTXO-I-getCoin, UTXO-V-mechanical, batch-balance-coin) are already proved.

CERTS PoV — design notes

PRE-CERT-pov uses applyWithdrawals-pov instead of Conway's constMap chain.
Conway's PRE-CERT zeros out withdrawn credentials via constMap wdrlCreds 0 ∪ˡ rewards, and the PoV proof decomposes the rewards map into restricted/complement parts, showing the zeroing removes exactly getCoin wdrls.

Dijkstra's PRE-CERT uses applyWithdrawals wdrls rewards (CIP-159 partial withdrawals), which subtracts each withdrawal amount. The PoV equation getCoin s ≡ getCoin s' + getCoin wdrls still holds, but the proof requires a new lemma (applyWithdrawals-pov) based on fold induction rather than map decomposition.
applyWithdrawals-pov is structured as three layers.
- Single-step (applyOne-pov): Decomposes the accumulator into complement + restriction, shows the decrease equals amt using m∸n+n≡m.
- Fold induction (foldl-applyOne-pov): Induction over setToList (wdrls ˢ), maintaining an invariant that remaining entries have registered credentials with bounded balances. Relies on NoDup (from stake injectivity via NetworkId constraint).
- Top-level (applyWithdrawals-pov): Instantiates the fold with the withdrawal map's list representation.
CERT-pov, POST-CERT-pov, sts-pov are essentially unchanged from Conway.
The Dijkstra DELEG-delegate and DELEG-dereg constructors have the same value-relevant structure (adding/removing zero-balance entries). POST-CERT still only filters voteDelegs.

LEDGER PoV — design notes

LEDGER-pov identifies applyDirectDeposits cancellation as the main new challenge.
In LEDGER-V, certStateFinal = record certState₂ { dState = applyDirectDeposits (allDirectDeposits tx) (DStateOf certState₂) }. Direct deposits appear in producedBatch (UTxO side) and in certStateFinal (CertState side), so they cancel in the total. The proof is an equational chain combining sub-level CERTS-pov (SUBLEDGERS-certs-pov), top-level CERTS-pov, a batch-UTxO-accounting step, and the applyDirectDeposits-rewardsBalance identity.

What's left (deferred to follow-ups)

Outstanding proof obligations (currently stated as module parameters or Claims with detailed proof sketches):

applyOne-pov / foldl-applyOne-pov in Certs.Properties.ApplyWithdrawalsPov.
applyDirectDeposits-rewardsBalance — should follow from ∪⁺ properties.
balance-∪ and split-balance in Utxo.Properties.Base — currently module parameters to Utxo.Properties.PoV. See dedicated tracking issue (the Conway proofs don't port verbatim because Dijkstra defines balance as ∑ˢ over a set of Values rather than indexedSumᵐ over a map of hashed TxOuts).
batch-utxo-accounting in Ledger.Properties.PoV — the final piece combining SUBLEDGERS-utxo-coin (induction over the SUBLEDGERS reflexive-transitive closure), batch-balance-coin, and posPart/negPart arithmetic from calculateDepositsChange. All its dependencies are now in place; the derivation is straightforward equational reasoning.
posPart/negPart depositsChange arithmetic — port from Ledger.Conway.Specification.Utxo.Properties.Base. Era-independent; could be a standalone follow-up.

Invariant properties (§§3–6 of the issue): Direct deposit registration, phantom asset, non-negative balance, balance interval satisfaction. These are mostly straightforward consequences of UTXO-Premises conjuncts. Deferred to follow-up.

Final UTXO-pov statement form: currently a {!!} placeholder pending coordination with the BatchUtxoAccounting consumer.

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

…nce intervals (#1117) CIP-159 changes the transaction balancing rules and introduces Phase-1 balance interval validation. This commit updates the UTxO transition system accordingly. `Utxo.lagda.md`: + Add accountBalances : Rewards field to UTxOEnv and SubUTxOEnv for pre-batch account balance lookups; + Add HasAccountBalances type class and instances; + Update producedTx to include direct deposit amounts on the produced side of the preservation-of-value equation; + Add direct deposit registration premise to UTXO and SUBUTXO (`dom DirectDepositsOf ⊆ dom AccountBalancesOf`); + Add balance interval validation premise to UTXO and SUBUTXO (∀ (c,interval) ∈ BalanceIntervalsOf, InBalanceInterval using pre-batch account balances). `Utxo/Properties/Computational.lagda.md`: + Update Computational-UTXO for new premise tuple arity (19+h → 21+h) `Ledger.lagda.md`: + Add accountBalances field to SubLedgerEnv; + Populate accountBalances in SUBLEDGER-V, SUBLEDGER-I, LEDGER-V, LEDGER-I using RewardsOf certState₀ (pre-batch balances).

#1122) After all sub-rule transitions (`SUBLEDGERS`, `CERTS`, `GOVS`, `UTXOW`), apply batch-wide direct deposits to the final CertState via `applyDirectDeposits` and `allDirectDeposits`. `Ledger.lagda.md`: + Update `LEDGER-V` output: compute `certStateFinal` by applying `allDirectDeposits` to `certState₂`, use `certStateFinal` in the output `LedgerState` and in `rmOrphanDRepVotes`; + `LEDGER-I` unchanged (invalid batches don't apply deposits); + Document direct deposit application ordering and phantom asset prevention rationale. `Ledger/Properties/Computational.lagda.md`: + Update `computeProof` valid branch to compute `certStateFinal` and use it in the output `LedgerState`.

Add preservation-of-value property modules for the Dijkstra era, adapted from the Conway PoV proof structure for CIP-159 (partial withdrawals and direct deposits). New modules: - Certs.Properties.PoVLemmas: CERT-pov, POST-CERT-pov, sts-pov, PRE-CERT-pov (adapted for applyWithdrawals subtraction semantics) - Certs.Properties.PoV: CERTS-pov top-level theorem - Certs.Properties.ApplyWithdrawalsPov: Key new lemma showing applyWithdrawals decreases rewardsBalance by exactly getCoin wdrls - Ledger.Properties.PoV: HasCoin instances, LEDGER-pov statement with proof sketch for direct deposit cancellation Design notes: - PRE-CERT-pov delegates to applyWithdrawals-pov (fold induction) instead of Conway's constMap/res-decomp/sumConstZero chain - LEDGER-pov identifies the applyDirectDeposits cancellation as the main new proof obligation vs Conway - applyWithdrawals-pov is structured as three layers: single-step (applyOne-pov), fold induction (foldl-applyOne-pov), top-level Status: Skeleton with holes; does not yet fully typecheck.

There were unresolved proof obligations from Conway.

Add the applyWithdrawals preservation-of-value proof machinery and prove several lemmas that were previously assumed as module parameters in Conway. New proofs in Ledger.Prelude (previously Conway module parameters): - indexedSumᵛ'-∪: getCoin distributes over disjoint ∪ˡ - sumConstZero: getCoin (constMap X 0) ≡ 0 - getCoin-cong: indexedSum' proj₂ respects set equality - res-decomp: (m ∪ˡ m') ≡ᵉ (m ∪ˡ (m' ∣ dom m ᶜ)) - getCoin-singleton, ≡ᵉ-getCoin, ∪ˡsingleton∈dom, ∪ˡsingleton∉dom, ∪ˡsingleton0≡: singleton map getCoin lemmas - indexedSumL-proj₂-zero: sum of zero-valued entries is zero - setToList-∈: opaque bridge from list membership to set membership New module Certs.Properties.ApplyWithdrawalsPoV: - applyOne-pov: single withdrawal step decreases getCoin by amt - foldl-applyOne-pov: fold induction with Unique invariant - applyWithdrawals-pov: top-level lemma for PRE-CERT-pov - ∪ˡ-res-dom-preserve: ∪ˡ with complement restriction preserves domain membership for other credentials Remaining assumptions (deferred to agda-sets library): - ∪ˡ-res-lookup-preserve: lookupᵐ? stability under ∪ˡ for other keys - sum-map-proj₂≡getCoin: relates list-level sum to indexedSumᵛ' - setToList-Unique: credential uniqueness of withdrawal list - ≡ᵉ-getCoinˢ: getCoin invariance under injective key renaming

State and partially prove the Dijkstra LEDGER preservation-of-value theorem with the corrected HasCoin-LedgerState that includes deposits. - LEDGER-I (invalid case): Fully proved via utxow-pov-invalid. - LEDGER-V (valid case): Equational chain with holes, to be filled. The HasCoin-LedgerState total is: getCoin utxoSt + rewardsBalance(certState) + coinFromDeposits(certState) Key insight: SUBLEDGERS-pov cannot be proved independently because individual SUBUTXO rules have no balance premise — only the batch-level consumedBatch ≡ producedBatch constrains the total. The LEDGER-V proof must reason about the entire step at once.

Complete the LEDGER preservation-of-value proof structure for Dijkstra. - LEDGER-I: Fully proved via utxow-pov-invalid. - LEDGER-V: Complete equational chain with no holes or unresolved metas. Decomposes into: - step-i: combined CERTS accounting (sub + top level) - arithmetic-1, arithmetic-2: ℕ rearrangements - step-iii-iv: batch UTxO + deposit accounting (assumption) - step-ii: applyDirectDeposits cancellation (assumption) New sub-lemma proved: - SUBLEDGERS-certs-pov: induction on ReflexiveTransitiveClosure showing rewardsBalance decreases by exactly the sum of sub-withdrawal amounts. Dispatches SUBLEDGER-I (impossible when isTopLevelValid ≡ true) and SUBLEDGER-V (uses sub-level CERTS-pov with NetworkId extracted from SUBUTXOW → SUBUTXO premises). Remaining assumptions (module parameters): - batch-utxo-accounting: consumedBatch ≡ producedBatch coin projection combined with mechanical UTxO tracking and deposit accounting - applyDirectDeposits-rewardsBalance: gc-hom (∪⁺ distributes getCoin) - utxow-pov-invalid: collateral collection preserves getCoin utxoSt - ∪ˡ-res-lookup-preserve, sum-map-proj₂≡getCoin, setToList-Unique

Introduce three new modules implementing the UTXO-level building blocks of the Dijkstra-era preservation-of-value proof (towards closing #1123 / CIP-159-11): + `Utxo/Properties/Base.lagda.md` Era-independent helper lemmas: `∙-homo-Coin`, `newTxid⇒disj`, `outs-disjoint`. Intentionally minimal for now — the Conway Base proofs of `balance-cong`, `balance-∪`, and `split-balance` do not port verbatim because Dijkstra defines `balance` as `∑ˢ` over a set of Values rather than as `indexedSumᵐ` over a map of hashed TxOuts. Tracking issue filed for the proper port. + `Utxo/Properties/PoV.lagda.md` The Dijkstra UTXO preservation-of-value proof is split into two orthogonal pieces: - Mechanical state change (`UTXO-I-getCoin`, `UTXO-V-mechanical`): relates `getCoin s₀` to `getCoin s₁` from the UTxOState transition alone, using `split-balance` and `balance-∪`. Proved. - Batch coin balance (`batch-balance-coin`): the coin projection of the `consumedBatch ≡ producedBatch` premise (premise p₇ of the UTXO rule). Proved from the two module parameters `coin-of-consumedBatch` and `coin-of-producedBatch`, which are themselves left as assumptions for now (see PoV follow-up work). The combined `UTXO-pov` theorem is stated but left as a placeholder (`?`); its exact form depends on how `LEDGER-pov`'s `BatchUtxoAccounting` consumer threads sub-transaction state. + `Utxow/Properties/PoV.lagda.md` UTXOW-level wrappers that extract the UTXO derivation from either `UTXOW-normal` or `UTXOW-legacy` (via a shared `UTXOW⇒UTXO` extractor) and delegate to the UTXO-level lemmas. Provides `utxow-pov-invalid` in the exact shape required as a module parameter by `Ledger/Properties/PoV.lagda.md`. Proof-internal notes: + `balance-∪` and `split-balance` are currently module parameters to `Utxo/Properties/PoV` pending the port of Conway Base's balance arithmetic to Dijkstra (see tracking issue). + The 7-term +-commutative-monoid shuffle in `UTXO-V-mechanical` is proved by hand using a `swap-right` helper; this could later be replaced by a call to a commutative-monoid solver. + All three modules typecheck under `--safe`.

Replace the two `coin-of-consumedBatch` / `coin-of-producedBatch` module parameters of `Utxo/Properties/PoV` with direct proofs. The proofs are organised as three layers: + Layer 1 — single-transaction coin equations `coin-producedTx : coin (producedTx t) ≡ cbalance (outs t) + DonationsOf t + getCoin (DirectDepositsOf t)` `coin-consumedTx : coin (MintedValueOf t) ≡ 0 → coin (consumedTx t utxo₀) ≡ cbalance (utxo₀ ∣ SpendInputsOf t) + getCoin (WithdrawalsOf t)` Each is a direct unfolding: repeated `∙-homo-Coin` to distribute `coin` across `+`, followed by `coin∘inject≗id` to strip each `inject`. The consumed version additionally uses `coin (MintedValueOf t) ≡ 0` to cancel the mint term (from UTXO premise p₆ / SUBUTXO premise). + Layer 2 — sum-over-sub-transactions coin equations `coin-∑-producedTx-sub` : pushes `coin` through the `∑ˡ`-indexed sum over `SubTransactionsOf tx` using the new `coin-∑ˡ` lemma (from `Utxo/Properties/Base`), then applies Layer 1 pointwise by list induction. `coin-∑-consumedTx-sub` : same shape, threading a `noMintingSubTxs tx` hypothesis (`∀ stx → stx ∈ˡ SubTransactionsOf tx → coin (MintedValueOf stx) ≡ 0`) through the induction so each element's Layer-1 application has its `noMint` premise available. + Layer 3 — the two batch-level coin equations `coin-of-consumedBatch` and `coin-of-producedBatch`: unfold the outer `+ inject _` / `+ ∑ˡ _` structure of `consumedBatch` / `producedBatch` by repeated `∙-homo-Coin` and `coin∘inject≗id`, substitute the Layer-1 top-level equation for the top-level summand, and substitute the Layer-2 equation for the sub-transaction sum. The produced-side proof ends with a small associative-commutative shuffle (`reshape-top`) that reorders the top-level fields from `(outs + Donations + DirectDeposits) + TxFees` to the stated `outs + TxFees + Donations + DirectDeposits`. The shuffle uses the same `swap-right` helper already used in `UTXO-V-mechanical`. + Supporting change Adds a small helper alias `noMintingSubTxs` at the top of the file to keep the sub-level mint-conservation hypothesis readable in the theorem statements. All proofs typecheck under `--safe`. The `UTXO-pov` placeholder remains; this commit delivers the coin-balance infrastructure that the eventual full proof (and the LEDGER-pov's `BatchUtxoAccounting` consumer) will depend on.

Proves by induction on the SUBLEDGERS transition that the UTxO-state coin total at the start of a sub-tx batch plus all outs + donations equals the UTxO coin total at the end plus all consumed spend inputs (compared against the batch-start snapshot `utxo₀`): ```agda getCoin (UTxOStateOf s₀) + Σ (cbalance (outs stx) + DonationsOf stx) ≡ getCoin (UTxOStateOf s₁) + Σ cbalance (utxo₀ ∣ SpendInputsOf stx) ``` Base case (`BS-base Id-nop`): both sides reduce to `x + 0`, so `refl`. Inductive case: `SUBLEDGER-I` is impossible under `isTopLevelValid ≡ true`; `SUBLEDGER-V` combines the per-step SUBUTXOW balance with the IH via an eight-step +-commutative-monoid rearrangement. Introduces `subutxow-step-coin` as a new module parameter: ```agda getCoin s₀ + cbalance (outs stx) + DonationsOf stx ≡ getCoin s₁ + cbalance (UTxOOf Γ ∣ SpendInputsOf stx) ``` + Rationale for keeping this as a parameter at the SUBLEDGERS level: proving it locally requires, beyond `balance-∪` and `split-balance`, two batch-wide invariants: 1. the running UTxO agrees with `utxo₀` on every sub-tx's spend inputs, and 2. freshness of each sub-tx's TxId relative to the running UTxO neither of which is a local SUBUTXO premise; both follow from batch-wide disjointness exposed by the outer UTXO rule and will be discharged in a follow-up PR dedicated to general Dijkstra PoV infrastructure. Statement parallels the existing `SUBLEDGERS-certs-pov`, uses `SubLedgerEnv.utxo₀ Γ` uniformly on the RHS (matching the shape of `batch-balance-coin`), and is the key lemma needed to derive `batch-utxo-accounting` internally in the next step of this PR.

williamdemeo self-assigned this Apr 14, 2026

williamdemeo marked this pull request as draft April 14, 2026 06:08

williamdemeo force-pushed the 1123-cip-159-11-prove-pov-and-invariants branch 4 times, most recently from 9ad5a26 to e04bad7 Compare April 16, 2026 04:20

williamdemeo added CIP 118 nested transactions CIP 159 Account Address Enhancement property labels Apr 16, 2026

williamdemeo changed the title ~~[Dijkstra] CIP-159-11: Initial PoV property module skeletons (#1123)~~ [Dijkstra] CIP-159-11: PoV property proofs (#1123) Apr 16, 2026

williamdemeo changed the title ~~[Dijkstra] CIP-159-11: PoV property proofs (#1123)~~ WIP [Dijkstra] CIP-159-11: PoV property proofs (#1123) Apr 17, 2026

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

[Dijkstra] CIP-159-11: Prove preservation of value and invariant properties for CIP-159 #1123

Open

8 tasks

williamdemeo force-pushed the 1112-dijkstra-cip-159-master branch from 88b4874 to 4b99a0d Compare April 21, 2026 19:23

williamdemeo force-pushed the 1123-cip-159-11-prove-pov-and-invariants branch from bc16d2d to db63073 Compare April 21, 2026 19:24

williamdemeo force-pushed the 1112-dijkstra-cip-159-master branch from 4b99a0d to d524949 Compare April 22, 2026 15:02

williamdemeo force-pushed the 1123-cip-159-11-prove-pov-and-invariants branch 5 times, most recently from 754b432 to 384db50 Compare April 23, 2026 06:07

williamdemeo force-pushed the 1112-dijkstra-cip-159-master branch 3 times, most recently from 2b2ca4b to 5e3de61 Compare April 29, 2026 00:42

williamdemeo force-pushed the 1123-cip-159-11-prove-pov-and-invariants branch from 384db50 to 364f1e7 Compare April 29, 2026 08:31

williamdemeo force-pushed the 1112-dijkstra-cip-159-master branch from 5e3de61 to 4d0857b Compare April 29, 2026 08:36

williamdemeo force-pushed the 1123-cip-159-11-prove-pov-and-invariants branch from 364f1e7 to ce74043 Compare April 29, 2026 08:44

williamdemeo changed the title ~~WIP [Dijkstra] CIP-159-11: PoV property proofs (#1123)~~ [Dijkstra] CIP-159-11: PoV property proofs (#1123) Apr 29, 2026

williamdemeo marked this pull request as ready for review April 29, 2026 08:45

williamdemeo changed the base branch from 1112-dijkstra-cip-159-master to master April 30, 2026 19:15

williamdemeo changed the base branch from master to 1122-cip-159-10-update-ledger-direct-deps-and-account-bals April 30, 2026 19:15

williamdemeo force-pushed the 1122-cip-159-10-update-ledger-direct-deps-and-account-bals branch 3 times, most recently from cc27e6c to 93423f0 Compare May 6, 2026 03:57

williamdemeo added 10 commits May 5, 2026 22:05

indexedSumᵛ'-∪ and sumConstZero have proofs!

840e812

There were unresolved proof obligations from Conway.

williamdemeo force-pushed the 1123-cip-159-11-prove-pov-and-invariants branch from ce74043 to 4b6470e Compare May 6, 2026 04:05

williamdemeo marked this pull request as draft May 7, 2026 07:43

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

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

[Dijkstra] CIP-159-11: PoV property proofs (#1123)#1169
williamdemeo wants to merge 10 commits into1122-cip-159-10-update-ledger-direct-deps-and-account-balsfrom
1123-cip-159-11-prove-pov-and-invariants

williamdemeo commented Apr 14, 2026 •

edited

Loading

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

1 participant

Conversation

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

Uh oh!

Description

Summary

Modules

UTXO / UTXOW PoV — what's proved

CERTS PoV — design notes

LEDGER PoV — design notes

What's left (deferred to follow-ups)

Checklist

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

1 participant

williamdemeo commented Apr 14, 2026 •

edited

Loading