Gov property #414: state that GA deposits are eventually refunded by williamdemeo · Pull Request #1217 · IntersectMBO/formal-ledger-specifications

williamdemeo · 2026-06-09T13:53:07Z

Description

Closes #414.

States and proves the governance property in #414 ("GA deposits are eventually refunded"). The proof is machine-checked under --safe with Agda 2.8.0.

New module Ledger.Conway.Specification.Chain.Properties.EventuallyRefunded:

gaDepositInPot cs gaid — the deposit pot of a ChainState still holds the GovActionDeposit for gaid.
CHAINStar — reflexive-transitive closure of CHAIN along a list of blocks.
FreshId gaid bs — no transaction in bs has TxId equal to proj₁ gaid.
SucIsLeast — successor is least: e < e' → sucᵉ e ≤ e'.
InvariantAt / CHAINStar-Invariant — IH conditions at intermediate states.
_⊢_⇀⦇_,REFUNDED⦈_ — bundles all premises into a single STS-style relation.
GADepositsEventuallyRefunded — the theorem type: given a REFUNDED derivation, ¬ gaDepositInPot cs' gaid.
gaDepositsEventuallyRefunded — the proof.

Also wires the module into the Chain.Properties aggregator, lists the claim in the properties index (Ledger.Conway.Specification.Properties), and adds a CHANGELOG entry.

Theorem

The REFUNDED relation bundles the premises in STS style. The theorem gaDepositsEventuallyRefunded states: given a REFUNDED derivation, the deposit is no longer in the pot.

The REFUNDED premises are:

#	Precondition	Status
1	`govDepsMatch`	Known `CHAIN` invariant
2	`GovState` membership	Identifies the action
3	`LastEpochOf cs ≤ expiresIn gaSt`	Action not yet expired
4	`FreshId`	Holds in practice (`TxId` is a hash)
5	`SucIsLeast`	Holds for ℕ; missing `EpochStructure` axiom (see #1263)
6	`CHAINStar-Invariant`	Holds for reachable states; derivation requires additional infrastructure

Witness epoch: sucᵉ (sucᵉ (expiresIn gaSt)) — two epochs due to the RATIFY/GovernanceUpdate pipeline (RATIFY marks for removal at sucᵉ (expiresIn); GovernanceUpdate filters at the following epoch).

Preconditions 4–6 are "engineering debt": they hold for all reachable states but their formal derivation from the existing abstract interface requires infrastructure not yet present in the specification.

Proof structure

The theorem gaDepositsEventuallyRefunded unpacks the REFUNDED derivation and delegates to the workhorse gaDepositsEventuallyRefunded', which proceeds by induction on CHAINStar:

Base case: vacuous (≤e<sucᵉsucᵉ⇒⊥).
Inductive step: the CHAINStar-Invariant at the intermediate state is either inj₁ (deposit already absent → CHAINStar-GA-absent propagates) or inj₂ (IH preconditions hold → recurse).

Key sub-lemmas proved

ratifies-expired∈⇒in-removed — RATIFIES puts expired actions in removed
govUpdate-removes — GovernanceUpdate filters condemned actions from govSt'
EPOCH-GA-absent — EPOCH preserves GA-deposit absence (deposits only shrink via ∣_ᶜ)
LEDGER-GA-absent / LEDGERS-GA-absent — LEDGER preserves GA-deposit absence (via updateDeposits-GA-absent)
CHAIN-GA-absent / CHAINStar-GA-absent — the "stays gone" invariant
updateDeposits-GA-absent — combined cert + proposal deposit absence preservation
gdm-dep⇒dpMap / gdm-¬dpMap⇒¬dep — govDepsMatch bridges

Key discoveries

Two-epoch pipeline: RATIFY marks at sucᵉ(expiresIn), GovernanceUpdate removes at sucᵉ(sucᵉ(expiresIn))
govDepsMatch alone insufficient — orphan deposits, expired-but-present actions
FreshId needed — abstract TxId has no freshness guarantee
SucIsLeast needed — not derivable from existing EpochStructure axioms

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

Adds a new Conway governance property statement (no proof yet) asserting that held governance action (GA) deposits are eventually refunded, and wires it into the spec’s property aggregation/index and changelog.

Changes:

Introduces Ledger.Conway.Specification.Chain.Properties.EventuallyRefunded with definitions for gaDepositInPot, CHAINStar, and the property statement GADepositsEventuallyRefunded (proof TODO).
Registers the new property module in the Chain.Properties aggregator and lists the claim in the properties index.
Documents the new stated claim in CHANGELOG.md.

Reviewed changes

Copilot reviewed 4 out of 4 changed files in this pull request and generated 2 comments.

File	Description
src/Ledger/Conway/Specification/Chain/Properties/EventuallyRefunded.lagda.md	New property statement module + supporting definitions (proof stub).
src/Ledger/Conway/Specification/Chain/Properties.lagda.md	Exposes the new property module via the properties aggregator.
src/Ledger/Conway/Specification/Properties.lagda.md	Adds the claim to the properties index.
CHANGELOG.md	Notes the addition of the stated (unproved) claim.

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

williamdemeo · 2026-06-23T06:12:39Z

Machine-checked this branch with Agda 2.8.0 (via the project's Nix flake): EventuallyRefunded.lagda.md and the Ledger.Conway.Specification.Properties index both typecheck under --safe with no errors or warnings. The statement stands as a Claim (CHAINStar, Σ[ e ∈ Epoch ], and e ≤ LastEpochOf cs' all elaborate as written) — no proof yet.

Pushed two small refinements:

Switched the pending marker from *Proof*. (TODO) to *Proof*. (coming soon). That string is the machine-readable "proof pending" signal the property-tracking scanner keys on; with (TODO) the claim would later be misread as proved.
Fixed the roadmap cross-link: added the [CHAIN-EventuallyRefunded] / [Chain.Properties.EventuallyRefunded] link definitions in includes/links.md and rendered the claim as a list item, matching its siblings.

Statement only; proof to follow. Part of #414.

Generated by Claude Code

Add the statement stub for issue #414 as a CHAIN-level claim in a new module Ledger.Conway.Specification.Chain.Properties.EventuallyRefunded: - gaDepositInPot: a governance-action deposit is still held in a chain state - CHAINStar: reflexive-transitive closure of CHAIN over a list of blocks - GADepositsEventuallyRefunded: every held GA deposit is eventually removed from the deposit pot once the chain progresses past its expiry epoch The proof is left as future work ("coming soon"). Wire the module into the Chain.Properties aggregator, list the claim in the properties index, and note it in the changelog.

Co-authored-by: Copilot Autofix powered by AI <175728472+Copilot@users.noreply.github.com>

The EventuallyRefunded statement stub typechecks under Agda 2.8.0 as-is (no proof yet). Two refinements: - Use the `*Proof*. (coming soon)` pending marker (was `(TODO)`), matching the convention the property-tracking scanner keys on, so the claim is read as `stated` (proof pending) rather than being mistaken for proved. - Fix the roadmap entry in the Conway properties index: add the `[CHAIN-EventuallyRefunded]` / `[Chain.Properties.EventuallyRefunded]` link definitions and render the claim as a list item, matching siblings. Part of #414 (statement only; proof to follow). Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01RP1jARAhD3898yZhVnPHZ4

The naive statement is false for arbitrary ChainStates: an "orphan" GovActionDeposit entry (present in the deposit map but absent from GovState) would never be removed by any EPOCH transition. Adding govDepsMatch—a known CHAIN invariant—ensures every such deposit has a matching GovActionState with an expiresIn epoch. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>

Revise GADepositsEventuallyRefunded with four preconditions: 1. govDepsMatch — deposits match governance state 2. GovState membership — identifies the action's expiresIn 3. LastEpochOf cs ≤ expiresIn gaSt — action not yet expired 4. FreshId gaid bs — no transaction reuses the GovActionID (NEW) FreshId is needed because the formal spec's abstract TxId type does not enforce freshness; in practice TxId is a hash so collisions cannot happen. Also prove supporting lemmas: - ≤e<sucᵉ⇒⊥: discharges the CHAINStar base case - gdm-dep⇒dpMap / gdm-¬dpMap⇒¬dep: bridge between govDepsMatch and deposit-pot membership Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>

…Y lemmas The EPOCH transition uses a two-epoch pipeline: at epoch sucᵉ (expiresIn), RATIFIES marks the expired action for removal (adding it to fut'.removed); at the FOLLOWING epoch, GovernanceUpdate actually filters it out of the governance state. The previous witness sucᵉ (expiresIn) was one epoch too early. Changes: - Update cutoff to sucᵉ (sucᵉ (expiresIn gaSt)) in statement and prose - Add ≤e<sucᵉsucᵉ⇒⊥ corollary for the base case - Prove four RATIFY/RATIFIES lemmas: * ratify-expired⇒in-removed: single step, expired → in removed * ratify-removed-mono: single step preserves removed membership * ratifies-removed-mono: RTC preserves removed membership * ratifies-expired∈⇒in-removed: expired action in processed list ends up in removed (main lemma) Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>

Changes to EventuallyRefunded: - Add SucIsLeast as a 5th precondition (e < e' → sucᵉ e ≤ e', needed for the inductive step, not yet an EpochStructure axiom) - Fix witness epoch to sucᵉ (sucᵉ (expiresIn gaSt)) to account for the two-epoch RATIFY/GovernanceUpdate pipeline - Add ≤e<sucᵉsucᵉ⇒⊥ corollary for the base case - Prove govUpdate-removes: actions in fut.removed are filtered out of GovernanceUpdate.govSt' - Prove RATIFY/RATIFIES lemmas: * ratify-expired⇒in-removed (single step) * ratify/ratifies-removed-mono (removed only grows) * ratifies-expired∈⇒in-removed (expired in list → in removed) Also write /tmp/new-issue-add-axiom.md proposing the addition of <⇒sucᵉ≤ to EpochStructure. Proof of the full theorem is in progress; remaining sub-lemmas (LEDGERS preserves/doesn't add GovState entries with fresh TxId) require further set-theoretic infrastructure. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>

Prove that GovActionDeposit gaid stays absent from the deposits map through all deposit-modifying operations, given FreshId: - GA∉dom-certDep: cert deposits never add GA keys - updCertDeps-GA-absent: updateCertDeposits preserves GA absence (by induction on certs; each case uses ∪⁺/∪ˡ/∣_ᶜ helpers) - GovActionDeposit-inj: constructor is injective - updPropDeps-GA-absent: updateProposalDeposits with fresh TxId preserves GA absence - updateDeposits-GA-absent: combined lemma for updateDeposits These lemmas establish the "stays gone" invariant: once a GA deposit is removed by EPOCH, it cannot be re-added by LEDGER steps when FreshId holds. All domain-specific sub-lemmas for GADepositsEventuallyRefunded are now proved. Epoch order: ≤e<sucᵉ⇒⊥, ≤e<sucᵉsucᵉ⇒⊥ govDepsMatch bridges: gdm-dep⇒dpMap, gdm-¬dpMap⇒¬dep RATIFY/RATIFIES: ratify-expired⇒in-removed, ratify-removed-mono, ratifies-removed-mono, ratifies-expired∈⇒in-removed GovernanceUpdate: govUpdate-removes Deposit-absence preservation: GA∉dom-certDep, updCertDeps-GA-absent, GovActionDeposit-inj, updPropDeps-GA-absent, updateDeposits-GA-absent, ∉-dom-∪⁺ᵈ, ∉-dom-∪ˡᵈ, ∉-dom-resᶜᵈ The proof section now contains a detailed roadmap for the remaining assembly: connecting these lemmas through the nested CHAIN/TICK/NEWEPOCH/BBODY/LEDGERS derivation structure. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>

Prove the "stays gone" chain of lemmas: once GovActionDeposit gaid is absent from the deposits, it stays absent through any chain extension (given FreshId). New lemmas: - EPOCH-GA-absent: EPOCH preserves deposit absence (deposits only shrink via GovernanceUpdate ∣_ᶜ and POOLREAP ∣_ᶜ) - LEDGER-GA-absent: single LEDGER step preserves absence (via updateDeposits-GA-absent for Scripts-Yes, identity for Scripts-No) - LEDGERS-GA-absent: lift to LEDGERS (RTC of LEDGER) - CHAIN-GA-absent: single CHAIN step, case-splitting on NEWEPOCH-New / Not-New / No-Reward-Update - CHAINStar-GA-absent: lift to full CHAINStar — the main "stays gone" invariant Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>

The proof of gaDepositsEventuallyRefunded is complete under --safe. Update the prose to accurately describe the proved theorem: - Fix precondition count (5 → 6) to include CHAINStar-Invariant - Add description of CHAINStar-Invariant and InvariantAt - Replace "deferred to a follow-up" with accurate proof description - Add summary table of all six preconditions and their status - Rename <⇒sucᵉ≤ reference to SucIsLeast in prose Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>

- Swap primes: GADepositsEventuallyRefunded is now the clean theorem statement (pattern-matches REFUNDED to extract gaid); GADepositsEventuallyRefunded' is the flat workhorse proof - Add gaDepositsEventuallyRefunded as the main theorem, which unpacks the REFUNDED derivation and delegates to the workhorse - Fix gaid scoping in GADepositsEventuallyRefunded (option A: pattern-match on REFUNDED constructor to bind gaid) - Update prose to refer to gaDepositsEventuallyRefunded Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>

Copilot

Pull request overview

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


 ## Conway spec

+- State the claim that governance action deposits are eventually refunded (statement only; see #414)


+blocks.
+
+```agda
+-- The deposits of `cs` still holds the deposit for governance action `gaid`.


+  The membership witness
+   `(gaid , gaSt) ∈ fromList (GovStateOf cs)`{.Agda}
+   identifies the `GovActionState`{.AgdaRecord} whose `expiresIn`{.AgdaField} field
+   determines the deadline.


williamdemeo marked this pull request as ready for review June 23, 2026 02:44

williamdemeo requested a review from Copilot June 23, 2026 02:44

Copilot started reviewing on behalf of williamdemeo June 23, 2026 02:44 View session

Copilot AI reviewed Jun 23, 2026

View reviewed changes

Comment thread src/Ledger/Conway/Specification/Properties.lagda.md Outdated

Comment thread src/Ledger/Conway/Specification/Chain/Properties/EventuallyRefunded.lagda.md Outdated

williamdemeo self-assigned this Jun 23, 2026

williamdemeo requested a review from carlostome June 23, 2026 05:47

williamdemeo marked this pull request as draft June 24, 2026 14:39

williamdemeo force-pushed the claude/414-property-eventually-refunded branch from 46683f0 to 88b7157 Compare June 25, 2026 02:59

williamdemeo changed the title ~~Gov property #414: state that GA deposits are eventually refunded~~ WIP -- Gov property #414: state that GA deposits are eventually refunded Jun 25, 2026

williamdemeo force-pushed the claude/414-property-eventually-refunded branch 2 times, most recently from a161a6b to e3e7ecd Compare July 1, 2026 04:34

williamdemeo changed the title ~~WIP -- Gov property #414: state that GA deposits are eventually refunded~~ Gov property #414: state that GA deposits are eventually refunded Jul 1, 2026

williamdemeo marked this pull request as ready for review July 1, 2026 05:10

williamdemeo marked this pull request as draft July 1, 2026 14:32

claude and others added 15 commits July 1, 2026 20:17

remove unneeded import causing clash of type definitions

5e1104b

remove unneeded import causing clash of type definitions

547b7f1

Apply suggestions from code review

599b15f

Co-authored-by: Copilot Autofix powered by AI <175728472+Copilot@users.noreply.github.com>

final cleanup

be80c3f

williamdemeo force-pushed the claude/414-property-eventually-refunded branch from 53f5072 to be80c3f Compare July 2, 2026 02:18

williamdemeo marked this pull request as ready for review July 2, 2026 02:18

williamdemeo requested a review from Copilot July 2, 2026 02:18

Copilot started reviewing on behalf of williamdemeo July 2, 2026 02:18 View session

Copilot AI reviewed Jul 2, 2026

View reviewed changes

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Uh oh!

Gov property #414: state that GA deposits are eventually refunded#1217

Gov property #414: state that GA deposits are eventually refunded#1217
williamdemeo wants to merge 15 commits into
masterfrom
claude/414-property-eventually-refunded

williamdemeo commented Jun 9, 2026 •

edited

Loading

Uh oh!

Copilot AI left a comment

Uh oh!

Uh oh!

Uh oh!

williamdemeo commented Jun 23, 2026

Uh oh!

Copilot AI left a comment

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants


		## Conway spec

		- State the claim that governance action deposits are eventually refunded (statement only; see #414)

Uh oh!

Conversation

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

Uh oh!

Description

Theorem

Proof structure

Key sub-lemmas proved

Key discoveries

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!

williamdemeo commented Jun 23, 2026

Uh oh!

Copilot AI left a comment

Choose a reason for hiding this comment

Pull request overview

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

williamdemeo commented Jun 9, 2026 •

edited

Loading