Skip to content

Commit fcac7de

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 9018ac5 commit fcac7de

5 files changed

Lines changed: 407 additions & 58 deletions

File tree

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

Lines changed: 95 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -302,6 +302,101 @@ rewardsBalance : DState → Coin
302302
rewardsBalance ds = ∑[ x ← RewardsOf ds ] x
303303
```
304304

305+
306+
## Cert-State Deposit Accounting {#sec:cert-state-deposit-accounting}
307+
308+
The following helpers compute, in closed form, how a list of `DCert`s
309+
affects the three deposit pots (`DState.deposits`, `PState.deposits`,
310+
`GState.deposits`) carried by a `CertState`. They are used by the
311+
`UTXO` batch-balance equation (in `Utxo.lagda.md`) and by the
312+
preservation-of-value proof (in `Ledger.Properties.PoV`); see the
313+
"Design Note: Cert-State Threading and Deposit Accounting" subsection
314+
in `Utxo.lagda.md` for the rationale.
315+
316+
These helpers were previously defined inside the `module _ (pp) (certState)`
317+
block in `Utxo.lagda.md`. They have been hoisted here because they refer
318+
only to `Certs`-level definitions (`PParams`, `DCert`, `CertState`) and
319+
because downstream proofs in `Certs.Properties.PoVLemmas` need to refer
320+
to them while remaining parameterised only over `GovStructure`.
321+
322+
```agda
323+
module _ (pp : PParams) where
324+
325+
-- Closed-form pot evolution for a single `DCert`. This mirrors the
326+
-- deposit-pot evolution that the corresponding `CERT` sub-rule produces;
327+
-- the parallel is made formal by `CERT-deposits-updateCertDeposit` in
328+
-- `Certs.Properties.PoVLemmas`.
329+
--
330+
-- Any drift between this function and the `CERT` sub-rule semantics is a
331+
-- soundness problem: it would allow the UTXO batch-balance equation to
332+
-- accept transactions whose actual `CertState` evolution doesn't balance.
333+
updateCertDeposit : DCert
334+
→ (Credential ⇀ Coin) × (KeyHash ⇀ Coin) × (Credential ⇀ Coin)
335+
→ (Credential ⇀ Coin) × (KeyHash ⇀ Coin) × (Credential ⇀ Coin)
336+
updateCertDeposit cert (depositsᵈ , depositsᵖ , depositsᵍ) =
337+
case cert of λ where
338+
(delegate c _ _ d) → (depositsᵈ ∪⁺ ❴ c , d ❵ , depositsᵖ , depositsᵍ)
339+
(dereg c _ ) → (depositsᵈ ∣ ❴ c ❵ ᶜ , depositsᵖ , depositsᵍ)
340+
(regpool kh _ ) → (depositsᵈ , depositsᵖ ∪ˡ ❴ kh , pp .poolDeposit ❵ , depositsᵍ)
341+
(regdrep c d _ ) → (depositsᵈ , depositsᵖ , depositsᵍ ∪⁺ ❴ c , d ❵)
342+
(deregdrep c _ ) → (depositsᵈ , depositsᵖ , depositsᵍ ∣ ❴ c ❵ ᶜ)
343+
_ → (depositsᵈ , depositsᵖ , depositsᵍ)
344+
345+
-- Per-cert `CertState` step. Extracted as a named function (rather than an
346+
-- inline lambda in `updateCertDeposits`'s fold) so that downstream proofs can
347+
-- state and use the per-step pots equation
348+
-- `pots (updateCertDepositsStep pp s c) ≡ updateCertDeposit pp c (pots s)`
349+
-- in `Certs.Properties.PoV`.
350+
--
351+
-- This function updates only the three deposit pots of its input `CertState`;
352+
-- all other fields (`voteDelegs`, `stakeDelegs`, `rewards`, `pools`, `fPools`,
353+
-- `retiring`, `dreps`, `ccHotKeys`) are inherited unchanged.
354+
updateCertDepositsStep : CertState → DCert → CertState
355+
updateCertDepositsStep certState c =
356+
let open CertState certState
357+
result = updateCertDeposit c
358+
( DepositsOf dState , DepositsOf pState , DepositsOf gState )
359+
in ⟦ record dState { deposits = proj₁ result }
360+
, record pState { deposits = proj₁ (proj₂ result) }
361+
, record gState { deposits = proj₂ (proj₂ result) } ⟧
362+
363+
364+
coinFromDeposits : CertState → Coin
365+
coinFromDeposits certState =
366+
getCoin (DepositsOf (DStateOf certState))
367+
+ getCoin (DepositsOf (PStateOf certState))
368+
+ getCoin (DepositsOf (GStateOf certState))
369+
370+
module _ (pp : PParams) (certState : CertState) where
371+
372+
-- Iterated cert-deposit accounting starting from `certState`. Returns a
373+
-- new `CertState` whose three deposit pots reflect the cumulative effect
374+
-- of the given certificate list; other fields are inherited unchanged from
375+
-- `certState`.
376+
updateCertDeposits : List DCert → CertState
377+
-- The `CERTS` rule processes certificates left-to-right (head first via
378+
-- `BS-ind`). We thread `updateCertDepositsStep` through the cert list in the
379+
-- same direction via `foldl`, which is the order-correct closed form.
380+
--
381+
-- (Previous versions of this definition used `foldr`, which processes the
382+
-- list right-to-left. `foldr` is unsound here because cert operations are
383+
-- not order-independent in general: e.g. `[delegate c d, dereg c (just d)]`
384+
-- for a fresh credential should end with `c ∉ deposits` per `CERTS`, but
385+
-- `foldr` processes `dereg c` first (a no-op on the fresh state) and then
386+
-- `delegate c d`, ending with `c ∈ deposits`.)
387+
updateCertDeposits = foldl (updateCertDepositsStep pp) certState
388+
389+
depositsChange : List DCert → ℤ
390+
depositsChange certs = coinFromDeposits (updateCertDeposits certs) - coinFromDeposits certState
391+
392+
newCertDeposits : List DCert → Coin
393+
newCertDeposits certs = posPart (depositsChange certs)
394+
395+
refundCertDeposits : List DCert → Coin
396+
refundCertDeposits certs = negPart (depositsChange certs)
397+
```
398+
399+
305400
<!--
306401
```agda
307402
instance

‎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+
```

0 commit comments

Comments
 (0)