Skip to content

Commit 1ca3f25

Browse files
williamdemeowilliamdemeo
committed
[Dijkstra] Prove Gov preservation-of-value facts in new Gov.Properties.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)
1 parent cf1f977 commit 1ca3f25

2 files changed

Lines changed: 264 additions & 0 deletions

File tree

‎src/Ledger/Dijkstra/Specification/Gov/Properties.lagda.md‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -14,4 +14,5 @@ module Ledger.Dijkstra.Specification.Gov.Properties where
1414

1515
```agda
1616
open import Ledger.Dijkstra.Specification.Gov.Properties.Computational
17+
open import Ledger.Dijkstra.Specification.Gov.Properties.PoV
1718
```

‎src/Ledger/Dijkstra/Specification/Gov/Properties/PoV.lagda.md‎

Lines changed: 263 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,263 @@
1+
---
2+
source_branch: master
3+
source_path: src/Ledger/Dijkstra/Specification/Gov/Properties/PoV.lagda.md
4+
---
5+
6+
# Properties of `GOV`: Preservation of Value {#sec:gov-properties-pov}
7+
8+
This module proves the two governance-deposit accounting facts that the top-level
9+
preservation-of-value proof (`LEDGER-pov`{.AgdaFunction} in
10+
`Ledger.Properties.PoV`{.AgdaModule}) assumes as module parameters (#1276):
11+
12+
+ `rmOrphanDRepVotes-coinFromGovDeposit`{.AgdaFunction}:
13+
`rmOrphanDRepVotes`{.AgdaFunction} only rewrites the `gvDRep`{.AgdaField} votes of
14+
each governance action, never `GovActionState.deposit`{.AgdaField}, so it leaves
15+
`coinFromGovDeposit`{.AgdaFunction} unchanged.
16+
17+
+ `GOVS-coinFromGovDeposit`{.AgdaFunction}: a `GOVS`{.AgdaDatatype} step grows
18+
`coinFromGovDeposit`{.AgdaFunction} by exactly the
19+
`govProposalsDeposits`{.AgdaFunction} of the proposals in its signal list —
20+
`GOV-Propose`{.AgdaInductiveConstructor} stores `deposit = pp .govActionDeposit`
21+
for the new action, and `GOV-Vote`{.AgdaInductiveConstructor} never changes a
22+
deposit.
23+
24+
??? note "**Status: complete**"
25+
26+
Both facts typecheck under `--safe`, with no module parameters and no postulates.
27+
Their statements match the corresponding `LEDGER-PoV`{.AgdaModule} module
28+
parameters (modulo this module's own `proposalsOf`{.AgdaFunction} copy; see
29+
below), so the rewiring (#1277) can instantiate them directly.
30+
31+
<!--
32+
```agda
33+
{-# OPTIONS --safe #-}
34+
35+
open import Ledger.Dijkstra.Specification.Transaction
36+
open import Ledger.Dijkstra.Specification.Abstract
37+
38+
module Ledger.Dijkstra.Specification.Gov.Properties.PoV
39+
(txs : _) (open TransactionStructure txs)
40+
(abs : AbstractFunctions txs) (open AbstractFunctions abs)
41+
where
42+
43+
open import Data.Nat.Base using () renaming (_+_ to infixl 6 _+ᴺ_)
44+
open import Data.Nat.Properties using (+-assoc; +-identityʳ)
45+
open import Data.Nat.Tactic.RingSolver using (solve-∀)
46+
47+
open import Ledger.Prelude
48+
49+
open import Ledger.Dijkstra.Specification.Certs govStructure
50+
open import Ledger.Dijkstra.Specification.Gov govStructure
51+
open import Ledger.Dijkstra.Specification.Ledger txs abs
52+
open import Ledger.Dijkstra.Specification.Utxo txs abs
53+
54+
open import Interface.STS
55+
```
56+
-->
57+
58+
## `proposalsOf`
59+
60+
The right injections of a list of sums, used (at `GovVote ⊎ GovProposal`) to extract
61+
the proposals from a mixed `GOVS`{.AgdaDatatype} signal list.
62+
`Ledger.Properties.PoV`{.AgdaModule} defines an identical function for stating its
63+
`GOVS-coinFromGovDeposit`{.AgdaFunction} parameter, but importing it here would
64+
create an import cycle once #1277 rewires `Ledger.Properties.PoV`{.AgdaModule} to
65+
import *this* module. So we keep a local copy (clause-for-clause identical),
66+
together with the `proposalsOf-Proposals+Votes`{.AgdaFunction} extraction lemma; the
67+
rewiring should delete the copies in `Ledger.Properties.PoV`{.AgdaModule} and import
68+
these.
69+
70+
```agda
71+
proposalsOf : ∀ {A B : Type} → List (A ⊎ B) → List B
72+
proposalsOf [] = []
73+
proposalsOf (inj₁ _ ∷ xs) = proposalsOf xs
74+
proposalsOf (inj₂ p ∷ xs) = p ∷ proposalsOf xs
75+
```
76+
77+
`proposalsOf (GovProposals+Votes t)` recovers exactly the proposals of `t`, since
78+
`GovProposals+Votes`{.AgdaFunction} lists all proposals (as right injections) before
79+
all votes (as left injections).
80+
81+
```agda
82+
proposalsOf-Proposals+Votes : ∀ {ℓ} (t : Tx ℓ)
83+
→ proposalsOf (GovProposals+Votes t) ≡ ListOfGovProposalsOf t
84+
proposalsOf-Proposals+Votes t = go (ListOfGovProposalsOf t) (ListOfGovVotesOf t)
85+
where
86+
drop-votes : ∀ {A B : Type} (vs : List A)
87+
→ proposalsOf {A = A} {B = B} (map inj₁ vs) ≡ []
88+
drop-votes [] = refl
89+
drop-votes (_ ∷ vs) = drop-votes vs
90+
go : ∀ {A B : Type} (ps : List B) (vs : List A)
91+
→ proposalsOf (map inj₂ ps ++ map inj₁ vs) ≡ ps
92+
go [] vs = drop-votes vs
93+
go (p ∷ ps) vs = cong (p ∷_) (go ps vs)
94+
```
95+
96+
## Arithmetic helpers
97+
98+
The two pure `+`-rearrangements below are discharged by the reflective ring solver
99+
over the commutative semiring of naturals (`Data.Nat.Tactic.RingSolver`). The
100+
solver recognises the ring's operations *syntactically*, so the
101+
`Ledger.Prelude`{.AgdaModule} overloaded `_+_` (a `HasAdd`{.AgdaRecord} method,
102+
which merely *reduces* to `Data.Nat._+_`) defeats it. The solver-facing statements
103+
are therefore written with the raw natural-number addition, imported as `_+ᴺ_` —
104+
definitionally equal to `_+_` at `Coin`, so the lemmas discharge `_+_` goals
105+
unchanged.
106+
107+
```agda
108+
swap-head : ∀ a b c → a +ᴺ (b +ᴺ c) ≡ b +ᴺ (a +ᴺ c)
109+
swap-head = solve-∀
110+
111+
rotate-in : ∀ a b c → a +ᴺ b +ᴺ c ≡ b +ᴺ (a +ᴺ c)
112+
rotate-in = solve-∀
113+
```
114+
115+
## `rmOrphanDRepVotes` preserves `coinFromGovDeposit`
116+
117+
`rmOrphanDRepVotes`{.AgdaFunction} maps over the `GovState`{.AgdaRecord}, rewriting
118+
only the `votes`{.AgdaField} field of each `GovActionState`{.AgdaRecord} (it filters
119+
the `gvDRep`{.AgdaField} votes down to registered DReps). The record update leaves
120+
`deposit`{.AgdaField} definitionally unchanged in every cons cell, so a list
121+
induction closes the proof.
122+
123+
```agda
124+
rmOrphanDRepVotes-coinFromGovDeposit : ∀ (cs : CertState) (g : GovState)
125+
→ coinFromGovDeposit (rmOrphanDRepVotes cs g) ≡ coinFromGovDeposit g
126+
rmOrphanDRepVotes-coinFromGovDeposit cs [] = refl
127+
rmOrphanDRepVotes-coinFromGovDeposit cs ((_ , gas) ∷ g) =
128+
cong (GovActionState.deposit gas +_) (rmOrphanDRepVotes-coinFromGovDeposit cs g)
129+
```
130+
131+
## A cons law for `govProposalsDeposits`
132+
133+
`govProposalsDeposits`{.AgdaFunction} is a `foldl`{.AgdaFunction} that adds the
134+
(constant) `govActionDeposit`{.AgdaField} to its accumulator once per proposal.
135+
The `GOVS`{.AgdaDatatype} induction below consumes proposals head-first, so it needs
136+
the cons law: one proposal contributes one `govActionDeposit`{.AgdaField}. Since
137+
`foldl`{.AgdaFunction} buries the head's contribution in the accumulator, the
138+
workhorse is the accumulator-shift lemma
139+
`govProposalsDeposits-acc`{.AgdaFunction}; the cons law is its direct corollary.
140+
(The `GOVS`{.AgdaDatatype} induction uses the shift lemma directly: the fold
141+
discards the list elements, so after reduction the head proposal never appears in
142+
the equation.)
143+
144+
```agda
145+
govProposalsDeposits-acc : ∀ (pp : PParams) (acc : Coin) (ps : List GovProposal)
146+
→ foldl (λ a _ → a + PParams.govActionDeposit pp) acc ps
147+
≡ acc + govProposalsDeposits pp ps
148+
govProposalsDeposits-acc pp acc [] = sym (+-identityʳ acc)
149+
govProposalsDeposits-acc pp acc (_ ∷ ps) =
150+
trans (govProposalsDeposits-acc pp (acc + d) ps)
151+
(trans (+-assoc acc d (govProposalsDeposits pp ps))
152+
(cong (acc +_) (sym (govProposalsDeposits-acc pp d ps))))
153+
where d = PParams.govActionDeposit pp
154+
155+
govProposalsDeposits-∷ : ∀ (pp : PParams) {p : GovProposal} (ps : List GovProposal)
156+
→ govProposalsDeposits pp (p ∷ ps)
157+
≡ PParams.govActionDeposit pp + govProposalsDeposits pp ps
158+
govProposalsDeposits-∷ pp = govProposalsDeposits-acc pp (PParams.govActionDeposit pp)
159+
```
160+
161+
## Per-step facts: `addVote` and `insertGovAction`
162+
163+
A `GOV-Vote`{.AgdaInductiveConstructor} step concludes in `addVote`{.AgdaFunction},
164+
which maps over the state, rewriting only the `votes`{.AgdaField} field of the
165+
matching action. Whether or not an entry matches the voted action id, its
166+
`deposit`{.AgdaField} is untouched, so `coinFromGovDeposit`{.AgdaFunction} is
167+
preserved. (`addVote`{.AgdaFunction} is `opaque`{.AgdaKeyword}, so the proof must
168+
unfold it explicitly.)
169+
170+
```agda
171+
opaque
172+
unfolding addVote
173+
174+
addVote-coinFromGovDeposit :
175+
∀ {s : GovState} {aid voter v}
176+
→ coinFromGovDeposit (addVote s aid voter v) ≡ coinFromGovDeposit s
177+
addVote-coinFromGovDeposit {[]} = refl
178+
addVote-coinFromGovDeposit {(gid , gas) ∷ s} {aid} {voter} {v}
179+
with gid ≟ aid
180+
... | yes _ = cong (GovActionState.deposit gas +_)
181+
(addVote-coinFromGovDeposit {s} {aid} {voter} {v})
182+
... | no _ = cong (GovActionState.deposit gas +_)
183+
(addVote-coinFromGovDeposit {s} {aid} {voter} {v})
184+
```
185+
186+
A `GOV-Propose`{.AgdaInductiveConstructor} step concludes in
187+
`addAction`{.AgdaFunction}, which is `insertGovAction`{.AgdaFunction} of a fresh
188+
`GovActionState`{.AgdaRecord} pair carrying `deposit = pp .govActionDeposit`.
189+
`insertGovAction`{.AgdaFunction} is a priority-ordered insertion; wherever the new
190+
pair lands, `coinFromGovDeposit`{.AgdaFunction} grows by exactly its deposit. The
191+
proof is a list induction with a case split on the priority comparison: in the
192+
*then* branch the new pair sinks past the head, so the head's deposit and the
193+
inserted deposit swap places (`swap-head`{.AgdaFunction}); in the *else* branch the
194+
list is extended in place and both sides agree definitionally.
195+
196+
```agda
197+
insertGovAction-coinFromGovDeposit :
198+
∀ {s : GovState} {p : GovActionID × GovActionState}
199+
→ coinFromGovDeposit (insertGovAction s p)
200+
≡ GovActionState.deposit (proj₂ p) + coinFromGovDeposit s
201+
insertGovAction-coinFromGovDeposit {[]} {_} = refl
202+
insertGovAction-coinFromGovDeposit {(gaID₀ , gaSt₀) ∷ s} {gaID₁ , gaSt₁}
203+
with govActionPriority (GovActionTypeOf gaSt₀)
204+
≤? govActionPriority (GovActionTypeOf gaSt₁)
205+
... | yes _ =
206+
trans (cong (GovActionState.deposit gaSt₀ +_)
207+
(insertGovAction-coinFromGovDeposit {s} {gaID₁ , gaSt₁}))
208+
(swap-head (GovActionState.deposit gaSt₀)
209+
(GovActionState.deposit gaSt₁)
210+
(coinFromGovDeposit s))
211+
... | no _ = refl
212+
```
213+
214+
## `GOVS` accounting
215+
216+
`GOVS`{.AgdaDatatype} is the *indexed* reflexive-transitive closure of
217+
`GOV`{.AgdaDatatype}: the convenience wrapper fixes the index at `0`, but
218+
`BS-ind`{.AgdaInductiveConstructor}'s tail runs at `suc n`, so the induction must be
219+
stated over the primed relation `_⊢_⇀⟦_⟧ᵢ*'_`{.AgdaDatatype}, generalized over the
220+
environment-index pair, and then specialized to `0`. Per step,
221+
`GOV-Vote`{.AgdaInductiveConstructor} preserves the deposit total
222+
(`addVote-coinFromGovDeposit`{.AgdaFunction}, and its signal contributes no
223+
proposal), while `GOV-Propose`{.AgdaInductiveConstructor} adds one
224+
`govActionDeposit`{.AgdaField} on both sides
225+
(`insertGovAction-coinFromGovDeposit`{.AgdaFunction} on the state side,
226+
`govProposalsDeposits-∷`{.AgdaFunction} on the accounting side).
227+
228+
```agda
229+
GOVSᵢ-coinFromGovDeposit :
230+
∀ {Γ : GovEnv} {n : ℕ} {s s' : GovState} {sigs : List (GovVote ⊎ GovProposal)}
231+
→ _⊢_⇀⟦_⟧ᵢ*'_ {_⊢_⇀⟦_⟧ᵇ_ = IdSTS} {_⊢_⇀⦇_,GOV⦈_} (Γ , n) s sigs s'
232+
→ coinFromGovDeposit s'
233+
≡ coinFromGovDeposit s + govProposalsDeposits (PParamsOf Γ) (proposalsOf sigs)
234+
235+
GOVSᵢ-coinFromGovDeposit (BS-base Id-nop) = sym (+-identityʳ _)
236+
237+
GOVSᵢ-coinFromGovDeposit {Γ} (BS-ind {sigs = sigs} (GOV-Vote _) rest) =
238+
trans (GOVSᵢ-coinFromGovDeposit rest)
239+
(cong (_+ govProposalsDeposits (PParamsOf Γ) (proposalsOf sigs))
240+
addVote-coinFromGovDeposit)
241+
242+
GOVSᵢ-coinFromGovDeposit {Γ} {s = s} (BS-ind {sigs = sigs} (GOV-Propose _) rest) =
243+
trans (GOVSᵢ-coinFromGovDeposit rest)
244+
(trans (cong (_+ X) (insertGovAction-coinFromGovDeposit {s = s}))
245+
(trans (rotate-in dep (coinFromGovDeposit s) X)
246+
(cong (coinFromGovDeposit s +_)
247+
(sym (govProposalsDeposits-acc (PParamsOf Γ) dep (proposalsOf sigs))))))
248+
where
249+
X = govProposalsDeposits (PParamsOf Γ) (proposalsOf sigs)
250+
dep = PParams.govActionDeposit (PParamsOf Γ)
251+
```
252+
253+
Specializing to index `0` gives the statement in the shape of the
254+
`LEDGER-PoV`{.AgdaModule} module parameter:
255+
256+
```agda
257+
GOVS-coinFromGovDeposit :
258+
∀ {Γ : GovEnv} {govSt govSt′ : GovState} {props : List (GovVote ⊎ GovProposal)}
259+
→ Γ ⊢ govSt ⇀⦇ props ,GOVS⦈ govSt′
260+
→ coinFromGovDeposit govSt′
261+
≡ coinFromGovDeposit govSt + govProposalsDeposits (PParamsOf Γ) (proposalsOf props)
262+
GOVS-coinFromGovDeposit = GOVSᵢ-coinFromGovDeposit
263+
```

0 commit comments

Comments
 (0)