Skip to content

Commit 9c64cfb

Browse files
williamdemeowilliamdemeo
committed
Add ENTITIES preservation-of-value
Step 4 of the LEDGER preservation-of-value plan (#1187). Chains the three lemmas already proved in steps 2-3 over the single ENTITIES constructor: applyWithdrawals-pov on (wdrls, r₀) CERTS-pov on the inner ⟦ ... ,CERTS⦈ premise applyDirectDeposits-pov on (dd, r₁) The resulting equation is the value-flow statement for the whole rule: getCoin s + getCoin (DirectDepositsOf Γ) ≡ getCoin s' + getCoin (WithdrawalsOf Γ) ENTITIES-pov takes the two per-batch NetworkId witnesses as separate arguments, mirroring extract-netId's output in the old #1190 LEDGER-pov proof. These witnesses are produced at the call site by the SUBUTXOW/UTXOW step and threaded into ENTITIES-pov from there. The module ENTITIES-PoV inherits and re-exports the three set/map parameters of ApplyToRewards-PoV (∪ˡ-lookup-preserve, sum-map-proj₂≡getCoin, setToList-Unique), to be discharged in a follow-up. Also adds a top-level Entities.Properties module that re-exports the two property submodules, matching the existing Certs.Properties convention.
1 parent 7f267f4 commit 9c64cfb

4 files changed

Lines changed: 170 additions & 6 deletions

File tree

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

Lines changed: 9 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -33,6 +33,15 @@ DirectDeposits : Type
3333
DirectDeposits = RewardAddress ⇀ Coin
3434
```
3535

36+
<!--
37+
```agda
38+
record HasDirectDeposits {a} (A : Type a) : Type a where
39+
field DirectDepositsOf : A → DirectDeposits
40+
open HasDirectDeposits ⦃...⦄ public
41+
```
42+
-->
43+
44+
3645
## Balance Intervals {#sec:balance-intervals}
3746

3847
[CIP 159][] allows a transaction to assert that an account's balance falls within a

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

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -192,6 +192,9 @@ instance
192192
HasWithdrawals-CertEnv : HasWithdrawals CertEnv
193193
HasWithdrawals-CertEnv .WithdrawalsOf = CertEnv.wdrls
194194
195+
HasDirectDeposits-CertEnv : HasDirectDeposits CertEnv
196+
HasDirectDeposits-CertEnv .DirectDepositsOf = CertEnv.directDeposits
197+
195198
HasVoteDelegs-DState : HasVoteDelegs DState
196199
HasVoteDelegs-DState .VoteDelegsOf = DState.voteDelegs
197200

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

Lines changed: 158 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,13 +1,169 @@
11
---
22
source_branch: master
3-
source_path: src/Ledger/Dijkstra/Specification/Entitities/Properties/PoV.lagda.md
3+
source_path: src/Ledger/Dijkstra/Specification/Entities/Properties/PoV.lagda.md
44
---
55

6+
# Properties of `ENTITIES`: Preservation of Value {#thm:ENTITIES-PoV}
7+
8+
This module proves preservation of value for the `ENTITIES`{.AgdaDatatype} rule
9+
introduced in [CIP-159-11d][PR-1201]. In the Dijkstra era, `ENTITIES`{.AgdaDatatype}
10+
wraps the inner `CERTS`{.AgdaDatatype} step with per-transaction withdrawal- and
11+
direct-deposit-handling: withdrawals are applied to the rewards balance *before*
12+
`CERTS`{.AgdaDatatype}, direct deposits *after*. The value-flow equation captures
13+
the net effect of all three components on `getCoin (CertState)`:
14+
15+
getCoin s + getCoin (DirectDepositsOf Γ) ≡ getCoin s' + getCoin (WithdrawalsOf Γ)
16+
17+
Intuitively, the deposits added on the right are matched by the withdrawals removed
18+
on the left — they "pass through" the rule.
19+
20+
## Proof Strategy
21+
22+
Case-split on the single `ENTITIES`{.AgdaInductiveConstructor} constructor to expose
23+
the three internal phases. Letting `r₀`{.AgdaBound} denote the initial rewards map
24+
and `r₁`{.AgdaBound} the rewards map after `CERTS`{.AgdaDatatype}, the equational
25+
chain is
26+
27+
+ `applyWithdrawals-pov`{.AgdaFunction} on `(wdrls, r₀)` rewrites `getCoin r₀` as
28+
`getCoin (applyWithdrawals wdrls r₀) + getCoin wdrls`.
29+
+ `CERTS-pov`{.AgdaFunction} on the inner step rewrites
30+
`getCoin (applyWithdrawals wdrls r₀)` as `getCoin r₁` (the rewards balance is
31+
preserved by the closure of `CERT`{.AgdaDatatype}).
32+
+ `applyDirectDeposits-pov`{.AgdaFunction} on `(dd, r₁)` rewrites
33+
`getCoin (applyDirectDeposits dd r₁)` as `getCoin r₁ + getCoin dd`.
34+
35+
The three rewrites compose into the desired equation modulo associativity and
36+
commutativity of `+` on `Coin`.
37+
38+
[PR-1201]: https://github.com/IntersectMBO/formal-ledger-specifications/pull/1201
39+
40+
<!--
641
```agda
742
{-# OPTIONS --safe #-}
843
944
open import Ledger.Dijkstra.Specification.Gov.Base using (GovStructure)
1045
1146
module Ledger.Dijkstra.Specification.Entities.Properties.PoV
12-
(govStructure : GovStructure) where
47+
(gs : GovStructure) (open GovStructure gs) where
48+
49+
open import Ledger.Prelude
50+
open import Ledger.Dijkstra.Specification.Account gs -- using (DirectDeposits)
51+
open import Ledger.Dijkstra.Specification.Certs gs
52+
open import Ledger.Dijkstra.Specification.Entities gs
53+
open import Ledger.Dijkstra.Specification.Gov.Actions gs hiding (yes; no)
54+
55+
open import Ledger.Dijkstra.Specification.Certs.Properties.PoV gs
56+
open import Ledger.Dijkstra.Specification.Entities.Properties.ApplyToRewardsPoV gs
57+
58+
open import Data.List.Relation.Unary.Unique.Propositional using (Unique)
59+
open import Data.Nat.Properties using (+-comm; +-assoc; +-0-monoid)
60+
61+
open RewardAddress
62+
open ≡-Reasoning
63+
64+
private variable
65+
A : Type
66+
dCerts : List DCert
67+
68+
instance
69+
_ = +-0-monoid
1370
```
71+
-->
72+
73+
## The `ENTITIES-pov` module
74+
75+
`ENTITIES-pov`{.AgdaFunction} inherits the three set/map module parameters of
76+
`ApplyToRewards-PoV`{.AgdaModule} — they are needed by
77+
`applyWithdrawals-pov`{.AgdaFunction} and `applyDirectDeposits-pov`{.AgdaFunction} —
78+
and threads them through unchanged.
79+
80+
```agda
81+
module ENTITIES-PoV
82+
( ∪ˡ-lookup-preserve :
83+
(m : Rewards) (c : Credential) (v : Coin) (c' : Credential)
84+
→ c' ≢ c → lookupᵐ? (❴ c , v ❵ ∪ˡ m) c' ≡ lookupᵐ? m c' )
85+
86+
( sum-map-proj₂≡getCoin :
87+
(m : RewardAddress ⇀ Coin)
88+
→ sum (map proj₂ (setToList (m ˢ))) ≡ getCoin m )
89+
90+
( setToList-Unique :
91+
(m : RewardAddress ⇀ Coin)
92+
→ ∀[ a ∈ dom (m ˢ) ] NetworkIdOf a ≡ NetworkId
93+
→ Unique (map (stake ∘ proj₁) (setToList (m ˢ))) )
94+
where
95+
open ApplyToRewards-PoV ∪ˡ-lookup-preserve sum-map-proj₂≡getCoin setToList-Unique public
96+
```
97+
98+
## The `ENTITIES-pov` theorem
99+
100+
**Informally**. Let `s`{.AgdaBound}, `s'`{.AgdaBound} be `CertStates`{.AgdaRecord}
101+
related by `ENTITIES`{.AgdaDatatype} under some `CertEnv`{.AgdaRecord}
102+
`Γ`{.AgdaBound}, and let `wd-netId`{.AgdaBound} and `dd-netId`{.AgdaBound} be the
103+
per-batch `NetworkId`{.AgdaFunction} witnesses for `WithdrawalsOf Γ`{.AgdaBound} and
104+
`DirectDepositsOf Γ`{.AgdaBound} (produced at the call site by the
105+
`SUBUTXOW`{.AgdaDatatype} or `UTXOW`{.AgdaDatatype} step). Then,
106+
107+
getCoin s + getCoin (DirectDepositsOf Γ) ≡ getCoin s' + getCoin (WithdrawalsOf Γ)
108+
109+
**Formally**.
110+
111+
```agda
112+
ENTITIES-pov : {Γ : CertEnv} {s s' : CertState}
113+
→ ∀[ a ∈ dom (WithdrawalsOf Γ) ] NetworkIdOf a ≡ NetworkId
114+
→ ∀[ a ∈ dom (DirectDepositsOf Γ) ] NetworkIdOf a ≡ NetworkId
115+
→ Γ ⊢ s ⇀⦇ dCerts ,ENTITIES⦈ s'
116+
→ getCoin s + getCoin (DirectDepositsOf Γ) ≡ getCoin s' + getCoin (WithdrawalsOf Γ)
117+
```
118+
119+
**Proof**. Case-split on the single `ENTITIES`{.AgdaInductiveConstructor}
120+
constructor to expose the inner `CERTS`{.AgdaDatatype} step and the threaded states.
121+
122+
<!--
123+
```agda
124+
ENTITIES-pov {Γ = Γ}
125+
{s = ⟦ ⟦ _ , _ , r₀ , _ ⟧ᵈ , _ , _ ⟧ᶜˢ} {s' = ⟦ ⟦ _ , _ , _ , _ ⟧ᵈ , _ , _ ⟧ᶜˢ}
126+
wd-netId dd-netId (ENTITIES { rewards₁ = r₁ } (fst , wdrls⊆ , amts≤ , certsStep , ddCreds⊆ )) =
127+
begin
128+
G r₀ + DD
129+
≡⟨ cong (_+ DD) (applyWithdrawals-pov wdrls r₀ wdrls⊆ wd-netId amts≤) ⟩
130+
(G aw + W) + DD
131+
≡⟨ +-assoc (G aw) W DD ⟩
132+
G aw + (W + DD)
133+
≡⟨ cong (G aw +_) (+-comm W DD) ⟩
134+
G aw + (DD + W)
135+
≡˘⟨ +-assoc (G aw) DD W ⟩
136+
(G aw + DD) + W
137+
≡⟨ cong (λ x → (x + DD) + W) (CERTS-pov certsStep) ⟩
138+
(G r₁ + DD) + W
139+
≡˘⟨ cong (_+ W) (applyDirectDeposits-pov dd r₁ ddCreds⊆) ⟩
140+
G (applyDirectDeposits dd r₁) + W
141+
∎
142+
where
143+
wdrls : Withdrawals
144+
wdrls = WithdrawalsOf Γ
145+
dd : DirectDeposits
146+
dd = CertEnv.directDeposits Γ
147+
aw : Rewards
148+
aw = applyWithdrawals wdrls r₀
149+
G : Rewards → Coin
150+
G = getCoin
151+
W DD : Coin
152+
W = getCoin wdrls
153+
DD = getCoin dd
154+
```
155+
-->
156+
157+
The first three rewrites move `W` past `DD` to set up the
158+
`CERTS-pov`{.AgdaFunction} application; the `CERTS-pov`{.AgdaFunction}
159+
step then preserves `getCoin`{.AgdaFunction} through the inner closure;
160+
and the final rewrite folds `applyDirectDeposits`{.AgdaFunction} back
161+
into the LHS of the goal.
162+
163+
Equivalences used implicitly: under
164+
`HasCoin-CertState`{.AgdaFunction}, `getCoin (CertState) ≡ getCoin (rewards ∘ DStateOf)`,
165+
which is why `G r₀`, `G aw`, `G r₁`, and `G (applyDirectDeposits dd r₁)`
166+
are interchangeable with `getCoin s`, `getCoin <intermediate>`,
167+
`getCoin <post-CERTS>`, and `getCoin s'` respectively — both sides
168+
project to the `rewards`{.AgdaField} field, which is exactly what the
169+
chain manipulates.

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

Lines changed: 0 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -416,10 +416,6 @@ could be either of them.
416416
field CurrentTreasuryOf : A → Maybe Coin
417417
open HasCurrentTreasury ⦃...⦄ public
418418
419-
record HasDirectDeposits {a} (A : Type a) : Type a where
420-
field DirectDepositsOf : A → DirectDeposits
421-
open HasDirectDeposits ⦃...⦄ public
422-
423419
record HasBalanceIntervals {a} (A : Type a) : Type a where
424420
field BalanceIntervalsOf : A → AccountBalanceIntervals
425421
open HasBalanceIntervals ⦃...⦄ public

0 commit comments

Comments
 (0)