PoVLemmas
Theorem: The CERT rule preserves value
{-# OPTIONS --safe #-}
open import Ledger.Conway.Specification.Gov.Base
module Ledger.Conway.Specification.Certs.Properties.PoVLemmas ( gs : _) ( open GovStructure gs ) where
open import Ledger.Conway.Specification.Certs gs
open import Ledger.Conway.Specification.Gov.Actions gs hiding ( yes ; no )
open import Ledger.Prelude
open import Axiom.Set.Properties th
open import Algebra using ( CommutativeMonoid )
open import Data.Maybe.Properties
open import Data.Nat.Properties using ( +-0-monoid ; +-0-commutativeMonoid ; +-identityʳ ; +-identityˡ )
import Relation.Binary as Eq using ( IsEquivalence )
open import Relation.Nullary.Decidable
open import Tactic.ReduceDec
open Computational ⦃...⦄
open import stdlib-meta.Tactic.GenError using ( genErrors )
open CertState
private variable
dCert : DCert
l : List DCert
A A' B : Type
instance
_ = +-0-monoid
open ≡-Reasoning
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 . (Click the "Show more Agda" button to reveal the 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{1816}{\htmlClass{Symbol}{\text{\_}}}\, \\ \,\href{Ledger.Conway.Specification.Certs.Properties.PoVLemmas.html#1820}{\htmlId{1820}{\htmlClass{Bound}{\text{stᵖ}}}}\, \\ \,\href{Ledger.Conway.Specification.Certs.Properties.PoVLemmas.html#1826}{\htmlId{1826}{\htmlClass{Bound}{\text{stᵍ}}}}\, \end{pmatrix}$ }{ $\begin{pmatrix} \,\htmlId{1837}{\htmlClass{Symbol}{\text{\_}}}\, \\ \,\href{Ledger.Conway.Specification.Certs.Properties.PoVLemmas.html#1841}{\htmlId{1841}{\htmlClass{Bound}{\text{stᵖ'}}}}\, \\ \,\href{Ledger.Conway.Specification.Certs.Properties.PoVLemmas.html#1848}{\htmlId{1848}{\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#1911}{\htmlId{1955}{\htmlClass{Bound}{\text{vDelegs}}}}\, \\ \,\href{Ledger.Conway.Specification.Certs.Properties.PoVLemmas.html#1920}{\htmlId{1965}{\htmlClass{Bound}{\text{sDelegs}}}}\, \\ \,\href{Ledger.Conway.Specification.Certs.Properties.PoVLemmas.html#1894}{\htmlId{1975}{\htmlClass{Bound}{\text{rwds}}}}\, \end{pmatrix} \\ \,\href{Ledger.Conway.Specification.Certs.Properties.PoVLemmas.html#1820}{\htmlId{1984}{\htmlClass{Bound}{\text{stᵖ}}}}\, \\ \,\href{Ledger.Conway.Specification.Certs.Properties.PoVLemmas.html#1826}{\htmlId{1990}{\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#1911}{\htmlId{2324}{\htmlClass{Bound}{\text{vDelegs}}}}\, \,\href{Axiom.Set.Map.html#13606}{\htmlId{2332}{\htmlClass{Function Operator}{\text{∣}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{2334}{\htmlClass{Field Operator}{\text{❴}}}}\, \,\href{Ledger.Conway.Specification.Certs.Properties.PoVLemmas.html#1890}{\htmlId{2336}{\htmlClass{Bound}{\text{c}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{2338}{\htmlClass{Field Operator}{\text{❵}}}}\, \,\href{Axiom.Set.Map.html#13606}{\htmlId{2340}{\htmlClass{Function Operator}{\text{ᶜ}}}}\, \\ \,\href{Ledger.Conway.Specification.Certs.Properties.PoVLemmas.html#1920}{\htmlId{2344}{\htmlClass{Bound}{\text{sDelegs}}}}\, \,\href{Axiom.Set.Map.html#13606}{\htmlId{2352}{\htmlClass{Function Operator}{\text{∣}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{2354}{\htmlClass{Field Operator}{\text{❴}}}}\, \,\href{Ledger.Conway.Specification.Certs.Properties.PoVLemmas.html#1890}{\htmlId{2356}{\htmlClass{Bound}{\text{c}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{2358}{\htmlClass{Field Operator}{\text{❵}}}}\, \,\href{Axiom.Set.Map.html#13606}{\htmlId{2360}{\htmlClass{Function Operator}{\text{ᶜ}}}}\, \\ \,\href{Ledger.Conway.Specification.Certs.Properties.PoVLemmas.html#1894}{\htmlId{2364}{\htmlClass{Bound}{\text{rwds}}}}\, \,\href{Axiom.Set.Map.html#13606}{\htmlId{2369}{\htmlClass{Function Operator}{\text{∣}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{2371}{\htmlClass{Field Operator}{\text{❴}}}}\, \,\href{Ledger.Conway.Specification.Certs.Properties.PoVLemmas.html#1890}{\htmlId{2373}{\htmlClass{Bound}{\text{c}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{2375}{\htmlClass{Field Operator}{\text{❵}}}}\, \,\href{Axiom.Set.Map.html#13606}{\htmlId{2377}{\htmlClass{Function Operator}{\text{ᶜ}}}}\, \end{pmatrix} \\ \,\href{Ledger.Conway.Specification.Certs.Properties.PoVLemmas.html#1841}{\htmlId{2383}{\htmlClass{Bound}{\text{stᵖ'}}}}\, \\ \,\href{Ledger.Conway.Specification.Certs.Properties.PoVLemmas.html#1848}{\htmlId{2390}{\htmlClass{Bound}{\text{stᵍ'}}}}\, \end{pmatrix}$
∎
where
module ≡ᵉ = Eq.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 ( GOVCERT-regdrep _)) = refl
CERT-pov ( CERT-vdel ( GOVCERT-deregdrep _)) = refl
CERT-pov ( CERT-vdel ( GOVCERT-ccreghot _)) = refl
injOn : ( wdls : Withdrawals )
→ ∀[ a ∈ dom ( wdls ˢ ) ] NetworkIdOf a ≡ NetworkId
→ InjectiveOn ( dom ( wdls ˢ )) RewardAddress.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
( ≡ᵉ-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 . (Click the "Show more Agda" button to reveal the 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 ≡ᵉ = Eq.IsEquivalence ( ≡ᵉ-isEquivalence { Credential × Coin })
wdrlsCC = mapˢ ( map₁ RewardAddress.stake ) ( wdrls ˢ )
zeroMap = constMap ( mapˢ RewardAddress.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 (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 }
→ ReflexiveTransitiveClosure { sts = _⊢_⇀⦇_,CERT⦈_ } Γ s₁ sigs sₙ
→ getCoin s₁ ≡ getCoin sₙ
Proof .
sts-pov ( BS-base Id-nop ) = refl
sts-pov ( BS-ind x xs ) = trans ( CERT-pov x ) ( sts-pov xs )