[Conway] Property: ChangePParams proposals have a non-empty update group (#1234) - #1289
Merged
Merged
Conversation
williamdemeo
marked this pull request as draft
August 6, 2026 05:14
williamdemeo
changed the title
Contributor
There was a problem hiding this comment.
Pull request overview
This PR discharges the previously “coming soon”/unstated proof for the Conway governance property that accepted ChangePParams proposals must update at least one protocol parameter group, by strengthening the statement with the necessary STS premise (GOV acceptance) and then lifting it to GOVS and LEDGER.
Changes:
- Strengthen
ChangePPHasGroupto require aGOVstep premise (proposal is accepted), and provide the corresponding proof. - Add the lifted corollary
GOVS-ChangePPHasGroupand a newLEDGER-ChangePPHasGrouptheorem/module restoring the “proposal carried by a valid tx” formulation. - Wire the new Ledger-level property into the Ledger properties module and MkDocs navigation/links, and record it in the changelog.
Reviewed changes
Copilot reviewed 7 out of 7 changed files in this pull request and generated no comments.
Show a summary per file
| File | Description |
|---|---|
| src/Ledger/Conway/Specification/Properties.lagda.md | Updates the high-level properties list to reference the GOV- and LEDGER-level theorems. |
| src/Ledger/Conway/Specification/Ledger/Properties/ChangePPGroup.lagda.md | New Ledger-level theorem/module LEDGER-ChangePPHasGroup, lifting from GOVS-ChangePPHasGroup. |
| src/Ledger/Conway/Specification/Ledger/Properties.lagda.md | Exports the new Ledger property module. |
| src/Ledger/Conway/Specification/Gov/Properties/ChangePPGroup.lagda.md | Re-states the property with a GOV acceptance premise and adds proofs, plus a GOVS lift. |
| CHANGELOG.md | Notes the newly proven property at GOV/GOVS/LEDGER levels (issue #1234). |
| build-tools/static/mkdocs/mkdocs.yml | Adds the new Ledger property page to the documentation nav. |
| build-tools/static/mkdocs/includes/links.md | Adds links for the new Ledger property page and theorem anchor. |
💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.
williamdemeo
added a commit
that referenced
this pull request
Aug 7, 2026
williamdemeo
added a commit
that referenced
this pull request
Aug 7, 2026
williamdemeo
added a commit
that referenced
this pull request
Aug 7, 2026
williamdemeo
changed the title
williamdemeo
marked this pull request as ready for review
August 7, 2026 02:49
williamdemeo
added a commit
that referenced
this pull request
Aug 7, 2026
williamdemeo
force-pushed
the
1234-conway-changepparams-proposals
branch
from
August 10, 2026 19:51
d88c460 to
5eb232f
Compare
williamdemeo
added
era: conway
property
…roup Discharge the "coming soon" proof marker in Ledger.Conway.Specification.Gov.Properties.ChangePPGroup. As previously stated the claim was not provable: its only premises were that p is a proposal of a transaction body and that its action is ⟦ ChangePParams , pu ⟧ᵍᵃ, and an arbitrary transaction body may carry a degenerate proposal whose update touches no parameter group. What rules such a proposal out is the actionWellFormed premise of GOV-Propose, so the statement is strengthened with a GOV-step premise. The name ChangePPHasGroup and the clm:ChangePPGroup anchor are unchanged. - ChangePPHasGroup: if (Γ , k) ⊢ s ⇀⦇ inj₂ p ,GOV⦈ s' and the action of p is ⟦ ChangePParams , pu ⟧ᵍᵃ, then updateGroups pu ≢ ∅. Only GOV-Propose can consume a proposal signal; substituting the action equation into its actionWellFormed premise reduces it to ppdWellFormed pu, whose first component is the claim. - ChangePPHasGroupᵢ / GOVS-ChangePPHasGroup: the same for every proposal of a signal list accepted by GOVS, by induction on the indexed closure. The module no longer mentions Tx, so it is reparameterized by GovStructure, matching Gov.Properties.LastVoteApplied. A new module Ledger.Conway.Specification.Ledger.Properties.ChangePPGroup lifts the result to LEDGER, restoring the original "p ∈ Tx.body tx" formulation for a valid transaction: LEDGER-V feeds txgov txb to GOVS, so every proposal of the transaction is a GOVS signal. Update the properties index (Claim -> Theorem), the docs links and nav, and the changelog.
williamdemeo
force-pushed
the
1234-conway-changepparams-proposals
branch
from
September 2, 2026 02:55
5eb232f to
7cb2f67
Compare
williamdemeo
added a commit
that referenced
this pull request
Sep 3, 2026
The rebase brought in PR #1289 (ChangePPGroup proved at the GOV level, LEDGER-level lift added), which flips the derived statuses: Conway is now 15 proved / 5 stated / 0 planned. The committed dashboard was not regenerated with the rebase, so the properties-check gate was failing on the previous head — exactly the drift it exists to catch.
williamdemeo
added a commit
that referenced
this pull request
Sep 4, 2026
The rebase brought in PR #1289 (ChangePPGroup proved at the GOV level, LEDGER-level lift added), which flips the derived statuses: Conway is now 15 proved / 5 stated / 0 planned. The committed dashboard was not regenerated with the rebase, so the properties-check gate was failing on the previous head — exactly the drift it exists to catch.
williamdemeo
added a commit
that referenced
this pull request
Sep 4, 2026
The rebase brought in PR #1289 (ChangePPGroup proved at the GOV level, LEDGER-level lift added), which flips the derived statuses: Conway is now 15 proved / 5 stated / 0 planned. The committed dashboard was not regenerated with the rebase, so the properties-check gate was failing on the previous head — exactly the drift it exists to catch.
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.
Proves that if the
GOVrule accepts a proposal whose action is⟦ ChangePParams , pu ⟧ᵍᵃ, thenupdateGroups pu ≢ ∅, discharging the "coming soon" marker inGov.Properties.ChangePPGroup.The statement was fixed by adding a GOV-step premise.
As previously stated the claim had no STS premise, only
p ∈ Tx.body txtogether with the action equation, and in that form it is not provable: an arbitrary transaction body can carry a degenerate proposal whose update touches no parameter group.Such a proposal is not possible because of the
actionWellFormedpremise ofGOV-Propose, so the property is about proposals the ledger accepts.The name
ChangePPHasGroupand theclm:ChangePPGroupanchor are unchanged; the module is now parameterized byGovStructuresince it no longer mentionsTx, matchingGov.Properties.LastVoteApplied.Two corollaries are also proved in this PR.
GOVS-ChangePPHasGroup, for every proposal of a signal list accepted byGOVSLEDGER-ChangePPHasGroup, in the new moduleLedger.Properties.ChangePPGroup; it restores the originalp ∈ Tx.body txformulation for a valid transaction accepted byLEDGER.Closes #1234