Skip to content

Commit a5d4885

Browse files
williamdemeowilliamdemeo
committed
[Dijkstra] Certs PoV: discharge the five CERTS-side LEDGER-PoV parameters
Certs.Properties.PoVLemmas proves the per-CERT-step facts: rewards preservation, closed-form deposit accounting under PoolDepositsRegistered, preservation of that invariant, and the pool-set tracking of the newCertDeposits fold (via seed-certificate shift lemmas, a ∷-split, and ≡ᵉ-congruence in the pool-set argument), plus refundCertDeposits-++. Certs.Properties.PoV lifts these along the reflexive-transitive closure, with statements matching the LEDGER-PoV module parameters verbatim: CERTS-rewards-pov, CERTS-deposits-pov, CERTS-deposits-registered, CERTS-new-thread, refundCertDeposits-++. AI-assisted: Claude Fable 5 (Anthropic)
1 parent dbab7ef commit a5d4885

3 files changed

Lines changed: 590 additions & 0 deletions

File tree

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

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -14,4 +14,6 @@ module Ledger.Dijkstra.Specification.Certs.Properties where
1414

1515
```agda
1616
open import Ledger.Dijkstra.Specification.Certs.Properties.Computational
17+
open import Ledger.Dijkstra.Specification.Certs.Properties.PoVLemmas
18+
open import Ledger.Dijkstra.Specification.Certs.Properties.PoV
1719
```

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

Lines changed: 166 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,166 @@
1+
# `CERTS`{.AgdaDatatype} Properties: Preservation of Value {#sec:certs-pov}
2+
3+
This module provides the `CERTS`{.AgdaDatatype}-level value-accounting facts
4+
consumed by `Ledger.Properties.PoV`{.AgdaModule}: it discharges the
5+
`CERTS-rewards-pov`, `CERTS-deposits-pov`, `CERTS-deposits-registered`,
6+
`CERTS-new-thread` and `refundCertDeposits-++` module parameters of the
7+
`LEDGER-PoV`{.AgdaModule} consumer, with statements matching those parameters
8+
verbatim.
9+
10+
`CERTS`{.AgdaDatatype} is the reflexive–transitive closure of the
11+
single-certificate rule `CERT`{.AgdaDatatype}, so each fact is an induction
12+
over the closure whose step case is the corresponding per-step lemma of
13+
`Certs.Properties.PoVLemmas`{.AgdaModule}. Composing the deposit facts across
14+
steps rests on the pool-set threading explained there: peeling the first
15+
certificate off `newCertDeposits`{.AgdaFunction}
16+
(`newCertDeposits-∷`{.AgdaFunction}) leaves the tail charged against the
17+
evolved accumulator, which `CERT-poolSet`{.AgdaFunction} identifies — up to
18+
extensional equality, absorbed by `newCertDeposits-cong`{.AgdaFunction} — with
19+
the pool set of the state after the step.
20+
21+
<!--
22+
```agda
23+
{-# OPTIONS --safe #-}
24+
25+
open import Ledger.Dijkstra.Specification.Gov.Base using (GovStructure)
26+
27+
module Ledger.Dijkstra.Specification.Certs.Properties.PoV
28+
(gs : GovStructure) (open GovStructure gs) where
29+
30+
open import Data.Nat.Properties using (+-assoc; +-comm)
31+
32+
open import Ledger.Prelude
33+
open import Ledger.Dijkstra.Specification.Gov.Actions gs hiding (yes; no)
34+
open import Ledger.Dijkstra.Specification.Certs gs
35+
36+
open import Ledger.Dijkstra.Specification.Certs.Properties.PoVLemmas gs
37+
hiding (refundCertDeposits-++)
38+
open import Ledger.Dijkstra.Specification.Certs.Properties.PoVLemmas gs
39+
using (refundCertDeposits-++) public
40+
41+
open import Interface.STS
42+
43+
open ≡-Reasoning
44+
```
45+
-->
46+
47+
## Rewards preservation
48+
49+
A `CERTS`{.AgdaDatatype} run leaves the rewards balance unchanged, by chaining
50+
`CERT-rewards-pov`{.AgdaFunction} along the closure.
51+
52+
```agda
53+
CERTS-rewards-pov : {Γ : CertEnv} {s s' : CertState} {dCerts : List DCert}
54+
→ Γ ⊢ s ⇀⦇ dCerts ,CERTS⦈ s' → coinFromRewards s ≡ coinFromRewards s'
55+
CERTS-rewards-pov (BS-base Id-nop) = refl
56+
CERTS-rewards-pov (BS-ind step rest) =
57+
trans (CERT-rewards-pov step) (CERTS-rewards-pov rest)
58+
```
59+
60+
## Preservation of the pool-deposit registration invariant
61+
62+
```agda
63+
CERTS-deposits-registered : {Γ : CertEnv} {s s' : CertState} {dCerts : List DCert}
64+
→ PoolDepositsRegistered s
65+
→ Γ ⊢ s ⇀⦇ dCerts ,CERTS⦈ s'
66+
→ PoolDepositsRegistered s'
67+
CERTS-deposits-registered reg (BS-base Id-nop) = reg
68+
CERTS-deposits-registered reg (BS-ind step rest) =
69+
CERTS-deposits-registered (CERT-deposits-registered reg step) rest
70+
```
71+
72+
## Splitting `newCertDeposits`{.AgdaFunction} at a run boundary
73+
74+
For a `CERTS`{.AgdaDatatype} run followed by further certificates
75+
`ys`{.AgdaBound}, the new-deposit total splits at the boundary, with the
76+
trailing certificates charged against the run's *final* pool set. This is
77+
what lets per-step accounting compose across a batch.
78+
79+
```agda
80+
CERTS-new-thread : {Γ : CertEnv} {s s' : CertState} {dCerts : List DCert}
81+
→ Γ ⊢ s ⇀⦇ dCerts ,CERTS⦈ s'
82+
→ (ys : List DCert)
83+
→ newCertDeposits (PParamsOf Γ) (dom (PoolsOf s)) (dCerts ++ ys)
84+
≡ newCertDeposits (PParamsOf Γ) (dom (PoolsOf s)) dCerts
85+
+ newCertDeposits (PParamsOf Γ) (dom (PoolsOf s')) ys
86+
CERTS-new-thread (BS-base Id-nop) ys = refl
87+
CERTS-new-thread {Γ = Γ} (BS-ind {s = s₀} {sig = c} {s' = s₁} {sigs = cs} {s'' = s₂} step rest) ys =
88+
begin
89+
nc P₀ (c ∷ (cs ++ ys))
90+
≡⟨ newCertDeposits-∷ pp P₀ c (cs ++ ys) ⟩
91+
nc P₀ (c ∷ []) + nc (nextPools P₀ c) (cs ++ ys)
92+
≡⟨ cong (nc P₀ (c ∷ []) +_) (newCertDeposits-cong pp (cs ++ ys) (CERT-poolSet step)) ⟩
93+
nc P₀ (c ∷ []) + nc P₁ (cs ++ ys)
94+
≡⟨ cong (nc P₀ (c ∷ []) +_) (CERTS-new-thread rest ys) ⟩
95+
nc P₀ (c ∷ []) + (nc P₁ cs + nc P₂ ys)
96+
≡˘⟨ +-assoc (nc P₀ (c ∷ [])) (nc P₁ cs) (nc P₂ ys) ⟩
97+
nc P₀ (c ∷ []) + nc P₁ cs + nc P₂ ys
98+
≡˘⟨ cong (_+ nc P₂ ys) (head-split step) ⟩
99+
nc P₀ (c ∷ cs) + nc P₂ ys
100+
∎
101+
where
102+
pp = PParamsOf Γ
103+
nc = newCertDeposits pp
104+
P₀ = dom (PoolsOf s₀)
105+
P₁ = dom (PoolsOf s₁)
106+
P₂ = dom (PoolsOf s₂)
107+
108+
head-split : Γ ⊢ s₀ ⇀⦇ c ,CERT⦈ s₁ → nc P₀ (c ∷ cs) ≡ nc P₀ (c ∷ []) + nc P₁ cs
109+
head-split st = trans (newCertDeposits-∷ pp P₀ c cs)
110+
(cong (nc P₀ (c ∷ []) +_) (newCertDeposits-cong pp cs (CERT-poolSet st)))
111+
```
112+
113+
## Closed-form deposit accounting
114+
115+
Over a `CERTS`{.AgdaDatatype} run from a state satisfying
116+
`PoolDepositsRegistered`{.AgdaFunction}, the deposit pots satisfy
117+
*pre + new ≡ post + refunds* in the closed form of the `UTXO`{.AgdaDatatype}
118+
batch balance. The step case splits the new-deposit total as above, applies
119+
the per-step accounting, and recombines the refunds with
120+
`refundCertDeposits-++`{.AgdaFunction}; the invariant is threaded through the
121+
run by `CERT-deposits-registered`{.AgdaFunction}.
122+
123+
```agda
124+
CERTS-deposits-pov : {Γ : CertEnv} {s s' : CertState} {dCerts : List DCert}
125+
→ PoolDepositsRegistered s
126+
→ Γ ⊢ s ⇀⦇ dCerts ,CERTS⦈ s'
127+
→ coinFromDeposits s + newCertDeposits (PParamsOf Γ) (dom (PoolsOf s)) dCerts
128+
≡ coinFromDeposits s' + refundCertDeposits (PParamsOf Γ) dCerts
129+
CERTS-deposits-pov _ (BS-base Id-nop) = refl
130+
CERTS-deposits-pov {Γ = Γ} reg (BS-ind {s = s₀} {sig = c} {s' = s₁} {sigs = cs} {s'' = s₂} step rest) =
131+
begin
132+
D₀ + nc P₀ (c ∷ cs)
133+
≡⟨ cong (D₀ +_) (trans (newCertDeposits-∷ pp P₀ c cs)
134+
(cong (nc P₀ (c ∷ []) +_)
135+
(newCertDeposits-cong pp cs (CERT-poolSet step)))) ⟩
136+
D₀ + (nc P₀ (c ∷ []) + nc P₁ cs)
137+
≡˘⟨ +-assoc D₀ (nc P₀ (c ∷ [])) (nc P₁ cs) ⟩
138+
D₀ + nc P₀ (c ∷ []) + nc P₁ cs
139+
≡⟨ cong (_+ nc P₁ cs) (CERT-deposits-pov reg step) ⟩
140+
D₁ + refund (c ∷ []) + nc P₁ cs
141+
≡⟨ +-assoc D₁ (refund (c ∷ [])) (nc P₁ cs) ⟩
142+
D₁ + (refund (c ∷ []) + nc P₁ cs)
143+
≡⟨ cong (D₁ +_) (+-comm (refund (c ∷ [])) (nc P₁ cs)) ⟩
144+
D₁ + (nc P₁ cs + refund (c ∷ []))
145+
≡˘⟨ +-assoc D₁ (nc P₁ cs) (refund (c ∷ [])) ⟩
146+
D₁ + nc P₁ cs + refund (c ∷ [])
147+
≡⟨ cong (_+ refund (c ∷ []))
148+
(CERTS-deposits-pov (CERT-deposits-registered reg step) rest) ⟩
149+
D₂ + refund cs + refund (c ∷ [])
150+
≡⟨ +-assoc D₂ (refund cs) (refund (c ∷ [])) ⟩
151+
D₂ + (refund cs + refund (c ∷ []))
152+
≡⟨ cong (D₂ +_) (+-comm (refund cs) (refund (c ∷ []))) ⟩
153+
D₂ + (refund (c ∷ []) + refund cs)
154+
≡˘⟨ cong (D₂ +_) (refundCertDeposits-++ pp (c ∷ []) cs) ⟩
155+
D₂ + refund (c ∷ cs)
156+
∎
157+
where
158+
pp = PParamsOf Γ
159+
nc = newCertDeposits pp
160+
refund = refundCertDeposits pp
161+
D₀ = coinFromDeposits s₀
162+
D₁ = coinFromDeposits s₁
163+
D₂ = coinFromDeposits s₂
164+
P₀ = dom (PoolsOf s₀)
165+
P₁ = dom (PoolsOf s₁)
166+
```

0 commit comments

Comments
 (0)