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 : VoteDelegs
stakeDelegs : Credential ⇀ KeyHash
rewards : Rewards
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 : Rewards
dReps : Credential ⇀ Epoch
sDelegs stakeDelegs : Credential ⇀ KeyHash
ccKeys ccHotKeys : Credential ⇀ Maybe Credential
vDelegs voteDelegs : VoteDelegs
pools : Pools
retiring : KeyHash ⇀ Epoch
wdrls : Withdrawals
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 : StakePoolParams
pp : PParams
mv : Maybe VDeleg
stᵈ stᵈ' : DState
stᵍ stᵍ' : GState
stᵖ stᵖ' : PState
open GovVote
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#3038}{\htmlId{3941}{\htmlClass{Generalizable}{\text{pools}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3071}{\htmlId{3949}{\htmlClass{Generalizable}{\text{retiring}}}}\, \end{pmatrix}$ ⇀⦇ regpool kh poolParams ,POOL⦈
$\begin{pmatrix} \,\href{Class.HasSingleton.html#288}{\htmlId{4006}{\htmlClass{Field Operator}{\text{❴}}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#3469}{\htmlId{4008}{\htmlClass{Generalizable}{\text{kh}}}}\, , \,\href{Ledger.Conway.Conformance.Certs.html#3529}{\htmlId{4013}{\htmlClass{Generalizable}{\text{poolParams}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{4024}{\htmlClass{Field Operator}{\text{❵}}}}\, \,\href{Axiom.Set.Map.html#6320}{\htmlId{4026}{\htmlClass{Function Operator}{\text{∪ˡ}}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#3038}{\htmlId{4029}{\htmlClass{Generalizable}{\text{pools}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3071}{\htmlId{4037}{\htmlClass{Generalizable}{\text{retiring}}}}\, \end{pmatrix}$
POOL-retirepool :
────────────────────────────────
pp ⊢ $\begin{pmatrix} \,\href{Ledger.Conway.Conformance.Certs.html#3038}{\htmlId{4117}{\htmlClass{Generalizable}{\text{pools}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3071}{\htmlId{4125}{\htmlClass{Generalizable}{\text{retiring}}}}\, \end{pmatrix}$ ⇀⦇ retirepool kh e ,POOL⦈ $\begin{pmatrix} \,\href{Ledger.Conway.Conformance.Certs.html#3038}{\htmlId{4164}{\htmlClass{Generalizable}{\text{pools}}}}\, \\ \,\href{Class.HasSingleton.html#288}{\htmlId{4172}{\htmlClass{Field Operator}{\text{❴}}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#3469}{\htmlId{4174}{\htmlClass{Generalizable}{\text{kh}}}}\, , \,\href{Ledger.Conway.Conformance.Certs.html#3412}{\htmlId{4179}{\htmlClass{Generalizable}{\text{e}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{4181}{\htmlClass{Field Operator}{\text{❵}}}}\, \,\href{Axiom.Set.Map.html#6320}{\htmlId{4183}{\htmlClass{Function Operator}{\text{∪ˡ}}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#3071}{\htmlId{4186}{\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 ∘ vDelegCredential) delegatees ∪
fromList
( nothing
∷ just vDelegAbstain
∷ just vDelegNoConfidence
∷ []
)
∙ mkh ∈ mapˢ just (dom pools) ∪ ❴ nothing ❵
────────────────────────────────
$\begin{pmatrix} \,\href{Ledger.Conway.Conformance.Certs.html#3564}{\htmlId{4614}{\htmlClass{Generalizable}{\text{pp}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3038}{\htmlId{4619}{\htmlClass{Generalizable}{\text{pools}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3327}{\htmlId{4627}{\htmlClass{Generalizable}{\text{delegatees}}}}\, \end{pmatrix}$ ⊢
$\begin{pmatrix} \,\href{Ledger.Conway.Conformance.Certs.html#3000}{\htmlId{4650}{\htmlClass{Generalizable}{\text{vDelegs}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#2895}{\htmlId{4660}{\htmlClass{Generalizable}{\text{sDelegs}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#2814}{\htmlId{4670}{\htmlClass{Generalizable}{\text{rwds}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3384}{\htmlId{4677}{\htmlClass{Generalizable}{\text{dep}}}}\, \end{pmatrix}$
⇀⦇ delegate c mv mkh d ,DELEG⦈
$\begin{pmatrix} \,\href{Axiom.Set.Map.html#7168}{\htmlId{4728}{\htmlClass{Function}{\text{insertIfJust}}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#3261}{\htmlId{4741}{\htmlClass{Generalizable}{\text{c}}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#3591}{\htmlId{4743}{\htmlClass{Generalizable}{\text{mv}}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#3000}{\htmlId{4746}{\htmlClass{Generalizable}{\text{vDelegs}}}}\, \\ \,\href{Axiom.Set.Map.html#7168}{\htmlId{4756}{\htmlClass{Function}{\text{insertIfJust}}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#3261}{\htmlId{4769}{\htmlClass{Generalizable}{\text{c}}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#3496}{\htmlId{4771}{\htmlClass{Generalizable}{\text{mkh}}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#2895}{\htmlId{4775}{\htmlClass{Generalizable}{\text{sDelegs}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#2814}{\htmlId{4785}{\htmlClass{Generalizable}{\text{rwds}}}}\, \,\href{Axiom.Set.Map.html#6320}{\htmlId{4790}{\htmlClass{Function Operator}{\text{∪ˡ}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{4793}{\htmlClass{Field Operator}{\text{❴}}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#3261}{\htmlId{4795}{\htmlClass{Generalizable}{\text{c}}}}\, , \,\htmlId{4799}{\htmlClass{Number}{\text{0}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{4801}{\htmlClass{Field Operator}{\text{❵}}}}\,
\\ \,\href{Ledger.Conway.Conformance.Certs.html#1950}{\htmlId{4811}{\htmlClass{Function}{\text{updateCertDeposit}}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#3564}{\htmlId{4829}{\htmlClass{Generalizable}{\text{pp}}}}\, \,\htmlId{4832}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Conway.Specification.Certs.html#2899}{\htmlId{4833}{\htmlClass{InductiveConstructor}{\text{delegate}}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#3261}{\htmlId{4842}{\htmlClass{Generalizable}{\text{c}}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#3591}{\htmlId{4844}{\htmlClass{Generalizable}{\text{mv}}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#3496}{\htmlId{4847}{\htmlClass{Generalizable}{\text{mkh}}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#3207}{\htmlId{4851}{\htmlClass{Generalizable}{\text{d}}}}\,\,\htmlId{4852}{\htmlClass{Symbol}{\text{)}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#3384}{\htmlId{4854}{\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#3564}{\htmlId{5016}{\htmlClass{Generalizable}{\text{pp}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3038}{\htmlId{5021}{\htmlClass{Generalizable}{\text{pools}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3327}{\htmlId{5029}{\htmlClass{Generalizable}{\text{delegatees}}}}\, \end{pmatrix}$ ⊢
$\begin{pmatrix} \,\href{Ledger.Conway.Conformance.Certs.html#3000}{\htmlId{5052}{\htmlClass{Generalizable}{\text{vDelegs}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#2895}{\htmlId{5062}{\htmlClass{Generalizable}{\text{sDelegs}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#2814}{\htmlId{5072}{\htmlClass{Generalizable}{\text{rwds}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3384}{\htmlId{5079}{\htmlClass{Generalizable}{\text{dep}}}}\, \end{pmatrix}$
⇀⦇ dereg c md ,DELEG⦈
$\begin{pmatrix} \,\href{Ledger.Conway.Conformance.Certs.html#3000}{\htmlId{5121}{\htmlClass{Generalizable}{\text{vDelegs}}}}\, \,\href{Axiom.Set.Map.html#10748}{\htmlId{5129}{\htmlClass{Function Operator}{\text{∣}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{5131}{\htmlClass{Field Operator}{\text{❴}}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#3261}{\htmlId{5133}{\htmlClass{Generalizable}{\text{c}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{5135}{\htmlClass{Field Operator}{\text{❵}}}}\, \,\href{Axiom.Set.Map.html#10748}{\htmlId{5137}{\htmlClass{Function Operator}{\text{ᶜ}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#2895}{\htmlId{5141}{\htmlClass{Generalizable}{\text{sDelegs}}}}\, \,\href{Axiom.Set.Map.html#10748}{\htmlId{5149}{\htmlClass{Function Operator}{\text{∣}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{5151}{\htmlClass{Field Operator}{\text{❴}}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#3261}{\htmlId{5153}{\htmlClass{Generalizable}{\text{c}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{5155}{\htmlClass{Field Operator}{\text{❵}}}}\, \,\href{Axiom.Set.Map.html#10748}{\htmlId{5157}{\htmlClass{Function Operator}{\text{ᶜ}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#2814}{\htmlId{5161}{\htmlClass{Generalizable}{\text{rwds}}}}\, \,\href{Axiom.Set.Map.html#10748}{\htmlId{5166}{\htmlClass{Function Operator}{\text{∣}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{5168}{\htmlClass{Field Operator}{\text{❴}}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#3261}{\htmlId{5170}{\htmlClass{Generalizable}{\text{c}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{5172}{\htmlClass{Field Operator}{\text{❵}}}}\, \,\href{Axiom.Set.Map.html#10748}{\htmlId{5174}{\htmlClass{Function Operator}{\text{ᶜ}}}}\,
\\ \,\href{Ledger.Conway.Conformance.Certs.html#1950}{\htmlId{5184}{\htmlClass{Function}{\text{updateCertDeposit}}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#3564}{\htmlId{5202}{\htmlClass{Generalizable}{\text{pp}}}}\, \,\htmlId{5205}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Conway.Specification.Certs.html#2972}{\htmlId{5206}{\htmlClass{InductiveConstructor}{\text{dereg}}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#3261}{\htmlId{5212}{\htmlClass{Generalizable}{\text{c}}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#3231}{\htmlId{5214}{\htmlClass{Generalizable}{\text{md}}}}\,\,\htmlId{5216}{\htmlClass{Symbol}{\text{)}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#3384}{\htmlId{5218}{\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#3564}{\htmlId{5357}{\htmlClass{Generalizable}{\text{pp}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3038}{\htmlId{5362}{\htmlClass{Generalizable}{\text{pools}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3327}{\htmlId{5370}{\htmlClass{Generalizable}{\text{delegatees}}}}\, \end{pmatrix}$ ⊢
$\begin{pmatrix} \,\href{Ledger.Conway.Conformance.Certs.html#3000}{\htmlId{5395}{\htmlClass{Generalizable}{\text{vDelegs}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#2895}{\htmlId{5405}{\htmlClass{Generalizable}{\text{sDelegs}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#2814}{\htmlId{5415}{\htmlClass{Generalizable}{\text{rwds}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3384}{\htmlId{5422}{\htmlClass{Generalizable}{\text{dep}}}}\, \end{pmatrix}$ ⇀⦇ reg c d ,DELEG⦈
$\begin{pmatrix} \,\href{Ledger.Conway.Conformance.Certs.html#3000}{\htmlId{5457}{\htmlClass{Generalizable}{\text{vDelegs}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#2895}{\htmlId{5467}{\htmlClass{Generalizable}{\text{sDelegs}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#2814}{\htmlId{5477}{\htmlClass{Generalizable}{\text{rwds}}}}\, \,\href{Axiom.Set.Map.html#6320}{\htmlId{5482}{\htmlClass{Function Operator}{\text{∪ˡ}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{5485}{\htmlClass{Field Operator}{\text{❴}}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#3261}{\htmlId{5487}{\htmlClass{Generalizable}{\text{c}}}}\, , \,\htmlId{5491}{\htmlClass{Number}{\text{0}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{5493}{\htmlClass{Field Operator}{\text{❵}}}}\,
\\ \,\href{Ledger.Conway.Conformance.Certs.html#1950}{\htmlId{5505}{\htmlClass{Function}{\text{updateCertDeposit}}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#3564}{\htmlId{5523}{\htmlClass{Generalizable}{\text{pp}}}}\, \,\htmlId{5526}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Conway.Specification.Certs.html#3608}{\htmlId{5527}{\htmlClass{InductiveConstructor}{\text{reg}}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#3261}{\htmlId{5531}{\htmlClass{Generalizable}{\text{c}}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#3207}{\htmlId{5533}{\htmlClass{Generalizable}{\text{d}}}}\,\,\htmlId{5534}{\htmlClass{Symbol}{\text{)}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#3384}{\htmlId{5536}{\htmlClass{Generalizable}{\text{dep}}}}\, \end{pmatrix}$
data _⊢_⇀⦇_,GOVCERT⦈_ : CertEnv → 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#3412}{\htmlId{5779}{\htmlClass{Generalizable}{\text{e}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#5637}{\htmlId{5783}{\htmlClass{Bound}{\text{pp}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3437}{\htmlId{5788}{\htmlClass{Generalizable}{\text{vs}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3114}{\htmlId{5793}{\htmlClass{Generalizable}{\text{wdrls}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3338}{\htmlId{5801}{\htmlClass{Generalizable}{\text{cc}}}}\, \end{pmatrix}$ ⊢
$\begin{pmatrix} \,\href{Ledger.Conway.Conformance.Certs.html#2849}{\htmlId{5816}{\htmlClass{Generalizable}{\text{dReps}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#2943}{\htmlId{5824}{\htmlClass{Generalizable}{\text{ccKeys}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3384}{\htmlId{5833}{\htmlClass{Generalizable}{\text{dep}}}}\, \end{pmatrix}$
⇀⦇ regdrep c d an ,GOVCERT⦈
$\begin{pmatrix} \,\href{Class.HasSingleton.html#288}{\htmlId{5883}{\htmlClass{Field Operator}{\text{❴}}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#3261}{\htmlId{5885}{\htmlClass{Generalizable}{\text{c}}}}\, , \,\href{Ledger.Conway.Conformance.Certs.html#3412}{\htmlId{5889}{\htmlClass{Generalizable}{\text{e}}}}\, \,\href{Class.HasAdd.Core.html#162}{\htmlId{5891}{\htmlClass{Field Operator}{\text{+}}}}\, \,\href{Ledger.Conway.Specification.PParams.html#4875}{\htmlId{5893}{\htmlClass{Field}{\text{drepActivity}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{5906}{\htmlClass{Field Operator}{\text{❵}}}}\, \,\href{Axiom.Set.Map.html#6320}{\htmlId{5908}{\htmlClass{Function Operator}{\text{∪ˡ}}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#2849}{\htmlId{5911}{\htmlClass{Generalizable}{\text{dReps}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#2943}{\htmlId{5919}{\htmlClass{Generalizable}{\text{ccKeys}}}}\,
\\ \,\href{Ledger.Conway.Conformance.Certs.html#1950}{\htmlId{5934}{\htmlClass{Function}{\text{updateCertDeposit}}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#5637}{\htmlId{5952}{\htmlClass{Bound}{\text{pp}}}}\, \,\htmlId{5955}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Conway.Specification.Certs.html#3110}{\htmlId{5956}{\htmlClass{InductiveConstructor}{\text{regdrep}}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#3261}{\htmlId{5964}{\htmlClass{Generalizable}{\text{c}}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#3207}{\htmlId{5966}{\htmlClass{Generalizable}{\text{d}}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#3154}{\htmlId{5968}{\htmlClass{Generalizable}{\text{an}}}}\, \,\htmlId{5971}{\htmlClass{Symbol}{\text{)}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#3384}{\htmlId{5973}{\htmlClass{Generalizable}{\text{dep}}}}\, \end{pmatrix}$
GOVCERT-deregdrep :
∙ c ∈ dom dReps
∙ (DRepDeposit c , d) ∈ dep
────────────────────────────────
$\begin{pmatrix} \,\href{Ledger.Conway.Conformance.Certs.html#3412}{\htmlId{6101}{\htmlClass{Generalizable}{\text{e}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3564}{\htmlId{6105}{\htmlClass{Generalizable}{\text{pp}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3437}{\htmlId{6110}{\htmlClass{Generalizable}{\text{vs}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3114}{\htmlId{6115}{\htmlClass{Generalizable}{\text{wdrls}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3338}{\htmlId{6123}{\htmlClass{Generalizable}{\text{cc}}}}\, \end{pmatrix}$ ⊢ $\begin{pmatrix} \,\href{Ledger.Conway.Conformance.Certs.html#2849}{\htmlId{6132}{\htmlClass{Generalizable}{\text{dReps}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#2943}{\htmlId{6140}{\htmlClass{Generalizable}{\text{ccKeys}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3384}{\htmlId{6149}{\htmlClass{Generalizable}{\text{dep}}}}\, \end{pmatrix}$
⇀⦇ deregdrep c d ,GOVCERT⦈
$\begin{pmatrix} \,\href{Ledger.Conway.Conformance.Certs.html#2849}{\htmlId{6204}{\htmlClass{Generalizable}{\text{dReps}}}}\, \,\href{Axiom.Set.Map.html#10748}{\htmlId{6210}{\htmlClass{Function Operator}{\text{∣}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{6212}{\htmlClass{Field Operator}{\text{❴}}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#3261}{\htmlId{6214}{\htmlClass{Generalizable}{\text{c}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{6216}{\htmlClass{Field Operator}{\text{❵}}}}\, \,\href{Axiom.Set.Map.html#10748}{\htmlId{6218}{\htmlClass{Function Operator}{\text{ᶜ}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#2943}{\htmlId{6222}{\htmlClass{Generalizable}{\text{ccKeys}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#1950}{\htmlId{6231}{\htmlClass{Function}{\text{updateCertDeposit}}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#3564}{\htmlId{6249}{\htmlClass{Generalizable}{\text{pp}}}}\, \,\htmlId{6252}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Conway.Specification.Certs.html#3161}{\htmlId{6253}{\htmlClass{InductiveConstructor}{\text{deregdrep}}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#3261}{\htmlId{6263}{\htmlClass{Generalizable}{\text{c}}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#3207}{\htmlId{6265}{\htmlClass{Generalizable}{\text{d}}}}\,\,\htmlId{6266}{\htmlClass{Symbol}{\text{)}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#3384}{\htmlId{6268}{\htmlClass{Generalizable}{\text{dep}}}}\, \end{pmatrix}$
GOVCERT-ccreghot :
∙ (c , nothing) ∉ ccKeys
∙ c ∈ cc
────────────────────────────────
$\begin{pmatrix} \,\href{Ledger.Conway.Conformance.Certs.html#3412}{\htmlId{6385}{\htmlClass{Generalizable}{\text{e}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3564}{\htmlId{6389}{\htmlClass{Generalizable}{\text{pp}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3437}{\htmlId{6394}{\htmlClass{Generalizable}{\text{vs}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3114}{\htmlId{6399}{\htmlClass{Generalizable}{\text{wdrls}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3338}{\htmlId{6407}{\htmlClass{Generalizable}{\text{cc}}}}\, \end{pmatrix}$ ⊢ $\begin{pmatrix} \,\href{Ledger.Conway.Conformance.Certs.html#2849}{\htmlId{6416}{\htmlClass{Generalizable}{\text{dReps}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#2943}{\htmlId{6424}{\htmlClass{Generalizable}{\text{ccKeys}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3384}{\htmlId{6433}{\htmlClass{Generalizable}{\text{dep}}}}\, \end{pmatrix}$
⇀⦇ ccreghot c mc ,GOVCERT⦈
$\begin{pmatrix} \,\href{Ledger.Conway.Conformance.Certs.html#2849}{\htmlId{6488}{\htmlClass{Generalizable}{\text{dReps}}}}\, \\ \,\href{Class.HasSingleton.html#288}{\htmlId{6496}{\htmlClass{Field Operator}{\text{❴}}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#3261}{\htmlId{6498}{\htmlClass{Generalizable}{\text{c}}}}\, , \,\href{Ledger.Conway.Conformance.Certs.html#3291}{\htmlId{6502}{\htmlClass{Generalizable}{\text{mc}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{6505}{\htmlClass{Field Operator}{\text{❵}}}}\, \,\href{Axiom.Set.Map.html#6320}{\htmlId{6507}{\htmlClass{Function Operator}{\text{∪ˡ}}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#2943}{\htmlId{6510}{\htmlClass{Generalizable}{\text{ccKeys}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#1950}{\htmlId{6519}{\htmlClass{Function}{\text{updateCertDeposit}}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#3564}{\htmlId{6537}{\htmlClass{Generalizable}{\text{pp}}}}\, \,\htmlId{6540}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Conway.Specification.Certs.html#3203}{\htmlId{6541}{\htmlClass{InductiveConstructor}{\text{ccreghot}}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#3261}{\htmlId{6550}{\htmlClass{Generalizable}{\text{c}}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#3291}{\htmlId{6552}{\htmlClass{Generalizable}{\text{mc}}}}\,\,\htmlId{6554}{\htmlClass{Symbol}{\text{)}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#3384}{\htmlId{6556}{\htmlClass{Generalizable}{\text{dep}}}}\, \end{pmatrix}$
data _⊢_⇀⦇_,CERT⦈_ : CertEnv → CertState → DCert → CertState → Type where
CERT-deleg :
∙ $\begin{pmatrix} \,\href{Ledger.Conway.Conformance.Certs.html#3564}{\htmlId{6660}{\htmlClass{Generalizable}{\text{pp}}}}\, \\ \,\href{Ledger.Conway.Specification.Certs.html#4853}{\htmlId{6665}{\htmlClass{Field}{\text{PState.pools}}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#3664}{\htmlId{6678}{\htmlClass{Generalizable}{\text{stᵖ}}}}\, \\ \,\href{Class.IsSet.html#916}{\htmlId{6684}{\htmlClass{Function}{\text{dom}}}}\, \,\htmlId{6688}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Conway.Conformance.Certs.html#931}{\htmlId{6689}{\htmlClass{Field}{\text{GState.dreps}}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#3644}{\htmlId{6702}{\htmlClass{Generalizable}{\text{stᵍ}}}}\,\,\htmlId{6705}{\htmlClass{Symbol}{\text{)}}}\, \end{pmatrix}$ ⊢ stᵈ ⇀⦇ dCert ,DELEG⦈ stᵈ'
────────────────────────────────
$\begin{pmatrix} \,\href{Ledger.Conway.Conformance.Certs.html#3412}{\htmlId{6784}{\htmlClass{Generalizable}{\text{e}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3564}{\htmlId{6788}{\htmlClass{Generalizable}{\text{pp}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3437}{\htmlId{6793}{\htmlClass{Generalizable}{\text{vs}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3114}{\htmlId{6798}{\htmlClass{Generalizable}{\text{wdrls}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3338}{\htmlId{6806}{\htmlClass{Generalizable}{\text{cc}}}}\, \end{pmatrix}$ ⊢ $\begin{pmatrix} \,\href{Ledger.Conway.Conformance.Certs.html#3624}{\htmlId{6815}{\htmlClass{Generalizable}{\text{stᵈ}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3664}{\htmlId{6821}{\htmlClass{Generalizable}{\text{stᵖ}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3644}{\htmlId{6827}{\htmlClass{Generalizable}{\text{stᵍ}}}}\, \end{pmatrix}$ ⇀⦇ dCert ,CERT⦈ $\begin{pmatrix} \,\href{Ledger.Conway.Conformance.Certs.html#3628}{\htmlId{6851}{\htmlClass{Generalizable}{\text{stᵈ'}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3664}{\htmlId{6858}{\htmlClass{Generalizable}{\text{stᵖ}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3644}{\htmlId{6864}{\htmlClass{Generalizable}{\text{stᵍ}}}}\, \end{pmatrix}$
CERT-pool :
∙ pp ⊢ stᵖ ⇀⦇ dCert ,POOL⦈ stᵖ'
────────────────────────────────
$\begin{pmatrix} \,\href{Ledger.Conway.Conformance.Certs.html#3412}{\htmlId{6968}{\htmlClass{Generalizable}{\text{e}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3564}{\htmlId{6972}{\htmlClass{Generalizable}{\text{pp}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3437}{\htmlId{6977}{\htmlClass{Generalizable}{\text{vs}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3114}{\htmlId{6982}{\htmlClass{Generalizable}{\text{wdrls}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3338}{\htmlId{6990}{\htmlClass{Generalizable}{\text{cc}}}}\, \end{pmatrix}$ ⊢ $\begin{pmatrix} \,\href{Ledger.Conway.Conformance.Certs.html#3624}{\htmlId{6999}{\htmlClass{Generalizable}{\text{stᵈ}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3664}{\htmlId{7005}{\htmlClass{Generalizable}{\text{stᵖ}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3644}{\htmlId{7011}{\htmlClass{Generalizable}{\text{stᵍ}}}}\, \end{pmatrix}$ ⇀⦇ dCert ,CERT⦈ $\begin{pmatrix} \,\href{Ledger.Conway.Conformance.Certs.html#3624}{\htmlId{7035}{\htmlClass{Generalizable}{\text{stᵈ}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3668}{\htmlId{7041}{\htmlClass{Generalizable}{\text{stᵖ'}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3644}{\htmlId{7048}{\htmlClass{Generalizable}{\text{stᵍ}}}}\, \end{pmatrix}$
CERT-vdel :
∙ Γ ⊢ stᵍ ⇀⦇ dCert ,GOVCERT⦈ stᵍ'
────────────────────────────────
Γ ⊢ $\begin{pmatrix} \,\href{Ledger.Conway.Conformance.Certs.html#3624}{\htmlId{7158}{\htmlClass{Generalizable}{\text{stᵈ}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3664}{\htmlId{7164}{\htmlClass{Generalizable}{\text{stᵖ}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3644}{\htmlId{7170}{\htmlClass{Generalizable}{\text{stᵍ}}}}\, \end{pmatrix}$ ⇀⦇ dCert ,CERT⦈ $\begin{pmatrix} \,\href{Ledger.Conway.Conformance.Certs.html#3624}{\htmlId{7194}{\htmlClass{Generalizable}{\text{stᵈ}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3664}{\htmlId{7200}{\htmlClass{Generalizable}{\text{stᵖ}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3648}{\htmlId{7206}{\htmlClass{Generalizable}{\text{stᵍ'}}}}\, \end{pmatrix}$
data _⊢_⇀⦇_,CERTBASE⦈_ : CertEnv → CertState → ⊤ → CertState → Type where
CERT-base :
let open PParams pp
refresh = mapPartial (isGovVoterDRep ∘ voter) (fromList vs)
refreshedDReps = mapValueRestricted (const (e + drepActivity)) dReps refresh
wdrlCreds = mapˢ stake (dom wdrls)
validVoteDelegs = voteDelegs ∣^ (mapˢ vDelegCredential (dom dReps) ∪ fromList (vDelegNoConfidence ∷ vDelegAbstain ∷ []))
in
∙ filterˢ isKeyHash wdrlCreds ⊆ dom voteDelegs
∙ mapˢ (map₁ stake) (wdrls ˢ) ⊆ rewards ˢ
────────────────────────────────
$\begin{pmatrix} \,\href{Ledger.Conway.Conformance.Certs.html#3412}{\htmlId{7818}{\htmlClass{Generalizable}{\text{e}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3564}{\htmlId{7822}{\htmlClass{Generalizable}{\text{pp}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3437}{\htmlId{7827}{\htmlClass{Generalizable}{\text{vs}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3114}{\htmlId{7832}{\htmlClass{Generalizable}{\text{wdrls}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3338}{\htmlId{7840}{\htmlClass{Generalizable}{\text{cc}}}}\, \end{pmatrix}$ ⊢
$\begin{pmatrix} \begin{pmatrix} \,\href{Ledger.Conway.Conformance.Certs.html#3008}{\htmlId{7857}{\htmlClass{Generalizable}{\text{voteDelegs}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#2903}{\htmlId{7870}{\htmlClass{Generalizable}{\text{stakeDelegs}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#2819}{\htmlId{7884}{\htmlClass{Generalizable}{\text{rewards}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3388}{\htmlId{7894}{\htmlClass{Generalizable}{\text{ddep}}}}\, \end{pmatrix}
\\ \,\href{Ledger.Conway.Conformance.Certs.html#3664}{\htmlId{7909}{\htmlClass{Generalizable}{\text{stᵖ}}}}\,
\\ \begin{pmatrix} \,\href{Ledger.Conway.Conformance.Certs.html#2849}{\htmlId{7923}{\htmlClass{Generalizable}{\text{dReps}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#2950}{\htmlId{7931}{\htmlClass{Generalizable}{\text{ccHotKeys}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3393}{\htmlId{7943}{\htmlClass{Generalizable}{\text{gdep}}}}\, \end{pmatrix}
\end{pmatrix}$
⇀⦇ _ ,CERTBASE⦈
$\begin{pmatrix} \begin{pmatrix} \,\href{Ledger.Conway.Conformance.Certs.html#7545}{\htmlId{7990}{\htmlClass{Bound}{\text{validVoteDelegs}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#2903}{\htmlId{8008}{\htmlClass{Generalizable}{\text{stakeDelegs}}}}\, \\ \,\href{Axiom.Set.Map.html#9130}{\htmlId{8022}{\htmlClass{Function}{\text{constMap}}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#7496}{\htmlId{8031}{\htmlClass{Bound}{\text{wdrlCreds}}}}\, \,\htmlId{8041}{\htmlClass{Number}{\text{0}}}\, \,\href{Axiom.Set.Map.html#6320}{\htmlId{8043}{\htmlClass{Function Operator}{\text{∪ˡ}}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#2819}{\htmlId{8046}{\htmlClass{Generalizable}{\text{rewards}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3388}{\htmlId{8056}{\htmlClass{Generalizable}{\text{ddep}}}}\, \end{pmatrix}
\\ \,\href{Ledger.Conway.Conformance.Certs.html#3664}{\htmlId{8071}{\htmlClass{Generalizable}{\text{stᵖ}}}}\,
\\ \begin{pmatrix} \,\href{Ledger.Conway.Conformance.Certs.html#7410}{\htmlId{8085}{\htmlClass{Bound}{\text{refreshedDReps}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#2950}{\htmlId{8102}{\htmlClass{Generalizable}{\text{ccHotKeys}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3393}{\htmlId{8114}{\htmlClass{Generalizable}{\text{gdep}}}}\, \end{pmatrix}
\end{pmatrix}$
_⊢_⇀⦇_,CERTS⦈_ : CertEnv → CertState → List DCert → CertState → Type
_⊢_⇀⦇_,CERTS⦈_ = ReflexiveTransitiveClosureᵇ' {_⊢_⇀⟦_⟧ᵇ_ = _⊢_⇀⦇_,CERTBASE⦈_}{_⊢_⇀⦇_,CERT⦈_}