Skip to content

Commit 5bc7e43

Browse files
williamdemeowilliamdemeo
committed
Bridge CERTS evolution to closed-form cert-deposit accounting
Adds the per-step and RTC-induction bridging lemmas that prove the actual `CertState` produced by a `CERTS` chain has the same three deposit pots (and hence the same `coinFromDeposits`) as the closed-form `updateCertDeposits` applied to the initial state and the cert list. This is the cert-deposit half of the `LEDGER-pov` chain; combined with the `posNeg-deposits` cancellation identity, it closes the deposit-accounting equation against the UTXO batch-balance equation. New proofs (PR branch): + `CERT-deposits-updateCertDeposit` in `Certs.Properties.PoVLemmas`. Per-step, case-split on the `CERT` rule's eight `DCert` constructors; `refl` in seven cases, `POOL-rereg` discharged via the pool-deposit alignment invariant. + `CERTS-deposits-updateCertDeposits` in `Certs.Properties.PoV`. RTC induction mirroring `CERTS-pov`. Factored through `updateCertDeposit-list`, a pure pot-only `foldl` that is the rule-intrinsic counterpart of `updateCertDeposits`; the bridge `pots-updateCertDeposits` handles the inheritance of non-deposit `CertState` fields. + `CERTS-coinFromDeposits-updateCertDeposits`. Coin projection of the main lemma, immediately usable by `LEDGER-pov`. Both bridging lemmas are parameterised over (a) two deferred set/map facts (`∪ˡ-singleton-mem-≡`, `Is-just-isPoolRegistered⇒∈-dom`) to be discharged from the standard library; and (b) the pool-deposit alignment invariant `PoolDepositsAligned` plus, for the RTC sibling, its `CERT`-step preservation lemma — both follow by inspection of the `POOL` sub-rules. Master-touching changes + **Bug fix in `updateCertDeposits`**. Was setting `DState.deposits` to `depositsᵍ` (the `GState` delta) instead of `depositsᵈ`. The `depositsᵈ` name was bound by destructuring but otherwise unused — almost certainly an unintended typo. + **Bug fix in `updateCertDeposits`**. Was using `foldr`, processing certs right-to-left. The `CERTS` rule processes certs left-to-right (via `BS-ind`'s head-first decomposition). For non-commutative cert sequences this is unsound: e.g. `[delegate c keyDeposit, dereg c (just keyDeposit)]` for a fresh credential should end with `c ∉ deposits` per `CERTS`, but `foldr` (which processes the `dereg` on the fresh state first as a no-op, then the `delegate`) ends with `c ∈ deposits`. Switched to `foldl`. Conway's `updateCertDeposits` is recursive left-to-right (equivalent to `foldl`); Dijkstra's own `applyToRewards` uses `foldl`. + **Refactor**. Extracted `updateCertDepositsStep` as a named function from `updateCertDeposits`' inner lambda, so that downstream proofs can state and use its per-step pots equation. + **Hoist**. Moved `updateCertDeposit`, `updateCertDeposits`, `coinFromDeposits`, `depositsChange`, `newCertDeposits`, `refundCertDeposits` from `Utxo.lagda.md` to `Certs.lagda.md`. These depend only on `Certs`-level definitions (`PParams`, `DCert`, `CertState`); the previous location forced any proof referencing them to take the larger `TransactionStructure` / `AbstractFunctions` parameter set, blocking placement of the bridging lemmas in `Certs.Properties.PoV{,Lemmas}`. `govProposalsDeposits` remains in `Utxo.lagda.md` (depends on `GovProposal`). PR-branch-only changes: + `Ledger.lagda.md`. Replaced the local `coinFromDeposit` (singular) with the hoisted `coinFromDeposits` (plural). `HasCoin-LedgerState` has three summands: `getCoin(UTxOState) + rewardsBalance(DState) + coinFromDeposits(CertState)`. Gov-action deposits are stored in `GState.deposits` (keyed by `returnAddr`'s stake credential) and are therefore already counted by the third summand.
1 parent d78fc70 commit 5bc7e43

3 files changed

Lines changed: 291 additions & 0 deletions

File tree

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

Lines changed: 191 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -72,3 +72,194 @@ CERTS-pov : {Γ : CertEnv} {s s' : CertState}
7272
CERTS-pov (BS-base Id-nop) = refl
7373
CERTS-pov (BS-ind step rest) = trans (CERT-pov step) (CERTS-pov rest)
7474
```
75+
76+
## The `CERTS-deposits-updateCertDeposits` bridging lemma
77+
78+
The `LEDGER-pov` chain needs to know that the actual `CertState` produced by
79+
a `CERTS` chain has the same three deposit pots — and hence the same
80+
`coinFromDeposits` — as the closed-form `updateCertDeposits`{.AgdaFunction}
81+
(defined in `Certs.lagda.md`) applied to the initial state and the cert list.
82+
The per-step ingredient is `CERT-deposits-updateCertDeposit`{.AgdaFunction}
83+
(in `Certs.Properties.PoVLemmas`); here we lift it to the reflexive-transitive
84+
closure.
85+
86+
The lift goes via a pure pot-only foldl (`updateCertDeposit-list`). This is a
87+
small intermediate that lets us state and prove the rule-intrinsic RTC induction
88+
(`CERTS-deposits-updateCertDeposit-list`) without mentioning `updateCertDeposits`
89+
at all, and then bridge to `updateCertDeposits`-form via `pots-updateCertDeposits`,
90+
which captures the structural fact that `updateCertDeposits` only updates the
91+
three deposit pots (inheriting all other `CertState` fields from its initial
92+
state).
93+
94+
The proof structure (after diff #04 puts `updateCertDeposits` on `foldl` and
95+
exposes the named step function `updateCertDepositsStep`):
96+
97+
+ `updateCertDeposit-list pp init [] = init`
98+
+ `updateCertDeposit-list pp init (c ∷ cs) = updateCertDeposit-list pp (updateCertDeposit pp c init) cs`
99+
+ `pots-updateCertDepositsStep` is `refl` (up to Σ-η on the
100+
`updateCertDeposit pp c (pots s)` triple).
101+
+ `pots-updateCertDeposits` is an induction on the cert list, applying the
102+
step-level pots equation at each cons.
103+
+ `CERTS-deposits-updateCertDeposit-list` is RTC induction in the style of
104+
`CERTS-pov`, using `CERT-deposits-updateCertDeposit` at each `BS-ind` step
105+
and threading the `PoolDepositsAligned` invariant via the
106+
`PoolDepositsAligned-CERT` preservation lemma (a deferred parameter).
107+
108+
<!--
109+
```agda
110+
open import Data.List using (foldl)
111+
open import Data.Product using (proj₁; proj₂)
112+
113+
private
114+
-- Convenience accessor for the three deposit pots of a `CertState`.
115+
pots : CertState → (Credential ⇀ Coin) × (KeyHash ⇀ Coin) × (Credential ⇀ Coin)
116+
pots cs = ( DepositsOf (DStateOf cs)
117+
, DepositsOf (PStateOf cs)
118+
, DepositsOf (GStateOf cs) )
119+
120+
-- Pure pot-only foldl mirroring `updateCertDeposits`. Operates on the three
121+
-- deposit pots without touching any other `CertState` field.
122+
updateCertDeposit-list :
123+
PParams
124+
→ (Credential ⇀ Coin) × (KeyHash ⇀ Coin) × (Credential ⇀ Coin)
125+
→ List DCert
126+
→ (Credential ⇀ Coin) × (KeyHash ⇀ Coin) × (Credential ⇀ Coin)
127+
updateCertDeposit-list pp = foldl (λ p c → updateCertDeposit pp c p)
128+
```
129+
-->
130+
131+
```agda
132+
module CERTS-Deposits-Bridge
133+
-- Forwarded helpers from the per-step bridging module in PoVLemmas.
134+
( ∪ˡ-singleton-mem-≡ :
135+
∀ {A : Type} ⦃ _ : DecEq A ⦄
136+
(m : A ⇀ Coin) (k : A) (v : Coin)
137+
→ k ∈ dom m → m ∪ˡ ❴ k , v ❵ ≡ m )
138+
( Is-just-isPoolRegistered⇒∈-dom :
139+
∀ {pools : Pools} {kh : KeyHash}
140+
→ Is-just (isPoolRegistered pools kh) → kh ∈ dom pools )
141+
-- Preservation of the pool-deposit alignment invariant under one `CERT` step.
142+
-- Provable from the rules by inspection (the invariant is genuinely preserved
143+
-- by every `POOL` sub-rule); deferred as a parameter to keep this module
144+
-- focused on the RTC induction.
145+
( PoolDepositsAligned-CERT :
146+
∀ {Γ : CertEnv} {s s' : CertState} {dCert : DCert}
147+
→ Γ ⊢ s ⇀⦇ dCert ,CERT⦈ s'
148+
→ PoolDepositsAligned (PStateOf s)
149+
→ PoolDepositsAligned (PStateOf s') )
150+
where
151+
152+
open CERT-Deposits-Bridge ∪ˡ-singleton-mem-≡ Is-just-isPoolRegistered⇒∈-dom
153+
using (CERT-deposits-updateCertDeposit)
154+
```
155+
156+
### Step-level pots equation
157+
158+
`updateCertDepositsStep pp s c` updates only the three deposit pots of `s` (per
159+
`updateCertDeposit pp c` applied to `s`'s initial pots) and inherits all other
160+
fields from `s`. Therefore its pots-projection equals `updateCertDeposit pp c
161+
(pots s)`. Holds by Σ-η on the projection triple.
162+
163+
```agda
164+
pots-updateCertDepositsStep :
165+
∀ (pp : PParams) (s : CertState) (c : DCert)
166+
→ pots (updateCertDepositsStep pp s c) ≡ updateCertDeposit pp c (pots s)
167+
pots-updateCertDepositsStep pp s c = refl
168+
-- If Agda balks here (because Σ-η isn't kicking in through the `let`-binding
169+
-- in `updateCertDepositsStep`'s definition), fall back to a case split on the
170+
-- seven `DCert` constructors, each closing by `refl`.
171+
```
172+
173+
### Bridging `updateCertDeposits` to the pure pots fold
174+
175+
Captures that `updateCertDeposits` only updates the deposit pots. Induction on
176+
the cert list; per-step we apply the step-level pots equation under `cong`.
177+
178+
```agda
179+
pots-updateCertDeposits :
180+
∀ (pp : PParams) (s : CertState) (cs : List DCert)
181+
→ pots (updateCertDeposits pp s cs) ≡ updateCertDeposit-list pp (pots s) cs
182+
pots-updateCertDeposits pp s [] = refl
183+
pots-updateCertDeposits pp s (c ∷ cs) =
184+
-- After `foldl` unfolding (diff #04):
185+
-- updateCertDeposits pp s (c ∷ cs)
186+
-- = foldl (updateCertDepositsStep pp) s (c ∷ cs)
187+
-- = foldl (updateCertDepositsStep pp) (updateCertDepositsStep pp s c) cs
188+
-- = updateCertDeposits pp (updateCertDepositsStep pp s c) cs
189+
-- so the IH applies at the new initial state `updateCertDepositsStep pp s c`.
190+
trans
191+
(pots-updateCertDeposits pp (updateCertDepositsStep pp s c) cs)
192+
(cong (λ p → updateCertDeposit-list pp p cs)
193+
(pots-updateCertDepositsStep pp s c))
194+
```
195+
196+
### Rule-intrinsic RTC induction
197+
198+
Pots-only form of the main lemma. Mirrors `CERTS-pov`'s structure: empty
199+
chain is `refl`, cons-chain chains the per-step lemma with the IH on the tail.
200+
201+
```agda
202+
CERTS-deposits-updateCertDeposit-list :
203+
{Γ : CertEnv} {s s' : CertState}
204+
→ PoolDepositsAligned (PStateOf s)
205+
→ Γ ⊢ s ⇀⦇ dCerts ,CERTS⦈ s'
206+
→ pots s' ≡ updateCertDeposit-list (PParamsOf Γ) (pots s) dCerts
207+
CERTS-deposits-updateCertDeposit-list _ (BS-base Id-nop) = refl
208+
CERTS-deposits-updateCertDeposit-list
209+
{c ∷ cs} {Γ = Γ} poolInv (BS-ind step rest) =
210+
-- step : Γ ⊢ s ⇀⦇ c ,CERT⦈ s₁
211+
-- rest : Γ ⊢ s₁ ⇀⦇ cs ,CERTS⦈ s'
212+
--
213+
-- pots s'
214+
-- ≡ updateCertDeposit-list pp (pots s₁) cs [IH on `rest`]
215+
-- ≡ updateCertDeposit-list pp (updateCertDeposit pp c (pots s)) cs
216+
-- [cong, per-step lemma]
217+
-- = updateCertDeposit-list pp (pots s) (c ∷ cs) [def. of updateCertDeposit-list]
218+
trans
219+
(CERTS-deposits-updateCertDeposit-list
220+
(PoolDepositsAligned-CERT step poolInv) rest)
221+
(cong (λ p → updateCertDeposit-list (PParamsOf Γ) p cs)
222+
(CERT-deposits-updateCertDeposit poolInv step))
223+
```
224+
225+
### The main `updateCertDeposits`-form lemma
226+
227+
Combines the pots-only RTC induction with the bridge to `updateCertDeposits`.
228+
This is the form `LEDGER-pov` (and the `posNeg-deposits` cancellation) will
229+
actually consume.
230+
231+
```agda
232+
CERTS-deposits-updateCertDeposits :
233+
{Γ : CertEnv} {s s' : CertState}
234+
→ PoolDepositsAligned (PStateOf s)
235+
→ Γ ⊢ s ⇀⦇ dCerts ,CERTS⦈ s'
236+
→ pots s' ≡ pots (updateCertDeposits (PParamsOf Γ) s dCerts)
237+
CERTS-deposits-updateCertDeposits {dCerts} {Γ} {s} poolInv chain =
238+
trans
239+
(CERTS-deposits-updateCertDeposit-list poolInv chain)
240+
(sym (pots-updateCertDeposits (PParamsOf Γ) s dCerts))
241+
```
242+
243+
### Coin corollary
244+
245+
Projection of `CERTS-deposits-updateCertDeposits` to coin. This is the
246+
immediately-useful corollary for `LEDGER-pov`: it gives us a `coinFromDeposits`
247+
equation that matches the `consumed`/`produced` UTxO batch-balance terms (which
248+
are defined via `coinFromDeposits ∘ updateCertDeposits` inside
249+
`newCertDeposits` / `refundCertDeposits`).
250+
251+
```agda
252+
CERTS-coinFromDeposits-updateCertDeposits :
253+
{Γ : CertEnv} {s s' : CertState}
254+
→ PoolDepositsAligned (PStateOf s)
255+
→ Γ ⊢ s ⇀⦇ dCerts ,CERTS⦈ s'
256+
→ coinFromDeposits s' ≡ coinFromDeposits (updateCertDeposits (PParamsOf Γ) s dCerts)
257+
CERTS-coinFromDeposits-updateCertDeposits poolInv chain =
258+
-- `coinFromDeposits` is a function of the pots triple only:
259+
-- coinFromDeposits cs = getCoin (proj₁ (pots cs))
260+
-- + getCoin (proj₁ (proj₂ (pots cs)))
261+
-- + getCoin (proj₂ (proj₂ (pots cs)))
262+
-- so the pots equation transports straight through under `cong`.
263+
cong (λ (a , b , c) → getCoin a + getCoin b + getCoin c)
264+
(CERTS-deposits-updateCertDeposits poolInv chain)
265+
```

‎src/Ledger/Dijkstra/Specification/Certs/Properties/PoVLemmas.lagda.md‎

Lines changed: 94 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -127,3 +127,97 @@ CERT-pov (CERT-pool _) = refl
127127
CERT-pov (CERT-gov _) = refl
128128
```
129129
-->
130+
131+
132+
## The `CERT-deposits-updateCertDeposit` bridging lemma
133+
134+
The `LEDGER-pov` chain needs to relate the **`coinFromDeposits`** of the
135+
post-`CERTS` `CertState` to the **`updateCertDeposits`** closed-form
136+
computation appearing in `consumed`/`produced` via `newCertDeposits` /
137+
`refundCertDeposits` (see `Utxo.lagda.md`). The per-step ingredient is
138+
`CERT-deposits-updateCertDeposit`: for every `CERT` step `Γ ⊢ s ⇀⦇ dCert ,CERT⦈ s'`,
139+
the triple of post-step deposit pots `(DState.deposits, PState.deposits, GState.deposits)`
140+
of `s'` equals `updateCertDeposit (PParamsOf Γ) dCert` applied to the same
141+
triple from `s`.
142+
143+
The case analysis is constructor-for-constructor, mirroring the structure of
144+
`CERT-pov`:
145+
146+
+ `DELEG-delegate`, `DELEG-dereg`, `POOL-reg`, `POOL-retirepool`,
147+
`GOVCERT-regdrep`, `GOVCERT-deregdrep`, `GOVCERT-ccreghot`: each reduces to
148+
`refl`{.AgdaInductiveConstructor} because the rule's pot update and
149+
`updateCertDeposit`'s `case`-branch produce literally the same expression.
150+
+ `POOL-rereg`: the rule leaves `deposits` unchanged, but
151+
`updateCertDeposit (regpool kh _)` produces
152+
`deposits ∪ˡ ❴ kh , pp .poolDeposit ❵`. These agree under the
153+
ledger-wide invariant that every registered pool has a matching deposit
154+
entry — formally, `dom (PoolsOf ps) ⊆ dom (DepositsOf ps)` for the
155+
`PState ps` we are stepping from. Combined with `POOL-rereg`'s premise
156+
`Is-just (isPoolRegistered pools kh)` (i.e., `kh ∈ dom pools`), this gives
157+
`kh ∈ dom deposits`, making the `∪ˡ` a no-op.
158+
159+
The invariant is maintained globally by the ledger (it's a `CHAIN`-level
160+
invariant; see also the `PoolReap.lagda.md` comment about retiring pools
161+
always being registered). We thread it through the lemma as the explicit
162+
predicate `PoolDepositsAligned` (a `PState → Type`).
163+
164+
The lemma also depends on two small set/map facts that we package as
165+
module parameters of `CERT-Deposits-Bridge`:
166+
167+
+ `∪ˡ-singleton-mem-≡`. If `k ∈ dom m` then `m ∪ˡ ❴ k , v ❵ ≡ m` (pure `≡`,
168+
not just `≡ᵉ`). Provable from the left-biased semantics of `∪ˡ`.
169+
+ `Is-just-isPoolRegistered⇒∈-dom`. Standard `Is-just (lookupᵐ? m k) → k ∈ dom m`
170+
for finite maps. Almost certainly already lives in `Axiom.Set.Properties`
171+
or `Interface.HasMap`; if not, a few-line proof from `lookupᵐ?` semantics.
172+
173+
Both are filed as deferred parameters here so the lemma can compile cleanly
174+
now; they should be discharged from the standard map / set libraries when
175+
convenient.
176+
177+
```agda
178+
PoolDepositsAligned : PState → Type
179+
PoolDepositsAligned ps = dom (PoolsOf ps) ⊆ dom (DepositsOf ps)
180+
181+
module CERT-Deposits-Bridge
182+
( ∪ˡ-singleton-mem-≡ :
183+
∀ {A : Type} ⦃ _ : DecEq A ⦄
184+
(m : A ⇀ Coin) (k : A) (v : Coin)
185+
→ k ∈ dom m → m ∪ˡ ❴ k , v ❵ ≡ m )
186+
( Is-just-isPoolRegistered⇒∈-dom :
187+
∀ {pools : Pools} {kh : KeyHash}
188+
→ Is-just (isPoolRegistered pools kh) → kh ∈ dom pools )
189+
where
190+
191+
-- Per-step bridge: the triple of deposit pots after a single `CERT` step
192+
-- equals `updateCertDeposit` applied to the pre-step triple.
193+
CERT-deposits-updateCertDeposit :
194+
{Γ : CertEnv} {s s' : CertState}
195+
→ PoolDepositsAligned (PStateOf s)
196+
→ Γ ⊢ s ⇀⦇ dCert ,CERT⦈ s'
197+
→ ( DepositsOf (DStateOf s')
198+
, DepositsOf (PStateOf s')
199+
, DepositsOf (GStateOf s') )
200+
≡ updateCertDeposit (PParamsOf Γ) dCert
201+
( DepositsOf (DStateOf s)
202+
, DepositsOf (PStateOf s)
203+
, DepositsOf (GStateOf s) )
204+
205+
CERT-deposits-updateCertDeposit _ (CERT-deleg (DELEG-delegate _)) = refl
206+
CERT-deposits-updateCertDeposit _ (CERT-deleg (DELEG-dereg _)) = refl
207+
CERT-deposits-updateCertDeposit _ (CERT-pool (POOL-reg _)) = refl
208+
CERT-deposits-updateCertDeposit
209+
{Γ = Γ} {s = s} poolInv (CERT-pool (POOL-rereg {kh = kh} regd)) =
210+
-- The rule's output pot is `deposits` (unchanged), but `updateCertDeposit`
211+
-- produces `deposits ∪ˡ ❴ kh , pp .poolDeposit ❵`. The pool-deposit
212+
-- invariant `poolInv` plus the rereg premise `regd : Is-just …`
213+
-- give `kh ∈ dom deposits`; `∪ˡ-singleton-mem-≡` then makes the union
214+
-- a no-op.
215+
cong (λ x → ( DepositsOf (DStateOf s) , x , DepositsOf (GStateOf s) ))
216+
(sym (∪ˡ-singleton-mem-≡
217+
(DepositsOf (PStateOf s)) kh _
218+
(poolInv (Is-just-isPoolRegistered⇒∈-dom regd))))
219+
CERT-deposits-updateCertDeposit _ (CERT-pool POOL-retirepool) = refl
220+
CERT-deposits-updateCertDeposit _ (CERT-gov (GOVCERT-regdrep _)) = refl
221+
CERT-deposits-updateCertDeposit _ (CERT-gov (GOVCERT-deregdrep _)) = refl
222+
CERT-deposits-updateCertDeposit _ (CERT-gov (GOVCERT-ccreghot _)) = refl
223+
```

‎src/Ledger/Dijkstra/Specification/Utxo.lagda.md‎

Lines changed: 6 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -292,6 +292,12 @@ collateralCheck pp txTop utxo =
292292

293293
### Governance Proposal Deposits
294294

295+
The closed-form cert-deposit helpers (`updateCertDeposit`, `updateCertDeposits`,
296+
`coinFromDeposits`, `depositsChange`, `newCertDeposits`, `refundCertDeposits`) have
297+
been moved to `Ledger.Dijkstra.Specification.Certs` so that downstream proofs in
298+
`Certs.Properties.PoVLemmas` (parameterised only by `GovStructure`) can reference
299+
them. They are imported here via the open import of `Certs` at the top of this module.
300+
295301
```agda
296302
module _ (pp : PParams) where
297303
govProposalsDeposits : List GovProposal → Coin

0 commit comments

Comments
 (0)