Certs
{-# OPTIONS --safe #-}
open import Ledger.Prelude
open import Ledger.Conway.Specification.Gov.Base
import Ledger.Conway.Specification.Certs
module Ledger.Conway.Conformance.Certs
(gs : _) (open GovStructure gs)
where
open import Ledger.Conway.Specification.Gov.Actions gs
private module Certs = Ledger.Conway.Specification.Certs gs
open Certs public
hiding (DState; GState; CertState; HasCast-DState; HasCast-GState; HasCast-CertState;
_⊢_⇀⦇_,POOL⦈_; _⊢_⇀⦇_,DELEG⦈_; _⊢_⇀⦇_,GOVCERT⦈_;
_⊢_⇀⦇_,CERT⦈_; _⊢_⇀⦇_,CERTBASE⦈_; _⊢_⇀⦇_,CERTS⦈_; ⟦_,_,_⟧ᵈ)
open RwdAddr
record DState : Type where
constructor ⟦_,_,_,_⟧ᵈ
field
voteDelegs : Credential ⇀ VDeleg
stakeDelegs : Credential ⇀ KeyHash
rewards : Credential ⇀ Coin
deposits : Deposits
record GState : Type where
constructor ⟦_,_,_⟧ᵛ
field
dreps : Credential ⇀ Epoch
ccHotKeys : Credential ⇀ Maybe Credential
deposits : Deposits
record CertState : Type where
constructor ⟦_,_,_⟧ᶜˢ
field
dState : DState
pState : PState
gState : GState
instance
unquoteDecl HasCast-DState HasCast-GState HasCast-CertState = derive-HasCast
( (quote DState , HasCast-DState)
∷ (quote GState , HasCast-GState)
∷ [ (quote CertState , HasCast-CertState) ])
certDeposit : DCert → PParams → Deposits
certDeposit (delegate c _ _ v) _ = ❴ CredentialDeposit c , v ❵
certDeposit (regdrep c v _) _ = ❴ DRepDeposit c , v ❵
certDeposit (reg c v) pp = ❴ CredentialDeposit c , pp .PParams.keyDeposit ❵
certDeposit _ _ = ∅
certRefund : DCert → ℙ DepositPurpose
certRefund (dereg c _) = ❴ CredentialDeposit c ❵
certRefund (deregdrep c _) = ❴ DRepDeposit c ❵
certRefund _ = ∅
updateCertDeposit : PParams → DCert → Deposits → Deposits
updateCertDeposit pp (delegate c _ _ v) deposits = deposits ∪⁺ ❴ CredentialDeposit c , v ❵
updateCertDeposit pp (reg c _) deposits = deposits ∪⁺ ❴ CredentialDeposit c , pp .PParams.keyDeposit ❵
updateCertDeposit pp (regdrep c v _) deposits = deposits ∪⁺ ❴ DRepDeposit c , v ❵
updateCertDeposit pp (dereg c _) deposits = deposits ∣ ❴ CredentialDeposit c ❵ ᶜ
updateCertDeposit pp (deregdrep c _) deposits = deposits ∣ ❴ DRepDeposit c ❵ ᶜ
updateCertDeposit pp (regpool kh _) deposits = deposits ∪⁺ ❴ PoolDeposit kh , pp .PParams.poolDeposit ❵
updateCertDeposit _ (retirepool _ _) deposits = deposits
updateCertDeposit _ (ccreghot _ _) deposits = deposits
private variable
rwds rewards : Credential ⇀ Coin
dReps : Credential ⇀ Epoch
sDelegs stakeDelegs : Credential ⇀ KeyHash
ccKeys ccHotKeys : Credential ⇀ Maybe Credential
vDelegs voteDelegs : Credential ⇀ VDeleg
pools : KeyHash ⇀ PoolParams
retiring : KeyHash ⇀ Epoch
wdrls : RwdAddr ⇀ Coin
an : Anchor
Γ : CertEnv
d : Coin
md : Maybe Coin
c : Credential
mc : Maybe Credential
delegatees cc : ℙ Credential
dCert : DCert
dep ddep gdep : Deposits
e : Epoch
vs : List GovVote
kh : KeyHash
mkh : Maybe KeyHash
poolParams : PoolParams
pp : PParams
mv : Maybe VDeleg
stᵈ stᵈ' : DState
stᵍ stᵍ' : GState
stᵖ stᵖ' : PState
data _⊢_⇀⦇_,POOL⦈_ : PoolEnv → PState → DCert → PState → Type
data _⊢_⇀⦇_,DELEG⦈_ : DelegEnv → DState → DCert → DState → Type
data _⊢_⇀⦇_,POOL⦈_ where
POOL-regpool :
∙ kh ∉ dom pools
────────────────────────────────
pp ⊢ $\begin{pmatrix} \,\href{Ledger.Conway.Conformance.Certs.html#2991}{\htmlId{3893}{\htmlClass{Generalizable}{\text{pools}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3039}{\htmlId{3901}{\htmlClass{Generalizable}{\text{retiring}}}}\, \end{pmatrix}$ ⇀⦇ regpool kh poolParams ,POOL⦈
$\begin{pmatrix} \,\href{Class.HasSingleton.html#288}{\htmlId{3958}{\htmlClass{Field Operator}{\text{❴}}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#3440}{\htmlId{3960}{\htmlClass{Generalizable}{\text{kh}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3500}{\htmlId{3965}{\htmlClass{Generalizable}{\text{poolParams}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{3976}{\htmlClass{Field Operator}{\text{❵}}}}\, \,\href{Axiom.Set.Map.html#6320}{\htmlId{3978}{\htmlClass{Function Operator}{\text{∪ˡ}}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#2991}{\htmlId{3981}{\htmlClass{Generalizable}{\text{pools}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3039}{\htmlId{3989}{\htmlClass{Generalizable}{\text{retiring}}}}\, \end{pmatrix}$
POOL-retirepool :
────────────────────────────────
pp ⊢ $\begin{pmatrix} \,\href{Ledger.Conway.Conformance.Certs.html#2991}{\htmlId{4069}{\htmlClass{Generalizable}{\text{pools}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3039}{\htmlId{4077}{\htmlClass{Generalizable}{\text{retiring}}}}\, \end{pmatrix}$ ⇀⦇ retirepool kh e ,POOL⦈ $\begin{pmatrix} \,\href{Ledger.Conway.Conformance.Certs.html#2991}{\htmlId{4116}{\htmlClass{Generalizable}{\text{pools}}}}\, \\ \,\href{Class.HasSingleton.html#288}{\htmlId{4124}{\htmlClass{Field Operator}{\text{❴}}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#3440}{\htmlId{4126}{\htmlClass{Generalizable}{\text{kh}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3383}{\htmlId{4131}{\htmlClass{Generalizable}{\text{e}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{4133}{\htmlClass{Field Operator}{\text{❵}}}}\, \,\href{Axiom.Set.Map.html#6320}{\htmlId{4135}{\htmlClass{Function Operator}{\text{∪ˡ}}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#3039}{\htmlId{4138}{\htmlClass{Generalizable}{\text{retiring}}}}\, \end{pmatrix}$
data _⊢_⇀⦇_,DELEG⦈_ where
DELEG-delegate : let open PParams pp in
∙ (c ∉ dom rwds → d ≡ keyDeposit)
∙ (c ∈ dom rwds → d ≡ 0)
∙ mv ∈ mapˢ (just ∘ credVoter DRep) delegatees ∪
fromList
( nothing
∷ just abstainRep
∷ just noConfidenceRep
∷ []
)
∙ mkh ∈ mapˢ just (dom pools) ∪ ❴ nothing ❵
────────────────────────────────
$\begin{pmatrix} \,\href{Ledger.Conway.Conformance.Certs.html#3530}{\htmlId{4558}{\htmlClass{Generalizable}{\text{pp}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#2991}{\htmlId{4563}{\htmlClass{Generalizable}{\text{pools}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3298}{\htmlId{4571}{\htmlClass{Generalizable}{\text{delegatees}}}}\, \end{pmatrix}$ ⊢
$\begin{pmatrix} \,\href{Ledger.Conway.Conformance.Certs.html#2944}{\htmlId{4594}{\htmlClass{Generalizable}{\text{vDelegs}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#2839}{\htmlId{4604}{\htmlClass{Generalizable}{\text{sDelegs}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#2748}{\htmlId{4614}{\htmlClass{Generalizable}{\text{rwds}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3355}{\htmlId{4621}{\htmlClass{Generalizable}{\text{dep}}}}\, \end{pmatrix}$
⇀⦇ delegate c mv mkh d ,DELEG⦈
$\begin{pmatrix} \,\href{Axiom.Set.Map.html#7168}{\htmlId{4672}{\htmlClass{Function}{\text{insertIfJust}}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#3232}{\htmlId{4685}{\htmlClass{Generalizable}{\text{c}}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#3557}{\htmlId{4687}{\htmlClass{Generalizable}{\text{mv}}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#2944}{\htmlId{4690}{\htmlClass{Generalizable}{\text{vDelegs}}}}\, \\ \,\href{Axiom.Set.Map.html#7168}{\htmlId{4700}{\htmlClass{Function}{\text{insertIfJust}}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#3232}{\htmlId{4713}{\htmlClass{Generalizable}{\text{c}}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#3467}{\htmlId{4715}{\htmlClass{Generalizable}{\text{mkh}}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#2839}{\htmlId{4719}{\htmlClass{Generalizable}{\text{sDelegs}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#2748}{\htmlId{4729}{\htmlClass{Generalizable}{\text{rwds}}}}\, \,\href{Axiom.Set.Map.html#6320}{\htmlId{4734}{\htmlClass{Function Operator}{\text{∪ˡ}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{4737}{\htmlClass{Field Operator}{\text{❴}}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#3232}{\htmlId{4739}{\htmlClass{Generalizable}{\text{c}}}}\, \\ \,\htmlId{4743}{\htmlClass{Number}{\text{0}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{4745}{\htmlClass{Field Operator}{\text{❵}}}}\,
\\ \,\href{Ledger.Conway.Conformance.Certs.html#1884}{\htmlId{4755}{\htmlClass{Function}{\text{updateCertDeposit}}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#3530}{\htmlId{4773}{\htmlClass{Generalizable}{\text{pp}}}}\, (\,\href{Ledger.Conway.Specification.Certs.html#1877}{\htmlId{4777}{\htmlClass{InductiveConstructor}{\text{delegate}}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#3232}{\htmlId{4786}{\htmlClass{Generalizable}{\text{c}}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#3557}{\htmlId{4788}{\htmlClass{Generalizable}{\text{mv}}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#3467}{\htmlId{4791}{\htmlClass{Generalizable}{\text{mkh}}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#3178}{\htmlId{4795}{\htmlClass{Generalizable}{\text{d}}}}\,) \,\href{Ledger.Conway.Conformance.Certs.html#3355}{\htmlId{4798}{\htmlClass{Generalizable}{\text{dep}}}}\, \end{pmatrix}$
DELEG-dereg :
∙ (c , 0) ∈ rwds
∙ (CredentialDeposit c , d) ∈ dep
∙ md ≡ nothing ⊎ md ≡ just d
────────────────────────────────
$\begin{pmatrix} \,\href{Ledger.Conway.Conformance.Certs.html#3530}{\htmlId{4960}{\htmlClass{Generalizable}{\text{pp}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#2991}{\htmlId{4965}{\htmlClass{Generalizable}{\text{pools}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3298}{\htmlId{4973}{\htmlClass{Generalizable}{\text{delegatees}}}}\, \end{pmatrix}$ ⊢
$\begin{pmatrix} \,\href{Ledger.Conway.Conformance.Certs.html#2944}{\htmlId{4996}{\htmlClass{Generalizable}{\text{vDelegs}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#2839}{\htmlId{5006}{\htmlClass{Generalizable}{\text{sDelegs}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#2748}{\htmlId{5016}{\htmlClass{Generalizable}{\text{rwds}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3355}{\htmlId{5023}{\htmlClass{Generalizable}{\text{dep}}}}\, \end{pmatrix}$
⇀⦇ dereg c md ,DELEG⦈
$\begin{pmatrix} \,\href{Ledger.Conway.Conformance.Certs.html#2944}{\htmlId{5065}{\htmlClass{Generalizable}{\text{vDelegs}}}}\, \,\href{Axiom.Set.Map.html#10748}{\htmlId{5073}{\htmlClass{Function Operator}{\text{∣}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{5075}{\htmlClass{Field Operator}{\text{❴}}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#3232}{\htmlId{5077}{\htmlClass{Generalizable}{\text{c}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{5079}{\htmlClass{Field Operator}{\text{❵}}}}\, \,\href{Axiom.Set.Map.html#10748}{\htmlId{5081}{\htmlClass{Function Operator}{\text{ᶜ}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#2839}{\htmlId{5085}{\htmlClass{Generalizable}{\text{sDelegs}}}}\, \,\href{Axiom.Set.Map.html#10748}{\htmlId{5093}{\htmlClass{Function Operator}{\text{∣}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{5095}{\htmlClass{Field Operator}{\text{❴}}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#3232}{\htmlId{5097}{\htmlClass{Generalizable}{\text{c}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{5099}{\htmlClass{Field Operator}{\text{❵}}}}\, \,\href{Axiom.Set.Map.html#10748}{\htmlId{5101}{\htmlClass{Function Operator}{\text{ᶜ}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#2748}{\htmlId{5105}{\htmlClass{Generalizable}{\text{rwds}}}}\, \,\href{Axiom.Set.Map.html#10748}{\htmlId{5110}{\htmlClass{Function Operator}{\text{∣}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{5112}{\htmlClass{Field Operator}{\text{❴}}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#3232}{\htmlId{5114}{\htmlClass{Generalizable}{\text{c}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{5116}{\htmlClass{Field Operator}{\text{❵}}}}\, \,\href{Axiom.Set.Map.html#10748}{\htmlId{5118}{\htmlClass{Function Operator}{\text{ᶜ}}}}\,
\\ \,\href{Ledger.Conway.Conformance.Certs.html#1884}{\htmlId{5128}{\htmlClass{Function}{\text{updateCertDeposit}}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#3530}{\htmlId{5146}{\htmlClass{Generalizable}{\text{pp}}}}\, (\,\href{Ledger.Conway.Specification.Certs.html#1950}{\htmlId{5150}{\htmlClass{InductiveConstructor}{\text{dereg}}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#3232}{\htmlId{5156}{\htmlClass{Generalizable}{\text{c}}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#3202}{\htmlId{5158}{\htmlClass{Generalizable}{\text{md}}}}\,) \,\href{Ledger.Conway.Conformance.Certs.html#3355}{\htmlId{5162}{\htmlClass{Generalizable}{\text{dep}}}}\, \end{pmatrix}$
DELEG-reg : let open PParams pp in
∙ c ∉ dom rwds
∙ d ≡ keyDeposit ⊎ d ≡ 0
────────────────────────────────
$\begin{pmatrix} \,\href{Ledger.Conway.Conformance.Certs.html#3530}{\htmlId{5301}{\htmlClass{Generalizable}{\text{pp}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#2991}{\htmlId{5306}{\htmlClass{Generalizable}{\text{pools}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3298}{\htmlId{5314}{\htmlClass{Generalizable}{\text{delegatees}}}}\, \end{pmatrix}$ ⊢
$\begin{pmatrix} \,\href{Ledger.Conway.Conformance.Certs.html#2944}{\htmlId{5339}{\htmlClass{Generalizable}{\text{vDelegs}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#2839}{\htmlId{5349}{\htmlClass{Generalizable}{\text{sDelegs}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#2748}{\htmlId{5359}{\htmlClass{Generalizable}{\text{rwds}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3355}{\htmlId{5366}{\htmlClass{Generalizable}{\text{dep}}}}\, \end{pmatrix}$ ⇀⦇ reg c d ,DELEG⦈
$\begin{pmatrix} \,\href{Ledger.Conway.Conformance.Certs.html#2944}{\htmlId{5401}{\htmlClass{Generalizable}{\text{vDelegs}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#2839}{\htmlId{5411}{\htmlClass{Generalizable}{\text{sDelegs}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#2748}{\htmlId{5421}{\htmlClass{Generalizable}{\text{rwds}}}}\, \,\href{Axiom.Set.Map.html#6320}{\htmlId{5426}{\htmlClass{Function Operator}{\text{∪ˡ}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{5429}{\htmlClass{Field Operator}{\text{❴}}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#3232}{\htmlId{5431}{\htmlClass{Generalizable}{\text{c}}}}\, \\ \,\htmlId{5435}{\htmlClass{Number}{\text{0}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{5437}{\htmlClass{Field Operator}{\text{❵}}}}\,
\\ \,\href{Ledger.Conway.Conformance.Certs.html#1884}{\htmlId{5449}{\htmlClass{Function}{\text{updateCertDeposit}}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#3530}{\htmlId{5467}{\htmlClass{Generalizable}{\text{pp}}}}\, (\,\href{Ledger.Conway.Specification.Certs.html#2581}{\htmlId{5471}{\htmlClass{InductiveConstructor}{\text{reg}}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#3232}{\htmlId{5475}{\htmlClass{Generalizable}{\text{c}}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#3178}{\htmlId{5477}{\htmlClass{Generalizable}{\text{d}}}}\,) \,\href{Ledger.Conway.Conformance.Certs.html#3355}{\htmlId{5480}{\htmlClass{Generalizable}{\text{dep}}}}\, \end{pmatrix}$
data _⊢_⇀⦇_,GOVCERT⦈_ : GovCertEnv → GState → DCert → GState → Type where
GOVCERT-regdrep : ∀ {pp} → let open PParams pp in
∙ (d ≡ drepDeposit × c ∉ dom dReps) ⊎ (d ≡ 0 × c ∈ dom dReps)
────────────────────────────────
$\begin{pmatrix} \,\href{Ledger.Conway.Conformance.Certs.html#3383}{\htmlId{5726}{\htmlClass{Generalizable}{\text{e}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#5584}{\htmlId{5730}{\htmlClass{Bound}{\text{pp}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3408}{\htmlId{5735}{\htmlClass{Generalizable}{\text{vs}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3082}{\htmlId{5740}{\htmlClass{Generalizable}{\text{wdrls}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3309}{\htmlId{5748}{\htmlClass{Generalizable}{\text{cc}}}}\, \end{pmatrix}$ ⊢
$\begin{pmatrix} \,\href{Ledger.Conway.Conformance.Certs.html#2793}{\htmlId{5763}{\htmlClass{Generalizable}{\text{dReps}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#2887}{\htmlId{5771}{\htmlClass{Generalizable}{\text{ccKeys}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3355}{\htmlId{5780}{\htmlClass{Generalizable}{\text{dep}}}}\, \end{pmatrix}$
⇀⦇ regdrep c d an ,GOVCERT⦈
$\begin{pmatrix} \,\href{Class.HasSingleton.html#288}{\htmlId{5830}{\htmlClass{Field Operator}{\text{❴}}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#3232}{\htmlId{5832}{\htmlClass{Generalizable}{\text{c}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3383}{\htmlId{5836}{\htmlClass{Generalizable}{\text{e}}}}\, \,\href{Class.HasAdd.Core.html#162}{\htmlId{5838}{\htmlClass{Field Operator}{\text{+}}}}\, \,\href{Ledger.Conway.Specification.PParams.html#4827}{\htmlId{5840}{\htmlClass{Field}{\text{drepActivity}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{5853}{\htmlClass{Field Operator}{\text{❵}}}}\, \,\href{Axiom.Set.Map.html#6320}{\htmlId{5855}{\htmlClass{Function Operator}{\text{∪ˡ}}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#2793}{\htmlId{5858}{\htmlClass{Generalizable}{\text{dReps}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#2887}{\htmlId{5866}{\htmlClass{Generalizable}{\text{ccKeys}}}}\,
\\ \,\href{Ledger.Conway.Conformance.Certs.html#1884}{\htmlId{5881}{\htmlClass{Function}{\text{updateCertDeposit}}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#5584}{\htmlId{5899}{\htmlClass{Bound}{\text{pp}}}}\, (\,\href{Ledger.Conway.Specification.Certs.html#2083}{\htmlId{5903}{\htmlClass{InductiveConstructor}{\text{regdrep}}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#3232}{\htmlId{5911}{\htmlClass{Generalizable}{\text{c}}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#3178}{\htmlId{5913}{\htmlClass{Generalizable}{\text{d}}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#3125}{\htmlId{5915}{\htmlClass{Generalizable}{\text{an}}}}\, ) \,\href{Ledger.Conway.Conformance.Certs.html#3355}{\htmlId{5920}{\htmlClass{Generalizable}{\text{dep}}}}\, \end{pmatrix}$
GOVCERT-deregdrep :
∙ c ∈ dom dReps
∙ (DRepDeposit c , d) ∈ dep
────────────────────────────────
$\begin{pmatrix} \,\href{Ledger.Conway.Conformance.Certs.html#3383}{\htmlId{6048}{\htmlClass{Generalizable}{\text{e}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3530}{\htmlId{6052}{\htmlClass{Generalizable}{\text{pp}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3408}{\htmlId{6057}{\htmlClass{Generalizable}{\text{vs}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3082}{\htmlId{6062}{\htmlClass{Generalizable}{\text{wdrls}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3309}{\htmlId{6070}{\htmlClass{Generalizable}{\text{cc}}}}\, \end{pmatrix}$ ⊢ $\begin{pmatrix} \,\href{Ledger.Conway.Conformance.Certs.html#2793}{\htmlId{6079}{\htmlClass{Generalizable}{\text{dReps}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#2887}{\htmlId{6087}{\htmlClass{Generalizable}{\text{ccKeys}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3355}{\htmlId{6096}{\htmlClass{Generalizable}{\text{dep}}}}\, \end{pmatrix}$
⇀⦇ deregdrep c d ,GOVCERT⦈
$\begin{pmatrix} \,\href{Ledger.Conway.Conformance.Certs.html#2793}{\htmlId{6151}{\htmlClass{Generalizable}{\text{dReps}}}}\, \,\href{Axiom.Set.Map.html#10748}{\htmlId{6157}{\htmlClass{Function Operator}{\text{∣}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{6159}{\htmlClass{Field Operator}{\text{❴}}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#3232}{\htmlId{6161}{\htmlClass{Generalizable}{\text{c}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{6163}{\htmlClass{Field Operator}{\text{❵}}}}\, \,\href{Axiom.Set.Map.html#10748}{\htmlId{6165}{\htmlClass{Function Operator}{\text{ᶜ}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#2887}{\htmlId{6169}{\htmlClass{Generalizable}{\text{ccKeys}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#1884}{\htmlId{6178}{\htmlClass{Function}{\text{updateCertDeposit}}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#3530}{\htmlId{6196}{\htmlClass{Generalizable}{\text{pp}}}}\, (\,\href{Ledger.Conway.Specification.Certs.html#2134}{\htmlId{6200}{\htmlClass{InductiveConstructor}{\text{deregdrep}}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#3232}{\htmlId{6210}{\htmlClass{Generalizable}{\text{c}}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#3178}{\htmlId{6212}{\htmlClass{Generalizable}{\text{d}}}}\,) \,\href{Ledger.Conway.Conformance.Certs.html#3355}{\htmlId{6215}{\htmlClass{Generalizable}{\text{dep}}}}\, \end{pmatrix}$
GOVCERT-ccreghot :
∙ (c , nothing) ∉ ccKeys
∙ c ∈ cc
────────────────────────────────
$\begin{pmatrix} \,\href{Ledger.Conway.Conformance.Certs.html#3383}{\htmlId{6332}{\htmlClass{Generalizable}{\text{e}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3530}{\htmlId{6336}{\htmlClass{Generalizable}{\text{pp}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3408}{\htmlId{6341}{\htmlClass{Generalizable}{\text{vs}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3082}{\htmlId{6346}{\htmlClass{Generalizable}{\text{wdrls}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3309}{\htmlId{6354}{\htmlClass{Generalizable}{\text{cc}}}}\, \end{pmatrix}$ ⊢ $\begin{pmatrix} \,\href{Ledger.Conway.Conformance.Certs.html#2793}{\htmlId{6363}{\htmlClass{Generalizable}{\text{dReps}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#2887}{\htmlId{6371}{\htmlClass{Generalizable}{\text{ccKeys}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3355}{\htmlId{6380}{\htmlClass{Generalizable}{\text{dep}}}}\, \end{pmatrix}$
⇀⦇ ccreghot c mc ,GOVCERT⦈
$\begin{pmatrix} \,\href{Ledger.Conway.Conformance.Certs.html#2793}{\htmlId{6435}{\htmlClass{Generalizable}{\text{dReps}}}}\, \\ \,\href{Class.HasSingleton.html#288}{\htmlId{6443}{\htmlClass{Field Operator}{\text{❴}}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#3232}{\htmlId{6445}{\htmlClass{Generalizable}{\text{c}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3262}{\htmlId{6449}{\htmlClass{Generalizable}{\text{mc}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{6452}{\htmlClass{Field Operator}{\text{❵}}}}\, \,\href{Axiom.Set.Map.html#6320}{\htmlId{6454}{\htmlClass{Function Operator}{\text{∪ˡ}}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#2887}{\htmlId{6457}{\htmlClass{Generalizable}{\text{ccKeys}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#1884}{\htmlId{6466}{\htmlClass{Function}{\text{updateCertDeposit}}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#3530}{\htmlId{6484}{\htmlClass{Generalizable}{\text{pp}}}}\, (\,\href{Ledger.Conway.Specification.Certs.html#2176}{\htmlId{6488}{\htmlClass{InductiveConstructor}{\text{ccreghot}}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#3232}{\htmlId{6497}{\htmlClass{Generalizable}{\text{c}}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#3262}{\htmlId{6499}{\htmlClass{Generalizable}{\text{mc}}}}\,) \,\href{Ledger.Conway.Conformance.Certs.html#3355}{\htmlId{6503}{\htmlClass{Generalizable}{\text{dep}}}}\, \end{pmatrix}$
data _⊢_⇀⦇_,CERT⦈_ : CertEnv → CertState → DCert → CertState → Type where
CERT-deleg :
∙ $\begin{pmatrix} \,\href{Ledger.Conway.Conformance.Certs.html#3530}{\htmlId{6607}{\htmlClass{Generalizable}{\text{pp}}}}\, \\ \,\href{Ledger.Conway.Specification.Certs.html#4566}{\htmlId{6612}{\htmlClass{Field}{\text{PState.pools}}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#3630}{\htmlId{6625}{\htmlClass{Generalizable}{\text{stᵖ}}}}\, \\ \,\href{Class.IsSet.html#916}{\htmlId{6631}{\htmlClass{Function}{\text{dom}}}}\, (\,\href{Ledger.Conway.Conformance.Certs.html#865}{\htmlId{6636}{\htmlClass{Field}{\text{GState.dreps}}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#3610}{\htmlId{6649}{\htmlClass{Generalizable}{\text{stᵍ}}}}\,) \end{pmatrix}$ ⊢ stᵈ ⇀⦇ dCert ,DELEG⦈ stᵈ'
────────────────────────────────
$\begin{pmatrix} \,\href{Ledger.Conway.Conformance.Certs.html#3383}{\htmlId{6731}{\htmlClass{Generalizable}{\text{e}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3530}{\htmlId{6735}{\htmlClass{Generalizable}{\text{pp}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3408}{\htmlId{6740}{\htmlClass{Generalizable}{\text{vs}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3082}{\htmlId{6745}{\htmlClass{Generalizable}{\text{wdrls}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3309}{\htmlId{6753}{\htmlClass{Generalizable}{\text{cc}}}}\, \end{pmatrix}$ ⊢ $\begin{pmatrix} \,\href{Ledger.Conway.Conformance.Certs.html#3590}{\htmlId{6762}{\htmlClass{Generalizable}{\text{stᵈ}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3630}{\htmlId{6768}{\htmlClass{Generalizable}{\text{stᵖ}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3610}{\htmlId{6774}{\htmlClass{Generalizable}{\text{stᵍ}}}}\, \end{pmatrix}$ ⇀⦇ dCert ,CERT⦈ $\begin{pmatrix} \,\href{Ledger.Conway.Conformance.Certs.html#3594}{\htmlId{6798}{\htmlClass{Generalizable}{\text{stᵈ'}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3630}{\htmlId{6805}{\htmlClass{Generalizable}{\text{stᵖ}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3610}{\htmlId{6811}{\htmlClass{Generalizable}{\text{stᵍ}}}}\, \end{pmatrix}$
CERT-pool :
∙ pp ⊢ stᵖ ⇀⦇ dCert ,POOL⦈ stᵖ'
────────────────────────────────
$\begin{pmatrix} \,\href{Ledger.Conway.Conformance.Certs.html#3383}{\htmlId{6915}{\htmlClass{Generalizable}{\text{e}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3530}{\htmlId{6919}{\htmlClass{Generalizable}{\text{pp}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3408}{\htmlId{6924}{\htmlClass{Generalizable}{\text{vs}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3082}{\htmlId{6929}{\htmlClass{Generalizable}{\text{wdrls}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3309}{\htmlId{6937}{\htmlClass{Generalizable}{\text{cc}}}}\, \end{pmatrix}$ ⊢ $\begin{pmatrix} \,\href{Ledger.Conway.Conformance.Certs.html#3590}{\htmlId{6946}{\htmlClass{Generalizable}{\text{stᵈ}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3630}{\htmlId{6952}{\htmlClass{Generalizable}{\text{stᵖ}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3610}{\htmlId{6958}{\htmlClass{Generalizable}{\text{stᵍ}}}}\, \end{pmatrix}$ ⇀⦇ dCert ,CERT⦈ $\begin{pmatrix} \,\href{Ledger.Conway.Conformance.Certs.html#3590}{\htmlId{6982}{\htmlClass{Generalizable}{\text{stᵈ}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3634}{\htmlId{6988}{\htmlClass{Generalizable}{\text{stᵖ'}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3610}{\htmlId{6995}{\htmlClass{Generalizable}{\text{stᵍ}}}}\, \end{pmatrix}$
CERT-vdel :
∙ Γ ⊢ stᵍ ⇀⦇ dCert ,GOVCERT⦈ stᵍ'
────────────────────────────────
Γ ⊢ $\begin{pmatrix} \,\href{Ledger.Conway.Conformance.Certs.html#3590}{\htmlId{7105}{\htmlClass{Generalizable}{\text{stᵈ}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3630}{\htmlId{7111}{\htmlClass{Generalizable}{\text{stᵖ}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3610}{\htmlId{7117}{\htmlClass{Generalizable}{\text{stᵍ}}}}\, \end{pmatrix}$ ⇀⦇ dCert ,CERT⦈ $\begin{pmatrix} \,\href{Ledger.Conway.Conformance.Certs.html#3590}{\htmlId{7141}{\htmlClass{Generalizable}{\text{stᵈ}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3630}{\htmlId{7147}{\htmlClass{Generalizable}{\text{stᵖ}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3614}{\htmlId{7153}{\htmlClass{Generalizable}{\text{stᵍ'}}}}\, \end{pmatrix}$
data _⊢_⇀⦇_,CERTBASE⦈_ : CertEnv → CertState → ⊤ → CertState → Type where
CERT-base :
let open PParams pp
refresh = mapPartial getDRepVote (fromList vs)
refreshedDReps = mapValueRestricted (const (e + drepActivity)) dReps refresh
wdrlCreds = mapˢ stake (dom wdrls)
validVoteDelegs = voteDelegs ∣^ (mapˢ (credVoter DRep) (dom dReps) ∪ fromList (noConfidenceRep ∷ abstainRep ∷ []))
in
∙ filterˢ isKeyHash wdrlCreds ⊆ dom voteDelegs
∙ mapˢ (map₁ stake) (wdrls ˢ) ⊆ rewards ˢ
────────────────────────────────
$\begin{pmatrix} \,\href{Ledger.Conway.Conformance.Certs.html#3383}{\htmlId{7746}{\htmlClass{Generalizable}{\text{e}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3530}{\htmlId{7750}{\htmlClass{Generalizable}{\text{pp}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3408}{\htmlId{7755}{\htmlClass{Generalizable}{\text{vs}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3082}{\htmlId{7760}{\htmlClass{Generalizable}{\text{wdrls}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3309}{\htmlId{7768}{\htmlClass{Generalizable}{\text{cc}}}}\, \end{pmatrix}$ ⊢
$\begin{pmatrix} \begin{pmatrix} \,\href{Ledger.Conway.Conformance.Certs.html#2952}{\htmlId{7785}{\htmlClass{Generalizable}{\text{voteDelegs}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#2847}{\htmlId{7798}{\htmlClass{Generalizable}{\text{stakeDelegs}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#2753}{\htmlId{7812}{\htmlClass{Generalizable}{\text{rewards}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3359}{\htmlId{7822}{\htmlClass{Generalizable}{\text{ddep}}}}\, \end{pmatrix}
\\ \,\href{Ledger.Conway.Conformance.Certs.html#3630}{\htmlId{7837}{\htmlClass{Generalizable}{\text{stᵖ}}}}\,
\\ \begin{pmatrix} \,\href{Ledger.Conway.Conformance.Certs.html#2793}{\htmlId{7851}{\htmlClass{Generalizable}{\text{dReps}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#2894}{\htmlId{7859}{\htmlClass{Generalizable}{\text{ccHotKeys}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3364}{\htmlId{7871}{\htmlClass{Generalizable}{\text{gdep}}}}\, \end{pmatrix}
\end{pmatrix}$
⇀⦇ _ ,CERTBASE⦈
$\begin{pmatrix} \begin{pmatrix} \,\href{Ledger.Conway.Conformance.Certs.html#7479}{\htmlId{7918}{\htmlClass{Bound}{\text{validVoteDelegs}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#2847}{\htmlId{7936}{\htmlClass{Generalizable}{\text{stakeDelegs}}}}\, \\ \,\href{Axiom.Set.Map.html#9130}{\htmlId{7950}{\htmlClass{Function}{\text{constMap}}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#7430}{\htmlId{7959}{\htmlClass{Bound}{\text{wdrlCreds}}}}\, \,\htmlId{7969}{\htmlClass{Number}{\text{0}}}\, \,\href{Axiom.Set.Map.html#6320}{\htmlId{7971}{\htmlClass{Function Operator}{\text{∪ˡ}}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#2753}{\htmlId{7974}{\htmlClass{Generalizable}{\text{rewards}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3359}{\htmlId{7984}{\htmlClass{Generalizable}{\text{ddep}}}}\, \end{pmatrix}
\\ \,\href{Ledger.Conway.Conformance.Certs.html#3630}{\htmlId{7999}{\htmlClass{Generalizable}{\text{stᵖ}}}}\,
\\ \begin{pmatrix} \,\href{Ledger.Conway.Conformance.Certs.html#7344}{\htmlId{8013}{\htmlClass{Bound}{\text{refreshedDReps}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#2894}{\htmlId{8030}{\htmlClass{Generalizable}{\text{ccHotKeys}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3364}{\htmlId{8042}{\htmlClass{Generalizable}{\text{gdep}}}}\, \end{pmatrix}
\end{pmatrix}$
_⊢_⇀⦇_,CERTS⦈_ : CertEnv → CertState → List DCert → CertState → Type
_⊢_⇀⦇_,CERTS⦈_ = ReflexiveTransitiveClosureᵇ' {_⊢_⇀⟦_⟧ᵇ_ = _⊢_⇀⦇_,CERTBASE⦈_}{_⊢_⇀⦇_,CERT⦈_}