[Dijkstra] Certs PoV

[williamdemeo]

Description

Parent issue: #1187 (LEDGER PoV)

Depends on: #1116, #1197 (CIP-159 DirectDeposits keyed by RewardAddress)

This issue discharges the single Certs-level lemma that LEDGER-pov (#1187) calls out by name: CERTS-pov.

Theorem

For a CERTS step Γ ⊢ s₁ ⇀⦇ l ,CERTS⦈ sₙ, under the network-id integrity premises and the deposit-membership premise carried by the rule:
getCoin s₁ + getCoin (DirectDepositsOf Γ) ≡ getCoin sₙ + getCoin (WithdrawalsOf Γ)
This is the symmetric "consumed equals produced" form: withdrawals (consumed-side) and direct deposits (produced-side) balance the rewards-balance change. CIP-159 introduces both partial withdrawals (PR #1116) and the new applyToRewards fold for direct deposits and withdrawals (PR #1197); the proof composes their two parallel "applyToRewards is value-preserving up to the total amount" lemmas.

What CERTS-pov needs and how it decomposes

• PRE-CERT-pov. Reduces to applyWithdrawals-pov.
• sts-pov. Reduces to CERT-pov (preservation) on each intermediate step and POST-CERT-pov at the end.
• POST-CERT-pov. Reduces to applyDirectDeposits-pov.
• CERT-pov. Same as the Conway version (Dijkstra's value-relevant CERT rules are unchanged).

The two applyToRewards lemmas (applyWithdrawals-pov, applyDirectDeposits-pov) share a common fold-induction skeleton parameterised over the per-step operation (_∸_ for withdrawals, _+_ for direct deposits). Both follow the same three layers used in the Conway analogue: single-step decomposition (applyOne-pov{,-add}), fold induction (foldl-applyOne-pov{,-add}), and top-level (applyWithdrawals-pov/applyDirectDeposits-pov).

Module parameters

Three agda-sets-API bridging assumptions remain as module parameters of Certs.Properties.ApplyWithdrawalsPoV:

• ∪ˡ-res-lookup-preserve. Lookup in a left-biased union with a singleton-overwrite preserves values at other keys.
• sum-map-proj₂≡getCoin. getCoin representation as a list sum over setToList.
• setToList-Unique. Uniqueness of credentials in setToList (m ˢ) for m : RewardAddress ⇀ Coin under the network-id constraint (follows from injectivity of stake on dom m).

These are deferred to keep this issue focused on the new fold-induction infrastructure. None of them depend on CIP-159; all three are pure agda-sets API gaps.

Modules introduced

Module	Purpose
Certs.Properties.ApplyWithdrawalsPoV	getCoin-∪ˡ-overwrite bridge, applyOne-pov{,-add}, foldl-applyOne-pov{,-add}, applyWithdrawals-pov, applyDirectDeposits-pov
Certs.Properties.PoVLemmas	CERT-pov, POST-CERT-pov, sts-pov, PRE-CERT-pov
Certs.Properties.PoV	CERTS-pov

(The file name ApplyWithdrawalsPoV.lagda.md is retained for now; it will be renamed to ApplyToRewardsPoV.lagda.md in a small follow-up since the module now houses both directions.)

Acceptance criteria

• CERTS-pov is exposed to LEDGER-pov ([Dijkstra] LEDGER PoV #1187) under its post-Change the type of DirectDeposits to have RewardAddress as its domain #1197 signature: two NetworkId integrity premises (one for withdrawals, one for direct deposits) and one deposit-membership premise.
• All three modules compile with --safe.
• No use of ∪⁺ reasoning in the PoV chain (post-Change the type of DirectDeposits to have RewardAddress as its domain #1197, POST-CERT-pov goes through applyDirectDeposits-pov, not indexedSumᵛ'-∪⁺).

References

• Conway analogue: Ledger.Conway.Specification.Certs.Properties.{PoV,PoVLemmas}.
• CIP-159 partial withdrawals: [Dijkstra] CIP-159-04: Update certificate rules for partial withdrawals #1116.
• CIP-159 DirectDeposits retyping + applyToRewards: PR Change the type of DirectDeposits to have RewardAddress as its domain #1197.
• applyToRewards, applyWithdrawals, applyDirectDeposits definitions: src/Ledger/Dijkstra/Specification/Certs.lagda.md.