Description

Update: LEDGER-pov planning (post-ENTITIES)

The existing LEDGER-pov proof in PR #1190 is essentially the right shape for the post-ENTITIES world: it's already organized top-down around the LEDGER-V equational chain, with CERTS-pov called only where the chain demands it. The migration to ENTITIES will be roughly as follows:

1. Add HasCoin-LedgerState and coinFromDeposits (preliminary; missing from master).
2. Replace every appearance of CERTS-pov with a new ENTITIES-pov of the same statement shape.
3. Prove ENTITIES-pov once, by case-splitting on the single ENTITIES constructor and chaining applyWithdrawals-pov → CERTS-pov-rtc → applyDirectDeposits-pov.
4. Carry the rest of [Dijkstra] (DEPRECATED) CIP-159-11c: Prove LEDGER PoV #1190 through essentially verbatim, retargeting the certStep premise types from ,CERTS⦈ to ,ENTITIES⦈.

What we drop from #1188: the composite CERTS-pov for RunTraceAfterAndThen PRE-CERT CERT POST-CERT, plus the now-orphan
PRE-CERT-pov / POST-CERT-pov lemmas. We keep the genuinely reusable machinery (applyWithdrawals-pov and its applyOne-pov / foldl-applyOne-pov stack, CERT-pov).

Preliminary work (not in master)

These are needed before the LEDGER-pov statement typechecks. Best added to Ledger.lagda.md directly (or to a small adjacent module so the PoV proof can open them without touching Ledger.lagda.md).

-- Promote the where-bound helper inside `calculateDepositsChange` to top level
coinFromDeposits : CertState → Coin
coinFromDeposits cs =
    getCoin (DepositsOf (DStateOf cs))
  + getCoin (DepositsOf (PStateOf cs))
  + getCoin (DepositsOf (GStateOf cs))

instance
  HasCoin-LedgerState : HasCoin LedgerState
  HasCoin-LedgerState .getCoin s =
      getCoin (UTxOStateOf s)
    + rewardsBalance (DStateOf (CertStateOf s))
    + coinFromDeposits (CertStateOf s)

Rationale. LedgerState holds three coin-bearing components: UTxO state (includes fees/donations via existing HasCoin-UTxOState), the rewards balance in DState.rewards, and the three deposit pots (stake-key, pool, DRep). Existing HasCoin-CertState only counts the rewards balance; the deposit pots have to be added on at the LedgerState level to make the LEDGER-pov equation balance.

Original Issue 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.