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   : Credential

CCHotKeys : Type
CCHotKeys = Credential ⇀ Maybe Credential

PoolEnv : Type
PoolEnv = PParams

Pools : Type
Pools = 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

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

-- Certification Types
record CertEnv : Type where
  field
    epoch           : Epoch
    pp              : PParams
    votes           : List GovVote
    wdrls           : Withdrawals
    coldCreds       : ℙ Credential
    directDeposits  : DirectDeposits

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

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

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

  HasVotes-CertEnv : HasVotes CertEnv
  HasVotes-CertEnv .VotesOf = CertEnv.votes

  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
  dd                     : DirectDeposits
  A                      : Type
  deposits deposits'     : A ⇀ Coin

  an          : Anchor
  Γ           : CertEnv
  d           : 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

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

instance
  HasCoin-CertState : HasCoin CertState
  HasCoin-CertState .getCoin = rewardsBalance ∘ DStateOf

  unquoteDecl DecEq-StakePoolParams = derive-DecEq
    ((quote StakePoolParams , DecEq-StakePoolParams) ∷ [])
  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#8106}{\htmlId{10918}{\htmlClass{Generalizable}{\text{pp}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#7571}{\htmlId{10923}{\htmlClass{Generalizable}{\text{pools}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#7918}{\htmlId{10931}{\htmlClass{Generalizable}{\text{delegatees}}}}\, \end{pmatrix}$ ⊢ $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Certs.html#7533}{\htmlId{10948}{\htmlClass{Generalizable}{\text{vDelegs}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#7457}{\htmlId{10958}{\htmlClass{Generalizable}{\text{sDelegs}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#7389}{\htmlId{10968}{\htmlClass{Generalizable}{\text{rwds}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#7753}{\htmlId{10975}{\htmlClass{Generalizable}{\text{deposits}}}}\, \end{pmatrix}$ ⇀⦇ delegate c mvd mkh d ,DELEG⦈ $\begin{pmatrix} \,\href{Axiom.Set.Map.html#9262}{\htmlId{11020}{\htmlClass{Function}{\text{insertIfJust}}}}\, \,\href{Ledger.Dijkstra.Specification.Certs.html#7858}{\htmlId{11033}{\htmlClass{Generalizable}{\text{c}}}}\, \,\href{Ledger.Dijkstra.Specification.Certs.html#8130}{\htmlId{11035}{\htmlClass{Generalizable}{\text{mvd}}}}\, \,\href{Ledger.Dijkstra.Specification.Certs.html#7533}{\htmlId{11039}{\htmlClass{Generalizable}{\text{vDelegs}}}}\, \\ \,\href{Axiom.Set.Map.html#9262}{\htmlId{11049}{\htmlClass{Function}{\text{insertIfJust}}}}\, \,\href{Ledger.Dijkstra.Specification.Certs.html#7858}{\htmlId{11062}{\htmlClass{Generalizable}{\text{c}}}}\, \,\href{Ledger.Dijkstra.Specification.Certs.html#8044}{\htmlId{11064}{\htmlClass{Generalizable}{\text{mkh}}}}\, \,\href{Ledger.Dijkstra.Specification.Certs.html#7457}{\htmlId{11068}{\htmlClass{Generalizable}{\text{sDelegs}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#7389}{\htmlId{11078}{\htmlClass{Generalizable}{\text{rwds}}}}\, \,\href{Axiom.Set.Map.html#7640}{\htmlId{11083}{\htmlClass{Function Operator}{\text{∪ˡ}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{11086}{\htmlClass{Field Operator}{\text{❴}}}}\, \,\href{Ledger.Dijkstra.Specification.Certs.html#7858}{\htmlId{11088}{\htmlClass{Generalizable}{\text{c}}}}\, , \,\htmlId{11092}{\htmlClass{Number}{\text{0}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{11094}{\htmlClass{Field Operator}{\text{❵}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#7753}{\htmlId{11098}{\htmlClass{Generalizable}{\text{deposits}}}}\, \,\href{Axiom.Set.Map.Dec.html#2149}{\htmlId{11107}{\htmlClass{Function Operator}{\text{∪⁺}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{11110}{\htmlClass{Field Operator}{\text{❴}}}}\, \,\href{Ledger.Dijkstra.Specification.Certs.html#7858}{\htmlId{11112}{\htmlClass{Generalizable}{\text{c}}}}\, , \,\href{Ledger.Dijkstra.Specification.Certs.html#7837}{\htmlId{11116}{\htmlClass{Generalizable}{\text{d}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{11118}{\htmlClass{Field Operator}{\text{❵}}}}\, \end{pmatrix}$

  DELEG-dereg :
    ∙ (c , ) ∈ rwds
    ∙ (c , d) ∈ deposits
      ────────────────────────────────
      $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Certs.html#8106}{\htmlId{11232}{\htmlClass{Generalizable}{\text{pp}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#7571}{\htmlId{11237}{\htmlClass{Generalizable}{\text{pools}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#7918}{\htmlId{11245}{\htmlClass{Generalizable}{\text{delegatees}}}}\, \end{pmatrix}$ ⊢ $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Certs.html#7533}{\htmlId{11262}{\htmlClass{Generalizable}{\text{vDelegs}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#7457}{\htmlId{11272}{\htmlClass{Generalizable}{\text{sDelegs}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#7389}{\htmlId{11282}{\htmlClass{Generalizable}{\text{rwds}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#7753}{\htmlId{11289}{\htmlClass{Generalizable}{\text{deposits}}}}\, \end{pmatrix}$ ⇀⦇ dereg c d ,DELEG⦈ $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Certs.html#7533}{\htmlId{11323}{\htmlClass{Generalizable}{\text{vDelegs}}}}\, \,\href{Axiom.Set.Map.html#13606}{\htmlId{11331}{\htmlClass{Function Operator}{\text{∣}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{11333}{\htmlClass{Field Operator}{\text{❴}}}}\, \,\href{Ledger.Dijkstra.Specification.Certs.html#7858}{\htmlId{11335}{\htmlClass{Generalizable}{\text{c}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{11337}{\htmlClass{Field Operator}{\text{❵}}}}\, \,\href{Axiom.Set.Map.html#13606}{\htmlId{11339}{\htmlClass{Function Operator}{\text{ᶜ}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#7457}{\htmlId{11343}{\htmlClass{Generalizable}{\text{sDelegs}}}}\, \,\href{Axiom.Set.Map.html#13606}{\htmlId{11351}{\htmlClass{Function Operator}{\text{∣}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{11353}{\htmlClass{Field Operator}{\text{❴}}}}\, \,\href{Ledger.Dijkstra.Specification.Certs.html#7858}{\htmlId{11355}{\htmlClass{Generalizable}{\text{c}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{11357}{\htmlClass{Field Operator}{\text{❵}}}}\, \,\href{Axiom.Set.Map.html#13606}{\htmlId{11359}{\htmlClass{Function Operator}{\text{ᶜ}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#7389}{\htmlId{11363}{\htmlClass{Generalizable}{\text{rwds}}}}\, \,\href{Axiom.Set.Map.html#13606}{\htmlId{11368}{\htmlClass{Function Operator}{\text{∣}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{11370}{\htmlClass{Field Operator}{\text{❴}}}}\, \,\href{Ledger.Dijkstra.Specification.Certs.html#7858}{\htmlId{11372}{\htmlClass{Generalizable}{\text{c}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{11374}{\htmlClass{Field Operator}{\text{❵}}}}\, \,\href{Axiom.Set.Map.html#13606}{\htmlId{11376}{\htmlClass{Function Operator}{\text{ᶜ}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#7753}{\htmlId{11380}{\htmlClass{Generalizable}{\text{deposits}}}}\, \,\href{Axiom.Set.Map.html#13606}{\htmlId{11389}{\htmlClass{Function Operator}{\text{∣}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{11391}{\htmlClass{Field Operator}{\text{❴}}}}\, \,\href{Ledger.Dijkstra.Specification.Certs.html#7858}{\htmlId{11393}{\htmlClass{Generalizable}{\text{c}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{11395}{\htmlClass{Field Operator}{\text{❵}}}}\, \,\href{Axiom.Set.Map.html#13606}{\htmlId{11397}{\htmlClass{Function Operator}{\text{ᶜ}}}}\, \end{pmatrix}$

POOL Transition System

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

  POOL-reg :
    ∙ ¬ (IsPoolRegistered pools kh)
    ────────────────────────────────
    pp ⊢ $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Certs.html#7571}{\htmlId{11624}{\htmlClass{Generalizable}{\text{pools}}}}\,
         \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#7577}{\htmlId{11641}{\htmlClass{Generalizable}{\text{fPools}}}}\,
         \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#7604}{\htmlId{11659}{\htmlClass{Generalizable}{\text{retiring}}}}\,
         \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#7753}{\htmlId{11679}{\htmlClass{Generalizable}{\text{deposits}}}}\,
         \end{pmatrix}$ ⇀⦇ regpool kh poolParams ,POOL⦈ $\begin{pmatrix}
           \,\href{Ledger.Dijkstra.Specification.Certs.html#7571}{\htmlId{11744}{\htmlClass{Generalizable}{\text{pools}}}}\, \,\href{Axiom.Set.Map.html#7640}{\htmlId{11750}{\htmlClass{Function Operator}{\text{∪ˡ}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{11753}{\htmlClass{Field Operator}{\text{❴}}}}\, \,\href{Ledger.Dijkstra.Specification.Certs.html#8020}{\htmlId{11755}{\htmlClass{Generalizable}{\text{kh}}}}\, , \,\href{Ledger.Dijkstra.Specification.Certs.html#8074}{\htmlId{11760}{\htmlClass{Generalizable}{\text{poolParams}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{11771}{\htmlClass{Field Operator}{\text{❵}}}}\,
         \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#7577}{\htmlId{11784}{\htmlClass{Generalizable}{\text{fPools}}}}\,
         \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#7604}{\htmlId{11802}{\htmlClass{Generalizable}{\text{retiring}}}}\,
         \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#7753}{\htmlId{11822}{\htmlClass{Generalizable}{\text{deposits}}}}\, \,\href{Axiom.Set.Map.html#7640}{\htmlId{11831}{\htmlClass{Function Operator}{\text{∪ˡ}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{11834}{\htmlClass{Field Operator}{\text{❴}}}}\, \,\href{Ledger.Dijkstra.Specification.Certs.html#8020}{\htmlId{11836}{\htmlClass{Generalizable}{\text{kh}}}}\, , \,\href{Ledger.Dijkstra.Specification.Certs.html#8106}{\htmlId{11841}{\htmlClass{Generalizable}{\text{pp}}}}\, \,\htmlId{11844}{\htmlClass{Symbol}{\text{.}}}\,\,\href{Ledger.Dijkstra.Specification.PParams.html#3077}{\htmlId{11845}{\htmlClass{Field}{\text{poolDeposit}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{11857}{\htmlClass{Field Operator}{\text{❵}}}}\,
         \end{pmatrix}$

  POOL-rereg :
    ∙ IsPoolRegistered pools kh
    ────────────────────────────────
    pp ⊢ $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Certs.html#7571}{\htmlId{11966}{\htmlClass{Generalizable}{\text{pools}}}}\,
         \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#7577}{\htmlId{11983}{\htmlClass{Generalizable}{\text{fPools}}}}\,
         \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#7604}{\htmlId{12001}{\htmlClass{Generalizable}{\text{retiring}}}}\,
         \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#7753}{\htmlId{12021}{\htmlClass{Generalizable}{\text{deposits}}}}\,
         \end{pmatrix}$ ⇀⦇ regpool kh poolParams ,POOL⦈ $\begin{pmatrix}
           \,\href{Ledger.Dijkstra.Specification.Certs.html#7571}{\htmlId{12086}{\htmlClass{Generalizable}{\text{pools}}}}\,
         \\ \,\href{Class.HasSingleton.html#288}{\htmlId{12103}{\htmlClass{Field Operator}{\text{❴}}}}\, \,\href{Ledger.Dijkstra.Specification.Certs.html#8020}{\htmlId{12105}{\htmlClass{Generalizable}{\text{kh}}}}\, , \,\href{Ledger.Dijkstra.Specification.Certs.html#8074}{\htmlId{12110}{\htmlClass{Generalizable}{\text{poolParams}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{12121}{\htmlClass{Field Operator}{\text{❵}}}}\, \,\href{Axiom.Set.Map.html#7640}{\htmlId{12123}{\htmlClass{Function Operator}{\text{∪ˡ}}}}\, \,\href{Ledger.Dijkstra.Specification.Certs.html#7577}{\htmlId{12126}{\htmlClass{Generalizable}{\text{fPools}}}}\,
         \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#7604}{\htmlId{12144}{\htmlClass{Generalizable}{\text{retiring}}}}\, \,\href{Axiom.Set.Map.html#13606}{\htmlId{12153}{\htmlClass{Function Operator}{\text{∣}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{12155}{\htmlClass{Field Operator}{\text{❴}}}}\, \,\href{Ledger.Dijkstra.Specification.Certs.html#8020}{\htmlId{12157}{\htmlClass{Generalizable}{\text{kh}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{12160}{\htmlClass{Field Operator}{\text{❵}}}}\, \,\href{Axiom.Set.Map.html#13606}{\htmlId{12162}{\htmlClass{Function Operator}{\text{ᶜ}}}}\,
         \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#7753}{\htmlId{12175}{\htmlClass{Generalizable}{\text{deposits}}}}\,
         \end{pmatrix}$

  POOL-retirepool :
    ────────────────────────────────
    pp ⊢ $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Certs.html#7571}{\htmlId{12264}{\htmlClass{Generalizable}{\text{pools}}}}\,
         \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#7577}{\htmlId{12281}{\htmlClass{Generalizable}{\text{fPools}}}}\,
         \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#7604}{\htmlId{12299}{\htmlClass{Generalizable}{\text{retiring}}}}\,
         \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#7753}{\htmlId{12319}{\htmlClass{Generalizable}{\text{deposits}}}}\,
         \end{pmatrix}$ ⇀⦇ retirepool kh e ,POOL⦈ $\begin{pmatrix}
           \,\href{Ledger.Dijkstra.Specification.Certs.html#7571}{\htmlId{12378}{\htmlClass{Generalizable}{\text{pools}}}}\,
         \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#7577}{\htmlId{12395}{\htmlClass{Generalizable}{\text{fPools}}}}\,
         \\ \,\href{Class.HasSingleton.html#288}{\htmlId{12413}{\htmlClass{Field Operator}{\text{❴}}}}\, \,\href{Ledger.Dijkstra.Specification.Certs.html#8020}{\htmlId{12415}{\htmlClass{Generalizable}{\text{kh}}}}\, , \,\href{Ledger.Dijkstra.Specification.Certs.html#7969}{\htmlId{12420}{\htmlClass{Generalizable}{\text{e}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{12422}{\htmlClass{Field Operator}{\text{❵}}}}\, \,\href{Axiom.Set.Map.html#7640}{\htmlId{12424}{\htmlClass{Function Operator}{\text{∪ˡ}}}}\, \,\href{Ledger.Dijkstra.Specification.Certs.html#7604}{\htmlId{12427}{\htmlClass{Generalizable}{\text{retiring}}}}\,
         \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#7753}{\htmlId{12447}{\htmlClass{Generalizable}{\text{deposits}}}}\,
         \end{pmatrix}$

GOVCERT Transition System

data _⊢_⇀⦇_,GOVCERT⦈_ : CertEnv → GState → DCert → GState → Type where

  GOVCERT-regdrep :
    ∙ (d ≡ pp .drepDeposit × c ∉ dom dReps) ⊎ (d ≡  × c ∈ dom dReps)
      ────────────────────────────────
      $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Certs.html#7969}{\htmlId{12736}{\htmlClass{Generalizable}{\text{e}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#8106}{\htmlId{12740}{\htmlClass{Generalizable}{\text{pp}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#7991}{\htmlId{12745}{\htmlClass{Generalizable}{\text{vs}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#7640}{\htmlId{12750}{\htmlClass{Generalizable}{\text{wdrls}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#8220}{\htmlId{12758}{\htmlClass{Generalizable}{\text{cc}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#7679}{\htmlId{12763}{\htmlClass{Generalizable}{\text{dd}}}}\, \end{pmatrix}$ ⊢ $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Certs.html#7424}{\htmlId{12772}{\htmlClass{Generalizable}{\text{dReps}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#7496}{\htmlId{12780}{\htmlClass{Generalizable}{\text{ccKeys}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#7753}{\htmlId{12789}{\htmlClass{Generalizable}{\text{deposits}}}}\, \end{pmatrix}$ ⇀⦇ regdrep c d an ,GOVCERT⦈ $\begin{pmatrix} \,\href{Class.HasSingleton.html#288}{\htmlId{12830}{\htmlClass{Field Operator}{\text{❴}}}}\, \,\href{Ledger.Dijkstra.Specification.Certs.html#7858}{\htmlId{12832}{\htmlClass{Generalizable}{\text{c}}}}\, , \,\href{Ledger.Dijkstra.Specification.Certs.html#7969}{\htmlId{12836}{\htmlClass{Generalizable}{\text{e}}}}\, \,\href{Class.HasAdd.Core.html#162}{\htmlId{12838}{\htmlClass{Field Operator}{\text{+}}}}\, \,\href{Ledger.Dijkstra.Specification.Certs.html#8106}{\htmlId{12840}{\htmlClass{Generalizable}{\text{pp}}}}\, \,\htmlId{12843}{\htmlClass{Symbol}{\text{.}}}\,\,\href{Ledger.Dijkstra.Specification.PParams.html#4207}{\htmlId{12844}{\htmlClass{Field}{\text{drepActivity}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{12857}{\htmlClass{Field Operator}{\text{❵}}}}\, \,\href{Axiom.Set.Map.html#7640}{\htmlId{12859}{\htmlClass{Function Operator}{\text{∪ˡ}}}}\, \,\href{Ledger.Dijkstra.Specification.Certs.html#7424}{\htmlId{12862}{\htmlClass{Generalizable}{\text{dReps}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#7496}{\htmlId{12870}{\htmlClass{Generalizable}{\text{ccKeys}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#7753}{\htmlId{12879}{\htmlClass{Generalizable}{\text{deposits}}}}\, \,\href{Axiom.Set.Map.Dec.html#2149}{\htmlId{12888}{\htmlClass{Function Operator}{\text{∪⁺}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{12891}{\htmlClass{Field Operator}{\text{❴}}}}\, \,\href{Ledger.Dijkstra.Specification.Certs.html#7858}{\htmlId{12893}{\htmlClass{Generalizable}{\text{c}}}}\, , \,\href{Ledger.Dijkstra.Specification.Certs.html#7837}{\htmlId{12897}{\htmlClass{Generalizable}{\text{d}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{12899}{\htmlClass{Field Operator}{\text{❵}}}}\, \end{pmatrix}$

  GOVCERT-deregdrep :
    ∙ c ∈ dom dReps
    ∙ (c , d) ∈ deposits
      ────────────────────────────────
      $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Certs.html#7969}{\htmlId{13018}{\htmlClass{Generalizable}{\text{e}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#8106}{\htmlId{13022}{\htmlClass{Generalizable}{\text{pp}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#7991}{\htmlId{13027}{\htmlClass{Generalizable}{\text{vs}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#7640}{\htmlId{13032}{\htmlClass{Generalizable}{\text{wdrls}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#8220}{\htmlId{13040}{\htmlClass{Generalizable}{\text{cc}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#7679}{\htmlId{13045}{\htmlClass{Generalizable}{\text{dd}}}}\, \end{pmatrix}$ ⊢ $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Certs.html#7424}{\htmlId{13054}{\htmlClass{Generalizable}{\text{dReps}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#7496}{\htmlId{13062}{\htmlClass{Generalizable}{\text{ccKeys}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#7753}{\htmlId{13071}{\htmlClass{Generalizable}{\text{deposits}}}}\, \end{pmatrix}$ ⇀⦇ deregdrep c d ,GOVCERT⦈ $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Certs.html#7424}{\htmlId{13111}{\htmlClass{Generalizable}{\text{dReps}}}}\, \,\href{Axiom.Set.Map.html#13606}{\htmlId{13117}{\htmlClass{Function Operator}{\text{∣}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{13119}{\htmlClass{Field Operator}{\text{❴}}}}\, \,\href{Ledger.Dijkstra.Specification.Certs.html#7858}{\htmlId{13121}{\htmlClass{Generalizable}{\text{c}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{13123}{\htmlClass{Field Operator}{\text{❵}}}}\, \,\href{Axiom.Set.Map.html#13606}{\htmlId{13125}{\htmlClass{Function Operator}{\text{ᶜ}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#7496}{\htmlId{13129}{\htmlClass{Generalizable}{\text{ccKeys}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#7753}{\htmlId{13138}{\htmlClass{Generalizable}{\text{deposits}}}}\, \,\href{Axiom.Set.Map.html#13606}{\htmlId{13147}{\htmlClass{Function Operator}{\text{∣}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{13149}{\htmlClass{Field Operator}{\text{❴}}}}\, \,\href{Ledger.Dijkstra.Specification.Certs.html#7858}{\htmlId{13151}{\htmlClass{Generalizable}{\text{c}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{13153}{\htmlClass{Field Operator}{\text{❵}}}}\, \,\href{Axiom.Set.Map.html#13606}{\htmlId{13155}{\htmlClass{Function Operator}{\text{ᶜ}}}}\, \end{pmatrix}$

  GOVCERT-ccreghot :
    ∙ (c , nothing) ∉ ccKeys
    ∙ c ∈ cc
      ────────────────────────────────
      $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Certs.html#7969}{\htmlId{13270}{\htmlClass{Generalizable}{\text{e}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#8106}{\htmlId{13274}{\htmlClass{Generalizable}{\text{pp}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#7991}{\htmlId{13279}{\htmlClass{Generalizable}{\text{vs}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#7640}{\htmlId{13284}{\htmlClass{Generalizable}{\text{wdrls}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#8220}{\htmlId{13292}{\htmlClass{Generalizable}{\text{cc}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#7679}{\htmlId{13297}{\htmlClass{Generalizable}{\text{dd}}}}\, \end{pmatrix}$ ⊢ $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Certs.html#7424}{\htmlId{13306}{\htmlClass{Generalizable}{\text{dReps}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#7496}{\htmlId{13314}{\htmlClass{Generalizable}{\text{ccKeys}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#7753}{\htmlId{13323}{\htmlClass{Generalizable}{\text{deposits}}}}\, \end{pmatrix}$ ⇀⦇ ccreghot c mc ,GOVCERT⦈ $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Certs.html#7424}{\htmlId{13363}{\htmlClass{Generalizable}{\text{dReps}}}}\, \\ \,\href{Class.HasSingleton.html#288}{\htmlId{13371}{\htmlClass{Field Operator}{\text{❴}}}}\, \,\href{Ledger.Dijkstra.Specification.Certs.html#7858}{\htmlId{13373}{\htmlClass{Generalizable}{\text{c}}}}\, , \,\href{Ledger.Dijkstra.Specification.Certs.html#7885}{\htmlId{13377}{\htmlClass{Generalizable}{\text{mc}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{13380}{\htmlClass{Field Operator}{\text{❵}}}}\, \,\href{Axiom.Set.Map.html#7640}{\htmlId{13382}{\htmlClass{Function Operator}{\text{∪ˡ}}}}\, \,\href{Ledger.Dijkstra.Specification.Certs.html#7496}{\htmlId{13385}{\htmlClass{Generalizable}{\text{ccKeys}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#7753}{\htmlId{13394}{\htmlClass{Generalizable}{\text{deposits}}}}\, \end{pmatrix}$

CERT Transition System

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

  CERT-deleg :
    ∙ $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Certs.html#8106}{\htmlId{13560}{\htmlClass{Generalizable}{\text{pp}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#2747}{\htmlId{13565}{\htmlClass{Field}{\text{PState.pools}}}}\, \,\href{Ledger.Dijkstra.Specification.Certs.html#8200}{\htmlId{13578}{\htmlClass{Generalizable}{\text{stᵖ}}}}\, \\ \,\href{Class.IsSet.html#916}{\htmlId{13584}{\htmlClass{Function}{\text{dom}}}}\, \,\htmlId{13588}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Dijkstra.Specification.Certs.html#2913}{\htmlId{13589}{\htmlClass{Field}{\text{GState.dreps}}}}\, \,\href{Ledger.Dijkstra.Specification.Certs.html#8180}{\htmlId{13602}{\htmlClass{Generalizable}{\text{stᵍ}}}}\,\,\htmlId{13605}{\htmlClass{Symbol}{\text{)}}}\, \end{pmatrix}$ ⊢ stᵈ ⇀⦇ dCert ,DELEG⦈ stᵈ'
      ────────────────────────────────
      $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Certs.html#7969}{\htmlId{13684}{\htmlClass{Generalizable}{\text{e}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#8106}{\htmlId{13688}{\htmlClass{Generalizable}{\text{pp}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#7991}{\htmlId{13693}{\htmlClass{Generalizable}{\text{vs}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#7640}{\htmlId{13698}{\htmlClass{Generalizable}{\text{wdrls}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#8220}{\htmlId{13706}{\htmlClass{Generalizable}{\text{cc}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#7679}{\htmlId{13711}{\htmlClass{Generalizable}{\text{dd}}}}\, \end{pmatrix}$ ⊢ $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Certs.html#8160}{\htmlId{13720}{\htmlClass{Generalizable}{\text{stᵈ}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#8200}{\htmlId{13726}{\htmlClass{Generalizable}{\text{stᵖ}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#8180}{\htmlId{13732}{\htmlClass{Generalizable}{\text{stᵍ}}}}\, \end{pmatrix}$ ⇀⦇ dCert ,CERT⦈ $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Certs.html#8164}{\htmlId{13756}{\htmlClass{Generalizable}{\text{stᵈ'}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#8200}{\htmlId{13763}{\htmlClass{Generalizable}{\text{stᵖ}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#8180}{\htmlId{13769}{\htmlClass{Generalizable}{\text{stᵍ}}}}\, \end{pmatrix}$

  CERT-pool :
    ∙ pp ⊢ stᵖ ⇀⦇ dCert ,POOL⦈ stᵖ'
      ────────────────────────────────
      $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Certs.html#7969}{\htmlId{13873}{\htmlClass{Generalizable}{\text{e}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#8106}{\htmlId{13877}{\htmlClass{Generalizable}{\text{pp}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#7991}{\htmlId{13882}{\htmlClass{Generalizable}{\text{vs}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#7640}{\htmlId{13887}{\htmlClass{Generalizable}{\text{wdrls}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#8220}{\htmlId{13895}{\htmlClass{Generalizable}{\text{cc}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#7679}{\htmlId{13900}{\htmlClass{Generalizable}{\text{dd}}}}\, \end{pmatrix}$ ⊢ $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Certs.html#8160}{\htmlId{13909}{\htmlClass{Generalizable}{\text{stᵈ}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#8200}{\htmlId{13915}{\htmlClass{Generalizable}{\text{stᵖ}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#8180}{\htmlId{13921}{\htmlClass{Generalizable}{\text{stᵍ}}}}\, \end{pmatrix}$ ⇀⦇ dCert ,CERT⦈ $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Certs.html#8160}{\htmlId{13945}{\htmlClass{Generalizable}{\text{stᵈ}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#8204}{\htmlId{13951}{\htmlClass{Generalizable}{\text{stᵖ'}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#8180}{\htmlId{13958}{\htmlClass{Generalizable}{\text{stᵍ}}}}\, \end{pmatrix}$

  CERT-gov :
    ∙ Γ ⊢ stᵍ ⇀⦇ dCert ,GOVCERT⦈ stᵍ'
      ────────────────────────────────
      Γ ⊢ $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Certs.html#8160}{\htmlId{14067}{\htmlClass{Generalizable}{\text{stᵈ}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#8200}{\htmlId{14073}{\htmlClass{Generalizable}{\text{stᵖ}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#8180}{\htmlId{14079}{\htmlClass{Generalizable}{\text{stᵍ}}}}\, \end{pmatrix}$ ⇀⦇ dCert ,CERT⦈ $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Certs.html#8160}{\htmlId{14103}{\htmlClass{Generalizable}{\text{stᵈ}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#8200}{\htmlId{14109}{\htmlClass{Generalizable}{\text{stᵖ}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#8184}{\htmlId{14115}{\htmlClass{Generalizable}{\text{stᵍ'}}}}\, \end{pmatrix}$

CERTS Transition System

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