[Dijkstra] Certs PoV

[williamdemeo]

Description

Parent issue: #1187 (LEDGER PoV)

Builds on: #1203 (the LEDGER-PoV contract), #1250 (explicit-deposit certificates / newCertDeposits)

This issue discharges the five Certs-side module parameters of the LEDGER-PoV contract (the parameter block of module LEDGER-PoV in src/Ledger/Dijkstra/Specification/Ledger/Properties/PoV.lagda.md, frozen by #1203) as theorems, with statements matching the contract verbatim.

Implementation: PR #1210 (stacked on #1203's branch; retarget to master once #1203 merges).

The five target statements

All vocabulary from Ledger.Dijkstra.Specification.Certs:

• CERTS-rewards-pov — a CERTS run preserves the rewards balance:
  Γ ⊢ s ⇀⦇ dCerts ,CERTS⦈ s' → coinFromRewards s ≡ coinFromRewards s'
• CERTS-deposits-pov — closed-form deposit accounting, under PoolDepositsRegistered s:
  coinFromDeposits s + newCertDeposits (PParamsOf Γ) (dom (PoolsOf s)) dCerts ≡ coinFromDeposits s' + refundCertDeposits (PParamsOf Γ) dCerts
• CERTS-deposits-registered — a CERTS run preserves PoolDepositsRegistered.
• CERTS-new-thread — newCertDeposits over an appended certificate list splits at a CERTS-run boundary, the second half charged against the run's final pool set (what lets per-step accounting compose across a batch).
• refundCertDeposits-++ — refundCertDeposits distributes over _++_.

Decomposition

In Dijkstra, CERTS is a plain reflexive–transitive closure of the single-certificate rule CERT — the withdrawal and direct-deposit handling formerly attached to the Conway-era CERTS (the old PRE-CERT/POST-CERT phases) lives at the ENTITIES layer and is proved inside #1203 (Entities.Properties.{PoV,ApplyToRewardsPoV}). So each fact is an induction over the closure whose step case is a per-CERT lemma, plus fold algebra for the deposit folds:

• Per-step accounting — case split over the eight DELEG/POOL/GOVCERT rules. _∪⁺_ additions add their deposit to the pot total (getCoin-∪⁺-singleton, new in Ledger.Prelude); removals split off the entry whose value the rule's membership premise pins down (getCoin-remove); POOL-reg adds through a left-biased union, so it needs the key fresh in the pot — the rule's premise gives freshness in pools, and PoolDepositsRegistered transports it to the pot. That is the invariant's only use, and it is preserved because POOL-reg extends pot and pool map by the same key.
• Pool-set threading — newCertDeposits folds a pair accumulator (coin so far, pool keys registered so far); nextPools/CERT-poolSet identify the accumulator's evolution with dom (PoolsOf -) across a CERT step, up to ≡ᵉ, absorbed by a congruence lemma (the fold consumes the set only through membership tests). Since the fold's per-step function is local to Certs, the fold lemmas reach it through newCertDeposits itself via seed certificates (a fold state (d , P) is definitionally the fold from (0 , P) over one delegate/regdrep certificate carrying deposit d).

Modules

Module	Purpose
Certs.Properties.PoVLemmas	per-CERT-step lemmas (CERT-rewards-pov, CERT-deposits-pov, CERT-deposits-registered, CERT-poolSet) and fold lemmas (newCertDeposits-∷/-cong, shift lemmas, refundCertDeposits-++)
Certs.Properties.PoV	the five CERTS-level facts, statements matching the LEDGER-PoV parameters verbatim
Ledger.Prelude (additions)	getCoin-∪⁺-singleton, getCoin-remove, dom-∪ˡ-singleton and supporting ∪⁺ lemmas

Acceptance criteria

• All five LEDGER-PoV Certs-side parameters are provable by direct substitution (statements verbatim); verified by a drop-in instantiation of LEDGER-PoV.
• Everything compiles under --safe, with no deferred module parameters on the Certs side.
• Both property modules are registered in Certs.Properties (reachable from the Ledger.Dijkstra root).
• Follow-up (out of scope here): the mechanical rewiring of Ledger.Properties.PoV to open these proofs in place of its parameters — the Certs analogue of [Dijkstra] Rewire LEDGER-pov to consume the proved PoV modules and drop the discharged parameters #1277.

References

• The contract: module LEDGER-PoV parameters in src/Ledger/Dijkstra/Specification/Ledger/Properties/PoV.lagda.md ([Dijkstra] CIP-159-11c: Prove LEDGER preservation of value (#1187) #1203).
• The consumer: Entities.Properties.PoV (module ENTITIES-PoV, inside [Dijkstra] CIP-159-11c: Prove LEDGER preservation of value (#1187) #1203).
• Deposit folds and PoolDepositsRegistered: src/Ledger/Dijkstra/Specification/Certs.lagda.md ([Dijkstra] Explicit deposits in certificate deregistration #1250).
• Sibling UTxO-side issue/PR: [Dijkstra] UTxO and UTxOW PoV #1186 / [Dijkstra] CIP-159-11b: Prove UTxO and UTxOW preservation of value (#1186) #1189.

---

History (2026-08-05): this body was rewritten. The previous version predated #1250 and #1203's contract restatement: it targeted a single CERTS-pov lemma with the withdrawal/direct-deposit flows attached to CERTS and an applyToRewards fold decomposition — that machinery now lives at the ENTITIES layer inside #1203, and the three agda-sets bridging assumptions it listed are the ApplyToRewards-PoV parameters there, no longer in this issue's scope.