Ledger.Conway.Conformance.Certs

{-# OPTIONS --safe #-}

open import Ledger.Prelude
open import Ledger.Conway.Specification.Gov.Base
import Ledger.Conway.Specification.Certs

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


open import Ledger.Conway.Specification.Gov.Actions gs
private module Certs = Ledger.Conway.Specification.Certs gs
open Certs public
  hiding (DState; GState; CertState; HasCast-DState; HasCast-GState; HasCast-CertState;
          _⊢_⇀⦇_,POOL⦈_; _⊢_⇀⦇_,DELEG⦈_; _⊢_⇀⦇_,GOVCERT⦈_;
          _⊢_⇀⦇_,CERT⦈_; _⊢_⇀⦇_,PRE-CERT⦈_; _⊢_⇀⦇_,POST-CERT⦈_; _⊢_⇀⦇_,CERTS⦈_; ⟦_,_,_⟧ᵈ)
open RwdAddr

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

record GState : Type where
  constructor ⟦_,_,_⟧ᵛ
  field
    dreps      : Credential ⇀ Epoch
    ccHotKeys  : Credential ⇀ Maybe Credential
    deposits   : Deposits

record CertState : Type where
  constructor ⟦_,_,_⟧ᶜˢ
  field
    dState : DState
    pState : PState
    gState : GState

instance
  unquoteDecl HasCast-DState HasCast-GState HasCast-CertState = derive-HasCast
    (   (quote DState , HasCast-DState)
    ∷   (quote GState , HasCast-GState)
    ∷ [ (quote CertState , HasCast-CertState) ])

certDeposit : DCert → PParams → Deposits
certDeposit (delegate c _ _ v) _   = ❴ CredentialDeposit c , v ❵
certDeposit (regdrep c v _)    _   = ❴ DRepDeposit c , v ❵
certDeposit (reg c v)          pp  = ❴ CredentialDeposit c , pp .PParams.keyDeposit ❵
certDeposit _                  _   = ∅
-- handled in the Utxo module:
-- certDeposit (regpool kh _)     pp  = ❴ PoolDeposit kh , pp .poolDeposit ❵

certRefund : DCert → ℙ DepositPurpose
certRefund (dereg c _)      = ❴ CredentialDeposit c ❵
certRefund (deregdrep c _)  = ❴ DRepDeposit c ❵
certRefund _                = ∅

updateCertDeposit  : PParams → DCert → Deposits → Deposits
updateCertDeposit pp (delegate c _ _ v) deposits = deposits ∪⁺ ❴ CredentialDeposit c , v ❵
updateCertDeposit pp (reg c _)          deposits = deposits ∪⁺ ❴ CredentialDeposit c , pp .PParams.keyDeposit ❵
updateCertDeposit pp (regdrep c v _)    deposits = deposits ∪⁺ ❴ DRepDeposit c , v ❵
updateCertDeposit pp (dereg c _)        deposits = deposits ∣ ❴ CredentialDeposit c ❵ ᶜ
updateCertDeposit pp (deregdrep c _)    deposits = deposits ∣ ❴ DRepDeposit c ❵ ᶜ
updateCertDeposit pp (regpool kh _)     deposits = deposits ∪⁺ ❴ PoolDeposit kh , pp .PParams.poolDeposit ❵
updateCertDeposit _ (retirepool _ _)    deposits = deposits
updateCertDeposit _ (ccreghot _ _)      deposits = deposits
-- updateCertDeposit pp cert deposits
--   = (deposits ∪⁺ certDeposit cert pp) ∣ certRefund cert ᶜ

private variable
  rwds rewards           : Rewards
  dReps                  : Credential ⇀ Epoch
  sDelegs stakeDelegs    : Credential ⇀ KeyHash
  ccKeys ccHotKeys       : Credential ⇀ Maybe Credential
  vDelegs voteDelegs     : VoteDelegs
  pools fPools           : Pools
  retiring               : KeyHash ⇀ Epoch
  wdrls                  : Withdrawals

  an             : Anchor
  Γ              : CertEnv
  d              : Coin
  md             : Maybe Coin
  c              : Credential
  mc             : Maybe Credential
  delegatees cc  : ℙ Credential
  dCert          : DCert
  dep ddep gdep  : Deposits
  e              : Epoch
  vs             : List GovVote
  kh             : KeyHash
  mkh            : Maybe KeyHash
  poolParams     : StakePoolParams
  pp             : PParams
  mv             : Maybe VDeleg

  stᵈ stᵈ' : DState
  stᵍ stᵍ' : GState
  stᵖ stᵖ' : PState

open GovVote

data _⊢_⇀⦇_,POOL⦈_  : PoolEnv → PState → DCert → PState → Type
data _⊢_⇀⦇_,DELEG⦈_ : DelegEnv → DState → DCert → DState → Type

data _⊢_⇀⦇_,POOL⦈_ where
  POOL-regpool :
    ∙ kh ∉ dom pools
      ────────────────────────────────
      pp ⊢  $\begin{pmatrix} \,\href{Ledger.Conway.Conformance.Certs.html#2965}{\htmlId{3868}{\htmlClass{Generalizable}{\text{pools}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#2971}{\htmlId{3876}{\htmlClass{Generalizable}{\text{fPools}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#2998}{\htmlId{3885}{\htmlClass{Generalizable}{\text{retiring}}}}\, \end{pmatrix}$ ⇀⦇ regpool kh poolParams ,POOL⦈
            $\begin{pmatrix} \,\href{Class.HasSingleton.html#288}{\htmlId{3942}{\htmlClass{Field Operator}{\text{❴}}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#3396}{\htmlId{3944}{\htmlClass{Generalizable}{\text{kh}}}}\, , \,\href{Ledger.Conway.Conformance.Certs.html#3456}{\htmlId{3949}{\htmlClass{Generalizable}{\text{poolParams}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{3960}{\htmlClass{Field Operator}{\text{❵}}}}\, \,\href{Axiom.Set.Map.html#7638}{\htmlId{3962}{\htmlClass{Function Operator}{\text{∪ˡ}}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#2965}{\htmlId{3965}{\htmlClass{Generalizable}{\text{pools}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#2971}{\htmlId{3973}{\htmlClass{Generalizable}{\text{fPools}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#2998}{\htmlId{3982}{\htmlClass{Generalizable}{\text{retiring}}}}\, \end{pmatrix}$

  POOL-retirepool :
    ────────────────────────────────
    pp ⊢ $\begin{pmatrix} \,\href{Ledger.Conway.Conformance.Certs.html#2965}{\htmlId{4062}{\htmlClass{Generalizable}{\text{pools}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#2971}{\htmlId{4070}{\htmlClass{Generalizable}{\text{fPools}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#2998}{\htmlId{4079}{\htmlClass{Generalizable}{\text{retiring}}}}\, \end{pmatrix}$ ⇀⦇ retirepool kh e ,POOL⦈ $\begin{pmatrix} \,\href{Ledger.Conway.Conformance.Certs.html#2965}{\htmlId{4118}{\htmlClass{Generalizable}{\text{pools}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#2971}{\htmlId{4126}{\htmlClass{Generalizable}{\text{fPools}}}}\, \\ \,\href{Class.HasSingleton.html#288}{\htmlId{4135}{\htmlClass{Field Operator}{\text{❴}}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#3396}{\htmlId{4137}{\htmlClass{Generalizable}{\text{kh}}}}\, , \,\href{Ledger.Conway.Conformance.Certs.html#3339}{\htmlId{4142}{\htmlClass{Generalizable}{\text{e}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{4144}{\htmlClass{Field Operator}{\text{❵}}}}\, \,\href{Axiom.Set.Map.html#7638}{\htmlId{4146}{\htmlClass{Function Operator}{\text{∪ˡ}}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#2998}{\htmlId{4149}{\htmlClass{Generalizable}{\text{retiring}}}}\, \end{pmatrix}$

data _⊢_⇀⦇_,DELEG⦈_ where
  DELEG-delegate : let open PParams pp in
    ∙ (c ∉ dom rwds → d ≡ keyDeposit)
    ∙ (c ∈ dom rwds → d ≡ 0)
    ∙ mv ∈ mapˢ (just ∘ vDelegCredential) delegatees ∪
        fromList
          ( nothing
          ∷ just vDelegAbstain
          ∷ just vDelegNoConfidence
          ∷ []
          )
    ∙ mkh ∈ mapˢ just (dom pools) ∪ ❴ nothing ❵
      ────────────────────────────────
      $\begin{pmatrix} \,\href{Ledger.Conway.Conformance.Certs.html#3491}{\htmlId{4577}{\htmlClass{Generalizable}{\text{pp}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#2965}{\htmlId{4582}{\htmlClass{Generalizable}{\text{pools}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3254}{\htmlId{4590}{\htmlClass{Generalizable}{\text{delegatees}}}}\, \end{pmatrix}$ ⊢
      $\begin{pmatrix} \,\href{Ledger.Conway.Conformance.Certs.html#2927}{\htmlId{4613}{\htmlClass{Generalizable}{\text{vDelegs}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#2822}{\htmlId{4623}{\htmlClass{Generalizable}{\text{sDelegs}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#2741}{\htmlId{4633}{\htmlClass{Generalizable}{\text{rwds}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3311}{\htmlId{4640}{\htmlClass{Generalizable}{\text{dep}}}}\, \end{pmatrix}$
      ⇀⦇ delegate c mv mkh d ,DELEG⦈
      $\begin{pmatrix} \,\href{Axiom.Set.Map.html#9260}{\htmlId{4691}{\htmlClass{Function}{\text{insertIfJust}}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#3188}{\htmlId{4704}{\htmlClass{Generalizable}{\text{c}}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#3518}{\htmlId{4706}{\htmlClass{Generalizable}{\text{mv}}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#2927}{\htmlId{4709}{\htmlClass{Generalizable}{\text{vDelegs}}}}\, \\ \,\href{Axiom.Set.Map.html#9260}{\htmlId{4719}{\htmlClass{Function}{\text{insertIfJust}}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#3188}{\htmlId{4732}{\htmlClass{Generalizable}{\text{c}}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#3423}{\htmlId{4734}{\htmlClass{Generalizable}{\text{mkh}}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#2822}{\htmlId{4738}{\htmlClass{Generalizable}{\text{sDelegs}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#2741}{\htmlId{4748}{\htmlClass{Generalizable}{\text{rwds}}}}\, \,\href{Axiom.Set.Map.html#7638}{\htmlId{4753}{\htmlClass{Function Operator}{\text{∪ˡ}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{4756}{\htmlClass{Field Operator}{\text{❴}}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#3188}{\htmlId{4758}{\htmlClass{Generalizable}{\text{c}}}}\, , \,\htmlId{4762}{\htmlClass{Number}{\text{0}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{4764}{\htmlClass{Field Operator}{\text{❵}}}}\,
      \\ \,\href{Ledger.Conway.Conformance.Certs.html#1877}{\htmlId{4774}{\htmlClass{Function}{\text{updateCertDeposit}}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#3491}{\htmlId{4792}{\htmlClass{Generalizable}{\text{pp}}}}\, \,\htmlId{4795}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Conway.Specification.Certs.html#2259}{\htmlId{4796}{\htmlClass{InductiveConstructor}{\text{delegate}}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#3188}{\htmlId{4805}{\htmlClass{Generalizable}{\text{c}}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#3518}{\htmlId{4807}{\htmlClass{Generalizable}{\text{mv}}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#3423}{\htmlId{4810}{\htmlClass{Generalizable}{\text{mkh}}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#3134}{\htmlId{4814}{\htmlClass{Generalizable}{\text{d}}}}\,\,\htmlId{4815}{\htmlClass{Symbol}{\text{)}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#3311}{\htmlId{4817}{\htmlClass{Generalizable}{\text{dep}}}}\, \end{pmatrix}$

  DELEG-dereg :
    ∙ (c , 0) ∈ rwds
    ∙ (CredentialDeposit c , d) ∈ dep
    ∙ md ≡ nothing ⊎ md ≡ just d
      ────────────────────────────────
      $\begin{pmatrix} \,\href{Ledger.Conway.Conformance.Certs.html#3491}{\htmlId{4979}{\htmlClass{Generalizable}{\text{pp}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#2965}{\htmlId{4984}{\htmlClass{Generalizable}{\text{pools}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3254}{\htmlId{4992}{\htmlClass{Generalizable}{\text{delegatees}}}}\, \end{pmatrix}$ ⊢
      $\begin{pmatrix} \,\href{Ledger.Conway.Conformance.Certs.html#2927}{\htmlId{5015}{\htmlClass{Generalizable}{\text{vDelegs}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#2822}{\htmlId{5025}{\htmlClass{Generalizable}{\text{sDelegs}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#2741}{\htmlId{5035}{\htmlClass{Generalizable}{\text{rwds}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3311}{\htmlId{5042}{\htmlClass{Generalizable}{\text{dep}}}}\, \end{pmatrix}$
      ⇀⦇ dereg c md ,DELEG⦈
      $\begin{pmatrix} \,\href{Ledger.Conway.Conformance.Certs.html#2927}{\htmlId{5084}{\htmlClass{Generalizable}{\text{vDelegs}}}}\, \,\href{Axiom.Set.Map.html#12840}{\htmlId{5092}{\htmlClass{Function Operator}{\text{∣}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{5094}{\htmlClass{Field Operator}{\text{❴}}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#3188}{\htmlId{5096}{\htmlClass{Generalizable}{\text{c}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{5098}{\htmlClass{Field Operator}{\text{❵}}}}\, \,\href{Axiom.Set.Map.html#12840}{\htmlId{5100}{\htmlClass{Function Operator}{\text{ᶜ}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#2822}{\htmlId{5104}{\htmlClass{Generalizable}{\text{sDelegs}}}}\, \,\href{Axiom.Set.Map.html#12840}{\htmlId{5112}{\htmlClass{Function Operator}{\text{∣}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{5114}{\htmlClass{Field Operator}{\text{❴}}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#3188}{\htmlId{5116}{\htmlClass{Generalizable}{\text{c}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{5118}{\htmlClass{Field Operator}{\text{❵}}}}\, \,\href{Axiom.Set.Map.html#12840}{\htmlId{5120}{\htmlClass{Function Operator}{\text{ᶜ}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#2741}{\htmlId{5124}{\htmlClass{Generalizable}{\text{rwds}}}}\, \,\href{Axiom.Set.Map.html#12840}{\htmlId{5129}{\htmlClass{Function Operator}{\text{∣}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{5131}{\htmlClass{Field Operator}{\text{❴}}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#3188}{\htmlId{5133}{\htmlClass{Generalizable}{\text{c}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{5135}{\htmlClass{Field Operator}{\text{❵}}}}\, \,\href{Axiom.Set.Map.html#12840}{\htmlId{5137}{\htmlClass{Function Operator}{\text{ᶜ}}}}\,
      \\ \,\href{Ledger.Conway.Conformance.Certs.html#1877}{\htmlId{5147}{\htmlClass{Function}{\text{updateCertDeposit}}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#3491}{\htmlId{5165}{\htmlClass{Generalizable}{\text{pp}}}}\, \,\htmlId{5168}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Conway.Specification.Certs.html#2332}{\htmlId{5169}{\htmlClass{InductiveConstructor}{\text{dereg}}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#3188}{\htmlId{5175}{\htmlClass{Generalizable}{\text{c}}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#3158}{\htmlId{5177}{\htmlClass{Generalizable}{\text{md}}}}\,\,\htmlId{5179}{\htmlClass{Symbol}{\text{)}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#3311}{\htmlId{5181}{\htmlClass{Generalizable}{\text{dep}}}}\, \end{pmatrix}$

  DELEG-reg : let open PParams pp in
    ∙ c ∉ dom rwds
    ∙ d ≡ keyDeposit ⊎ d ≡ 0
      ────────────────────────────────
      $\begin{pmatrix} \,\href{Ledger.Conway.Conformance.Certs.html#3491}{\htmlId{5320}{\htmlClass{Generalizable}{\text{pp}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#2965}{\htmlId{5325}{\htmlClass{Generalizable}{\text{pools}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3254}{\htmlId{5333}{\htmlClass{Generalizable}{\text{delegatees}}}}\, \end{pmatrix}$ ⊢
        $\begin{pmatrix} \,\href{Ledger.Conway.Conformance.Certs.html#2927}{\htmlId{5358}{\htmlClass{Generalizable}{\text{vDelegs}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#2822}{\htmlId{5368}{\htmlClass{Generalizable}{\text{sDelegs}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#2741}{\htmlId{5378}{\htmlClass{Generalizable}{\text{rwds}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3311}{\htmlId{5385}{\htmlClass{Generalizable}{\text{dep}}}}\, \end{pmatrix}$ ⇀⦇ reg c d ,DELEG⦈
        $\begin{pmatrix} \,\href{Ledger.Conway.Conformance.Certs.html#2927}{\htmlId{5420}{\htmlClass{Generalizable}{\text{vDelegs}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#2822}{\htmlId{5430}{\htmlClass{Generalizable}{\text{sDelegs}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#2741}{\htmlId{5440}{\htmlClass{Generalizable}{\text{rwds}}}}\, \,\href{Axiom.Set.Map.html#7638}{\htmlId{5445}{\htmlClass{Function Operator}{\text{∪ˡ}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{5448}{\htmlClass{Field Operator}{\text{❴}}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#3188}{\htmlId{5450}{\htmlClass{Generalizable}{\text{c}}}}\, , \,\htmlId{5454}{\htmlClass{Number}{\text{0}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{5456}{\htmlClass{Field Operator}{\text{❵}}}}\,
        \\ \,\href{Ledger.Conway.Conformance.Certs.html#1877}{\htmlId{5468}{\htmlClass{Function}{\text{updateCertDeposit}}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#3491}{\htmlId{5486}{\htmlClass{Generalizable}{\text{pp}}}}\, \,\htmlId{5489}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Conway.Specification.Certs.html#2951}{\htmlId{5490}{\htmlClass{InductiveConstructor}{\text{reg}}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#3188}{\htmlId{5494}{\htmlClass{Generalizable}{\text{c}}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#3134}{\htmlId{5496}{\htmlClass{Generalizable}{\text{d}}}}\,\,\htmlId{5497}{\htmlClass{Symbol}{\text{)}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#3311}{\htmlId{5499}{\htmlClass{Generalizable}{\text{dep}}}}\, \end{pmatrix}$

data _⊢_⇀⦇_,GOVCERT⦈_ : CertEnv → GState → DCert → GState → Type where
  GOVCERT-regdrep : ∀ {pp} → let open PParams pp in
    ∙ (d ≡ drepDeposit × c ∉ dom dReps) ⊎ (d ≡ 0 × c ∈ dom dReps)
      ────────────────────────────────
      $\begin{pmatrix} \,\href{Ledger.Conway.Conformance.Certs.html#3339}{\htmlId{5742}{\htmlClass{Generalizable}{\text{e}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#5600}{\htmlId{5746}{\htmlClass{Bound}{\text{pp}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3364}{\htmlId{5751}{\htmlClass{Generalizable}{\text{vs}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3041}{\htmlId{5756}{\htmlClass{Generalizable}{\text{wdrls}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3265}{\htmlId{5764}{\htmlClass{Generalizable}{\text{cc}}}}\, \end{pmatrix}$ ⊢
      $\begin{pmatrix} \,\href{Ledger.Conway.Conformance.Certs.html#2776}{\htmlId{5779}{\htmlClass{Generalizable}{\text{dReps}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#2870}{\htmlId{5787}{\htmlClass{Generalizable}{\text{ccKeys}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3311}{\htmlId{5796}{\htmlClass{Generalizable}{\text{dep}}}}\, \end{pmatrix}$
        ⇀⦇ regdrep c d an ,GOVCERT⦈
      $\begin{pmatrix} \,\href{Class.HasSingleton.html#288}{\htmlId{5846}{\htmlClass{Field Operator}{\text{❴}}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#3188}{\htmlId{5848}{\htmlClass{Generalizable}{\text{c}}}}\, , \,\href{Ledger.Conway.Conformance.Certs.html#3339}{\htmlId{5852}{\htmlClass{Generalizable}{\text{e}}}}\, \,\href{Class.HasAdd.Core.html#162}{\htmlId{5854}{\htmlClass{Field Operator}{\text{+}}}}\, \,\href{Ledger.Conway.Specification.PParams.html#3442}{\htmlId{5856}{\htmlClass{Field}{\text{drepActivity}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{5869}{\htmlClass{Field Operator}{\text{❵}}}}\, \,\href{Axiom.Set.Map.html#7638}{\htmlId{5871}{\htmlClass{Function Operator}{\text{∪ˡ}}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#2776}{\htmlId{5874}{\htmlClass{Generalizable}{\text{dReps}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#2870}{\htmlId{5882}{\htmlClass{Generalizable}{\text{ccKeys}}}}\,
      \\ \,\href{Ledger.Conway.Conformance.Certs.html#1877}{\htmlId{5897}{\htmlClass{Function}{\text{updateCertDeposit}}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#5600}{\htmlId{5915}{\htmlClass{Bound}{\text{pp}}}}\, \,\htmlId{5918}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Conway.Specification.Certs.html#2470}{\htmlId{5919}{\htmlClass{InductiveConstructor}{\text{regdrep}}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#3188}{\htmlId{5927}{\htmlClass{Generalizable}{\text{c}}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#3134}{\htmlId{5929}{\htmlClass{Generalizable}{\text{d}}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#3081}{\htmlId{5931}{\htmlClass{Generalizable}{\text{an}}}}\, \,\htmlId{5934}{\htmlClass{Symbol}{\text{)}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#3311}{\htmlId{5936}{\htmlClass{Generalizable}{\text{dep}}}}\, \end{pmatrix}$

  GOVCERT-deregdrep :
    ∙ c ∈ dom dReps
    ∙ (DRepDeposit c , d) ∈ dep
      ────────────────────────────────
      $\begin{pmatrix} \,\href{Ledger.Conway.Conformance.Certs.html#3339}{\htmlId{6064}{\htmlClass{Generalizable}{\text{e}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3491}{\htmlId{6068}{\htmlClass{Generalizable}{\text{pp}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3364}{\htmlId{6073}{\htmlClass{Generalizable}{\text{vs}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3041}{\htmlId{6078}{\htmlClass{Generalizable}{\text{wdrls}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3265}{\htmlId{6086}{\htmlClass{Generalizable}{\text{cc}}}}\, \end{pmatrix}$ ⊢ $\begin{pmatrix} \,\href{Ledger.Conway.Conformance.Certs.html#2776}{\htmlId{6095}{\htmlClass{Generalizable}{\text{dReps}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#2870}{\htmlId{6103}{\htmlClass{Generalizable}{\text{ccKeys}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3311}{\htmlId{6112}{\htmlClass{Generalizable}{\text{dep}}}}\, \end{pmatrix}$
          ⇀⦇ deregdrep c d ,GOVCERT⦈
          $\begin{pmatrix} \,\href{Ledger.Conway.Conformance.Certs.html#2776}{\htmlId{6167}{\htmlClass{Generalizable}{\text{dReps}}}}\, \,\href{Axiom.Set.Map.html#12840}{\htmlId{6173}{\htmlClass{Function Operator}{\text{∣}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{6175}{\htmlClass{Field Operator}{\text{❴}}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#3188}{\htmlId{6177}{\htmlClass{Generalizable}{\text{c}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{6179}{\htmlClass{Field Operator}{\text{❵}}}}\, \,\href{Axiom.Set.Map.html#12840}{\htmlId{6181}{\htmlClass{Function Operator}{\text{ᶜ}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#2870}{\htmlId{6185}{\htmlClass{Generalizable}{\text{ccKeys}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#1877}{\htmlId{6194}{\htmlClass{Function}{\text{updateCertDeposit}}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#3491}{\htmlId{6212}{\htmlClass{Generalizable}{\text{pp}}}}\, \,\htmlId{6215}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Conway.Specification.Certs.html#2521}{\htmlId{6216}{\htmlClass{InductiveConstructor}{\text{deregdrep}}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#3188}{\htmlId{6226}{\htmlClass{Generalizable}{\text{c}}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#3134}{\htmlId{6228}{\htmlClass{Generalizable}{\text{d}}}}\,\,\htmlId{6229}{\htmlClass{Symbol}{\text{)}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#3311}{\htmlId{6231}{\htmlClass{Generalizable}{\text{dep}}}}\, \end{pmatrix}$

  GOVCERT-ccreghot :
    ∙ (c , nothing) ∉ ccKeys
    ∙ c ∈ cc
      ────────────────────────────────
      $\begin{pmatrix} \,\href{Ledger.Conway.Conformance.Certs.html#3339}{\htmlId{6348}{\htmlClass{Generalizable}{\text{e}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3491}{\htmlId{6352}{\htmlClass{Generalizable}{\text{pp}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3364}{\htmlId{6357}{\htmlClass{Generalizable}{\text{vs}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3041}{\htmlId{6362}{\htmlClass{Generalizable}{\text{wdrls}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3265}{\htmlId{6370}{\htmlClass{Generalizable}{\text{cc}}}}\, \end{pmatrix}$ ⊢ $\begin{pmatrix} \,\href{Ledger.Conway.Conformance.Certs.html#2776}{\htmlId{6379}{\htmlClass{Generalizable}{\text{dReps}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#2870}{\htmlId{6387}{\htmlClass{Generalizable}{\text{ccKeys}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3311}{\htmlId{6396}{\htmlClass{Generalizable}{\text{dep}}}}\, \end{pmatrix}$
          ⇀⦇ ccreghot c mc ,GOVCERT⦈
          $\begin{pmatrix} \,\href{Ledger.Conway.Conformance.Certs.html#2776}{\htmlId{6451}{\htmlClass{Generalizable}{\text{dReps}}}}\, \\ \,\href{Class.HasSingleton.html#288}{\htmlId{6459}{\htmlClass{Field Operator}{\text{❴}}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#3188}{\htmlId{6461}{\htmlClass{Generalizable}{\text{c}}}}\, , \,\href{Ledger.Conway.Conformance.Certs.html#3218}{\htmlId{6465}{\htmlClass{Generalizable}{\text{mc}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{6468}{\htmlClass{Field Operator}{\text{❵}}}}\, \,\href{Axiom.Set.Map.html#7638}{\htmlId{6470}{\htmlClass{Function Operator}{\text{∪ˡ}}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#2870}{\htmlId{6473}{\htmlClass{Generalizable}{\text{ccKeys}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#1877}{\htmlId{6482}{\htmlClass{Function}{\text{updateCertDeposit}}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#3491}{\htmlId{6500}{\htmlClass{Generalizable}{\text{pp}}}}\, \,\htmlId{6503}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Conway.Specification.Certs.html#2563}{\htmlId{6504}{\htmlClass{InductiveConstructor}{\text{ccreghot}}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#3188}{\htmlId{6513}{\htmlClass{Generalizable}{\text{c}}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#3218}{\htmlId{6515}{\htmlClass{Generalizable}{\text{mc}}}}\,\,\htmlId{6517}{\htmlClass{Symbol}{\text{)}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#3311}{\htmlId{6519}{\htmlClass{Generalizable}{\text{dep}}}}\, \end{pmatrix}$

data _⊢_⇀⦇_,CERT⦈_ : CertEnv → CertState → DCert → CertState → Type where
  CERT-deleg :
    ∙ $\begin{pmatrix} \,\href{Ledger.Conway.Conformance.Certs.html#3491}{\htmlId{6623}{\htmlClass{Generalizable}{\text{pp}}}}\, \\ \,\href{Ledger.Conway.Specification.Certs.html#4063}{\htmlId{6628}{\htmlClass{Field}{\text{PState.pools}}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#3591}{\htmlId{6641}{\htmlClass{Generalizable}{\text{stᵖ}}}}\, \\ \,\href{Class.IsSet.html#916}{\htmlId{6647}{\htmlClass{Function}{\text{dom}}}}\, \,\htmlId{6651}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Conway.Conformance.Certs.html#858}{\htmlId{6652}{\htmlClass{Field}{\text{GState.dreps}}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#3571}{\htmlId{6665}{\htmlClass{Generalizable}{\text{stᵍ}}}}\,\,\htmlId{6668}{\htmlClass{Symbol}{\text{)}}}\, \end{pmatrix}$ ⊢ stᵈ ⇀⦇ dCert ,DELEG⦈ stᵈ'
      ────────────────────────────────
      $\begin{pmatrix} \,\href{Ledger.Conway.Conformance.Certs.html#3339}{\htmlId{6747}{\htmlClass{Generalizable}{\text{e}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3491}{\htmlId{6751}{\htmlClass{Generalizable}{\text{pp}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3364}{\htmlId{6756}{\htmlClass{Generalizable}{\text{vs}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3041}{\htmlId{6761}{\htmlClass{Generalizable}{\text{wdrls}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3265}{\htmlId{6769}{\htmlClass{Generalizable}{\text{cc}}}}\, \end{pmatrix}$ ⊢ $\begin{pmatrix} \,\href{Ledger.Conway.Conformance.Certs.html#3551}{\htmlId{6778}{\htmlClass{Generalizable}{\text{stᵈ}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3591}{\htmlId{6784}{\htmlClass{Generalizable}{\text{stᵖ}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3571}{\htmlId{6790}{\htmlClass{Generalizable}{\text{stᵍ}}}}\, \end{pmatrix}$ ⇀⦇ dCert ,CERT⦈ $\begin{pmatrix} \,\href{Ledger.Conway.Conformance.Certs.html#3555}{\htmlId{6814}{\htmlClass{Generalizable}{\text{stᵈ'}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3591}{\htmlId{6821}{\htmlClass{Generalizable}{\text{stᵖ}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3571}{\htmlId{6827}{\htmlClass{Generalizable}{\text{stᵍ}}}}\, \end{pmatrix}$

  CERT-pool :
    ∙ pp ⊢ stᵖ ⇀⦇ dCert ,POOL⦈ stᵖ'
      ────────────────────────────────
      $\begin{pmatrix} \,\href{Ledger.Conway.Conformance.Certs.html#3339}{\htmlId{6931}{\htmlClass{Generalizable}{\text{e}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3491}{\htmlId{6935}{\htmlClass{Generalizable}{\text{pp}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3364}{\htmlId{6940}{\htmlClass{Generalizable}{\text{vs}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3041}{\htmlId{6945}{\htmlClass{Generalizable}{\text{wdrls}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3265}{\htmlId{6953}{\htmlClass{Generalizable}{\text{cc}}}}\, \end{pmatrix}$ ⊢ $\begin{pmatrix} \,\href{Ledger.Conway.Conformance.Certs.html#3551}{\htmlId{6962}{\htmlClass{Generalizable}{\text{stᵈ}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3591}{\htmlId{6968}{\htmlClass{Generalizable}{\text{stᵖ}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3571}{\htmlId{6974}{\htmlClass{Generalizable}{\text{stᵍ}}}}\, \end{pmatrix}$ ⇀⦇ dCert ,CERT⦈ $\begin{pmatrix} \,\href{Ledger.Conway.Conformance.Certs.html#3551}{\htmlId{6998}{\htmlClass{Generalizable}{\text{stᵈ}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3595}{\htmlId{7004}{\htmlClass{Generalizable}{\text{stᵖ'}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3571}{\htmlId{7011}{\htmlClass{Generalizable}{\text{stᵍ}}}}\, \end{pmatrix}$

  CERT-vdel :
    ∙ Γ ⊢ stᵍ ⇀⦇ dCert ,GOVCERT⦈ stᵍ'
      ────────────────────────────────
      Γ ⊢ $\begin{pmatrix} \,\href{Ledger.Conway.Conformance.Certs.html#3551}{\htmlId{7121}{\htmlClass{Generalizable}{\text{stᵈ}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3591}{\htmlId{7127}{\htmlClass{Generalizable}{\text{stᵖ}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3571}{\htmlId{7133}{\htmlClass{Generalizable}{\text{stᵍ}}}}\, \end{pmatrix}$ ⇀⦇ dCert ,CERT⦈ $\begin{pmatrix} \,\href{Ledger.Conway.Conformance.Certs.html#3551}{\htmlId{7157}{\htmlClass{Generalizable}{\text{stᵈ}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3591}{\htmlId{7163}{\htmlClass{Generalizable}{\text{stᵖ}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3575}{\htmlId{7169}{\htmlClass{Generalizable}{\text{stᵍ'}}}}\, \end{pmatrix}$

data _⊢_⇀⦇_,PRE-CERT⦈_ : CertEnv → CertState → ⊤ → CertState → Type where

  CERT-pre :
    let open PParams pp
        refresh         = mapPartial (isGovVoterDRep ∘ voter) (fromList vs)
        refreshedDReps  = mapValueRestricted (const (e + drepActivity)) dReps refresh
        wdrlCreds       = mapˢ stake (dom wdrls)
    in
    ∙ filterˢ isKeyHash wdrlCreds ⊆ dom voteDelegs
    ∙ mapˢ (map₁ stake) (wdrls ˢ) ⊆ rewards ˢ
      ────────────────────────────────
      $\begin{pmatrix} \,\href{Ledger.Conway.Conformance.Certs.html#3339}{\htmlId{7651}{\htmlClass{Generalizable}{\text{e}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3491}{\htmlId{7655}{\htmlClass{Generalizable}{\text{pp}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3364}{\htmlId{7660}{\htmlClass{Generalizable}{\text{vs}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3041}{\htmlId{7665}{\htmlClass{Generalizable}{\text{wdrls}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3265}{\htmlId{7673}{\htmlClass{Generalizable}{\text{cc}}}}\, \end{pmatrix}$ ⊢ $\begin{pmatrix} \begin{pmatrix} \,\href{Ledger.Conway.Conformance.Certs.html#2935}{\htmlId{7684}{\htmlClass{Generalizable}{\text{voteDelegs}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#2830}{\htmlId{7697}{\htmlClass{Generalizable}{\text{stakeDelegs}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#2746}{\htmlId{7711}{\htmlClass{Generalizable}{\text{rewards}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3315}{\htmlId{7721}{\htmlClass{Generalizable}{\text{ddep}}}}\, \end{pmatrix} \\ \,\href{Ledger.Conway.Conformance.Certs.html#3591}{\htmlId{7730}{\htmlClass{Generalizable}{\text{stᵖ}}}}\, \\ \begin{pmatrix} \,\href{Ledger.Conway.Conformance.Certs.html#2776}{\htmlId{7738}{\htmlClass{Generalizable}{\text{dReps}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#2877}{\htmlId{7746}{\htmlClass{Generalizable}{\text{ccHotKeys}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3320}{\htmlId{7758}{\htmlClass{Generalizable}{\text{gdep}}}}\, \end{pmatrix} \end{pmatrix}$
      ⇀⦇ _ ,PRE-CERT⦈
      $\begin{pmatrix} \begin{pmatrix} \,\href{Ledger.Conway.Conformance.Certs.html#2935}{\htmlId{7799}{\htmlClass{Generalizable}{\text{voteDelegs}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#2830}{\htmlId{7812}{\htmlClass{Generalizable}{\text{stakeDelegs}}}}\, \\ \,\href{Axiom.Set.Map.html#11222}{\htmlId{7826}{\htmlClass{Function}{\text{constMap}}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#7459}{\htmlId{7835}{\htmlClass{Bound}{\text{wdrlCreds}}}}\, \,\htmlId{7845}{\htmlClass{Number}{\text{0}}}\, \,\href{Axiom.Set.Map.html#7638}{\htmlId{7847}{\htmlClass{Function Operator}{\text{∪ˡ}}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#2746}{\htmlId{7850}{\htmlClass{Generalizable}{\text{rewards}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3315}{\htmlId{7860}{\htmlClass{Generalizable}{\text{ddep}}}}\, \end{pmatrix} \\ \,\href{Ledger.Conway.Conformance.Certs.html#3591}{\htmlId{7869}{\htmlClass{Generalizable}{\text{stᵖ}}}}\, \\ \begin{pmatrix} \,\href{Ledger.Conway.Conformance.Certs.html#7373}{\htmlId{7877}{\htmlClass{Bound}{\text{refreshedDReps}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#2877}{\htmlId{7894}{\htmlClass{Generalizable}{\text{ccHotKeys}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3320}{\htmlId{7906}{\htmlClass{Generalizable}{\text{gdep}}}}\, \end{pmatrix} \end{pmatrix}$

data _⊢_⇀⦇_,POST-CERT⦈_ : CertEnv → CertState → ⊤ → CertState → Type where

  CERT-post :
      $\begin{pmatrix} \,\href{Ledger.Conway.Conformance.Certs.html#3339}{\htmlId{8014}{\htmlClass{Generalizable}{\text{e}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3491}{\htmlId{8018}{\htmlClass{Generalizable}{\text{pp}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3364}{\htmlId{8023}{\htmlClass{Generalizable}{\text{vs}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3041}{\htmlId{8028}{\htmlClass{Generalizable}{\text{wdrls}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3265}{\htmlId{8036}{\htmlClass{Generalizable}{\text{cc}}}}\, \end{pmatrix}$
      ⊢ $\begin{pmatrix} \begin{pmatrix} \,\href{Ledger.Conway.Conformance.Certs.html#2935}{\htmlId{8053}{\htmlClass{Generalizable}{\text{voteDelegs}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#2830}{\htmlId{8066}{\htmlClass{Generalizable}{\text{stakeDelegs}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#2746}{\htmlId{8080}{\htmlClass{Generalizable}{\text{rewards}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3315}{\htmlId{8090}{\htmlClass{Generalizable}{\text{ddep}}}}\, \end{pmatrix} \\ \,\href{Ledger.Conway.Conformance.Certs.html#3591}{\htmlId{8099}{\htmlClass{Generalizable}{\text{stᵖ}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3571}{\htmlId{8105}{\htmlClass{Generalizable}{\text{stᵍ}}}}\, \end{pmatrix}$
        ⇀⦇ _ ,POST-CERT⦈
        $\begin{pmatrix} \begin{pmatrix} \,\href{Ledger.Conway.Conformance.Certs.html#2935}{\htmlId{8148}{\htmlClass{Generalizable}{\text{voteDelegs}}}}\, \,\href{Axiom.Set.Map.html#17009}{\htmlId{8159}{\htmlClass{Function Operator}{\text{∣\^{}}}}}\, \,\htmlId{8162}{\htmlClass{Symbol}{\text{(}}}\,\,\href{abstract-set-theory.FiniteSetTheory.html#519}{\htmlId{8163}{\htmlClass{Function}{\text{mapˢ}}}}\, \,\href{Ledger.Conway.Specification.Gov.Actions.html#696}{\htmlId{8168}{\htmlClass{InductiveConstructor}{\text{vDelegCredential}}}}\, \,\htmlId{8185}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Class.IsSet.html#916}{\htmlId{8186}{\htmlClass{Function}{\text{dom}}}}\, \,\htmlId{8190}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Conway.Conformance.Certs.html#858}{\htmlId{8191}{\htmlClass{Field}{\text{GState.dreps}}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#3571}{\htmlId{8204}{\htmlClass{Generalizable}{\text{stᵍ}}}}\,\,\htmlId{8207}{\htmlClass{Symbol}{\text{))}}}\, \,\href{Axiom.Set.html#8952}{\htmlId{8210}{\htmlClass{Function Operator}{\text{∪}}}}\, \,\href{Axiom.Set.html#5718}{\htmlId{8212}{\htmlClass{Function}{\text{fromList}}}}\, \,\htmlId{8221}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Conway.Specification.Gov.Actions.html#769}{\htmlId{8222}{\htmlClass{InductiveConstructor}{\text{vDelegNoConfidence}}}}\, \,\href{Agda.Builtin.List.html#199}{\htmlId{8241}{\htmlClass{InductiveConstructor Operator}{\text{∷}}}}\, \,\href{Ledger.Conway.Specification.Gov.Actions.html#739}{\htmlId{8243}{\htmlClass{InductiveConstructor}{\text{vDelegAbstain}}}}\, \,\href{Agda.Builtin.List.html#199}{\htmlId{8257}{\htmlClass{InductiveConstructor Operator}{\text{∷}}}}\, \,\href{Agda.Builtin.List.html#184}{\htmlId{8259}{\htmlClass{InductiveConstructor}{\text{[]}}}}\,\,\htmlId{8261}{\htmlClass{Symbol}{\text{))}}}\,
          , \,\href{Ledger.Conway.Conformance.Certs.html#2830}{\htmlId{8276}{\htmlClass{Generalizable}{\text{stakeDelegs}}}}\, , \,\href{Ledger.Conway.Conformance.Certs.html#2746}{\htmlId{8290}{\htmlClass{Generalizable}{\text{rewards}}}}\, , \,\href{Ledger.Conway.Conformance.Certs.html#3315}{\htmlId{8300}{\htmlClass{Generalizable}{\text{ddep}}}}\, \end{pmatrix} , \,\href{Ledger.Conway.Conformance.Certs.html#3591}{\htmlId{8309}{\htmlClass{Generalizable}{\text{stᵖ}}}}\, , \,\href{Ledger.Conway.Conformance.Certs.html#3571}{\htmlId{8315}{\htmlClass{Generalizable}{\text{stᵍ}}}}\, \end{pmatrix}$

_⊢_⇀⦇_,CERTS⦈_  : CertEnv → CertState  → List DCert  → CertState  → Type
_⊢_⇀⦇_,CERTS⦈_ = RunTraceAfterAndThen _⊢_⇀⦇_,PRE-CERT⦈_ _⊢_⇀⦇_,CERT⦈_ _⊢_⇀⦇_,POST-CERT⦈_