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 → Maybe Coin → DCert
  regpool     : KeyHash → StakePoolParams → DCert
  retirepool  : KeyHash → Epoch → DCert
  regdrep     : Credential → Coin → Anchor → DCert
  deregdrep   : Credential → Coin → DCert
  ccreghot    : Credential → Maybe Credential → DCert

cwitness : DCert → Maybe Credential
cwitness (delegate c _ _ _)  = just c
cwitness (dereg c _)         = just c
cwitness (regpool kh _)      = just $ KeyHashObj kh
cwitness (retirepool kh _)   = just $ KeyHashObj kh
cwitness (regdrep c _ _)     = just c
cwitness (deregdrep c _)     = just c
cwitness (ccreghot c _)      = just c

-- 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
  md          : Maybe Coin
  c           : Credential
  mc          : Maybe Credential
  delegatees  : ℙ Credential
  dCert       : DCert
  e           : Epoch
  vs          : List GovVote
  kh          : KeyHash
  mkh         : Maybe KeyHash
  poolParams  : StakePoolParams
  pp          : PParams
  mvd         : Maybe VDeleg

  stᵈ stᵈ' : DState
  stᵍ stᵍ' : GState
  stᵖ stᵖ' : PState
  cc : ℙ Credential

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

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

  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#8059}{\htmlId{9089}{\htmlClass{Generalizable}{\text{pp}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#7497}{\htmlId{9094}{\htmlClass{Generalizable}{\text{pools}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#7871}{\htmlId{9102}{\htmlClass{Generalizable}{\text{delegatees}}}}\, \end{pmatrix}$ ⊢ $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Certs.html#7459}{\htmlId{9119}{\htmlClass{Generalizable}{\text{vDelegs}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#7383}{\htmlId{9129}{\htmlClass{Generalizable}{\text{sDelegs}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#7315}{\htmlId{9139}{\htmlClass{Generalizable}{\text{rwds}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#7679}{\htmlId{9146}{\htmlClass{Generalizable}{\text{deposits}}}}\, \end{pmatrix}$ ⇀⦇ delegate c mvd mkh d ,DELEG⦈ $\begin{pmatrix} \,\href{Axiom.Set.Map.html#9262}{\htmlId{9191}{\htmlClass{Function}{\text{insertIfJust}}}}\, \,\href{Ledger.Dijkstra.Specification.Certs.html#7811}{\htmlId{9204}{\htmlClass{Generalizable}{\text{c}}}}\, \,\href{Ledger.Dijkstra.Specification.Certs.html#8083}{\htmlId{9206}{\htmlClass{Generalizable}{\text{mvd}}}}\, \,\href{Ledger.Dijkstra.Specification.Certs.html#7459}{\htmlId{9210}{\htmlClass{Generalizable}{\text{vDelegs}}}}\, \\ \,\href{Axiom.Set.Map.html#9262}{\htmlId{9220}{\htmlClass{Function}{\text{insertIfJust}}}}\, \,\href{Ledger.Dijkstra.Specification.Certs.html#7811}{\htmlId{9233}{\htmlClass{Generalizable}{\text{c}}}}\, \,\href{Ledger.Dijkstra.Specification.Certs.html#7997}{\htmlId{9235}{\htmlClass{Generalizable}{\text{mkh}}}}\, \,\href{Ledger.Dijkstra.Specification.Certs.html#7383}{\htmlId{9239}{\htmlClass{Generalizable}{\text{sDelegs}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#7315}{\htmlId{9249}{\htmlClass{Generalizable}{\text{rwds}}}}\, \,\href{Axiom.Set.Map.html#7640}{\htmlId{9254}{\htmlClass{Function Operator}{\text{∪ˡ}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{9257}{\htmlClass{Field Operator}{\text{❴}}}}\, \,\href{Ledger.Dijkstra.Specification.Certs.html#7811}{\htmlId{9259}{\htmlClass{Generalizable}{\text{c}}}}\, , \,\htmlId{9263}{\htmlClass{Number}{\text{0}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{9265}{\htmlClass{Field Operator}{\text{❵}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#7679}{\htmlId{9269}{\htmlClass{Generalizable}{\text{deposits}}}}\, \,\href{Axiom.Set.Map.Dec.html#2149}{\htmlId{9278}{\htmlClass{Function Operator}{\text{∪⁺}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{9281}{\htmlClass{Field Operator}{\text{❴}}}}\, \,\href{Ledger.Dijkstra.Specification.Certs.html#7811}{\htmlId{9283}{\htmlClass{Generalizable}{\text{c}}}}\, , \,\href{Ledger.Dijkstra.Specification.Certs.html#7763}{\htmlId{9287}{\htmlClass{Generalizable}{\text{d}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{9289}{\htmlClass{Field Operator}{\text{❵}}}}\, \end{pmatrix}$

  DELEG-dereg :
    ∙ (c , ) ∈ rwds
    ∙ (c , d) ∈ deposits
    ∙ md ≡ nothing ⊎ md ≡ just d
      ────────────────────────────────
      $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Certs.html#8059}{\htmlId{9436}{\htmlClass{Generalizable}{\text{pp}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#7497}{\htmlId{9441}{\htmlClass{Generalizable}{\text{pools}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#7871}{\htmlId{9449}{\htmlClass{Generalizable}{\text{delegatees}}}}\, \end{pmatrix}$ ⊢ $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Certs.html#7459}{\htmlId{9466}{\htmlClass{Generalizable}{\text{vDelegs}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#7383}{\htmlId{9476}{\htmlClass{Generalizable}{\text{sDelegs}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#7315}{\htmlId{9486}{\htmlClass{Generalizable}{\text{rwds}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#7679}{\htmlId{9493}{\htmlClass{Generalizable}{\text{deposits}}}}\, \end{pmatrix}$ ⇀⦇ dereg c md ,DELEG⦈ $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Certs.html#7459}{\htmlId{9528}{\htmlClass{Generalizable}{\text{vDelegs}}}}\, \,\href{Axiom.Set.Map.html#13606}{\htmlId{9536}{\htmlClass{Function Operator}{\text{∣}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{9538}{\htmlClass{Field Operator}{\text{❴}}}}\, \,\href{Ledger.Dijkstra.Specification.Certs.html#7811}{\htmlId{9540}{\htmlClass{Generalizable}{\text{c}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{9542}{\htmlClass{Field Operator}{\text{❵}}}}\, \,\href{Axiom.Set.Map.html#13606}{\htmlId{9544}{\htmlClass{Function Operator}{\text{ᶜ}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#7383}{\htmlId{9548}{\htmlClass{Generalizable}{\text{sDelegs}}}}\, \,\href{Axiom.Set.Map.html#13606}{\htmlId{9556}{\htmlClass{Function Operator}{\text{∣}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{9558}{\htmlClass{Field Operator}{\text{❴}}}}\, \,\href{Ledger.Dijkstra.Specification.Certs.html#7811}{\htmlId{9560}{\htmlClass{Generalizable}{\text{c}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{9562}{\htmlClass{Field Operator}{\text{❵}}}}\, \,\href{Axiom.Set.Map.html#13606}{\htmlId{9564}{\htmlClass{Function Operator}{\text{ᶜ}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#7315}{\htmlId{9568}{\htmlClass{Generalizable}{\text{rwds}}}}\, \,\href{Axiom.Set.Map.html#13606}{\htmlId{9573}{\htmlClass{Function Operator}{\text{∣}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{9575}{\htmlClass{Field Operator}{\text{❴}}}}\, \,\href{Ledger.Dijkstra.Specification.Certs.html#7811}{\htmlId{9577}{\htmlClass{Generalizable}{\text{c}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{9579}{\htmlClass{Field Operator}{\text{❵}}}}\, \,\href{Axiom.Set.Map.html#13606}{\htmlId{9581}{\htmlClass{Function Operator}{\text{ᶜ}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#7679}{\htmlId{9585}{\htmlClass{Generalizable}{\text{deposits}}}}\, \,\href{Axiom.Set.Map.html#13606}{\htmlId{9594}{\htmlClass{Function Operator}{\text{∣}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{9596}{\htmlClass{Field Operator}{\text{❴}}}}\, \,\href{Ledger.Dijkstra.Specification.Certs.html#7811}{\htmlId{9598}{\htmlClass{Generalizable}{\text{c}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{9600}{\htmlClass{Field Operator}{\text{❵}}}}\, \,\href{Axiom.Set.Map.html#13606}{\htmlId{9602}{\htmlClass{Function Operator}{\text{ᶜ}}}}\, \end{pmatrix}$


isPoolRegistered : Pools -> KeyHash -> Maybe StakePoolParams
isPoolRegistered ps kh = lookupᵐ? ps kh

POOL Transition System

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

  POOL-reg :
    ∙ Is-nothing (isPoolRegistered pools kh)
    ────────────────────────────────
    pp ⊢ $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Certs.html#7497}{\htmlId{9941}{\htmlClass{Generalizable}{\text{pools}}}}\,
         \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#7503}{\htmlId{9958}{\htmlClass{Generalizable}{\text{fPools}}}}\,
         \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#7530}{\htmlId{9976}{\htmlClass{Generalizable}{\text{retiring}}}}\,
         \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#7679}{\htmlId{9996}{\htmlClass{Generalizable}{\text{deposits}}}}\,
         \end{pmatrix}$ ⇀⦇ regpool kh poolParams ,POOL⦈ $\begin{pmatrix}
           \,\href{Ledger.Dijkstra.Specification.Certs.html#7497}{\htmlId{10061}{\htmlClass{Generalizable}{\text{pools}}}}\, \,\href{Axiom.Set.Map.html#7640}{\htmlId{10067}{\htmlClass{Function Operator}{\text{∪ˡ}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{10070}{\htmlClass{Field Operator}{\text{❴}}}}\, \,\href{Ledger.Dijkstra.Specification.Certs.html#7973}{\htmlId{10072}{\htmlClass{Generalizable}{\text{kh}}}}\, , \,\href{Ledger.Dijkstra.Specification.Certs.html#8027}{\htmlId{10077}{\htmlClass{Generalizable}{\text{poolParams}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{10088}{\htmlClass{Field Operator}{\text{❵}}}}\,
         \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#7503}{\htmlId{10101}{\htmlClass{Generalizable}{\text{fPools}}}}\,
         \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#7530}{\htmlId{10119}{\htmlClass{Generalizable}{\text{retiring}}}}\,
         \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#7679}{\htmlId{10139}{\htmlClass{Generalizable}{\text{deposits}}}}\, \,\href{Axiom.Set.Map.html#7640}{\htmlId{10148}{\htmlClass{Function Operator}{\text{∪ˡ}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{10151}{\htmlClass{Field Operator}{\text{❴}}}}\, \,\href{Ledger.Dijkstra.Specification.Certs.html#7973}{\htmlId{10153}{\htmlClass{Generalizable}{\text{kh}}}}\, , \,\href{Ledger.Dijkstra.Specification.Certs.html#8059}{\htmlId{10158}{\htmlClass{Generalizable}{\text{pp}}}}\, \,\htmlId{10161}{\htmlClass{Symbol}{\text{.}}}\,\,\href{Ledger.Dijkstra.Specification.PParams.html#3077}{\htmlId{10162}{\htmlClass{Field}{\text{poolDeposit}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{10174}{\htmlClass{Field Operator}{\text{❵}}}}\,
         \end{pmatrix}$

  POOL-rereg :
    ∙ Is-just (isPoolRegistered pools kh)
    ────────────────────────────────
    pp ⊢ $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Certs.html#7497}{\htmlId{10293}{\htmlClass{Generalizable}{\text{pools}}}}\,
         \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#7503}{\htmlId{10310}{\htmlClass{Generalizable}{\text{fPools}}}}\,
         \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#7530}{\htmlId{10328}{\htmlClass{Generalizable}{\text{retiring}}}}\,
         \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#7679}{\htmlId{10348}{\htmlClass{Generalizable}{\text{deposits}}}}\,
         \end{pmatrix}$ ⇀⦇ regpool kh poolParams ,POOL⦈ $\begin{pmatrix}
           \,\href{Ledger.Dijkstra.Specification.Certs.html#7497}{\htmlId{10413}{\htmlClass{Generalizable}{\text{pools}}}}\,
         \\ \,\href{Class.HasSingleton.html#288}{\htmlId{10430}{\htmlClass{Field Operator}{\text{❴}}}}\, \,\href{Ledger.Dijkstra.Specification.Certs.html#7973}{\htmlId{10432}{\htmlClass{Generalizable}{\text{kh}}}}\, , \,\href{Ledger.Dijkstra.Specification.Certs.html#8027}{\htmlId{10437}{\htmlClass{Generalizable}{\text{poolParams}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{10448}{\htmlClass{Field Operator}{\text{❵}}}}\, \,\href{Axiom.Set.Map.html#7640}{\htmlId{10450}{\htmlClass{Function Operator}{\text{∪ˡ}}}}\, \,\href{Ledger.Dijkstra.Specification.Certs.html#7503}{\htmlId{10453}{\htmlClass{Generalizable}{\text{fPools}}}}\,
         \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#7530}{\htmlId{10471}{\htmlClass{Generalizable}{\text{retiring}}}}\, \,\href{Axiom.Set.Map.html#13606}{\htmlId{10480}{\htmlClass{Function Operator}{\text{∣}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{10482}{\htmlClass{Field Operator}{\text{❴}}}}\, \,\href{Ledger.Dijkstra.Specification.Certs.html#7973}{\htmlId{10484}{\htmlClass{Generalizable}{\text{kh}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{10487}{\htmlClass{Field Operator}{\text{❵}}}}\, \,\href{Axiom.Set.Map.html#13606}{\htmlId{10489}{\htmlClass{Function Operator}{\text{ᶜ}}}}\,
         \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#7679}{\htmlId{10502}{\htmlClass{Generalizable}{\text{deposits}}}}\,
         \end{pmatrix}$

  POOL-retirepool :
    ────────────────────────────────
    pp ⊢ $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Certs.html#7497}{\htmlId{10591}{\htmlClass{Generalizable}{\text{pools}}}}\,
         \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#7503}{\htmlId{10608}{\htmlClass{Generalizable}{\text{fPools}}}}\,
         \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#7530}{\htmlId{10626}{\htmlClass{Generalizable}{\text{retiring}}}}\,
         \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#7679}{\htmlId{10646}{\htmlClass{Generalizable}{\text{deposits}}}}\,
         \end{pmatrix}$ ⇀⦇ retirepool kh e ,POOL⦈ $\begin{pmatrix}
           \,\href{Ledger.Dijkstra.Specification.Certs.html#7497}{\htmlId{10705}{\htmlClass{Generalizable}{\text{pools}}}}\,
         \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#7503}{\htmlId{10722}{\htmlClass{Generalizable}{\text{fPools}}}}\,
         \\ \,\href{Class.HasSingleton.html#288}{\htmlId{10740}{\htmlClass{Field Operator}{\text{❴}}}}\, \,\href{Ledger.Dijkstra.Specification.Certs.html#7973}{\htmlId{10742}{\htmlClass{Generalizable}{\text{kh}}}}\, , \,\href{Ledger.Dijkstra.Specification.Certs.html#7922}{\htmlId{10747}{\htmlClass{Generalizable}{\text{e}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{10749}{\htmlClass{Field Operator}{\text{❵}}}}\, \,\href{Axiom.Set.Map.html#7640}{\htmlId{10751}{\htmlClass{Function Operator}{\text{∪ˡ}}}}\, \,\href{Ledger.Dijkstra.Specification.Certs.html#7530}{\htmlId{10754}{\htmlClass{Generalizable}{\text{retiring}}}}\,
         \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#7679}{\htmlId{10774}{\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#7922}{\htmlId{11063}{\htmlClass{Generalizable}{\text{e}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#8059}{\htmlId{11067}{\htmlClass{Generalizable}{\text{pp}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#7944}{\htmlId{11072}{\htmlClass{Generalizable}{\text{vs}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#7566}{\htmlId{11077}{\htmlClass{Generalizable}{\text{wdrls}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#8173}{\htmlId{11085}{\htmlClass{Generalizable}{\text{cc}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#7605}{\htmlId{11090}{\htmlClass{Generalizable}{\text{dd}}}}\, \end{pmatrix}$ ⊢ $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Certs.html#7350}{\htmlId{11099}{\htmlClass{Generalizable}{\text{dReps}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#7422}{\htmlId{11107}{\htmlClass{Generalizable}{\text{ccKeys}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#7679}{\htmlId{11116}{\htmlClass{Generalizable}{\text{deposits}}}}\, \end{pmatrix}$ ⇀⦇ regdrep c d an ,GOVCERT⦈ $\begin{pmatrix} \,\href{Class.HasSingleton.html#288}{\htmlId{11157}{\htmlClass{Field Operator}{\text{❴}}}}\, \,\href{Ledger.Dijkstra.Specification.Certs.html#7811}{\htmlId{11159}{\htmlClass{Generalizable}{\text{c}}}}\, , \,\href{Ledger.Dijkstra.Specification.Certs.html#7922}{\htmlId{11163}{\htmlClass{Generalizable}{\text{e}}}}\, \,\href{Class.HasAdd.Core.html#162}{\htmlId{11165}{\htmlClass{Field Operator}{\text{+}}}}\, \,\href{Ledger.Dijkstra.Specification.Certs.html#8059}{\htmlId{11167}{\htmlClass{Generalizable}{\text{pp}}}}\, \,\htmlId{11170}{\htmlClass{Symbol}{\text{.}}}\,\,\href{Ledger.Dijkstra.Specification.PParams.html#4207}{\htmlId{11171}{\htmlClass{Field}{\text{drepActivity}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{11184}{\htmlClass{Field Operator}{\text{❵}}}}\, \,\href{Axiom.Set.Map.html#7640}{\htmlId{11186}{\htmlClass{Function Operator}{\text{∪ˡ}}}}\, \,\href{Ledger.Dijkstra.Specification.Certs.html#7350}{\htmlId{11189}{\htmlClass{Generalizable}{\text{dReps}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#7422}{\htmlId{11197}{\htmlClass{Generalizable}{\text{ccKeys}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#7679}{\htmlId{11206}{\htmlClass{Generalizable}{\text{deposits}}}}\, \,\href{Axiom.Set.Map.Dec.html#2149}{\htmlId{11215}{\htmlClass{Function Operator}{\text{∪⁺}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{11218}{\htmlClass{Field Operator}{\text{❴}}}}\, \,\href{Ledger.Dijkstra.Specification.Certs.html#7811}{\htmlId{11220}{\htmlClass{Generalizable}{\text{c}}}}\, , \,\href{Ledger.Dijkstra.Specification.Certs.html#7763}{\htmlId{11224}{\htmlClass{Generalizable}{\text{d}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{11226}{\htmlClass{Field Operator}{\text{❵}}}}\, \end{pmatrix}$

  GOVCERT-deregdrep :
    ∙ c ∈ dom dReps
    ∙ (c , d) ∈ deposits
      ────────────────────────────────
      $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Certs.html#7922}{\htmlId{11345}{\htmlClass{Generalizable}{\text{e}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#8059}{\htmlId{11349}{\htmlClass{Generalizable}{\text{pp}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#7944}{\htmlId{11354}{\htmlClass{Generalizable}{\text{vs}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#7566}{\htmlId{11359}{\htmlClass{Generalizable}{\text{wdrls}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#8173}{\htmlId{11367}{\htmlClass{Generalizable}{\text{cc}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#7605}{\htmlId{11372}{\htmlClass{Generalizable}{\text{dd}}}}\, \end{pmatrix}$ ⊢ $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Certs.html#7350}{\htmlId{11381}{\htmlClass{Generalizable}{\text{dReps}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#7422}{\htmlId{11389}{\htmlClass{Generalizable}{\text{ccKeys}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#7679}{\htmlId{11398}{\htmlClass{Generalizable}{\text{deposits}}}}\, \end{pmatrix}$ ⇀⦇ deregdrep c d ,GOVCERT⦈ $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Certs.html#7350}{\htmlId{11438}{\htmlClass{Generalizable}{\text{dReps}}}}\, \,\href{Axiom.Set.Map.html#13606}{\htmlId{11444}{\htmlClass{Function Operator}{\text{∣}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{11446}{\htmlClass{Field Operator}{\text{❴}}}}\, \,\href{Ledger.Dijkstra.Specification.Certs.html#7811}{\htmlId{11448}{\htmlClass{Generalizable}{\text{c}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{11450}{\htmlClass{Field Operator}{\text{❵}}}}\, \,\href{Axiom.Set.Map.html#13606}{\htmlId{11452}{\htmlClass{Function Operator}{\text{ᶜ}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#7422}{\htmlId{11456}{\htmlClass{Generalizable}{\text{ccKeys}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#7679}{\htmlId{11465}{\htmlClass{Generalizable}{\text{deposits}}}}\, \,\href{Axiom.Set.Map.html#13606}{\htmlId{11474}{\htmlClass{Function Operator}{\text{∣}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{11476}{\htmlClass{Field Operator}{\text{❴}}}}\, \,\href{Ledger.Dijkstra.Specification.Certs.html#7811}{\htmlId{11478}{\htmlClass{Generalizable}{\text{c}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{11480}{\htmlClass{Field Operator}{\text{❵}}}}\, \,\href{Axiom.Set.Map.html#13606}{\htmlId{11482}{\htmlClass{Function Operator}{\text{ᶜ}}}}\, \end{pmatrix}$

  GOVCERT-ccreghot :
    ∙ (c , nothing) ∉ ccKeys
    ∙ c ∈ cc
      ────────────────────────────────
      $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Certs.html#7922}{\htmlId{11597}{\htmlClass{Generalizable}{\text{e}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#8059}{\htmlId{11601}{\htmlClass{Generalizable}{\text{pp}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#7944}{\htmlId{11606}{\htmlClass{Generalizable}{\text{vs}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#7566}{\htmlId{11611}{\htmlClass{Generalizable}{\text{wdrls}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#8173}{\htmlId{11619}{\htmlClass{Generalizable}{\text{cc}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#7605}{\htmlId{11624}{\htmlClass{Generalizable}{\text{dd}}}}\, \end{pmatrix}$ ⊢ $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Certs.html#7350}{\htmlId{11633}{\htmlClass{Generalizable}{\text{dReps}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#7422}{\htmlId{11641}{\htmlClass{Generalizable}{\text{ccKeys}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#7679}{\htmlId{11650}{\htmlClass{Generalizable}{\text{deposits}}}}\, \end{pmatrix}$ ⇀⦇ ccreghot c mc ,GOVCERT⦈ $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Certs.html#7350}{\htmlId{11690}{\htmlClass{Generalizable}{\text{dReps}}}}\, \\ \,\href{Class.HasSingleton.html#288}{\htmlId{11698}{\htmlClass{Field Operator}{\text{❴}}}}\, \,\href{Ledger.Dijkstra.Specification.Certs.html#7811}{\htmlId{11700}{\htmlClass{Generalizable}{\text{c}}}}\, , \,\href{Ledger.Dijkstra.Specification.Certs.html#7838}{\htmlId{11704}{\htmlClass{Generalizable}{\text{mc}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{11707}{\htmlClass{Field Operator}{\text{❵}}}}\, \,\href{Axiom.Set.Map.html#7640}{\htmlId{11709}{\htmlClass{Function Operator}{\text{∪ˡ}}}}\, \,\href{Ledger.Dijkstra.Specification.Certs.html#7422}{\htmlId{11712}{\htmlClass{Generalizable}{\text{ccKeys}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#7679}{\htmlId{11721}{\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#8059}{\htmlId{11887}{\htmlClass{Generalizable}{\text{pp}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#2673}{\htmlId{11892}{\htmlClass{Field}{\text{PState.pools}}}}\, \,\href{Ledger.Dijkstra.Specification.Certs.html#8153}{\htmlId{11905}{\htmlClass{Generalizable}{\text{stᵖ}}}}\, \\ \,\href{Class.IsSet.html#916}{\htmlId{11911}{\htmlClass{Function}{\text{dom}}}}\, \,\htmlId{11915}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Dijkstra.Specification.Certs.html#2839}{\htmlId{11916}{\htmlClass{Field}{\text{GState.dreps}}}}\, \,\href{Ledger.Dijkstra.Specification.Certs.html#8133}{\htmlId{11929}{\htmlClass{Generalizable}{\text{stᵍ}}}}\,\,\htmlId{11932}{\htmlClass{Symbol}{\text{)}}}\, \end{pmatrix}$ ⊢ stᵈ ⇀⦇ dCert ,DELEG⦈ stᵈ'
      ────────────────────────────────
      $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Certs.html#7922}{\htmlId{12011}{\htmlClass{Generalizable}{\text{e}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#8059}{\htmlId{12015}{\htmlClass{Generalizable}{\text{pp}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#7944}{\htmlId{12020}{\htmlClass{Generalizable}{\text{vs}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#7566}{\htmlId{12025}{\htmlClass{Generalizable}{\text{wdrls}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#8173}{\htmlId{12033}{\htmlClass{Generalizable}{\text{cc}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#7605}{\htmlId{12038}{\htmlClass{Generalizable}{\text{dd}}}}\, \end{pmatrix}$ ⊢ $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Certs.html#8113}{\htmlId{12047}{\htmlClass{Generalizable}{\text{stᵈ}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#8153}{\htmlId{12053}{\htmlClass{Generalizable}{\text{stᵖ}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#8133}{\htmlId{12059}{\htmlClass{Generalizable}{\text{stᵍ}}}}\, \end{pmatrix}$ ⇀⦇ dCert ,CERT⦈ $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Certs.html#8117}{\htmlId{12083}{\htmlClass{Generalizable}{\text{stᵈ'}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#8153}{\htmlId{12090}{\htmlClass{Generalizable}{\text{stᵖ}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#8133}{\htmlId{12096}{\htmlClass{Generalizable}{\text{stᵍ}}}}\, \end{pmatrix}$

  CERT-pool :
    ∙ pp ⊢ stᵖ ⇀⦇ dCert ,POOL⦈ stᵖ'
      ────────────────────────────────
      $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Certs.html#7922}{\htmlId{12200}{\htmlClass{Generalizable}{\text{e}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#8059}{\htmlId{12204}{\htmlClass{Generalizable}{\text{pp}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#7944}{\htmlId{12209}{\htmlClass{Generalizable}{\text{vs}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#7566}{\htmlId{12214}{\htmlClass{Generalizable}{\text{wdrls}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#8173}{\htmlId{12222}{\htmlClass{Generalizable}{\text{cc}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#7605}{\htmlId{12227}{\htmlClass{Generalizable}{\text{dd}}}}\, \end{pmatrix}$ ⊢ $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Certs.html#8113}{\htmlId{12236}{\htmlClass{Generalizable}{\text{stᵈ}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#8153}{\htmlId{12242}{\htmlClass{Generalizable}{\text{stᵖ}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#8133}{\htmlId{12248}{\htmlClass{Generalizable}{\text{stᵍ}}}}\, \end{pmatrix}$ ⇀⦇ dCert ,CERT⦈ $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Certs.html#8113}{\htmlId{12272}{\htmlClass{Generalizable}{\text{stᵈ}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#8157}{\htmlId{12278}{\htmlClass{Generalizable}{\text{stᵖ'}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#8133}{\htmlId{12285}{\htmlClass{Generalizable}{\text{stᵍ}}}}\, \end{pmatrix}$

  CERT-gov :
    ∙ Γ ⊢ stᵍ ⇀⦇ dCert ,GOVCERT⦈ stᵍ'
      ────────────────────────────────
      Γ ⊢ $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Certs.html#8113}{\htmlId{12394}{\htmlClass{Generalizable}{\text{stᵈ}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#8153}{\htmlId{12400}{\htmlClass{Generalizable}{\text{stᵖ}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#8133}{\htmlId{12406}{\htmlClass{Generalizable}{\text{stᵍ}}}}\, \end{pmatrix}$ ⇀⦇ dCert ,CERT⦈ $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Certs.html#8113}{\htmlId{12430}{\htmlClass{Generalizable}{\text{stᵈ}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#8153}{\htmlId{12436}{\htmlClass{Generalizable}{\text{stᵖ}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#8137}{\htmlId{12442}{\htmlClass{Generalizable}{\text{stᵍ'}}}}\, \end{pmatrix}$

CERTS Transition System

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