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⦈_; _⊢_⇀⦇_,CERTBASE⦈_; _⊢_⇀⦇_,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                  : 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

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#2953}{\htmlId{3842}{\htmlClass{Generalizable}{\text{pools}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#2986}{\htmlId{3850}{\htmlClass{Generalizable}{\text{retiring}}}}\, \end{pmatrix}$ ⇀⦇ regpool kh poolParams ,POOL⦈
            $\begin{pmatrix} \,\href{Class.HasSingleton.html#288}{\htmlId{3907}{\htmlClass{Field Operator}{\text{❴}}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#3384}{\htmlId{3909}{\htmlClass{Generalizable}{\text{kh}}}}\, , \,\href{Ledger.Conway.Conformance.Certs.html#3444}{\htmlId{3914}{\htmlClass{Generalizable}{\text{poolParams}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{3925}{\htmlClass{Field Operator}{\text{❵}}}}\, \,\href{Axiom.Set.Map.html#6320}{\htmlId{3927}{\htmlClass{Function Operator}{\text{∪ˡ}}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#2953}{\htmlId{3930}{\htmlClass{Generalizable}{\text{pools}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#2986}{\htmlId{3938}{\htmlClass{Generalizable}{\text{retiring}}}}\, \end{pmatrix}$

  POOL-retirepool :
    ────────────────────────────────
    pp  $\begin{pmatrix} \,\href{Ledger.Conway.Conformance.Certs.html#2953}{\htmlId{4018}{\htmlClass{Generalizable}{\text{pools}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#2986}{\htmlId{4026}{\htmlClass{Generalizable}{\text{retiring}}}}\, \end{pmatrix}$ ⇀⦇ retirepool kh e ,POOL⦈ $\begin{pmatrix} \,\href{Ledger.Conway.Conformance.Certs.html#2953}{\htmlId{4065}{\htmlClass{Generalizable}{\text{pools}}}}\, \\ \,\href{Class.HasSingleton.html#288}{\htmlId{4073}{\htmlClass{Field Operator}{\text{❴}}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#3384}{\htmlId{4075}{\htmlClass{Generalizable}{\text{kh}}}}\, , \,\href{Ledger.Conway.Conformance.Certs.html#3327}{\htmlId{4080}{\htmlClass{Generalizable}{\text{e}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{4082}{\htmlClass{Field Operator}{\text{❵}}}}\, \,\href{Axiom.Set.Map.html#6320}{\htmlId{4084}{\htmlClass{Function Operator}{\text{∪ˡ}}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#2986}{\htmlId{4087}{\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  credVoter DRep) delegatees 
        fromList
          ( nothing
           just abstainRep
           just noConfidenceRep
           []
          )
     mkh  mapˢ just (dom pools)   nothing 
      ────────────────────────────────
      $\begin{pmatrix} \,\href{Ledger.Conway.Conformance.Certs.html#3479}{\htmlId{4507}{\htmlClass{Generalizable}{\text{pp}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#2953}{\htmlId{4512}{\htmlClass{Generalizable}{\text{pools}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3242}{\htmlId{4520}{\htmlClass{Generalizable}{\text{delegatees}}}}\, \end{pmatrix}$ 
      $\begin{pmatrix} \,\href{Ledger.Conway.Conformance.Certs.html#2915}{\htmlId{4543}{\htmlClass{Generalizable}{\text{vDelegs}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#2810}{\htmlId{4553}{\htmlClass{Generalizable}{\text{sDelegs}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#2729}{\htmlId{4563}{\htmlClass{Generalizable}{\text{rwds}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3299}{\htmlId{4570}{\htmlClass{Generalizable}{\text{dep}}}}\, \end{pmatrix}$
      ⇀⦇ delegate c mv mkh d ,DELEG⦈
      $\begin{pmatrix} \,\href{Axiom.Set.Map.html#7168}{\htmlId{4621}{\htmlClass{Function}{\text{insertIfJust}}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#3176}{\htmlId{4634}{\htmlClass{Generalizable}{\text{c}}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#3506}{\htmlId{4636}{\htmlClass{Generalizable}{\text{mv}}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#2915}{\htmlId{4639}{\htmlClass{Generalizable}{\text{vDelegs}}}}\, \\ \,\href{Axiom.Set.Map.html#7168}{\htmlId{4649}{\htmlClass{Function}{\text{insertIfJust}}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#3176}{\htmlId{4662}{\htmlClass{Generalizable}{\text{c}}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#3411}{\htmlId{4664}{\htmlClass{Generalizable}{\text{mkh}}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#2810}{\htmlId{4668}{\htmlClass{Generalizable}{\text{sDelegs}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#2729}{\htmlId{4678}{\htmlClass{Generalizable}{\text{rwds}}}}\, \,\href{Axiom.Set.Map.html#6320}{\htmlId{4683}{\htmlClass{Function Operator}{\text{∪ˡ}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{4686}{\htmlClass{Field Operator}{\text{❴}}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#3176}{\htmlId{4688}{\htmlClass{Generalizable}{\text{c}}}}\, , \,\htmlId{4692}{\htmlClass{Number}{\text{0}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{4694}{\htmlClass{Field Operator}{\text{❵}}}}\,
      \\ \,\href{Ledger.Conway.Conformance.Certs.html#1865}{\htmlId{4704}{\htmlClass{Function}{\text{updateCertDeposit}}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#3479}{\htmlId{4722}{\htmlClass{Generalizable}{\text{pp}}}}\, \,\htmlId{4725}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Conway.Specification.Certs.html#2667}{\htmlId{4726}{\htmlClass{InductiveConstructor}{\text{delegate}}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#3176}{\htmlId{4735}{\htmlClass{Generalizable}{\text{c}}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#3506}{\htmlId{4737}{\htmlClass{Generalizable}{\text{mv}}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#3411}{\htmlId{4740}{\htmlClass{Generalizable}{\text{mkh}}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#3122}{\htmlId{4744}{\htmlClass{Generalizable}{\text{d}}}}\,\,\htmlId{4745}{\htmlClass{Symbol}{\text{)}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#3299}{\htmlId{4747}{\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#3479}{\htmlId{4909}{\htmlClass{Generalizable}{\text{pp}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#2953}{\htmlId{4914}{\htmlClass{Generalizable}{\text{pools}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3242}{\htmlId{4922}{\htmlClass{Generalizable}{\text{delegatees}}}}\, \end{pmatrix}$ 
      $\begin{pmatrix} \,\href{Ledger.Conway.Conformance.Certs.html#2915}{\htmlId{4945}{\htmlClass{Generalizable}{\text{vDelegs}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#2810}{\htmlId{4955}{\htmlClass{Generalizable}{\text{sDelegs}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#2729}{\htmlId{4965}{\htmlClass{Generalizable}{\text{rwds}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3299}{\htmlId{4972}{\htmlClass{Generalizable}{\text{dep}}}}\, \end{pmatrix}$
      ⇀⦇ dereg c md ,DELEG⦈
      $\begin{pmatrix} \,\href{Ledger.Conway.Conformance.Certs.html#2915}{\htmlId{5014}{\htmlClass{Generalizable}{\text{vDelegs}}}}\, \,\href{Axiom.Set.Map.html#10748}{\htmlId{5022}{\htmlClass{Function Operator}{\text{∣}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{5024}{\htmlClass{Field Operator}{\text{❴}}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#3176}{\htmlId{5026}{\htmlClass{Generalizable}{\text{c}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{5028}{\htmlClass{Field Operator}{\text{❵}}}}\, \,\href{Axiom.Set.Map.html#10748}{\htmlId{5030}{\htmlClass{Function Operator}{\text{ᶜ}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#2810}{\htmlId{5034}{\htmlClass{Generalizable}{\text{sDelegs}}}}\, \,\href{Axiom.Set.Map.html#10748}{\htmlId{5042}{\htmlClass{Function Operator}{\text{∣}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{5044}{\htmlClass{Field Operator}{\text{❴}}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#3176}{\htmlId{5046}{\htmlClass{Generalizable}{\text{c}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{5048}{\htmlClass{Field Operator}{\text{❵}}}}\, \,\href{Axiom.Set.Map.html#10748}{\htmlId{5050}{\htmlClass{Function Operator}{\text{ᶜ}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#2729}{\htmlId{5054}{\htmlClass{Generalizable}{\text{rwds}}}}\, \,\href{Axiom.Set.Map.html#10748}{\htmlId{5059}{\htmlClass{Function Operator}{\text{∣}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{5061}{\htmlClass{Field Operator}{\text{❴}}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#3176}{\htmlId{5063}{\htmlClass{Generalizable}{\text{c}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{5065}{\htmlClass{Field Operator}{\text{❵}}}}\, \,\href{Axiom.Set.Map.html#10748}{\htmlId{5067}{\htmlClass{Function Operator}{\text{ᶜ}}}}\,
      \\ \,\href{Ledger.Conway.Conformance.Certs.html#1865}{\htmlId{5077}{\htmlClass{Function}{\text{updateCertDeposit}}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#3479}{\htmlId{5095}{\htmlClass{Generalizable}{\text{pp}}}}\, \,\htmlId{5098}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Conway.Specification.Certs.html#2740}{\htmlId{5099}{\htmlClass{InductiveConstructor}{\text{dereg}}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#3176}{\htmlId{5105}{\htmlClass{Generalizable}{\text{c}}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#3146}{\htmlId{5107}{\htmlClass{Generalizable}{\text{md}}}}\,\,\htmlId{5109}{\htmlClass{Symbol}{\text{)}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#3299}{\htmlId{5111}{\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#3479}{\htmlId{5250}{\htmlClass{Generalizable}{\text{pp}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#2953}{\htmlId{5255}{\htmlClass{Generalizable}{\text{pools}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3242}{\htmlId{5263}{\htmlClass{Generalizable}{\text{delegatees}}}}\, \end{pmatrix}$ 
        $\begin{pmatrix} \,\href{Ledger.Conway.Conformance.Certs.html#2915}{\htmlId{5288}{\htmlClass{Generalizable}{\text{vDelegs}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#2810}{\htmlId{5298}{\htmlClass{Generalizable}{\text{sDelegs}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#2729}{\htmlId{5308}{\htmlClass{Generalizable}{\text{rwds}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3299}{\htmlId{5315}{\htmlClass{Generalizable}{\text{dep}}}}\, \end{pmatrix}$ ⇀⦇ reg c d ,DELEG⦈
        $\begin{pmatrix} \,\href{Ledger.Conway.Conformance.Certs.html#2915}{\htmlId{5350}{\htmlClass{Generalizable}{\text{vDelegs}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#2810}{\htmlId{5360}{\htmlClass{Generalizable}{\text{sDelegs}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#2729}{\htmlId{5370}{\htmlClass{Generalizable}{\text{rwds}}}}\, \,\href{Axiom.Set.Map.html#6320}{\htmlId{5375}{\htmlClass{Function Operator}{\text{∪ˡ}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{5378}{\htmlClass{Field Operator}{\text{❴}}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#3176}{\htmlId{5380}{\htmlClass{Generalizable}{\text{c}}}}\, , \,\htmlId{5384}{\htmlClass{Number}{\text{0}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{5386}{\htmlClass{Field Operator}{\text{❵}}}}\,
        \\ \,\href{Ledger.Conway.Conformance.Certs.html#1865}{\htmlId{5398}{\htmlClass{Function}{\text{updateCertDeposit}}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#3479}{\htmlId{5416}{\htmlClass{Generalizable}{\text{pp}}}}\, \,\htmlId{5419}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Conway.Specification.Certs.html#3376}{\htmlId{5420}{\htmlClass{InductiveConstructor}{\text{reg}}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#3176}{\htmlId{5424}{\htmlClass{Generalizable}{\text{c}}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#3122}{\htmlId{5426}{\htmlClass{Generalizable}{\text{d}}}}\,\,\htmlId{5427}{\htmlClass{Symbol}{\text{)}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#3299}{\htmlId{5429}{\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#3327}{\htmlId{5672}{\htmlClass{Generalizable}{\text{e}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#5530}{\htmlId{5676}{\htmlClass{Bound}{\text{pp}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3352}{\htmlId{5681}{\htmlClass{Generalizable}{\text{vs}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3029}{\htmlId{5686}{\htmlClass{Generalizable}{\text{wdrls}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3253}{\htmlId{5694}{\htmlClass{Generalizable}{\text{cc}}}}\, \end{pmatrix}$ 
      $\begin{pmatrix} \,\href{Ledger.Conway.Conformance.Certs.html#2764}{\htmlId{5709}{\htmlClass{Generalizable}{\text{dReps}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#2858}{\htmlId{5717}{\htmlClass{Generalizable}{\text{ccKeys}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3299}{\htmlId{5726}{\htmlClass{Generalizable}{\text{dep}}}}\, \end{pmatrix}$
        ⇀⦇ regdrep c d an ,GOVCERT⦈
      $\begin{pmatrix} \,\href{Class.HasSingleton.html#288}{\htmlId{5776}{\htmlClass{Field Operator}{\text{❴}}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#3176}{\htmlId{5778}{\htmlClass{Generalizable}{\text{c}}}}\, , \,\href{Ledger.Conway.Conformance.Certs.html#3327}{\htmlId{5782}{\htmlClass{Generalizable}{\text{e}}}}\, \,\href{Class.HasAdd.Core.html#162}{\htmlId{5784}{\htmlClass{Field Operator}{\text{+}}}}\, \,\href{Ledger.Conway.Specification.PParams.html#4784}{\htmlId{5786}{\htmlClass{Field}{\text{drepActivity}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{5799}{\htmlClass{Field Operator}{\text{❵}}}}\, \,\href{Axiom.Set.Map.html#6320}{\htmlId{5801}{\htmlClass{Function Operator}{\text{∪ˡ}}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#2764}{\htmlId{5804}{\htmlClass{Generalizable}{\text{dReps}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#2858}{\htmlId{5812}{\htmlClass{Generalizable}{\text{ccKeys}}}}\,
      \\ \,\href{Ledger.Conway.Conformance.Certs.html#1865}{\htmlId{5827}{\htmlClass{Function}{\text{updateCertDeposit}}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#5530}{\htmlId{5845}{\htmlClass{Bound}{\text{pp}}}}\, \,\htmlId{5848}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Conway.Specification.Certs.html#2878}{\htmlId{5849}{\htmlClass{InductiveConstructor}{\text{regdrep}}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#3176}{\htmlId{5857}{\htmlClass{Generalizable}{\text{c}}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#3122}{\htmlId{5859}{\htmlClass{Generalizable}{\text{d}}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#3069}{\htmlId{5861}{\htmlClass{Generalizable}{\text{an}}}}\, \,\htmlId{5864}{\htmlClass{Symbol}{\text{)}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#3299}{\htmlId{5866}{\htmlClass{Generalizable}{\text{dep}}}}\, \end{pmatrix}$

  GOVCERT-deregdrep :
     c  dom dReps
     (DRepDeposit c , d)  dep
      ────────────────────────────────
      $\begin{pmatrix} \,\href{Ledger.Conway.Conformance.Certs.html#3327}{\htmlId{5994}{\htmlClass{Generalizable}{\text{e}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3479}{\htmlId{5998}{\htmlClass{Generalizable}{\text{pp}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3352}{\htmlId{6003}{\htmlClass{Generalizable}{\text{vs}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3029}{\htmlId{6008}{\htmlClass{Generalizable}{\text{wdrls}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3253}{\htmlId{6016}{\htmlClass{Generalizable}{\text{cc}}}}\, \end{pmatrix}$  $\begin{pmatrix} \,\href{Ledger.Conway.Conformance.Certs.html#2764}{\htmlId{6025}{\htmlClass{Generalizable}{\text{dReps}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#2858}{\htmlId{6033}{\htmlClass{Generalizable}{\text{ccKeys}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3299}{\htmlId{6042}{\htmlClass{Generalizable}{\text{dep}}}}\, \end{pmatrix}$
          ⇀⦇ deregdrep c d ,GOVCERT⦈
          $\begin{pmatrix} \,\href{Ledger.Conway.Conformance.Certs.html#2764}{\htmlId{6097}{\htmlClass{Generalizable}{\text{dReps}}}}\, \,\href{Axiom.Set.Map.html#10748}{\htmlId{6103}{\htmlClass{Function Operator}{\text{∣}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{6105}{\htmlClass{Field Operator}{\text{❴}}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#3176}{\htmlId{6107}{\htmlClass{Generalizable}{\text{c}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{6109}{\htmlClass{Field Operator}{\text{❵}}}}\, \,\href{Axiom.Set.Map.html#10748}{\htmlId{6111}{\htmlClass{Function Operator}{\text{ᶜ}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#2858}{\htmlId{6115}{\htmlClass{Generalizable}{\text{ccKeys}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#1865}{\htmlId{6124}{\htmlClass{Function}{\text{updateCertDeposit}}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#3479}{\htmlId{6142}{\htmlClass{Generalizable}{\text{pp}}}}\, \,\htmlId{6145}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Conway.Specification.Certs.html#2929}{\htmlId{6146}{\htmlClass{InductiveConstructor}{\text{deregdrep}}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#3176}{\htmlId{6156}{\htmlClass{Generalizable}{\text{c}}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#3122}{\htmlId{6158}{\htmlClass{Generalizable}{\text{d}}}}\,\,\htmlId{6159}{\htmlClass{Symbol}{\text{)}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#3299}{\htmlId{6161}{\htmlClass{Generalizable}{\text{dep}}}}\, \end{pmatrix}$

  GOVCERT-ccreghot :
     (c , nothing)  ccKeys
     c  cc
      ────────────────────────────────
      $\begin{pmatrix} \,\href{Ledger.Conway.Conformance.Certs.html#3327}{\htmlId{6278}{\htmlClass{Generalizable}{\text{e}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3479}{\htmlId{6282}{\htmlClass{Generalizable}{\text{pp}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3352}{\htmlId{6287}{\htmlClass{Generalizable}{\text{vs}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3029}{\htmlId{6292}{\htmlClass{Generalizable}{\text{wdrls}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3253}{\htmlId{6300}{\htmlClass{Generalizable}{\text{cc}}}}\, \end{pmatrix}$  $\begin{pmatrix} \,\href{Ledger.Conway.Conformance.Certs.html#2764}{\htmlId{6309}{\htmlClass{Generalizable}{\text{dReps}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#2858}{\htmlId{6317}{\htmlClass{Generalizable}{\text{ccKeys}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3299}{\htmlId{6326}{\htmlClass{Generalizable}{\text{dep}}}}\, \end{pmatrix}$
          ⇀⦇ ccreghot c mc ,GOVCERT⦈
          $\begin{pmatrix} \,\href{Ledger.Conway.Conformance.Certs.html#2764}{\htmlId{6381}{\htmlClass{Generalizable}{\text{dReps}}}}\, \\ \,\href{Class.HasSingleton.html#288}{\htmlId{6389}{\htmlClass{Field Operator}{\text{❴}}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#3176}{\htmlId{6391}{\htmlClass{Generalizable}{\text{c}}}}\, , \,\href{Ledger.Conway.Conformance.Certs.html#3206}{\htmlId{6395}{\htmlClass{Generalizable}{\text{mc}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{6398}{\htmlClass{Field Operator}{\text{❵}}}}\, \,\href{Axiom.Set.Map.html#6320}{\htmlId{6400}{\htmlClass{Function Operator}{\text{∪ˡ}}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#2858}{\htmlId{6403}{\htmlClass{Generalizable}{\text{ccKeys}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#1865}{\htmlId{6412}{\htmlClass{Function}{\text{updateCertDeposit}}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#3479}{\htmlId{6430}{\htmlClass{Generalizable}{\text{pp}}}}\, \,\htmlId{6433}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Conway.Specification.Certs.html#2971}{\htmlId{6434}{\htmlClass{InductiveConstructor}{\text{ccreghot}}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#3176}{\htmlId{6443}{\htmlClass{Generalizable}{\text{c}}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#3206}{\htmlId{6445}{\htmlClass{Generalizable}{\text{mc}}}}\,\,\htmlId{6447}{\htmlClass{Symbol}{\text{)}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#3299}{\htmlId{6449}{\htmlClass{Generalizable}{\text{dep}}}}\, \end{pmatrix}$

data _⊢_⇀⦇_,CERT⦈_ : CertEnv  CertState  DCert  CertState  Type where
  CERT-deleg :
     $\begin{pmatrix} \,\href{Ledger.Conway.Conformance.Certs.html#3479}{\htmlId{6553}{\htmlClass{Generalizable}{\text{pp}}}}\, \\ \,\href{Ledger.Conway.Specification.Certs.html#4621}{\htmlId{6558}{\htmlClass{Field}{\text{PState.pools}}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#3579}{\htmlId{6571}{\htmlClass{Generalizable}{\text{stᵖ}}}}\, \\ \,\href{Class.IsSet.html#916}{\htmlId{6577}{\htmlClass{Function}{\text{dom}}}}\, \,\htmlId{6581}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Conway.Conformance.Certs.html#846}{\htmlId{6582}{\htmlClass{Field}{\text{GState.dreps}}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#3559}{\htmlId{6595}{\htmlClass{Generalizable}{\text{stᵍ}}}}\,\,\htmlId{6598}{\htmlClass{Symbol}{\text{)}}}\, \end{pmatrix}$  stᵈ ⇀⦇ dCert ,DELEG⦈ stᵈ'
      ────────────────────────────────
      $\begin{pmatrix} \,\href{Ledger.Conway.Conformance.Certs.html#3327}{\htmlId{6677}{\htmlClass{Generalizable}{\text{e}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3479}{\htmlId{6681}{\htmlClass{Generalizable}{\text{pp}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3352}{\htmlId{6686}{\htmlClass{Generalizable}{\text{vs}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3029}{\htmlId{6691}{\htmlClass{Generalizable}{\text{wdrls}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3253}{\htmlId{6699}{\htmlClass{Generalizable}{\text{cc}}}}\, \end{pmatrix}$  $\begin{pmatrix} \,\href{Ledger.Conway.Conformance.Certs.html#3539}{\htmlId{6708}{\htmlClass{Generalizable}{\text{stᵈ}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3579}{\htmlId{6714}{\htmlClass{Generalizable}{\text{stᵖ}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3559}{\htmlId{6720}{\htmlClass{Generalizable}{\text{stᵍ}}}}\, \end{pmatrix}$ ⇀⦇ dCert ,CERT⦈ $\begin{pmatrix} \,\href{Ledger.Conway.Conformance.Certs.html#3543}{\htmlId{6744}{\htmlClass{Generalizable}{\text{stᵈ'}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3579}{\htmlId{6751}{\htmlClass{Generalizable}{\text{stᵖ}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3559}{\htmlId{6757}{\htmlClass{Generalizable}{\text{stᵍ}}}}\, \end{pmatrix}$

  CERT-pool :
     pp  stᵖ ⇀⦇ dCert ,POOL⦈ stᵖ'
      ────────────────────────────────
      $\begin{pmatrix} \,\href{Ledger.Conway.Conformance.Certs.html#3327}{\htmlId{6861}{\htmlClass{Generalizable}{\text{e}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3479}{\htmlId{6865}{\htmlClass{Generalizable}{\text{pp}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3352}{\htmlId{6870}{\htmlClass{Generalizable}{\text{vs}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3029}{\htmlId{6875}{\htmlClass{Generalizable}{\text{wdrls}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3253}{\htmlId{6883}{\htmlClass{Generalizable}{\text{cc}}}}\, \end{pmatrix}$  $\begin{pmatrix} \,\href{Ledger.Conway.Conformance.Certs.html#3539}{\htmlId{6892}{\htmlClass{Generalizable}{\text{stᵈ}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3579}{\htmlId{6898}{\htmlClass{Generalizable}{\text{stᵖ}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3559}{\htmlId{6904}{\htmlClass{Generalizable}{\text{stᵍ}}}}\, \end{pmatrix}$ ⇀⦇ dCert ,CERT⦈ $\begin{pmatrix} \,\href{Ledger.Conway.Conformance.Certs.html#3539}{\htmlId{6928}{\htmlClass{Generalizable}{\text{stᵈ}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3583}{\htmlId{6934}{\htmlClass{Generalizable}{\text{stᵖ'}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3559}{\htmlId{6941}{\htmlClass{Generalizable}{\text{stᵍ}}}}\, \end{pmatrix}$

  CERT-vdel :
     Γ  stᵍ ⇀⦇ dCert ,GOVCERT⦈ stᵍ'
      ────────────────────────────────
      Γ  $\begin{pmatrix} \,\href{Ledger.Conway.Conformance.Certs.html#3539}{\htmlId{7051}{\htmlClass{Generalizable}{\text{stᵈ}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3579}{\htmlId{7057}{\htmlClass{Generalizable}{\text{stᵖ}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3559}{\htmlId{7063}{\htmlClass{Generalizable}{\text{stᵍ}}}}\, \end{pmatrix}$ ⇀⦇ dCert ,CERT⦈ $\begin{pmatrix} \,\href{Ledger.Conway.Conformance.Certs.html#3539}{\htmlId{7087}{\htmlClass{Generalizable}{\text{stᵈ}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3579}{\htmlId{7093}{\htmlClass{Generalizable}{\text{stᵖ}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3563}{\htmlId{7099}{\htmlClass{Generalizable}{\text{stᵍ'}}}}\, \end{pmatrix}$

data _⊢_⇀⦇_,CERTBASE⦈_ : CertEnv  CertState    CertState  Type where
  CERT-base :
    let open PParams pp
        refresh         = mapPartial getDRepVote (fromList vs)
        refreshedDReps  = mapValueRestricted (const (e + 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.Conformance.Certs.html#3327}{\htmlId{7692}{\htmlClass{Generalizable}{\text{e}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3479}{\htmlId{7696}{\htmlClass{Generalizable}{\text{pp}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3352}{\htmlId{7701}{\htmlClass{Generalizable}{\text{vs}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3029}{\htmlId{7706}{\htmlClass{Generalizable}{\text{wdrls}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3253}{\htmlId{7714}{\htmlClass{Generalizable}{\text{cc}}}}\, \end{pmatrix}$ 
      $\begin{pmatrix} \begin{pmatrix} \,\href{Ledger.Conway.Conformance.Certs.html#2923}{\htmlId{7731}{\htmlClass{Generalizable}{\text{voteDelegs}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#2818}{\htmlId{7744}{\htmlClass{Generalizable}{\text{stakeDelegs}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#2734}{\htmlId{7758}{\htmlClass{Generalizable}{\text{rewards}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3303}{\htmlId{7768}{\htmlClass{Generalizable}{\text{ddep}}}}\, \end{pmatrix}
      \\ \,\href{Ledger.Conway.Conformance.Certs.html#3579}{\htmlId{7783}{\htmlClass{Generalizable}{\text{stᵖ}}}}\,
      \\ \begin{pmatrix} \,\href{Ledger.Conway.Conformance.Certs.html#2764}{\htmlId{7797}{\htmlClass{Generalizable}{\text{dReps}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#2865}{\htmlId{7805}{\htmlClass{Generalizable}{\text{ccHotKeys}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3308}{\htmlId{7817}{\htmlClass{Generalizable}{\text{gdep}}}}\, \end{pmatrix}
      \end{pmatrix}$
      ⇀⦇ _ ,CERTBASE⦈
      $\begin{pmatrix} \begin{pmatrix} \,\href{Ledger.Conway.Conformance.Certs.html#7425}{\htmlId{7864}{\htmlClass{Bound}{\text{validVoteDelegs}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#2818}{\htmlId{7882}{\htmlClass{Generalizable}{\text{stakeDelegs}}}}\, \\ \,\href{Axiom.Set.Map.html#9130}{\htmlId{7896}{\htmlClass{Function}{\text{constMap}}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#7376}{\htmlId{7905}{\htmlClass{Bound}{\text{wdrlCreds}}}}\, \,\htmlId{7915}{\htmlClass{Number}{\text{0}}}\, \,\href{Axiom.Set.Map.html#6320}{\htmlId{7917}{\htmlClass{Function Operator}{\text{∪ˡ}}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#2734}{\htmlId{7920}{\htmlClass{Generalizable}{\text{rewards}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3303}{\htmlId{7930}{\htmlClass{Generalizable}{\text{ddep}}}}\, \end{pmatrix}
      \\ \,\href{Ledger.Conway.Conformance.Certs.html#3579}{\htmlId{7945}{\htmlClass{Generalizable}{\text{stᵖ}}}}\,
      \\ \begin{pmatrix} \,\href{Ledger.Conway.Conformance.Certs.html#7290}{\htmlId{7959}{\htmlClass{Bound}{\text{refreshedDReps}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#2865}{\htmlId{7976}{\htmlClass{Generalizable}{\text{ccHotKeys}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3308}{\htmlId{7988}{\htmlClass{Generalizable}{\text{gdep}}}}\, \end{pmatrix}
      \end{pmatrix}$

_⊢_⇀⦇_,CERTS⦈_     : CertEnv  CertState  List DCert  CertState  Type
_⊢_⇀⦇_,CERTS⦈_ = ReflexiveTransitiveClosureᵇ' {_⊢_⇀⟦_⟧ᵇ_ = _⊢_⇀⦇_,CERTBASE⦈_}{_⊢_⇀⦇_,CERT⦈_}