PoVLemmas
Lemma (The CERT rule preserves value).
Informally.
Let s, s' be CertStates such that
s ⇀⦇ dcert ,CERT⦈ s' for
some dcert : DCert. Then,
getCoin s \(≡\) getCoin s'.
Formally.
CERT-pov : {Γ : CertEnv} {s s' : CertState} → Γ ⊢ s ⇀⦇ dCert ,CERT⦈ s' → getCoin s ≡ getCoin s'
Proof.
CERT-pov (CERT-deleg (DELEG-delegate {rwds = rwds} _)) = sym (∪ˡsingleton0≡ rwds) CERT-pov (CERT-deleg (DELEG-reg {rwds = rwds} _)) = sym (∪ˡsingleton0≡ rwds) CERT-pov {s = $\begin{pmatrix} \,\htmlId{2975}{\htmlClass{Symbol}{\text{\_}}}\, \\ \,\href{Ledger.Conway.Specification.Certs.Properties.PoVLemmas.html#2979}{\htmlId{2979}{\htmlClass{Bound}{\text{stᵖ}}}}\, \\ \,\href{Ledger.Conway.Specification.Certs.Properties.PoVLemmas.html#2985}{\htmlId{2985}{\htmlClass{Bound}{\text{stᵍ}}}}\, \end{pmatrix}$}{$\begin{pmatrix} \,\htmlId{2996}{\htmlClass{Symbol}{\text{\_}}}\, \\ \,\href{Ledger.Conway.Specification.Certs.Properties.PoVLemmas.html#3000}{\htmlId{3000}{\htmlClass{Bound}{\text{stᵖ'}}}}\, \\ \,\href{Ledger.Conway.Specification.Certs.Properties.PoVLemmas.html#3007}{\htmlId{3007}{\htmlClass{Bound}{\text{stᵍ'}}}}\, \end{pmatrix}$} (CERT-deleg (DELEG-dereg {c = c} {rwds} {vDelegs = vDelegs}{sDelegs} x)) = begin getCoin $\begin{pmatrix} \begin{pmatrix} \,\href{Ledger.Conway.Specification.Certs.Properties.PoVLemmas.html#3072}{\htmlId{3118}{\htmlClass{Bound}{\text{vDelegs}}}}\, \\ \,\href{Ledger.Conway.Specification.Certs.Properties.PoVLemmas.html#3081}{\htmlId{3128}{\htmlClass{Bound}{\text{sDelegs}}}}\, \\ \,\href{Ledger.Conway.Specification.Certs.Properties.PoVLemmas.html#3055}{\htmlId{3138}{\htmlClass{Bound}{\text{rwds}}}}\, \end{pmatrix} \\ \,\href{Ledger.Conway.Specification.Certs.Properties.PoVLemmas.html#2979}{\htmlId{3147}{\htmlClass{Bound}{\text{stᵖ}}}}\, \\ \,\href{Ledger.Conway.Specification.Certs.Properties.PoVLemmas.html#2985}{\htmlId{3153}{\htmlClass{Bound}{\text{stᵍ}}}}\, \end{pmatrix}$ ≡˘⟨ ≡ᵉ-getCoin rwds-∪ˡ-decomp rwds ( ≡ᵉ.trans rwds-∪ˡ-∪ (≡ᵉ.trans ∪-sym (res-ex-∪ Dec-∈-singleton)) ) ⟩ getCoin rwds-∪ˡ-decomp ≡⟨ ≡ᵉ-getCoin rwds-∪ˡ-decomp ((rwds ∣ ❴ c ❵ ᶜ) ∪ˡ ❴ (c , 0) ❵ᵐ) rwds-∪ˡ≡sing-∪ˡ ⟩ getCoin ((rwds ∣ ❴ c ❵ ᶜ) ∪ˡ ❴ (c , 0) ❵ᵐ ) ≡⟨ ∪ˡsingleton0≡ (rwds ∣ ❴ c ❵ ᶜ) ⟩ getCoin $\begin{pmatrix} \begin{pmatrix} \,\href{Ledger.Conway.Specification.Certs.Properties.PoVLemmas.html#3072}{\htmlId{3501}{\htmlClass{Bound}{\text{vDelegs}}}}\, \,\href{Axiom.Set.Map.html#13604}{\htmlId{3509}{\htmlClass{Function Operator}{\text{∣}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{3511}{\htmlClass{Field Operator}{\text{❴}}}}\, \,\href{Ledger.Conway.Specification.Certs.Properties.PoVLemmas.html#3051}{\htmlId{3513}{\htmlClass{Bound}{\text{c}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{3515}{\htmlClass{Field Operator}{\text{❵}}}}\, \,\href{Axiom.Set.Map.html#13604}{\htmlId{3517}{\htmlClass{Function Operator}{\text{ᶜ}}}}\, \\ \,\href{Ledger.Conway.Specification.Certs.Properties.PoVLemmas.html#3081}{\htmlId{3521}{\htmlClass{Bound}{\text{sDelegs}}}}\, \,\href{Axiom.Set.Map.html#13604}{\htmlId{3529}{\htmlClass{Function Operator}{\text{∣}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{3531}{\htmlClass{Field Operator}{\text{❴}}}}\, \,\href{Ledger.Conway.Specification.Certs.Properties.PoVLemmas.html#3051}{\htmlId{3533}{\htmlClass{Bound}{\text{c}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{3535}{\htmlClass{Field Operator}{\text{❵}}}}\, \,\href{Axiom.Set.Map.html#13604}{\htmlId{3537}{\htmlClass{Function Operator}{\text{ᶜ}}}}\, \\ \,\href{Ledger.Conway.Specification.Certs.Properties.PoVLemmas.html#3055}{\htmlId{3541}{\htmlClass{Bound}{\text{rwds}}}}\, \,\href{Axiom.Set.Map.html#13604}{\htmlId{3546}{\htmlClass{Function Operator}{\text{∣}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{3548}{\htmlClass{Field Operator}{\text{❴}}}}\, \,\href{Ledger.Conway.Specification.Certs.Properties.PoVLemmas.html#3051}{\htmlId{3550}{\htmlClass{Bound}{\text{c}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{3552}{\htmlClass{Field Operator}{\text{❵}}}}\, \,\href{Axiom.Set.Map.html#13604}{\htmlId{3554}{\htmlClass{Function Operator}{\text{ᶜ}}}}\, \end{pmatrix} \\ \,\href{Ledger.Conway.Specification.Certs.Properties.PoVLemmas.html#3000}{\htmlId{3560}{\htmlClass{Bound}{\text{stᵖ'}}}}\, \\ \,\href{Ledger.Conway.Specification.Certs.Properties.PoVLemmas.html#3007}{\htmlId{3567}{\htmlClass{Bound}{\text{stᵍ'}}}}\, \end{pmatrix}$ ∎ where module ≡ᵉ = IsEquivalence (≡ᵉ-isEquivalence {Credential × Coin}) rwds-∪ˡ-decomp = (rwds ∣ ❴ c ❵ ᶜ) ∪ˡ (rwds ∣ ❴ c ❵ ) rwds-∪ˡ-∪ : rwds-∪ˡ-decomp ˢ ≡ᵉ (rwds ∣ ❴ c ❵ ᶜ)ˢ ∪ (rwds ∣ ❴ c ❵)ˢ rwds-∪ˡ-∪ = disjoint-∪ˡ-∪ (disjoint-sym res-ex-disjoint) disj : disjoint (dom ((rwds ∣ ❴ c ❵ˢ ᶜ) ˢ)) (dom (❴ c , 0 ❵ᵐ ˢ)) disj {a} a∈res a∈dom = res-comp-dom a∈res (dom-single→single a∈dom) rwds-∪ˡ≡sing-∪ˡ : rwds-∪ˡ-decomp ˢ ≡ᵉ ((rwds ∣ ❴ c ❵ ᶜ) ∪ˡ ❴ (c , 0) ❵ᵐ )ˢ rwds-∪ˡ≡sing-∪ˡ = ≡ᵉ.trans rwds-∪ˡ-∪ ( ≡ᵉ.trans (∪-cong ≡ᵉ.refl (res-singleton'{m = rwds} x)) (≡ᵉ.sym $ disjoint-∪ˡ-∪ disj) ) CERT-pov (CERT-pool x) = refl CERT-pov (CERT-vdel x) = refl injOn : (wdls : Withdrawals) → ∀[ a ∈ dom (wdls ˢ) ] NetworkIdOf a ≡ NetworkId → InjectiveOn (dom (wdls ˢ)) RwdAddr.stake injOn _ h {record { stake = stakex }} {record { stake = stakey }} x∈ y∈ refl = cong (λ u → record { net = u ; stake = stakex }) (trans (h x∈) (sym (h y∈))) module Certs-Pov-lemmas -- TODO: prove some or all of the following assumptions, used in roof of `CERTBASE-pov`. ( sumConstZero : {A : Type} ⦃ _ : DecEq A ⦄ {X : ℙ A} → getCoin (constMap X 0) ≡ 0 ) ( res-decomp : {A : Type} ⦃ _ : DecEq A ⦄ (m m' : A ⇀ Coin) → (m ∪ˡ m')ˢ ≡ᵉ (m ∪ˡ (m' ∣ dom (m ˢ) ᶜ))ˢ ) ( getCoin-cong : {A : Type} ⦃ _ : DecEq A ⦄ (s : A ⇀ Coin) (s' : ℙ (A × Coin)) → s ˢ ≡ᵉ s' → indexedSum' proj₂ (s ˢ) ≡ indexedSum' proj₂ s' ) ( ≡ᵉ-getCoinˢ : {A A' : Type} ⦃ _ : DecEq A ⦄ ⦃ _ : DecEq A' ⦄ (s : ℙ (A × Coin)) {f : A → A'} → InjectiveOn (dom s) f → getCoin (mapˢ (map₁ f) s) ≡ getCoin s ) where
Lemma (PRE-CERT rule preserves value).
Informally.
Let Γ : CertEnv be a certificate environment, and let
s, s' : CertState be certificate states such that
s ⇀⦇ _ ,PRE-CERT⦈ s'.
Then, the value of s is equal to the value of s' plus the
value of the withdrawals in Γ. In other terms,
getCoin s \(≡\) getCoin s' + getCoin (Γ .wdrls ).
Formally.
PRE-CERT-pov : {Γ : CertEnv} {s s' : CertState} → ∀[ a ∈ dom (CertEnv.wdrls Γ) ] NetworkIdOf a ≡ NetworkId → Γ ⊢ s ⇀⦇ _ ,PRE-CERT⦈ s' → getCoin s ≡ getCoin s' + getCoin (CertEnv.wdrls Γ)
Proof.
PRE-CERT-pov {Γ = Γ}
{s = cs}
{s' = cs'}
validNetId
(CERT-pre {pp}{vs}{e}{dreps}{wdrls} (_ , wdrlsCC⊆rwds)) =
let
open DState (dState cs )
open DState (dState cs') renaming (rewards to rewards')
module ≡ᵉ = IsEquivalence (≡ᵉ-isEquivalence {Credential × Coin})
wdrlsCC = mapˢ (map₁ RwdAddr.stake) (wdrls ˢ)
zeroMap = constMap (mapˢ RwdAddr.stake (dom wdrls)) 0
rwds-∪ˡ-decomp = (rewards ∣ dom wdrlsCC ᶜ) ∪ˡ (rewards ∣ dom wdrlsCC)
in
begin
getCoin rewards
≡˘⟨ ≡ᵉ-getCoin rwds-∪ˡ-decomp rewards
( ≡ᵉ.trans (disjoint-∪ˡ-∪ (disjoint-sym res-ex-disjoint))
(≡ᵉ.trans ∪-sym (res-ex-∪ (_∈? dom wdrlsCC))) ) ⟩
getCoin rwds-∪ˡ-decomp
≡⟨ indexedSumᵛ'-∪ (rewards ∣ dom wdrlsCC ᶜ) (rewards ∣ dom wdrlsCC)
(disjoint-sym res-ex-disjoint) ⟩
getCoin (rewards ∣ dom wdrlsCC ᶜ) + getCoin (rewards ∣ dom wdrlsCC )
≡⟨ cong (getCoin (rewards ∣ dom wdrlsCC ᶜ) +_)
( getCoin-cong (rewards ∣ dom wdrlsCC) wdrlsCC (res-subset{m = rewards} wdrlsCC⊆rwds) ) ⟩
getCoin (rewards ∣ dom wdrlsCC ᶜ) + getCoin wdrlsCC
≡⟨ cong (getCoin (rewards ∣ dom wdrlsCC ᶜ) +_) (≡ᵉ-getCoinˢ (wdrls ˢ) (injOn wdrls validNetId)) ⟩
getCoin (rewards ∣ dom wdrlsCC ᶜ) + getCoin wdrls
≡˘⟨ cong (_+ getCoin wdrls)
( begin
getCoin (zeroMap ∪ˡ rewards)
≡⟨ ≡ᵉ-getCoin (zeroMap ∪ˡ rewards) (zeroMap ∪ˡ (rewards ∣ dom zeroMap ᶜ))
(res-decomp zeroMap rewards) ⟩
getCoin (zeroMap ∪ˡ (rewards ∣ dom zeroMap ᶜ))
≡⟨ indexedSumᵛ'-∪ zeroMap (rewards ∣ dom zeroMap ᶜ)
(disjoint-sym res-comp-dom) ⟩
getCoin zeroMap + getCoin (rewards ∣ dom zeroMap ᶜ)
≡⟨ cong (λ u → u + getCoin (rewards ∣ dom zeroMap ᶜ)) sumConstZero ⟩
0 + getCoin (rewards ∣ (dom zeroMap) ᶜ)
≡⟨ +-identityˡ (getCoin (rewards ∣ dom zeroMap ᶜ)) ⟩
getCoin (rewards ∣ dom zeroMap ᶜ)
≡⟨ ≡ᵉ-getCoin (rewards ∣ dom zeroMap ᶜ) (rewards ∣ dom wdrlsCC ᶜ)
( res-comp-cong
( ⊆-Transitive (proj₁ constMap-dom) (proj₂ dom-mapˡ≡map-dom)
, ⊆-Transitive (proj₁ dom-mapˡ≡map-dom) (proj₂ constMap-dom) ) ) ⟩
getCoin (rewards ∣ dom wdrlsCC ᶜ)
∎ ) ⟩
getCoin (zeroMap ∪ˡ rewards) + getCoin wdrls
∎
Lemma (POST-CERT rule preserves value).
Informally.
Let Γ : CertEnv be a certificate environment, and let
s, s' : CertState be certificate states such that
s ⇀⦇ _ ,POST-CERT⦈ s'.
Then, the value of s is equal to the value of s'.
In other terms,
getCoin s \(≡\) getCoin s'.
Formally.
POST-CERT-pov : {Γ : CertEnv} {s s' : CertState} → Γ ⊢ s ⇀⦇ _ ,POST-CERT⦈ s' → getCoin s ≡ getCoin s'
Proof.
POST-CERT-pov CERT-post = refl
Lemma (iteration of CERT rule preserves value).
Informally. Let l be a list of DCerts, and let
s₁, sₙ be CertStates such that, starting
with s₁ and successively applying the CERT rule to with
DCerts from the list l, we obtain sₙ.
Then, the value of s₁ is equal to the value of sₙ.
Formally.
sts-pov : {Γ : CertEnv} {s₁ sₙ : CertState} {sigs : List DCert} → RunTraceAndThen _⊢_⇀⦇_,CERT⦈_ _⊢_⇀⦇_,POST-CERT⦈_ Γ s₁ sigs sₙ → getCoin s₁ ≡ getCoin sₙ
Proof.
sts-pov (run-[] x) = POST-CERT-pov x sts-pov (run-∷ x xs) = trans (CERT-pov x) (sts-pov xs)