Ledger.Conway.Certs

{-# OPTIONS --safe #-}

open import Ledger.Prelude renaming (filterˢ to filter)
open import Ledger.Conway.Gov.Base
open import Ledger.Conway.Types.Numeric.UnitInterval

module Ledger.Conway.Certs (gs : _) (open GovStructure gs) where


open import Ledger.Conway.Gov.Actions gs
open RwdAddr
open PParams


data DepositPurpose : Type where
  CredentialDeposit  : Credential   → DepositPurpose
  PoolDeposit        : KeyHash      → DepositPurpose
  DRepDeposit        : Credential   → DepositPurpose
  GovActionDeposit   : GovActionID  → DepositPurpose

Deposits  = DepositPurpose ⇀ Coin
Rewards   = Credential ⇀ Coin
DReps     = Credential ⇀ Epoch


record HasDeposits {a} (A : Type a) : Type a where
  field DepositsOf : A → Deposits
open HasDeposits ⦃...⦄ public

record HasRewards {a} (A : Type a) : Type a where
  field RewardsOf : A → Rewards
open HasRewards  ⦃...⦄ public

record HasDReps {a} (A : Type a) : Type a where
  field DRepsOf : A → DReps
open HasDReps    ⦃...⦄ public

instance
  unquoteDecl DecEq-DepositPurpose = derive-DecEq
    ((quote DepositPurpose , DecEq-DepositPurpose) ∷ [])


record PoolParams : Type where
  field
    owners          : ℙ KeyHash
    cost            : Coin
    margin          : UnitInterval
    pledge          : Coin
    rewardAccount   : Credential


data DCert : Type where
  delegate    : Credential → Maybe VDeleg → Maybe KeyHash → Coin → DCert
  dereg       : Credential → Maybe Coin → DCert
  regpool     : KeyHash → PoolParams → DCert
  retirepool  : KeyHash → Epoch → DCert
  regdrep     : Credential → Coin → Anchor → DCert
  deregdrep   : Credential → Coin → DCert
  ccreghot    : Credential → Maybe Credential → DCert


  -- The `reg` cert is deprecated in Conway, but it's still present in this era
  -- for backwards compatibility. This has been added to the spec to make
  -- conformance testing work properly. We don't talk about this certificate
  -- in the pdf because it has been deprecated and we want to discourage people
  -- from using it.
  reg         : Credential → Coin → DCert


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


-- The implementation requires the `reg` cert to be witnessed only if the
-- deposit is set. There didn't use to be a field for the deposit, but that was
-- added in the Conway era to make it easier to determine, just by looking at
-- the transaction, how much deposit was paid for that certificate.
cwitness (reg _ zero)        = nothing
cwitness (reg c (suc _))     = just c


record CertEnv : Type where
  field
    epoch     : Epoch
    pp        : PParams
    votes     : List GovVote
    wdrls     : RwdAddr ⇀ Coin
    coldCreds : ℙ Credential


record HasWdrls {a} (A : Type a) : Type a where
  field wdrlsOf : A → RwdAddr ⇀ Coin
open HasWdrls ⦃...⦄ public

instance
  HasWdrls-CertEnv : HasWdrls CertEnv
  HasWdrls-CertEnv .wdrlsOf = CertEnv.wdrls



record DState : Type where


  constructor ⟦_,_,_⟧ᵈ


  field
    voteDelegs   : Credential ⇀ VDeleg
    stakeDelegs  : Credential ⇀ KeyHash
    rewards      : Credential ⇀ Coin


record HasDState {a} (A : Type a) : Type a where
  field DStateOf : A → DState
open HasDState ⦃...⦄ public

record HasVDelegs {a} (A : Type a) : Type a where
  field voteDelegsOf : A → Credential ⇀ VDeleg
open HasVDelegs ⦃...⦄ public

instance
  HasVDelegs-DState : HasVDelegs DState
  HasVDelegs-DState .voteDelegsOf = DState.voteDelegs

  HasRewards-DState : HasRewards DState
  HasRewards-DState .RewardsOf = DState.rewards



record PState : Type where
  field
    pools     : KeyHash ⇀ PoolParams
    retiring  : KeyHash ⇀ Epoch


record HasPState {a} (A : Type a) : Type a where
  field PStateOf : A → PState
open HasPState ⦃...⦄ public



record GState : Type where


  constructor ⟦_,_⟧ᵛ


  field
    dreps      : DReps
    ccHotKeys  : Credential ⇀ Maybe Credential


record HasGState {a} (A : Type a) : Type a where
  field GStateOf : A → GState
open HasGState ⦃...⦄ public

instance
  HasDReps-GState : HasDReps GState
  HasDReps-GState .DRepsOf = GState.dreps



record CertState : Type where


  constructor ⟦_,_,_⟧ᶜˢ


  field
    dState : DState
    pState : PState
    gState : GState


record HasCertState {a} (A : Type a) : Type a where
  field CertStateOf : A → CertState
open HasCertState ⦃...⦄ public

instance
  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



record DelegEnv : Type where
  field
    pparams       : PParams
    pools         : KeyHash ⇀ PoolParams
    delegatees    : ℙ Credential

GovCertEnv  = CertEnv
PoolEnv     = PParams


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

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


instance
  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    : Credential ⇀ KeyHash
  ccKeys ccHotKeys       : Credential ⇀ Maybe Credential
  vDelegs voteDelegs     : Credential ⇀ VDeleg
  pools                  : KeyHash ⇀ PoolParams
  retiring               : KeyHash ⇀ Epoch
  wdrls                  : RwdAddr ⇀ 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  : PoolParams
  pp          : PParams
  mv          : Maybe VDeleg

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


data


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


data


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


data


  _⊢_⇀⦇_,GOVCERT⦈_   : GovCertEnv  → GState     → DCert       → GState     → Type


data


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


data


  _⊢_⇀⦇_,CERTBASE⦈_  : CertEnv     → CertState  → ⊤           → CertState  → Type


module _ where  -- achieves uniform (but perhaps misleading) alignment of type signatures in fig


  _⊢_⇀⦇_,CERTS⦈_     : CertEnv     → CertState  → List DCert  → CertState  → Type


  _⊢_⇀⦇_,CERTS⦈_ = ReflexiveTransitiveClosureᵇ' {_⊢_⇀⟦_⟧ᵇ_ = _⊢_⇀⦇_,CERTBASE⦈_} {_⊢_⇀⦇_,CERT⦈_}


data _⊢_⇀⦇_,DELEG⦈_ where


  DELEG-delegate :
    let Γ = $\begin{pmatrix} \,\href{Ledger.Conway.Certs.html#6532}{\htmlId{7463}{\htmlClass{Generalizable}{\text{pp}}}}\, \\ \,\href{Ledger.Conway.Certs.html#6060}{\htmlId{7468}{\htmlClass{Generalizable}{\text{pools}}}}\, \\ \,\href{Ledger.Conway.Certs.html#6349}{\htmlId{7476}{\htmlClass{Generalizable}{\text{delegatees}}}}\, \end{pmatrix}$
    in
    ∙ (c ∉ dom rwds → d ≡ pp .keyDeposit)
    ∙ (c ∈ dom rwds → d ≡ 0)
    ∙ mv ∈ mapˢ (just ∘ credVoter DRep) delegatees ∪
        fromList ( nothing ∷ just abstainRep ∷ just noConfidenceRep ∷ [] )
    ∙ mkh ∈ mapˢ just (dom pools) ∪ ❴ nothing ❵
      ────────────────────────────────
      Γ ⊢  $\begin{pmatrix} \,\href{Ledger.Conway.Certs.html#6013}{\htmlId{7795}{\htmlClass{Generalizable}{\text{vDelegs}}}}\, \\ \,\href{Ledger.Conway.Certs.html#5908}{\htmlId{7805}{\htmlClass{Generalizable}{\text{sDelegs}}}}\, \\ \,\href{Ledger.Conway.Certs.html#5840}{\htmlId{7815}{\htmlClass{Generalizable}{\text{rwds}}}}\, \end{pmatrix}$ ⇀⦇ delegate c mv mkh d ,DELEG⦈
           $\begin{pmatrix} \,\href{Axiom.Set.Map.html#7168}{\htmlId{7866}{\htmlClass{Function}{\text{insertIfJust}}}}\, \,\href{Ledger.Conway.Certs.html#6289}{\htmlId{7879}{\htmlClass{Generalizable}{\text{c}}}}\, \,\href{Ledger.Conway.Certs.html#6556}{\htmlId{7881}{\htmlClass{Generalizable}{\text{mv}}}}\, \,\href{Ledger.Conway.Certs.html#6013}{\htmlId{7884}{\htmlClass{Generalizable}{\text{vDelegs}}}}\, \\ \,\href{Axiom.Set.Map.html#7168}{\htmlId{7894}{\htmlClass{Function}{\text{insertIfJust}}}}\, \,\href{Ledger.Conway.Certs.html#6289}{\htmlId{7907}{\htmlClass{Generalizable}{\text{c}}}}\, \,\href{Ledger.Conway.Certs.html#6475}{\htmlId{7909}{\htmlClass{Generalizable}{\text{mkh}}}}\, \,\href{Ledger.Conway.Certs.html#5908}{\htmlId{7913}{\htmlClass{Generalizable}{\text{sDelegs}}}}\, \\ \,\href{Ledger.Conway.Certs.html#5840}{\htmlId{7923}{\htmlClass{Generalizable}{\text{rwds}}}}\, \,\href{Axiom.Set.Map.html#6320}{\htmlId{7928}{\htmlClass{Function Operator}{\text{∪ˡ}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{7931}{\htmlClass{Field Operator}{\text{❴}}}}\, \,\href{Ledger.Conway.Certs.html#6289}{\htmlId{7933}{\htmlClass{Generalizable}{\text{c}}}}\, \\ \,\htmlId{7937}{\htmlClass{Number}{\text{0}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{7939}{\htmlClass{Field Operator}{\text{❵}}}}\, \end{pmatrix}$

  DELEG-dereg :
    ∙ (c , 0) ∈ rwds
      ────────────────────────────────
      $\begin{pmatrix} \,\href{Ledger.Conway.Certs.html#6532}{\htmlId{8028}{\htmlClass{Generalizable}{\text{pp}}}}\, \\ \,\href{Ledger.Conway.Certs.html#6060}{\htmlId{8033}{\htmlClass{Generalizable}{\text{pools}}}}\, \\ \,\href{Ledger.Conway.Certs.html#6349}{\htmlId{8041}{\htmlClass{Generalizable}{\text{delegatees}}}}\, \end{pmatrix}$ ⊢ $\begin{pmatrix} \,\href{Ledger.Conway.Certs.html#6013}{\htmlId{8058}{\htmlClass{Generalizable}{\text{vDelegs}}}}\, \\ \,\href{Ledger.Conway.Certs.html#5908}{\htmlId{8068}{\htmlClass{Generalizable}{\text{sDelegs}}}}\, \\ \,\href{Ledger.Conway.Certs.html#5840}{\htmlId{8078}{\htmlClass{Generalizable}{\text{rwds}}}}\, \end{pmatrix}$ ⇀⦇ dereg c md ,DELEG⦈
        $\begin{pmatrix} \,\href{Ledger.Conway.Certs.html#6013}{\htmlId{8117}{\htmlClass{Generalizable}{\text{vDelegs}}}}\, \,\href{Axiom.Set.Map.html#10748}{\htmlId{8125}{\htmlClass{Function Operator}{\text{∣}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{8127}{\htmlClass{Field Operator}{\text{❴}}}}\, \,\href{Ledger.Conway.Certs.html#6289}{\htmlId{8129}{\htmlClass{Generalizable}{\text{c}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{8131}{\htmlClass{Field Operator}{\text{❵}}}}\, \,\href{Axiom.Set.Map.html#10748}{\htmlId{8133}{\htmlClass{Function Operator}{\text{ᶜ}}}}\, \\ \,\href{Ledger.Conway.Certs.html#5908}{\htmlId{8137}{\htmlClass{Generalizable}{\text{sDelegs}}}}\, \,\href{Axiom.Set.Map.html#10748}{\htmlId{8145}{\htmlClass{Function Operator}{\text{∣}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{8147}{\htmlClass{Field Operator}{\text{❴}}}}\, \,\href{Ledger.Conway.Certs.html#6289}{\htmlId{8149}{\htmlClass{Generalizable}{\text{c}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{8151}{\htmlClass{Field Operator}{\text{❵}}}}\, \,\href{Axiom.Set.Map.html#10748}{\htmlId{8153}{\htmlClass{Function Operator}{\text{ᶜ}}}}\, \\ \,\href{Ledger.Conway.Certs.html#5840}{\htmlId{8157}{\htmlClass{Generalizable}{\text{rwds}}}}\, \,\href{Axiom.Set.Map.html#10748}{\htmlId{8162}{\htmlClass{Function Operator}{\text{∣}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{8164}{\htmlClass{Field Operator}{\text{❴}}}}\, \,\href{Ledger.Conway.Certs.html#6289}{\htmlId{8166}{\htmlClass{Generalizable}{\text{c}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{8168}{\htmlClass{Field Operator}{\text{❵}}}}\, \,\href{Axiom.Set.Map.html#10748}{\htmlId{8170}{\htmlClass{Function Operator}{\text{ᶜ}}}}\, \end{pmatrix}$

  DELEG-reg :
    ∙ c ∉ dom rwds
    ∙ d ≡ pp .keyDeposit ⊎ d ≡ 0
      ────────────────────────────────
      $\begin{pmatrix} \,\href{Ledger.Conway.Certs.html#6532}{\htmlId{8288}{\htmlClass{Generalizable}{\text{pp}}}}\, \\ \,\href{Ledger.Conway.Certs.html#6060}{\htmlId{8293}{\htmlClass{Generalizable}{\text{pools}}}}\, \\ \,\href{Ledger.Conway.Certs.html#6349}{\htmlId{8301}{\htmlClass{Generalizable}{\text{delegatees}}}}\, \end{pmatrix}$ ⊢
        $\begin{pmatrix} \,\href{Ledger.Conway.Certs.html#6013}{\htmlId{8326}{\htmlClass{Generalizable}{\text{vDelegs}}}}\, \\ \,\href{Ledger.Conway.Certs.html#5908}{\htmlId{8336}{\htmlClass{Generalizable}{\text{sDelegs}}}}\, \\ \,\href{Ledger.Conway.Certs.html#5840}{\htmlId{8346}{\htmlClass{Generalizable}{\text{rwds}}}}\, \end{pmatrix}$ ⇀⦇ reg c d ,DELEG⦈
        $\begin{pmatrix} \,\href{Ledger.Conway.Certs.html#6013}{\htmlId{8382}{\htmlClass{Generalizable}{\text{vDelegs}}}}\, \\ \,\href{Ledger.Conway.Certs.html#5908}{\htmlId{8392}{\htmlClass{Generalizable}{\text{sDelegs}}}}\, \\ \,\href{Ledger.Conway.Certs.html#5840}{\htmlId{8402}{\htmlClass{Generalizable}{\text{rwds}}}}\, \,\href{Axiom.Set.Map.html#6320}{\htmlId{8407}{\htmlClass{Function Operator}{\text{∪ˡ}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{8410}{\htmlClass{Field Operator}{\text{❴}}}}\, \,\href{Ledger.Conway.Certs.html#6289}{\htmlId{8412}{\htmlClass{Generalizable}{\text{c}}}}\, \\ \,\htmlId{8416}{\htmlClass{Number}{\text{0}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{8418}{\htmlClass{Field Operator}{\text{❵}}}}\, \end{pmatrix}$


data _⊢_⇀⦇_,POOL⦈_ where


  POOL-regpool :
    ∙ kh ∉ dom pools
      ────────────────────────────────
      pp ⊢  $\begin{pmatrix} \,\href{Ledger.Conway.Certs.html#6060}{\htmlId{8542}{\htmlClass{Generalizable}{\text{pools}}}}\, \\ \,\href{Ledger.Conway.Certs.html#6108}{\htmlId{8550}{\htmlClass{Generalizable}{\text{retiring}}}}\, \end{pmatrix}$ ⇀⦇ regpool kh poolParams ,POOL⦈
            $\begin{pmatrix} \,\href{Class.HasSingleton.html#288}{\htmlId{8607}{\htmlClass{Field Operator}{\text{❴}}}}\, \,\href{Ledger.Conway.Certs.html#6451}{\htmlId{8609}{\htmlClass{Generalizable}{\text{kh}}}}\, \\ \,\href{Ledger.Conway.Certs.html#6505}{\htmlId{8614}{\htmlClass{Generalizable}{\text{poolParams}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{8625}{\htmlClass{Field Operator}{\text{❵}}}}\, \,\href{Axiom.Set.Map.html#6320}{\htmlId{8627}{\htmlClass{Function Operator}{\text{∪ˡ}}}}\, \,\href{Ledger.Conway.Certs.html#6060}{\htmlId{8630}{\htmlClass{Generalizable}{\text{pools}}}}\, \\ \,\href{Ledger.Conway.Certs.html#6108}{\htmlId{8638}{\htmlClass{Generalizable}{\text{retiring}}}}\, \end{pmatrix}$

  POOL-retirepool :
    ────────────────────────────────
    pp ⊢ $\begin{pmatrix} \,\href{Ledger.Conway.Certs.html#6060}{\htmlId{8718}{\htmlClass{Generalizable}{\text{pools}}}}\, \\ \,\href{Ledger.Conway.Certs.html#6108}{\htmlId{8726}{\htmlClass{Generalizable}{\text{retiring}}}}\, \end{pmatrix}$ ⇀⦇ retirepool kh e ,POOL⦈ $\begin{pmatrix} \,\href{Ledger.Conway.Certs.html#6060}{\htmlId{8765}{\htmlClass{Generalizable}{\text{pools}}}}\, \\ \,\href{Class.HasSingleton.html#288}{\htmlId{8773}{\htmlClass{Field Operator}{\text{❴}}}}\, \,\href{Ledger.Conway.Certs.html#6451}{\htmlId{8775}{\htmlClass{Generalizable}{\text{kh}}}}\, \\ \,\href{Ledger.Conway.Certs.html#6400}{\htmlId{8780}{\htmlClass{Generalizable}{\text{e}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{8782}{\htmlClass{Field Operator}{\text{❵}}}}\, \,\href{Axiom.Set.Map.html#6320}{\htmlId{8784}{\htmlClass{Function Operator}{\text{∪ˡ}}}}\, \,\href{Ledger.Conway.Certs.html#6108}{\htmlId{8787}{\htmlClass{Generalizable}{\text{retiring}}}}\, \end{pmatrix}$


data _⊢_⇀⦇_,GOVCERT⦈_ where


  GOVCERT-regdrep :
    let Γ = $\begin{pmatrix} \,\href{Ledger.Conway.Certs.html#6400}{\htmlId{8864}{\htmlClass{Generalizable}{\text{e}}}}\, \\ \,\href{Ledger.Conway.Certs.html#6532}{\htmlId{8868}{\htmlClass{Generalizable}{\text{pp}}}}\, \\ \,\href{Ledger.Conway.Certs.html#6422}{\htmlId{8873}{\htmlClass{Generalizable}{\text{vs}}}}\, \\ \,\href{Ledger.Conway.Certs.html#6151}{\htmlId{8878}{\htmlClass{Generalizable}{\text{wdrls}}}}\, \\ \,\href{Ledger.Conway.Certs.html#6646}{\htmlId{8886}{\htmlClass{Generalizable}{\text{cc}}}}\, \end{pmatrix}$
    in
    ∙ (d ≡ pp .drepDeposit × c ∉ dom dReps) ⊎ (d ≡ 0 × c ∈ dom dReps)
      ────────────────────────────────
      Γ ⊢ $\begin{pmatrix} \,\href{Ledger.Conway.Certs.html#5875}{\htmlId{9019}{\htmlClass{Generalizable}{\text{dReps}}}}\, \\ \,\href{Ledger.Conway.Certs.html#5956}{\htmlId{9027}{\htmlClass{Generalizable}{\text{ccKeys}}}}\, \end{pmatrix}$ ⇀⦇ regdrep c d an ,GOVCERT⦈
          $\begin{pmatrix} \,\href{Class.HasSingleton.html#288}{\htmlId{9076}{\htmlClass{Field Operator}{\text{❴}}}}\, \,\href{Ledger.Conway.Certs.html#6289}{\htmlId{9078}{\htmlClass{Generalizable}{\text{c}}}}\, \\ \,\href{Ledger.Conway.Certs.html#6400}{\htmlId{9082}{\htmlClass{Generalizable}{\text{e}}}}\, \,\href{Class.HasAdd.Core.html#162}{\htmlId{9084}{\htmlClass{Field Operator}{\text{+}}}}\, \,\href{Ledger.Conway.Certs.html#6532}{\htmlId{9086}{\htmlClass{Generalizable}{\text{pp}}}}\, \,\htmlId{9089}{\htmlClass{Symbol}{\text{.}}}\,\,\href{Ledger.Conway.PParams.html#3451}{\htmlId{9090}{\htmlClass{Field}{\text{drepActivity}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{9103}{\htmlClass{Field Operator}{\text{❵}}}}\, \,\href{Axiom.Set.Map.html#6320}{\htmlId{9105}{\htmlClass{Function Operator}{\text{∪ˡ}}}}\, \,\href{Ledger.Conway.Certs.html#5875}{\htmlId{9108}{\htmlClass{Generalizable}{\text{dReps}}}}\, \\ \,\href{Ledger.Conway.Certs.html#5956}{\htmlId{9116}{\htmlClass{Generalizable}{\text{ccKeys}}}}\, \end{pmatrix}$

  GOVCERT-deregdrep :
    ∙ c ∈ dom dReps
      ────────────────────────────────
      $\begin{pmatrix} \,\href{Ledger.Conway.Certs.html#6400}{\htmlId{9215}{\htmlClass{Generalizable}{\text{e}}}}\, \\ \,\href{Ledger.Conway.Certs.html#6532}{\htmlId{9219}{\htmlClass{Generalizable}{\text{pp}}}}\, \\ \,\href{Ledger.Conway.Certs.html#6422}{\htmlId{9224}{\htmlClass{Generalizable}{\text{vs}}}}\, \\ \,\href{Ledger.Conway.Certs.html#6151}{\htmlId{9229}{\htmlClass{Generalizable}{\text{wdrls}}}}\, \\ \,\href{Ledger.Conway.Certs.html#6646}{\htmlId{9237}{\htmlClass{Generalizable}{\text{cc}}}}\, \end{pmatrix}$ ⊢ $\begin{pmatrix} \,\href{Ledger.Conway.Certs.html#5875}{\htmlId{9246}{\htmlClass{Generalizable}{\text{dReps}}}}\, \\ \,\href{Ledger.Conway.Certs.html#5956}{\htmlId{9254}{\htmlClass{Generalizable}{\text{ccKeys}}}}\, \end{pmatrix}$ ⇀⦇ deregdrep c d ,GOVCERT⦈ $\begin{pmatrix} \,\href{Ledger.Conway.Certs.html#5875}{\htmlId{9292}{\htmlClass{Generalizable}{\text{dReps}}}}\, \,\href{Axiom.Set.Map.html#10748}{\htmlId{9298}{\htmlClass{Function Operator}{\text{∣}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{9300}{\htmlClass{Field Operator}{\text{❴}}}}\, \,\href{Ledger.Conway.Certs.html#6289}{\htmlId{9302}{\htmlClass{Generalizable}{\text{c}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{9304}{\htmlClass{Field Operator}{\text{❵}}}}\, \,\href{Axiom.Set.Map.html#10748}{\htmlId{9306}{\htmlClass{Function Operator}{\text{ᶜ}}}}\, \\ \,\href{Ledger.Conway.Certs.html#5956}{\htmlId{9310}{\htmlClass{Generalizable}{\text{ccKeys}}}}\, \end{pmatrix}$

  GOVCERT-ccreghot :
    ∙ (c , nothing) ∉ ccKeys
    ∙ c ∈ cc
      ────────────────────────────────
      $\begin{pmatrix} \,\href{Ledger.Conway.Certs.html#6400}{\htmlId{9430}{\htmlClass{Generalizable}{\text{e}}}}\, \\ \,\href{Ledger.Conway.Certs.html#6532}{\htmlId{9434}{\htmlClass{Generalizable}{\text{pp}}}}\, \\ \,\href{Ledger.Conway.Certs.html#6422}{\htmlId{9439}{\htmlClass{Generalizable}{\text{vs}}}}\, \\ \,\href{Ledger.Conway.Certs.html#6151}{\htmlId{9444}{\htmlClass{Generalizable}{\text{wdrls}}}}\, \\ \,\href{Ledger.Conway.Certs.html#6646}{\htmlId{9452}{\htmlClass{Generalizable}{\text{cc}}}}\, \end{pmatrix}$ ⊢ $\begin{pmatrix} \,\href{Ledger.Conway.Certs.html#5875}{\htmlId{9461}{\htmlClass{Generalizable}{\text{dReps}}}}\, \\ \,\href{Ledger.Conway.Certs.html#5956}{\htmlId{9469}{\htmlClass{Generalizable}{\text{ccKeys}}}}\, \end{pmatrix}$ ⇀⦇ ccreghot c mc ,GOVCERT⦈ $\begin{pmatrix} \,\href{Ledger.Conway.Certs.html#5875}{\htmlId{9507}{\htmlClass{Generalizable}{\text{dReps}}}}\, \\ \,\href{Class.HasSingleton.html#288}{\htmlId{9515}{\htmlClass{Field Operator}{\text{❴}}}}\, \,\href{Ledger.Conway.Certs.html#6289}{\htmlId{9517}{\htmlClass{Generalizable}{\text{c}}}}\, \\ \,\href{Ledger.Conway.Certs.html#6316}{\htmlId{9521}{\htmlClass{Generalizable}{\text{mc}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{9524}{\htmlClass{Field Operator}{\text{❵}}}}\, \,\href{Axiom.Set.Map.html#6320}{\htmlId{9526}{\htmlClass{Function Operator}{\text{∪ˡ}}}}\, \,\href{Ledger.Conway.Certs.html#5956}{\htmlId{9529}{\htmlClass{Generalizable}{\text{ccKeys}}}}\, \end{pmatrix}$


data _⊢_⇀⦇_,CERT⦈_ where


  CERT-deleg :
    ∙ $\begin{pmatrix} \,\href{Ledger.Conway.Certs.html#6532}{\htmlId{9590}{\htmlClass{Generalizable}{\text{pp}}}}\, \\ \,\href{Ledger.Conway.Certs.html#3793}{\htmlId{9595}{\htmlClass{Field}{\text{PState.pools}}}}\, \,\href{Ledger.Conway.Certs.html#6626}{\htmlId{9608}{\htmlClass{Generalizable}{\text{stᵖ}}}}\, \\ \,\href{Class.IsSet.html#916}{\htmlId{9614}{\htmlClass{Function}{\text{dom}}}}\, (\,\href{Ledger.Conway.Certs.html#4034}{\htmlId{9619}{\htmlClass{Field}{\text{GState.dreps}}}}\, \,\href{Ledger.Conway.Certs.html#6606}{\htmlId{9632}{\htmlClass{Generalizable}{\text{stᵍ}}}}\,) \end{pmatrix}$ ⊢ stᵈ ⇀⦇ dCert ,DELEG⦈ stᵈ'
      ────────────────────────────────
      $\begin{pmatrix} \,\href{Ledger.Conway.Certs.html#6400}{\htmlId{9714}{\htmlClass{Generalizable}{\text{e}}}}\, \\ \,\href{Ledger.Conway.Certs.html#6532}{\htmlId{9718}{\htmlClass{Generalizable}{\text{pp}}}}\, \\ \,\href{Ledger.Conway.Certs.html#6422}{\htmlId{9723}{\htmlClass{Generalizable}{\text{vs}}}}\, \\ \,\href{Ledger.Conway.Certs.html#6151}{\htmlId{9728}{\htmlClass{Generalizable}{\text{wdrls}}}}\, \\ \,\href{Ledger.Conway.Certs.html#6646}{\htmlId{9736}{\htmlClass{Generalizable}{\text{cc}}}}\, \end{pmatrix}$ ⊢ $\begin{pmatrix} \,\href{Ledger.Conway.Certs.html#6586}{\htmlId{9745}{\htmlClass{Generalizable}{\text{stᵈ}}}}\, \\ \,\href{Ledger.Conway.Certs.html#6626}{\htmlId{9751}{\htmlClass{Generalizable}{\text{stᵖ}}}}\, \\ \,\href{Ledger.Conway.Certs.html#6606}{\htmlId{9757}{\htmlClass{Generalizable}{\text{stᵍ}}}}\, \end{pmatrix}$ ⇀⦇ dCert ,CERT⦈ $\begin{pmatrix} \,\href{Ledger.Conway.Certs.html#6590}{\htmlId{9781}{\htmlClass{Generalizable}{\text{stᵈ'}}}}\, \\ \,\href{Ledger.Conway.Certs.html#6626}{\htmlId{9788}{\htmlClass{Generalizable}{\text{stᵖ}}}}\, \\ \,\href{Ledger.Conway.Certs.html#6606}{\htmlId{9794}{\htmlClass{Generalizable}{\text{stᵍ}}}}\, \end{pmatrix}$

  CERT-pool :
    ∙ pp ⊢ stᵖ ⇀⦇ dCert ,POOL⦈ stᵖ'
      ────────────────────────────────
      $\begin{pmatrix} \,\href{Ledger.Conway.Certs.html#6400}{\htmlId{9898}{\htmlClass{Generalizable}{\text{e}}}}\, \\ \,\href{Ledger.Conway.Certs.html#6532}{\htmlId{9902}{\htmlClass{Generalizable}{\text{pp}}}}\, \\ \,\href{Ledger.Conway.Certs.html#6422}{\htmlId{9907}{\htmlClass{Generalizable}{\text{vs}}}}\, \\ \,\href{Ledger.Conway.Certs.html#6151}{\htmlId{9912}{\htmlClass{Generalizable}{\text{wdrls}}}}\, \\ \,\href{Ledger.Conway.Certs.html#6646}{\htmlId{9920}{\htmlClass{Generalizable}{\text{cc}}}}\, \end{pmatrix}$ ⊢ $\begin{pmatrix} \,\href{Ledger.Conway.Certs.html#6586}{\htmlId{9929}{\htmlClass{Generalizable}{\text{stᵈ}}}}\, \\ \,\href{Ledger.Conway.Certs.html#6626}{\htmlId{9935}{\htmlClass{Generalizable}{\text{stᵖ}}}}\, \\ \,\href{Ledger.Conway.Certs.html#6606}{\htmlId{9941}{\htmlClass{Generalizable}{\text{stᵍ}}}}\, \end{pmatrix}$ ⇀⦇ dCert ,CERT⦈ $\begin{pmatrix} \,\href{Ledger.Conway.Certs.html#6586}{\htmlId{9965}{\htmlClass{Generalizable}{\text{stᵈ}}}}\, \\ \,\href{Ledger.Conway.Certs.html#6630}{\htmlId{9971}{\htmlClass{Generalizable}{\text{stᵖ'}}}}\, \\ \,\href{Ledger.Conway.Certs.html#6606}{\htmlId{9978}{\htmlClass{Generalizable}{\text{stᵍ}}}}\, \end{pmatrix}$

  CERT-vdel :
    ∙ Γ ⊢ stᵍ ⇀⦇ dCert ,GOVCERT⦈ stᵍ'
      ────────────────────────────────
      Γ ⊢ $\begin{pmatrix} \,\href{Ledger.Conway.Certs.html#6586}{\htmlId{10088}{\htmlClass{Generalizable}{\text{stᵈ}}}}\, \\ \,\href{Ledger.Conway.Certs.html#6626}{\htmlId{10094}{\htmlClass{Generalizable}{\text{stᵖ}}}}\, \\ \,\href{Ledger.Conway.Certs.html#6606}{\htmlId{10100}{\htmlClass{Generalizable}{\text{stᵍ}}}}\, \end{pmatrix}$ ⇀⦇ dCert ,CERT⦈ $\begin{pmatrix} \,\href{Ledger.Conway.Certs.html#6586}{\htmlId{10124}{\htmlClass{Generalizable}{\text{stᵈ}}}}\, \\ \,\href{Ledger.Conway.Certs.html#6626}{\htmlId{10130}{\htmlClass{Generalizable}{\text{stᵖ}}}}\, \\ \,\href{Ledger.Conway.Certs.html#6610}{\htmlId{10136}{\htmlClass{Generalizable}{\text{stᵍ'}}}}\, \end{pmatrix}$


data _⊢_⇀⦇_,CERTBASE⦈_ where


  CERT-base :
    let refresh          = mapPartial getDRepVote (fromList vs)
        refreshedDReps   = mapValueRestricted (const (e + pp .drepActivity)) dReps refresh
        wdrlCreds        = mapˢ stake (dom wdrls)
        validVoteDelegs  = voteDelegs ∣^ (  mapˢ (credVoter DRep) (dom dReps)
                                        ∪ fromList (noConfidenceRep ∷ abstainRep ∷ []) )
    in
    ∙ filter isKeyHash wdrlCreds ⊆ dom voteDelegs
    ∙ mapˢ (map₁ stake) (wdrls ˢ) ⊆ rewards ˢ
      ────────────────────────────────
      $\begin{pmatrix} \,\href{Ledger.Conway.Certs.html#6400}{\htmlId{10712}{\htmlClass{Generalizable}{\text{e}}}}\, \\ \,\href{Ledger.Conway.Certs.html#6532}{\htmlId{10716}{\htmlClass{Generalizable}{\text{pp}}}}\, \\ \,\href{Ledger.Conway.Certs.html#6422}{\htmlId{10721}{\htmlClass{Generalizable}{\text{vs}}}}\, \\ \,\href{Ledger.Conway.Certs.html#6151}{\htmlId{10726}{\htmlClass{Generalizable}{\text{wdrls}}}}\, \\ \,\href{Ledger.Conway.Certs.html#6646}{\htmlId{10734}{\htmlClass{Generalizable}{\text{cc}}}}\, \end{pmatrix}$ ⊢
        $\begin{pmatrix} \begin{pmatrix} \,\href{Ledger.Conway.Certs.html#6021}{\htmlId{10753}{\htmlClass{Generalizable}{\text{voteDelegs}}}}\, \\ \,\href{Ledger.Conway.Certs.html#5916}{\htmlId{10766}{\htmlClass{Generalizable}{\text{stakeDelegs}}}}\, \\ \,\href{Ledger.Conway.Certs.html#5845}{\htmlId{10780}{\htmlClass{Generalizable}{\text{rewards}}}}\, \end{pmatrix}
        \\ \,\href{Ledger.Conway.Certs.html#6626}{\htmlId{10800}{\htmlClass{Generalizable}{\text{stᵖ}}}}\,
        \\ \begin{pmatrix} \,\href{Ledger.Conway.Certs.html#5875}{\htmlId{10816}{\htmlClass{Generalizable}{\text{dReps}}}}\, \\ \,\href{Ledger.Conway.Certs.html#5963}{\htmlId{10824}{\htmlClass{Generalizable}{\text{ccHotKeys}}}}\, \end{pmatrix}
        \end{pmatrix}$ ⇀⦇ _ ,CERTBASE⦈
        $\begin{pmatrix} \begin{pmatrix} \,\href{Ledger.Conway.Certs.html#10403}{\htmlId{10874}{\htmlClass{Bound}{\text{validVoteDelegs}}}}\, \\ \,\href{Ledger.Conway.Certs.html#5916}{\htmlId{10892}{\htmlClass{Generalizable}{\text{stakeDelegs}}}}\, \\ \,\href{Axiom.Set.Map.html#9130}{\htmlId{10906}{\htmlClass{Function}{\text{constMap}}}}\, \,\href{Ledger.Conway.Certs.html#10353}{\htmlId{10915}{\htmlClass{Bound}{\text{wdrlCreds}}}}\, \,\htmlId{10925}{\htmlClass{Number}{\text{0}}}\, \,\href{Axiom.Set.Map.html#6320}{\htmlId{10927}{\htmlClass{Function Operator}{\text{∪ˡ}}}}\, \,\href{Ledger.Conway.Certs.html#5845}{\htmlId{10930}{\htmlClass{Generalizable}{\text{rewards}}}}\, \end{pmatrix}
        \\ \,\href{Ledger.Conway.Certs.html#6626}{\htmlId{10950}{\htmlClass{Generalizable}{\text{stᵖ}}}}\,
        \\ \begin{pmatrix} \,\href{Ledger.Conway.Certs.html#10262}{\htmlId{10966}{\htmlClass{Bound}{\text{refreshedDReps}}}}\, \\ \,\href{Ledger.Conway.Certs.html#5963}{\htmlId{10983}{\htmlClass{Generalizable}{\text{ccHotKeys}}}}\, \end{pmatrix}
        \end{pmatrix}$