WIP -- [Dijkstra] CIP-159: Prove Gov preservation-of-value facts (#1276) - #1278
Draft
williamdemeo wants to merge 4 commits into
Draft
WIP -- [Dijkstra] CIP-159: Prove Gov preservation-of-value facts (#1276)#1278williamdemeo wants to merge 4 commits into
williamdemeo wants to merge 4 commits into
Conversation
williamdemeo
changed the title
williamdemeo
force-pushed
the
1276-dijkstra-gov-pov
branch
2 times, most recently
from
July 31, 2026 05:41
cd63a6e to
020bae4
Compare
williamdemeo
marked this pull request as ready for review
July 31, 2026 05:49
williamdemeo
marked this pull request as draft
July 31, 2026 05:50
Contributor
There was a problem hiding this comment.
Pull request overview
This PR adds a Dijkstra-era governance PoV properties module that discharges the two LEDGER-PoV governance-deposit accounting assumptions: (1) rmOrphanDRepVotes preserves coinFromGovDeposit, and (2) a GOVS step increases coinFromGovDeposit by exactly govProposalsDeposits of the proposals in the step’s signals. It integrates the new module into the Gov.Properties registration path and records the work in the WIP changelog.
Changes:
- Add
Ledger.Dijkstra.Specification.Gov.Properties.PoVprovingrmOrphanDRepVotes-coinFromGovDepositandGOVS-coinFromGovDeposit(plus localproposalsOfand helper lemmas). - Register the new PoV properties module from
Ledger.Dijkstra.Specification.Gov.Properties. - Add a WIP
CHANGELOG.mdentry describing the new proofs and their role in dischargingLEDGER-PoVparameters.
Reviewed changes
Copilot reviewed 3 out of 3 changed files in this pull request and generated no comments.
| File | Description |
|---|---|
| src/Ledger/Dijkstra/Specification/Gov/Properties/PoV.lagda.md | New Gov PoV module proving the two governance-deposit accounting lemmas used by LEDGER-pov. |
| src/Ledger/Dijkstra/Specification/Gov/Properties.lagda.md | Registers the new Gov PoV module so it is reachable from the Dijkstra specification root. |
| CHANGELOG.md | Documents the new Gov PoV proofs under WIP and links them to #1276 / #1277. |
💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.
4 tasks
williamdemeo
force-pushed
the
1276-dijkstra-gov-pov
branch
from
August 10, 2026 19:56
020bae4 to
bfd965c
Compare
williamdemeo
force-pushed
the
1276-dijkstra-gov-pov
branch
from
August 13, 2026 03:37
bfd965c to
3a97d65
Compare
williamdemeo
added
property
Base automatically changed from
1187-dijkstra-NEW-ENTITIES-ledger-pov
to
master
September 4, 2026 03:21
williamdemeo
force-pushed
the
1276-dijkstra-gov-pov
branch
from
September 8, 2026 19:56
3a97d65 to
993e5e8
Compare
williamdemeo
changed the base branch from
master
to
1185-dijkstra-NEW-ENTITIES-certs-pov
September 8, 2026 19:57
williamdemeo
force-pushed
the
1276-dijkstra-gov-pov
branch
from
September 8, 2026 20:20
993e5e8 to
d31af54
Compare
williamdemeo
force-pushed
the
1276-dijkstra-gov-pov
branch
2 times, most recently
from
September 8, 2026 21:24
1ca1005 to
e63e8ff
Compare
williamdemeo
force-pushed
the
1276-dijkstra-gov-pov
branch
from
September 8, 2026 23:45
23593d1 to
19f5c9a
Compare
2 tasks
williamdemeo
force-pushed
the
1276-dijkstra-gov-pov
branch
from
September 9, 2026 02:11
19f5c9a to
659ae9a
Compare
williamdemeo
force-pushed
the
1276-dijkstra-gov-pov
branch
from
September 9, 2026 02:26
659ae9a to
068c368
Compare
4 tasks
williamdemeo
force-pushed
the
1276-dijkstra-gov-pov
branch
from
September 9, 2026 02:49
068c368 to
b574b14
Compare
…s.PoV (#1276) Discharge the two governance-deposit module parameters of LEDGER-PoV (Ledger.Properties.PoV): - rmOrphanDRepVotes-coinFromGovDeposit: rmOrphanDRepVotes rewrites only the gvDRep votes of each action, so coinFromGovDeposit is unchanged (list induction; the record update leaves .deposit definitionally intact). - GOVS-coinFromGovDeposit: a GOVS step grows coinFromGovDeposit by exactly govProposalsDeposits of its signal's proposals. Proved by induction over the primed indexed RTC generalized over the environment-index pair (the GOVS wrapper fixes index 0 but BS-ind's tail runs at suc n), then specialized to 0. Per step: GOV-Vote preserves the total (addVote is opaque and deposit-preserving; proof unfolds it), GOV-Propose adds one govActionDeposit on both sides (insertGovAction lemma with a priority if-split on the state side, foldl accumulator-shift lemma on the accounting side). proposalsOf and proposalsOf-Proposals+Votes are defined here with clauses identical to Ledger.Properties.PoV's copies: importing that module here would become an import cycle once #1277 rewires it to import this module, at which point its copies should be deleted in favour of these. Pure +-rearrangements are discharged with the reflective ring solver over raw _+N_, per the pattern established in Ledger.Properties.PoV. Green under --safe; no module parameters, no postulates. Closes #1276 AI-assisted development: Claude Fable 5 (Anthropic)
Per the review policy established on the base PR: issue numbers, status admonitions, and rewiring instructions move to the PR description; the ring-solver/HasAdd explanation duplicated from Ledger.Properties.PoV becomes a cross-reference. AI-assisted development: Claude Fable 5 (Anthropic)
…their parameters rmOrphanDRepVotes-coinFromGovDeposit and GOVS-coinFromGovDeposit are theorems on this branch, so LEDGER-PoV now imports Gov.Properties.PoV instead of assuming them. proposalsOf and proposalsOf-Proposals+Votes now have their single home in Gov.Properties.PoV; the consumer's copies are deleted. AI-assisted development: Claude Fable 5 (Anthropic)
williamdemeo
force-pushed
the
1276-dijkstra-gov-pov
branch
from
September 9, 2026 20:01
b574b14 to
ae36396
Compare
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Description
Closes #1276. Stacked on #1210 (base:
1185-dijkstra-NEW-ENTITIES-certs-pov); GitHub retargets it as the PRs below merge.Discharges the two governance-deposit parameters of the
LEDGER-PoVcontract (#1203):rmOrphanDRepVotes-coinFromGovDepositandGOVS-coinFromGovDeposit.What lands
Gov.Properties.PoV(one new module) and its registration inGov.Properties.dijkstra-gov-povnow derives as proved.Ledger.Properties.PoVrewiring: the two gov parameters are deleted and the facts imported fromGov.Properties.PoV(contract from 12 to 10 parameters).Key points for review
GOVSis the indexed reflexive-transitive closure ofGOV, so the induction is stated over the primed relation_⊢_⇀⟦_⟧ᵢ*'_, generalized over the index, then specialized to0.proposalsOfand its extraction lemma now have their single home inGov.Properties.PoV; the rewiring commit deletes the consumer's copies.Verification
Ledger.Properties.PoVtypechecks with the two parameters deleted, which verifies the discharge by construction; the ten remaining parameters are owned elsewhere ([Dijkstra] Batch-threading UTxO invariants for LEDGER-pov #1274, [Dijkstra] Discharge the no-truncation withdrawal bounds (ENTITIES/SUBENTITIES-wdrls-bounded) #1275, and theApplyToRewardsidentities).agda src/Ledger.lagda.mdandscan_properties.py --checkboth green.Checklist
CHANGELOG.md(none in this PR)🤖 AI-assisted development: Claude Fable 5 (Anthropic)