{-# OPTIONS --safe #-}
open import Ledger.Dijkstra.Specification.Gov.Base using (GovStructure)
module Ledger.Dijkstra.Specification.Certs
(gs : GovStructure) (open GovStructure gs) where
open import Ledger.Prelude renaming (filterˢ to filter)
open import Ledger.Prelude.Numeric.UnitInterval
open import Ledger.Dijkstra.Specification.Gov.Actions gs hiding (yes; no)
open RewardAddress
open PParams
record StakePoolParams : Type where
field
owners : ℙ KeyHash
cost : Coin
margin : UnitInterval
pledge : Coin
rewardAccount : Credential
CCHotKeys : Type
CCHotKeys = Credential ⇀ Maybe Credential
PoolEnv : Type
PoolEnv = PParams
Pools : Type
Pools = KeyHash ⇀ StakePoolParams
Retiring : Type
Retiring = KeyHash ⇀ Epoch
Rewards : Type
Rewards = Credential ⇀ Coin
Stake : Type
Stake = Credential ⇀ Coin
StakeDelegs : Type
StakeDelegs = Credential ⇀ KeyHash
data DCert : Type where
delegate : Credential → Maybe VDeleg → Maybe KeyHash → Coin → DCert
dereg : Credential → Maybe Coin → DCert
regpool : KeyHash → StakePoolParams → DCert
retirepool : KeyHash → Epoch → DCert
regdrep : Credential → Coin → Anchor → DCert
deregdrep : Credential → Coin → DCert
ccreghot : Credential → Maybe Credential → DCert
cwitness : DCert → Maybe Credential
cwitness (delegate c _ _ _) = just c
cwitness (dereg c _) = just c
cwitness (regpool kh _) = just $ KeyHashObj kh
cwitness (retirepool kh _) = just $ KeyHashObj kh
cwitness (regdrep c _ _) = just c
cwitness (deregdrep c _) = just c
cwitness (ccreghot c _) = just c
record CertEnv : Type where
field
epoch : Epoch
pp : PParams
votes : List GovVote
wdrls : Withdrawals
coldCreds : ℙ Credential
record DState : Type where
constructor ⟦_,_,_⟧ᵈ
field
voteDelegs : VoteDelegs
stakeDelegs : StakeDelegs
rewards : Rewards
deposits : Credential ⇀ Coin
record PState : Type where
field
pools : Pools
fPools : Pools
retiring : KeyHash ⇀ Epoch
deposits : KeyHash ⇀ Coin
record GState : Type where
constructor ⟦_,_⟧ᵛ
field
dreps : DReps
ccHotKeys : Credential ⇀ Maybe Credential
deposits : Credential ⇀ Coin
record CertState : Type where
constructor ⟦_,_,_⟧ᶜˢ
field
dState : DState
pState : PState
gState : GState
record DelegEnv : Type where
field
pparams : PParams
pools : Pools
delegatees : ℙ Credential
record HasDeposits (A : Type) {K : Type} : Type where
field DepositsOf : A → K ⇀ Coin
open HasDeposits ⦃...⦄ public
record HasCCHotKeys {a} (A : Type a) : Type a where
field CCHotKeysOf : A → CCHotKeys
open HasCCHotKeys ⦃...⦄ public
record HasPools {a} (A : Type a) : Type a where
field PoolsOf : A → Pools
open HasPools ⦃...⦄ public
record HasRetiring {a} (A : Type a) : Type a where
field RetiringOf : A → Retiring
open HasRetiring ⦃...⦄ public
record HasRewards {a} (A : Type a) : Type a where
field RewardsOf : A → Rewards
open HasRewards ⦃...⦄ public
record HasStake {a} (A : Type a) : Type a where
field StakeOf : A -> Stake
open HasStake ⦃...⦄ public
record HasStakeDelegs {a} (A : Type a) : Type a where
field StakeDelegsOf : A -> StakeDelegs
open HasStakeDelegs ⦃...⦄ public
record HasDState {a} (A : Type a) : Type a where
field DStateOf : A → DState
open HasDState ⦃...⦄ public
record HasPState {a} (A : Type a) : Type a where
field PStateOf : A → PState
open HasPState ⦃...⦄ public
record HasGState {a} (A : Type a) : Type a where
field GStateOf : A → GState
open HasGState ⦃...⦄ public
record HasCertState {a} (A : Type a) : Type a where
field CertStateOf : A → CertState
open HasCertState ⦃...⦄ public
instance
HasPParams-CertEnv : HasPParams CertEnv
HasPParams-CertEnv .PParamsOf = CertEnv.pp
HasWithdrawals-CertEnv : HasWithdrawals CertEnv
HasWithdrawals-CertEnv .WithdrawalsOf = CertEnv.wdrls
HasVoteDelegs-DState : HasVoteDelegs DState
HasVoteDelegs-DState .VoteDelegsOf = DState.voteDelegs
HasStakeDelegs-DState : HasStakeDelegs DState
HasStakeDelegs-DState .StakeDelegsOf = DState.stakeDelegs
HasRewards-DState : HasRewards DState
HasRewards-DState .RewardsOf = DState.rewards
HasDeposits-DState : HasDeposits DState
HasDeposits-DState .DepositsOf = DState.deposits
HasPools-PState : HasPools PState
HasPools-PState .PoolsOf = PState.pools
HasDeposits-PState : HasDeposits PState
HasDeposits-PState .DepositsOf = PState.deposits
HasRetiring-PState : HasRetiring PState
HasRetiring-PState .RetiringOf = PState.retiring
HasDReps-GState : HasDReps GState
HasDReps-GState .DRepsOf = GState.dreps
HasCCHotKeys-GState : HasCCHotKeys GState
HasCCHotKeys-GState .CCHotKeysOf = GState.ccHotKeys
HasDeposits-GState : HasDeposits GState
HasDeposits-GState .DepositsOf = GState.deposits
HasDState-CertState : HasDState CertState
HasDState-CertState .DStateOf = CertState.dState
HasPState-CertState : HasPState CertState
HasPState-CertState .PStateOf = CertState.pState
HasGState-CertState : HasGState CertState
HasGState-CertState .GStateOf = CertState.gState
HasRewards-CertState : HasRewards CertState
HasRewards-CertState .RewardsOf = RewardsOf ∘ DStateOf
HasDReps-CertState : HasDReps CertState
HasDReps-CertState .DRepsOf = DRepsOf ∘ GStateOf
HasCCHotKeys-CertState : HasCCHotKeys CertState
HasCCHotKeys-CertState .CCHotKeysOf = CCHotKeysOf ∘ GStateOf
HasPools-CertState : HasPools CertState
HasPools-CertState .PoolsOf = PoolsOf ∘ PStateOf
HasVoteDelegs-CertState : HasVoteDelegs CertState
HasVoteDelegs-CertState .VoteDelegsOf = VoteDelegsOf ∘ DStateOf
HasStakeDelegs-CertState : HasStakeDelegs CertState
HasStakeDelegs-CertState .StakeDelegsOf = StakeDelegsOf ∘ DStateOf
unquoteDecl HasCast-CertEnv HasCast-DState HasCast-PState HasCast-GState HasCast-CertState HasCast-DelegEnv = derive-HasCast
( (quote CertEnv , HasCast-CertEnv)
∷ (quote DState , HasCast-DState)
∷ (quote PState , HasCast-PState)
∷ (quote GState , HasCast-GState)
∷ (quote CertState , HasCast-CertState)
∷ [ (quote DelegEnv , HasCast-DelegEnv) ])
private variable
rwds rewards : Rewards
dReps : DReps
sDelegs stakeDelegs : StakeDelegs
ccKeys ccHotKeys : CCHotKeys
vDelegs voteDelegs : VoteDelegs
pools fPools : Pools
retiring : Retiring
wdrls : Withdrawals
A : Type
deposits deposits' : A ⇀ Coin
an : Anchor
Γ : CertEnv
d : Coin
md : Maybe Coin
c : Credential
mc : Maybe Credential
delegatees : ℙ Credential
dCert : DCert
e : Epoch
vs : List GovVote
kh : KeyHash
mkh : Maybe KeyHash
poolParams : StakePoolParams
pp : PParams
mvd : Maybe VDeleg
stᵈ stᵈ' : DState
stᵍ stᵍ' : GState
stᵖ stᵖ' : PState
cc : ℙ Credential
rewardsBalance : DState → Coin
rewardsBalance ds = ∑[ x ← RewardsOf ds ] x
instance
HasCoin-CertState : HasCoin CertState
HasCoin-CertState .getCoin = rewardsBalance ∘ DStateOf
data _⊢_⇀⦇_,DELEG⦈_ : DelegEnv → DState → DCert → DState → Type where
DELEG-delegate :
∙ (c ∉ dom rwds → d ≡ pp .keyDeposit)
∙ (c ∈ dom rwds → d ≡ 0)
∙ mvd ∈ mapˢ (just ∘ vDelegCredential) delegatees ∪
fromList ( nothing ∷ just vDelegAbstain ∷ just vDelegNoConfidence ∷ [] )
∙ mkh ∈ mapˢ just (dom pools) ∪ ❴ nothing ❵
────────────────────────────────
$\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Certs.html#7061}{\htmlId{7817}{\htmlClass{Generalizable}{\text{pp}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#6541}{\htmlId{7822}{\htmlClass{Generalizable}{\text{pools}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#6873}{\htmlId{7830}{\htmlClass{Generalizable}{\text{delegatees}}}}\, \end{pmatrix}$ ⊢ $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Certs.html#6503}{\htmlId{7847}{\htmlClass{Generalizable}{\text{vDelegs}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#6427}{\htmlId{7857}{\htmlClass{Generalizable}{\text{sDelegs}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#6359}{\htmlId{7867}{\htmlClass{Generalizable}{\text{rwds}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#6681}{\htmlId{7874}{\htmlClass{Generalizable}{\text{deposits}}}}\, \end{pmatrix}$ ⇀⦇ delegate c mvd mkh d ,DELEG⦈ $\begin{pmatrix} \,\href{Axiom.Set.Map.html#9262}{\htmlId{7919}{\htmlClass{Function}{\text{insertIfJust}}}}\, \,\href{Ledger.Dijkstra.Specification.Certs.html#6813}{\htmlId{7932}{\htmlClass{Generalizable}{\text{c}}}}\, \,\href{Ledger.Dijkstra.Specification.Certs.html#7085}{\htmlId{7934}{\htmlClass{Generalizable}{\text{mvd}}}}\, \,\href{Ledger.Dijkstra.Specification.Certs.html#6503}{\htmlId{7938}{\htmlClass{Generalizable}{\text{vDelegs}}}}\, \\ \,\href{Axiom.Set.Map.html#9262}{\htmlId{7948}{\htmlClass{Function}{\text{insertIfJust}}}}\, \,\href{Ledger.Dijkstra.Specification.Certs.html#6813}{\htmlId{7961}{\htmlClass{Generalizable}{\text{c}}}}\, \,\href{Ledger.Dijkstra.Specification.Certs.html#6999}{\htmlId{7963}{\htmlClass{Generalizable}{\text{mkh}}}}\, \,\href{Ledger.Dijkstra.Specification.Certs.html#6427}{\htmlId{7967}{\htmlClass{Generalizable}{\text{sDelegs}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#6359}{\htmlId{7977}{\htmlClass{Generalizable}{\text{rwds}}}}\, \,\href{Axiom.Set.Map.html#7640}{\htmlId{7982}{\htmlClass{Function Operator}{\text{∪ˡ}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{7985}{\htmlClass{Field Operator}{\text{❴}}}}\, \,\href{Ledger.Dijkstra.Specification.Certs.html#6813}{\htmlId{7987}{\htmlClass{Generalizable}{\text{c}}}}\, , \,\htmlId{7991}{\htmlClass{Number}{\text{0}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{7993}{\htmlClass{Field Operator}{\text{❵}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#6681}{\htmlId{7997}{\htmlClass{Generalizable}{\text{deposits}}}}\, \,\href{Axiom.Set.Map.Dec.html#2149}{\htmlId{8006}{\htmlClass{Function Operator}{\text{∪⁺}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{8009}{\htmlClass{Field Operator}{\text{❴}}}}\, \,\href{Ledger.Dijkstra.Specification.Certs.html#6813}{\htmlId{8011}{\htmlClass{Generalizable}{\text{c}}}}\, , \,\href{Ledger.Dijkstra.Specification.Certs.html#6765}{\htmlId{8015}{\htmlClass{Generalizable}{\text{d}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{8017}{\htmlClass{Field Operator}{\text{❵}}}}\, \end{pmatrix}$
DELEG-dereg :
∙ (c , 0) ∈ rwds
∙ (c , d) ∈ deposits
∙ md ≡ nothing ⊎ md ≡ just d
────────────────────────────────
$\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Certs.html#7061}{\htmlId{8164}{\htmlClass{Generalizable}{\text{pp}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#6541}{\htmlId{8169}{\htmlClass{Generalizable}{\text{pools}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#6873}{\htmlId{8177}{\htmlClass{Generalizable}{\text{delegatees}}}}\, \end{pmatrix}$ ⊢ $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Certs.html#6503}{\htmlId{8194}{\htmlClass{Generalizable}{\text{vDelegs}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#6427}{\htmlId{8204}{\htmlClass{Generalizable}{\text{sDelegs}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#6359}{\htmlId{8214}{\htmlClass{Generalizable}{\text{rwds}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#6681}{\htmlId{8221}{\htmlClass{Generalizable}{\text{deposits}}}}\, \end{pmatrix}$ ⇀⦇ dereg c md ,DELEG⦈ $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Certs.html#6503}{\htmlId{8256}{\htmlClass{Generalizable}{\text{vDelegs}}}}\, \,\href{Axiom.Set.Map.html#13606}{\htmlId{8264}{\htmlClass{Function Operator}{\text{∣}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{8266}{\htmlClass{Field Operator}{\text{❴}}}}\, \,\href{Ledger.Dijkstra.Specification.Certs.html#6813}{\htmlId{8268}{\htmlClass{Generalizable}{\text{c}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{8270}{\htmlClass{Field Operator}{\text{❵}}}}\, \,\href{Axiom.Set.Map.html#13606}{\htmlId{8272}{\htmlClass{Function Operator}{\text{ᶜ}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#6427}{\htmlId{8276}{\htmlClass{Generalizable}{\text{sDelegs}}}}\, \,\href{Axiom.Set.Map.html#13606}{\htmlId{8284}{\htmlClass{Function Operator}{\text{∣}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{8286}{\htmlClass{Field Operator}{\text{❴}}}}\, \,\href{Ledger.Dijkstra.Specification.Certs.html#6813}{\htmlId{8288}{\htmlClass{Generalizable}{\text{c}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{8290}{\htmlClass{Field Operator}{\text{❵}}}}\, \,\href{Axiom.Set.Map.html#13606}{\htmlId{8292}{\htmlClass{Function Operator}{\text{ᶜ}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#6359}{\htmlId{8296}{\htmlClass{Generalizable}{\text{rwds}}}}\, \,\href{Axiom.Set.Map.html#13606}{\htmlId{8301}{\htmlClass{Function Operator}{\text{∣}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{8303}{\htmlClass{Field Operator}{\text{❴}}}}\, \,\href{Ledger.Dijkstra.Specification.Certs.html#6813}{\htmlId{8305}{\htmlClass{Generalizable}{\text{c}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{8307}{\htmlClass{Field Operator}{\text{❵}}}}\, \,\href{Axiom.Set.Map.html#13606}{\htmlId{8309}{\htmlClass{Function Operator}{\text{ᶜ}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#6681}{\htmlId{8313}{\htmlClass{Generalizable}{\text{deposits}}}}\, \,\href{Axiom.Set.Map.html#13606}{\htmlId{8322}{\htmlClass{Function Operator}{\text{∣}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{8324}{\htmlClass{Field Operator}{\text{❴}}}}\, \,\href{Ledger.Dijkstra.Specification.Certs.html#6813}{\htmlId{8326}{\htmlClass{Generalizable}{\text{c}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{8328}{\htmlClass{Field Operator}{\text{❵}}}}\, \,\href{Axiom.Set.Map.html#13606}{\htmlId{8330}{\htmlClass{Function Operator}{\text{ᶜ}}}}\, \end{pmatrix}$
isPoolRegistered : Pools -> KeyHash -> Maybe StakePoolParams
isPoolRegistered ps kh = lookupᵐ? ps kh
data _⊢_⇀⦇_,POOL⦈_ : PoolEnv → PState → DCert → PState → Type where
POOL-reg :
∙ Is-nothing (isPoolRegistered pools kh)
────────────────────────────────
pp ⊢ $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Certs.html#6541}{\htmlId{8652}{\htmlClass{Generalizable}{\text{pools}}}}\,
\\ \,\href{Ledger.Dijkstra.Specification.Certs.html#6547}{\htmlId{8669}{\htmlClass{Generalizable}{\text{fPools}}}}\,
\\ \,\href{Ledger.Dijkstra.Specification.Certs.html#6574}{\htmlId{8687}{\htmlClass{Generalizable}{\text{retiring}}}}\,
\\ \,\href{Ledger.Dijkstra.Specification.Certs.html#6681}{\htmlId{8707}{\htmlClass{Generalizable}{\text{deposits}}}}\,
\end{pmatrix}$ ⇀⦇ regpool kh poolParams ,POOL⦈ $\begin{pmatrix}
\,\href{Ledger.Dijkstra.Specification.Certs.html#6541}{\htmlId{8772}{\htmlClass{Generalizable}{\text{pools}}}}\, \,\href{Axiom.Set.Map.html#7640}{\htmlId{8778}{\htmlClass{Function Operator}{\text{∪ˡ}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{8781}{\htmlClass{Field Operator}{\text{❴}}}}\, \,\href{Ledger.Dijkstra.Specification.Certs.html#6975}{\htmlId{8783}{\htmlClass{Generalizable}{\text{kh}}}}\, , \,\href{Ledger.Dijkstra.Specification.Certs.html#7029}{\htmlId{8788}{\htmlClass{Generalizable}{\text{poolParams}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{8799}{\htmlClass{Field Operator}{\text{❵}}}}\,
\\ \,\href{Ledger.Dijkstra.Specification.Certs.html#6547}{\htmlId{8812}{\htmlClass{Generalizable}{\text{fPools}}}}\,
\\ \,\href{Ledger.Dijkstra.Specification.Certs.html#6574}{\htmlId{8830}{\htmlClass{Generalizable}{\text{retiring}}}}\,
\\ \,\href{Ledger.Dijkstra.Specification.Certs.html#6681}{\htmlId{8850}{\htmlClass{Generalizable}{\text{deposits}}}}\, \,\href{Axiom.Set.Map.html#7640}{\htmlId{8859}{\htmlClass{Function Operator}{\text{∪ˡ}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{8862}{\htmlClass{Field Operator}{\text{❴}}}}\, \,\href{Ledger.Dijkstra.Specification.Certs.html#6975}{\htmlId{8864}{\htmlClass{Generalizable}{\text{kh}}}}\, , \,\href{Ledger.Dijkstra.Specification.Certs.html#7061}{\htmlId{8869}{\htmlClass{Generalizable}{\text{pp}}}}\, \,\htmlId{8872}{\htmlClass{Symbol}{\text{.}}}\,\,\href{Ledger.Dijkstra.Specification.PParams.html#2502}{\htmlId{8873}{\htmlClass{Field}{\text{poolDeposit}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{8885}{\htmlClass{Field Operator}{\text{❵}}}}\,
\end{pmatrix}$
POOL-rereg :
∙ Is-just (isPoolRegistered pools kh)
────────────────────────────────
pp ⊢ $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Certs.html#6541}{\htmlId{9004}{\htmlClass{Generalizable}{\text{pools}}}}\,
\\ \,\href{Ledger.Dijkstra.Specification.Certs.html#6547}{\htmlId{9021}{\htmlClass{Generalizable}{\text{fPools}}}}\,
\\ \,\href{Ledger.Dijkstra.Specification.Certs.html#6574}{\htmlId{9039}{\htmlClass{Generalizable}{\text{retiring}}}}\,
\\ \,\href{Ledger.Dijkstra.Specification.Certs.html#6681}{\htmlId{9059}{\htmlClass{Generalizable}{\text{deposits}}}}\,
\end{pmatrix}$ ⇀⦇ regpool kh poolParams ,POOL⦈ $\begin{pmatrix}
\,\href{Ledger.Dijkstra.Specification.Certs.html#6541}{\htmlId{9124}{\htmlClass{Generalizable}{\text{pools}}}}\,
\\ \,\href{Class.HasSingleton.html#288}{\htmlId{9141}{\htmlClass{Field Operator}{\text{❴}}}}\, \,\href{Ledger.Dijkstra.Specification.Certs.html#6975}{\htmlId{9143}{\htmlClass{Generalizable}{\text{kh}}}}\, , \,\href{Ledger.Dijkstra.Specification.Certs.html#7029}{\htmlId{9148}{\htmlClass{Generalizable}{\text{poolParams}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{9159}{\htmlClass{Field Operator}{\text{❵}}}}\, \,\href{Axiom.Set.Map.html#7640}{\htmlId{9161}{\htmlClass{Function Operator}{\text{∪ˡ}}}}\, \,\href{Ledger.Dijkstra.Specification.Certs.html#6547}{\htmlId{9164}{\htmlClass{Generalizable}{\text{fPools}}}}\,
\\ \,\href{Ledger.Dijkstra.Specification.Certs.html#6574}{\htmlId{9182}{\htmlClass{Generalizable}{\text{retiring}}}}\, \,\href{Axiom.Set.Map.html#13606}{\htmlId{9191}{\htmlClass{Function Operator}{\text{∣}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{9193}{\htmlClass{Field Operator}{\text{❴}}}}\, \,\href{Ledger.Dijkstra.Specification.Certs.html#6975}{\htmlId{9195}{\htmlClass{Generalizable}{\text{kh}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{9198}{\htmlClass{Field Operator}{\text{❵}}}}\, \,\href{Axiom.Set.Map.html#13606}{\htmlId{9200}{\htmlClass{Function Operator}{\text{ᶜ}}}}\,
\\ \,\href{Ledger.Dijkstra.Specification.Certs.html#6681}{\htmlId{9213}{\htmlClass{Generalizable}{\text{deposits}}}}\,
\end{pmatrix}$
POOL-retirepool :
────────────────────────────────
pp ⊢ $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Certs.html#6541}{\htmlId{9302}{\htmlClass{Generalizable}{\text{pools}}}}\,
\\ \,\href{Ledger.Dijkstra.Specification.Certs.html#6547}{\htmlId{9319}{\htmlClass{Generalizable}{\text{fPools}}}}\,
\\ \,\href{Ledger.Dijkstra.Specification.Certs.html#6574}{\htmlId{9337}{\htmlClass{Generalizable}{\text{retiring}}}}\,
\\ \,\href{Ledger.Dijkstra.Specification.Certs.html#6681}{\htmlId{9357}{\htmlClass{Generalizable}{\text{deposits}}}}\,
\end{pmatrix}$ ⇀⦇ retirepool kh e ,POOL⦈ $\begin{pmatrix}
\,\href{Ledger.Dijkstra.Specification.Certs.html#6541}{\htmlId{9416}{\htmlClass{Generalizable}{\text{pools}}}}\,
\\ \,\href{Ledger.Dijkstra.Specification.Certs.html#6547}{\htmlId{9433}{\htmlClass{Generalizable}{\text{fPools}}}}\,
\\ \,\href{Class.HasSingleton.html#288}{\htmlId{9451}{\htmlClass{Field Operator}{\text{❴}}}}\, \,\href{Ledger.Dijkstra.Specification.Certs.html#6975}{\htmlId{9453}{\htmlClass{Generalizable}{\text{kh}}}}\, , \,\href{Ledger.Dijkstra.Specification.Certs.html#6924}{\htmlId{9458}{\htmlClass{Generalizable}{\text{e}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{9460}{\htmlClass{Field Operator}{\text{❵}}}}\, \,\href{Axiom.Set.Map.html#7640}{\htmlId{9462}{\htmlClass{Function Operator}{\text{∪ˡ}}}}\, \,\href{Ledger.Dijkstra.Specification.Certs.html#6574}{\htmlId{9465}{\htmlClass{Generalizable}{\text{retiring}}}}\,
\\ \,\href{Ledger.Dijkstra.Specification.Certs.html#6681}{\htmlId{9485}{\htmlClass{Generalizable}{\text{deposits}}}}\,
\end{pmatrix}$
data _⊢_⇀⦇_,GOVCERT⦈_ : CertEnv → GState → DCert → GState → Type where
GOVCERT-regdrep :
∙ (d ≡ pp .drepDeposit × c ∉ dom dReps) ⊎ (d ≡ 0 × c ∈ dom dReps)
────────────────────────────────
$\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Certs.html#6924}{\htmlId{9758}{\htmlClass{Generalizable}{\text{e}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#7061}{\htmlId{9762}{\htmlClass{Generalizable}{\text{pp}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#6946}{\htmlId{9767}{\htmlClass{Generalizable}{\text{vs}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#6610}{\htmlId{9772}{\htmlClass{Generalizable}{\text{wdrls}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#7175}{\htmlId{9780}{\htmlClass{Generalizable}{\text{cc}}}}\, \end{pmatrix}$ ⊢ $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Certs.html#6394}{\htmlId{9789}{\htmlClass{Generalizable}{\text{dReps}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#6466}{\htmlId{9797}{\htmlClass{Generalizable}{\text{ccKeys}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#6681}{\htmlId{9806}{\htmlClass{Generalizable}{\text{deposits}}}}\, \end{pmatrix}$ ⇀⦇ regdrep c d an ,GOVCERT⦈ $\begin{pmatrix} \,\href{Class.HasSingleton.html#288}{\htmlId{9847}{\htmlClass{Field Operator}{\text{❴}}}}\, \,\href{Ledger.Dijkstra.Specification.Certs.html#6813}{\htmlId{9849}{\htmlClass{Generalizable}{\text{c}}}}\, , \,\href{Ledger.Dijkstra.Specification.Certs.html#6924}{\htmlId{9853}{\htmlClass{Generalizable}{\text{e}}}}\, \,\href{Class.HasAdd.Core.html#162}{\htmlId{9855}{\htmlClass{Field Operator}{\text{+}}}}\, \,\href{Ledger.Dijkstra.Specification.Certs.html#7061}{\htmlId{9857}{\htmlClass{Generalizable}{\text{pp}}}}\, \,\htmlId{9860}{\htmlClass{Symbol}{\text{.}}}\,\,\href{Ledger.Dijkstra.Specification.PParams.html#3632}{\htmlId{9861}{\htmlClass{Field}{\text{drepActivity}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{9874}{\htmlClass{Field Operator}{\text{❵}}}}\, \,\href{Axiom.Set.Map.html#7640}{\htmlId{9876}{\htmlClass{Function Operator}{\text{∪ˡ}}}}\, \,\href{Ledger.Dijkstra.Specification.Certs.html#6394}{\htmlId{9879}{\htmlClass{Generalizable}{\text{dReps}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#6466}{\htmlId{9887}{\htmlClass{Generalizable}{\text{ccKeys}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#6681}{\htmlId{9896}{\htmlClass{Generalizable}{\text{deposits}}}}\, \,\href{Axiom.Set.Map.Dec.html#2149}{\htmlId{9905}{\htmlClass{Function Operator}{\text{∪⁺}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{9908}{\htmlClass{Field Operator}{\text{❴}}}}\, \,\href{Ledger.Dijkstra.Specification.Certs.html#6813}{\htmlId{9910}{\htmlClass{Generalizable}{\text{c}}}}\, , \,\href{Ledger.Dijkstra.Specification.Certs.html#6765}{\htmlId{9914}{\htmlClass{Generalizable}{\text{d}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{9916}{\htmlClass{Field Operator}{\text{❵}}}}\, \end{pmatrix}$
GOVCERT-deregdrep :
∙ c ∈ dom dReps
∙ (c , d) ∈ deposits
────────────────────────────────
$\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Certs.html#6924}{\htmlId{10035}{\htmlClass{Generalizable}{\text{e}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#7061}{\htmlId{10039}{\htmlClass{Generalizable}{\text{pp}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#6946}{\htmlId{10044}{\htmlClass{Generalizable}{\text{vs}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#6610}{\htmlId{10049}{\htmlClass{Generalizable}{\text{wdrls}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#7175}{\htmlId{10057}{\htmlClass{Generalizable}{\text{cc}}}}\, \end{pmatrix}$ ⊢ $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Certs.html#6394}{\htmlId{10066}{\htmlClass{Generalizable}{\text{dReps}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#6466}{\htmlId{10074}{\htmlClass{Generalizable}{\text{ccKeys}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#6681}{\htmlId{10083}{\htmlClass{Generalizable}{\text{deposits}}}}\, \end{pmatrix}$ ⇀⦇ deregdrep c d ,GOVCERT⦈ $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Certs.html#6394}{\htmlId{10123}{\htmlClass{Generalizable}{\text{dReps}}}}\, \,\href{Axiom.Set.Map.html#13606}{\htmlId{10129}{\htmlClass{Function Operator}{\text{∣}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{10131}{\htmlClass{Field Operator}{\text{❴}}}}\, \,\href{Ledger.Dijkstra.Specification.Certs.html#6813}{\htmlId{10133}{\htmlClass{Generalizable}{\text{c}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{10135}{\htmlClass{Field Operator}{\text{❵}}}}\, \,\href{Axiom.Set.Map.html#13606}{\htmlId{10137}{\htmlClass{Function Operator}{\text{ᶜ}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#6466}{\htmlId{10141}{\htmlClass{Generalizable}{\text{ccKeys}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#6681}{\htmlId{10150}{\htmlClass{Generalizable}{\text{deposits}}}}\, \,\href{Axiom.Set.Map.html#13606}{\htmlId{10159}{\htmlClass{Function Operator}{\text{∣}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{10161}{\htmlClass{Field Operator}{\text{❴}}}}\, \,\href{Ledger.Dijkstra.Specification.Certs.html#6813}{\htmlId{10163}{\htmlClass{Generalizable}{\text{c}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{10165}{\htmlClass{Field Operator}{\text{❵}}}}\, \,\href{Axiom.Set.Map.html#13606}{\htmlId{10167}{\htmlClass{Function Operator}{\text{ᶜ}}}}\, \end{pmatrix}$
GOVCERT-ccreghot :
∙ (c , nothing) ∉ ccKeys
∙ c ∈ cc
────────────────────────────────
$\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Certs.html#6924}{\htmlId{10282}{\htmlClass{Generalizable}{\text{e}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#7061}{\htmlId{10286}{\htmlClass{Generalizable}{\text{pp}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#6946}{\htmlId{10291}{\htmlClass{Generalizable}{\text{vs}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#6610}{\htmlId{10296}{\htmlClass{Generalizable}{\text{wdrls}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#7175}{\htmlId{10304}{\htmlClass{Generalizable}{\text{cc}}}}\, \end{pmatrix}$ ⊢ $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Certs.html#6394}{\htmlId{10313}{\htmlClass{Generalizable}{\text{dReps}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#6466}{\htmlId{10321}{\htmlClass{Generalizable}{\text{ccKeys}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#6681}{\htmlId{10330}{\htmlClass{Generalizable}{\text{deposits}}}}\, \end{pmatrix}$ ⇀⦇ ccreghot c mc ,GOVCERT⦈ $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Certs.html#6394}{\htmlId{10370}{\htmlClass{Generalizable}{\text{dReps}}}}\, \\ \,\href{Class.HasSingleton.html#288}{\htmlId{10378}{\htmlClass{Field Operator}{\text{❴}}}}\, \,\href{Ledger.Dijkstra.Specification.Certs.html#6813}{\htmlId{10380}{\htmlClass{Generalizable}{\text{c}}}}\, , \,\href{Ledger.Dijkstra.Specification.Certs.html#6840}{\htmlId{10384}{\htmlClass{Generalizable}{\text{mc}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{10387}{\htmlClass{Field Operator}{\text{❵}}}}\, \,\href{Axiom.Set.Map.html#7640}{\htmlId{10389}{\htmlClass{Function Operator}{\text{∪ˡ}}}}\, \,\href{Ledger.Dijkstra.Specification.Certs.html#6466}{\htmlId{10392}{\htmlClass{Generalizable}{\text{ccKeys}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#6681}{\htmlId{10401}{\htmlClass{Generalizable}{\text{deposits}}}}\, \end{pmatrix}$
data _⊢_⇀⦇_,CERT⦈_ : CertEnv → CertState → DCert → CertState → Type where
CERT-deleg :
∙ $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Certs.html#7061}{\htmlId{10541}{\htmlClass{Generalizable}{\text{pp}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#2116}{\htmlId{10546}{\htmlClass{Field}{\text{PState.pools}}}}\, \,\href{Ledger.Dijkstra.Specification.Certs.html#7155}{\htmlId{10559}{\htmlClass{Generalizable}{\text{stᵖ}}}}\, \\ \,\href{Class.IsSet.html#916}{\htmlId{10565}{\htmlClass{Function}{\text{dom}}}}\, \,\htmlId{10569}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Dijkstra.Specification.Certs.html#2280}{\htmlId{10570}{\htmlClass{Field}{\text{GState.dreps}}}}\, \,\href{Ledger.Dijkstra.Specification.Certs.html#7135}{\htmlId{10583}{\htmlClass{Generalizable}{\text{stᵍ}}}}\,\,\htmlId{10586}{\htmlClass{Symbol}{\text{)}}}\, \end{pmatrix}$ ⊢ stᵈ ⇀⦇ dCert ,DELEG⦈ stᵈ'
────────────────────────────────
$\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Certs.html#6924}{\htmlId{10665}{\htmlClass{Generalizable}{\text{e}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#7061}{\htmlId{10669}{\htmlClass{Generalizable}{\text{pp}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#6946}{\htmlId{10674}{\htmlClass{Generalizable}{\text{vs}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#6610}{\htmlId{10679}{\htmlClass{Generalizable}{\text{wdrls}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#7175}{\htmlId{10687}{\htmlClass{Generalizable}{\text{cc}}}}\, \end{pmatrix}$ ⊢ $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Certs.html#7115}{\htmlId{10696}{\htmlClass{Generalizable}{\text{stᵈ}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#7155}{\htmlId{10702}{\htmlClass{Generalizable}{\text{stᵖ}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#7135}{\htmlId{10708}{\htmlClass{Generalizable}{\text{stᵍ}}}}\, \end{pmatrix}$ ⇀⦇ dCert ,CERT⦈ $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Certs.html#7119}{\htmlId{10732}{\htmlClass{Generalizable}{\text{stᵈ'}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#7155}{\htmlId{10739}{\htmlClass{Generalizable}{\text{stᵖ}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#7135}{\htmlId{10745}{\htmlClass{Generalizable}{\text{stᵍ}}}}\, \end{pmatrix}$
CERT-pool :
∙ pp ⊢ stᵖ ⇀⦇ dCert ,POOL⦈ stᵖ'
────────────────────────────────
$\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Certs.html#6924}{\htmlId{10849}{\htmlClass{Generalizable}{\text{e}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#7061}{\htmlId{10853}{\htmlClass{Generalizable}{\text{pp}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#6946}{\htmlId{10858}{\htmlClass{Generalizable}{\text{vs}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#6610}{\htmlId{10863}{\htmlClass{Generalizable}{\text{wdrls}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#7175}{\htmlId{10871}{\htmlClass{Generalizable}{\text{cc}}}}\, \end{pmatrix}$ ⊢ $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Certs.html#7115}{\htmlId{10880}{\htmlClass{Generalizable}{\text{stᵈ}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#7155}{\htmlId{10886}{\htmlClass{Generalizable}{\text{stᵖ}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#7135}{\htmlId{10892}{\htmlClass{Generalizable}{\text{stᵍ}}}}\, \end{pmatrix}$ ⇀⦇ dCert ,CERT⦈ $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Certs.html#7115}{\htmlId{10916}{\htmlClass{Generalizable}{\text{stᵈ}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#7159}{\htmlId{10922}{\htmlClass{Generalizable}{\text{stᵖ'}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#7135}{\htmlId{10929}{\htmlClass{Generalizable}{\text{stᵍ}}}}\, \end{pmatrix}$
CERT-gov :
∙ Γ ⊢ stᵍ ⇀⦇ dCert ,GOVCERT⦈ stᵍ'
────────────────────────────────
Γ ⊢ $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Certs.html#7115}{\htmlId{11038}{\htmlClass{Generalizable}{\text{stᵈ}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#7155}{\htmlId{11044}{\htmlClass{Generalizable}{\text{stᵖ}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#7135}{\htmlId{11050}{\htmlClass{Generalizable}{\text{stᵍ}}}}\, \end{pmatrix}$ ⇀⦇ dCert ,CERT⦈ $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Certs.html#7115}{\htmlId{11074}{\htmlClass{Generalizable}{\text{stᵈ}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#7155}{\htmlId{11080}{\htmlClass{Generalizable}{\text{stᵖ}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#7139}{\htmlId{11086}{\htmlClass{Generalizable}{\text{stᵍ'}}}}\, \end{pmatrix}$
open GovVote using (voter)
data _⊢_⇀⦇_,PRE-CERT⦈_ : CertEnv → CertState → ⊤ → CertState → Type where
CERT-pre :
let refresh = mapPartial (isGovVoterDRep ∘ voter) (fromList vs)
refreshedDReps = mapValueRestricted (const (e + pp .drepActivity)) dReps refresh
wdrlCreds = mapˢ stake (dom wdrls)
in
∙ filter isKeyHash wdrlCreds ⊆ dom voteDelegs
∙ mapˢ (map₁ stake) (wdrls ˢ) ⊆ rewards ˢ
────────────────────────────────
$\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Certs.html#6924}{\htmlId{11608}{\htmlClass{Generalizable}{\text{e}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#7061}{\htmlId{11612}{\htmlClass{Generalizable}{\text{pp}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#6946}{\htmlId{11617}{\htmlClass{Generalizable}{\text{vs}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#6610}{\htmlId{11622}{\htmlClass{Generalizable}{\text{wdrls}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#7175}{\htmlId{11630}{\htmlClass{Generalizable}{\text{cc}}}}\, \end{pmatrix}$ ⊢ $\begin{pmatrix} \begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Certs.html#6511}{\htmlId{11641}{\htmlClass{Generalizable}{\text{voteDelegs}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#6435}{\htmlId{11654}{\htmlClass{Generalizable}{\text{stakeDelegs}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#6364}{\htmlId{11668}{\htmlClass{Generalizable}{\text{rewards}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#6681}{\htmlId{11678}{\htmlClass{Generalizable}{\text{deposits}}}}\, \end{pmatrix} \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#7155}{\htmlId{11691}{\htmlClass{Generalizable}{\text{stᵖ}}}}\, \\ \begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Certs.html#6394}{\htmlId{11699}{\htmlClass{Generalizable}{\text{dReps}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#6473}{\htmlId{11707}{\htmlClass{Generalizable}{\text{ccHotKeys}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#6690}{\htmlId{11719}{\htmlClass{Generalizable}{\text{deposits'}}}}\, \end{pmatrix} \end{pmatrix}$ ⇀⦇ _ ,PRE-CERT⦈ $\begin{pmatrix} \begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Certs.html#6511}{\htmlId{11753}{\htmlClass{Generalizable}{\text{voteDelegs}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#6435}{\htmlId{11766}{\htmlClass{Generalizable}{\text{stakeDelegs}}}}\, \\ \,\href{Axiom.Set.Map.html#11988}{\htmlId{11780}{\htmlClass{Function}{\text{constMap}}}}\, \,\href{Ledger.Dijkstra.Specification.Certs.html#11417}{\htmlId{11789}{\htmlClass{Bound}{\text{wdrlCreds}}}}\, \,\htmlId{11799}{\htmlClass{Number}{\text{0}}}\, \,\href{Axiom.Set.Map.html#7640}{\htmlId{11801}{\htmlClass{Function Operator}{\text{∪ˡ}}}}\, \,\href{Ledger.Dijkstra.Specification.Certs.html#6364}{\htmlId{11804}{\htmlClass{Generalizable}{\text{rewards}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#6681}{\htmlId{11814}{\htmlClass{Generalizable}{\text{deposits}}}}\, \end{pmatrix} \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#7155}{\htmlId{11827}{\htmlClass{Generalizable}{\text{stᵖ}}}}\, \\ \begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Certs.html#11327}{\htmlId{11835}{\htmlClass{Bound}{\text{refreshedDReps}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#6473}{\htmlId{11852}{\htmlClass{Generalizable}{\text{ccHotKeys}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#6690}{\htmlId{11864}{\htmlClass{Generalizable}{\text{deposits'}}}}\, \end{pmatrix} \end{pmatrix}$
data _⊢_⇀⦇_,POST-CERT⦈_ : CertEnv → CertState → ⊤ → CertState → Type where
CERT-post :
let activeVDelegs = mapˢ vDelegCredential (dom (DRepsOf stᵍ))
∪ fromList (vDelegNoConfidence ∷ vDelegAbstain ∷ [])
in
$\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Certs.html#6924}{\htmlId{12162}{\htmlClass{Generalizable}{\text{e}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#7061}{\htmlId{12166}{\htmlClass{Generalizable}{\text{pp}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#6946}{\htmlId{12171}{\htmlClass{Generalizable}{\text{vs}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#6610}{\htmlId{12176}{\htmlClass{Generalizable}{\text{wdrls}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#7175}{\htmlId{12184}{\htmlClass{Generalizable}{\text{cc}}}}\, \end{pmatrix}$ ⊢ $\begin{pmatrix} \begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Certs.html#6511}{\htmlId{12195}{\htmlClass{Generalizable}{\text{voteDelegs}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#6435}{\htmlId{12208}{\htmlClass{Generalizable}{\text{stakeDelegs}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#6364}{\htmlId{12222}{\htmlClass{Generalizable}{\text{rewards}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#6681}{\htmlId{12232}{\htmlClass{Generalizable}{\text{deposits}}}}\, \end{pmatrix} \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#7155}{\htmlId{12245}{\htmlClass{Generalizable}{\text{stᵖ}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#7135}{\htmlId{12251}{\htmlClass{Generalizable}{\text{stᵍ}}}}\, \end{pmatrix}$ ⇀⦇ _ ,POST-CERT⦈ $\begin{pmatrix} \begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Certs.html#6511}{\htmlId{12278}{\htmlClass{Generalizable}{\text{voteDelegs}}}}\, \,\href{Axiom.Set.Map.html#17775}{\htmlId{12289}{\htmlClass{Function Operator}{\text{∣\^{}}}}}\, \,\href{Ledger.Dijkstra.Specification.Certs.html#12011}{\htmlId{12292}{\htmlClass{Bound}{\text{activeVDelegs}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#6435}{\htmlId{12308}{\htmlClass{Generalizable}{\text{stakeDelegs}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#6364}{\htmlId{12322}{\htmlClass{Generalizable}{\text{rewards}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#6681}{\htmlId{12332}{\htmlClass{Generalizable}{\text{deposits}}}}\, \end{pmatrix} \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#7155}{\htmlId{12345}{\htmlClass{Generalizable}{\text{stᵖ}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#7135}{\htmlId{12351}{\htmlClass{Generalizable}{\text{stᵍ}}}}\, \end{pmatrix}$
_⊢_⇀⦇_,CERTS⦈_ : CertEnv → CertState → List DCert → CertState → Type
_⊢_⇀⦇_,CERTS⦈_ = RunTraceAfterAndThen _⊢_⇀⦇_,PRE-CERT⦈_ _⊢_⇀⦇_,CERT⦈_ _⊢_⇀⦇_,POST-CERT⦈_