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;
_⊢_⇀⦇_,DELEG⦈_; _⊢_⇀⦇_,GOVCERT⦈_;
_⊢_⇀⦇_,CERT⦈_; _⊢_⇀⦇_,PRE-CERT⦈_; _⊢_⇀⦇_,CERTS⦈_; ⟦_,_,_⟧ᵈ)
open RewardAddress
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 fPools : 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
stᶜ stᶜ' : CertState
open GovVote
data _⊢_⇀⦇_,DELEG⦈_ : DelegEnv → DState → DCert → DState → Type
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#3558}{\htmlId{4195}{\htmlClass{Generalizable}{\text{pp}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3032}{\htmlId{4200}{\htmlClass{Generalizable}{\text{pools}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3321}{\htmlId{4208}{\htmlClass{Generalizable}{\text{delegatees}}}}\, \end{pmatrix}$ ⊢
$\begin{pmatrix} \,\href{Ledger.Conway.Conformance.Certs.html#2994}{\htmlId{4231}{\htmlClass{Generalizable}{\text{vDelegs}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#2889}{\htmlId{4241}{\htmlClass{Generalizable}{\text{sDelegs}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#2808}{\htmlId{4251}{\htmlClass{Generalizable}{\text{rwds}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3378}{\htmlId{4258}{\htmlClass{Generalizable}{\text{dep}}}}\, \end{pmatrix}$
⇀⦇ delegate c mv mkh d ,DELEG⦈
$\begin{pmatrix} \,\href{Axiom.Set.Map.html#9262}{\htmlId{4309}{\htmlClass{Function}{\text{insertIfJust}}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#3255}{\htmlId{4322}{\htmlClass{Generalizable}{\text{c}}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#3585}{\htmlId{4324}{\htmlClass{Generalizable}{\text{mv}}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#2994}{\htmlId{4327}{\htmlClass{Generalizable}{\text{vDelegs}}}}\, \\ \,\href{Axiom.Set.Map.html#9262}{\htmlId{4337}{\htmlClass{Function}{\text{insertIfJust}}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#3255}{\htmlId{4350}{\htmlClass{Generalizable}{\text{c}}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#3490}{\htmlId{4352}{\htmlClass{Generalizable}{\text{mkh}}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#2889}{\htmlId{4356}{\htmlClass{Generalizable}{\text{sDelegs}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#2808}{\htmlId{4366}{\htmlClass{Generalizable}{\text{rwds}}}}\, \,\href{Axiom.Set.Map.html#7640}{\htmlId{4371}{\htmlClass{Function Operator}{\text{∪ˡ}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{4374}{\htmlClass{Field Operator}{\text{❴}}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#3255}{\htmlId{4376}{\htmlClass{Generalizable}{\text{c}}}}\, , \,\htmlId{4380}{\htmlClass{Number}{\text{0}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{4382}{\htmlClass{Field Operator}{\text{❵}}}}\,
\\ \,\href{Ledger.Conway.Conformance.Certs.html#1944}{\htmlId{4392}{\htmlClass{Function}{\text{updateCertDeposit}}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#3558}{\htmlId{4410}{\htmlClass{Generalizable}{\text{pp}}}}\, \,\htmlId{4413}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Conway.Specification.Certs.html#2482}{\htmlId{4414}{\htmlClass{InductiveConstructor}{\text{delegate}}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#3255}{\htmlId{4423}{\htmlClass{Generalizable}{\text{c}}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#3585}{\htmlId{4425}{\htmlClass{Generalizable}{\text{mv}}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#3490}{\htmlId{4428}{\htmlClass{Generalizable}{\text{mkh}}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#3201}{\htmlId{4432}{\htmlClass{Generalizable}{\text{d}}}}\,\,\htmlId{4433}{\htmlClass{Symbol}{\text{)}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#3378}{\htmlId{4435}{\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#3558}{\htmlId{4597}{\htmlClass{Generalizable}{\text{pp}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3032}{\htmlId{4602}{\htmlClass{Generalizable}{\text{pools}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3321}{\htmlId{4610}{\htmlClass{Generalizable}{\text{delegatees}}}}\, \end{pmatrix}$ ⊢
$\begin{pmatrix} \,\href{Ledger.Conway.Conformance.Certs.html#2994}{\htmlId{4633}{\htmlClass{Generalizable}{\text{vDelegs}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#2889}{\htmlId{4643}{\htmlClass{Generalizable}{\text{sDelegs}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#2808}{\htmlId{4653}{\htmlClass{Generalizable}{\text{rwds}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3378}{\htmlId{4660}{\htmlClass{Generalizable}{\text{dep}}}}\, \end{pmatrix}$
⇀⦇ dereg c md ,DELEG⦈
$\begin{pmatrix} \,\href{Ledger.Conway.Conformance.Certs.html#2994}{\htmlId{4702}{\htmlClass{Generalizable}{\text{vDelegs}}}}\, \,\href{Axiom.Set.Map.html#13606}{\htmlId{4710}{\htmlClass{Function Operator}{\text{∣}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{4712}{\htmlClass{Field Operator}{\text{❴}}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#3255}{\htmlId{4714}{\htmlClass{Generalizable}{\text{c}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{4716}{\htmlClass{Field Operator}{\text{❵}}}}\, \,\href{Axiom.Set.Map.html#13606}{\htmlId{4718}{\htmlClass{Function Operator}{\text{ᶜ}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#2889}{\htmlId{4722}{\htmlClass{Generalizable}{\text{sDelegs}}}}\, \,\href{Axiom.Set.Map.html#13606}{\htmlId{4730}{\htmlClass{Function Operator}{\text{∣}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{4732}{\htmlClass{Field Operator}{\text{❴}}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#3255}{\htmlId{4734}{\htmlClass{Generalizable}{\text{c}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{4736}{\htmlClass{Field Operator}{\text{❵}}}}\, \,\href{Axiom.Set.Map.html#13606}{\htmlId{4738}{\htmlClass{Function Operator}{\text{ᶜ}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#2808}{\htmlId{4742}{\htmlClass{Generalizable}{\text{rwds}}}}\, \,\href{Axiom.Set.Map.html#13606}{\htmlId{4747}{\htmlClass{Function Operator}{\text{∣}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{4749}{\htmlClass{Field Operator}{\text{❴}}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#3255}{\htmlId{4751}{\htmlClass{Generalizable}{\text{c}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{4753}{\htmlClass{Field Operator}{\text{❵}}}}\, \,\href{Axiom.Set.Map.html#13606}{\htmlId{4755}{\htmlClass{Function Operator}{\text{ᶜ}}}}\,
\\ \,\href{Ledger.Conway.Conformance.Certs.html#1944}{\htmlId{4765}{\htmlClass{Function}{\text{updateCertDeposit}}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#3558}{\htmlId{4783}{\htmlClass{Generalizable}{\text{pp}}}}\, \,\htmlId{4786}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Conway.Specification.Certs.html#2555}{\htmlId{4787}{\htmlClass{InductiveConstructor}{\text{dereg}}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#3255}{\htmlId{4793}{\htmlClass{Generalizable}{\text{c}}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#3225}{\htmlId{4795}{\htmlClass{Generalizable}{\text{md}}}}\,\,\htmlId{4797}{\htmlClass{Symbol}{\text{)}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#3378}{\htmlId{4799}{\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#3558}{\htmlId{4938}{\htmlClass{Generalizable}{\text{pp}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3032}{\htmlId{4943}{\htmlClass{Generalizable}{\text{pools}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3321}{\htmlId{4951}{\htmlClass{Generalizable}{\text{delegatees}}}}\, \end{pmatrix}$ ⊢
$\begin{pmatrix} \,\href{Ledger.Conway.Conformance.Certs.html#2994}{\htmlId{4976}{\htmlClass{Generalizable}{\text{vDelegs}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#2889}{\htmlId{4986}{\htmlClass{Generalizable}{\text{sDelegs}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#2808}{\htmlId{4996}{\htmlClass{Generalizable}{\text{rwds}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3378}{\htmlId{5003}{\htmlClass{Generalizable}{\text{dep}}}}\, \end{pmatrix}$ ⇀⦇ reg c d ,DELEG⦈
$\begin{pmatrix} \,\href{Ledger.Conway.Conformance.Certs.html#2994}{\htmlId{5038}{\htmlClass{Generalizable}{\text{vDelegs}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#2889}{\htmlId{5048}{\htmlClass{Generalizable}{\text{sDelegs}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#2808}{\htmlId{5058}{\htmlClass{Generalizable}{\text{rwds}}}}\, \,\href{Axiom.Set.Map.html#7640}{\htmlId{5063}{\htmlClass{Function Operator}{\text{∪ˡ}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{5066}{\htmlClass{Field Operator}{\text{❴}}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#3255}{\htmlId{5068}{\htmlClass{Generalizable}{\text{c}}}}\, , \,\htmlId{5072}{\htmlClass{Number}{\text{0}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{5074}{\htmlClass{Field Operator}{\text{❵}}}}\,
\\ \,\href{Ledger.Conway.Conformance.Certs.html#1944}{\htmlId{5086}{\htmlClass{Function}{\text{updateCertDeposit}}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#3558}{\htmlId{5104}{\htmlClass{Generalizable}{\text{pp}}}}\, \,\htmlId{5107}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Conway.Specification.Certs.html#3190}{\htmlId{5108}{\htmlClass{InductiveConstructor}{\text{reg}}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#3255}{\htmlId{5112}{\htmlClass{Generalizable}{\text{c}}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#3201}{\htmlId{5114}{\htmlClass{Generalizable}{\text{d}}}}\,\,\htmlId{5115}{\htmlClass{Symbol}{\text{)}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#3378}{\htmlId{5117}{\htmlClass{Generalizable}{\text{dep}}}}\, \end{pmatrix}$
data _⊢_⇀⦇_,GOVCERT⦈_ : CertEnv → CertState → DCert → CertState → 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#3406}{\htmlId{5366}{\htmlClass{Generalizable}{\text{e}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#5224}{\htmlId{5370}{\htmlClass{Bound}{\text{pp}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3431}{\htmlId{5375}{\htmlClass{Generalizable}{\text{vs}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3108}{\htmlId{5380}{\htmlClass{Generalizable}{\text{wdrls}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3332}{\htmlId{5388}{\htmlClass{Generalizable}{\text{cc}}}}\, \end{pmatrix}$ ⊢
$\begin{pmatrix} \,\href{Ledger.Conway.Conformance.Certs.html#3618}{\htmlId{5403}{\htmlClass{Generalizable}{\text{stᵈ}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3658}{\htmlId{5409}{\htmlClass{Generalizable}{\text{stᵖ}}}}\, \\ \begin{pmatrix} \,\href{Ledger.Conway.Conformance.Certs.html#2843}{\htmlId{5417}{\htmlClass{Generalizable}{\text{dReps}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#2937}{\htmlId{5425}{\htmlClass{Generalizable}{\text{ccKeys}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3378}{\htmlId{5434}{\htmlClass{Generalizable}{\text{dep}}}}\, \end{pmatrix} \end{pmatrix}$
⇀⦇ regdrep c d an ,GOVCERT⦈
$\begin{pmatrix} \,\href{Ledger.Conway.Conformance.Certs.html#3618}{\htmlId{5486}{\htmlClass{Generalizable}{\text{stᵈ}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3658}{\htmlId{5492}{\htmlClass{Generalizable}{\text{stᵖ}}}}\, \\ \begin{pmatrix} \,\href{Class.HasSingleton.html#288}{\htmlId{5500}{\htmlClass{Field Operator}{\text{❴}}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#3255}{\htmlId{5502}{\htmlClass{Generalizable}{\text{c}}}}\, , \,\href{Ledger.Conway.Conformance.Certs.html#3406}{\htmlId{5506}{\htmlClass{Generalizable}{\text{e}}}}\, \,\href{Class.HasAdd.Core.html#162}{\htmlId{5508}{\htmlClass{Field Operator}{\text{+}}}}\, \,\href{Ledger.Conway.Specification.PParams.html#7184}{\htmlId{5510}{\htmlClass{Field}{\text{drepActivity}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{5523}{\htmlClass{Field Operator}{\text{❵}}}}\, \,\href{Axiom.Set.Map.html#7640}{\htmlId{5525}{\htmlClass{Function Operator}{\text{∪ˡ}}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#2843}{\htmlId{5528}{\htmlClass{Generalizable}{\text{dReps}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#2937}{\htmlId{5536}{\htmlClass{Generalizable}{\text{ccKeys}}}}\,
\\ \,\href{Ledger.Conway.Conformance.Certs.html#1944}{\htmlId{5551}{\htmlClass{Function}{\text{updateCertDeposit}}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#5224}{\htmlId{5569}{\htmlClass{Bound}{\text{pp}}}}\, \,\htmlId{5572}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Conway.Specification.Certs.html#2693}{\htmlId{5573}{\htmlClass{InductiveConstructor}{\text{regdrep}}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#3255}{\htmlId{5581}{\htmlClass{Generalizable}{\text{c}}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#3201}{\htmlId{5583}{\htmlClass{Generalizable}{\text{d}}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#3148}{\htmlId{5585}{\htmlClass{Generalizable}{\text{an}}}}\, \,\htmlId{5588}{\htmlClass{Symbol}{\text{)}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#3378}{\htmlId{5590}{\htmlClass{Generalizable}{\text{dep}}}}\, \end{pmatrix} \end{pmatrix}$
GOVCERT-deregdrep :
∙ c ∈ dom dReps
∙ (DRepDeposit c , d) ∈ dep
────────────────────────────────
$\begin{pmatrix} \,\href{Ledger.Conway.Conformance.Certs.html#3406}{\htmlId{5720}{\htmlClass{Generalizable}{\text{e}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3558}{\htmlId{5724}{\htmlClass{Generalizable}{\text{pp}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3431}{\htmlId{5729}{\htmlClass{Generalizable}{\text{vs}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3108}{\htmlId{5734}{\htmlClass{Generalizable}{\text{wdrls}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3332}{\htmlId{5742}{\htmlClass{Generalizable}{\text{cc}}}}\, \end{pmatrix}$ ⊢ $\begin{pmatrix} \begin{pmatrix} \,\href{Ledger.Conway.Conformance.Certs.html#2994}{\htmlId{5753}{\htmlClass{Generalizable}{\text{vDelegs}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#2889}{\htmlId{5763}{\htmlClass{Generalizable}{\text{sDelegs}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#2808}{\htmlId{5773}{\htmlClass{Generalizable}{\text{rwds}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3382}{\htmlId{5780}{\htmlClass{Generalizable}{\text{ddep}}}}\, \end{pmatrix} \\ \,\href{Ledger.Conway.Conformance.Certs.html#3658}{\htmlId{5790}{\htmlClass{Generalizable}{\text{stᵖ}}}}\, \\ \begin{pmatrix} \,\href{Ledger.Conway.Conformance.Certs.html#2843}{\htmlId{5798}{\htmlClass{Generalizable}{\text{dReps}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#2937}{\htmlId{5806}{\htmlClass{Generalizable}{\text{ccKeys}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3378}{\htmlId{5815}{\htmlClass{Generalizable}{\text{dep}}}}\, \end{pmatrix} \end{pmatrix}$
⇀⦇ deregdrep c d ,GOVCERT⦈
$\begin{pmatrix} \begin{pmatrix} \,\href{Ledger.Conway.Conformance.Certs.html#2994}{\htmlId{5874}{\htmlClass{Generalizable}{\text{vDelegs}}}}\, \,\href{Axiom.Set.Map.html#17850}{\htmlId{5882}{\htmlClass{Function Operator}{\text{∣\^{}}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{5885}{\htmlClass{Field Operator}{\text{❴}}}}\, \,\href{Ledger.Conway.Specification.Gov.Actions.html#8450}{\htmlId{5887}{\htmlClass{InductiveConstructor}{\text{vDelegCredential}}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#3255}{\htmlId{5904}{\htmlClass{Generalizable}{\text{c}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{5906}{\htmlClass{Field Operator}{\text{❵}}}}\, \,\href{Axiom.Set.Map.html#17850}{\htmlId{5908}{\htmlClass{Function Operator}{\text{ᶜ}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#2889}{\htmlId{5912}{\htmlClass{Generalizable}{\text{sDelegs}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#2808}{\htmlId{5922}{\htmlClass{Generalizable}{\text{rwds}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3382}{\htmlId{5929}{\htmlClass{Generalizable}{\text{ddep}}}}\, \end{pmatrix} \\ \,\href{Ledger.Conway.Conformance.Certs.html#3658}{\htmlId{5939}{\htmlClass{Generalizable}{\text{stᵖ}}}}\, \\ \begin{pmatrix} \,\href{Ledger.Conway.Conformance.Certs.html#2843}{\htmlId{5947}{\htmlClass{Generalizable}{\text{dReps}}}}\, \,\href{Axiom.Set.Map.html#13606}{\htmlId{5953}{\htmlClass{Function Operator}{\text{∣}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{5955}{\htmlClass{Field Operator}{\text{❴}}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#3255}{\htmlId{5957}{\htmlClass{Generalizable}{\text{c}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{5959}{\htmlClass{Field Operator}{\text{❵}}}}\, \,\href{Axiom.Set.Map.html#13606}{\htmlId{5961}{\htmlClass{Function Operator}{\text{ᶜ}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#2937}{\htmlId{5965}{\htmlClass{Generalizable}{\text{ccKeys}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#1944}{\htmlId{5974}{\htmlClass{Function}{\text{updateCertDeposit}}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#3558}{\htmlId{5992}{\htmlClass{Generalizable}{\text{pp}}}}\, \,\htmlId{5995}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Conway.Specification.Certs.html#2744}{\htmlId{5996}{\htmlClass{InductiveConstructor}{\text{deregdrep}}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#3255}{\htmlId{6006}{\htmlClass{Generalizable}{\text{c}}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#3201}{\htmlId{6008}{\htmlClass{Generalizable}{\text{d}}}}\,\,\htmlId{6009}{\htmlClass{Symbol}{\text{)}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#3378}{\htmlId{6011}{\htmlClass{Generalizable}{\text{dep}}}}\, \end{pmatrix} \end{pmatrix}$
GOVCERT-ccreghot :
∙ (c , nothing) ∉ ccKeys
∙ c ∈ cc
────────────────────────────────
$\begin{pmatrix} \,\href{Ledger.Conway.Conformance.Certs.html#3406}{\htmlId{6130}{\htmlClass{Generalizable}{\text{e}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3558}{\htmlId{6134}{\htmlClass{Generalizable}{\text{pp}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3431}{\htmlId{6139}{\htmlClass{Generalizable}{\text{vs}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3108}{\htmlId{6144}{\htmlClass{Generalizable}{\text{wdrls}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3332}{\htmlId{6152}{\htmlClass{Generalizable}{\text{cc}}}}\, \end{pmatrix}$ ⊢ $\begin{pmatrix} \,\href{Ledger.Conway.Conformance.Certs.html#3618}{\htmlId{6161}{\htmlClass{Generalizable}{\text{stᵈ}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3658}{\htmlId{6167}{\htmlClass{Generalizable}{\text{stᵖ}}}}\, \\ \begin{pmatrix} \,\href{Ledger.Conway.Conformance.Certs.html#2843}{\htmlId{6175}{\htmlClass{Generalizable}{\text{dReps}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#2937}{\htmlId{6183}{\htmlClass{Generalizable}{\text{ccKeys}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3378}{\htmlId{6192}{\htmlClass{Generalizable}{\text{dep}}}}\, \end{pmatrix} \end{pmatrix}$
⇀⦇ ccreghot c mc ,GOVCERT⦈
$\begin{pmatrix} \,\href{Ledger.Conway.Conformance.Certs.html#3618}{\htmlId{6249}{\htmlClass{Generalizable}{\text{stᵈ}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3658}{\htmlId{6255}{\htmlClass{Generalizable}{\text{stᵖ}}}}\, \\ \begin{pmatrix} \,\href{Ledger.Conway.Conformance.Certs.html#2843}{\htmlId{6263}{\htmlClass{Generalizable}{\text{dReps}}}}\, \\ \,\href{Class.HasSingleton.html#288}{\htmlId{6271}{\htmlClass{Field Operator}{\text{❴}}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#3255}{\htmlId{6273}{\htmlClass{Generalizable}{\text{c}}}}\, , \,\href{Ledger.Conway.Conformance.Certs.html#3285}{\htmlId{6277}{\htmlClass{Generalizable}{\text{mc}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{6280}{\htmlClass{Field Operator}{\text{❵}}}}\, \,\href{Axiom.Set.Map.html#7640}{\htmlId{6282}{\htmlClass{Function Operator}{\text{∪ˡ}}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#2937}{\htmlId{6285}{\htmlClass{Generalizable}{\text{ccKeys}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#1944}{\htmlId{6294}{\htmlClass{Function}{\text{updateCertDeposit}}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#3558}{\htmlId{6312}{\htmlClass{Generalizable}{\text{pp}}}}\, \,\htmlId{6315}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Conway.Specification.Certs.html#2786}{\htmlId{6316}{\htmlClass{InductiveConstructor}{\text{ccreghot}}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#3255}{\htmlId{6325}{\htmlClass{Generalizable}{\text{c}}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#3285}{\htmlId{6327}{\htmlClass{Generalizable}{\text{mc}}}}\,\,\htmlId{6329}{\htmlClass{Symbol}{\text{)}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#3378}{\htmlId{6331}{\htmlClass{Generalizable}{\text{dep}}}}\, \end{pmatrix} \end{pmatrix}$
data _⊢_⇀⦇_,CERT⦈_ : CertEnv → CertState → DCert → CertState → Type where
CERT-deleg :
∙ $\begin{pmatrix} \,\href{Ledger.Conway.Conformance.Certs.html#3558}{\htmlId{6437}{\htmlClass{Generalizable}{\text{pp}}}}\, \\ \,\href{Ledger.Conway.Specification.Certs.html#4604}{\htmlId{6442}{\htmlClass{Field}{\text{PState.pools}}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#3658}{\htmlId{6455}{\htmlClass{Generalizable}{\text{stᵖ}}}}\, \\ \,\href{Class.IsSet.html#916}{\htmlId{6461}{\htmlClass{Function}{\text{dom}}}}\, \,\htmlId{6465}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Conway.Conformance.Certs.html#925}{\htmlId{6466}{\htmlClass{Field}{\text{GState.dreps}}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#3638}{\htmlId{6479}{\htmlClass{Generalizable}{\text{stᵍ}}}}\,\,\htmlId{6482}{\htmlClass{Symbol}{\text{)}}}\, \end{pmatrix}$ ⊢ stᵈ ⇀⦇ dCert ,DELEG⦈ stᵈ'
────────────────────────────────
$\begin{pmatrix} \,\href{Ledger.Conway.Conformance.Certs.html#3406}{\htmlId{6561}{\htmlClass{Generalizable}{\text{e}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3558}{\htmlId{6565}{\htmlClass{Generalizable}{\text{pp}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3431}{\htmlId{6570}{\htmlClass{Generalizable}{\text{vs}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3108}{\htmlId{6575}{\htmlClass{Generalizable}{\text{wdrls}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3332}{\htmlId{6583}{\htmlClass{Generalizable}{\text{cc}}}}\, \end{pmatrix}$ ⊢ $\begin{pmatrix} \,\href{Ledger.Conway.Conformance.Certs.html#3618}{\htmlId{6592}{\htmlClass{Generalizable}{\text{stᵈ}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3658}{\htmlId{6598}{\htmlClass{Generalizable}{\text{stᵖ}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3638}{\htmlId{6604}{\htmlClass{Generalizable}{\text{stᵍ}}}}\, \end{pmatrix}$ ⇀⦇ dCert ,CERT⦈ $\begin{pmatrix} \,\href{Ledger.Conway.Conformance.Certs.html#3622}{\htmlId{6628}{\htmlClass{Generalizable}{\text{stᵈ'}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3658}{\htmlId{6635}{\htmlClass{Generalizable}{\text{stᵖ}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3638}{\htmlId{6641}{\htmlClass{Generalizable}{\text{stᵍ}}}}\, \end{pmatrix}$
CERT-pool :
∙ pp ⊢ stᵖ ⇀⦇ dCert ,POOL⦈ stᵖ'
────────────────────────────────
$\begin{pmatrix} \,\href{Ledger.Conway.Conformance.Certs.html#3406}{\htmlId{6745}{\htmlClass{Generalizable}{\text{e}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3558}{\htmlId{6749}{\htmlClass{Generalizable}{\text{pp}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3431}{\htmlId{6754}{\htmlClass{Generalizable}{\text{vs}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3108}{\htmlId{6759}{\htmlClass{Generalizable}{\text{wdrls}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3332}{\htmlId{6767}{\htmlClass{Generalizable}{\text{cc}}}}\, \end{pmatrix}$ ⊢ $\begin{pmatrix} \,\href{Ledger.Conway.Conformance.Certs.html#3618}{\htmlId{6776}{\htmlClass{Generalizable}{\text{stᵈ}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3658}{\htmlId{6782}{\htmlClass{Generalizable}{\text{stᵖ}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3638}{\htmlId{6788}{\htmlClass{Generalizable}{\text{stᵍ}}}}\, \end{pmatrix}$ ⇀⦇ dCert ,CERT⦈ $\begin{pmatrix} \,\href{Ledger.Conway.Conformance.Certs.html#3618}{\htmlId{6812}{\htmlClass{Generalizable}{\text{stᵈ}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3662}{\htmlId{6818}{\htmlClass{Generalizable}{\text{stᵖ'}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3638}{\htmlId{6825}{\htmlClass{Generalizable}{\text{stᵍ}}}}\, \end{pmatrix}$
CERT-vdel :
∙ Γ ⊢ stᶜ ⇀⦇ dCert ,GOVCERT⦈ stᶜ'
────────────────────────────────
Γ ⊢ stᶜ ⇀⦇ dCert ,CERT⦈ stᶜ'
data _⊢_⇀⦇_,PRE-CERT⦈_ : CertEnv → CertState → ⊤ → CertState → Type where
CERT-pre :
let open PParams pp
refresh = mapPartial (isGovVoterDRep ∘ voter) (fromList vs)
refreshedDReps = mapValueRestricted (const (e + drepActivity)) dReps refresh
wdrlCreds = mapˢ stake (dom wdrls)
in
∙ filterˢ isKeyHash wdrlCreds ⊆ dom voteDelegs
∙ mapˢ (map₁ stake) (wdrls ˢ) ⊆ rewards ˢ
────────────────────────────────
$\begin{pmatrix} \,\href{Ledger.Conway.Conformance.Certs.html#3406}{\htmlId{7433}{\htmlClass{Generalizable}{\text{e}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3558}{\htmlId{7437}{\htmlClass{Generalizable}{\text{pp}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3431}{\htmlId{7442}{\htmlClass{Generalizable}{\text{vs}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3108}{\htmlId{7447}{\htmlClass{Generalizable}{\text{wdrls}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3332}{\htmlId{7455}{\htmlClass{Generalizable}{\text{cc}}}}\, \end{pmatrix}$ ⊢ $\begin{pmatrix} \begin{pmatrix} \,\href{Ledger.Conway.Conformance.Certs.html#3002}{\htmlId{7466}{\htmlClass{Generalizable}{\text{voteDelegs}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#2897}{\htmlId{7479}{\htmlClass{Generalizable}{\text{stakeDelegs}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#2813}{\htmlId{7493}{\htmlClass{Generalizable}{\text{rewards}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3382}{\htmlId{7503}{\htmlClass{Generalizable}{\text{ddep}}}}\, \end{pmatrix} \\ \,\href{Ledger.Conway.Conformance.Certs.html#3658}{\htmlId{7512}{\htmlClass{Generalizable}{\text{stᵖ}}}}\, \\ \begin{pmatrix} \,\href{Ledger.Conway.Conformance.Certs.html#2843}{\htmlId{7520}{\htmlClass{Generalizable}{\text{dReps}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#2944}{\htmlId{7528}{\htmlClass{Generalizable}{\text{ccHotKeys}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3387}{\htmlId{7540}{\htmlClass{Generalizable}{\text{gdep}}}}\, \end{pmatrix} \end{pmatrix}$
⇀⦇ _ ,PRE-CERT⦈
$\begin{pmatrix} \begin{pmatrix} \,\href{Ledger.Conway.Conformance.Certs.html#3002}{\htmlId{7581}{\htmlClass{Generalizable}{\text{voteDelegs}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#2897}{\htmlId{7594}{\htmlClass{Generalizable}{\text{stakeDelegs}}}}\, \\ \,\href{Axiom.Set.Map.html#11988}{\htmlId{7608}{\htmlClass{Function}{\text{constMap}}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#7241}{\htmlId{7617}{\htmlClass{Bound}{\text{wdrlCreds}}}}\, \,\htmlId{7627}{\htmlClass{Number}{\text{0}}}\, \,\href{Axiom.Set.Map.html#7640}{\htmlId{7629}{\htmlClass{Function Operator}{\text{∪ˡ}}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#2813}{\htmlId{7632}{\htmlClass{Generalizable}{\text{rewards}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3382}{\htmlId{7642}{\htmlClass{Generalizable}{\text{ddep}}}}\, \end{pmatrix} \\ \,\href{Ledger.Conway.Conformance.Certs.html#3658}{\htmlId{7651}{\htmlClass{Generalizable}{\text{stᵖ}}}}\, \\ \begin{pmatrix} \,\href{Ledger.Conway.Conformance.Certs.html#7155}{\htmlId{7659}{\htmlClass{Bound}{\text{refreshedDReps}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#2944}{\htmlId{7676}{\htmlClass{Generalizable}{\text{ccHotKeys}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3387}{\htmlId{7688}{\htmlClass{Generalizable}{\text{gdep}}}}\, \end{pmatrix} \end{pmatrix}$
_⊢_⇀⦇_,CERTS⦈_ : CertEnv → CertState → List DCert → CertState → Type
_⊢_⇀⦇_,CERTS⦈_ = RunTraceAfter _⊢_⇀⦇_,PRE-CERT⦈_ _⊢_⇀⦇_,CERT⦈_