{-# OPTIONS --safe #-}
open import Ledger.Prelude renaming (filterˢ to filter)
open import Ledger.Conway.Specification.Gov.Base
open import Ledger.Prelude.Numeric.UnitInterval
module Ledger.Conway.Specification.Certs (gs : _) (open GovStructure gs) where
open import Ledger.Conway.Specification.Gov.Actions gs
open RwdAddr
open PParams
record StakePoolParams : Type where
field
owners : ℙ KeyHash
cost : Coin
margin : UnitInterval
pledge : Coin
rewardAccount : Credential
data DepositPurpose : Type where
CredentialDeposit : Credential → DepositPurpose
PoolDeposit : KeyHash → DepositPurpose
DRepDeposit : Credential → DepositPurpose
GovActionDeposit : GovActionID → DepositPurpose
Deposits : Type
Deposits = DepositPurpose ⇀ Coin
record HasDeposits {a} (A : Type a) : Type a where
field DepositsOf : A → Deposits
open HasDeposits ⦃...⦄ public
instance
unquoteDecl DecEq-DepositPurpose = derive-DecEq
((quote DepositPurpose , DecEq-DepositPurpose) ∷ [])
CCHotKeys DReps PoolEnv Pools Retiring Rewards Stake StakeDelegs : Type
CCHotKeys = Credential ⇀ Maybe Credential
DReps = Credential ⇀ Epoch
PoolEnv = PParams
Pools = KeyHash ⇀ StakePoolParams
Retiring = KeyHash ⇀ Epoch
Rewards = Credential ⇀ Coin
Stake = Credential ⇀ Coin
StakeDelegs = Credential ⇀ KeyHash
record HasCCHotKeys {a} (A : Type a) : Type a where
field CCHotKeysOf : A → CCHotKeys
record HasDReps {a} (A : Type a) : Type a where
field DRepsOf : A → DReps
record HasPools {a} (A : Type a) : Type a where
field PoolsOf : A → Pools
record HasRetiring {a} (A : Type a) : Type a where
field RetiringOf : A → Retiring
record HasRewards {a} (A : Type a) : Type a where
field RewardsOf : A → Rewards
record HasStake {a} (A : Type a) : Type a where
field StakeOf : A -> Stake
record HasStakeDelegs {a} (A : Type a) : Type a where
field StakeDelegsOf : A -> StakeDelegs
open HasCCHotKeys ⦃...⦄ public
open HasDReps ⦃...⦄ public
open HasPools ⦃...⦄ public
open HasRetiring ⦃...⦄ public
open HasRewards ⦃...⦄ public
open HasStake ⦃...⦄ public
open HasStakeDelegs ⦃...⦄ public
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
reg : Credential → Coin → 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
cwitness (reg _ zero) = nothing
cwitness (reg c (suc _)) = 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
record PState : Type where
field
pools : Pools
retiring : KeyHash ⇀ Epoch
record GState : Type where
constructor ⟦_,_⟧ᵛ
field
dreps : DReps
ccHotKeys : Credential ⇀ Maybe Credential
record CertState : Type where
constructor ⟦_,_,_⟧ᶜˢ
field
dState : DState
pState : PState
gState : GState
record DelegEnv : Type where
field
pparams : PParams
pools : Pools
delegatees : ℙ Credential
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
HasPools-PState : HasPools PState
HasPools-PState .PoolsOf = PState.pools
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
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
rewardsBalance : DState → Coin
rewardsBalance ds = ∑[ x ← RewardsOf ds ] x
instance
HasCoin-CertState : HasCoin CertState
HasCoin-CertState .getCoin = rewardsBalance ∘ 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 : Pools
retiring : Retiring
wdrls : Withdrawals
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
data _⊢_⇀⦇_,DELEG⦈_ : DelegEnv → DState → DCert → DState → Type
data _⊢_⇀⦇_,POOL⦈_ : PoolEnv → PState → DCert → PState → Type
data _⊢_⇀⦇_,GOVCERT⦈_ : CertEnv → GState → DCert → GState → Type
data _⊢_⇀⦇_,CERT⦈_ : CertEnv → CertState → DCert → CertState → Type
data _⊢_⇀⦇_,CERTBASE⦈_ : CertEnv → CertState → ⊤ → CertState → Type
_⊢_⇀⦇_,CERTS⦈_ : CertEnv → CertState → List DCert → CertState → Type
_⊢_⇀⦇_,CERTS⦈_ = ReflexiveTransitiveClosureᵇ' {_⊢_⇀⟦_⟧ᵇ_ = _⊢_⇀⦇_,CERTBASE⦈_} {_⊢_⇀⦇_,CERT⦈_}
data _⊢_⇀⦇_,DELEG⦈_
where
DELEG-delegate :
let Γ = $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Certs.html#7813}{\htmlId{8620}{\htmlClass{Generalizable}{\text{pp}}}}\, \\ \,\href{Ledger.Conway.Specification.Certs.html#7361}{\htmlId{8625}{\htmlClass{Generalizable}{\text{pools}}}}\, \\ \,\href{Ledger.Conway.Specification.Certs.html#7625}{\htmlId{8633}{\htmlClass{Generalizable}{\text{delegatees}}}}\, \end{pmatrix}$
in
∙ (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.Conway.Specification.Certs.html#7323}{\htmlId{8964}{\htmlClass{Generalizable}{\text{vDelegs}}}}\, \\ \,\href{Ledger.Conway.Specification.Certs.html#7247}{\htmlId{8974}{\htmlClass{Generalizable}{\text{sDelegs}}}}\, \\ \,\href{Ledger.Conway.Specification.Certs.html#7179}{\htmlId{8984}{\htmlClass{Generalizable}{\text{rwds}}}}\, \end{pmatrix}$ ⇀⦇ delegate c mvd mkh d ,DELEG⦈ $\begin{pmatrix} \,\href{Axiom.Set.Map.html#7168}{\htmlId{9025}{\htmlClass{Function}{\text{insertIfJust}}}}\, \,\href{Ledger.Conway.Specification.Certs.html#7565}{\htmlId{9038}{\htmlClass{Generalizable}{\text{c}}}}\, \,\href{Ledger.Conway.Specification.Certs.html#7837}{\htmlId{9040}{\htmlClass{Generalizable}{\text{mvd}}}}\, \,\href{Ledger.Conway.Specification.Certs.html#7323}{\htmlId{9044}{\htmlClass{Generalizable}{\text{vDelegs}}}}\, \\ \,\href{Axiom.Set.Map.html#7168}{\htmlId{9054}{\htmlClass{Function}{\text{insertIfJust}}}}\, \,\href{Ledger.Conway.Specification.Certs.html#7565}{\htmlId{9067}{\htmlClass{Generalizable}{\text{c}}}}\, \,\href{Ledger.Conway.Specification.Certs.html#7751}{\htmlId{9069}{\htmlClass{Generalizable}{\text{mkh}}}}\, \,\href{Ledger.Conway.Specification.Certs.html#7247}{\htmlId{9073}{\htmlClass{Generalizable}{\text{sDelegs}}}}\, \\ \,\href{Ledger.Conway.Specification.Certs.html#7179}{\htmlId{9083}{\htmlClass{Generalizable}{\text{rwds}}}}\, \,\href{Axiom.Set.Map.html#6320}{\htmlId{9088}{\htmlClass{Function Operator}{\text{∪ˡ}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{9091}{\htmlClass{Field Operator}{\text{❴}}}}\, \,\href{Ledger.Conway.Specification.Certs.html#7565}{\htmlId{9093}{\htmlClass{Generalizable}{\text{c}}}}\, , \,\htmlId{9097}{\htmlClass{Number}{\text{0}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{9099}{\htmlClass{Field Operator}{\text{❵}}}}\, \end{pmatrix}$
DELEG-dereg :
∙ (c , 0) ∈ rwds
────────────────────────────────
$\begin{pmatrix} \,\href{Ledger.Conway.Specification.Certs.html#7813}{\htmlId{9188}{\htmlClass{Generalizable}{\text{pp}}}}\, \\ \,\href{Ledger.Conway.Specification.Certs.html#7361}{\htmlId{9193}{\htmlClass{Generalizable}{\text{pools}}}}\, \\ \,\href{Ledger.Conway.Specification.Certs.html#7625}{\htmlId{9201}{\htmlClass{Generalizable}{\text{delegatees}}}}\, \end{pmatrix}$ ⊢ $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Certs.html#7323}{\htmlId{9218}{\htmlClass{Generalizable}{\text{vDelegs}}}}\, \\ \,\href{Ledger.Conway.Specification.Certs.html#7247}{\htmlId{9228}{\htmlClass{Generalizable}{\text{sDelegs}}}}\, \\ \,\href{Ledger.Conway.Specification.Certs.html#7179}{\htmlId{9238}{\htmlClass{Generalizable}{\text{rwds}}}}\, \end{pmatrix}$ ⇀⦇ dereg c md ,DELEG⦈ $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Certs.html#7323}{\htmlId{9269}{\htmlClass{Generalizable}{\text{vDelegs}}}}\, \,\href{Axiom.Set.Map.html#10748}{\htmlId{9277}{\htmlClass{Function Operator}{\text{∣}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{9279}{\htmlClass{Field Operator}{\text{❴}}}}\, \,\href{Ledger.Conway.Specification.Certs.html#7565}{\htmlId{9281}{\htmlClass{Generalizable}{\text{c}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{9283}{\htmlClass{Field Operator}{\text{❵}}}}\, \,\href{Axiom.Set.Map.html#10748}{\htmlId{9285}{\htmlClass{Function Operator}{\text{ᶜ}}}}\, \\ \,\href{Ledger.Conway.Specification.Certs.html#7247}{\htmlId{9289}{\htmlClass{Generalizable}{\text{sDelegs}}}}\, \,\href{Axiom.Set.Map.html#10748}{\htmlId{9297}{\htmlClass{Function Operator}{\text{∣}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{9299}{\htmlClass{Field Operator}{\text{❴}}}}\, \,\href{Ledger.Conway.Specification.Certs.html#7565}{\htmlId{9301}{\htmlClass{Generalizable}{\text{c}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{9303}{\htmlClass{Field Operator}{\text{❵}}}}\, \,\href{Axiom.Set.Map.html#10748}{\htmlId{9305}{\htmlClass{Function Operator}{\text{ᶜ}}}}\, \\ \,\href{Ledger.Conway.Specification.Certs.html#7179}{\htmlId{9309}{\htmlClass{Generalizable}{\text{rwds}}}}\, \,\href{Axiom.Set.Map.html#10748}{\htmlId{9314}{\htmlClass{Function Operator}{\text{∣}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{9316}{\htmlClass{Field Operator}{\text{❴}}}}\, \,\href{Ledger.Conway.Specification.Certs.html#7565}{\htmlId{9318}{\htmlClass{Generalizable}{\text{c}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{9320}{\htmlClass{Field Operator}{\text{❵}}}}\, \,\href{Axiom.Set.Map.html#10748}{\htmlId{9322}{\htmlClass{Function Operator}{\text{ᶜ}}}}\, \end{pmatrix}$
DELEG-reg :
∙ c ∉ dom rwds
∙ d ≡ pp .keyDeposit ⊎ d ≡ 0
────────────────────────────────
$\begin{pmatrix} \,\href{Ledger.Conway.Specification.Certs.html#7813}{\htmlId{9440}{\htmlClass{Generalizable}{\text{pp}}}}\, \\ \,\href{Ledger.Conway.Specification.Certs.html#7361}{\htmlId{9445}{\htmlClass{Generalizable}{\text{pools}}}}\, \\ \,\href{Ledger.Conway.Specification.Certs.html#7625}{\htmlId{9453}{\htmlClass{Generalizable}{\text{delegatees}}}}\, \end{pmatrix}$ ⊢ $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Certs.html#7323}{\htmlId{9470}{\htmlClass{Generalizable}{\text{vDelegs}}}}\, \\ \,\href{Ledger.Conway.Specification.Certs.html#7247}{\htmlId{9480}{\htmlClass{Generalizable}{\text{sDelegs}}}}\, \\ \,\href{Ledger.Conway.Specification.Certs.html#7179}{\htmlId{9490}{\htmlClass{Generalizable}{\text{rwds}}}}\, \end{pmatrix}$ ⇀⦇ reg c d ,DELEG⦈ $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Certs.html#7323}{\htmlId{9518}{\htmlClass{Generalizable}{\text{vDelegs}}}}\, \\ \,\href{Ledger.Conway.Specification.Certs.html#7247}{\htmlId{9528}{\htmlClass{Generalizable}{\text{sDelegs}}}}\, \\ \,\href{Ledger.Conway.Specification.Certs.html#7179}{\htmlId{9538}{\htmlClass{Generalizable}{\text{rwds}}}}\, \,\href{Axiom.Set.Map.html#6320}{\htmlId{9543}{\htmlClass{Function Operator}{\text{∪ˡ}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{9546}{\htmlClass{Field Operator}{\text{❴}}}}\, \,\href{Ledger.Conway.Specification.Certs.html#7565}{\htmlId{9548}{\htmlClass{Generalizable}{\text{c}}}}\, , \,\htmlId{9552}{\htmlClass{Number}{\text{0}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{9554}{\htmlClass{Field Operator}{\text{❵}}}}\, \end{pmatrix}$
data _⊢_⇀⦇_,POOL⦈_
where
POOL-regpool :
∙ kh ∉ dom pools
────────────────────────────────
pp ⊢ $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Certs.html#7361}{\htmlId{9725}{\htmlClass{Generalizable}{\text{pools}}}}\, \\ \,\href{Ledger.Conway.Specification.Certs.html#7394}{\htmlId{9733}{\htmlClass{Generalizable}{\text{retiring}}}}\, \end{pmatrix}$ ⇀⦇ regpool kh poolParams ,POOL⦈ $\begin{pmatrix} \,\href{Class.HasSingleton.html#288}{\htmlId{9778}{\htmlClass{Field Operator}{\text{❴}}}}\, \,\href{Ledger.Conway.Specification.Certs.html#7727}{\htmlId{9780}{\htmlClass{Generalizable}{\text{kh}}}}\, , \,\href{Ledger.Conway.Specification.Certs.html#7781}{\htmlId{9785}{\htmlClass{Generalizable}{\text{poolParams}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{9796}{\htmlClass{Field Operator}{\text{❵}}}}\, \,\href{Axiom.Set.Map.html#6320}{\htmlId{9798}{\htmlClass{Function Operator}{\text{∪ˡ}}}}\, \,\href{Ledger.Conway.Specification.Certs.html#7361}{\htmlId{9801}{\htmlClass{Generalizable}{\text{pools}}}}\, \\ \,\href{Ledger.Conway.Specification.Certs.html#7394}{\htmlId{9809}{\htmlClass{Generalizable}{\text{retiring}}}}\, \end{pmatrix}$
POOL-retirepool :
────────────────────────────────
pp ⊢ $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Certs.html#7361}{\htmlId{9889}{\htmlClass{Generalizable}{\text{pools}}}}\, \\ \,\href{Ledger.Conway.Specification.Certs.html#7394}{\htmlId{9897}{\htmlClass{Generalizable}{\text{retiring}}}}\, \end{pmatrix}$ ⇀⦇ retirepool kh e ,POOL⦈ $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Certs.html#7361}{\htmlId{9936}{\htmlClass{Generalizable}{\text{pools}}}}\, \\ \,\href{Class.HasSingleton.html#288}{\htmlId{9944}{\htmlClass{Field Operator}{\text{❴}}}}\, \,\href{Ledger.Conway.Specification.Certs.html#7727}{\htmlId{9946}{\htmlClass{Generalizable}{\text{kh}}}}\, , \,\href{Ledger.Conway.Specification.Certs.html#7676}{\htmlId{9951}{\htmlClass{Generalizable}{\text{e}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{9953}{\htmlClass{Field Operator}{\text{❵}}}}\, \,\href{Axiom.Set.Map.html#6320}{\htmlId{9955}{\htmlClass{Function Operator}{\text{∪ˡ}}}}\, \,\href{Ledger.Conway.Specification.Certs.html#7394}{\htmlId{9958}{\htmlClass{Generalizable}{\text{retiring}}}}\, \end{pmatrix}$
data _⊢_⇀⦇_,GOVCERT⦈_
where
GOVCERT-regdrep :
let Γ = $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Certs.html#7676}{\htmlId{10082}{\htmlClass{Generalizable}{\text{e}}}}\, \\ \,\href{Ledger.Conway.Specification.Certs.html#7813}{\htmlId{10086}{\htmlClass{Generalizable}{\text{pp}}}}\, \\ \,\href{Ledger.Conway.Specification.Certs.html#7698}{\htmlId{10091}{\htmlClass{Generalizable}{\text{vs}}}}\, \\ \,\href{Ledger.Conway.Specification.Certs.html#7430}{\htmlId{10096}{\htmlClass{Generalizable}{\text{wdrls}}}}\, \\ \,\href{Ledger.Conway.Specification.Certs.html#7927}{\htmlId{10104}{\htmlClass{Generalizable}{\text{cc}}}}\, \end{pmatrix}$
in
∙ (d ≡ pp .drepDeposit × c ∉ dom dReps) ⊎ (d ≡ 0 × c ∈ dom dReps)
────────────────────────────────
Γ ⊢ $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Certs.html#7214}{\htmlId{10237}{\htmlClass{Generalizable}{\text{dReps}}}}\, \\ \,\href{Ledger.Conway.Specification.Certs.html#7286}{\htmlId{10245}{\htmlClass{Generalizable}{\text{ccKeys}}}}\, \end{pmatrix}$ ⇀⦇ regdrep c d an ,GOVCERT⦈ $\begin{pmatrix} \,\href{Class.HasSingleton.html#288}{\htmlId{10284}{\htmlClass{Field Operator}{\text{❴}}}}\, \,\href{Ledger.Conway.Specification.Certs.html#7565}{\htmlId{10286}{\htmlClass{Generalizable}{\text{c}}}}\, , \,\href{Ledger.Conway.Specification.Certs.html#7676}{\htmlId{10290}{\htmlClass{Generalizable}{\text{e}}}}\, \,\href{Class.HasAdd.Core.html#162}{\htmlId{10292}{\htmlClass{Field Operator}{\text{+}}}}\, \,\href{Ledger.Conway.Specification.Certs.html#7813}{\htmlId{10294}{\htmlClass{Generalizable}{\text{pp}}}}\, \,\htmlId{10297}{\htmlClass{Symbol}{\text{.}}}\,\,\href{Ledger.Conway.Specification.PParams.html#3442}{\htmlId{10298}{\htmlClass{Field}{\text{drepActivity}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{10311}{\htmlClass{Field Operator}{\text{❵}}}}\, \,\href{Axiom.Set.Map.html#6320}{\htmlId{10313}{\htmlClass{Function Operator}{\text{∪ˡ}}}}\, \,\href{Ledger.Conway.Specification.Certs.html#7214}{\htmlId{10316}{\htmlClass{Generalizable}{\text{dReps}}}}\, \\ \,\href{Ledger.Conway.Specification.Certs.html#7286}{\htmlId{10324}{\htmlClass{Generalizable}{\text{ccKeys}}}}\, \end{pmatrix}$
GOVCERT-deregdrep :
∙ c ∈ dom dReps
────────────────────────────────
$\begin{pmatrix} \,\href{Ledger.Conway.Specification.Certs.html#7676}{\htmlId{10423}{\htmlClass{Generalizable}{\text{e}}}}\, \\ \,\href{Ledger.Conway.Specification.Certs.html#7813}{\htmlId{10427}{\htmlClass{Generalizable}{\text{pp}}}}\, \\ \,\href{Ledger.Conway.Specification.Certs.html#7698}{\htmlId{10432}{\htmlClass{Generalizable}{\text{vs}}}}\, \\ \,\href{Ledger.Conway.Specification.Certs.html#7430}{\htmlId{10437}{\htmlClass{Generalizable}{\text{wdrls}}}}\, \\ \,\href{Ledger.Conway.Specification.Certs.html#7927}{\htmlId{10445}{\htmlClass{Generalizable}{\text{cc}}}}\, \end{pmatrix}$ ⊢ $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Certs.html#7214}{\htmlId{10454}{\htmlClass{Generalizable}{\text{dReps}}}}\, \\ \,\href{Ledger.Conway.Specification.Certs.html#7286}{\htmlId{10462}{\htmlClass{Generalizable}{\text{ccKeys}}}}\, \end{pmatrix}$ ⇀⦇ deregdrep c d ,GOVCERT⦈ $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Certs.html#7214}{\htmlId{10500}{\htmlClass{Generalizable}{\text{dReps}}}}\, \,\href{Axiom.Set.Map.html#10748}{\htmlId{10506}{\htmlClass{Function Operator}{\text{∣}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{10508}{\htmlClass{Field Operator}{\text{❴}}}}\, \,\href{Ledger.Conway.Specification.Certs.html#7565}{\htmlId{10510}{\htmlClass{Generalizable}{\text{c}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{10512}{\htmlClass{Field Operator}{\text{❵}}}}\, \,\href{Axiom.Set.Map.html#10748}{\htmlId{10514}{\htmlClass{Function Operator}{\text{ᶜ}}}}\, \\ \,\href{Ledger.Conway.Specification.Certs.html#7286}{\htmlId{10518}{\htmlClass{Generalizable}{\text{ccKeys}}}}\, \end{pmatrix}$
GOVCERT-ccreghot :
∙ (c , nothing) ∉ ccKeys
∙ c ∈ cc
────────────────────────────────
$\begin{pmatrix} \,\href{Ledger.Conway.Specification.Certs.html#7676}{\htmlId{10638}{\htmlClass{Generalizable}{\text{e}}}}\, \\ \,\href{Ledger.Conway.Specification.Certs.html#7813}{\htmlId{10642}{\htmlClass{Generalizable}{\text{pp}}}}\, \\ \,\href{Ledger.Conway.Specification.Certs.html#7698}{\htmlId{10647}{\htmlClass{Generalizable}{\text{vs}}}}\, \\ \,\href{Ledger.Conway.Specification.Certs.html#7430}{\htmlId{10652}{\htmlClass{Generalizable}{\text{wdrls}}}}\, \\ \,\href{Ledger.Conway.Specification.Certs.html#7927}{\htmlId{10660}{\htmlClass{Generalizable}{\text{cc}}}}\, \end{pmatrix}$ ⊢ $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Certs.html#7214}{\htmlId{10669}{\htmlClass{Generalizable}{\text{dReps}}}}\, \\ \,\href{Ledger.Conway.Specification.Certs.html#7286}{\htmlId{10677}{\htmlClass{Generalizable}{\text{ccKeys}}}}\, \end{pmatrix}$ ⇀⦇ ccreghot c mc ,GOVCERT⦈ $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Certs.html#7214}{\htmlId{10715}{\htmlClass{Generalizable}{\text{dReps}}}}\, \\ \,\href{Class.HasSingleton.html#288}{\htmlId{10723}{\htmlClass{Field Operator}{\text{❴}}}}\, \,\href{Ledger.Conway.Specification.Certs.html#7565}{\htmlId{10725}{\htmlClass{Generalizable}{\text{c}}}}\, , \,\href{Ledger.Conway.Specification.Certs.html#7592}{\htmlId{10729}{\htmlClass{Generalizable}{\text{mc}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{10732}{\htmlClass{Field Operator}{\text{❵}}}}\, \,\href{Axiom.Set.Map.html#6320}{\htmlId{10734}{\htmlClass{Function Operator}{\text{∪ˡ}}}}\, \,\href{Ledger.Conway.Specification.Certs.html#7286}{\htmlId{10737}{\htmlClass{Generalizable}{\text{ccKeys}}}}\, \end{pmatrix}$
data _⊢_⇀⦇_,CERT⦈_
where
CERT-deleg :
∙ $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Certs.html#7813}{\htmlId{10858}{\htmlClass{Generalizable}{\text{pp}}}}\, \\ \,\href{Ledger.Conway.Specification.Certs.html#4045}{\htmlId{10863}{\htmlClass{Field}{\text{PState.pools}}}}\, \,\href{Ledger.Conway.Specification.Certs.html#7907}{\htmlId{10876}{\htmlClass{Generalizable}{\text{stᵖ}}}}\, \\ \,\href{Class.IsSet.html#916}{\htmlId{10882}{\htmlClass{Function}{\text{dom}}}}\, \,\htmlId{10886}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Conway.Specification.Certs.html#4160}{\htmlId{10887}{\htmlClass{Field}{\text{GState.dreps}}}}\, \,\href{Ledger.Conway.Specification.Certs.html#7887}{\htmlId{10900}{\htmlClass{Generalizable}{\text{stᵍ}}}}\,\,\htmlId{10903}{\htmlClass{Symbol}{\text{)}}}\, \end{pmatrix}$ ⊢ stᵈ ⇀⦇ dCert ,DELEG⦈ stᵈ'
────────────────────────────────
$\begin{pmatrix} \,\href{Ledger.Conway.Specification.Certs.html#7676}{\htmlId{10982}{\htmlClass{Generalizable}{\text{e}}}}\, \\ \,\href{Ledger.Conway.Specification.Certs.html#7813}{\htmlId{10986}{\htmlClass{Generalizable}{\text{pp}}}}\, \\ \,\href{Ledger.Conway.Specification.Certs.html#7698}{\htmlId{10991}{\htmlClass{Generalizable}{\text{vs}}}}\, \\ \,\href{Ledger.Conway.Specification.Certs.html#7430}{\htmlId{10996}{\htmlClass{Generalizable}{\text{wdrls}}}}\, \\ \,\href{Ledger.Conway.Specification.Certs.html#7927}{\htmlId{11004}{\htmlClass{Generalizable}{\text{cc}}}}\, \end{pmatrix}$ ⊢ $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Certs.html#7867}{\htmlId{11013}{\htmlClass{Generalizable}{\text{stᵈ}}}}\, \\ \,\href{Ledger.Conway.Specification.Certs.html#7907}{\htmlId{11019}{\htmlClass{Generalizable}{\text{stᵖ}}}}\, \\ \,\href{Ledger.Conway.Specification.Certs.html#7887}{\htmlId{11025}{\htmlClass{Generalizable}{\text{stᵍ}}}}\, \end{pmatrix}$ ⇀⦇ dCert ,CERT⦈ $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Certs.html#7871}{\htmlId{11049}{\htmlClass{Generalizable}{\text{stᵈ'}}}}\, \\ \,\href{Ledger.Conway.Specification.Certs.html#7907}{\htmlId{11056}{\htmlClass{Generalizable}{\text{stᵖ}}}}\, \\ \,\href{Ledger.Conway.Specification.Certs.html#7887}{\htmlId{11062}{\htmlClass{Generalizable}{\text{stᵍ}}}}\, \end{pmatrix}$
CERT-pool :
∙ pp ⊢ stᵖ ⇀⦇ dCert ,POOL⦈ stᵖ'
────────────────────────────────
$\begin{pmatrix} \,\href{Ledger.Conway.Specification.Certs.html#7676}{\htmlId{11166}{\htmlClass{Generalizable}{\text{e}}}}\, \\ \,\href{Ledger.Conway.Specification.Certs.html#7813}{\htmlId{11170}{\htmlClass{Generalizable}{\text{pp}}}}\, \\ \,\href{Ledger.Conway.Specification.Certs.html#7698}{\htmlId{11175}{\htmlClass{Generalizable}{\text{vs}}}}\, \\ \,\href{Ledger.Conway.Specification.Certs.html#7430}{\htmlId{11180}{\htmlClass{Generalizable}{\text{wdrls}}}}\, \\ \,\href{Ledger.Conway.Specification.Certs.html#7927}{\htmlId{11188}{\htmlClass{Generalizable}{\text{cc}}}}\, \end{pmatrix}$ ⊢ $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Certs.html#7867}{\htmlId{11197}{\htmlClass{Generalizable}{\text{stᵈ}}}}\, \\ \,\href{Ledger.Conway.Specification.Certs.html#7907}{\htmlId{11203}{\htmlClass{Generalizable}{\text{stᵖ}}}}\, \\ \,\href{Ledger.Conway.Specification.Certs.html#7887}{\htmlId{11209}{\htmlClass{Generalizable}{\text{stᵍ}}}}\, \end{pmatrix}$ ⇀⦇ dCert ,CERT⦈ $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Certs.html#7867}{\htmlId{11233}{\htmlClass{Generalizable}{\text{stᵈ}}}}\, \\ \,\href{Ledger.Conway.Specification.Certs.html#7911}{\htmlId{11239}{\htmlClass{Generalizable}{\text{stᵖ'}}}}\, \\ \,\href{Ledger.Conway.Specification.Certs.html#7887}{\htmlId{11246}{\htmlClass{Generalizable}{\text{stᵍ}}}}\, \end{pmatrix}$
CERT-vdel :
∙ Γ ⊢ stᵍ ⇀⦇ dCert ,GOVCERT⦈ stᵍ'
────────────────────────────────
Γ ⊢ $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Certs.html#7867}{\htmlId{11356}{\htmlClass{Generalizable}{\text{stᵈ}}}}\, \\ \,\href{Ledger.Conway.Specification.Certs.html#7907}{\htmlId{11362}{\htmlClass{Generalizable}{\text{stᵖ}}}}\, \\ \,\href{Ledger.Conway.Specification.Certs.html#7887}{\htmlId{11368}{\htmlClass{Generalizable}{\text{stᵍ}}}}\, \end{pmatrix}$ ⇀⦇ dCert ,CERT⦈ $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Certs.html#7867}{\htmlId{11392}{\htmlClass{Generalizable}{\text{stᵈ}}}}\, \\ \,\href{Ledger.Conway.Specification.Certs.html#7907}{\htmlId{11398}{\htmlClass{Generalizable}{\text{stᵖ}}}}\, \\ \,\href{Ledger.Conway.Specification.Certs.html#7891}{\htmlId{11404}{\htmlClass{Generalizable}{\text{stᵍ'}}}}\, \end{pmatrix}$
open GovVote using (voter)
data _⊢_⇀⦇_,CERTBASE⦈_ where
CERT-base :
let refresh = mapPartial (isGovVoterDRep ∘ voter) (fromList vs)
refreshedDReps = mapValueRestricted (const (e + pp .drepActivity)) dReps refresh
wdrlCreds = mapˢ stake (dom wdrls)
validVoteDelegs = voteDelegs ∣^ ( mapˢ vDelegCredential (dom dReps)
∪ fromList (vDelegNoConfidence ∷ vDelegAbstain ∷ []) )
in
∙ filter isKeyHash wdrlCreds ⊆ dom voteDelegs
∙ mapˢ (map₁ stake) (wdrls ˢ) ⊆ rewards ˢ
────────────────────────────────
$\begin{pmatrix} \,\href{Ledger.Conway.Specification.Certs.html#7676}{\htmlId{12027}{\htmlClass{Generalizable}{\text{e}}}}\, \\ \,\href{Ledger.Conway.Specification.Certs.html#7813}{\htmlId{12031}{\htmlClass{Generalizable}{\text{pp}}}}\, \\ \,\href{Ledger.Conway.Specification.Certs.html#7698}{\htmlId{12036}{\htmlClass{Generalizable}{\text{vs}}}}\, \\ \,\href{Ledger.Conway.Specification.Certs.html#7430}{\htmlId{12041}{\htmlClass{Generalizable}{\text{wdrls}}}}\, \\ \,\href{Ledger.Conway.Specification.Certs.html#7927}{\htmlId{12049}{\htmlClass{Generalizable}{\text{cc}}}}\, \end{pmatrix}$ ⊢ $\begin{pmatrix} \begin{pmatrix} \,\href{Ledger.Conway.Specification.Certs.html#7331}{\htmlId{12060}{\htmlClass{Generalizable}{\text{voteDelegs}}}}\, \\ \,\href{Ledger.Conway.Specification.Certs.html#7255}{\htmlId{12073}{\htmlClass{Generalizable}{\text{stakeDelegs}}}}\, \\ \,\href{Ledger.Conway.Specification.Certs.html#7184}{\htmlId{12087}{\htmlClass{Generalizable}{\text{rewards}}}}\, \end{pmatrix} \\ \,\href{Ledger.Conway.Specification.Certs.html#7907}{\htmlId{12099}{\htmlClass{Generalizable}{\text{stᵖ}}}}\, \\ \begin{pmatrix} \,\href{Ledger.Conway.Specification.Certs.html#7214}{\htmlId{12107}{\htmlClass{Generalizable}{\text{dReps}}}}\, \\ \,\href{Ledger.Conway.Specification.Certs.html#7293}{\htmlId{12115}{\htmlClass{Generalizable}{\text{ccHotKeys}}}}\, \end{pmatrix} \end{pmatrix}$ ⇀⦇ _ ,CERTBASE⦈ $\begin{pmatrix} \begin{pmatrix} \,\href{Ledger.Conway.Specification.Certs.html#11712}{\htmlId{12149}{\htmlClass{Bound}{\text{validVoteDelegs}}}}\, \\ \,\href{Ledger.Conway.Specification.Certs.html#7255}{\htmlId{12167}{\htmlClass{Generalizable}{\text{stakeDelegs}}}}\, \\ \,\href{Axiom.Set.Map.html#9130}{\htmlId{12181}{\htmlClass{Function}{\text{constMap}}}}\, \,\href{Ledger.Conway.Specification.Certs.html#11662}{\htmlId{12190}{\htmlClass{Bound}{\text{wdrlCreds}}}}\, \,\htmlId{12200}{\htmlClass{Number}{\text{0}}}\, \,\href{Axiom.Set.Map.html#6320}{\htmlId{12202}{\htmlClass{Function Operator}{\text{∪ˡ}}}}\, \,\href{Ledger.Conway.Specification.Certs.html#7184}{\htmlId{12205}{\htmlClass{Generalizable}{\text{rewards}}}}\, \end{pmatrix} \\ \,\href{Ledger.Conway.Specification.Certs.html#7907}{\htmlId{12217}{\htmlClass{Generalizable}{\text{stᵖ}}}}\, \\ \begin{pmatrix} \,\href{Ledger.Conway.Specification.Certs.html#11571}{\htmlId{12225}{\htmlClass{Bound}{\text{refreshedDReps}}}}\, \\ \,\href{Ledger.Conway.Specification.Certs.html#7293}{\htmlId{12242}{\htmlClass{Generalizable}{\text{ccHotKeys}}}}\, \end{pmatrix} \end{pmatrix}$