[Dijkstra] LEDGER PoV

[williamdemeo]

Description

Parent issue: #1123

Sub-issues: #1185 (Certs PoV), #1186 (UTxO/UTxOW PoV)

This issue proves the top-level LEDGER-pov theorem for the Dijkstra era — the headline preservation-of-value property for CIP-159 — and identifies exactly which lower-level lemmas it depends on. Those dependencies are discharged in #1185 (Certs side) and #1186 (UTxO/UTxOW side).

Theorem

For a LEDGER step Γ ⊢ s ⇀⦇ tx ,LEDGER⦈ s', getCoin s ≡ getCoin s'.

This is stronger than per-rule PoV: sub-transactions in a CIP-159 batch can individually move value between the UTxO side and the CertState side without locally balancing, so the proof reasons about the entire LEDGER-V step as a single equational chain.

The invalid case (LEDGER-I) is straightforward: certState and govSt are unchanged, SUBLEDGERS is a no-op, and only the UTXOW step affects getCoin, which it preserves via utxow-pov-invalid (sub-issue #1186).

What LEDGER-pov needs from the lower layers

The proof's only references to the lower-level PoV machinery are:

• from Certs.Properties.PoV: the single theorem CERTS-pov (the symmetric "consumed equals produced" equation for the CERTS rule, balancing direct deposits against withdrawals);
• from Utxow.Properties.PoV: UTXOW-batch-balance-coin, UTXOW-V-mechanical, and utxow-pov-invalid.

Sub-issues #1185 and #1186 are scoped exactly to deliver those. Anything else in the lower layers is supporting infrastructure for these three named obligations; nothing in #1185 or #1186 is independent of LEDGER-pov's requirements.

Helpers proved in this PR

• SUBLEDGERS-certs-pov. Induction over the SUBLEDGERS reflexive-transitive closure, composing per-sub-transaction CERTS-pov invocations into the batch-wide "rewards balance before plus direct deposits equals rewards balance after plus withdrawals" equation.
• SUBLEDGERS-utxo-coin. Parallel induction tracking getCoin (UTxOStateOf _) through the SUBLEDGERS chain via a per-step SUBUTXOW coin equation.
• The LEDGER-V arithmetic chain. Composes the four key equations (batch UTxO balance, combined CERTS-pov, deposit accounting, mechanical UTxO tracking) into the main statement.

Module parameters (deferred to follow-up)

The following are taken as module parameters with proof sketches in comments. Each will be discharged in a small follow-up; none of them are CIP-159-specific or blocked by the agda-sets library:

• subutxow-step-coin. Per-step SUBUTXOW coin equation. Beyond the era-independent balance-∪/split-balance lemmas, requires a batch-wide "spend inputs preserved" invariant and freshness of each sub-tx's TxId relative to the running UTxO.
• utxo₁-tx-spend-eq and fresh-top-tx-id. 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 the batch level but doesn't expose per-step.
• posNeg-deposits. Deposit-change posPart/negPart identity. Provable from the definition of calculateDepositsChange and the standard y + posPart (x − y) ≡ x + negPart (x − y) lemma (per-component, then composed across top and sub).
• balance-∪, split-balance. Era-independent UTxO-balance arithmetic; the Conway versions don't transport because Dijkstra defines balance over ℙ Value rather than a finite map. Port deferred.

Acceptance criteria

• Ledger.Properties.PoV proves LEDGER-pov for both LEDGER-V and LEDGER-I (modulo the module parameters listed above).
• The proof invokes only CERTS-pov from the Certs layer and only UTXOW-batch-balance-coin / UTXOW-V-mechanical / utxow-pov-invalid from the Utxo/Utxow layer.
• Module compiles with --safe.

References

• Conway analogue: Ledger.Conway.Specification.Ledger.Properties.PoV.
• LEDGER-V / LEDGER-I definitions: src/Ledger/Dijkstra/Specification/Ledger.lagda.md.
• calculateDepositsChange: same module.
• CIP-159 PR Change the type of DirectDeposits to have RewardAddress as its domain #1197 (DirectDeposits keyed by RewardAddress, applyToRewards factoring) is a dependency of all three sub-issues.