{-# 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#7065}{\htmlId{7821}{\htmlClass{Generalizable}{\text{pp}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#6545}{\htmlId{7826}{\htmlClass{Generalizable}{\text{pools}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#6877}{\htmlId{7834}{\htmlClass{Generalizable}{\text{delegatees}}}}\, \end{pmatrix}$ ⊢ $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Certs.html#6507}{\htmlId{7851}{\htmlClass{Generalizable}{\text{vDelegs}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#6431}{\htmlId{7861}{\htmlClass{Generalizable}{\text{sDelegs}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#6363}{\htmlId{7871}{\htmlClass{Generalizable}{\text{rwds}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#6685}{\htmlId{7878}{\htmlClass{Generalizable}{\text{deposits}}}}\, \end{pmatrix}$ ⇀⦇ delegate c mvd mkh d ,DELEG⦈ $\begin{pmatrix} \,\href{Axiom.Set.Map.html#9262}{\htmlId{7923}{\htmlClass{Function}{\text{insertIfJust}}}}\, \,\href{Ledger.Dijkstra.Specification.Certs.html#6817}{\htmlId{7936}{\htmlClass{Generalizable}{\text{c}}}}\, \,\href{Ledger.Dijkstra.Specification.Certs.html#7089}{\htmlId{7938}{\htmlClass{Generalizable}{\text{mvd}}}}\, \,\href{Ledger.Dijkstra.Specification.Certs.html#6507}{\htmlId{7942}{\htmlClass{Generalizable}{\text{vDelegs}}}}\, \\ \,\href{Axiom.Set.Map.html#9262}{\htmlId{7952}{\htmlClass{Function}{\text{insertIfJust}}}}\, \,\href{Ledger.Dijkstra.Specification.Certs.html#6817}{\htmlId{7965}{\htmlClass{Generalizable}{\text{c}}}}\, \,\href{Ledger.Dijkstra.Specification.Certs.html#7003}{\htmlId{7967}{\htmlClass{Generalizable}{\text{mkh}}}}\, \,\href{Ledger.Dijkstra.Specification.Certs.html#6431}{\htmlId{7971}{\htmlClass{Generalizable}{\text{sDelegs}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#6363}{\htmlId{7981}{\htmlClass{Generalizable}{\text{rwds}}}}\, \,\href{Axiom.Set.Map.html#7640}{\htmlId{7986}{\htmlClass{Function Operator}{\text{∪ˡ}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{7989}{\htmlClass{Field Operator}{\text{❴}}}}\, \,\href{Ledger.Dijkstra.Specification.Certs.html#6817}{\htmlId{7991}{\htmlClass{Generalizable}{\text{c}}}}\, , \,\htmlId{7995}{\htmlClass{Number}{\text{0}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{7997}{\htmlClass{Field Operator}{\text{❵}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#6685}{\htmlId{8001}{\htmlClass{Generalizable}{\text{deposits}}}}\, \,\href{Axiom.Set.Map.Dec.html#2149}{\htmlId{8010}{\htmlClass{Function Operator}{\text{∪⁺}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{8013}{\htmlClass{Field Operator}{\text{❴}}}}\, \,\href{Ledger.Dijkstra.Specification.Certs.html#6817}{\htmlId{8015}{\htmlClass{Generalizable}{\text{c}}}}\, , \,\href{Ledger.Dijkstra.Specification.Certs.html#6769}{\htmlId{8019}{\htmlClass{Generalizable}{\text{d}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{8021}{\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#7065}{\htmlId{8168}{\htmlClass{Generalizable}{\text{pp}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#6545}{\htmlId{8173}{\htmlClass{Generalizable}{\text{pools}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#6877}{\htmlId{8181}{\htmlClass{Generalizable}{\text{delegatees}}}}\, \end{pmatrix}$ ⊢ $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Certs.html#6507}{\htmlId{8198}{\htmlClass{Generalizable}{\text{vDelegs}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#6431}{\htmlId{8208}{\htmlClass{Generalizable}{\text{sDelegs}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#6363}{\htmlId{8218}{\htmlClass{Generalizable}{\text{rwds}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#6685}{\htmlId{8225}{\htmlClass{Generalizable}{\text{deposits}}}}\, \end{pmatrix}$ ⇀⦇ dereg c md ,DELEG⦈ $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Certs.html#6507}{\htmlId{8260}{\htmlClass{Generalizable}{\text{vDelegs}}}}\, \,\href{Axiom.Set.Map.html#13606}{\htmlId{8268}{\htmlClass{Function Operator}{\text{∣}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{8270}{\htmlClass{Field Operator}{\text{❴}}}}\, \,\href{Ledger.Dijkstra.Specification.Certs.html#6817}{\htmlId{8272}{\htmlClass{Generalizable}{\text{c}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{8274}{\htmlClass{Field Operator}{\text{❵}}}}\, \,\href{Axiom.Set.Map.html#13606}{\htmlId{8276}{\htmlClass{Function Operator}{\text{ᶜ}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#6431}{\htmlId{8280}{\htmlClass{Generalizable}{\text{sDelegs}}}}\, \,\href{Axiom.Set.Map.html#13606}{\htmlId{8288}{\htmlClass{Function Operator}{\text{∣}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{8290}{\htmlClass{Field Operator}{\text{❴}}}}\, \,\href{Ledger.Dijkstra.Specification.Certs.html#6817}{\htmlId{8292}{\htmlClass{Generalizable}{\text{c}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{8294}{\htmlClass{Field Operator}{\text{❵}}}}\, \,\href{Axiom.Set.Map.html#13606}{\htmlId{8296}{\htmlClass{Function Operator}{\text{ᶜ}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#6363}{\htmlId{8300}{\htmlClass{Generalizable}{\text{rwds}}}}\, \,\href{Axiom.Set.Map.html#13606}{\htmlId{8305}{\htmlClass{Function Operator}{\text{∣}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{8307}{\htmlClass{Field Operator}{\text{❴}}}}\, \,\href{Ledger.Dijkstra.Specification.Certs.html#6817}{\htmlId{8309}{\htmlClass{Generalizable}{\text{c}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{8311}{\htmlClass{Field Operator}{\text{❵}}}}\, \,\href{Axiom.Set.Map.html#13606}{\htmlId{8313}{\htmlClass{Function Operator}{\text{ᶜ}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#6685}{\htmlId{8317}{\htmlClass{Generalizable}{\text{deposits}}}}\, \,\href{Axiom.Set.Map.html#13606}{\htmlId{8326}{\htmlClass{Function Operator}{\text{∣}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{8328}{\htmlClass{Field Operator}{\text{❴}}}}\, \,\href{Ledger.Dijkstra.Specification.Certs.html#6817}{\htmlId{8330}{\htmlClass{Generalizable}{\text{c}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{8332}{\htmlClass{Field Operator}{\text{❵}}}}\, \,\href{Axiom.Set.Map.html#13606}{\htmlId{8334}{\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#6545}{\htmlId{8656}{\htmlClass{Generalizable}{\text{pools}}}}\,
\\ \,\href{Ledger.Dijkstra.Specification.Certs.html#6551}{\htmlId{8673}{\htmlClass{Generalizable}{\text{fPools}}}}\,
\\ \,\href{Ledger.Dijkstra.Specification.Certs.html#6578}{\htmlId{8691}{\htmlClass{Generalizable}{\text{retiring}}}}\,
\\ \,\href{Ledger.Dijkstra.Specification.Certs.html#6685}{\htmlId{8711}{\htmlClass{Generalizable}{\text{deposits}}}}\,
\end{pmatrix}$ ⇀⦇ regpool kh poolParams ,POOL⦈ $\begin{pmatrix}
\,\href{Ledger.Dijkstra.Specification.Certs.html#6545}{\htmlId{8776}{\htmlClass{Generalizable}{\text{pools}}}}\, \,\href{Axiom.Set.Map.html#7640}{\htmlId{8782}{\htmlClass{Function Operator}{\text{∪ˡ}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{8785}{\htmlClass{Field Operator}{\text{❴}}}}\, \,\href{Ledger.Dijkstra.Specification.Certs.html#6979}{\htmlId{8787}{\htmlClass{Generalizable}{\text{kh}}}}\, , \,\href{Ledger.Dijkstra.Specification.Certs.html#7033}{\htmlId{8792}{\htmlClass{Generalizable}{\text{poolParams}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{8803}{\htmlClass{Field Operator}{\text{❵}}}}\,
\\ \,\href{Ledger.Dijkstra.Specification.Certs.html#6551}{\htmlId{8816}{\htmlClass{Generalizable}{\text{fPools}}}}\,
\\ \,\href{Ledger.Dijkstra.Specification.Certs.html#6578}{\htmlId{8834}{\htmlClass{Generalizable}{\text{retiring}}}}\,
\\ \,\href{Ledger.Dijkstra.Specification.Certs.html#6685}{\htmlId{8854}{\htmlClass{Generalizable}{\text{deposits}}}}\, \,\href{Axiom.Set.Map.html#7640}{\htmlId{8863}{\htmlClass{Function Operator}{\text{∪ˡ}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{8866}{\htmlClass{Field Operator}{\text{❴}}}}\, \,\href{Ledger.Dijkstra.Specification.Certs.html#6979}{\htmlId{8868}{\htmlClass{Generalizable}{\text{kh}}}}\, , \,\href{Ledger.Dijkstra.Specification.Certs.html#7065}{\htmlId{8873}{\htmlClass{Generalizable}{\text{pp}}}}\, \,\htmlId{8876}{\htmlClass{Symbol}{\text{.}}}\,\,\href{Ledger.Dijkstra.Specification.PParams.html#2416}{\htmlId{8877}{\htmlClass{Field}{\text{poolDeposit}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{8889}{\htmlClass{Field Operator}{\text{❵}}}}\,
\end{pmatrix}$
POOL-rereg :
∙ Is-just (isPoolRegistered pools kh)
────────────────────────────────
pp ⊢ $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Certs.html#6545}{\htmlId{9008}{\htmlClass{Generalizable}{\text{pools}}}}\,
\\ \,\href{Ledger.Dijkstra.Specification.Certs.html#6551}{\htmlId{9025}{\htmlClass{Generalizable}{\text{fPools}}}}\,
\\ \,\href{Ledger.Dijkstra.Specification.Certs.html#6578}{\htmlId{9043}{\htmlClass{Generalizable}{\text{retiring}}}}\,
\\ \,\href{Ledger.Dijkstra.Specification.Certs.html#6685}{\htmlId{9063}{\htmlClass{Generalizable}{\text{deposits}}}}\,
\end{pmatrix}$ ⇀⦇ regpool kh poolParams ,POOL⦈ $\begin{pmatrix}
\,\href{Ledger.Dijkstra.Specification.Certs.html#6545}{\htmlId{9128}{\htmlClass{Generalizable}{\text{pools}}}}\,
\\ \,\href{Class.HasSingleton.html#288}{\htmlId{9145}{\htmlClass{Field Operator}{\text{❴}}}}\, \,\href{Ledger.Dijkstra.Specification.Certs.html#6979}{\htmlId{9147}{\htmlClass{Generalizable}{\text{kh}}}}\, , \,\href{Ledger.Dijkstra.Specification.Certs.html#7033}{\htmlId{9152}{\htmlClass{Generalizable}{\text{poolParams}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{9163}{\htmlClass{Field Operator}{\text{❵}}}}\, \,\href{Axiom.Set.Map.html#7640}{\htmlId{9165}{\htmlClass{Function Operator}{\text{∪ˡ}}}}\, \,\href{Ledger.Dijkstra.Specification.Certs.html#6551}{\htmlId{9168}{\htmlClass{Generalizable}{\text{fPools}}}}\,
\\ \,\href{Ledger.Dijkstra.Specification.Certs.html#6578}{\htmlId{9186}{\htmlClass{Generalizable}{\text{retiring}}}}\, \,\href{Axiom.Set.Map.html#13606}{\htmlId{9195}{\htmlClass{Function Operator}{\text{∣}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{9197}{\htmlClass{Field Operator}{\text{❴}}}}\, \,\href{Ledger.Dijkstra.Specification.Certs.html#6979}{\htmlId{9199}{\htmlClass{Generalizable}{\text{kh}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{9202}{\htmlClass{Field Operator}{\text{❵}}}}\, \,\href{Axiom.Set.Map.html#13606}{\htmlId{9204}{\htmlClass{Function Operator}{\text{ᶜ}}}}\,
\\ \,\href{Ledger.Dijkstra.Specification.Certs.html#6685}{\htmlId{9217}{\htmlClass{Generalizable}{\text{deposits}}}}\,
\end{pmatrix}$
POOL-retirepool :
────────────────────────────────
pp ⊢ $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Certs.html#6545}{\htmlId{9306}{\htmlClass{Generalizable}{\text{pools}}}}\,
\\ \,\href{Ledger.Dijkstra.Specification.Certs.html#6551}{\htmlId{9323}{\htmlClass{Generalizable}{\text{fPools}}}}\,
\\ \,\href{Ledger.Dijkstra.Specification.Certs.html#6578}{\htmlId{9341}{\htmlClass{Generalizable}{\text{retiring}}}}\,
\\ \,\href{Ledger.Dijkstra.Specification.Certs.html#6685}{\htmlId{9361}{\htmlClass{Generalizable}{\text{deposits}}}}\,
\end{pmatrix}$ ⇀⦇ retirepool kh e ,POOL⦈ $\begin{pmatrix}
\,\href{Ledger.Dijkstra.Specification.Certs.html#6545}{\htmlId{9420}{\htmlClass{Generalizable}{\text{pools}}}}\,
\\ \,\href{Ledger.Dijkstra.Specification.Certs.html#6551}{\htmlId{9437}{\htmlClass{Generalizable}{\text{fPools}}}}\,
\\ \,\href{Class.HasSingleton.html#288}{\htmlId{9455}{\htmlClass{Field Operator}{\text{❴}}}}\, \,\href{Ledger.Dijkstra.Specification.Certs.html#6979}{\htmlId{9457}{\htmlClass{Generalizable}{\text{kh}}}}\, , \,\href{Ledger.Dijkstra.Specification.Certs.html#6928}{\htmlId{9462}{\htmlClass{Generalizable}{\text{e}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{9464}{\htmlClass{Field Operator}{\text{❵}}}}\, \,\href{Axiom.Set.Map.html#7640}{\htmlId{9466}{\htmlClass{Function Operator}{\text{∪ˡ}}}}\, \,\href{Ledger.Dijkstra.Specification.Certs.html#6578}{\htmlId{9469}{\htmlClass{Generalizable}{\text{retiring}}}}\,
\\ \,\href{Ledger.Dijkstra.Specification.Certs.html#6685}{\htmlId{9489}{\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#6928}{\htmlId{9762}{\htmlClass{Generalizable}{\text{e}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#7065}{\htmlId{9766}{\htmlClass{Generalizable}{\text{pp}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#6950}{\htmlId{9771}{\htmlClass{Generalizable}{\text{vs}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#6614}{\htmlId{9776}{\htmlClass{Generalizable}{\text{wdrls}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#7179}{\htmlId{9784}{\htmlClass{Generalizable}{\text{cc}}}}\, \end{pmatrix}$ ⊢ $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Certs.html#6398}{\htmlId{9793}{\htmlClass{Generalizable}{\text{dReps}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#6470}{\htmlId{9801}{\htmlClass{Generalizable}{\text{ccKeys}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#6685}{\htmlId{9810}{\htmlClass{Generalizable}{\text{deposits}}}}\, \end{pmatrix}$ ⇀⦇ regdrep c d an ,GOVCERT⦈ $\begin{pmatrix} \,\href{Class.HasSingleton.html#288}{\htmlId{9851}{\htmlClass{Field Operator}{\text{❴}}}}\, \,\href{Ledger.Dijkstra.Specification.Certs.html#6817}{\htmlId{9853}{\htmlClass{Generalizable}{\text{c}}}}\, , \,\href{Ledger.Dijkstra.Specification.Certs.html#6928}{\htmlId{9857}{\htmlClass{Generalizable}{\text{e}}}}\, \,\href{Class.HasAdd.Core.html#162}{\htmlId{9859}{\htmlClass{Field Operator}{\text{+}}}}\, \,\href{Ledger.Dijkstra.Specification.Certs.html#7065}{\htmlId{9861}{\htmlClass{Generalizable}{\text{pp}}}}\, \,\htmlId{9864}{\htmlClass{Symbol}{\text{.}}}\,\,\href{Ledger.Dijkstra.Specification.PParams.html#3546}{\htmlId{9865}{\htmlClass{Field}{\text{drepActivity}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{9878}{\htmlClass{Field Operator}{\text{❵}}}}\, \,\href{Axiom.Set.Map.html#7640}{\htmlId{9880}{\htmlClass{Function Operator}{\text{∪ˡ}}}}\, \,\href{Ledger.Dijkstra.Specification.Certs.html#6398}{\htmlId{9883}{\htmlClass{Generalizable}{\text{dReps}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#6470}{\htmlId{9891}{\htmlClass{Generalizable}{\text{ccKeys}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#6685}{\htmlId{9900}{\htmlClass{Generalizable}{\text{deposits}}}}\, \,\href{Axiom.Set.Map.Dec.html#2149}{\htmlId{9909}{\htmlClass{Function Operator}{\text{∪⁺}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{9912}{\htmlClass{Field Operator}{\text{❴}}}}\, \,\href{Ledger.Dijkstra.Specification.Certs.html#6817}{\htmlId{9914}{\htmlClass{Generalizable}{\text{c}}}}\, , \,\href{Ledger.Dijkstra.Specification.Certs.html#6769}{\htmlId{9918}{\htmlClass{Generalizable}{\text{d}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{9920}{\htmlClass{Field Operator}{\text{❵}}}}\, \end{pmatrix}$
GOVCERT-deregdrep :
∙ c ∈ dom dReps
∙ (c , d) ∈ deposits
────────────────────────────────
$\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Certs.html#6928}{\htmlId{10039}{\htmlClass{Generalizable}{\text{e}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#7065}{\htmlId{10043}{\htmlClass{Generalizable}{\text{pp}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#6950}{\htmlId{10048}{\htmlClass{Generalizable}{\text{vs}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#6614}{\htmlId{10053}{\htmlClass{Generalizable}{\text{wdrls}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#7179}{\htmlId{10061}{\htmlClass{Generalizable}{\text{cc}}}}\, \end{pmatrix}$ ⊢ $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Certs.html#6398}{\htmlId{10070}{\htmlClass{Generalizable}{\text{dReps}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#6470}{\htmlId{10078}{\htmlClass{Generalizable}{\text{ccKeys}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#6685}{\htmlId{10087}{\htmlClass{Generalizable}{\text{deposits}}}}\, \end{pmatrix}$ ⇀⦇ deregdrep c d ,GOVCERT⦈ $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Certs.html#6398}{\htmlId{10127}{\htmlClass{Generalizable}{\text{dReps}}}}\, \,\href{Axiom.Set.Map.html#13606}{\htmlId{10133}{\htmlClass{Function Operator}{\text{∣}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{10135}{\htmlClass{Field Operator}{\text{❴}}}}\, \,\href{Ledger.Dijkstra.Specification.Certs.html#6817}{\htmlId{10137}{\htmlClass{Generalizable}{\text{c}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{10139}{\htmlClass{Field Operator}{\text{❵}}}}\, \,\href{Axiom.Set.Map.html#13606}{\htmlId{10141}{\htmlClass{Function Operator}{\text{ᶜ}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#6470}{\htmlId{10145}{\htmlClass{Generalizable}{\text{ccKeys}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#6685}{\htmlId{10154}{\htmlClass{Generalizable}{\text{deposits}}}}\, \,\href{Axiom.Set.Map.html#13606}{\htmlId{10163}{\htmlClass{Function Operator}{\text{∣}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{10165}{\htmlClass{Field Operator}{\text{❴}}}}\, \,\href{Ledger.Dijkstra.Specification.Certs.html#6817}{\htmlId{10167}{\htmlClass{Generalizable}{\text{c}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{10169}{\htmlClass{Field Operator}{\text{❵}}}}\, \,\href{Axiom.Set.Map.html#13606}{\htmlId{10171}{\htmlClass{Function Operator}{\text{ᶜ}}}}\, \end{pmatrix}$
GOVCERT-ccreghot :
∙ (c , nothing) ∉ ccKeys
∙ c ∈ cc
────────────────────────────────
$\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Certs.html#6928}{\htmlId{10286}{\htmlClass{Generalizable}{\text{e}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#7065}{\htmlId{10290}{\htmlClass{Generalizable}{\text{pp}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#6950}{\htmlId{10295}{\htmlClass{Generalizable}{\text{vs}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#6614}{\htmlId{10300}{\htmlClass{Generalizable}{\text{wdrls}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#7179}{\htmlId{10308}{\htmlClass{Generalizable}{\text{cc}}}}\, \end{pmatrix}$ ⊢ $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Certs.html#6398}{\htmlId{10317}{\htmlClass{Generalizable}{\text{dReps}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#6470}{\htmlId{10325}{\htmlClass{Generalizable}{\text{ccKeys}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#6685}{\htmlId{10334}{\htmlClass{Generalizable}{\text{deposits}}}}\, \end{pmatrix}$ ⇀⦇ ccreghot c mc ,GOVCERT⦈ $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Certs.html#6398}{\htmlId{10374}{\htmlClass{Generalizable}{\text{dReps}}}}\, \\ \,\href{Class.HasSingleton.html#288}{\htmlId{10382}{\htmlClass{Field Operator}{\text{❴}}}}\, \,\href{Ledger.Dijkstra.Specification.Certs.html#6817}{\htmlId{10384}{\htmlClass{Generalizable}{\text{c}}}}\, , \,\href{Ledger.Dijkstra.Specification.Certs.html#6844}{\htmlId{10388}{\htmlClass{Generalizable}{\text{mc}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{10391}{\htmlClass{Field Operator}{\text{❵}}}}\, \,\href{Axiom.Set.Map.html#7640}{\htmlId{10393}{\htmlClass{Function Operator}{\text{∪ˡ}}}}\, \,\href{Ledger.Dijkstra.Specification.Certs.html#6470}{\htmlId{10396}{\htmlClass{Generalizable}{\text{ccKeys}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#6685}{\htmlId{10405}{\htmlClass{Generalizable}{\text{deposits}}}}\, \end{pmatrix}$
data _⊢_⇀⦇_,CERT⦈_ : CertEnv → CertState → DCert → CertState → Type where
CERT-deleg :
∙ $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Certs.html#7065}{\htmlId{10545}{\htmlClass{Generalizable}{\text{pp}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#2118}{\htmlId{10550}{\htmlClass{Field}{\text{PState.pools}}}}\, \,\href{Ledger.Dijkstra.Specification.Certs.html#7159}{\htmlId{10563}{\htmlClass{Generalizable}{\text{stᵖ}}}}\, \\ \,\href{Class.IsSet.html#916}{\htmlId{10569}{\htmlClass{Function}{\text{dom}}}}\, \,\htmlId{10573}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Dijkstra.Specification.Certs.html#2284}{\htmlId{10574}{\htmlClass{Field}{\text{GState.dreps}}}}\, \,\href{Ledger.Dijkstra.Specification.Certs.html#7139}{\htmlId{10587}{\htmlClass{Generalizable}{\text{stᵍ}}}}\,\,\htmlId{10590}{\htmlClass{Symbol}{\text{)}}}\, \end{pmatrix}$ ⊢ stᵈ ⇀⦇ dCert ,DELEG⦈ stᵈ'
────────────────────────────────
$\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Certs.html#6928}{\htmlId{10669}{\htmlClass{Generalizable}{\text{e}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#7065}{\htmlId{10673}{\htmlClass{Generalizable}{\text{pp}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#6950}{\htmlId{10678}{\htmlClass{Generalizable}{\text{vs}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#6614}{\htmlId{10683}{\htmlClass{Generalizable}{\text{wdrls}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#7179}{\htmlId{10691}{\htmlClass{Generalizable}{\text{cc}}}}\, \end{pmatrix}$ ⊢ $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Certs.html#7119}{\htmlId{10700}{\htmlClass{Generalizable}{\text{stᵈ}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#7159}{\htmlId{10706}{\htmlClass{Generalizable}{\text{stᵖ}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#7139}{\htmlId{10712}{\htmlClass{Generalizable}{\text{stᵍ}}}}\, \end{pmatrix}$ ⇀⦇ dCert ,CERT⦈ $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Certs.html#7123}{\htmlId{10736}{\htmlClass{Generalizable}{\text{stᵈ'}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#7159}{\htmlId{10743}{\htmlClass{Generalizable}{\text{stᵖ}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#7139}{\htmlId{10749}{\htmlClass{Generalizable}{\text{stᵍ}}}}\, \end{pmatrix}$
CERT-pool :
∙ pp ⊢ stᵖ ⇀⦇ dCert ,POOL⦈ stᵖ'
────────────────────────────────
$\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Certs.html#6928}{\htmlId{10853}{\htmlClass{Generalizable}{\text{e}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#7065}{\htmlId{10857}{\htmlClass{Generalizable}{\text{pp}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#6950}{\htmlId{10862}{\htmlClass{Generalizable}{\text{vs}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#6614}{\htmlId{10867}{\htmlClass{Generalizable}{\text{wdrls}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#7179}{\htmlId{10875}{\htmlClass{Generalizable}{\text{cc}}}}\, \end{pmatrix}$ ⊢ $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Certs.html#7119}{\htmlId{10884}{\htmlClass{Generalizable}{\text{stᵈ}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#7159}{\htmlId{10890}{\htmlClass{Generalizable}{\text{stᵖ}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#7139}{\htmlId{10896}{\htmlClass{Generalizable}{\text{stᵍ}}}}\, \end{pmatrix}$ ⇀⦇ dCert ,CERT⦈ $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Certs.html#7119}{\htmlId{10920}{\htmlClass{Generalizable}{\text{stᵈ}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#7163}{\htmlId{10926}{\htmlClass{Generalizable}{\text{stᵖ'}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#7139}{\htmlId{10933}{\htmlClass{Generalizable}{\text{stᵍ}}}}\, \end{pmatrix}$
CERT-gov :
∙ Γ ⊢ stᵍ ⇀⦇ dCert ,GOVCERT⦈ stᵍ'
────────────────────────────────
Γ ⊢ $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Certs.html#7119}{\htmlId{11042}{\htmlClass{Generalizable}{\text{stᵈ}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#7159}{\htmlId{11048}{\htmlClass{Generalizable}{\text{stᵖ}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#7139}{\htmlId{11054}{\htmlClass{Generalizable}{\text{stᵍ}}}}\, \end{pmatrix}$ ⇀⦇ dCert ,CERT⦈ $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Certs.html#7119}{\htmlId{11078}{\htmlClass{Generalizable}{\text{stᵈ}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#7159}{\htmlId{11084}{\htmlClass{Generalizable}{\text{stᵖ}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#7143}{\htmlId{11090}{\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#6928}{\htmlId{11612}{\htmlClass{Generalizable}{\text{e}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#7065}{\htmlId{11616}{\htmlClass{Generalizable}{\text{pp}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#6950}{\htmlId{11621}{\htmlClass{Generalizable}{\text{vs}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#6614}{\htmlId{11626}{\htmlClass{Generalizable}{\text{wdrls}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#7179}{\htmlId{11634}{\htmlClass{Generalizable}{\text{cc}}}}\, \end{pmatrix}$ ⊢ $\begin{pmatrix} \begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Certs.html#6515}{\htmlId{11645}{\htmlClass{Generalizable}{\text{voteDelegs}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#6439}{\htmlId{11658}{\htmlClass{Generalizable}{\text{stakeDelegs}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#6368}{\htmlId{11672}{\htmlClass{Generalizable}{\text{rewards}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#6685}{\htmlId{11682}{\htmlClass{Generalizable}{\text{deposits}}}}\, \end{pmatrix} \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#7159}{\htmlId{11695}{\htmlClass{Generalizable}{\text{stᵖ}}}}\, \\ \begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Certs.html#6398}{\htmlId{11703}{\htmlClass{Generalizable}{\text{dReps}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#6477}{\htmlId{11711}{\htmlClass{Generalizable}{\text{ccHotKeys}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#6694}{\htmlId{11723}{\htmlClass{Generalizable}{\text{deposits'}}}}\, \end{pmatrix} \end{pmatrix}$ ⇀⦇ _ ,PRE-CERT⦈ $\begin{pmatrix} \begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Certs.html#6515}{\htmlId{11757}{\htmlClass{Generalizable}{\text{voteDelegs}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#6439}{\htmlId{11770}{\htmlClass{Generalizable}{\text{stakeDelegs}}}}\, \\ \,\href{Axiom.Set.Map.html#11988}{\htmlId{11784}{\htmlClass{Function}{\text{constMap}}}}\, \,\href{Ledger.Dijkstra.Specification.Certs.html#11421}{\htmlId{11793}{\htmlClass{Bound}{\text{wdrlCreds}}}}\, \,\htmlId{11803}{\htmlClass{Number}{\text{0}}}\, \,\href{Axiom.Set.Map.html#7640}{\htmlId{11805}{\htmlClass{Function Operator}{\text{∪ˡ}}}}\, \,\href{Ledger.Dijkstra.Specification.Certs.html#6368}{\htmlId{11808}{\htmlClass{Generalizable}{\text{rewards}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#6685}{\htmlId{11818}{\htmlClass{Generalizable}{\text{deposits}}}}\, \end{pmatrix} \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#7159}{\htmlId{11831}{\htmlClass{Generalizable}{\text{stᵖ}}}}\, \\ \begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Certs.html#11331}{\htmlId{11839}{\htmlClass{Bound}{\text{refreshedDReps}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#6477}{\htmlId{11856}{\htmlClass{Generalizable}{\text{ccHotKeys}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#6694}{\htmlId{11868}{\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#6928}{\htmlId{12166}{\htmlClass{Generalizable}{\text{e}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#7065}{\htmlId{12170}{\htmlClass{Generalizable}{\text{pp}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#6950}{\htmlId{12175}{\htmlClass{Generalizable}{\text{vs}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#6614}{\htmlId{12180}{\htmlClass{Generalizable}{\text{wdrls}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#7179}{\htmlId{12188}{\htmlClass{Generalizable}{\text{cc}}}}\, \end{pmatrix}$ ⊢ $\begin{pmatrix} \begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Certs.html#6515}{\htmlId{12199}{\htmlClass{Generalizable}{\text{voteDelegs}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#6439}{\htmlId{12212}{\htmlClass{Generalizable}{\text{stakeDelegs}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#6368}{\htmlId{12226}{\htmlClass{Generalizable}{\text{rewards}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#6685}{\htmlId{12236}{\htmlClass{Generalizable}{\text{deposits}}}}\, \end{pmatrix} \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#7159}{\htmlId{12249}{\htmlClass{Generalizable}{\text{stᵖ}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#7139}{\htmlId{12255}{\htmlClass{Generalizable}{\text{stᵍ}}}}\, \end{pmatrix}$ ⇀⦇ _ ,POST-CERT⦈ $\begin{pmatrix} \begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Certs.html#6515}{\htmlId{12282}{\htmlClass{Generalizable}{\text{voteDelegs}}}}\, \,\href{Axiom.Set.Map.html#17775}{\htmlId{12293}{\htmlClass{Function Operator}{\text{∣\^{}}}}}\, \,\href{Ledger.Dijkstra.Specification.Certs.html#12015}{\htmlId{12296}{\htmlClass{Bound}{\text{activeVDelegs}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#6439}{\htmlId{12312}{\htmlClass{Generalizable}{\text{stakeDelegs}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#6368}{\htmlId{12326}{\htmlClass{Generalizable}{\text{rewards}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#6685}{\htmlId{12336}{\htmlClass{Generalizable}{\text{deposits}}}}\, \end{pmatrix} \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#7159}{\htmlId{12349}{\htmlClass{Generalizable}{\text{stᵖ}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#7139}{\htmlId{12355}{\htmlClass{Generalizable}{\text{stᵍ}}}}\, \end{pmatrix}$
_⊢_⇀⦇_,CERTS⦈_ : CertEnv → CertState → List DCert → CertState → Type
_⊢_⇀⦇_,CERTS⦈_ = RunTraceAfterAndThen _⊢_⇀⦇_,PRE-CERT⦈_ _⊢_⇀⦇_,CERT⦈_ _⊢_⇀⦇_,POST-CERT⦈_