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;
          _⊢_⇀⦇_,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 _⊢_⇀⦇_,DELEG⦈_ : DelegEnv → DState → DCert → DState → Type

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#3476}{\htmlId{4090}{\htmlClass{Generalizable}{\text{pp}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#2950}{\htmlId{4095}{\htmlClass{Generalizable}{\text{pools}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3239}{\htmlId{4103}{\htmlClass{Generalizable}{\text{delegatees}}}}\, \end{pmatrix}$ ⊢
      $\begin{pmatrix} \,\href{Ledger.Conway.Conformance.Certs.html#2912}{\htmlId{4126}{\htmlClass{Generalizable}{\text{vDelegs}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#2807}{\htmlId{4136}{\htmlClass{Generalizable}{\text{sDelegs}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#2726}{\htmlId{4146}{\htmlClass{Generalizable}{\text{rwds}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3296}{\htmlId{4153}{\htmlClass{Generalizable}{\text{dep}}}}\, \end{pmatrix}$
      ⇀⦇ delegate c mv mkh d ,DELEG⦈
      $\begin{pmatrix} \,\href{Axiom.Set.Map.html#9260}{\htmlId{4204}{\htmlClass{Function}{\text{insertIfJust}}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#3173}{\htmlId{4217}{\htmlClass{Generalizable}{\text{c}}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#3503}{\htmlId{4219}{\htmlClass{Generalizable}{\text{mv}}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#2912}{\htmlId{4222}{\htmlClass{Generalizable}{\text{vDelegs}}}}\, \\ \,\href{Axiom.Set.Map.html#9260}{\htmlId{4232}{\htmlClass{Function}{\text{insertIfJust}}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#3173}{\htmlId{4245}{\htmlClass{Generalizable}{\text{c}}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#3408}{\htmlId{4247}{\htmlClass{Generalizable}{\text{mkh}}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#2807}{\htmlId{4251}{\htmlClass{Generalizable}{\text{sDelegs}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#2726}{\htmlId{4261}{\htmlClass{Generalizable}{\text{rwds}}}}\, \,\href{Axiom.Set.Map.html#7638}{\htmlId{4266}{\htmlClass{Function Operator}{\text{∪ˡ}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{4269}{\htmlClass{Field Operator}{\text{❴}}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#3173}{\htmlId{4271}{\htmlClass{Generalizable}{\text{c}}}}\, , \,\htmlId{4275}{\htmlClass{Number}{\text{0}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{4277}{\htmlClass{Field Operator}{\text{❵}}}}\,
      \\ \,\href{Ledger.Conway.Conformance.Certs.html#1862}{\htmlId{4287}{\htmlClass{Function}{\text{updateCertDeposit}}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#3476}{\htmlId{4305}{\htmlClass{Generalizable}{\text{pp}}}}\, \,\htmlId{4308}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Conway.Specification.Certs.html#2276}{\htmlId{4309}{\htmlClass{InductiveConstructor}{\text{delegate}}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#3173}{\htmlId{4318}{\htmlClass{Generalizable}{\text{c}}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#3503}{\htmlId{4320}{\htmlClass{Generalizable}{\text{mv}}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#3408}{\htmlId{4323}{\htmlClass{Generalizable}{\text{mkh}}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#3119}{\htmlId{4327}{\htmlClass{Generalizable}{\text{d}}}}\,\,\htmlId{4328}{\htmlClass{Symbol}{\text{)}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#3296}{\htmlId{4330}{\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#3476}{\htmlId{4492}{\htmlClass{Generalizable}{\text{pp}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#2950}{\htmlId{4497}{\htmlClass{Generalizable}{\text{pools}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3239}{\htmlId{4505}{\htmlClass{Generalizable}{\text{delegatees}}}}\, \end{pmatrix}$ ⊢
      $\begin{pmatrix} \,\href{Ledger.Conway.Conformance.Certs.html#2912}{\htmlId{4528}{\htmlClass{Generalizable}{\text{vDelegs}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#2807}{\htmlId{4538}{\htmlClass{Generalizable}{\text{sDelegs}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#2726}{\htmlId{4548}{\htmlClass{Generalizable}{\text{rwds}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3296}{\htmlId{4555}{\htmlClass{Generalizable}{\text{dep}}}}\, \end{pmatrix}$
      ⇀⦇ dereg c md ,DELEG⦈
      $\begin{pmatrix} \,\href{Ledger.Conway.Conformance.Certs.html#2912}{\htmlId{4597}{\htmlClass{Generalizable}{\text{vDelegs}}}}\, \,\href{Axiom.Set.Map.html#13604}{\htmlId{4605}{\htmlClass{Function Operator}{\text{∣}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{4607}{\htmlClass{Field Operator}{\text{❴}}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#3173}{\htmlId{4609}{\htmlClass{Generalizable}{\text{c}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{4611}{\htmlClass{Field Operator}{\text{❵}}}}\, \,\href{Axiom.Set.Map.html#13604}{\htmlId{4613}{\htmlClass{Function Operator}{\text{ᶜ}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#2807}{\htmlId{4617}{\htmlClass{Generalizable}{\text{sDelegs}}}}\, \,\href{Axiom.Set.Map.html#13604}{\htmlId{4625}{\htmlClass{Function Operator}{\text{∣}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{4627}{\htmlClass{Field Operator}{\text{❴}}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#3173}{\htmlId{4629}{\htmlClass{Generalizable}{\text{c}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{4631}{\htmlClass{Field Operator}{\text{❵}}}}\, \,\href{Axiom.Set.Map.html#13604}{\htmlId{4633}{\htmlClass{Function Operator}{\text{ᶜ}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#2726}{\htmlId{4637}{\htmlClass{Generalizable}{\text{rwds}}}}\, \,\href{Axiom.Set.Map.html#13604}{\htmlId{4642}{\htmlClass{Function Operator}{\text{∣}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{4644}{\htmlClass{Field Operator}{\text{❴}}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#3173}{\htmlId{4646}{\htmlClass{Generalizable}{\text{c}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{4648}{\htmlClass{Field Operator}{\text{❵}}}}\, \,\href{Axiom.Set.Map.html#13604}{\htmlId{4650}{\htmlClass{Function Operator}{\text{ᶜ}}}}\,
      \\ \,\href{Ledger.Conway.Conformance.Certs.html#1862}{\htmlId{4660}{\htmlClass{Function}{\text{updateCertDeposit}}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#3476}{\htmlId{4678}{\htmlClass{Generalizable}{\text{pp}}}}\, \,\htmlId{4681}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Conway.Specification.Certs.html#2349}{\htmlId{4682}{\htmlClass{InductiveConstructor}{\text{dereg}}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#3173}{\htmlId{4688}{\htmlClass{Generalizable}{\text{c}}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#3143}{\htmlId{4690}{\htmlClass{Generalizable}{\text{md}}}}\,\,\htmlId{4692}{\htmlClass{Symbol}{\text{)}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#3296}{\htmlId{4694}{\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#3476}{\htmlId{4833}{\htmlClass{Generalizable}{\text{pp}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#2950}{\htmlId{4838}{\htmlClass{Generalizable}{\text{pools}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3239}{\htmlId{4846}{\htmlClass{Generalizable}{\text{delegatees}}}}\, \end{pmatrix}$ ⊢
        $\begin{pmatrix} \,\href{Ledger.Conway.Conformance.Certs.html#2912}{\htmlId{4871}{\htmlClass{Generalizable}{\text{vDelegs}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#2807}{\htmlId{4881}{\htmlClass{Generalizable}{\text{sDelegs}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#2726}{\htmlId{4891}{\htmlClass{Generalizable}{\text{rwds}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3296}{\htmlId{4898}{\htmlClass{Generalizable}{\text{dep}}}}\, \end{pmatrix}$ ⇀⦇ reg c d ,DELEG⦈
        $\begin{pmatrix} \,\href{Ledger.Conway.Conformance.Certs.html#2912}{\htmlId{4933}{\htmlClass{Generalizable}{\text{vDelegs}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#2807}{\htmlId{4943}{\htmlClass{Generalizable}{\text{sDelegs}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#2726}{\htmlId{4953}{\htmlClass{Generalizable}{\text{rwds}}}}\, \,\href{Axiom.Set.Map.html#7638}{\htmlId{4958}{\htmlClass{Function Operator}{\text{∪ˡ}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{4961}{\htmlClass{Field Operator}{\text{❴}}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#3173}{\htmlId{4963}{\htmlClass{Generalizable}{\text{c}}}}\, , \,\htmlId{4967}{\htmlClass{Number}{\text{0}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{4969}{\htmlClass{Field Operator}{\text{❵}}}}\,
        \\ \,\href{Ledger.Conway.Conformance.Certs.html#1862}{\htmlId{4981}{\htmlClass{Function}{\text{updateCertDeposit}}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#3476}{\htmlId{4999}{\htmlClass{Generalizable}{\text{pp}}}}\, \,\htmlId{5002}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Conway.Specification.Certs.html#2968}{\htmlId{5003}{\htmlClass{InductiveConstructor}{\text{reg}}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#3173}{\htmlId{5007}{\htmlClass{Generalizable}{\text{c}}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#3119}{\htmlId{5009}{\htmlClass{Generalizable}{\text{d}}}}\,\,\htmlId{5010}{\htmlClass{Symbol}{\text{)}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#3296}{\htmlId{5012}{\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#3324}{\htmlId{5255}{\htmlClass{Generalizable}{\text{e}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#5113}{\htmlId{5259}{\htmlClass{Bound}{\text{pp}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3349}{\htmlId{5264}{\htmlClass{Generalizable}{\text{vs}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3026}{\htmlId{5269}{\htmlClass{Generalizable}{\text{wdrls}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3250}{\htmlId{5277}{\htmlClass{Generalizable}{\text{cc}}}}\, \end{pmatrix}$ ⊢
      $\begin{pmatrix} \,\href{Ledger.Conway.Conformance.Certs.html#2761}{\htmlId{5292}{\htmlClass{Generalizable}{\text{dReps}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#2855}{\htmlId{5300}{\htmlClass{Generalizable}{\text{ccKeys}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3296}{\htmlId{5309}{\htmlClass{Generalizable}{\text{dep}}}}\, \end{pmatrix}$
        ⇀⦇ regdrep c d an ,GOVCERT⦈
      $\begin{pmatrix} \,\href{Class.HasSingleton.html#288}{\htmlId{5359}{\htmlClass{Field Operator}{\text{❴}}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#3173}{\htmlId{5361}{\htmlClass{Generalizable}{\text{c}}}}\, , \,\href{Ledger.Conway.Conformance.Certs.html#3324}{\htmlId{5365}{\htmlClass{Generalizable}{\text{e}}}}\, \,\href{Class.HasAdd.Core.html#162}{\htmlId{5367}{\htmlClass{Field Operator}{\text{+}}}}\, \,\href{Ledger.Conway.Specification.PParams.html#3446}{\htmlId{5369}{\htmlClass{Field}{\text{drepActivity}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{5382}{\htmlClass{Field Operator}{\text{❵}}}}\, \,\href{Axiom.Set.Map.html#7638}{\htmlId{5384}{\htmlClass{Function Operator}{\text{∪ˡ}}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#2761}{\htmlId{5387}{\htmlClass{Generalizable}{\text{dReps}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#2855}{\htmlId{5395}{\htmlClass{Generalizable}{\text{ccKeys}}}}\,
      \\ \,\href{Ledger.Conway.Conformance.Certs.html#1862}{\htmlId{5410}{\htmlClass{Function}{\text{updateCertDeposit}}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#5113}{\htmlId{5428}{\htmlClass{Bound}{\text{pp}}}}\, \,\htmlId{5431}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Conway.Specification.Certs.html#2487}{\htmlId{5432}{\htmlClass{InductiveConstructor}{\text{regdrep}}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#3173}{\htmlId{5440}{\htmlClass{Generalizable}{\text{c}}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#3119}{\htmlId{5442}{\htmlClass{Generalizable}{\text{d}}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#3066}{\htmlId{5444}{\htmlClass{Generalizable}{\text{an}}}}\, \,\htmlId{5447}{\htmlClass{Symbol}{\text{)}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#3296}{\htmlId{5449}{\htmlClass{Generalizable}{\text{dep}}}}\, \end{pmatrix}$

  GOVCERT-deregdrep :
    ∙ c ∈ dom dReps
    ∙ (DRepDeposit c , d) ∈ dep
      ────────────────────────────────
      $\begin{pmatrix} \,\href{Ledger.Conway.Conformance.Certs.html#3324}{\htmlId{5577}{\htmlClass{Generalizable}{\text{e}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3476}{\htmlId{5581}{\htmlClass{Generalizable}{\text{pp}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3349}{\htmlId{5586}{\htmlClass{Generalizable}{\text{vs}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3026}{\htmlId{5591}{\htmlClass{Generalizable}{\text{wdrls}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3250}{\htmlId{5599}{\htmlClass{Generalizable}{\text{cc}}}}\, \end{pmatrix}$ ⊢ $\begin{pmatrix} \,\href{Ledger.Conway.Conformance.Certs.html#2761}{\htmlId{5608}{\htmlClass{Generalizable}{\text{dReps}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#2855}{\htmlId{5616}{\htmlClass{Generalizable}{\text{ccKeys}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3296}{\htmlId{5625}{\htmlClass{Generalizable}{\text{dep}}}}\, \end{pmatrix}$
          ⇀⦇ deregdrep c d ,GOVCERT⦈
          $\begin{pmatrix} \,\href{Ledger.Conway.Conformance.Certs.html#2761}{\htmlId{5680}{\htmlClass{Generalizable}{\text{dReps}}}}\, \,\href{Axiom.Set.Map.html#13604}{\htmlId{5686}{\htmlClass{Function Operator}{\text{∣}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{5688}{\htmlClass{Field Operator}{\text{❴}}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#3173}{\htmlId{5690}{\htmlClass{Generalizable}{\text{c}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{5692}{\htmlClass{Field Operator}{\text{❵}}}}\, \,\href{Axiom.Set.Map.html#13604}{\htmlId{5694}{\htmlClass{Function Operator}{\text{ᶜ}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#2855}{\htmlId{5698}{\htmlClass{Generalizable}{\text{ccKeys}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#1862}{\htmlId{5707}{\htmlClass{Function}{\text{updateCertDeposit}}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#3476}{\htmlId{5725}{\htmlClass{Generalizable}{\text{pp}}}}\, \,\htmlId{5728}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Conway.Specification.Certs.html#2538}{\htmlId{5729}{\htmlClass{InductiveConstructor}{\text{deregdrep}}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#3173}{\htmlId{5739}{\htmlClass{Generalizable}{\text{c}}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#3119}{\htmlId{5741}{\htmlClass{Generalizable}{\text{d}}}}\,\,\htmlId{5742}{\htmlClass{Symbol}{\text{)}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#3296}{\htmlId{5744}{\htmlClass{Generalizable}{\text{dep}}}}\, \end{pmatrix}$

  GOVCERT-ccreghot :
    ∙ (c , nothing) ∉ ccKeys
    ∙ c ∈ cc
      ────────────────────────────────
      $\begin{pmatrix} \,\href{Ledger.Conway.Conformance.Certs.html#3324}{\htmlId{5861}{\htmlClass{Generalizable}{\text{e}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3476}{\htmlId{5865}{\htmlClass{Generalizable}{\text{pp}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3349}{\htmlId{5870}{\htmlClass{Generalizable}{\text{vs}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3026}{\htmlId{5875}{\htmlClass{Generalizable}{\text{wdrls}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3250}{\htmlId{5883}{\htmlClass{Generalizable}{\text{cc}}}}\, \end{pmatrix}$ ⊢ $\begin{pmatrix} \,\href{Ledger.Conway.Conformance.Certs.html#2761}{\htmlId{5892}{\htmlClass{Generalizable}{\text{dReps}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#2855}{\htmlId{5900}{\htmlClass{Generalizable}{\text{ccKeys}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3296}{\htmlId{5909}{\htmlClass{Generalizable}{\text{dep}}}}\, \end{pmatrix}$
          ⇀⦇ ccreghot c mc ,GOVCERT⦈
          $\begin{pmatrix} \,\href{Ledger.Conway.Conformance.Certs.html#2761}{\htmlId{5964}{\htmlClass{Generalizable}{\text{dReps}}}}\, \\ \,\href{Class.HasSingleton.html#288}{\htmlId{5972}{\htmlClass{Field Operator}{\text{❴}}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#3173}{\htmlId{5974}{\htmlClass{Generalizable}{\text{c}}}}\, , \,\href{Ledger.Conway.Conformance.Certs.html#3203}{\htmlId{5978}{\htmlClass{Generalizable}{\text{mc}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{5981}{\htmlClass{Field Operator}{\text{❵}}}}\, \,\href{Axiom.Set.Map.html#7638}{\htmlId{5983}{\htmlClass{Function Operator}{\text{∪ˡ}}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#2855}{\htmlId{5986}{\htmlClass{Generalizable}{\text{ccKeys}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#1862}{\htmlId{5995}{\htmlClass{Function}{\text{updateCertDeposit}}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#3476}{\htmlId{6013}{\htmlClass{Generalizable}{\text{pp}}}}\, \,\htmlId{6016}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Conway.Specification.Certs.html#2580}{\htmlId{6017}{\htmlClass{InductiveConstructor}{\text{ccreghot}}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#3173}{\htmlId{6026}{\htmlClass{Generalizable}{\text{c}}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#3203}{\htmlId{6028}{\htmlClass{Generalizable}{\text{mc}}}}\,\,\htmlId{6030}{\htmlClass{Symbol}{\text{)}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#3296}{\htmlId{6032}{\htmlClass{Generalizable}{\text{dep}}}}\, \end{pmatrix}$

data _⊢_⇀⦇_,CERT⦈_ : CertEnv → CertState → DCert → CertState → Type where
  CERT-deleg :
    ∙ $\begin{pmatrix} \,\href{Ledger.Conway.Conformance.Certs.html#3476}{\htmlId{6136}{\htmlClass{Generalizable}{\text{pp}}}}\, \\ \,\href{Ledger.Conway.Specification.Certs.html#4080}{\htmlId{6141}{\htmlClass{Field}{\text{PState.pools}}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#3576}{\htmlId{6154}{\htmlClass{Generalizable}{\text{stᵖ}}}}\, \\ \,\href{Class.IsSet.html#916}{\htmlId{6160}{\htmlClass{Function}{\text{dom}}}}\, \,\htmlId{6164}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Conway.Conformance.Certs.html#843}{\htmlId{6165}{\htmlClass{Field}{\text{GState.dreps}}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#3556}{\htmlId{6178}{\htmlClass{Generalizable}{\text{stᵍ}}}}\,\,\htmlId{6181}{\htmlClass{Symbol}{\text{)}}}\, \end{pmatrix}$ ⊢ stᵈ ⇀⦇ dCert ,DELEG⦈ stᵈ'
      ────────────────────────────────
      $\begin{pmatrix} \,\href{Ledger.Conway.Conformance.Certs.html#3324}{\htmlId{6260}{\htmlClass{Generalizable}{\text{e}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3476}{\htmlId{6264}{\htmlClass{Generalizable}{\text{pp}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3349}{\htmlId{6269}{\htmlClass{Generalizable}{\text{vs}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3026}{\htmlId{6274}{\htmlClass{Generalizable}{\text{wdrls}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3250}{\htmlId{6282}{\htmlClass{Generalizable}{\text{cc}}}}\, \end{pmatrix}$ ⊢ $\begin{pmatrix} \,\href{Ledger.Conway.Conformance.Certs.html#3536}{\htmlId{6291}{\htmlClass{Generalizable}{\text{stᵈ}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3576}{\htmlId{6297}{\htmlClass{Generalizable}{\text{stᵖ}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3556}{\htmlId{6303}{\htmlClass{Generalizable}{\text{stᵍ}}}}\, \end{pmatrix}$ ⇀⦇ dCert ,CERT⦈ $\begin{pmatrix} \,\href{Ledger.Conway.Conformance.Certs.html#3540}{\htmlId{6327}{\htmlClass{Generalizable}{\text{stᵈ'}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3576}{\htmlId{6334}{\htmlClass{Generalizable}{\text{stᵖ}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3556}{\htmlId{6340}{\htmlClass{Generalizable}{\text{stᵍ}}}}\, \end{pmatrix}$

  CERT-pool :
    ∙ pp ⊢ stᵖ ⇀⦇ dCert ,POOL⦈ stᵖ'
      ────────────────────────────────
      $\begin{pmatrix} \,\href{Ledger.Conway.Conformance.Certs.html#3324}{\htmlId{6444}{\htmlClass{Generalizable}{\text{e}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3476}{\htmlId{6448}{\htmlClass{Generalizable}{\text{pp}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3349}{\htmlId{6453}{\htmlClass{Generalizable}{\text{vs}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3026}{\htmlId{6458}{\htmlClass{Generalizable}{\text{wdrls}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3250}{\htmlId{6466}{\htmlClass{Generalizable}{\text{cc}}}}\, \end{pmatrix}$ ⊢ $\begin{pmatrix} \,\href{Ledger.Conway.Conformance.Certs.html#3536}{\htmlId{6475}{\htmlClass{Generalizable}{\text{stᵈ}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3576}{\htmlId{6481}{\htmlClass{Generalizable}{\text{stᵖ}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3556}{\htmlId{6487}{\htmlClass{Generalizable}{\text{stᵍ}}}}\, \end{pmatrix}$ ⇀⦇ dCert ,CERT⦈ $\begin{pmatrix} \,\href{Ledger.Conway.Conformance.Certs.html#3536}{\htmlId{6511}{\htmlClass{Generalizable}{\text{stᵈ}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3580}{\htmlId{6517}{\htmlClass{Generalizable}{\text{stᵖ'}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3556}{\htmlId{6524}{\htmlClass{Generalizable}{\text{stᵍ}}}}\, \end{pmatrix}$

  CERT-vdel :
    ∙ Γ ⊢ stᵍ ⇀⦇ dCert ,GOVCERT⦈ stᵍ'
      ────────────────────────────────
      Γ ⊢ $\begin{pmatrix} \,\href{Ledger.Conway.Conformance.Certs.html#3536}{\htmlId{6634}{\htmlClass{Generalizable}{\text{stᵈ}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3576}{\htmlId{6640}{\htmlClass{Generalizable}{\text{stᵖ}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3556}{\htmlId{6646}{\htmlClass{Generalizable}{\text{stᵍ}}}}\, \end{pmatrix}$ ⇀⦇ dCert ,CERT⦈ $\begin{pmatrix} \,\href{Ledger.Conway.Conformance.Certs.html#3536}{\htmlId{6670}{\htmlClass{Generalizable}{\text{stᵈ}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3576}{\htmlId{6676}{\htmlClass{Generalizable}{\text{stᵖ}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3560}{\htmlId{6682}{\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#3324}{\htmlId{7164}{\htmlClass{Generalizable}{\text{e}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3476}{\htmlId{7168}{\htmlClass{Generalizable}{\text{pp}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3349}{\htmlId{7173}{\htmlClass{Generalizable}{\text{vs}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3026}{\htmlId{7178}{\htmlClass{Generalizable}{\text{wdrls}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3250}{\htmlId{7186}{\htmlClass{Generalizable}{\text{cc}}}}\, \end{pmatrix}$ ⊢ $\begin{pmatrix} \begin{pmatrix} \,\href{Ledger.Conway.Conformance.Certs.html#2920}{\htmlId{7197}{\htmlClass{Generalizable}{\text{voteDelegs}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#2815}{\htmlId{7210}{\htmlClass{Generalizable}{\text{stakeDelegs}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#2731}{\htmlId{7224}{\htmlClass{Generalizable}{\text{rewards}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3300}{\htmlId{7234}{\htmlClass{Generalizable}{\text{ddep}}}}\, \end{pmatrix} \\ \,\href{Ledger.Conway.Conformance.Certs.html#3576}{\htmlId{7243}{\htmlClass{Generalizable}{\text{stᵖ}}}}\, \\ \begin{pmatrix} \,\href{Ledger.Conway.Conformance.Certs.html#2761}{\htmlId{7251}{\htmlClass{Generalizable}{\text{dReps}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#2862}{\htmlId{7259}{\htmlClass{Generalizable}{\text{ccHotKeys}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3305}{\htmlId{7271}{\htmlClass{Generalizable}{\text{gdep}}}}\, \end{pmatrix} \end{pmatrix}$
      ⇀⦇ _ ,PRE-CERT⦈
      $\begin{pmatrix} \begin{pmatrix} \,\href{Ledger.Conway.Conformance.Certs.html#2920}{\htmlId{7312}{\htmlClass{Generalizable}{\text{voteDelegs}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#2815}{\htmlId{7325}{\htmlClass{Generalizable}{\text{stakeDelegs}}}}\, \\ \,\href{Axiom.Set.Map.html#11986}{\htmlId{7339}{\htmlClass{Function}{\text{constMap}}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#6972}{\htmlId{7348}{\htmlClass{Bound}{\text{wdrlCreds}}}}\, \,\htmlId{7358}{\htmlClass{Number}{\text{0}}}\, \,\href{Axiom.Set.Map.html#7638}{\htmlId{7360}{\htmlClass{Function Operator}{\text{∪ˡ}}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#2731}{\htmlId{7363}{\htmlClass{Generalizable}{\text{rewards}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3300}{\htmlId{7373}{\htmlClass{Generalizable}{\text{ddep}}}}\, \end{pmatrix} \\ \,\href{Ledger.Conway.Conformance.Certs.html#3576}{\htmlId{7382}{\htmlClass{Generalizable}{\text{stᵖ}}}}\, \\ \begin{pmatrix} \,\href{Ledger.Conway.Conformance.Certs.html#6886}{\htmlId{7390}{\htmlClass{Bound}{\text{refreshedDReps}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#2862}{\htmlId{7407}{\htmlClass{Generalizable}{\text{ccHotKeys}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3305}{\htmlId{7419}{\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#3324}{\htmlId{7527}{\htmlClass{Generalizable}{\text{e}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3476}{\htmlId{7531}{\htmlClass{Generalizable}{\text{pp}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3349}{\htmlId{7536}{\htmlClass{Generalizable}{\text{vs}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3026}{\htmlId{7541}{\htmlClass{Generalizable}{\text{wdrls}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3250}{\htmlId{7549}{\htmlClass{Generalizable}{\text{cc}}}}\, \end{pmatrix}$
      ⊢ $\begin{pmatrix} \begin{pmatrix} \,\href{Ledger.Conway.Conformance.Certs.html#2920}{\htmlId{7566}{\htmlClass{Generalizable}{\text{voteDelegs}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#2815}{\htmlId{7579}{\htmlClass{Generalizable}{\text{stakeDelegs}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#2731}{\htmlId{7593}{\htmlClass{Generalizable}{\text{rewards}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3300}{\htmlId{7603}{\htmlClass{Generalizable}{\text{ddep}}}}\, \end{pmatrix} \\ \,\href{Ledger.Conway.Conformance.Certs.html#3576}{\htmlId{7612}{\htmlClass{Generalizable}{\text{stᵖ}}}}\, \\ \,\href{Ledger.Conway.Conformance.Certs.html#3556}{\htmlId{7618}{\htmlClass{Generalizable}{\text{stᵍ}}}}\, \end{pmatrix}$
        ⇀⦇ _ ,POST-CERT⦈
        $\begin{pmatrix} \begin{pmatrix} \,\href{Ledger.Conway.Conformance.Certs.html#2920}{\htmlId{7661}{\htmlClass{Generalizable}{\text{voteDelegs}}}}\, \,\href{Axiom.Set.Map.html#17773}{\htmlId{7672}{\htmlClass{Function Operator}{\text{∣\^{}}}}}\, \,\htmlId{7675}{\htmlClass{Symbol}{\text{(}}}\,\,\href{abstract-set-theory.FiniteSetTheory.html#519}{\htmlId{7676}{\htmlClass{Function}{\text{mapˢ}}}}\, \,\href{Ledger.Conway.Specification.Gov.Actions.html#2591}{\htmlId{7681}{\htmlClass{InductiveConstructor}{\text{vDelegCredential}}}}\, \,\htmlId{7698}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Class.IsSet.html#916}{\htmlId{7699}{\htmlClass{Function}{\text{dom}}}}\, \,\htmlId{7703}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Conway.Conformance.Certs.html#843}{\htmlId{7704}{\htmlClass{Field}{\text{GState.dreps}}}}\, \,\href{Ledger.Conway.Conformance.Certs.html#3556}{\htmlId{7717}{\htmlClass{Generalizable}{\text{stᵍ}}}}\,\,\htmlId{7720}{\htmlClass{Symbol}{\text{))}}}\, \,\href{Axiom.Set.html#9137}{\htmlId{7723}{\htmlClass{Function Operator}{\text{∪}}}}\, \,\href{Axiom.Set.html#5903}{\htmlId{7725}{\htmlClass{Function}{\text{fromList}}}}\, \,\htmlId{7734}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Conway.Specification.Gov.Actions.html#2664}{\htmlId{7735}{\htmlClass{InductiveConstructor}{\text{vDelegNoConfidence}}}}\, \,\href{Agda.Builtin.List.html#199}{\htmlId{7754}{\htmlClass{InductiveConstructor Operator}{\text{∷}}}}\, \,\href{Ledger.Conway.Specification.Gov.Actions.html#2634}{\htmlId{7756}{\htmlClass{InductiveConstructor}{\text{vDelegAbstain}}}}\, \,\href{Agda.Builtin.List.html#199}{\htmlId{7770}{\htmlClass{InductiveConstructor Operator}{\text{∷}}}}\, \,\href{Agda.Builtin.List.html#184}{\htmlId{7772}{\htmlClass{InductiveConstructor}{\text{[]}}}}\,\,\htmlId{7774}{\htmlClass{Symbol}{\text{))}}}\,
          , \,\href{Ledger.Conway.Conformance.Certs.html#2815}{\htmlId{7789}{\htmlClass{Generalizable}{\text{stakeDelegs}}}}\, , \,\href{Ledger.Conway.Conformance.Certs.html#2731}{\htmlId{7803}{\htmlClass{Generalizable}{\text{rewards}}}}\, , \,\href{Ledger.Conway.Conformance.Certs.html#3300}{\htmlId{7813}{\htmlClass{Generalizable}{\text{ddep}}}}\, \end{pmatrix} , \,\href{Ledger.Conway.Conformance.Certs.html#3576}{\htmlId{7822}{\htmlClass{Generalizable}{\text{stᵖ}}}}\, , \,\href{Ledger.Conway.Conformance.Certs.html#3556}{\htmlId{7828}{\htmlClass{Generalizable}{\text{stᵍ}}}}\, \end{pmatrix}$

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