Certificates

{-# 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 import Ledger.Dijkstra.Specification.Account gs
open RewardAddress
open PParams

record StakePoolParams : Type where
  field
    owners          : ℙ KeyHash
    cost            : Coin
    margin          : UnitInterval
    pledge          : Coin
    rewardAccount   : RewardAddress
    vrf             : VRF
    bls             : Maybe (BlsVKey × BlsPoP)

The stake pool state extends the stake pool registration parameters with the epoch when the BLS key is first registered. This epoch is used to compute its expiration epoch.

record StakePoolState : Type where
  field
    owners          : ℙ KeyHash
    cost            : Coin
    margin          : UnitInterval
    pledge          : Coin
    rewardAccount   : RewardAddress
    vrf             : VRF
    bls             : Maybe (BlsVKey × Epoch)

The function mkStakePoolState maps a value of StakePoolParams to StakePoolState. Note that it drops the Proof of Possesion accompanying the BLS key and records the registration epoch of the key.

mkStakePoolState : Epoch → StakePoolParams → StakePoolState
mkStakePoolState e spp =
  record
    { owners = owners
    ; cost = cost
    ; margin = margin
    ; pledge = pledge
    ; rewardAccount = rewardAccount
    ; vrf = vrf
    ; bls = bls >>= λ (blsKey , PoP) → just (blsKey , e)
    }
    where open StakePoolParams spp

CCHotKeys : Type
CCHotKeys = Credential ⇀ Maybe Credential

Pools : Type
Pools = KeyHash ⇀ StakePoolState

FPools : Type
FPools = KeyHash ⇀ StakePoolParams

Retiring : Type
Retiring = KeyHash ⇀ Epoch

In the Dijkstra era, the Rewards map represents account balances, not just staking rewards. An account's balance may increase via staking rewards (at epoch boundaries) or via direct deposits (CIP-159). Withdrawals decrease the balance. The name Rewards is retained for backwards compatibility.

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 → 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

poolOwners : DCert → ℙ KeyHash
poolOwners (regpool _ pps) = StakePoolParams.owners pps
poolOwners _               = ∅

IsPoolRegistered : Pools → KeyHash → Type
IsPoolRegistered ps kh = kh ∈ dom ps

IsConwayCert : DCert → Type
IsConwayCert (regdrep _ _ _)           = ⊤
IsConwayCert (deregdrep _ _)           = ⊤
IsConwayCert (ccreghot _ _)            = ⊤
IsConwayCert (delegate _ (just _) _ _) = ⊤
IsConwayCert _                         = ⊥

record CertEnv : Type where
  field
    epoch           : Epoch
    pp              : PParams
    coldCredentials : ℙ Credential

record DState : Type where
  constructor ⟦_,_,_,_⟧ᵈ
  field
    voteDelegs   : VoteDelegs
    stakeDelegs  : StakeDelegs
    rewards      : Rewards
    deposits     : Credential ⇀ Coin

record PState : Type where
  field
    pools     : Pools
    fPools    : FPools
    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 PoolEnv : Type where
  field
    epoch           : Epoch
    pp              : PParams

record GovCertEnv : Type where
  field
    epoch           : Epoch
    pp              : PParams
    coldCredentials : ℙ Credential

open StakePoolParams
open StakePoolState

IsConwayCert? : IsConwayCert ⁇¹
IsConwayCert? {x} .dec with x
... | regdrep _ _ _ = yes tt
... | deregdrep _ _ = yes tt
... | ccreghot _ _  = yes tt
... | delegate _ (just _) _ _ = yes tt
... | delegate _ nothing  _ _ = no (λ ())
... | dereg _ _ = no (λ ())
... | regpool _ _ = no (λ ())
... | retirepool _ _ = no (λ ())

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 HasColdCredentials {a} (A : Type a) : Type a where
  field ColdCredentialsOf : A → ℙ Credential
open HasColdCredentials ⦃...⦄ public

record HasPools {a} (A : Type a) : Type a where
  field PoolsOf : A → Pools
open HasPools ⦃...⦄ public

record HasFuturePools {a} (A : Type a) : Type a where
  field FuturePoolsOf : A → FPools
open HasFuturePools ⦃...⦄ 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

record HasEpoch {a} (A : Type a) : Type a where
  field EpochOf : A → Epoch
open HasEpoch ⦃...⦄ public

record HasVotes {a} (A : Type a) : Type a where
  field VotesOf : A → List GovVote
open HasVotes ⦃...⦄ public

instance
  HasPParams-CertEnv : HasPParams CertEnv
  HasPParams-CertEnv .PParamsOf = CertEnv.pp

  HasPParams-GovCertEnv : HasPParams GovCertEnv
  HasPParams-GovCertEnv .PParamsOf = GovCertEnv.pp

  HasColdCredentials-GovCertEnv : HasColdCredentials GovCertEnv
  HasColdCredentials-GovCertEnv .ColdCredentialsOf = GovCertEnv.coldCredentials

  HasColdCredentials-CertEnv : HasColdCredentials CertEnv
  HasColdCredentials-CertEnv .ColdCredentialsOf = CertEnv.coldCredentials

  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

  HasFuturePools-PState : HasFuturePools PState
  HasFuturePools-PState .FuturePoolsOf = PState.fPools

  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

  HasEpoch-GovCertEnv : HasEpoch GovCertEnv
  HasEpoch-GovCertEnv .EpochOf = GovCertEnv.epoch

  HasEpoch-CertEnv : HasEpoch CertEnv
  HasEpoch-CertEnv .EpochOf = CertEnv.epoch

  unquoteDecl HasCast-StakePoolState HasCast-CertEnv HasCast-DState HasCast-PState HasCast-GState HasCast-CertState HasCast-DelegEnv HasCast-PoolEnv HasCast-GovCertEnv = derive-HasCast
    (   (quote StakePoolState , HasCast-StakePoolState)
    ∷   (quote CertEnv , HasCast-CertEnv)
    ∷   (quote DState , HasCast-DState)
    ∷   (quote PState , HasCast-PState)
    ∷   (quote GState , HasCast-GState)
    ∷   (quote CertState , HasCast-CertState)
    ∷   (quote PoolEnv , HasCast-PoolEnv)
    ∷   (quote GovCertEnv , HasCast-GovCertEnv)
    ∷ [ (quote DelegEnv , HasCast-DelegEnv) ])


private variable
  rwds rewards           : Rewards
  dReps                  : DReps
  sDelegs stakeDelegs    : StakeDelegs
  ccKeys ccHotKeys       : CCHotKeys
  vDelegs voteDelegs     : VoteDelegs
  pools                  : Pools
  fPools                 : FPools
  retiring               : Retiring
  A                      : Type
  deposits deposits'     : A ⇀ Coin
  depositsᵍ depositsᵍ'    : Credential ⇀ Coin
  depositsᵈ depositsᵈ'    : Credential ⇀ Coin

  an          : Anchor
  Γ           : CertEnv
  d           : Coin
  c           : Credential
  mc          : Maybe Credential
  delegatees  : ℙ Credential
  dCert       : DCert
  e 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
  stᶜ stᶜ' : CertState
  cc : ℙ Credential

rewardsBalance : DState → Coin
rewardsBalance ds = ∑[ x ← RewardsOf ds ] x

Cert-State Deposit Accounting

Functions in this section compute the effect that a DCert list has on the three deposit fields (DState.deposits, PState.deposits, GState.deposits) carried by a CertState.

In Dijkstra, delegation and DRep (de)registration certificates carry their deposit explicitly, so new and refunded deposits can be computed from the certificate list alone. The exception is pool registration: regpool carries no deposit, and whether it charges poolDeposit depends on whether the pool is already registered. newCertDeposits therefore additionally takes the set of registered pool keys (pools : ℙ KeyHash), and threads it through the certificate list, charging each newly registered pool exactly once.

module _ (pp : PParams) where

  newCertDeposits : ℙ KeyHash → List DCert → Coin
  newCertDeposits pools = proj₁ ∘ foldl addNewCertDeposit ( , pools)
    where
      addNewCertDeposit : Coin × ℙ KeyHash → DCert → Coin × ℙ KeyHash
      addNewCertDeposit (dep , pools) (delegate _ _ _ d) = dep + d , pools
      addNewCertDeposit (dep , pools) (regpool kh _)     =
        if kh ∈ pools
          then (dep , pools)
          else (dep + pp .poolDeposit , pools ∪ ❴ kh ❵)
      addNewCertDeposit (dep , pools) (regdrep _ d _) = dep + d , pools
      addNewCertDeposit acc           _               = acc

  refundCertDeposits : List DCert → Coin
  refundCertDeposits = foldl addRefundCertDeposit 
    where
      addRefundCertDeposit : Coin → DCert → Coin
      addRefundCertDeposit acc (dereg _ d)     = acc + d
      addRefundCertDeposit acc (deregdrep _ d) = acc + d
      addRefundCertDeposit acc _               = acc

The two coin-bearing components of a CertState are the rewards (account) balances and the three deposit pots. coinFromRewards and coinFromDeposits project their totals; getCoin on a CertState is their sum, so preservation-of-value statements can be phrased at the CertState level.

coinFromRewards : CertState → Coin
coinFromRewards = rewardsBalance ∘ DStateOf

coinFromDeposits : CertState → Coin
coinFromDeposits cs =
  getCoin (DepositsOf (DStateOf cs)) + getCoin (DepositsOf (PStateOf cs)) + getCoin (DepositsOf (GStateOf cs))

A CertState is pool-deposit registered when every entry of the pool deposit pot belongs to a registered pool.

PoolDepositsRegistered : CertState → Type
PoolDepositsRegistered cs = dom (DepositsOf (PStateOf cs)) ⊆ dom (PoolsOf cs)

instance
  HasCoin-CertState : HasCoin CertState
  -- Total coin held in a CertState: the rewards balance plus the deposit pots.
  HasCoin-CertState .getCoin = λ cs → coinFromRewards cs + coinFromDeposits cs

  unquoteDecl DecEq-StakePoolParams = derive-DecEq
    ((quote StakePoolParams , DecEq-StakePoolParams) ∷ [])
  unquoteDecl DecEq-StakePoolState = derive-DecEq
    ((quote StakePoolState , DecEq-StakePoolState) ∷ [])
  unquoteDecl DecEq-DCert = derive-DecEq
    ((quote DCert , DecEq-DCert) ∷ [])

Auxiliary Transition Systems

DELEG Transition System

data _⊢_⇀⦇_,DELEG⦈_ : DelegEnv → DState → DCert → DState → Type where

  DELEG-delegate :
    ∙ (c ∉ dom rwds → d ≡ pp .keyDeposit)
    ∙ (c ∈ dom rwds → d ≡ )
    ∙ 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#10967}{\htmlId{14913}{\htmlClass{Generalizable}{\text{pp}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#10387}{\htmlId{14918}{\htmlClass{Generalizable}{\text{pools}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#10779}{\htmlId{14926}{\htmlClass{Generalizable}{\text{delegatees}}}}\, \end{pmatrix}$ ⊢ $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Certs.html#10349}{\htmlId{14943}{\htmlClass{Generalizable}{\text{vDelegs}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#10273}{\htmlId{14953}{\htmlClass{Generalizable}{\text{sDelegs}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#10205}{\htmlId{14963}{\htmlClass{Generalizable}{\text{rwds}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#10522}{\htmlId{14970}{\htmlClass{Generalizable}{\text{deposits}}}}\, \end{pmatrix}$ ⇀⦇ delegate c mvd mkh d ,DELEG⦈ $\begin{pmatrix} \,\href{Axiom.Set.Map.html#9262}{\htmlId{15015}{\htmlClass{Function}{\text{insertIfJust}}}}\, \,\href{Ledger.Dijkstra.Specification.Certs.html#10719}{\htmlId{15028}{\htmlClass{Generalizable}{\text{c}}}}\, \,\href{Ledger.Dijkstra.Specification.Certs.html#10991}{\htmlId{15030}{\htmlClass{Generalizable}{\text{mvd}}}}\, \,\href{Ledger.Dijkstra.Specification.Certs.html#10349}{\htmlId{15034}{\htmlClass{Generalizable}{\text{vDelegs}}}}\, \\ \,\href{Axiom.Set.Map.html#9262}{\htmlId{15044}{\htmlClass{Function}{\text{insertIfJust}}}}\, \,\href{Ledger.Dijkstra.Specification.Certs.html#10719}{\htmlId{15057}{\htmlClass{Generalizable}{\text{c}}}}\, \,\href{Ledger.Dijkstra.Specification.Certs.html#10905}{\htmlId{15059}{\htmlClass{Generalizable}{\text{mkh}}}}\, \,\href{Ledger.Dijkstra.Specification.Certs.html#10273}{\htmlId{15063}{\htmlClass{Generalizable}{\text{sDelegs}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#10205}{\htmlId{15073}{\htmlClass{Generalizable}{\text{rwds}}}}\, \,\href{Axiom.Set.Map.html#7640}{\htmlId{15078}{\htmlClass{Function Operator}{\text{∪ˡ}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{15081}{\htmlClass{Field Operator}{\text{❴}}}}\, \,\href{Ledger.Dijkstra.Specification.Certs.html#10719}{\htmlId{15083}{\htmlClass{Generalizable}{\text{c}}}}\, , \,\htmlId{15087}{\htmlClass{Number}{\text{0}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{15089}{\htmlClass{Field Operator}{\text{❵}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#10522}{\htmlId{15093}{\htmlClass{Generalizable}{\text{deposits}}}}\, \,\href{Axiom.Set.Map.Dec.html#2149}{\htmlId{15102}{\htmlClass{Function Operator}{\text{∪⁺}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{15105}{\htmlClass{Field Operator}{\text{❴}}}}\, \,\href{Ledger.Dijkstra.Specification.Certs.html#10719}{\htmlId{15107}{\htmlClass{Generalizable}{\text{c}}}}\, , \,\href{Ledger.Dijkstra.Specification.Certs.html#10698}{\htmlId{15111}{\htmlClass{Generalizable}{\text{d}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{15113}{\htmlClass{Field Operator}{\text{❵}}}}\, \end{pmatrix}$

  DELEG-dereg :
    ∙ (c , ) ∈ rwds
    ∙ (c , d) ∈ deposits
      ────────────────────────────────
      $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Certs.html#10967}{\htmlId{15227}{\htmlClass{Generalizable}{\text{pp}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#10387}{\htmlId{15232}{\htmlClass{Generalizable}{\text{pools}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#10779}{\htmlId{15240}{\htmlClass{Generalizable}{\text{delegatees}}}}\, \end{pmatrix}$ ⊢ $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Certs.html#10349}{\htmlId{15257}{\htmlClass{Generalizable}{\text{vDelegs}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#10273}{\htmlId{15267}{\htmlClass{Generalizable}{\text{sDelegs}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#10205}{\htmlId{15277}{\htmlClass{Generalizable}{\text{rwds}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#10522}{\htmlId{15284}{\htmlClass{Generalizable}{\text{deposits}}}}\, \end{pmatrix}$ ⇀⦇ dereg c d ,DELEG⦈ $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Certs.html#10349}{\htmlId{15318}{\htmlClass{Generalizable}{\text{vDelegs}}}}\, \,\href{Axiom.Set.Map.html#13606}{\htmlId{15326}{\htmlClass{Function Operator}{\text{∣}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{15328}{\htmlClass{Field Operator}{\text{❴}}}}\, \,\href{Ledger.Dijkstra.Specification.Certs.html#10719}{\htmlId{15330}{\htmlClass{Generalizable}{\text{c}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{15332}{\htmlClass{Field Operator}{\text{❵}}}}\, \,\href{Axiom.Set.Map.html#13606}{\htmlId{15334}{\htmlClass{Function Operator}{\text{ᶜ}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#10273}{\htmlId{15338}{\htmlClass{Generalizable}{\text{sDelegs}}}}\, \,\href{Axiom.Set.Map.html#13606}{\htmlId{15346}{\htmlClass{Function Operator}{\text{∣}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{15348}{\htmlClass{Field Operator}{\text{❴}}}}\, \,\href{Ledger.Dijkstra.Specification.Certs.html#10719}{\htmlId{15350}{\htmlClass{Generalizable}{\text{c}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{15352}{\htmlClass{Field Operator}{\text{❵}}}}\, \,\href{Axiom.Set.Map.html#13606}{\htmlId{15354}{\htmlClass{Function Operator}{\text{ᶜ}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#10205}{\htmlId{15358}{\htmlClass{Generalizable}{\text{rwds}}}}\, \,\href{Axiom.Set.Map.html#13606}{\htmlId{15363}{\htmlClass{Function Operator}{\text{∣}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{15365}{\htmlClass{Field Operator}{\text{❴}}}}\, \,\href{Ledger.Dijkstra.Specification.Certs.html#10719}{\htmlId{15367}{\htmlClass{Generalizable}{\text{c}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{15369}{\htmlClass{Field Operator}{\text{❵}}}}\, \,\href{Axiom.Set.Map.html#13606}{\htmlId{15371}{\htmlClass{Function Operator}{\text{ᶜ}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#10522}{\htmlId{15375}{\htmlClass{Generalizable}{\text{deposits}}}}\, \,\href{Axiom.Set.Map.html#13606}{\htmlId{15384}{\htmlClass{Function Operator}{\text{∣}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{15386}{\htmlClass{Field Operator}{\text{❴}}}}\, \,\href{Ledger.Dijkstra.Specification.Certs.html#10719}{\htmlId{15388}{\htmlClass{Generalizable}{\text{c}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{15390}{\htmlClass{Field Operator}{\text{❵}}}}\, \,\href{Axiom.Set.Map.html#13606}{\htmlId{15392}{\htmlClass{Function Operator}{\text{ᶜ}}}}\, \end{pmatrix}$

POOL Transition System

Auxiliary Functions

We define three auxiliary predicates that enforce:

• Uniqueness of VRF keys: a VRF key belongs at most to one stake pool

• Uniqueness of BLS keys: a BLS key belongs at most to one stake pool

• Validity of the Proof of Possesion that accompanies a BLS key.

IsVRFUnique : VRF → Pools → FPools → Type
IsVRFUnique vrfKey pools fPools = 
   ¬ vrfKey ∈ mapˢ vrf (range pools) ∪ mapˢ vrf (range fPools)

IsBLSUnique : Maybe BlsVKey → Pools → FPools → Type
IsBLSUnique nothing       pools fPools = ⊤
IsBLSUnique (just blsKey) pools fPools =
   ¬ blsKey ∈ mapPartial ((proj₁ <$>_) ∘ bls) (range pools) ∪ mapPartial ((proj₁ <$>_) ∘ bls) (range fPools)

IsValidBLSPoP : Maybe (BlsVKey × BlsPoP) → Type
IsValidBLSPoP nothing                   = ⊤
IsValidBLSPoP (just (blsVKey , blsPoP)) = isValidPoP blsVKey blsPoP

IsBLSUnique? : ∀ {blsKey pools fPools} → IsBLSUnique blsKey pools fPools ⁇
IsBLSUnique? {(just x)} = Dec-→
IsBLSUnique? {nothing}  = Dec-⊤

IsValidBLSPoP? : ∀ {x} → IsValidBLSPoP x ⁇
IsValidBLSPoP? {just x}  = Dec-isValidPoP
IsValidBLSPoP? {nothing} = Dec-⊤

data _⊢_⇀⦇_,POOL⦈_ : PoolEnv → PState → DCert → PState → Type where

  POOL-reg :
    ∙ ¬ (IsPoolRegistered pools kh)
    ∙ IsVRFUnique (poolParams .vrf) pools fPools
    ∙ IsBLSUnique (proj₁ <$> poolParams .bls) pools fPools
    ∙ IsValidBLSPoP (poolParams .bls)
    ∙ NetworkIdOf (poolParams .rewardAccount) ≡ NetworkId
    ∙ pp .minPoolCost ≤ poolParams .cost
    ────────────────────────────────
    $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Certs.html#10830}{\htmlId{17002}{\htmlClass{Generalizable}{\text{e}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#10967}{\htmlId{17006}{\htmlClass{Generalizable}{\text{pp}}}}\, \end{pmatrix}$ ⊢ $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Certs.html#10387}{\htmlId{17015}{\htmlClass{Generalizable}{\text{pools}}}}\,
                 \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#10420}{\htmlId{17040}{\htmlClass{Generalizable}{\text{fPools}}}}\,
                 \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#10454}{\htmlId{17066}{\htmlClass{Generalizable}{\text{retiring}}}}\,
                 \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#10522}{\htmlId{17094}{\htmlClass{Generalizable}{\text{deposits}}}}\,
                 \end{pmatrix}$ ⇀⦇ regpool kh poolParams ,POOL⦈ $\begin{pmatrix}
                   \,\href{Ledger.Dijkstra.Specification.Certs.html#10387}{\htmlId{17175}{\htmlClass{Generalizable}{\text{pools}}}}\, \,\href{Axiom.Set.Map.html#7640}{\htmlId{17181}{\htmlClass{Function Operator}{\text{∪ˡ}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{17184}{\htmlClass{Field Operator}{\text{❴}}}}\, \,\href{Ledger.Dijkstra.Specification.Certs.html#10881}{\htmlId{17186}{\htmlClass{Generalizable}{\text{kh}}}}\, , \,\href{Ledger.Dijkstra.Specification.Certs.html#1604}{\htmlId{17191}{\htmlClass{Function}{\text{mkStakePoolState}}}}\, \,\href{Ledger.Dijkstra.Specification.Certs.html#10830}{\htmlId{17208}{\htmlClass{Generalizable}{\text{e}}}}\, \,\href{Ledger.Dijkstra.Specification.Certs.html#10935}{\htmlId{17210}{\htmlClass{Generalizable}{\text{poolParams}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{17221}{\htmlClass{Field Operator}{\text{❵}}}}\,
                 \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#10420}{\htmlId{17242}{\htmlClass{Generalizable}{\text{fPools}}}}\,
                 \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#10454}{\htmlId{17268}{\htmlClass{Generalizable}{\text{retiring}}}}\,
                 \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#10522}{\htmlId{17296}{\htmlClass{Generalizable}{\text{deposits}}}}\, \,\href{Axiom.Set.Map.html#7640}{\htmlId{17305}{\htmlClass{Function Operator}{\text{∪ˡ}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{17308}{\htmlClass{Field Operator}{\text{❴}}}}\, \,\href{Ledger.Dijkstra.Specification.Certs.html#10881}{\htmlId{17310}{\htmlClass{Generalizable}{\text{kh}}}}\, , \,\href{Ledger.Dijkstra.Specification.Certs.html#10967}{\htmlId{17315}{\htmlClass{Generalizable}{\text{pp}}}}\, \,\htmlId{17318}{\htmlClass{Symbol}{\text{.}}}\,\,\href{Ledger.Dijkstra.Specification.PParams.html#3499}{\htmlId{17319}{\htmlClass{Field}{\text{poolDeposit}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{17331}{\htmlClass{Field Operator}{\text{❵}}}}\,
                 \end{pmatrix}$

  POOL-rereg :
    ∙ IsPoolRegistered pools kh
    ∙ IsVRFUnique (poolParams .vrf) (pools ∣ ❴ kh ❵ ᶜ) (fPools ∣ ❴ kh ❵ ᶜ)
    ∙ IsBLSUnique (proj₁ <$> poolParams .bls) (pools ∣ ❴ kh ❵ ᶜ) (fPools ∣ ❴ kh ❵ ᶜ)
    ∙ IsValidBLSPoP (poolParams .bls)
    ∙ NetworkIdOf (poolParams .rewardAccount) ≡ NetworkId
    ∙ pp .minPoolCost ≤ poolParams .cost
    ────────────────────────────────
    $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Certs.html#10830}{\htmlId{17740}{\htmlClass{Generalizable}{\text{e}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#10967}{\htmlId{17744}{\htmlClass{Generalizable}{\text{pp}}}}\, \end{pmatrix}$ ⊢ $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Certs.html#10387}{\htmlId{17753}{\htmlClass{Generalizable}{\text{pools}}}}\,
                 \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#10420}{\htmlId{17778}{\htmlClass{Generalizable}{\text{fPools}}}}\,
                 \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#10454}{\htmlId{17804}{\htmlClass{Generalizable}{\text{retiring}}}}\,
                 \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#10522}{\htmlId{17832}{\htmlClass{Generalizable}{\text{deposits}}}}\,
                 \end{pmatrix}$ ⇀⦇ regpool kh poolParams ,POOL⦈ $\begin{pmatrix}
                   \,\href{Ledger.Dijkstra.Specification.Certs.html#10387}{\htmlId{17913}{\htmlClass{Generalizable}{\text{pools}}}}\,
                 \\ \,\href{Class.HasSingleton.html#288}{\htmlId{17938}{\htmlClass{Field Operator}{\text{❴}}}}\, \,\href{Ledger.Dijkstra.Specification.Certs.html#10881}{\htmlId{17940}{\htmlClass{Generalizable}{\text{kh}}}}\, , \,\href{Ledger.Dijkstra.Specification.Certs.html#10935}{\htmlId{17945}{\htmlClass{Generalizable}{\text{poolParams}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{17956}{\htmlClass{Field Operator}{\text{❵}}}}\, \,\href{Axiom.Set.Map.html#7640}{\htmlId{17958}{\htmlClass{Function Operator}{\text{∪ˡ}}}}\, \,\href{Ledger.Dijkstra.Specification.Certs.html#10420}{\htmlId{17961}{\htmlClass{Generalizable}{\text{fPools}}}}\,
                 \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#10454}{\htmlId{17987}{\htmlClass{Generalizable}{\text{retiring}}}}\, \,\href{Axiom.Set.Map.html#13606}{\htmlId{17996}{\htmlClass{Function Operator}{\text{∣}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{17998}{\htmlClass{Field Operator}{\text{❴}}}}\, \,\href{Ledger.Dijkstra.Specification.Certs.html#10881}{\htmlId{18000}{\htmlClass{Generalizable}{\text{kh}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{18003}{\htmlClass{Field Operator}{\text{❵}}}}\, \,\href{Axiom.Set.Map.html#13606}{\htmlId{18005}{\htmlClass{Function Operator}{\text{ᶜ}}}}\,
                 \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#10522}{\htmlId{18026}{\htmlClass{Generalizable}{\text{deposits}}}}\,
                 \end{pmatrix}$

  POOL-retirepool :
    ∙ IsPoolRegistered pools kh
    ∙ e < e'
    ∙ e' ≤ e + pp .Emax
    ────────────────────────────────
    $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Certs.html#10830}{\htmlId{18187}{\htmlClass{Generalizable}{\text{e}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#10967}{\htmlId{18191}{\htmlClass{Generalizable}{\text{pp}}}}\, \end{pmatrix}$ ⊢ $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Certs.html#10387}{\htmlId{18200}{\htmlClass{Generalizable}{\text{pools}}}}\,
                 \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#10420}{\htmlId{18225}{\htmlClass{Generalizable}{\text{fPools}}}}\,
                 \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#10454}{\htmlId{18251}{\htmlClass{Generalizable}{\text{retiring}}}}\,
                 \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#10522}{\htmlId{18279}{\htmlClass{Generalizable}{\text{deposits}}}}\,
                 \end{pmatrix}$ ⇀⦇ retirepool kh e' ,POOL⦈ $\begin{pmatrix}
                   \,\href{Ledger.Dijkstra.Specification.Certs.html#10387}{\htmlId{18355}{\htmlClass{Generalizable}{\text{pools}}}}\,
                 \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#10420}{\htmlId{18380}{\htmlClass{Generalizable}{\text{fPools}}}}\,
                 \\ \,\href{Class.HasSingleton.html#288}{\htmlId{18406}{\htmlClass{Field Operator}{\text{❴}}}}\, \,\href{Ledger.Dijkstra.Specification.Certs.html#10881}{\htmlId{18408}{\htmlClass{Generalizable}{\text{kh}}}}\, , \,\href{Ledger.Dijkstra.Specification.Certs.html#10832}{\htmlId{18413}{\htmlClass{Generalizable}{\text{e'}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{18416}{\htmlClass{Field Operator}{\text{❵}}}}\, \,\href{Axiom.Set.Map.html#7640}{\htmlId{18418}{\htmlClass{Function Operator}{\text{∪ˡ}}}}\, \,\href{Ledger.Dijkstra.Specification.Certs.html#10454}{\htmlId{18421}{\htmlClass{Generalizable}{\text{retiring}}}}\,
                 \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#10522}{\htmlId{18449}{\htmlClass{Generalizable}{\text{deposits}}}}\,
                 \end{pmatrix}$

GOVCERT Transition System

data _⊢_⇀⦇_,GOVCERT⦈_ : GovCertEnv → CertState → DCert → CertState → Type where

  GOVCERT-regdrep :
    ∙ (d ≡ pp .drepDeposit × c ∉ dom dReps) ⊎ (d ≡  × c ∈ dom dReps)
      ────────────────────────────────
      $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Certs.html#10830}{\htmlId{18755}{\htmlClass{Generalizable}{\text{e}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#10967}{\htmlId{18759}{\htmlClass{Generalizable}{\text{pp}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#11104}{\htmlId{18764}{\htmlClass{Generalizable}{\text{cc}}}}\, \end{pmatrix}$ ⊢ $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Certs.html#11021}{\htmlId{18773}{\htmlClass{Generalizable}{\text{stᵈ}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#11061}{\htmlId{18779}{\htmlClass{Generalizable}{\text{stᵖ}}}}\, \\ \begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Certs.html#10240}{\htmlId{18787}{\htmlClass{Generalizable}{\text{dReps}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#10312}{\htmlId{18795}{\htmlClass{Generalizable}{\text{ccKeys}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#10558}{\htmlId{18804}{\htmlClass{Generalizable}{\text{depositsᵍ}}}}\, \end{pmatrix} \end{pmatrix}$ ⇀⦇ regdrep c d an ,GOVCERT⦈ $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Certs.html#11021}{\htmlId{18848}{\htmlClass{Generalizable}{\text{stᵈ}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#11061}{\htmlId{18854}{\htmlClass{Generalizable}{\text{stᵖ}}}}\, \\ \begin{pmatrix} \,\href{Class.HasSingleton.html#288}{\htmlId{18862}{\htmlClass{Field Operator}{\text{❴}}}}\, \,\href{Ledger.Dijkstra.Specification.Certs.html#10719}{\htmlId{18864}{\htmlClass{Generalizable}{\text{c}}}}\, , \,\href{Ledger.Dijkstra.Specification.Certs.html#10830}{\htmlId{18868}{\htmlClass{Generalizable}{\text{e}}}}\, \,\href{Class.HasAdd.Core.html#162}{\htmlId{18870}{\htmlClass{Field Operator}{\text{+}}}}\, \,\href{Ledger.Dijkstra.Specification.Certs.html#10967}{\htmlId{18872}{\htmlClass{Generalizable}{\text{pp}}}}\, \,\htmlId{18875}{\htmlClass{Symbol}{\text{.}}}\,\,\href{Ledger.Dijkstra.Specification.PParams.html#4670}{\htmlId{18876}{\htmlClass{Field}{\text{drepActivity}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{18889}{\htmlClass{Field Operator}{\text{❵}}}}\, \,\href{Axiom.Set.Map.html#7640}{\htmlId{18891}{\htmlClass{Function Operator}{\text{∪ˡ}}}}\, \,\href{Ledger.Dijkstra.Specification.Certs.html#10240}{\htmlId{18894}{\htmlClass{Generalizable}{\text{dReps}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#10312}{\htmlId{18902}{\htmlClass{Generalizable}{\text{ccKeys}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#10558}{\htmlId{18911}{\htmlClass{Generalizable}{\text{depositsᵍ}}}}\, \,\href{Axiom.Set.Map.Dec.html#2149}{\htmlId{18921}{\htmlClass{Function Operator}{\text{∪⁺}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{18924}{\htmlClass{Field Operator}{\text{❴}}}}\, \,\href{Ledger.Dijkstra.Specification.Certs.html#10719}{\htmlId{18926}{\htmlClass{Generalizable}{\text{c}}}}\, , \,\href{Ledger.Dijkstra.Specification.Certs.html#10698}{\htmlId{18930}{\htmlClass{Generalizable}{\text{d}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{18932}{\htmlClass{Field Operator}{\text{❵}}}}\, \end{pmatrix} \end{pmatrix}$

  GOVCERT-deregdrep :
    ∙ c ∈ dom dReps
    ∙ (c , d) ∈ depositsᵍ
      ────────────────────────────────
      $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Certs.html#10830}{\htmlId{19054}{\htmlClass{Generalizable}{\text{e}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#10967}{\htmlId{19058}{\htmlClass{Generalizable}{\text{pp}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#11104}{\htmlId{19063}{\htmlClass{Generalizable}{\text{cc}}}}\, \end{pmatrix}$ ⊢ $\begin{pmatrix} \begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Certs.html#10349}{\htmlId{19074}{\htmlClass{Generalizable}{\text{vDelegs}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#10273}{\htmlId{19084}{\htmlClass{Generalizable}{\text{sDelegs}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#10205}{\htmlId{19094}{\htmlClass{Generalizable}{\text{rwds}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#10604}{\htmlId{19101}{\htmlClass{Generalizable}{\text{depositsᵈ}}}}\, \end{pmatrix} \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#11061}{\htmlId{19115}{\htmlClass{Generalizable}{\text{stᵖ}}}}\, \\ \begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Certs.html#10240}{\htmlId{19123}{\htmlClass{Generalizable}{\text{dReps}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#10312}{\htmlId{19131}{\htmlClass{Generalizable}{\text{ccKeys}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#10558}{\htmlId{19140}{\htmlClass{Generalizable}{\text{depositsᵍ}}}}\, \end{pmatrix} \end{pmatrix}$ ⇀⦇ deregdrep c d ,GOVCERT⦈ $\begin{pmatrix} \begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Certs.html#10349}{\htmlId{19185}{\htmlClass{Generalizable}{\text{vDelegs}}}}\, \,\href{Axiom.Set.Map.html#17850}{\htmlId{19193}{\htmlClass{Function Operator}{\text{∣\^{}}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{19196}{\htmlClass{Field Operator}{\text{❴}}}}\, \,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#2719}{\htmlId{19198}{\htmlClass{InductiveConstructor}{\text{vDelegCredential}}}}\, \,\href{Ledger.Dijkstra.Specification.Certs.html#10719}{\htmlId{19215}{\htmlClass{Generalizable}{\text{c}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{19217}{\htmlClass{Field Operator}{\text{❵}}}}\, \,\href{Axiom.Set.Map.html#17850}{\htmlId{19219}{\htmlClass{Function Operator}{\text{ᶜ}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#10273}{\htmlId{19223}{\htmlClass{Generalizable}{\text{sDelegs}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#10205}{\htmlId{19233}{\htmlClass{Generalizable}{\text{rwds}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#10604}{\htmlId{19240}{\htmlClass{Generalizable}{\text{depositsᵈ}}}}\, \end{pmatrix} \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#11061}{\htmlId{19254}{\htmlClass{Generalizable}{\text{stᵖ}}}}\, \\ \begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Certs.html#10240}{\htmlId{19262}{\htmlClass{Generalizable}{\text{dReps}}}}\, \,\href{Axiom.Set.Map.html#13606}{\htmlId{19268}{\htmlClass{Function Operator}{\text{∣}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{19270}{\htmlClass{Field Operator}{\text{❴}}}}\, \,\href{Ledger.Dijkstra.Specification.Certs.html#10719}{\htmlId{19272}{\htmlClass{Generalizable}{\text{c}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{19274}{\htmlClass{Field Operator}{\text{❵}}}}\, \,\href{Axiom.Set.Map.html#13606}{\htmlId{19276}{\htmlClass{Function Operator}{\text{ᶜ}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#10312}{\htmlId{19280}{\htmlClass{Generalizable}{\text{ccKeys}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#10558}{\htmlId{19289}{\htmlClass{Generalizable}{\text{depositsᵍ}}}}\, \,\href{Axiom.Set.Map.html#13606}{\htmlId{19299}{\htmlClass{Function Operator}{\text{∣}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{19301}{\htmlClass{Field Operator}{\text{❴}}}}\, \,\href{Ledger.Dijkstra.Specification.Certs.html#10719}{\htmlId{19303}{\htmlClass{Generalizable}{\text{c}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{19305}{\htmlClass{Field Operator}{\text{❵}}}}\, \,\href{Axiom.Set.Map.html#13606}{\htmlId{19307}{\htmlClass{Function Operator}{\text{ᶜ}}}}\, \end{pmatrix} \end{pmatrix}$

  GOVCERT-ccreghot :
    ∙ (c , nothing) ∉ ccKeys
    ∙ c ∈ cc
      ────────────────────────────────
      $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Certs.html#10830}{\htmlId{19424}{\htmlClass{Generalizable}{\text{e}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#10967}{\htmlId{19428}{\htmlClass{Generalizable}{\text{pp}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#11104}{\htmlId{19433}{\htmlClass{Generalizable}{\text{cc}}}}\, \end{pmatrix}$ ⊢ $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Certs.html#11021}{\htmlId{19442}{\htmlClass{Generalizable}{\text{stᵈ}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#11061}{\htmlId{19448}{\htmlClass{Generalizable}{\text{stᵖ}}}}\, \\ \begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Certs.html#10240}{\htmlId{19456}{\htmlClass{Generalizable}{\text{dReps}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#10312}{\htmlId{19464}{\htmlClass{Generalizable}{\text{ccKeys}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#10558}{\htmlId{19473}{\htmlClass{Generalizable}{\text{depositsᵍ}}}}\, \end{pmatrix} \end{pmatrix}$ ⇀⦇ ccreghot c mc ,GOVCERT⦈ $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Certs.html#11021}{\htmlId{19516}{\htmlClass{Generalizable}{\text{stᵈ}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#11061}{\htmlId{19522}{\htmlClass{Generalizable}{\text{stᵖ}}}}\, \\ \begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Certs.html#10240}{\htmlId{19530}{\htmlClass{Generalizable}{\text{dReps}}}}\, \\ \,\href{Class.HasSingleton.html#288}{\htmlId{19538}{\htmlClass{Field Operator}{\text{❴}}}}\, \,\href{Ledger.Dijkstra.Specification.Certs.html#10719}{\htmlId{19540}{\htmlClass{Generalizable}{\text{c}}}}\, , \,\href{Ledger.Dijkstra.Specification.Certs.html#10746}{\htmlId{19544}{\htmlClass{Generalizable}{\text{mc}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{19547}{\htmlClass{Field Operator}{\text{❵}}}}\, \,\href{Axiom.Set.Map.html#7640}{\htmlId{19549}{\htmlClass{Function Operator}{\text{∪ˡ}}}}\, \,\href{Ledger.Dijkstra.Specification.Certs.html#10312}{\htmlId{19552}{\htmlClass{Generalizable}{\text{ccKeys}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#10558}{\htmlId{19561}{\htmlClass{Generalizable}{\text{depositsᵍ}}}}\, \end{pmatrix} \end{pmatrix}$

CERT Transition System

data _⊢_⇀⦇_,CERT⦈_  : CertEnv → CertState → DCert → CertState → Type where

  CERT-deleg :
    ∙ $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Certs.html#10967}{\htmlId{19730}{\htmlClass{Generalizable}{\text{pp}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#5677}{\htmlId{19735}{\htmlClass{Field}{\text{PoolsOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Certs.html#11061}{\htmlId{19743}{\htmlClass{Generalizable}{\text{stᵖ}}}}\, \\ \,\href{Class.IsSet.html#916}{\htmlId{19749}{\htmlClass{Function}{\text{dom}}}}\, \,\htmlId{19753}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#5444}{\htmlId{19754}{\htmlClass{Field}{\text{DRepsOf}}}}\, \,\href{Ledger.Dijkstra.Specification.Certs.html#11041}{\htmlId{19762}{\htmlClass{Generalizable}{\text{stᵍ}}}}\,\,\htmlId{19765}{\htmlClass{Symbol}{\text{)}}}\, \end{pmatrix}$ ⊢ stᵈ ⇀⦇ dCert ,DELEG⦈ stᵈ'
      ────────────────────────────────
      $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Certs.html#10830}{\htmlId{19844}{\htmlClass{Generalizable}{\text{e}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#10967}{\htmlId{19848}{\htmlClass{Generalizable}{\text{pp}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#11104}{\htmlId{19853}{\htmlClass{Generalizable}{\text{cc}}}}\, \end{pmatrix}$ ⊢ $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Certs.html#11021}{\htmlId{19862}{\htmlClass{Generalizable}{\text{stᵈ}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#11061}{\htmlId{19868}{\htmlClass{Generalizable}{\text{stᵖ}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#11041}{\htmlId{19874}{\htmlClass{Generalizable}{\text{stᵍ}}}}\, \end{pmatrix}$ ⇀⦇ dCert ,CERT⦈ $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Certs.html#11025}{\htmlId{19898}{\htmlClass{Generalizable}{\text{stᵈ'}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#11061}{\htmlId{19905}{\htmlClass{Generalizable}{\text{stᵖ}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#11041}{\htmlId{19911}{\htmlClass{Generalizable}{\text{stᵍ}}}}\, \end{pmatrix}$

  CERT-pool :
    ∙ $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Certs.html#10830}{\htmlId{19940}{\htmlClass{Generalizable}{\text{e}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#10967}{\htmlId{19944}{\htmlClass{Generalizable}{\text{pp}}}}\, \end{pmatrix}$ ⊢ stᵖ ⇀⦇ dCert ,POOL⦈ stᵖ'
      ────────────────────────────────
      $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Certs.html#10830}{\htmlId{20023}{\htmlClass{Generalizable}{\text{e}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#10967}{\htmlId{20027}{\htmlClass{Generalizable}{\text{pp}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#11104}{\htmlId{20032}{\htmlClass{Generalizable}{\text{cc}}}}\, \end{pmatrix}$ ⊢ $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Certs.html#11021}{\htmlId{20041}{\htmlClass{Generalizable}{\text{stᵈ}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#11061}{\htmlId{20047}{\htmlClass{Generalizable}{\text{stᵖ}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#11041}{\htmlId{20053}{\htmlClass{Generalizable}{\text{stᵍ}}}}\, \end{pmatrix}$ ⇀⦇ dCert ,CERT⦈ $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Certs.html#11021}{\htmlId{20077}{\htmlClass{Generalizable}{\text{stᵈ}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#11065}{\htmlId{20083}{\htmlClass{Generalizable}{\text{stᵖ'}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#11041}{\htmlId{20090}{\htmlClass{Generalizable}{\text{stᵍ}}}}\, \end{pmatrix}$

  CERT-gov :
    ∙ $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Certs.html#10830}{\htmlId{20118}{\htmlClass{Generalizable}{\text{e}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#10967}{\htmlId{20122}{\htmlClass{Generalizable}{\text{pp}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#11104}{\htmlId{20127}{\htmlClass{Generalizable}{\text{cc}}}}\, \end{pmatrix}$ ⊢ stᶜ ⇀⦇ dCert ,GOVCERT⦈ stᶜ'
      ────────────────────────────────
      $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Certs.html#10830}{\htmlId{20209}{\htmlClass{Generalizable}{\text{e}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#10967}{\htmlId{20213}{\htmlClass{Generalizable}{\text{pp}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#11104}{\htmlId{20218}{\htmlClass{Generalizable}{\text{cc}}}}\, \end{pmatrix}$ ⊢ stᶜ ⇀⦇ dCert ,CERT⦈ stᶜ'

CERTS Transition System

_⊢_⇀⦇_,CERTS⦈_  : CertEnv → CertState  → List DCert  → CertState  → Type
_⊢_⇀⦇_,CERTS⦈_ = ReflexiveTransitiveClosure {sts = _⊢_⇀⦇_,CERT⦈_}