Skip to content

Commit a8d7bf2

Browse files
williamdemeowilliamdemeo
committed
simplify and improve Conway Certs PoV proofs
1 parent 5e41b66 commit a8d7bf2

3 files changed

Lines changed: 51 additions & 71 deletions

File tree

‎src/Ledger/Conway/Conformance/Properties.lagda.md‎

Lines changed: 0 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -124,8 +124,6 @@ module _ (s : ChainState) where
124124
-- Transaction properties
125125
126126
module _ {slot} {tx} (let txb = body tx) (valid : validTxIn₂ s slot tx)
127-
(indexedSum-∪⁺-hom : ∀ {A V : Type} ⦃ _ : DecEq A ⦄ ⦃ _ : DecEq V ⦄ ⦃ mon : CommutativeMonoid 0ℓ 0ℓ V ⦄
128-
→ (d₁ d₂ : A ⇀ V) → indexedSumᵛ' id (d₁ ∪⁺ d₂) ≡ indexedSumᵛ' id d₁ ◇ indexedSumᵛ' id d₂)
129127
(indexedSum-⊆ : ∀ {A : Type} ⦃ _ : DecEq A ⦄ (d d' : A ⇀ ℕ) → d ˢ ⊆ d' ˢ
130128
→ indexedSumᵛ' id d ≤ indexedSumᵛ' id d') -- technically we could use an ordered monoid instead of ℕ
131129
where

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

Lines changed: 5 additions & 12 deletions
Original file line numberDiff line numberDiff line change
@@ -46,19 +46,12 @@ private variable
4646
instance
4747
_ = +-0-monoid
4848
49-
module Certs-PoV ( indexedSumᵛ'-∪' : {A : Type} ⦃ _ : DecEq A ⦄ (m m' : A ⇀ Coin)
50-
→ disjoint (dom m) (dom m')
51-
→ getCoin (m ∪ˡ m') ≡ getCoin m + getCoin m' )
52-
-- TODO: prove some or all of the following assumptions, used in roof of `CERTBASE-pov`.
53-
( sumConstZero' : {A : Type} ⦃ _ : DecEq A ⦄ {X : ℙ A} → getCoin (constMap X 0) ≡ 0 )
54-
( res-decomp' : {A : Type} ⦃ _ : DecEq A ⦄ (m m' : A ⇀ Coin)
55-
→ (m ∪ˡ m')ˢ ≡ᵉ (m ∪ˡ (m' ∣ dom (m ˢ) ᶜ))ˢ )
56-
( getCoin-cong' : {A : Type} ⦃ _ : DecEq A ⦄ (s : A ⇀ Coin) (s' : ℙ (A × Coin)) → s ˢ ≡ᵉ s'
57-
→ indexedSum' proj₂ (s ˢ) ≡ indexedSum' proj₂ s' )
58-
( ≡ᵉ-getCoinˢ' : {A A' : Type} ⦃ _ : DecEq A ⦄ ⦃ _ : DecEq A' ⦄ (s : ℙ (A × Coin)) {f : A → A'}
59-
→ InjectiveOn (dom s) f → getCoin (mapˢ (map₁ f) s) ≡ getCoin s )
49+
module Certs-PoV
50+
-- TODO: prove the following assumption, used in roof of `CERTBASE-pov`.
51+
( ≡ᵉ-getCoinˢ' : {A A' : Type} ⦃ _ : DecEq A ⦄ ⦃ _ : DecEq A' ⦄ (s : ℙ (A × Coin)) {f : A → A'}
52+
→ InjectiveOn (dom s) f → getCoin (mapˢ (map₁ f) s) ≡ getCoin s )
6053
where
61-
open Certs-Pov-lemmas indexedSumᵛ'-∪' sumConstZero' res-decomp' getCoin-cong' ≡ᵉ-getCoinˢ'
54+
open Certs-Pov-lemmas ≡ᵉ-getCoinˢ'
6255
```
6356
-->
6457

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

Lines changed: 46 additions & 57 deletions
Original file line numberDiff line numberDiff line change
@@ -23,7 +23,7 @@ open import Axiom.Set.Properties th
2323
open import Algebra using (CommutativeMonoid)
2424
open import Data.Maybe.Properties
2525
open import Data.Nat.Properties using (+-0-monoid; +-0-commutativeMonoid; +-identityʳ; +-identityˡ)
26-
open import Relation.Binary using (IsEquivalence)
26+
import Relation.Binary as Eq using (IsEquivalence)
2727
open import Relation.Nullary.Decidable
2828
open import Tactic.ReduceDec
2929
@@ -40,12 +40,7 @@ private variable
4040
instance
4141
_ = +-0-monoid
4242
43-
module _ ( indexedSumᵛ'-∪ : {A : Type} ⦃ _ : DecEq A ⦄ (m m' : A ⇀ Coin)
44-
→ disjoint (dom m) (dom m')
45-
→ getCoin (m ∪ˡ m') ≡ getCoin m + getCoin m' )
46-
where
47-
open ≡-Reasoning
48-
open Equivalence
43+
open ≡-Reasoning
4944
```
5045
-->
5146

@@ -60,61 +55,55 @@ some `dcert`{.AgdaBound} : `DCert`{.AgdaDatatype}. Then,
6055
*Formally*.
6156

6257
```agda
63-
CERT-pov : {Γ : CertEnv} {s s' : CertState}
64-
→ Γ ⊢ s ⇀⦇ dCert ,CERT⦈ s'
65-
→ getCoin s ≡ getCoin s'
58+
CERT-pov : {Γ : CertEnv} {s s' : CertState}
59+
→ Γ ⊢ s ⇀⦇ dCert ,CERT⦈ s' → getCoin s ≡ getCoin s'
6660
```
6761

6862
*Proof*. (Click the "Show more Agda" button to reveal the proof.)
6963

7064
<!--
7165
```agda
72-
CERT-pov (CERT-deleg (DELEG-delegate {rwds = rwds} _)) = sym (∪ˡsingleton0≡ rwds)
73-
CERT-pov (CERT-deleg (DELEG-reg {rwds = rwds} _)) = sym (∪ˡsingleton0≡ rwds)
74-
CERT-pov {s = ⟦ _ , stᵖ , stᵍ ⟧ᶜˢ}{⟦ _ , stᵖ' , stᵍ' ⟧ᶜˢ}
75-
(CERT-deleg (DELEG-dereg {c = c} {rwds} {vDelegs = vDelegs}{sDelegs} x)) = begin
76-
getCoin ⟦ ⟦ vDelegs , sDelegs , rwds ⟧ , stᵖ , stᵍ ⟧
77-
≡˘⟨ ≡ᵉ-getCoin rwds-∪ˡ-decomp rwds
78-
( ≡ᵉ.trans rwds-∪ˡ-∪ (≡ᵉ.trans ∪-sym (res-ex-∪ Dec-∈-singleton)) ) ⟩
79-
getCoin rwds-∪ˡ-decomp
80-
≡⟨ ≡ᵉ-getCoin rwds-∪ˡ-decomp ((rwds ∣ ❴ c ❵ ᶜ) ∪ˡ ❴ (c , 0) ❵ᵐ) rwds-∪ˡ≡sing-∪ˡ ⟩
81-
getCoin ((rwds ∣ ❴ c ❵ ᶜ) ∪ˡ ❴ (c , 0) ❵ᵐ )
82-
≡⟨ ∪ˡsingleton0≡ (rwds ∣ ❴ c ❵ ᶜ) ⟩
83-
getCoin ⟦ ⟦ vDelegs ∣ ❴ c ❵ ᶜ , sDelegs ∣ ❴ c ❵ ᶜ , rwds ∣ ❴ c ❵ ᶜ ⟧ , stᵖ' , stᵍ' ⟧
84-
∎
85-
where
86-
module ≡ᵉ = IsEquivalence (≡ᵉ-isEquivalence {Credential × Coin})
87-
rwds-∪ˡ-decomp = (rwds ∣ ❴ c ❵ ᶜ) ∪ˡ (rwds ∣ ❴ c ❵ )
88-
89-
rwds-∪ˡ-∪ : rwds-∪ˡ-decomp ˢ ≡ᵉ (rwds ∣ ❴ c ❵ ᶜ)ˢ ∪ (rwds ∣ ❴ c ❵)ˢ
90-
rwds-∪ˡ-∪ = disjoint-∪ˡ-∪ (disjoint-sym res-ex-disjoint)
91-
92-
disj : disjoint (dom ((rwds ∣ ❴ c ❵ˢ ᶜ) ˢ)) (dom (❴ c , 0 ❵ᵐ ˢ))
93-
disj {a} a∈res a∈dom = res-comp-dom a∈res (dom-single→single a∈dom)
94-
95-
rwds-∪ˡ≡sing-∪ˡ : rwds-∪ˡ-decomp ˢ ≡ᵉ ((rwds ∣ ❴ c ❵ ᶜ) ∪ˡ ❴ (c , 0) ❵ᵐ )ˢ
96-
rwds-∪ˡ≡sing-∪ˡ = ≡ᵉ.trans rwds-∪ˡ-∪
97-
( ≡ᵉ.trans (∪-cong ≡ᵉ.refl (res-singleton'{m = rwds} x))
98-
(≡ᵉ.sym $ disjoint-∪ˡ-∪ disj) )
99-
CERT-pov (CERT-pool x) = refl
100-
CERT-pov (CERT-vdel x) = refl
101-
102-
injOn : (wdls : Withdrawals)
103-
→ ∀[ a ∈ dom (wdls ˢ) ] NetworkIdOf a ≡ NetworkId
104-
→ InjectiveOn (dom (wdls ˢ)) RewardAddress.stake
105-
injOn _ h {record { stake = stakex }} {record { stake = stakey }} x∈ y∈ refl =
106-
cong (λ u → record { net = u ; stake = stakex }) (trans (h x∈) (sym (h y∈)))
107-
108-
module Certs-Pov-lemmas
109-
-- TODO: prove some or all of the following assumptions, used in roof of `CERTBASE-pov`.
110-
( sumConstZero : {A : Type} ⦃ _ : DecEq A ⦄ {X : ℙ A} → getCoin (constMap X 0) ≡ 0 )
111-
( res-decomp : {A : Type} ⦃ _ : DecEq A ⦄ (m m' : A ⇀ Coin)
112-
→ (m ∪ˡ m')ˢ ≡ᵉ (m ∪ˡ (m' ∣ dom (m ˢ) ᶜ))ˢ )
113-
( getCoin-cong : {A : Type} ⦃ _ : DecEq A ⦄ (s : A ⇀ Coin) (s' : ℙ (A × Coin)) → s ˢ ≡ᵉ s'
114-
→ indexedSum' proj₂ (s ˢ) ≡ indexedSum' proj₂ s' )
115-
( ≡ᵉ-getCoinˢ : {A A' : Type} ⦃ _ : DecEq A ⦄ ⦃ _ : DecEq A' ⦄ (s : ℙ (A × Coin)) {f : A → A'}
116-
→ InjectiveOn (dom s) f → getCoin (mapˢ (map₁ f) s) ≡ getCoin s )
117-
where
66+
CERT-pov (CERT-deleg (DELEG-delegate {rwds = rwds} _)) = sym (∪ˡsingleton0≡ rwds)
67+
CERT-pov (CERT-deleg (DELEG-reg {rwds = rwds} _)) = sym (∪ˡsingleton0≡ rwds)
68+
CERT-pov {s = ⟦ _ , stᵖ , stᵍ ⟧ᶜˢ}{⟦ _ , stᵖ' , stᵍ' ⟧ᶜˢ}
69+
(CERT-deleg (DELEG-dereg {c = c} {rwds} {vDelegs = vDelegs}{sDelegs} x)) = begin
70+
getCoin ⟦ ⟦ vDelegs , sDelegs , rwds ⟧ , stᵖ , stᵍ ⟧
71+
≡˘⟨ ≡ᵉ-getCoin rwds-∪ˡ-decomp rwds
72+
( ≡ᵉ.trans rwds-∪ˡ-∪ (≡ᵉ.trans ∪-sym (res-ex-∪ Dec-∈-singleton)) ) ⟩
73+
getCoin rwds-∪ˡ-decomp
74+
≡⟨ ≡ᵉ-getCoin rwds-∪ˡ-decomp ((rwds ∣ ❴ c ❵ ᶜ) ∪ˡ ❴ (c , 0) ❵ᵐ) rwds-∪ˡ≡sing-∪ˡ ⟩
75+
getCoin ((rwds ∣ ❴ c ❵ ᶜ) ∪ˡ ❴ (c , 0) ❵ᵐ )
76+
≡⟨ ∪ˡsingleton0≡ (rwds ∣ ❴ c ❵ ᶜ) ⟩
77+
getCoin ⟦ ⟦ vDelegs ∣ ❴ c ❵ ᶜ , sDelegs ∣ ❴ c ❵ ᶜ , rwds ∣ ❴ c ❵ ᶜ ⟧ , stᵖ' , stᵍ' ⟧
78+
∎
79+
where
80+
module ≡ᵉ = Eq.IsEquivalence (≡ᵉ-isEquivalence {Credential × Coin})
81+
rwds-∪ˡ-decomp = (rwds ∣ ❴ c ❵ ᶜ) ∪ˡ (rwds ∣ ❴ c ❵ )
82+
83+
rwds-∪ˡ-∪ : rwds-∪ˡ-decomp ˢ ≡ᵉ (rwds ∣ ❴ c ❵ ᶜ)ˢ ∪ (rwds ∣ ❴ c ❵)ˢ
84+
rwds-∪ˡ-∪ = disjoint-∪ˡ-∪ (disjoint-sym res-ex-disjoint)
85+
86+
disj : disjoint (dom ((rwds ∣ ❴ c ❵ˢ ᶜ) ˢ)) (dom (❴ c , 0 ❵ᵐ ˢ))
87+
disj {a} a∈res a∈dom = res-comp-dom a∈res (dom-single→single a∈dom)
88+
89+
rwds-∪ˡ≡sing-∪ˡ : rwds-∪ˡ-decomp ˢ ≡ᵉ ((rwds ∣ ❴ c ❵ ᶜ) ∪ˡ ❴ (c , 0) ❵ᵐ )ˢ
90+
rwds-∪ˡ≡sing-∪ˡ = ≡ᵉ.trans rwds-∪ˡ-∪
91+
( ≡ᵉ.trans (∪-cong ≡ᵉ.refl (res-singleton'{m = rwds} x))
92+
(≡ᵉ.sym $ disjoint-∪ˡ-∪ disj) )
93+
CERT-pov (CERT-pool x) = refl
94+
CERT-pov (CERT-vdel x) = refl
95+
96+
injOn : (wdls : Withdrawals)
97+
→ ∀[ a ∈ dom (wdls ˢ) ] NetworkIdOf a ≡ NetworkId
98+
→ InjectiveOn (dom (wdls ˢ)) RewardAddress.stake
99+
injOn _ h {record { stake = stakex }} {record { stake = stakey }} x∈ y∈ refl =
100+
cong (λ u → record { net = u ; stake = stakex }) (trans (h x∈) (sym (h y∈)))
101+
102+
module Certs-Pov-lemmas
103+
-- TODO: prove the following assumption, used in roof of `CERTBASE-pov`.
104+
( ≡ᵉ-getCoinˢ : {A A' : Type} ⦃ _ : DecEq A ⦄ ⦃ _ : DecEq A' ⦄ (s : ℙ (A × Coin)) {f : A → A'}
105+
→ InjectiveOn (dom s) f → getCoin (mapˢ (map₁ f) s) ≡ getCoin s )
106+
where
118107
```
119108
-->
120109

@@ -152,7 +141,7 @@ value of the withdrawals in `Γ`{.AgdaBound}. In other terms,
152141
let
153142
open DState (dState cs )
154143
open DState (dState cs') renaming (rewards to rewards')
155-
module ≡ᵉ = IsEquivalence (≡ᵉ-isEquivalence {Credential × Coin})
144+
module ≡ᵉ = Eq.IsEquivalence (≡ᵉ-isEquivalence {Credential × Coin})
156145
wdrlsCC = mapˢ (map₁ RewardAddress.stake) (wdrls ˢ)
157146
zeroMap = constMap (mapˢ RewardAddress.stake (dom wdrls)) 0
158147
rwds-∪ˡ-decomp = (rewards ∣ dom wdrlsCC ᶜ) ∪ˡ (rewards ∣ dom wdrlsCC)

0 commit comments

Comments
 (0)