{-# OPTIONS --safe #-}

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

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

open import Tactic.Derive.DecEq

open import Ledger.Conway.GovernanceActions 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#6580}{\htmlId{7511}{\htmlClass{Generalizable}{\text{pp}}}}\, \\ \,\href{Ledger.Conway.Certs.html#6108}{\htmlId{7516}{\htmlClass{Generalizable}{\text{pools}}}}\, \\ \,\href{Ledger.Conway.Certs.html#6397}{\htmlId{7524}{\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#6061}{\htmlId{7843}{\htmlClass{Generalizable}{\text{vDelegs}}}}\, \\ \,\href{Ledger.Conway.Certs.html#5956}{\htmlId{7853}{\htmlClass{Generalizable}{\text{sDelegs}}}}\, \\ \,\href{Ledger.Conway.Certs.html#5888}{\htmlId{7863}{\htmlClass{Generalizable}{\text{rwds}}}}\, \end{pmatrix}$ ⇀⦇ delegate c mv mkh d ,DELEG⦈
           $\begin{pmatrix} \,\href{Axiom.Set.Map.html#7168}{\htmlId{7914}{\htmlClass{Function}{\text{insertIfJust}}}}\, \,\href{Ledger.Conway.Certs.html#6337}{\htmlId{7927}{\htmlClass{Generalizable}{\text{c}}}}\, \,\href{Ledger.Conway.Certs.html#6604}{\htmlId{7929}{\htmlClass{Generalizable}{\text{mv}}}}\, \,\href{Ledger.Conway.Certs.html#6061}{\htmlId{7932}{\htmlClass{Generalizable}{\text{vDelegs}}}}\, \\ \,\href{Axiom.Set.Map.html#7168}{\htmlId{7942}{\htmlClass{Function}{\text{insertIfJust}}}}\, \,\href{Ledger.Conway.Certs.html#6337}{\htmlId{7955}{\htmlClass{Generalizable}{\text{c}}}}\, \,\href{Ledger.Conway.Certs.html#6523}{\htmlId{7957}{\htmlClass{Generalizable}{\text{mkh}}}}\, \,\href{Ledger.Conway.Certs.html#5956}{\htmlId{7961}{\htmlClass{Generalizable}{\text{sDelegs}}}}\, \\ \,\href{Ledger.Conway.Certs.html#5888}{\htmlId{7971}{\htmlClass{Generalizable}{\text{rwds}}}}\, \,\href{Axiom.Set.Map.html#6320}{\htmlId{7976}{\htmlClass{Function Operator}{\text{∪ˡ}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{7979}{\htmlClass{Field Operator}{\text{❴}}}}\, \,\href{Ledger.Conway.Certs.html#6337}{\htmlId{7981}{\htmlClass{Generalizable}{\text{c}}}}\, \\ \,\htmlId{7985}{\htmlClass{Number}{\text{0}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{7987}{\htmlClass{Field Operator}{\text{❵}}}}\, \end{pmatrix}$

  DELEG-dereg :
    ∙ (c , 0) ∈ rwds
      ────────────────────────────────
      $\begin{pmatrix} \,\href{Ledger.Conway.Certs.html#6580}{\htmlId{8076}{\htmlClass{Generalizable}{\text{pp}}}}\, \\ \,\href{Ledger.Conway.Certs.html#6108}{\htmlId{8081}{\htmlClass{Generalizable}{\text{pools}}}}\, \\ \,\href{Ledger.Conway.Certs.html#6397}{\htmlId{8089}{\htmlClass{Generalizable}{\text{delegatees}}}}\, \end{pmatrix}$ ⊢ $\begin{pmatrix} \,\href{Ledger.Conway.Certs.html#6061}{\htmlId{8106}{\htmlClass{Generalizable}{\text{vDelegs}}}}\, \\ \,\href{Ledger.Conway.Certs.html#5956}{\htmlId{8116}{\htmlClass{Generalizable}{\text{sDelegs}}}}\, \\ \,\href{Ledger.Conway.Certs.html#5888}{\htmlId{8126}{\htmlClass{Generalizable}{\text{rwds}}}}\, \end{pmatrix}$ ⇀⦇ dereg c md ,DELEG⦈
        $\begin{pmatrix} \,\href{Ledger.Conway.Certs.html#6061}{\htmlId{8165}{\htmlClass{Generalizable}{\text{vDelegs}}}}\, \,\href{Axiom.Set.Map.html#10748}{\htmlId{8173}{\htmlClass{Function Operator}{\text{∣}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{8175}{\htmlClass{Field Operator}{\text{❴}}}}\, \,\href{Ledger.Conway.Certs.html#6337}{\htmlId{8177}{\htmlClass{Generalizable}{\text{c}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{8179}{\htmlClass{Field Operator}{\text{❵}}}}\, \,\href{Axiom.Set.Map.html#10748}{\htmlId{8181}{\htmlClass{Function Operator}{\text{ᶜ}}}}\, \\ \,\href{Ledger.Conway.Certs.html#5956}{\htmlId{8185}{\htmlClass{Generalizable}{\text{sDelegs}}}}\, \,\href{Axiom.Set.Map.html#10748}{\htmlId{8193}{\htmlClass{Function Operator}{\text{∣}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{8195}{\htmlClass{Field Operator}{\text{❴}}}}\, \,\href{Ledger.Conway.Certs.html#6337}{\htmlId{8197}{\htmlClass{Generalizable}{\text{c}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{8199}{\htmlClass{Field Operator}{\text{❵}}}}\, \,\href{Axiom.Set.Map.html#10748}{\htmlId{8201}{\htmlClass{Function Operator}{\text{ᶜ}}}}\, \\ \,\href{Ledger.Conway.Certs.html#5888}{\htmlId{8205}{\htmlClass{Generalizable}{\text{rwds}}}}\, \,\href{Axiom.Set.Map.html#10748}{\htmlId{8210}{\htmlClass{Function Operator}{\text{∣}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{8212}{\htmlClass{Field Operator}{\text{❴}}}}\, \,\href{Ledger.Conway.Certs.html#6337}{\htmlId{8214}{\htmlClass{Generalizable}{\text{c}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{8216}{\htmlClass{Field Operator}{\text{❵}}}}\, \,\href{Axiom.Set.Map.html#10748}{\htmlId{8218}{\htmlClass{Function Operator}{\text{ᶜ}}}}\, \end{pmatrix}$

  DELEG-reg :
    ∙ c ∉ dom rwds
    ∙ d ≡ pp .keyDeposit ⊎ d ≡ 0
      ────────────────────────────────
      $\begin{pmatrix} \,\href{Ledger.Conway.Certs.html#6580}{\htmlId{8336}{\htmlClass{Generalizable}{\text{pp}}}}\, \\ \,\href{Ledger.Conway.Certs.html#6108}{\htmlId{8341}{\htmlClass{Generalizable}{\text{pools}}}}\, \\ \,\href{Ledger.Conway.Certs.html#6397}{\htmlId{8349}{\htmlClass{Generalizable}{\text{delegatees}}}}\, \end{pmatrix}$ ⊢
        $\begin{pmatrix} \,\href{Ledger.Conway.Certs.html#6061}{\htmlId{8374}{\htmlClass{Generalizable}{\text{vDelegs}}}}\, \\ \,\href{Ledger.Conway.Certs.html#5956}{\htmlId{8384}{\htmlClass{Generalizable}{\text{sDelegs}}}}\, \\ \,\href{Ledger.Conway.Certs.html#5888}{\htmlId{8394}{\htmlClass{Generalizable}{\text{rwds}}}}\, \end{pmatrix}$ ⇀⦇ reg c d ,DELEG⦈
        $\begin{pmatrix} \,\href{Ledger.Conway.Certs.html#6061}{\htmlId{8430}{\htmlClass{Generalizable}{\text{vDelegs}}}}\, \\ \,\href{Ledger.Conway.Certs.html#5956}{\htmlId{8440}{\htmlClass{Generalizable}{\text{sDelegs}}}}\, \\ \,\href{Ledger.Conway.Certs.html#5888}{\htmlId{8450}{\htmlClass{Generalizable}{\text{rwds}}}}\, \,\href{Axiom.Set.Map.html#6320}{\htmlId{8455}{\htmlClass{Function Operator}{\text{∪ˡ}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{8458}{\htmlClass{Field Operator}{\text{❴}}}}\, \,\href{Ledger.Conway.Certs.html#6337}{\htmlId{8460}{\htmlClass{Generalizable}{\text{c}}}}\, \\ \,\htmlId{8464}{\htmlClass{Number}{\text{0}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{8466}{\htmlClass{Field Operator}{\text{❵}}}}\, \end{pmatrix}$


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


  POOL-regpool :
    ∙ kh ∉ dom pools
      ────────────────────────────────
      pp ⊢  $\begin{pmatrix} \,\href{Ledger.Conway.Certs.html#6108}{\htmlId{8590}{\htmlClass{Generalizable}{\text{pools}}}}\, \\ \,\href{Ledger.Conway.Certs.html#6156}{\htmlId{8598}{\htmlClass{Generalizable}{\text{retiring}}}}\, \end{pmatrix}$ ⇀⦇ regpool kh poolParams ,POOL⦈
            $\begin{pmatrix} \,\href{Class.HasSingleton.html#288}{\htmlId{8655}{\htmlClass{Field Operator}{\text{❴}}}}\, \,\href{Ledger.Conway.Certs.html#6499}{\htmlId{8657}{\htmlClass{Generalizable}{\text{kh}}}}\, \\ \,\href{Ledger.Conway.Certs.html#6553}{\htmlId{8662}{\htmlClass{Generalizable}{\text{poolParams}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{8673}{\htmlClass{Field Operator}{\text{❵}}}}\, \,\href{Axiom.Set.Map.html#6320}{\htmlId{8675}{\htmlClass{Function Operator}{\text{∪ˡ}}}}\, \,\href{Ledger.Conway.Certs.html#6108}{\htmlId{8678}{\htmlClass{Generalizable}{\text{pools}}}}\, \\ \,\href{Ledger.Conway.Certs.html#6156}{\htmlId{8686}{\htmlClass{Generalizable}{\text{retiring}}}}\, \end{pmatrix}$

  POOL-retirepool :
    ────────────────────────────────
    pp ⊢ $\begin{pmatrix} \,\href{Ledger.Conway.Certs.html#6108}{\htmlId{8766}{\htmlClass{Generalizable}{\text{pools}}}}\, \\ \,\href{Ledger.Conway.Certs.html#6156}{\htmlId{8774}{\htmlClass{Generalizable}{\text{retiring}}}}\, \end{pmatrix}$ ⇀⦇ retirepool kh e ,POOL⦈ $\begin{pmatrix} \,\href{Ledger.Conway.Certs.html#6108}{\htmlId{8813}{\htmlClass{Generalizable}{\text{pools}}}}\, \\ \,\href{Class.HasSingleton.html#288}{\htmlId{8821}{\htmlClass{Field Operator}{\text{❴}}}}\, \,\href{Ledger.Conway.Certs.html#6499}{\htmlId{8823}{\htmlClass{Generalizable}{\text{kh}}}}\, \\ \,\href{Ledger.Conway.Certs.html#6448}{\htmlId{8828}{\htmlClass{Generalizable}{\text{e}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{8830}{\htmlClass{Field Operator}{\text{❵}}}}\, \,\href{Axiom.Set.Map.html#6320}{\htmlId{8832}{\htmlClass{Function Operator}{\text{∪ˡ}}}}\, \,\href{Ledger.Conway.Certs.html#6156}{\htmlId{8835}{\htmlClass{Generalizable}{\text{retiring}}}}\, \end{pmatrix}$


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


  GOVCERT-regdrep :
    let Γ = $\begin{pmatrix} \,\href{Ledger.Conway.Certs.html#6448}{\htmlId{8912}{\htmlClass{Generalizable}{\text{e}}}}\, \\ \,\href{Ledger.Conway.Certs.html#6580}{\htmlId{8916}{\htmlClass{Generalizable}{\text{pp}}}}\, \\ \,\href{Ledger.Conway.Certs.html#6470}{\htmlId{8921}{\htmlClass{Generalizable}{\text{vs}}}}\, \\ \,\href{Ledger.Conway.Certs.html#6199}{\htmlId{8926}{\htmlClass{Generalizable}{\text{wdrls}}}}\, \\ \,\href{Ledger.Conway.Certs.html#6694}{\htmlId{8934}{\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#5923}{\htmlId{9067}{\htmlClass{Generalizable}{\text{dReps}}}}\, \\ \,\href{Ledger.Conway.Certs.html#6004}{\htmlId{9075}{\htmlClass{Generalizable}{\text{ccKeys}}}}\, \end{pmatrix}$ ⇀⦇ regdrep c d an ,GOVCERT⦈
          $\begin{pmatrix} \,\href{Class.HasSingleton.html#288}{\htmlId{9124}{\htmlClass{Field Operator}{\text{❴}}}}\, \,\href{Ledger.Conway.Certs.html#6337}{\htmlId{9126}{\htmlClass{Generalizable}{\text{c}}}}\, \\ \,\href{Ledger.Conway.Certs.html#6448}{\htmlId{9130}{\htmlClass{Generalizable}{\text{e}}}}\, \,\href{Class.HasAdd.Core.html#162}{\htmlId{9132}{\htmlClass{Field Operator}{\text{+}}}}\, \,\href{Ledger.Conway.Certs.html#6580}{\htmlId{9134}{\htmlClass{Generalizable}{\text{pp}}}}\, \,\htmlId{9137}{\htmlClass{Symbol}{\text{.}}}\,\,\href{Ledger.Conway.PParams.html#3478}{\htmlId{9138}{\htmlClass{Field}{\text{drepActivity}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{9151}{\htmlClass{Field Operator}{\text{❵}}}}\, \,\href{Axiom.Set.Map.html#6320}{\htmlId{9153}{\htmlClass{Function Operator}{\text{∪ˡ}}}}\, \,\href{Ledger.Conway.Certs.html#5923}{\htmlId{9156}{\htmlClass{Generalizable}{\text{dReps}}}}\, \\ \,\href{Ledger.Conway.Certs.html#6004}{\htmlId{9164}{\htmlClass{Generalizable}{\text{ccKeys}}}}\, \end{pmatrix}$

  GOVCERT-deregdrep :
    ∙ c ∈ dom dReps
      ────────────────────────────────
      $\begin{pmatrix} \,\href{Ledger.Conway.Certs.html#6448}{\htmlId{9263}{\htmlClass{Generalizable}{\text{e}}}}\, \\ \,\href{Ledger.Conway.Certs.html#6580}{\htmlId{9267}{\htmlClass{Generalizable}{\text{pp}}}}\, \\ \,\href{Ledger.Conway.Certs.html#6470}{\htmlId{9272}{\htmlClass{Generalizable}{\text{vs}}}}\, \\ \,\href{Ledger.Conway.Certs.html#6199}{\htmlId{9277}{\htmlClass{Generalizable}{\text{wdrls}}}}\, \\ \,\href{Ledger.Conway.Certs.html#6694}{\htmlId{9285}{\htmlClass{Generalizable}{\text{cc}}}}\, \end{pmatrix}$ ⊢ $\begin{pmatrix} \,\href{Ledger.Conway.Certs.html#5923}{\htmlId{9294}{\htmlClass{Generalizable}{\text{dReps}}}}\, \\ \,\href{Ledger.Conway.Certs.html#6004}{\htmlId{9302}{\htmlClass{Generalizable}{\text{ccKeys}}}}\, \end{pmatrix}$ ⇀⦇ deregdrep c d ,GOVCERT⦈ $\begin{pmatrix} \,\href{Ledger.Conway.Certs.html#5923}{\htmlId{9340}{\htmlClass{Generalizable}{\text{dReps}}}}\, \,\href{Axiom.Set.Map.html#10748}{\htmlId{9346}{\htmlClass{Function Operator}{\text{∣}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{9348}{\htmlClass{Field Operator}{\text{❴}}}}\, \,\href{Ledger.Conway.Certs.html#6337}{\htmlId{9350}{\htmlClass{Generalizable}{\text{c}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{9352}{\htmlClass{Field Operator}{\text{❵}}}}\, \,\href{Axiom.Set.Map.html#10748}{\htmlId{9354}{\htmlClass{Function Operator}{\text{ᶜ}}}}\, \\ \,\href{Ledger.Conway.Certs.html#6004}{\htmlId{9358}{\htmlClass{Generalizable}{\text{ccKeys}}}}\, \end{pmatrix}$

  GOVCERT-ccreghot :
    ∙ (c , nothing) ∉ ccKeys
    ∙ c ∈ cc
      ────────────────────────────────
      $\begin{pmatrix} \,\href{Ledger.Conway.Certs.html#6448}{\htmlId{9478}{\htmlClass{Generalizable}{\text{e}}}}\, \\ \,\href{Ledger.Conway.Certs.html#6580}{\htmlId{9482}{\htmlClass{Generalizable}{\text{pp}}}}\, \\ \,\href{Ledger.Conway.Certs.html#6470}{\htmlId{9487}{\htmlClass{Generalizable}{\text{vs}}}}\, \\ \,\href{Ledger.Conway.Certs.html#6199}{\htmlId{9492}{\htmlClass{Generalizable}{\text{wdrls}}}}\, \\ \,\href{Ledger.Conway.Certs.html#6694}{\htmlId{9500}{\htmlClass{Generalizable}{\text{cc}}}}\, \end{pmatrix}$ ⊢ $\begin{pmatrix} \,\href{Ledger.Conway.Certs.html#5923}{\htmlId{9509}{\htmlClass{Generalizable}{\text{dReps}}}}\, \\ \,\href{Ledger.Conway.Certs.html#6004}{\htmlId{9517}{\htmlClass{Generalizable}{\text{ccKeys}}}}\, \end{pmatrix}$ ⇀⦇ ccreghot c mc ,GOVCERT⦈ $\begin{pmatrix} \,\href{Ledger.Conway.Certs.html#5923}{\htmlId{9555}{\htmlClass{Generalizable}{\text{dReps}}}}\, \\ \,\href{Class.HasSingleton.html#288}{\htmlId{9563}{\htmlClass{Field Operator}{\text{❴}}}}\, \,\href{Ledger.Conway.Certs.html#6337}{\htmlId{9565}{\htmlClass{Generalizable}{\text{c}}}}\, \\ \,\href{Ledger.Conway.Certs.html#6364}{\htmlId{9569}{\htmlClass{Generalizable}{\text{mc}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{9572}{\htmlClass{Field Operator}{\text{❵}}}}\, \,\href{Axiom.Set.Map.html#6320}{\htmlId{9574}{\htmlClass{Function Operator}{\text{∪ˡ}}}}\, \,\href{Ledger.Conway.Certs.html#6004}{\htmlId{9577}{\htmlClass{Generalizable}{\text{ccKeys}}}}\, \end{pmatrix}$


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


  CERT-deleg :
    ∙ $\begin{pmatrix} \,\href{Ledger.Conway.Certs.html#6580}{\htmlId{9638}{\htmlClass{Generalizable}{\text{pp}}}}\, \\ \,\href{Ledger.Conway.Certs.html#3841}{\htmlId{9643}{\htmlClass{Field}{\text{PState.pools}}}}\, \,\href{Ledger.Conway.Certs.html#6674}{\htmlId{9656}{\htmlClass{Generalizable}{\text{stᵖ}}}}\, \\ \,\href{Class.IsSet.html#916}{\htmlId{9662}{\htmlClass{Function}{\text{dom}}}}\, (\,\href{Ledger.Conway.Certs.html#4082}{\htmlId{9667}{\htmlClass{Field}{\text{GState.dreps}}}}\, \,\href{Ledger.Conway.Certs.html#6654}{\htmlId{9680}{\htmlClass{Generalizable}{\text{stᵍ}}}}\,) \end{pmatrix}$ ⊢ stᵈ ⇀⦇ dCert ,DELEG⦈ stᵈ'
      ────────────────────────────────
      $\begin{pmatrix} \,\href{Ledger.Conway.Certs.html#6448}{\htmlId{9762}{\htmlClass{Generalizable}{\text{e}}}}\, \\ \,\href{Ledger.Conway.Certs.html#6580}{\htmlId{9766}{\htmlClass{Generalizable}{\text{pp}}}}\, \\ \,\href{Ledger.Conway.Certs.html#6470}{\htmlId{9771}{\htmlClass{Generalizable}{\text{vs}}}}\, \\ \,\href{Ledger.Conway.Certs.html#6199}{\htmlId{9776}{\htmlClass{Generalizable}{\text{wdrls}}}}\, \\ \,\href{Ledger.Conway.Certs.html#6694}{\htmlId{9784}{\htmlClass{Generalizable}{\text{cc}}}}\, \end{pmatrix}$ ⊢ $\begin{pmatrix} \,\href{Ledger.Conway.Certs.html#6634}{\htmlId{9793}{\htmlClass{Generalizable}{\text{stᵈ}}}}\, \\ \,\href{Ledger.Conway.Certs.html#6674}{\htmlId{9799}{\htmlClass{Generalizable}{\text{stᵖ}}}}\, \\ \,\href{Ledger.Conway.Certs.html#6654}{\htmlId{9805}{\htmlClass{Generalizable}{\text{stᵍ}}}}\, \end{pmatrix}$ ⇀⦇ dCert ,CERT⦈ $\begin{pmatrix} \,\href{Ledger.Conway.Certs.html#6638}{\htmlId{9829}{\htmlClass{Generalizable}{\text{stᵈ'}}}}\, \\ \,\href{Ledger.Conway.Certs.html#6674}{\htmlId{9836}{\htmlClass{Generalizable}{\text{stᵖ}}}}\, \\ \,\href{Ledger.Conway.Certs.html#6654}{\htmlId{9842}{\htmlClass{Generalizable}{\text{stᵍ}}}}\, \end{pmatrix}$

  CERT-pool :
    ∙ pp ⊢ stᵖ ⇀⦇ dCert ,POOL⦈ stᵖ'
      ────────────────────────────────
      $\begin{pmatrix} \,\href{Ledger.Conway.Certs.html#6448}{\htmlId{9946}{\htmlClass{Generalizable}{\text{e}}}}\, \\ \,\href{Ledger.Conway.Certs.html#6580}{\htmlId{9950}{\htmlClass{Generalizable}{\text{pp}}}}\, \\ \,\href{Ledger.Conway.Certs.html#6470}{\htmlId{9955}{\htmlClass{Generalizable}{\text{vs}}}}\, \\ \,\href{Ledger.Conway.Certs.html#6199}{\htmlId{9960}{\htmlClass{Generalizable}{\text{wdrls}}}}\, \\ \,\href{Ledger.Conway.Certs.html#6694}{\htmlId{9968}{\htmlClass{Generalizable}{\text{cc}}}}\, \end{pmatrix}$ ⊢ $\begin{pmatrix} \,\href{Ledger.Conway.Certs.html#6634}{\htmlId{9977}{\htmlClass{Generalizable}{\text{stᵈ}}}}\, \\ \,\href{Ledger.Conway.Certs.html#6674}{\htmlId{9983}{\htmlClass{Generalizable}{\text{stᵖ}}}}\, \\ \,\href{Ledger.Conway.Certs.html#6654}{\htmlId{9989}{\htmlClass{Generalizable}{\text{stᵍ}}}}\, \end{pmatrix}$ ⇀⦇ dCert ,CERT⦈ $\begin{pmatrix} \,\href{Ledger.Conway.Certs.html#6634}{\htmlId{10013}{\htmlClass{Generalizable}{\text{stᵈ}}}}\, \\ \,\href{Ledger.Conway.Certs.html#6678}{\htmlId{10019}{\htmlClass{Generalizable}{\text{stᵖ'}}}}\, \\ \,\href{Ledger.Conway.Certs.html#6654}{\htmlId{10026}{\htmlClass{Generalizable}{\text{stᵍ}}}}\, \end{pmatrix}$

  CERT-vdel :
    ∙ Γ ⊢ stᵍ ⇀⦇ dCert ,GOVCERT⦈ stᵍ'
      ────────────────────────────────
      Γ ⊢ $\begin{pmatrix} \,\href{Ledger.Conway.Certs.html#6634}{\htmlId{10136}{\htmlClass{Generalizable}{\text{stᵈ}}}}\, \\ \,\href{Ledger.Conway.Certs.html#6674}{\htmlId{10142}{\htmlClass{Generalizable}{\text{stᵖ}}}}\, \\ \,\href{Ledger.Conway.Certs.html#6654}{\htmlId{10148}{\htmlClass{Generalizable}{\text{stᵍ}}}}\, \end{pmatrix}$ ⇀⦇ dCert ,CERT⦈ $\begin{pmatrix} \,\href{Ledger.Conway.Certs.html#6634}{\htmlId{10172}{\htmlClass{Generalizable}{\text{stᵈ}}}}\, \\ \,\href{Ledger.Conway.Certs.html#6674}{\htmlId{10178}{\htmlClass{Generalizable}{\text{stᵖ}}}}\, \\ \,\href{Ledger.Conway.Certs.html#6658}{\htmlId{10184}{\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#6448}{\htmlId{10760}{\htmlClass{Generalizable}{\text{e}}}}\, \\ \,\href{Ledger.Conway.Certs.html#6580}{\htmlId{10764}{\htmlClass{Generalizable}{\text{pp}}}}\, \\ \,\href{Ledger.Conway.Certs.html#6470}{\htmlId{10769}{\htmlClass{Generalizable}{\text{vs}}}}\, \\ \,\href{Ledger.Conway.Certs.html#6199}{\htmlId{10774}{\htmlClass{Generalizable}{\text{wdrls}}}}\, \\ \,\href{Ledger.Conway.Certs.html#6694}{\htmlId{10782}{\htmlClass{Generalizable}{\text{cc}}}}\, \end{pmatrix}$ ⊢
        $\begin{pmatrix} \begin{pmatrix} \,\href{Ledger.Conway.Certs.html#6069}{\htmlId{10801}{\htmlClass{Generalizable}{\text{voteDelegs}}}}\, \\ \,\href{Ledger.Conway.Certs.html#5964}{\htmlId{10814}{\htmlClass{Generalizable}{\text{stakeDelegs}}}}\, \\ \,\href{Ledger.Conway.Certs.html#5893}{\htmlId{10828}{\htmlClass{Generalizable}{\text{rewards}}}}\, \end{pmatrix}
        \\ \,\href{Ledger.Conway.Certs.html#6674}{\htmlId{10848}{\htmlClass{Generalizable}{\text{stᵖ}}}}\,
        \\ \begin{pmatrix} \,\href{Ledger.Conway.Certs.html#5923}{\htmlId{10864}{\htmlClass{Generalizable}{\text{dReps}}}}\, \\ \,\href{Ledger.Conway.Certs.html#6011}{\htmlId{10872}{\htmlClass{Generalizable}{\text{ccHotKeys}}}}\, \end{pmatrix}
        \end{pmatrix}$ ⇀⦇ _ ,CERTBASE⦈
        $\begin{pmatrix} \begin{pmatrix} \,\href{Ledger.Conway.Certs.html#10451}{\htmlId{10922}{\htmlClass{Bound}{\text{validVoteDelegs}}}}\, \\ \,\href{Ledger.Conway.Certs.html#5964}{\htmlId{10940}{\htmlClass{Generalizable}{\text{stakeDelegs}}}}\, \\ \,\href{Axiom.Set.Map.html#9130}{\htmlId{10954}{\htmlClass{Function}{\text{constMap}}}}\, \,\href{Ledger.Conway.Certs.html#10401}{\htmlId{10963}{\htmlClass{Bound}{\text{wdrlCreds}}}}\, \,\htmlId{10973}{\htmlClass{Number}{\text{0}}}\, \,\href{Axiom.Set.Map.html#6320}{\htmlId{10975}{\htmlClass{Function Operator}{\text{∪ˡ}}}}\, \,\href{Ledger.Conway.Certs.html#5893}{\htmlId{10978}{\htmlClass{Generalizable}{\text{rewards}}}}\, \end{pmatrix}
        \\ \,\href{Ledger.Conway.Certs.html#6674}{\htmlId{10998}{\htmlClass{Generalizable}{\text{stᵖ}}}}\,
        \\ \begin{pmatrix} \,\href{Ledger.Conway.Certs.html#10310}{\htmlId{11014}{\htmlClass{Bound}{\text{refreshedDReps}}}}\, \\ \,\href{Ledger.Conway.Certs.html#6011}{\htmlId{11031}{\htmlClass{Generalizable}{\text{ccHotKeys}}}}\, \end{pmatrix}
        \end{pmatrix}$