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

[williamdemeo]

Description

Closes #1187.

This PR proves the top-level LEDGER-pov theorem for the Dijkstra era, building on the Certs and Utxo/Utxow PoV machinery from PRs #<new-A> and #<new-B>. It is the third of three replacing the original PR #1169.

It targets the branch of PR #<new-B> so that CI sees the full PoV chain in order; once #<new-B> merges, this PR will be retargeted to master.

---

Module

Module	Purpose	Status
Ledger.Properties.PoV	HasCoin instances and LEDGER-pov	Proved (modulo module parameters)

---

Design notes

Why the proof reasons about LEDGER-V as a single step

The Dijkstra LEDGER-pov proof does not decompose into independent SUBLEDGERS-pov and UTXOW-pov pieces, because (i) individual SUBUTXO rules have no balance equation — only the batch-level consumedBatch ≡ producedBatch (in UTXO) constrains the total — and (ii) sub-transactions may individually transfer value between UTxO and CertState (via sub-withdrawals, sub-deposits, sub-direct-deposits) without local balancing. Instead, the proof reasons about the entire LEDGER-V step at once.

applyDirectDeposits cancellation is the main new challenge

In LEDGER-V, certStateFinal = certStateWithDDeps tx certState₂ = record certState₂ { dState = applyDirectDeposits (DirectDepositsOf tx) (DStateOf certState₂) }. Direct deposit value appears in producedBatch (UTxO side) and in certStateFinal (CertState side), so it cancels in the total. The proof is an equational chain combining SUBLEDGERS-certs-pov, top-level CERTS-pov, the batch-UTxO-accounting step, and the applyDirectDeposits-rewardsBalance identity. Per-transaction direct deposit application (PR #1161) makes this slightly cleaner than batch-wide application would have been, because each transaction's direct-deposit total appears next to its own producedTx term in producedBatch, mirrored by its own certStateWithDDeps step.

Helpers proved here

• SUBLEDGERS-certs-pov — induction over the SUBLEDGERS reflexive-transitive closure, composing per-sub-transaction CERTS-pov invocations.
• SUBLEDGERS-utxo-coin — parallel induction tracking getCoin (UTxOStateOf _) through the SUBLEDGERS chain via the per-step SUBUTXOW coin equation.
• LEDGER-pov — both LEDGER-V and LEDGER-I cases.

The LEDGER-I case 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 (from PR #<new-B>).

---

Outstanding proof obligations

The following are stated as module parameters of Ledger.Properties.PoV, with detailed proof sketches in comments. Each will be discharged in a follow-up; the dependencies are now in place.

CIP-159–specific or Dijkstra-specific:

• applyDirectDeposits-rewardsBalance — should follow from ∪⁺ properties.
• subutxow-step-coin — per-step SUBUTXOW coin equation. 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 does not expose per-step.

Era-independent (can be discharged in a small standalone follow-up):

• 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.
• DD-split — aggregation identity for allDirectDeposits. Provable once we confirm allDirectDeposits sums top-level and sub-level direct deposits disjointly.
• sum-map-+ — standard list algebra.

The shared parameters (balance-∪, split-balance, outs-disjoint, noMintTx, noMintSubTx, ∪ˡ-res-lookup-preserve, sum-map-proj₂≡getCoin, setToList-Unique) are the same ones already taken as parameters in PRs #<new-A> and #<new-B>; they are threaded through here.

The invariant properties from §§3–6 of the parent issue #1123 (phantom asset, non-negative balance, direct-deposit registration, balance-interval satisfaction) are mostly straightforward consequences of UTXO-Premises conjuncts and are deferred to a follow-up.

---

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