Skip to content

Commit f8a60cf

Browse files
williamdemeowilliamdemeo
committed
CIP-159-11: Initial PoV property module skeletons (#1123)
Add preservation-of-value property modules for the Dijkstra era, adapted from the Conway PoV proof structure for CIP-159 (partial withdrawals and direct deposits). New modules: - Certs.Properties.PoVLemmas: CERT-pov, POST-CERT-pov, sts-pov, PRE-CERT-pov (adapted for applyWithdrawals subtraction semantics) - Certs.Properties.PoV: CERTS-pov top-level theorem - Certs.Properties.ApplyWithdrawalsPov: Key new lemma showing applyWithdrawals decreases rewardsBalance by exactly getCoin wdrls - Ledger.Properties.PoV: HasCoin instances, LEDGER-pov statement with proof sketch for direct deposit cancellation Design notes: - PRE-CERT-pov delegates to applyWithdrawals-pov (fold induction) instead of Conway's constMap/res-decomp/sumConstZero chain - LEDGER-pov identifies the applyDirectDeposits cancellation as the main new proof obligation vs Conway - applyWithdrawals-pov is structured as three layers: single-step (applyOne-pov), fold induction (foldl-applyOne-pov), top-level Status: Skeleton with holes; does not yet fully typecheck.
1 parent 88b4874 commit f8a60cf

4 files changed

Lines changed: 646 additions & 0 deletions

File tree

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

Lines changed: 257 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,257 @@
1+
---
2+
source_branch: master
3+
source_path: src/Ledger/Dijkstra/Specification/Certs/Properties/ApplyWithdrawalsPoV.lagda.md
4+
---
5+
6+
7+
# `applyWithdrawals` Preservation of Value {#sec:apply-withdrawals-pov}
8+
9+
This module proves that `applyWithdrawals` decreases the total rewards balance
10+
by exactly the sum of the withdrawal amounts. This is the key new lemma
11+
for the Dijkstra (CIP-159) CERTS preservation-of-value proof.
12+
13+
## Proof Strategy
14+
15+
`applyWithdrawals` is defined as a `foldl` over the list representation of the
16+
withdrawal map. The proof proceeds by induction on this list, with a single-step
17+
lemma showing that each `applyOne` step decreases `getCoin` by exactly the
18+
withdrawal amount.
19+
20+
The single-step argument decomposes the accumulator map `acc` into:
21+
`acc ≡ᵉ (acc ∣ ❴ c ❵ ᶜ) ∪ˡ (acc ∣ ❴ c ❵)`
22+
where `c = stake addr`. When `lookupᵐ? acc c ≡ just bal` and `amt ≤ bal`:
23+
`getCoin acc = getCoin (acc ∣ ❴ c ❵ ᶜ) + bal`, by decomposition;
24+
`getCoin (applyOne acc (addr , amt))` = `getCoin (❴ c , bal ∸ amt ❵ ∪ˡ (acc ∣ ❴ c ❵ ᶜ))`
25+
= `(bal ∸ amt) + getCoin (acc ∣ ❴ c ❵ ᶜ)`, by disjoint union.
26+
27+
So the decrease is `bal - (bal ∸ amt) = amt` (since `amt ≤ bal`).
28+
29+
For the fold induction, the invariant is maintained because:
30+
- Each credential is targeted at most once (by injectivity of `stake` on `dom wdrls`,
31+
which follows from the `NetworkId` constraint).
32+
- `applyOne` preserves domain membership (it replaces entries, never removes them).
33+
- Therefore, remaining entries still have their credentials registered and their
34+
amounts bounded by the (unchanged) balances.
35+
36+
<!--
37+
```agda
38+
{-# OPTIONS --safe #-}
39+
40+
open import Ledger.Dijkstra.Specification.Gov.Base using (GovStructure)
41+
42+
module Ledger.Dijkstra.Specification.Certs.Properties.ApplyWithdrawalsPoV
43+
(gs : GovStructure) (open GovStructure gs) where
44+
45+
open import Ledger.Dijkstra.Specification.Certs gs
46+
open import Ledger.Dijkstra.Specification.Gov.Actions gs hiding (yes; no)
47+
open import Ledger.Prelude
48+
open import Axiom.Set.Properties th
49+
open import Data.Nat.Properties
50+
using ( +-0-monoid; +-identityʳ; +-identityˡ; +-comm; +-assoc
51+
; m∸n+n≡m )
52+
open import Relation.Binary using (IsEquivalence)
53+
54+
open RewardAddress
55+
56+
private variable
57+
A : Type
58+
59+
instance
60+
_ = +-0-monoid
61+
```
62+
-->
63+
64+
## Module parameters
65+
66+
We parameterize over the standard finite-map sum lemmas (same pattern as Conway).
67+
68+
<!--
69+
```agda
70+
module ApplyWithdrawals-PoV
71+
( indexedSumᵛ'-∪ : {A : Type} ⦃ _ : DecEq A ⦄ (m m' : A ⇀ Coin)
72+
→ disjoint (dom m) (dom m')
73+
→ getCoin (m ∪ˡ m') ≡ getCoin m + getCoin m' )
74+
( getCoin-cong : {A : Type} ⦃ _ : DecEq A ⦄ (s : A ⇀ Coin) (s' : ℙ (A × Coin))
75+
→ s ˢ ≡ᵉ s' → indexedSum' proj₂ (s ˢ) ≡ indexedSum' proj₂ s' )
76+
where
77+
open ≡-Reasoning
78+
open Equivalence
79+
module ≡ᵉ = IsEquivalence (≡ᵉ-isEquivalence {Credential × Coin})
80+
```
81+
-->
82+
83+
## Single-step lemma: `applyOne` decreases `getCoin` by `amt`
84+
85+
When `stake addr ∈ dom acc` and `amt ≤ bal` (where `bal` is the current balance),
86+
applying a single withdrawal decreases the total by exactly `amt`.
87+
88+
```agda
89+
applyOne-pov :
90+
(acc : Rewards) (addr : RewardAddress) (amt bal : Coin)
91+
→ lookupᵐ? acc (stake addr) ≡ just bal
92+
→ amt ≤ bal
93+
→ getCoin acc ≡ getCoin (❴ stake addr , bal ∸ amt ❵ ∪ˡ (acc ∣ ❴ stake addr ❵ ᶜ)) + amt
94+
```
95+
96+
<!--
97+
```agda
98+
applyOne-pov acc addr amt bal lookup-eq amt≤bal = {!!}
99+
-- Proof sketch:
100+
--
101+
-- getCoin acc
102+
-- ≡ getCoin (acc ∣ ❴ c ❵ ᶜ) + getCoin (acc ∣ ❴ c ❵)
103+
-- -- by: acc ≡ᵉ (acc ∣ ❴ c ❵ ᶜ) ∪ (acc ∣ ❴ c ❵), then indexedSumᵛ'-∪
104+
-- ≡ getCoin (acc ∣ ❴ c ❵ ᶜ) + bal
105+
-- -- by: getCoin-cong on (acc ∣ ❴ c ❵) ≡ᵉ ❴ c , bal ❵ (from lookup-eq)
106+
-- ≡ getCoin (acc ∣ ❴ c ❵ ᶜ) + (bal ∸ amt + amt)
107+
-- -- by: m∸n+n≡m amt≤bal
108+
-- ≡ (bal ∸ amt) + getCoin (acc ∣ ❴ c ❵ ᶜ) + amt
109+
-- -- by: +-comm, +-assoc
110+
-- ≡ getCoin (❴ c , bal ∸ amt ❵ ∪ˡ (acc ∣ ❴ c ❵ ᶜ)) + amt
111+
-- -- by: indexedSumᵛ'-∪ (disjoint since c ∉ dom (acc ∣ ❴ c ❵ ᶜ))
112+
-- where c = stake addr
113+
```
114+
-->
115+
116+
## Fold invariant
117+
118+
The fold invariant tracks three properties through the induction:
119+
120+
1. All remaining withdrawal credentials are in the current accumulator's domain.
121+
2. All remaining withdrawal amounts are bounded by the current balances.
122+
3. Each credential appears at most once in the remaining list (NoDup on credentials).
123+
124+
<!--
125+
```agda
126+
-- The fold invariant for the induction.
127+
--
128+
-- After processing some prefix of withdrawals, the remaining suffix still
129+
-- has all its credentials registered in the accumulator, with amounts bounded
130+
-- by current (possibly reduced) balances.
131+
--
132+
-- The NoDup condition ensures each credential is targeted at most once,
133+
-- which is critical: applyOne replaces (not removes) the entry, so other
134+
-- credentials' balances are unchanged, but the same credential's balance
135+
-- IS reduced. NoDup guarantees we never revisit a reduced balance.
136+
--
137+
-- NoDup on (mapˢ (stake ∘ proj₁) entries) follows from injectivity of
138+
-- `stake` on `dom wdrls`, which follows from the NetworkId constraint.
139+
```
140+
-->
141+
142+
## Main lemma: fold over the full list
143+
144+
```agda
145+
applyOne : Rewards → RewardAddress × Coin → Rewards
146+
applyOne ac (addr , amt) =
147+
case lookupᵐ? ac (stake addr) of λ where
148+
(just bal) → ❴ stake addr , bal ∸ amt ❵ ∪ˡ (ac ∣ ❴ stake addr ❵ ᶜ)
149+
nothing → ac
150+
151+
foldl-applyOne-pov :
152+
(acc : Rewards) (entries : List (RewardAddress × Coin))
153+
→ (∀ {addr amt} → (addr , amt) ∈ˡ entries
154+
→ stake addr ∈ dom acc
155+
× amt ≤ maybe id 0 (lookupᵐ? acc (stake addr)))
156+
-- → NoDup (map (stake ∘ proj₁) entries) -- needed for invariant preservation
157+
→ getCoin acc ≡ getCoin (foldl applyOne acc entries) + sum (map proj₂ entries)
158+
```
159+
160+
<!--
161+
```agda
162+
foldl-applyOne-pov = {!!}
163+
-- Proof by induction on entries:
164+
--
165+
-- Base case (entries = []):
166+
-- getCoin acc ≡ getCoin acc + 0 -- by +-identityʳ
167+
--
168+
-- Step case (entries = (addr , amt) ∷ rest):
169+
-- Let acc' = applyOne acc (addr , amt).
170+
-- By the invariant, stake addr ∈ dom acc and amt ≤ bal.
171+
-- So lookupᵐ? acc (stake addr) ≡ just bal for some bal.
172+
--
173+
-- (1) applyOne-pov gives:
174+
-- getCoin acc ≡ getCoin acc' + amt
175+
--
176+
-- (2) For the IH, we need the invariant for (acc', rest).
177+
-- - Domain: applyOne replaces the entry for `stake addr`,
178+
-- so all credentials remain in dom acc'. For credentials
179+
-- ≠ stake addr, the complement restriction preserves them.
180+
-- - Bounds: Since NoDup ensures `stake addr` does not appear
181+
-- again in rest, remaining entries target different credentials
182+
-- whose balances are unchanged by applyOne.
183+
--
184+
-- (3) IH on (acc', rest) gives:
185+
-- getCoin acc' ≡ getCoin (foldl applyOne acc' rest) + sum (map proj₂ rest)
186+
--
187+
-- (4) Combining (1) and (3):
188+
-- getCoin acc
189+
-- ≡ getCoin acc' + amt
190+
-- ≡ getCoin (foldl applyOne acc' rest) + sum (map proj₂ rest) + amt
191+
-- ≡ getCoin (foldl applyOne acc ((addr,amt) ∷ rest)) + (amt + sum (map proj₂ rest))
192+
-- ≡ getCoin (foldl applyOne acc ((addr,amt) ∷ rest)) + sum (map proj₂ ((addr,amt) ∷ rest))
193+
```
194+
-->
195+
196+
## Top-level lemma
197+
198+
This is the form needed by `PRE-CERT-pov`.
199+
200+
```agda
201+
applyWithdrawals-pov :
202+
(wdrls : Withdrawals) (rwds : Rewards)
203+
→ mapˢ stake (dom wdrls) ⊆ dom rwds
204+
→ (∀[ (addr , amt) ∈ wdrls ˢ ] amt ≤ maybe id 0 (lookupᵐ? rwds (stake addr)))
205+
→ getCoin rwds ≡ getCoin (applyWithdrawals wdrls rwds) + getCoin wdrls
206+
```
207+
208+
<!--
209+
```agda
210+
applyWithdrawals-pov = {!!}
211+
-- Proof:
212+
--
213+
-- applyWithdrawals wdrls rwds = foldl applyOne rwds (setToList (wdrls ˢ))
214+
--
215+
-- Apply foldl-applyOne-pov with acc = rwds, entries = setToList (wdrls ˢ).
216+
--
217+
-- The preconditions of foldl-applyOne-pov follow from:
218+
-- - Domain membership: from `mapˢ stake (dom wdrls) ⊆ dom rwds`
219+
-- - Amount bounds: from the second precondition
220+
-- - NoDup: from injectivity of `stake` on `dom wdrls`
221+
-- (which follows from the NetworkId constraint, established in PRE-CERT-pov)
222+
--
223+
-- The remaining step is to relate:
224+
-- sum (map proj₂ (setToList (wdrls ˢ))) ≡ getCoin wdrls
225+
--
226+
-- This holds because getCoin for a finite map is defined as
227+
-- indexedSumᵛ' which sums over the set representation, and
228+
-- summing proj₂ over the list representation of the same set
229+
-- gives the same result (by properties of setToList/indexedSum).
230+
```
231+
-->
232+
233+
## Supporting lemmas (to be proved)
234+
235+
The following auxiliary properties are needed but not yet proved.
236+
They are standard finite-map facts independent of CIP-159.
237+
238+
```agda
239+
-- applyOne preserves domain membership for other credentials.
240+
Claim-applyOne-dom-preserve :
241+
∀ (acc : Rewards) (addr : RewardAddress) (amt : Coin) (c : Credential)
242+
→ c ∈ dom acc → c ≢ stake addr
243+
→ c ∈ dom (case lookupᵐ? acc (stake addr) of λ where
244+
(just bal) → ❴ stake addr , bal ∸ amt ❵ ∪ˡ (acc ∣ ❴ stake addr ❵ ᶜ)
245+
nothing → acc)
246+
Claim-applyOne-dom-preserve = {!!}
247+
248+
-- applyOne preserves balance for other credentials.
249+
Claim-applyOne-balance-preserve :
250+
∀ (acc : Rewards) (addr : RewardAddress) (amt : Coin) (c : Credential)
251+
→ c ≢ stake addr
252+
→ lookupᵐ? (case lookupᵐ? acc (stake addr) of λ where
253+
(just bal) → ❴ stake addr , bal ∸ amt ❵ ∪ˡ (acc ∣ ❴ stake addr ❵ ᶜ)
254+
nothing → acc) c
255+
≡ lookupᵐ? acc c
256+
Claim-applyOne-balance-preserve = {!!}
257+
```

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

Lines changed: 64 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,64 @@
1+
---
2+
source_branch: master
3+
source_path: src/Ledger/Dijkstra/Specification/Certs/Properties/PoV.lagda.md
4+
---
5+
6+
# CERTS: Preservation of Value {#sec:certs-pov}
7+
8+
<!--
9+
```agda
10+
{-# OPTIONS --safe #-}
11+
12+
open import Ledger.Dijkstra.Specification.Gov.Base using (GovStructure)
13+
14+
module Ledger.Dijkstra.Specification.Certs.Properties.PoV
15+
(gs : GovStructure) (open GovStructure gs) where
16+
17+
open import Ledger.Dijkstra.Specification.Certs gs
18+
open import Ledger.Dijkstra.Specification.Certs.Properties.PoVLemmas gs
19+
open import Ledger.Dijkstra.Specification.Gov.Actions gs hiding (yes; no)
20+
open import Ledger.Prelude
21+
open import Data.Nat.Properties using (+-0-monoid)
22+
23+
open CertState
24+
25+
private variable
26+
l : List DCert
27+
28+
instance
29+
_ = +-0-monoid
30+
31+
module Certs-PoV
32+
( indexedSumᵛ'-∪' : {A : Type} ⦃ _ : DecEq A ⦄ (m m' : A ⇀ Coin)
33+
→ disjoint (dom m) (dom m')
34+
→ getCoin (m ∪ˡ m') ≡ getCoin m + getCoin m' )
35+
( applyWithdrawals-pov' :
36+
(wdrls : Withdrawals) (rwds : Rewards)
37+
→ mapˢ RewardAddress.stake (dom wdrls) ⊆ dom rwds
38+
→ (∀[ (addr , amt) ∈ wdrls ˢ ]
39+
amt ≤ maybe id 0 (lookupᵐ? rwds (RewardAddress.stake addr)))
40+
→ getCoin rwds ≡ getCoin (applyWithdrawals wdrls rwds) + getCoin wdrls )
41+
( ≡ᵉ-getCoinˢ' :
42+
{A A' : Type} ⦃ _ : DecEq A ⦄ ⦃ _ : DecEq A' ⦄
43+
(s : ℙ (A × Coin)) {f : A → A'}
44+
→ InjectiveOn (dom s) f
45+
→ getCoin (mapˢ (map₁ f) s) ≡ getCoin s )
46+
where
47+
open Certs-Pov-lemmas indexedSumᵛ'-∪' applyWithdrawals-pov' ≡ᵉ-getCoinˢ'
48+
```
49+
-->
50+
51+
## Theorem: The `CERTS` rule preserves value {#thm:CERTS-PoV}
52+
53+
```agda
54+
CERTS-pov : {Γ : CertEnv} {s₁ sₙ : CertState}
55+
→ ∀[ a ∈ dom (WithdrawalsOf Γ) ] NetworkIdOf a ≡ NetworkId
56+
→ Γ ⊢ s₁ ⇀⦇ l ,CERTS⦈ sₙ
57+
→ getCoin s₁ ≡ getCoin sₙ + getCoin (WithdrawalsOf Γ)
58+
```
59+
60+
```agda
61+
CERTS-pov {Γ = Γ} validNetId (run (pre-cert , certs)) =
62+
trans (PRE-CERT-pov validNetId pre-cert)
63+
(cong (_+ getCoin (WithdrawalsOf Γ)) {!!}) -- (sts-pov certs))
64+
```

0 commit comments

Comments
 (0)