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⦈_; _⊢_⇀⦇_,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#2945}{\htmlId{3834}{\htmlClass{Generalizable}{\text{pools}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#2978}{\htmlId{3842}{\htmlClass{Generalizable}{\text{retiring}}}}\, \end{pmatrix}$ ⇀⦇ regpool kh poolParams ,POOL⦈
            $\begin{pmatrix} \,\href{Class.HasSingleton.html#288}{\htmlId{3899}{\htmlClass{Field Operator}{\text{❴}}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#3376}{\htmlId{3901}{\htmlClass{Generalizable}{\text{kh}}}}\, , \,\href{Ledger.Conway.Conformance.Certs.html#3436}{\htmlId{3906}{\htmlClass{Generalizable}{\text{poolParams}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{3917}{\htmlClass{Field Operator}{\text{❵}}}}\, \,\href{Axiom.Set.Map.html#6320}{\htmlId{3919}{\htmlClass{Function Operator}{\text{∪ˡ}}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#2945}{\htmlId{3922}{\htmlClass{Generalizable}{\text{pools}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#2978}{\htmlId{3930}{\htmlClass{Generalizable}{\text{retiring}}}}\, \end{pmatrix}$

  POOL-retirepool :
    ────────────────────────────────
    pp ⊢ $\begin{pmatrix} \,\href{Ledger.Conway.Conformance.Certs.html#2945}{\htmlId{4010}{\htmlClass{Generalizable}{\text{pools}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#2978}{\htmlId{4018}{\htmlClass{Generalizable}{\text{retiring}}}}\, \end{pmatrix}$ ⇀⦇ retirepool kh e ,POOL⦈ $\begin{pmatrix} \,\href{Ledger.Conway.Conformance.Certs.html#2945}{\htmlId{4057}{\htmlClass{Generalizable}{\text{pools}}}}\, \\ \,\href{Class.HasSingleton.html#288}{\htmlId{4065}{\htmlClass{Field Operator}{\text{❴}}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#3376}{\htmlId{4067}{\htmlClass{Generalizable}{\text{kh}}}}\, , \,\href{Ledger.Conway.Conformance.Certs.html#3319}{\htmlId{4072}{\htmlClass{Generalizable}{\text{e}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{4074}{\htmlClass{Field Operator}{\text{❵}}}}\, \,\href{Axiom.Set.Map.html#6320}{\htmlId{4076}{\htmlClass{Function Operator}{\text{∪ˡ}}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#2978}{\htmlId{4079}{\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#3471}{\htmlId{4499}{\htmlClass{Generalizable}{\text{pp}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#2945}{\htmlId{4504}{\htmlClass{Generalizable}{\text{pools}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3234}{\htmlId{4512}{\htmlClass{Generalizable}{\text{delegatees}}}}\, \end{pmatrix}$ ⊢
      $\begin{pmatrix} \,\href{Ledger.Conway.Conformance.Certs.html#2907}{\htmlId{4535}{\htmlClass{Generalizable}{\text{vDelegs}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#2802}{\htmlId{4545}{\htmlClass{Generalizable}{\text{sDelegs}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#2721}{\htmlId{4555}{\htmlClass{Generalizable}{\text{rwds}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3291}{\htmlId{4562}{\htmlClass{Generalizable}{\text{dep}}}}\, \end{pmatrix}$
      ⇀⦇ delegate c mv mkh d ,DELEG⦈
      $\begin{pmatrix} \,\href{Axiom.Set.Map.html#7168}{\htmlId{4613}{\htmlClass{Function}{\text{insertIfJust}}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#3168}{\htmlId{4626}{\htmlClass{Generalizable}{\text{c}}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#3498}{\htmlId{4628}{\htmlClass{Generalizable}{\text{mv}}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#2907}{\htmlId{4631}{\htmlClass{Generalizable}{\text{vDelegs}}}}\, \\ \,\href{Axiom.Set.Map.html#7168}{\htmlId{4641}{\htmlClass{Function}{\text{insertIfJust}}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#3168}{\htmlId{4654}{\htmlClass{Generalizable}{\text{c}}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#3403}{\htmlId{4656}{\htmlClass{Generalizable}{\text{mkh}}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#2802}{\htmlId{4660}{\htmlClass{Generalizable}{\text{sDelegs}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#2721}{\htmlId{4670}{\htmlClass{Generalizable}{\text{rwds}}}}\, \,\href{Axiom.Set.Map.html#6320}{\htmlId{4675}{\htmlClass{Function Operator}{\text{∪ˡ}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{4678}{\htmlClass{Field Operator}{\text{❴}}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#3168}{\htmlId{4680}{\htmlClass{Generalizable}{\text{c}}}}\, , \,\htmlId{4684}{\htmlClass{Number}{\text{0}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{4686}{\htmlClass{Field Operator}{\text{❵}}}}\,
      \\ \,\href{Ledger.Conway.Conformance.Certs.html#1857}{\htmlId{4696}{\htmlClass{Function}{\text{updateCertDeposit}}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#3471}{\htmlId{4714}{\htmlClass{Generalizable}{\text{pp}}}}\, \,\htmlId{4717}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Conway.Specification.Certs.html#2098}{\htmlId{4718}{\htmlClass{InductiveConstructor}{\text{delegate}}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#3168}{\htmlId{4727}{\htmlClass{Generalizable}{\text{c}}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#3498}{\htmlId{4729}{\htmlClass{Generalizable}{\text{mv}}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#3403}{\htmlId{4732}{\htmlClass{Generalizable}{\text{mkh}}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#3114}{\htmlId{4736}{\htmlClass{Generalizable}{\text{d}}}}\,\,\htmlId{4737}{\htmlClass{Symbol}{\text{)}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#3291}{\htmlId{4739}{\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#3471}{\htmlId{4901}{\htmlClass{Generalizable}{\text{pp}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#2945}{\htmlId{4906}{\htmlClass{Generalizable}{\text{pools}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3234}{\htmlId{4914}{\htmlClass{Generalizable}{\text{delegatees}}}}\, \end{pmatrix}$ ⊢
      $\begin{pmatrix} \,\href{Ledger.Conway.Conformance.Certs.html#2907}{\htmlId{4937}{\htmlClass{Generalizable}{\text{vDelegs}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#2802}{\htmlId{4947}{\htmlClass{Generalizable}{\text{sDelegs}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#2721}{\htmlId{4957}{\htmlClass{Generalizable}{\text{rwds}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3291}{\htmlId{4964}{\htmlClass{Generalizable}{\text{dep}}}}\, \end{pmatrix}$
      ⇀⦇ dereg c md ,DELEG⦈
      $\begin{pmatrix} \,\href{Ledger.Conway.Conformance.Certs.html#2907}{\htmlId{5006}{\htmlClass{Generalizable}{\text{vDelegs}}}}\, \,\href{Axiom.Set.Map.html#10748}{\htmlId{5014}{\htmlClass{Function Operator}{\text{∣}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{5016}{\htmlClass{Field Operator}{\text{❴}}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#3168}{\htmlId{5018}{\htmlClass{Generalizable}{\text{c}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{5020}{\htmlClass{Field Operator}{\text{❵}}}}\, \,\href{Axiom.Set.Map.html#10748}{\htmlId{5022}{\htmlClass{Function Operator}{\text{ᶜ}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#2802}{\htmlId{5026}{\htmlClass{Generalizable}{\text{sDelegs}}}}\, \,\href{Axiom.Set.Map.html#10748}{\htmlId{5034}{\htmlClass{Function Operator}{\text{∣}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{5036}{\htmlClass{Field Operator}{\text{❴}}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#3168}{\htmlId{5038}{\htmlClass{Generalizable}{\text{c}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{5040}{\htmlClass{Field Operator}{\text{❵}}}}\, \,\href{Axiom.Set.Map.html#10748}{\htmlId{5042}{\htmlClass{Function Operator}{\text{ᶜ}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#2721}{\htmlId{5046}{\htmlClass{Generalizable}{\text{rwds}}}}\, \,\href{Axiom.Set.Map.html#10748}{\htmlId{5051}{\htmlClass{Function Operator}{\text{∣}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{5053}{\htmlClass{Field Operator}{\text{❴}}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#3168}{\htmlId{5055}{\htmlClass{Generalizable}{\text{c}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{5057}{\htmlClass{Field Operator}{\text{❵}}}}\, \,\href{Axiom.Set.Map.html#10748}{\htmlId{5059}{\htmlClass{Function Operator}{\text{ᶜ}}}}\,
      \\ \,\href{Ledger.Conway.Conformance.Certs.html#1857}{\htmlId{5069}{\htmlClass{Function}{\text{updateCertDeposit}}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#3471}{\htmlId{5087}{\htmlClass{Generalizable}{\text{pp}}}}\, \,\htmlId{5090}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Conway.Specification.Certs.html#2171}{\htmlId{5091}{\htmlClass{InductiveConstructor}{\text{dereg}}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#3168}{\htmlId{5097}{\htmlClass{Generalizable}{\text{c}}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#3138}{\htmlId{5099}{\htmlClass{Generalizable}{\text{md}}}}\,\,\htmlId{5101}{\htmlClass{Symbol}{\text{)}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#3291}{\htmlId{5103}{\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#3471}{\htmlId{5242}{\htmlClass{Generalizable}{\text{pp}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#2945}{\htmlId{5247}{\htmlClass{Generalizable}{\text{pools}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3234}{\htmlId{5255}{\htmlClass{Generalizable}{\text{delegatees}}}}\, \end{pmatrix}$ ⊢
        $\begin{pmatrix} \,\href{Ledger.Conway.Conformance.Certs.html#2907}{\htmlId{5280}{\htmlClass{Generalizable}{\text{vDelegs}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#2802}{\htmlId{5290}{\htmlClass{Generalizable}{\text{sDelegs}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#2721}{\htmlId{5300}{\htmlClass{Generalizable}{\text{rwds}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3291}{\htmlId{5307}{\htmlClass{Generalizable}{\text{dep}}}}\, \end{pmatrix}$ ⇀⦇ reg c d ,DELEG⦈
        $\begin{pmatrix} \,\href{Ledger.Conway.Conformance.Certs.html#2907}{\htmlId{5342}{\htmlClass{Generalizable}{\text{vDelegs}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#2802}{\htmlId{5352}{\htmlClass{Generalizable}{\text{sDelegs}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#2721}{\htmlId{5362}{\htmlClass{Generalizable}{\text{rwds}}}}\, \,\href{Axiom.Set.Map.html#6320}{\htmlId{5367}{\htmlClass{Function Operator}{\text{∪ˡ}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{5370}{\htmlClass{Field Operator}{\text{❴}}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#3168}{\htmlId{5372}{\htmlClass{Generalizable}{\text{c}}}}\, , \,\htmlId{5376}{\htmlClass{Number}{\text{0}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{5378}{\htmlClass{Field Operator}{\text{❵}}}}\,
        \\ \,\href{Ledger.Conway.Conformance.Certs.html#1857}{\htmlId{5390}{\htmlClass{Function}{\text{updateCertDeposit}}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#3471}{\htmlId{5408}{\htmlClass{Generalizable}{\text{pp}}}}\, \,\htmlId{5411}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Conway.Specification.Certs.html#2789}{\htmlId{5412}{\htmlClass{InductiveConstructor}{\text{reg}}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#3168}{\htmlId{5416}{\htmlClass{Generalizable}{\text{c}}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#3114}{\htmlId{5418}{\htmlClass{Generalizable}{\text{d}}}}\,\,\htmlId{5419}{\htmlClass{Symbol}{\text{)}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#3291}{\htmlId{5421}{\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#3319}{\htmlId{5664}{\htmlClass{Generalizable}{\text{e}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#5522}{\htmlId{5668}{\htmlClass{Bound}{\text{pp}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3344}{\htmlId{5673}{\htmlClass{Generalizable}{\text{vs}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3021}{\htmlId{5678}{\htmlClass{Generalizable}{\text{wdrls}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3245}{\htmlId{5686}{\htmlClass{Generalizable}{\text{cc}}}}\, \end{pmatrix}$ ⊢
      $\begin{pmatrix} \,\href{Ledger.Conway.Conformance.Certs.html#2756}{\htmlId{5701}{\htmlClass{Generalizable}{\text{dReps}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#2850}{\htmlId{5709}{\htmlClass{Generalizable}{\text{ccKeys}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3291}{\htmlId{5718}{\htmlClass{Generalizable}{\text{dep}}}}\, \end{pmatrix}$
        ⇀⦇ regdrep c d an ,GOVCERT⦈
      $\begin{pmatrix} \,\href{Class.HasSingleton.html#288}{\htmlId{5768}{\htmlClass{Field Operator}{\text{❴}}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#3168}{\htmlId{5770}{\htmlClass{Generalizable}{\text{c}}}}\, , \,\href{Ledger.Conway.Conformance.Certs.html#3319}{\htmlId{5774}{\htmlClass{Generalizable}{\text{e}}}}\, \,\href{Class.HasAdd.Core.html#162}{\htmlId{5776}{\htmlClass{Field Operator}{\text{+}}}}\, \,\href{Ledger.Conway.Specification.PParams.html#3442}{\htmlId{5778}{\htmlClass{Field}{\text{drepActivity}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{5791}{\htmlClass{Field Operator}{\text{❵}}}}\, \,\href{Axiom.Set.Map.html#6320}{\htmlId{5793}{\htmlClass{Function Operator}{\text{∪ˡ}}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#2756}{\htmlId{5796}{\htmlClass{Generalizable}{\text{dReps}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#2850}{\htmlId{5804}{\htmlClass{Generalizable}{\text{ccKeys}}}}\,
      \\ \,\href{Ledger.Conway.Conformance.Certs.html#1857}{\htmlId{5819}{\htmlClass{Function}{\text{updateCertDeposit}}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#5522}{\htmlId{5837}{\htmlClass{Bound}{\text{pp}}}}\, \,\htmlId{5840}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Conway.Specification.Certs.html#2309}{\htmlId{5841}{\htmlClass{InductiveConstructor}{\text{regdrep}}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#3168}{\htmlId{5849}{\htmlClass{Generalizable}{\text{c}}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#3114}{\htmlId{5851}{\htmlClass{Generalizable}{\text{d}}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#3061}{\htmlId{5853}{\htmlClass{Generalizable}{\text{an}}}}\, \,\htmlId{5856}{\htmlClass{Symbol}{\text{)}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#3291}{\htmlId{5858}{\htmlClass{Generalizable}{\text{dep}}}}\, \end{pmatrix}$

  GOVCERT-deregdrep :
    ∙ c ∈ dom dReps
    ∙ (DRepDeposit c , d) ∈ dep
      ────────────────────────────────
      $\begin{pmatrix} \,\href{Ledger.Conway.Conformance.Certs.html#3319}{\htmlId{5986}{\htmlClass{Generalizable}{\text{e}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3471}{\htmlId{5990}{\htmlClass{Generalizable}{\text{pp}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3344}{\htmlId{5995}{\htmlClass{Generalizable}{\text{vs}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3021}{\htmlId{6000}{\htmlClass{Generalizable}{\text{wdrls}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3245}{\htmlId{6008}{\htmlClass{Generalizable}{\text{cc}}}}\, \end{pmatrix}$ ⊢ $\begin{pmatrix} \,\href{Ledger.Conway.Conformance.Certs.html#2756}{\htmlId{6017}{\htmlClass{Generalizable}{\text{dReps}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#2850}{\htmlId{6025}{\htmlClass{Generalizable}{\text{ccKeys}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3291}{\htmlId{6034}{\htmlClass{Generalizable}{\text{dep}}}}\, \end{pmatrix}$
          ⇀⦇ deregdrep c d ,GOVCERT⦈
          $\begin{pmatrix} \,\href{Ledger.Conway.Conformance.Certs.html#2756}{\htmlId{6089}{\htmlClass{Generalizable}{\text{dReps}}}}\, \,\href{Axiom.Set.Map.html#10748}{\htmlId{6095}{\htmlClass{Function Operator}{\text{∣}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{6097}{\htmlClass{Field Operator}{\text{❴}}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#3168}{\htmlId{6099}{\htmlClass{Generalizable}{\text{c}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{6101}{\htmlClass{Field Operator}{\text{❵}}}}\, \,\href{Axiom.Set.Map.html#10748}{\htmlId{6103}{\htmlClass{Function Operator}{\text{ᶜ}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#2850}{\htmlId{6107}{\htmlClass{Generalizable}{\text{ccKeys}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#1857}{\htmlId{6116}{\htmlClass{Function}{\text{updateCertDeposit}}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#3471}{\htmlId{6134}{\htmlClass{Generalizable}{\text{pp}}}}\, \,\htmlId{6137}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Conway.Specification.Certs.html#2360}{\htmlId{6138}{\htmlClass{InductiveConstructor}{\text{deregdrep}}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#3168}{\htmlId{6148}{\htmlClass{Generalizable}{\text{c}}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#3114}{\htmlId{6150}{\htmlClass{Generalizable}{\text{d}}}}\,\,\htmlId{6151}{\htmlClass{Symbol}{\text{)}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#3291}{\htmlId{6153}{\htmlClass{Generalizable}{\text{dep}}}}\, \end{pmatrix}$

  GOVCERT-ccreghot :
    ∙ (c , nothing) ∉ ccKeys
    ∙ c ∈ cc
      ────────────────────────────────
      $\begin{pmatrix} \,\href{Ledger.Conway.Conformance.Certs.html#3319}{\htmlId{6270}{\htmlClass{Generalizable}{\text{e}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3471}{\htmlId{6274}{\htmlClass{Generalizable}{\text{pp}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3344}{\htmlId{6279}{\htmlClass{Generalizable}{\text{vs}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3021}{\htmlId{6284}{\htmlClass{Generalizable}{\text{wdrls}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3245}{\htmlId{6292}{\htmlClass{Generalizable}{\text{cc}}}}\, \end{pmatrix}$ ⊢ $\begin{pmatrix} \,\href{Ledger.Conway.Conformance.Certs.html#2756}{\htmlId{6301}{\htmlClass{Generalizable}{\text{dReps}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#2850}{\htmlId{6309}{\htmlClass{Generalizable}{\text{ccKeys}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3291}{\htmlId{6318}{\htmlClass{Generalizable}{\text{dep}}}}\, \end{pmatrix}$
          ⇀⦇ ccreghot c mc ,GOVCERT⦈
          $\begin{pmatrix} \,\href{Ledger.Conway.Conformance.Certs.html#2756}{\htmlId{6373}{\htmlClass{Generalizable}{\text{dReps}}}}\, \\ \,\href{Class.HasSingleton.html#288}{\htmlId{6381}{\htmlClass{Field Operator}{\text{❴}}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#3168}{\htmlId{6383}{\htmlClass{Generalizable}{\text{c}}}}\, , \,\href{Ledger.Conway.Conformance.Certs.html#3198}{\htmlId{6387}{\htmlClass{Generalizable}{\text{mc}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{6390}{\htmlClass{Field Operator}{\text{❵}}}}\, \,\href{Axiom.Set.Map.html#6320}{\htmlId{6392}{\htmlClass{Function Operator}{\text{∪ˡ}}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#2850}{\htmlId{6395}{\htmlClass{Generalizable}{\text{ccKeys}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#1857}{\htmlId{6404}{\htmlClass{Function}{\text{updateCertDeposit}}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#3471}{\htmlId{6422}{\htmlClass{Generalizable}{\text{pp}}}}\, \,\htmlId{6425}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Conway.Specification.Certs.html#2402}{\htmlId{6426}{\htmlClass{InductiveConstructor}{\text{ccreghot}}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#3168}{\htmlId{6435}{\htmlClass{Generalizable}{\text{c}}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#3198}{\htmlId{6437}{\htmlClass{Generalizable}{\text{mc}}}}\,\,\htmlId{6439}{\htmlClass{Symbol}{\text{)}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#3291}{\htmlId{6441}{\htmlClass{Generalizable}{\text{dep}}}}\, \end{pmatrix}$

data _⊢_⇀⦇_,CERT⦈_ : CertEnv → CertState → DCert → CertState → Type where
  CERT-deleg :
    ∙ $\begin{pmatrix} \,\href{Ledger.Conway.Conformance.Certs.html#3471}{\htmlId{6545}{\htmlClass{Generalizable}{\text{pp}}}}\, \\ \,\href{Ledger.Conway.Specification.Certs.html#3901}{\htmlId{6550}{\htmlClass{Field}{\text{PState.pools}}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#3571}{\htmlId{6563}{\htmlClass{Generalizable}{\text{stᵖ}}}}\, \\ \,\href{Class.IsSet.html#916}{\htmlId{6569}{\htmlClass{Function}{\text{dom}}}}\, \,\htmlId{6573}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Conway.Conformance.Certs.html#838}{\htmlId{6574}{\htmlClass{Field}{\text{GState.dreps}}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#3551}{\htmlId{6587}{\htmlClass{Generalizable}{\text{stᵍ}}}}\,\,\htmlId{6590}{\htmlClass{Symbol}{\text{)}}}\, \end{pmatrix}$ ⊢ stᵈ ⇀⦇ dCert ,DELEG⦈ stᵈ'
      ────────────────────────────────
      $\begin{pmatrix} \,\href{Ledger.Conway.Conformance.Certs.html#3319}{\htmlId{6669}{\htmlClass{Generalizable}{\text{e}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3471}{\htmlId{6673}{\htmlClass{Generalizable}{\text{pp}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3344}{\htmlId{6678}{\htmlClass{Generalizable}{\text{vs}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3021}{\htmlId{6683}{\htmlClass{Generalizable}{\text{wdrls}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3245}{\htmlId{6691}{\htmlClass{Generalizable}{\text{cc}}}}\, \end{pmatrix}$ ⊢ $\begin{pmatrix} \,\href{Ledger.Conway.Conformance.Certs.html#3531}{\htmlId{6700}{\htmlClass{Generalizable}{\text{stᵈ}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3571}{\htmlId{6706}{\htmlClass{Generalizable}{\text{stᵖ}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3551}{\htmlId{6712}{\htmlClass{Generalizable}{\text{stᵍ}}}}\, \end{pmatrix}$ ⇀⦇ dCert ,CERT⦈ $\begin{pmatrix} \,\href{Ledger.Conway.Conformance.Certs.html#3535}{\htmlId{6736}{\htmlClass{Generalizable}{\text{stᵈ'}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3571}{\htmlId{6743}{\htmlClass{Generalizable}{\text{stᵖ}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3551}{\htmlId{6749}{\htmlClass{Generalizable}{\text{stᵍ}}}}\, \end{pmatrix}$

  CERT-pool :
    ∙ pp ⊢ stᵖ ⇀⦇ dCert ,POOL⦈ stᵖ'
      ────────────────────────────────
      $\begin{pmatrix} \,\href{Ledger.Conway.Conformance.Certs.html#3319}{\htmlId{6853}{\htmlClass{Generalizable}{\text{e}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3471}{\htmlId{6857}{\htmlClass{Generalizable}{\text{pp}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3344}{\htmlId{6862}{\htmlClass{Generalizable}{\text{vs}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3021}{\htmlId{6867}{\htmlClass{Generalizable}{\text{wdrls}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3245}{\htmlId{6875}{\htmlClass{Generalizable}{\text{cc}}}}\, \end{pmatrix}$ ⊢ $\begin{pmatrix} \,\href{Ledger.Conway.Conformance.Certs.html#3531}{\htmlId{6884}{\htmlClass{Generalizable}{\text{stᵈ}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3571}{\htmlId{6890}{\htmlClass{Generalizable}{\text{stᵖ}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3551}{\htmlId{6896}{\htmlClass{Generalizable}{\text{stᵍ}}}}\, \end{pmatrix}$ ⇀⦇ dCert ,CERT⦈ $\begin{pmatrix} \,\href{Ledger.Conway.Conformance.Certs.html#3531}{\htmlId{6920}{\htmlClass{Generalizable}{\text{stᵈ}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3575}{\htmlId{6926}{\htmlClass{Generalizable}{\text{stᵖ'}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3551}{\htmlId{6933}{\htmlClass{Generalizable}{\text{stᵍ}}}}\, \end{pmatrix}$

  CERT-vdel :
    ∙ Γ ⊢ stᵍ ⇀⦇ dCert ,GOVCERT⦈ stᵍ'
      ────────────────────────────────
      Γ ⊢ $\begin{pmatrix} \,\href{Ledger.Conway.Conformance.Certs.html#3531}{\htmlId{7043}{\htmlClass{Generalizable}{\text{stᵈ}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3571}{\htmlId{7049}{\htmlClass{Generalizable}{\text{stᵖ}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3551}{\htmlId{7055}{\htmlClass{Generalizable}{\text{stᵍ}}}}\, \end{pmatrix}$ ⇀⦇ dCert ,CERT⦈ $\begin{pmatrix} \,\href{Ledger.Conway.Conformance.Certs.html#3531}{\htmlId{7079}{\htmlClass{Generalizable}{\text{stᵈ}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3571}{\htmlId{7085}{\htmlClass{Generalizable}{\text{stᵖ}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3555}{\htmlId{7091}{\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#3319}{\htmlId{7684}{\htmlClass{Generalizable}{\text{e}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3471}{\htmlId{7688}{\htmlClass{Generalizable}{\text{pp}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3344}{\htmlId{7693}{\htmlClass{Generalizable}{\text{vs}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3021}{\htmlId{7698}{\htmlClass{Generalizable}{\text{wdrls}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3245}{\htmlId{7706}{\htmlClass{Generalizable}{\text{cc}}}}\, \end{pmatrix}$ ⊢
      $\begin{pmatrix} \begin{pmatrix} \,\href{Ledger.Conway.Conformance.Certs.html#2915}{\htmlId{7723}{\htmlClass{Generalizable}{\text{voteDelegs}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#2810}{\htmlId{7736}{\htmlClass{Generalizable}{\text{stakeDelegs}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#2726}{\htmlId{7750}{\htmlClass{Generalizable}{\text{rewards}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3295}{\htmlId{7760}{\htmlClass{Generalizable}{\text{ddep}}}}\, \end{pmatrix}
      \\ \,\href{Ledger.Conway.Conformance.Certs.html#3571}{\htmlId{7775}{\htmlClass{Generalizable}{\text{stᵖ}}}}\,
      \\ \begin{pmatrix} \,\href{Ledger.Conway.Conformance.Certs.html#2756}{\htmlId{7789}{\htmlClass{Generalizable}{\text{dReps}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#2857}{\htmlId{7797}{\htmlClass{Generalizable}{\text{ccHotKeys}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3300}{\htmlId{7809}{\htmlClass{Generalizable}{\text{gdep}}}}\, \end{pmatrix}
      \end{pmatrix}$
      ⇀⦇ _ ,CERTBASE⦈
      $\begin{pmatrix} \begin{pmatrix} \,\href{Ledger.Conway.Conformance.Certs.html#7417}{\htmlId{7856}{\htmlClass{Bound}{\text{validVoteDelegs}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#2810}{\htmlId{7874}{\htmlClass{Generalizable}{\text{stakeDelegs}}}}\, \\ \,\href{Axiom.Set.Map.html#9130}{\htmlId{7888}{\htmlClass{Function}{\text{constMap}}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#7368}{\htmlId{7897}{\htmlClass{Bound}{\text{wdrlCreds}}}}\, \,\htmlId{7907}{\htmlClass{Number}{\text{0}}}\, \,\href{Axiom.Set.Map.html#6320}{\htmlId{7909}{\htmlClass{Function Operator}{\text{∪ˡ}}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#2726}{\htmlId{7912}{\htmlClass{Generalizable}{\text{rewards}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3295}{\htmlId{7922}{\htmlClass{Generalizable}{\text{ddep}}}}\, \end{pmatrix}
      \\ \,\href{Ledger.Conway.Conformance.Certs.html#3571}{\htmlId{7937}{\htmlClass{Generalizable}{\text{stᵖ}}}}\,
      \\ \begin{pmatrix} \,\href{Ledger.Conway.Conformance.Certs.html#7282}{\htmlId{7951}{\htmlClass{Bound}{\text{refreshedDReps}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#2857}{\htmlId{7968}{\htmlClass{Generalizable}{\text{ccHotKeys}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3300}{\htmlId{7980}{\htmlClass{Generalizable}{\text{gdep}}}}\, \end{pmatrix}
      \end{pmatrix}$

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