{-# OPTIONS --safe #-}
open import Ledger.Prelude
open import Ledger.Conway.Types.GovStructure
import Ledger.Conway.Certs
module Ledger.Conway.Conformance.Certs
(gs : _) (open GovStructure gs)
where
open import Tactic.Derive.DecEq
open import Ledger.Conway.GovernanceActions gs
private module Certs = Ledger.Conway.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#2975}{\htmlId{3877}{\htmlClass{Generalizable}{\text{pools}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3023}{\htmlId{3885}{\htmlClass{Generalizable}{\text{retiring}}}}\, \end{pmatrix}$ ⇀⦇ regpool kh poolParams ,POOL⦈
$\begin{pmatrix} \,\href{Class.HasSingleton.html#288}{\htmlId{3942}{\htmlClass{Field Operator}{\text{❴}}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#3424}{\htmlId{3944}{\htmlClass{Generalizable}{\text{kh}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3484}{\htmlId{3949}{\htmlClass{Generalizable}{\text{poolParams}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{3960}{\htmlClass{Field Operator}{\text{❵}}}}\, \,\href{Axiom.Set.Map.html#6320}{\htmlId{3962}{\htmlClass{Function Operator}{\text{∪ˡ}}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#2975}{\htmlId{3965}{\htmlClass{Generalizable}{\text{pools}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3023}{\htmlId{3973}{\htmlClass{Generalizable}{\text{retiring}}}}\, \end{pmatrix}$
POOL-retirepool :
────────────────────────────────
pp ⊢ $\begin{pmatrix} \,\href{Ledger.Conway.Conformance.Certs.html#2975}{\htmlId{4053}{\htmlClass{Generalizable}{\text{pools}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3023}{\htmlId{4061}{\htmlClass{Generalizable}{\text{retiring}}}}\, \end{pmatrix}$ ⇀⦇ retirepool kh e ,POOL⦈ $\begin{pmatrix} \,\href{Ledger.Conway.Conformance.Certs.html#2975}{\htmlId{4100}{\htmlClass{Generalizable}{\text{pools}}}}\, \\ \,\href{Class.HasSingleton.html#288}{\htmlId{4108}{\htmlClass{Field Operator}{\text{❴}}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#3424}{\htmlId{4110}{\htmlClass{Generalizable}{\text{kh}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3367}{\htmlId{4115}{\htmlClass{Generalizable}{\text{e}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{4117}{\htmlClass{Field Operator}{\text{❵}}}}\, \,\href{Axiom.Set.Map.html#6320}{\htmlId{4119}{\htmlClass{Function Operator}{\text{∪ˡ}}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#3023}{\htmlId{4122}{\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#3514}{\htmlId{4542}{\htmlClass{Generalizable}{\text{pp}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#2975}{\htmlId{4547}{\htmlClass{Generalizable}{\text{pools}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3282}{\htmlId{4555}{\htmlClass{Generalizable}{\text{delegatees}}}}\, \end{pmatrix}$ ⊢
$\begin{pmatrix} \,\href{Ledger.Conway.Conformance.Certs.html#2928}{\htmlId{4578}{\htmlClass{Generalizable}{\text{vDelegs}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#2823}{\htmlId{4588}{\htmlClass{Generalizable}{\text{sDelegs}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#2732}{\htmlId{4598}{\htmlClass{Generalizable}{\text{rwds}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3339}{\htmlId{4605}{\htmlClass{Generalizable}{\text{dep}}}}\, \end{pmatrix}$
⇀⦇ delegate c mv mkh d ,DELEG⦈
$\begin{pmatrix} \,\href{Axiom.Set.Map.html#7168}{\htmlId{4656}{\htmlClass{Function}{\text{insertIfJust}}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#3216}{\htmlId{4669}{\htmlClass{Generalizable}{\text{c}}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#3541}{\htmlId{4671}{\htmlClass{Generalizable}{\text{mv}}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#2928}{\htmlId{4674}{\htmlClass{Generalizable}{\text{vDelegs}}}}\, \\ \,\href{Axiom.Set.Map.html#7168}{\htmlId{4684}{\htmlClass{Function}{\text{insertIfJust}}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#3216}{\htmlId{4697}{\htmlClass{Generalizable}{\text{c}}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#3451}{\htmlId{4699}{\htmlClass{Generalizable}{\text{mkh}}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#2823}{\htmlId{4703}{\htmlClass{Generalizable}{\text{sDelegs}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#2732}{\htmlId{4713}{\htmlClass{Generalizable}{\text{rwds}}}}\, \,\href{Axiom.Set.Map.html#6320}{\htmlId{4718}{\htmlClass{Function Operator}{\text{∪ˡ}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{4721}{\htmlClass{Field Operator}{\text{❴}}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#3216}{\htmlId{4723}{\htmlClass{Generalizable}{\text{c}}}}\, \\ \,\htmlId{4727}{\htmlClass{Number}{\text{0}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{4729}{\htmlClass{Field Operator}{\text{❵}}}}\,
\\ \,\href{Ledger.Conway.Conformance.Certs.html#1868}{\htmlId{4739}{\htmlClass{Function}{\text{updateCertDeposit}}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#3514}{\htmlId{4757}{\htmlClass{Generalizable}{\text{pp}}}}\, (\,\href{Ledger.Conway.Certs.html#1373}{\htmlId{4761}{\htmlClass{InductiveConstructor}{\text{delegate}}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#3216}{\htmlId{4770}{\htmlClass{Generalizable}{\text{c}}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#3541}{\htmlId{4772}{\htmlClass{Generalizable}{\text{mv}}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#3451}{\htmlId{4775}{\htmlClass{Generalizable}{\text{mkh}}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#3162}{\htmlId{4779}{\htmlClass{Generalizable}{\text{d}}}}\,) \,\href{Ledger.Conway.Conformance.Certs.html#3339}{\htmlId{4782}{\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#3514}{\htmlId{4944}{\htmlClass{Generalizable}{\text{pp}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#2975}{\htmlId{4949}{\htmlClass{Generalizable}{\text{pools}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3282}{\htmlId{4957}{\htmlClass{Generalizable}{\text{delegatees}}}}\, \end{pmatrix}$ ⊢
$\begin{pmatrix} \,\href{Ledger.Conway.Conformance.Certs.html#2928}{\htmlId{4980}{\htmlClass{Generalizable}{\text{vDelegs}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#2823}{\htmlId{4990}{\htmlClass{Generalizable}{\text{sDelegs}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#2732}{\htmlId{5000}{\htmlClass{Generalizable}{\text{rwds}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3339}{\htmlId{5007}{\htmlClass{Generalizable}{\text{dep}}}}\, \end{pmatrix}$
⇀⦇ dereg c md ,DELEG⦈
$\begin{pmatrix} \,\href{Ledger.Conway.Conformance.Certs.html#2928}{\htmlId{5049}{\htmlClass{Generalizable}{\text{vDelegs}}}}\, \,\href{Axiom.Set.Map.html#10748}{\htmlId{5057}{\htmlClass{Function Operator}{\text{∣}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{5059}{\htmlClass{Field Operator}{\text{❴}}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#3216}{\htmlId{5061}{\htmlClass{Generalizable}{\text{c}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{5063}{\htmlClass{Field Operator}{\text{❵}}}}\, \,\href{Axiom.Set.Map.html#10748}{\htmlId{5065}{\htmlClass{Function Operator}{\text{ᶜ}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#2823}{\htmlId{5069}{\htmlClass{Generalizable}{\text{sDelegs}}}}\, \,\href{Axiom.Set.Map.html#10748}{\htmlId{5077}{\htmlClass{Function Operator}{\text{∣}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{5079}{\htmlClass{Field Operator}{\text{❴}}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#3216}{\htmlId{5081}{\htmlClass{Generalizable}{\text{c}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{5083}{\htmlClass{Field Operator}{\text{❵}}}}\, \,\href{Axiom.Set.Map.html#10748}{\htmlId{5085}{\htmlClass{Function Operator}{\text{ᶜ}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#2732}{\htmlId{5089}{\htmlClass{Generalizable}{\text{rwds}}}}\, \,\href{Axiom.Set.Map.html#10748}{\htmlId{5094}{\htmlClass{Function Operator}{\text{∣}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{5096}{\htmlClass{Field Operator}{\text{❴}}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#3216}{\htmlId{5098}{\htmlClass{Generalizable}{\text{c}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{5100}{\htmlClass{Field Operator}{\text{❵}}}}\, \,\href{Axiom.Set.Map.html#10748}{\htmlId{5102}{\htmlClass{Function Operator}{\text{ᶜ}}}}\,
\\ \,\href{Ledger.Conway.Conformance.Certs.html#1868}{\htmlId{5112}{\htmlClass{Function}{\text{updateCertDeposit}}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#3514}{\htmlId{5130}{\htmlClass{Generalizable}{\text{pp}}}}\, (\,\href{Ledger.Conway.Certs.html#1446}{\htmlId{5134}{\htmlClass{InductiveConstructor}{\text{dereg}}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#3216}{\htmlId{5140}{\htmlClass{Generalizable}{\text{c}}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#3186}{\htmlId{5142}{\htmlClass{Generalizable}{\text{md}}}}\,) \,\href{Ledger.Conway.Conformance.Certs.html#3339}{\htmlId{5146}{\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#3514}{\htmlId{5285}{\htmlClass{Generalizable}{\text{pp}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#2975}{\htmlId{5290}{\htmlClass{Generalizable}{\text{pools}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3282}{\htmlId{5298}{\htmlClass{Generalizable}{\text{delegatees}}}}\, \end{pmatrix}$ ⊢
$\begin{pmatrix} \,\href{Ledger.Conway.Conformance.Certs.html#2928}{\htmlId{5323}{\htmlClass{Generalizable}{\text{vDelegs}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#2823}{\htmlId{5333}{\htmlClass{Generalizable}{\text{sDelegs}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#2732}{\htmlId{5343}{\htmlClass{Generalizable}{\text{rwds}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3339}{\htmlId{5350}{\htmlClass{Generalizable}{\text{dep}}}}\, \end{pmatrix}$ ⇀⦇ reg c d ,DELEG⦈
$\begin{pmatrix} \,\href{Ledger.Conway.Conformance.Certs.html#2928}{\htmlId{5385}{\htmlClass{Generalizable}{\text{vDelegs}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#2823}{\htmlId{5395}{\htmlClass{Generalizable}{\text{sDelegs}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#2732}{\htmlId{5405}{\htmlClass{Generalizable}{\text{rwds}}}}\, \,\href{Axiom.Set.Map.html#6320}{\htmlId{5410}{\htmlClass{Function Operator}{\text{∪ˡ}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{5413}{\htmlClass{Field Operator}{\text{❴}}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#3216}{\htmlId{5415}{\htmlClass{Generalizable}{\text{c}}}}\, \\ \,\htmlId{5419}{\htmlClass{Number}{\text{0}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{5421}{\htmlClass{Field Operator}{\text{❵}}}}\,
\\ \,\href{Ledger.Conway.Conformance.Certs.html#1868}{\htmlId{5433}{\htmlClass{Function}{\text{updateCertDeposit}}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#3514}{\htmlId{5451}{\htmlClass{Generalizable}{\text{pp}}}}\, (\,\href{Ledger.Conway.Certs.html#2059}{\htmlId{5455}{\htmlClass{InductiveConstructor}{\text{reg}}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#3216}{\htmlId{5459}{\htmlClass{Generalizable}{\text{c}}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#3162}{\htmlId{5461}{\htmlClass{Generalizable}{\text{d}}}}\,) \,\href{Ledger.Conway.Conformance.Certs.html#3339}{\htmlId{5464}{\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#3367}{\htmlId{5710}{\htmlClass{Generalizable}{\text{e}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#5568}{\htmlId{5714}{\htmlClass{Bound}{\text{pp}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3392}{\htmlId{5719}{\htmlClass{Generalizable}{\text{vs}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3066}{\htmlId{5724}{\htmlClass{Generalizable}{\text{wdrls}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3293}{\htmlId{5732}{\htmlClass{Generalizable}{\text{cc}}}}\, \end{pmatrix}$ ⊢
$\begin{pmatrix} \,\href{Ledger.Conway.Conformance.Certs.html#2777}{\htmlId{5747}{\htmlClass{Generalizable}{\text{dReps}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#2871}{\htmlId{5755}{\htmlClass{Generalizable}{\text{ccKeys}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3339}{\htmlId{5764}{\htmlClass{Generalizable}{\text{dep}}}}\, \end{pmatrix}$
⇀⦇ regdrep c d an ,GOVCERT⦈
$\begin{pmatrix} \,\href{Class.HasSingleton.html#288}{\htmlId{5814}{\htmlClass{Field Operator}{\text{❴}}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#3216}{\htmlId{5816}{\htmlClass{Generalizable}{\text{c}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3367}{\htmlId{5820}{\htmlClass{Generalizable}{\text{e}}}}\, \,\href{Class.HasAdd.Core.html#162}{\htmlId{5822}{\htmlClass{Field Operator}{\text{+}}}}\, \,\href{Ledger.Conway.PParams.html#3478}{\htmlId{5824}{\htmlClass{Field}{\text{drepActivity}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{5837}{\htmlClass{Field Operator}{\text{❵}}}}\, \,\href{Axiom.Set.Map.html#6320}{\htmlId{5839}{\htmlClass{Function Operator}{\text{∪ˡ}}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#2777}{\htmlId{5842}{\htmlClass{Generalizable}{\text{dReps}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#2871}{\htmlId{5850}{\htmlClass{Generalizable}{\text{ccKeys}}}}\,
\\ \,\href{Ledger.Conway.Conformance.Certs.html#1868}{\htmlId{5865}{\htmlClass{Function}{\text{updateCertDeposit}}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#5568}{\htmlId{5883}{\htmlClass{Bound}{\text{pp}}}}\, (\,\href{Ledger.Conway.Certs.html#1579}{\htmlId{5887}{\htmlClass{InductiveConstructor}{\text{regdrep}}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#3216}{\htmlId{5895}{\htmlClass{Generalizable}{\text{c}}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#3162}{\htmlId{5897}{\htmlClass{Generalizable}{\text{d}}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#3109}{\htmlId{5899}{\htmlClass{Generalizable}{\text{an}}}}\, ) \,\href{Ledger.Conway.Conformance.Certs.html#3339}{\htmlId{5904}{\htmlClass{Generalizable}{\text{dep}}}}\, \end{pmatrix}$
GOVCERT-deregdrep :
∙ c ∈ dom dReps
∙ (DRepDeposit c , d) ∈ dep
────────────────────────────────
$\begin{pmatrix} \,\href{Ledger.Conway.Conformance.Certs.html#3367}{\htmlId{6032}{\htmlClass{Generalizable}{\text{e}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3514}{\htmlId{6036}{\htmlClass{Generalizable}{\text{pp}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3392}{\htmlId{6041}{\htmlClass{Generalizable}{\text{vs}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3066}{\htmlId{6046}{\htmlClass{Generalizable}{\text{wdrls}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3293}{\htmlId{6054}{\htmlClass{Generalizable}{\text{cc}}}}\, \end{pmatrix}$ ⊢ $\begin{pmatrix} \,\href{Ledger.Conway.Conformance.Certs.html#2777}{\htmlId{6063}{\htmlClass{Generalizable}{\text{dReps}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#2871}{\htmlId{6071}{\htmlClass{Generalizable}{\text{ccKeys}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3339}{\htmlId{6080}{\htmlClass{Generalizable}{\text{dep}}}}\, \end{pmatrix}$
⇀⦇ deregdrep c d ,GOVCERT⦈
$\begin{pmatrix} \,\href{Ledger.Conway.Conformance.Certs.html#2777}{\htmlId{6135}{\htmlClass{Generalizable}{\text{dReps}}}}\, \,\href{Axiom.Set.Map.html#10748}{\htmlId{6141}{\htmlClass{Function Operator}{\text{∣}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{6143}{\htmlClass{Field Operator}{\text{❴}}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#3216}{\htmlId{6145}{\htmlClass{Generalizable}{\text{c}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{6147}{\htmlClass{Field Operator}{\text{❵}}}}\, \,\href{Axiom.Set.Map.html#10748}{\htmlId{6149}{\htmlClass{Function Operator}{\text{ᶜ}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#2871}{\htmlId{6153}{\htmlClass{Generalizable}{\text{ccKeys}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#1868}{\htmlId{6162}{\htmlClass{Function}{\text{updateCertDeposit}}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#3514}{\htmlId{6180}{\htmlClass{Generalizable}{\text{pp}}}}\, (\,\href{Ledger.Conway.Certs.html#1630}{\htmlId{6184}{\htmlClass{InductiveConstructor}{\text{deregdrep}}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#3216}{\htmlId{6194}{\htmlClass{Generalizable}{\text{c}}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#3162}{\htmlId{6196}{\htmlClass{Generalizable}{\text{d}}}}\,) \,\href{Ledger.Conway.Conformance.Certs.html#3339}{\htmlId{6199}{\htmlClass{Generalizable}{\text{dep}}}}\, \end{pmatrix}$
GOVCERT-ccreghot :
∙ (c , nothing) ∉ ccKeys
∙ c ∈ cc
────────────────────────────────
$\begin{pmatrix} \,\href{Ledger.Conway.Conformance.Certs.html#3367}{\htmlId{6316}{\htmlClass{Generalizable}{\text{e}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3514}{\htmlId{6320}{\htmlClass{Generalizable}{\text{pp}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3392}{\htmlId{6325}{\htmlClass{Generalizable}{\text{vs}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3066}{\htmlId{6330}{\htmlClass{Generalizable}{\text{wdrls}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3293}{\htmlId{6338}{\htmlClass{Generalizable}{\text{cc}}}}\, \end{pmatrix}$ ⊢ $\begin{pmatrix} \,\href{Ledger.Conway.Conformance.Certs.html#2777}{\htmlId{6347}{\htmlClass{Generalizable}{\text{dReps}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#2871}{\htmlId{6355}{\htmlClass{Generalizable}{\text{ccKeys}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3339}{\htmlId{6364}{\htmlClass{Generalizable}{\text{dep}}}}\, \end{pmatrix}$
⇀⦇ ccreghot c mc ,GOVCERT⦈
$\begin{pmatrix} \,\href{Ledger.Conway.Conformance.Certs.html#2777}{\htmlId{6419}{\htmlClass{Generalizable}{\text{dReps}}}}\, \\ \,\href{Class.HasSingleton.html#288}{\htmlId{6427}{\htmlClass{Field Operator}{\text{❴}}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#3216}{\htmlId{6429}{\htmlClass{Generalizable}{\text{c}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3246}{\htmlId{6433}{\htmlClass{Generalizable}{\text{mc}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{6436}{\htmlClass{Field Operator}{\text{❵}}}}\, \,\href{Axiom.Set.Map.html#6320}{\htmlId{6438}{\htmlClass{Function Operator}{\text{∪ˡ}}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#2871}{\htmlId{6441}{\htmlClass{Generalizable}{\text{ccKeys}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#1868}{\htmlId{6450}{\htmlClass{Function}{\text{updateCertDeposit}}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#3514}{\htmlId{6468}{\htmlClass{Generalizable}{\text{pp}}}}\, (\,\href{Ledger.Conway.Certs.html#1672}{\htmlId{6472}{\htmlClass{InductiveConstructor}{\text{ccreghot}}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#3216}{\htmlId{6481}{\htmlClass{Generalizable}{\text{c}}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#3246}{\htmlId{6483}{\htmlClass{Generalizable}{\text{mc}}}}\,) \,\href{Ledger.Conway.Conformance.Certs.html#3339}{\htmlId{6487}{\htmlClass{Generalizable}{\text{dep}}}}\, \end{pmatrix}$
data _⊢_⇀⦇_,CERT⦈_ : CertEnv → CertState → DCert → CertState → Type where
CERT-deleg :
∙ $\begin{pmatrix} \,\href{Ledger.Conway.Conformance.Certs.html#3514}{\htmlId{6591}{\htmlClass{Generalizable}{\text{pp}}}}\, \\ \,\href{Ledger.Conway.Certs.html#3841}{\htmlId{6596}{\htmlClass{Field}{\text{PState.pools}}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#3614}{\htmlId{6609}{\htmlClass{Generalizable}{\text{stᵖ}}}}\, \\ \,\href{Class.IsSet.html#916}{\htmlId{6615}{\htmlClass{Function}{\text{dom}}}}\, (\,\href{Ledger.Conway.Conformance.Certs.html#849}{\htmlId{6620}{\htmlClass{Field}{\text{GState.dreps}}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#3594}{\htmlId{6633}{\htmlClass{Generalizable}{\text{stᵍ}}}}\,) \end{pmatrix}$ ⊢ stᵈ ⇀⦇ dCert ,DELEG⦈ stᵈ'
────────────────────────────────
$\begin{pmatrix} \,\href{Ledger.Conway.Conformance.Certs.html#3367}{\htmlId{6715}{\htmlClass{Generalizable}{\text{e}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3514}{\htmlId{6719}{\htmlClass{Generalizable}{\text{pp}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3392}{\htmlId{6724}{\htmlClass{Generalizable}{\text{vs}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3066}{\htmlId{6729}{\htmlClass{Generalizable}{\text{wdrls}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3293}{\htmlId{6737}{\htmlClass{Generalizable}{\text{cc}}}}\, \end{pmatrix}$ ⊢ $\begin{pmatrix} \,\href{Ledger.Conway.Conformance.Certs.html#3574}{\htmlId{6746}{\htmlClass{Generalizable}{\text{stᵈ}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3614}{\htmlId{6752}{\htmlClass{Generalizable}{\text{stᵖ}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3594}{\htmlId{6758}{\htmlClass{Generalizable}{\text{stᵍ}}}}\, \end{pmatrix}$ ⇀⦇ dCert ,CERT⦈ $\begin{pmatrix} \,\href{Ledger.Conway.Conformance.Certs.html#3578}{\htmlId{6782}{\htmlClass{Generalizable}{\text{stᵈ'}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3614}{\htmlId{6789}{\htmlClass{Generalizable}{\text{stᵖ}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3594}{\htmlId{6795}{\htmlClass{Generalizable}{\text{stᵍ}}}}\, \end{pmatrix}$
CERT-pool :
∙ pp ⊢ stᵖ ⇀⦇ dCert ,POOL⦈ stᵖ'
────────────────────────────────
$\begin{pmatrix} \,\href{Ledger.Conway.Conformance.Certs.html#3367}{\htmlId{6899}{\htmlClass{Generalizable}{\text{e}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3514}{\htmlId{6903}{\htmlClass{Generalizable}{\text{pp}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3392}{\htmlId{6908}{\htmlClass{Generalizable}{\text{vs}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3066}{\htmlId{6913}{\htmlClass{Generalizable}{\text{wdrls}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3293}{\htmlId{6921}{\htmlClass{Generalizable}{\text{cc}}}}\, \end{pmatrix}$ ⊢ $\begin{pmatrix} \,\href{Ledger.Conway.Conformance.Certs.html#3574}{\htmlId{6930}{\htmlClass{Generalizable}{\text{stᵈ}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3614}{\htmlId{6936}{\htmlClass{Generalizable}{\text{stᵖ}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3594}{\htmlId{6942}{\htmlClass{Generalizable}{\text{stᵍ}}}}\, \end{pmatrix}$ ⇀⦇ dCert ,CERT⦈ $\begin{pmatrix} \,\href{Ledger.Conway.Conformance.Certs.html#3574}{\htmlId{6966}{\htmlClass{Generalizable}{\text{stᵈ}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3618}{\htmlId{6972}{\htmlClass{Generalizable}{\text{stᵖ'}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3594}{\htmlId{6979}{\htmlClass{Generalizable}{\text{stᵍ}}}}\, \end{pmatrix}$
CERT-vdel :
∙ Γ ⊢ stᵍ ⇀⦇ dCert ,GOVCERT⦈ stᵍ'
────────────────────────────────
Γ ⊢ $\begin{pmatrix} \,\href{Ledger.Conway.Conformance.Certs.html#3574}{\htmlId{7089}{\htmlClass{Generalizable}{\text{stᵈ}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3614}{\htmlId{7095}{\htmlClass{Generalizable}{\text{stᵖ}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3594}{\htmlId{7101}{\htmlClass{Generalizable}{\text{stᵍ}}}}\, \end{pmatrix}$ ⇀⦇ dCert ,CERT⦈ $\begin{pmatrix} \,\href{Ledger.Conway.Conformance.Certs.html#3574}{\htmlId{7125}{\htmlClass{Generalizable}{\text{stᵈ}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3614}{\htmlId{7131}{\htmlClass{Generalizable}{\text{stᵖ}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3598}{\htmlId{7137}{\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#3367}{\htmlId{7730}{\htmlClass{Generalizable}{\text{e}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3514}{\htmlId{7734}{\htmlClass{Generalizable}{\text{pp}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3392}{\htmlId{7739}{\htmlClass{Generalizable}{\text{vs}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3066}{\htmlId{7744}{\htmlClass{Generalizable}{\text{wdrls}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3293}{\htmlId{7752}{\htmlClass{Generalizable}{\text{cc}}}}\, \end{pmatrix}$ ⊢
$\begin{pmatrix} \begin{pmatrix} \,\href{Ledger.Conway.Conformance.Certs.html#2936}{\htmlId{7769}{\htmlClass{Generalizable}{\text{voteDelegs}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#2831}{\htmlId{7782}{\htmlClass{Generalizable}{\text{stakeDelegs}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#2737}{\htmlId{7796}{\htmlClass{Generalizable}{\text{rewards}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3343}{\htmlId{7806}{\htmlClass{Generalizable}{\text{ddep}}}}\, \end{pmatrix}
\\ \,\href{Ledger.Conway.Conformance.Certs.html#3614}{\htmlId{7821}{\htmlClass{Generalizable}{\text{stᵖ}}}}\,
\\ \begin{pmatrix} \,\href{Ledger.Conway.Conformance.Certs.html#2777}{\htmlId{7835}{\htmlClass{Generalizable}{\text{dReps}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#2878}{\htmlId{7843}{\htmlClass{Generalizable}{\text{ccHotKeys}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3348}{\htmlId{7855}{\htmlClass{Generalizable}{\text{gdep}}}}\, \end{pmatrix}
\end{pmatrix}$
⇀⦇ _ ,CERTBASE⦈
$\begin{pmatrix} \begin{pmatrix} \,\href{Ledger.Conway.Conformance.Certs.html#7463}{\htmlId{7902}{\htmlClass{Bound}{\text{validVoteDelegs}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#2831}{\htmlId{7920}{\htmlClass{Generalizable}{\text{stakeDelegs}}}}\, \\ \,\href{Axiom.Set.Map.html#9130}{\htmlId{7934}{\htmlClass{Function}{\text{constMap}}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#7414}{\htmlId{7943}{\htmlClass{Bound}{\text{wdrlCreds}}}}\, \,\htmlId{7953}{\htmlClass{Number}{\text{0}}}\, \,\href{Axiom.Set.Map.html#6320}{\htmlId{7955}{\htmlClass{Function Operator}{\text{∪ˡ}}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#2737}{\htmlId{7958}{\htmlClass{Generalizable}{\text{rewards}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3343}{\htmlId{7968}{\htmlClass{Generalizable}{\text{ddep}}}}\, \end{pmatrix}
\\ \,\href{Ledger.Conway.Conformance.Certs.html#3614}{\htmlId{7983}{\htmlClass{Generalizable}{\text{stᵖ}}}}\,
\\ \begin{pmatrix} \,\href{Ledger.Conway.Conformance.Certs.html#7328}{\htmlId{7997}{\htmlClass{Bound}{\text{refreshedDReps}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#2878}{\htmlId{8014}{\htmlClass{Generalizable}{\text{ccHotKeys}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3348}{\htmlId{8026}{\htmlClass{Generalizable}{\text{gdep}}}}\, \end{pmatrix}
\end{pmatrix}$
_⊢_⇀⦇_,CERTS⦈_ : CertEnv → CertState → List DCert → CertState → Type
_⊢_⇀⦇_,CERTS⦈_ = ReflexiveTransitiveClosureᵇ' {_⊢_⇀⟦_⟧ᵇ_ = _⊢_⇀⦇_,CERTBASE⦈_}{_⊢_⇀⦇_,CERT⦈_}