[Dijkstra] (DEPRECATED) CIP-159-11a: Prove Certs preservation of value (#1185) by williamdemeo · Pull Request #1188 · IntersectMBO/formal-ledger-specifications

williamdemeo · 2026-05-07T19:47:52Z

DEPRECATED. This PR was based on CERT-Post and CERT-Pre setup. It is superseded by #1210 which is based on the ENTITIES approach.

Description

Closes #1185.

This PR adds the preservation-of-value (PoV) proofs for the Dijkstra Certs rules. The Conway CERTS-pov proves getCoin s₁ ≡ getCoin sₙ + getCoin (WithdrawalsOf Γ) assuming full withdrawals; CIP-159 introduces partial withdrawals (#1116), so the equation still holds — getCoin (WithdrawalsOf Γ) is the actual amount withdrawn — but the underlying PRE-CERT rule changes from constMap-based zeroing to fold-based subtraction, requiring a new applyWithdrawals-pov lemma.

This PR is the first of three replacing the original PR #1169, which has been split along module-tree boundaries. It contains only the Certs/Properties sub-tree.

Modules

Module	Purpose	Status
`Certs.Properties.ApplyWithdrawalsPoV`	`applyWithdrawals-pov` (top-level) plus `applyOne-pov` / `foldl-applyOne-pov` building blocks	Proved (modulo three module parameters)
`Certs.Properties.PoVLemmas`	`CERT-pov`, `POST-CERT-pov`, `sts-pov`, `PRE-CERT-pov`	Proved
`Certs.Properties.PoV`	`CERTS-pov` top-level theorem	Proved

Design notes

`PRE-CERT-pov` uses `applyWithdrawals-pov` instead of Conway's `constMap` chain

Conway's PRE-CERT zeros out withdrawn credentials via constMap wdrlCreds 0 ∪ˡ rewards, and the PoV proof decomposes the rewards map into restricted/complement parts, showing the zeroing removes exactly getCoin wdrls.

Dijkstra's PRE-CERT uses applyWithdrawals wdrls rewards (CIP-159 partial withdrawals), which subtracts each withdrawal amount. The PoV equation getCoin s ≡ getCoin s' + getCoin wdrls still holds, but the proof requires a new lemma — applyWithdrawals-pov — based on fold induction rather than map decomposition.

`applyWithdrawals-pov` is structured as three layers

Single step (applyOne-pov). Decomposes the accumulator into complement + restriction, shows the per-step decrease equals amt using m∸n+n≡m.
Fold induction (foldl-applyOne-pov). Induction over setToList (wdrls ˢ), maintaining an invariant that remaining entries have registered credentials with bounded balances. Relies on Unique (from stake injectivity, which follows from the per-batch NetworkId constraint).
Top-level (applyWithdrawals-pov). Instantiates the fold with the withdrawal map's list representation.

`CERT-pov`, `POST-CERT-pov`, `sts-pov` are essentially unchanged from Conway

The Dijkstra DELEG-delegate and DELEG-dereg constructors have the same value-relevant structure (adding/removing zero-balance entries), and POST-CERT still only filters voteDelegs. CERT-pov is missing the CERT-vdel case because Dijkstra has only CERT-deleg, CERT-pool, CERT-gov.

Outstanding proof obligations

Three lemmas are stated as module parameters with detailed proof sketches in comments. Each is provable from the existing agda-sets / Withdrawals machinery; they are kept as parameters here to keep this PR focused on the new fold-induction infrastructure.

∪ˡ-res-lookup-preserve — for any c' ≠ c, lookup in ❴ c , v ❵ ∪ˡ (m ∣ ❴ c ❵ ᶜ) agrees with lookup in m. Painful to thread through agda-sets ⁇ instance resolution.
sum-map-proj₂≡getCoin — getCoin representation of a withdrawal map's coin sum.
setToList-Unique — Unique on map (stake ∘ proj₁) (setToList (wdrls ˢ)). Follows from stake injectivity, which holds because the per-batch NetworkId constraint forces all withdrawals to share the same net.

These will be discharged in a follow-up; the relevant tracking has been added to issue #1185.

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

Copilot

Pull request overview

This PR adds the Dijkstra-era CERTS preservation-of-value (PoV) proof stack (including the new fold-based applyWithdrawals PoV lemma needed for CIP-159 partial withdrawals), and refactors/shared some generic getCoin/set-theory lemmas into Ledger.Prelude so Conway/Dijkstra PoV code can reuse them.

Changes:

Introduces new Dijkstra Certs.Properties PoV modules (ApplyWithdrawalsPoV, PoVLemmas, PoV) and wires them into the subtree aggregator.
Extends Ledger.Prelude with reusable getCoin/indexedSum lemmas (singleton/union/congruence, sumConstZero, setToList-∈).
Moves/centralizes HasDirectDeposits (removed from Transaction, now defined alongside account types) and updates related instances/usages; minor Conway PoV cleanups to rely on Prelude lemmas.

Reviewed changes

Copilot reviewed 13 out of 13 changed files in this pull request and generated 5 comments.

Show a summary per file

File	Description
src/Ledger/Prelude.lagda.md	Adds reusable `getCoin`/`indexedSum` helper lemmas (singleton/union/congruence, `sumConstZero`, `setToList-∈`).
src/Ledger/Dijkstra/Specification/Transaction.lagda.md	Removes the local `HasDirectDeposits` record (keeps instances), relying on the Account-level definition.
src/Ledger/Dijkstra/Specification/Certs/Properties/PoVLemmas.lagda.md	New Dijkstra CERTS PoV lemma module (parameterized, CIP-159-aware).
src/Ledger/Dijkstra/Specification/Certs/Properties/PoV.lagda.md	New Dijkstra top-level `CERTS-pov` theorem (accounts for withdrawals and direct deposits).
src/Ledger/Dijkstra/Specification/Certs/Properties/ApplyWithdrawalsPoV.lagda.md	New fold-induction infrastructure for `applyWithdrawals-pov` (parameterized by a few deferred lemmas).
src/Ledger/Dijkstra/Specification/Certs/Properties.lagda.md	Imports/exports the new PoV modules in the Certs properties subtree.
src/Ledger/Dijkstra/Specification/Certs.lagda.md	Refactors `applyWithdrawals` by lifting `applyOne`; adds `HasDirectDeposits` instance for `CertEnv`; uses type aliases `Retiring`/`CCHotKeys`.
src/Ledger/Dijkstra/Specification/Account.lagda.md	Introduces `HasDirectDeposits` alongside `DirectDeposits` (so it can be shared/re-exported).
src/Ledger/Conway/Specification/Utxo/Properties/GenMinSpend.lagda.md	Switches to Prelude’s `getCoin-singleton` lemma (removes local duplicate).
src/Ledger/Conway/Specification/Ledger/Properties/PoV.lagda.md	Simplifies parameters by relying on `Certs-PoV` with fewer assumptions.
src/Ledger/Conway/Specification/Certs/Properties/PoVLemmas.lagda.md	Removes duplicated helper lemmas/import tweaks; relies on Prelude-provided helpers.
src/Ledger/Conway/Specification/Certs/Properties/PoV.lagda.md	Simplifies `Certs-PoV` module parameters to match the updated lemma structure.
src/Ledger/Conway/Conformance/Properties.lagda.md	Drops an unused/removed `indexedSum-∪⁺-hom` parameter from a local module.

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

+In Dijkstra, the `CERTS`{.AgdaDatatype} rule processes withdrawals (via
+`PRE-CERT`{.AgdaDatatype}) and direct deposits (via `POST-CERT`{.AgdaDatatype})
+in addition to the certificate steps.  Withdrawals reduce the rewards balance;
+direct deposits increase it; the preservation-of-value equation is a symmetric
+"consumed equals produced" statement:
+
+`getCoin s₁ + getCoin (CertEnv.directDeposits Γ) ≡ getCoin sₙ + getCoin (WithdrawalsOf Γ)`.
+
+Equivalently, the *increase* in rewards balance from `s₁`{.AgdaBound} to
+`sₙ`{.AgdaBound} equals `directDeposits − withdrawals`.
+
+```agda
+  CERTS-pov : {Γ : CertEnv} {s₁ sₙ : CertState}
+    → ∀[ a ∈ dom (WithdrawalsOf Γ) ] NetworkIdOf a ≡ NetworkId
+    → Γ ⊢ s₁ ⇀⦇ l ,CERTS⦈ sₙ
+    → getCoin s₁ + getCoin (DirectDepositsOf Γ) ≡ getCoin sₙ + getCoin (WithdrawalsOf Γ)
+```


Copilot

Pull request overview

Copilot reviewed 13 out of 13 changed files in this pull request and generated 1 comment.

+  res-decomp m m' = ∪-cong (≡ᵉ.refl {x = m ˢ}) (≡ᵉ.sym (filterᵐ-idem {m = m'}))
+    where module ≡ᵉ = IsEquivalence (≡ᵉ-isEquivalence {A × Coin})


…CIP-159) After direct-deposit application moved from LEDGER-V/SUBLEDGER-V into the POST-CERT rule, the Certs preservation-of-value proofs needed to account for the `getCoin (DirectDepositsOf Γ)` increase that POST-CERT now produces via `rewards ∪⁺ directDeposits`. Statement changes: - POST-CERT-pov: getCoin s ≡ getCoin s' → getCoin s + getCoin (DirectDepositsOf Γ) ≡ getCoin s' - sts-pov: gains a `+ getCoin (DirectDepositsOf Γ)` term on the LHS - CERTS-pov: becomes the symmetric "consumed = produced" form getCoin s₁ + getCoin (DirectDepositsOf Γ) ≡ getCoin sₙ + getCoin (WithdrawalsOf Γ) Structural changes: - POST-CERT-pov and sts-pov move into the parameterized `Certs-Pov-lemmas` sub-module (alongside PRE-CERT-pov), since they now require a fourth module parameter: indexedSumᵛ'-∪⁺ : ∀ (m m' : Rewards) → getCoin (m ∪⁺ m') ≡ getCoin m + getCoin m' This is the natural ∪⁺ analogue of the existing `indexedSumᵛ'-∪` lemma for `∪ˡ` on disjoint domains, but unconditional because `∪⁺` adds (rather than drops) values at shared keys. TODO: upstream to agda-sets. - `Certs-PoV` (in PoV.lagda.md) gains the same parameter and forwards it. CERT-pov and PRE-CERT-pov are unchanged: the CERT and PRE-CERT rules did not change in this refactor. Closes part of #1185.

Following the merge of CIP-159 PR #1197 (DirectDeposits keyed by RewardAddress; applyDirectDeposits and applyWithdrawals refactored through a shared applyToRewards fold) and the agda-sets cleanup PR #1196 (Conway Equivalence.Map utilities moved into Ledger.Prelude), this commit updates the Dijkstra CERTS preservation-of-value proofs to compile against the new APIs. Main changes: + Rename `ApplyWithdrawals-PoV` sub-module to `ApplyToRewards-PoV`, since it now houses lemmas for both withdrawals and direct deposits. + Add `getCoin-∪ˡ-overwrite` bridge lemma: `getCoin (❴ c , v ❵ ∪ˡ acc) ≡ v + getCoin (acc ∣ ❴ c ❵ ᶜ)`. Encapsulates the listing-vs-replacement reconciliation between the new `❴ k , v ❵ ∪ˡ acc` form (used by `applyToRewards`) and the equivalent complement-restricted form used by the existing decomposition reasoning. + Factor `split-by-lookup` as a top-level lemma decomposing `getCoin acc` along a known lookup result. Used by both `applyOne-pov` (subtraction) and the new `applyOne-pov-add` (addition). + Add the additive parallel: `applyOne-pov-add`, `foldl-applyOne-pov-add`, and `applyDirectDeposits-pov`. Mirrors the existing withdrawal chain, sharing `getCoin-∪ˡ-overwrite` and `split-by-lookup`. + Strengthen the `setToList-Unique` module parameter with a `NetworkId` premise on the map's domain (the assumption no longer conflates withdrawals-specifically with general `RewardAddress ⇀ Coin` maps). + Replace the `∪ˡ-res-lookup-preserve` module parameter (which carried a no-longer-needed complement restriction on the right operand) with `∪ˡ-lookup-preserve`, stated against the new `❴ c , v ❵ ∪ˡ m` form. + Add a small top-level helper `∈-dom⇒¬lookup-nothing` to discharge the defensive `nothing` case of `foldl-applyOne-pov-add`. + Update `POST-CERT-pov` to use the new `applyDirectDeposits-pov`; the proof is `sym (applyDirectDeposits-pov ...)`. The CERT-post step's own `mapˢ stake (dom dd) ⊆ dom rewards` premise is extracted from the pattern rather than threaded as a separate parameter, since the pre-CERT* state's `dom rewards` is not preserved across `CERT` trace steps (in particular by `DELEG-dereg`). + Update `sts-pov` and `CERTS-pov` signatures accordingly: add the `DirectDeposits`-`NetworkId` premise, drop the membership-of-deposits premise. The proofs now typecheck on top of master.

williamdemeo · 2026-06-23T05:45:40Z

superseded by PR #1210

williamdemeo self-assigned this May 7, 2026

williamdemeo linked an issue May 7, 2026 that may be closed by this pull request

[Dijkstra] Certs PoV #1185

Open

3 tasks

williamdemeo force-pushed the 1185-dijkstra-certs-pov branch 4 times, most recently from e4f46a7 to 4e3d554 Compare May 7, 2026 20:33

williamdemeo mentioned this pull request May 11, 2026

[Dijkstra] CIP-159-11: PoV property proofs (#1123) #1169

Closed

4 tasks

williamdemeo force-pushed the 1185-dijkstra-certs-pov branch from c4f6a1b to a2963c6 Compare May 12, 2026 05:24

williamdemeo marked this pull request as ready for review May 12, 2026 05:24

williamdemeo requested a review from Copilot May 14, 2026 04:44

Copilot started reviewing on behalf of williamdemeo May 14, 2026 04:44 View session

williamdemeo force-pushed the 1185-dijkstra-certs-pov branch from a2963c6 to f635bd6 Compare May 14, 2026 04:45

Copilot AI reviewed May 14, 2026

View reviewed changes

williamdemeo force-pushed the 1185-dijkstra-certs-pov branch 2 times, most recently from 013fa3e to 9f21a34 Compare May 15, 2026 02:18

williamdemeo marked this pull request as draft May 15, 2026 02:18

williamdemeo force-pushed the 1185-dijkstra-certs-pov branch from b99a69f to 1db822b Compare May 15, 2026 05:12

williamdemeo marked this pull request as ready for review May 15, 2026 05:14

williamdemeo requested a review from Copilot May 15, 2026 05:15

Copilot started reviewing on behalf of williamdemeo May 15, 2026 05:15 View session

Copilot AI reviewed May 15, 2026

View reviewed changes

Comment thread src/Ledger/Prelude.lagda.md

Comment on lines +134 to +135

res-decomp m m' = ∪-cong (≡ᵉ.refl {x = m ˢ}) (≡ᵉ.sym (filterᵐ-idem {m = m'}))

where module ≡ᵉ = IsEquivalence (≡ᵉ-isEquivalence {A × Coin})

williamdemeo added 8 commits May 19, 2026 15:37

[Dijkstra] CIP-159-11a: Prove Certs preservation of value (#1185)

abbc397

simplify and improve Conway Certs PoV proofs

631f227

adopt improvements from PR #1169

32ffd9e

in preparation for Carlos' recent refactor

e28815b

refactor to reflect Carlos' refactor

72e273e

fix typechecking

79db9df

williamdemeo force-pushed the 1185-dijkstra-certs-pov branch from 1db822b to 2a6a3dd Compare May 19, 2026 21:37

williamdemeo marked this pull request as draft May 19, 2026 22:40

This was referenced May 20, 2026

[Dijkstra] LEDGER PoV #1187

Open

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

Draft

williamdemeo changed the title ~~[Dijkstra] CIP-159-11a: Prove Certs preservation of value (#1185)~~ [Dijkstra] (DEPRECATED) CIP-159-11a: Prove Certs preservation of value (#1185) May 28, 2026

williamdemeo closed this Jun 23, 2026

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Uh oh!

[Dijkstra] (DEPRECATED) CIP-159-11a: Prove Certs preservation of value (#1185)#1188

[Dijkstra] (DEPRECATED) CIP-159-11a: Prove Certs preservation of value (#1185)#1188
williamdemeo wants to merge 8 commits into
masterfrom
1185-dijkstra-certs-pov

williamdemeo commented May 7, 2026 •

edited

Loading

Uh oh!

Copilot AI left a comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Copilot AI left a comment

Uh oh!

williamdemeo commented Jun 23, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants

		res-decomp m m' = ∪-cong (≡ᵉ.refl {x = m ˢ}) (≡ᵉ.sym (filterᵐ-idem {m = m'}))
		where module ≡ᵉ = IsEquivalence (≡ᵉ-isEquivalence {A × Coin})

Uh oh!

Conversation

williamdemeo commented May 7, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Description

Modules

Design notes

PRE-CERT-pov uses applyWithdrawals-pov instead of Conway's constMap chain

applyWithdrawals-pov is structured as three layers

CERT-pov, POST-CERT-pov, sts-pov are essentially unchanged from Conway

Outstanding proof obligations

Checklist

Uh oh!

Copilot AI left a comment

Choose a reason for hiding this comment

Pull request overview

Reviewed changes

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Copilot AI left a comment

Choose a reason for hiding this comment

Pull request overview

Uh oh!

williamdemeo commented Jun 23, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants

williamdemeo commented May 7, 2026 •

edited

Loading

`PRE-CERT-pov` uses `applyWithdrawals-pov` instead of Conway's `constMap` chain

`applyWithdrawals-pov` is structured as three layers

`CERT-pov`, `POST-CERT-pov`, `sts-pov` are essentially unchanged from Conway