[Dijkstra] LEDGER-pov: complete the proof — gov re-derivation; Certs/Utxo/Utxow facts as parameters

[williamdemeo]

Description

Follow-up into 1187-dijkstra-NEW-ENTITIES-ledger-pov (the lead PR #1203), completing the top-down LEDGER-pov plan from the Ledger/Properties/PoV.lagda.md resume note: prove LEDGER-pov in full, leaving the Certs / Utxo / Utxow PoV facts as module-parameter stubs (discharged later by #1210 and the utxo/utxow-pov work, #1186).

Ledger/Properties/PoV.lagda.md now typechecks end-to-end — Agda 2.8.0 via the project Nix flake, --safe, no postulates or holes, clean recompile.

1 — Remove the Certs-PoV providers; lift CERTS-pov to a parameter

• Delete Certs/Properties/PoV.lagda.md and Certs/Properties/PoVLemmas.lagda.md.
• Drop their imports from Certs/Properties.lagda.md (keep Computational).
• Add CERTS-pov as a parameter of ENTITIES-PoV (Entities/Properties/PoV.lagda.md) and of LEDGER-PoV, threaded into the open ENTITIES-PoV … instantiation, alongside the CERTS-coinFromDeposits-updateCertDeposits parameter (closed-form cert-deposit coin equation WIP -- [Dijkstra] CIP-159-11a: Certs PoV (per-step coin bridge + RTC lift) (#1185) #1210 provides).

2 — Complete the LEDGER-pov proof

getCoin on a LedgerState has four summands: UTxO coin, rewards balance, the cert-deposit pots (coinFromDeposits), and the gov-action deposits (coinFromGovDeposit (GovStateOf s), post-#1214). The LEDGER-V chain proves the full four-summand goal getCoin s ≡ getCoin s' where G' = coinFromGovDeposit (rmOrphanDRepVotes cs₂ govSt₂):

• coinFromDeposit → coinFromDeposits (spec rename); local deposit-change interface (DepositsChange, calculateDepositsChange, the DepositsChange{Top,Sub}Of projections) and posPart-negPart-sym.
• Gov summand (the re-derivation). UTXOW-batch-balance-coin is the coin projection of the spec's consumedBatch ≡ producedBatch premise, with the produced-side govProposalsDeposits (top + per-sub) collected into a single trailing totGov. + totGov is threaded through bat' → LHS+E≡RHS+E → step-ii (a mid-extract lemma pulls it out of the middle; the existing arithmetic runs under cong (_+ totGov)), giving three-summand : U₀+R₀+D₀ ≡ U₂+R₂+D₂+totGov. A new SUBLEDGERS-gov-coin induction (over the sub-tx GOVS steps) + GOVS-coinFromGovDeposit (top GOVS step, via a small proposalsOf bridge) + rmOrphanDRepVotes-coinFromGovDeposit give gov-acc : totGov + G₀ ≡ G'. The body assembles the two.

The Utxo/Utxow-PoV facts — utxow-pov-invalid, UTXOW-V-mechanical, UTXOW-batch-balance-coin, and the UTxO algebra (balance-∪, split-balance, subutxow-step-coin, utxo₁-tx-spend-eq, fresh-top-tx-id, …) — remain module parameters, the interface to be discharged by #1186 (…NEW-ENTITIES-utxo-utxow-pov). UTXOW-batch-balance-coin is stated as the coin projection of the spec's batch-balance premise, so its discharge there is direct.

Conway-side touches (resume-note item 7)

The Conway changes already on #1203 (Conway/Conformance/Properties, the Conway Certs/Ledger PoV files, Conway/…/GenMinSpend) are a Conway-internal refactor that drops now-provable assumption parameters made redundant by the Ledger.Prelude hoist; none reference Dijkstra code, and part of that hoist (sum-map-+) is used by the LEDGER-pov chain. They are therefore not "only needed for the removed modules", so they are kept (reverting would cascade into the Prelude hoist for no correctness gain).

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

https://claude.ai/code/session_01We2YdXX2ozJAdAbCrRwi6r

---

Generated by Claude Code

[Copilot]

Pull request overview

This PR completes the Dijkstra-era LEDGER-pov preservation-of-value proof in Ledger/Properties/PoV.lagda.md while intentionally leaving Certs / UTxO / UTxOW PoV facts as module-parameter stubs to be discharged by follow-up work (#1210, #1186). It also removes the Dijkstra Certs PoV provider modules and threads CERTS-pov as a parameter through ENTITIES-PoV into LEDGER-PoV.

Changes:

• Finalize the LEDGER-pov equational chain for the 4-summand getCoin (UTxO + rewards + cert deposits + gov deposits), including a new SUBLEDGERS-gov-coin induction and gov-deposit accounting wiring.
• Remove Dijkstra Certs.Properties.PoV / Certs.Properties.PoVLemmas modules and lift CERTS-pov (and the closed-form coinFromDeposits bridge) into parameters.
• Minor documentation/wording adjustment in Utxo.lagda.md to reflect the Certs-level PoV usage of hoisted helpers.

Reviewed changes

Copilot reviewed 6 out of 6 changed files in this pull request and generated no comments.

Show a summary per file

File	Description
src/Ledger/Dijkstra/Specification/Utxo.lagda.md	Updates narrative text about hoisted cert-deposit helpers and their downstream use.
src/Ledger/Dijkstra/Specification/Ledger/Properties/PoV.lagda.md	Completes LEDGER-pov proof end-to-end, adds gov-deposit accounting and threads Certs/UTxO/UTxOW facts as parameters.
src/Ledger/Dijkstra/Specification/Entities/Properties/PoV.lagda.md	Removes dependency on Dijkstra Certs PoV module; adds CERTS-pov as a module parameter.
src/Ledger/Dijkstra/Specification/Certs/Properties/PoVLemmas.lagda.md	Deleted (Certs PoV provider removed per top-down plan).
src/Ledger/Dijkstra/Specification/Certs/Properties/PoV.lagda.md	Deleted (Certs PoV provider removed per top-down plan).
src/Ledger/Dijkstra/Specification/Certs/Properties.lagda.md	Stops re-exporting the deleted PoV modules; keeps Computational.

---

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