Ledger.Conway.Specification.Certs

{-# OPTIONS --safe #-}

open import Ledger.Prelude renaming (filterˢ to filter)
open import Ledger.Conway.Specification.Gov.Base
open import Ledger.Prelude.Numeric.UnitInterval

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

open import Ledger.Conway.Specification.Gov.Actions gs
open RwdAddr
open PParams


record StakePoolParams : Type where
  field
    owners          : ℙ KeyHash
    cost            : Coin
    margin          : UnitInterval
    pledge          : Coin
    rewardAccount   : Credential


data DepositPurpose : Type where
  CredentialDeposit  : Credential   → DepositPurpose
  PoolDeposit        : KeyHash      → DepositPurpose
  DRepDeposit        : Credential   → DepositPurpose
  GovActionDeposit   : GovActionID  → DepositPurpose

Deposits : Type
Deposits = DepositPurpose ⇀ Coin


record HasDeposits {a} (A : Type a) : Type a where
  field DepositsOf : A → Deposits
open HasDeposits ⦃...⦄ public

instance
  unquoteDecl DecEq-DepositPurpose = derive-DecEq
    ((quote DepositPurpose , DecEq-DepositPurpose) ∷ [])


CCHotKeys DReps PoolEnv Pools Retiring Rewards StakeDelegs : Type
CCHotKeys    = Credential ⇀ Maybe Credential
DReps        = Credential ⇀ Epoch
PoolEnv      = PParams
Pools        = KeyHash ⇀ StakePoolParams
Retiring     = KeyHash ⇀ Epoch
Rewards      = Credential ⇀ Coin
StakeDelegs  = Credential ⇀ KeyHash


record HasCCHotKeys {a} (A : Type a) : Type a where
  field CCHotKeysOf : A → CCHotKeys

record HasDReps {a} (A : Type a) : Type a where
  field DRepsOf : A → DReps

record HasPools {a} (A : Type a) : Type a where
  field PoolsOf : A → Pools

record HasRetiring {a} (A : Type a) : Type a where
  field RetiringOf : A → Retiring

record HasRewards {a} (A : Type a) : Type a where
  field RewardsOf : A → Rewards

record HasStakeDelegs {a} (A : Type a) : Type a where
  field StakeDelegsOf : A -> StakeDelegs

open HasCCHotKeys ⦃...⦄ public
open HasDReps ⦃...⦄ public
open HasPools ⦃...⦄ public
open HasRetiring ⦃...⦄ public
open HasRewards ⦃...⦄ public
open HasStakeDelegs ⦃...⦄ public


data DCert : Type where
  delegate    : Credential → Maybe VDeleg → Maybe KeyHash → Coin → DCert
  dereg       : Credential → Maybe Coin → DCert
  regpool     : KeyHash → StakePoolParams → DCert
  retirepool  : KeyHash → Epoch → DCert
  regdrep     : Credential → Coin → Anchor → DCert
  deregdrep   : Credential → Coin → DCert
  ccreghot    : Credential → Maybe Credential → DCert


  -- The `reg` cert is deprecated in Conway, but it's still present in this era
  -- for backwards compatibility. This has been added to the spec to make
  -- conformance testing work properly. We don't talk about this certificate
  -- in the pdf because it has been deprecated and we want to discourage people
  -- from using it.
  reg         : Credential → Coin → DCert


cwitness : DCert → Maybe Credential
cwitness (delegate c _ _ _)  = just c
cwitness (dereg c _)         = just c
cwitness (regpool kh _)      = just $ KeyHashObj kh
cwitness (retirepool kh _)   = just $ KeyHashObj kh
cwitness (regdrep c _ _)     = just c
cwitness (deregdrep c _)     = just c
cwitness (ccreghot c _)      = just c


-- The implementation requires the `reg` cert to be witnessed only if the
-- deposit is set. There didn't use to be a field for the deposit, but that was
-- added in the Conway era to make it easier to determine, just by looking at
-- the transaction, how much deposit was paid for that certificate.
cwitness (reg _ zero)        = nothing
cwitness (reg c (suc _))     = just c


record CertEnv : Type where
  field
    epoch     : Epoch
    pp        : PParams
    votes     : List GovVote
    wdrls     : Withdrawals
    coldCreds : ℙ Credential

record DState : Type where


  constructor ⟦_,_,_⟧ᵈ


  field
    voteDelegs   : VoteDelegs
    stakeDelegs  : StakeDelegs
    rewards      : Rewards

record PState : Type where
  field
    pools     : Pools
    retiring  : KeyHash ⇀ Epoch

record GState : Type where


  constructor ⟦_,_⟧ᵛ


  field
    dreps      : DReps
    ccHotKeys  : Credential ⇀ Maybe Credential

record CertState : Type where


  constructor ⟦_,_,_⟧ᶜˢ


  field
    dState : DState
    pState : PState
    gState : GState

record DelegEnv : Type where
  field
    pparams       : PParams
    pools         : Pools
    delegatees    : ℙ Credential


record HasDState {a} (A : Type a) : Type a where
  field DStateOf : A → DState
open HasDState ⦃...⦄ public

record HasPState {a} (A : Type a) : Type a where
  field PStateOf : A → PState
open HasPState ⦃...⦄ public

record HasGState {a} (A : Type a) : Type a where
  field GStateOf : A → GState
open HasGState ⦃...⦄ public

record HasCertState {a} (A : Type a) : Type a where
  field CertStateOf : A → CertState
open HasCertState ⦃...⦄ public

instance
  HasPParams-CertEnv : HasPParams CertEnv
  HasPParams-CertEnv .PParamsOf = CertEnv.pp

  HasWithdrawals-CertEnv : HasWithdrawals CertEnv
  HasWithdrawals-CertEnv .WithdrawalsOf = CertEnv.wdrls

  HasVoteDelegs-DState : HasVoteDelegs DState
  HasVoteDelegs-DState .VoteDelegsOf = DState.voteDelegs

  HasStakeDelegs-DState : HasStakeDelegs DState
  HasStakeDelegs-DState .StakeDelegsOf = DState.stakeDelegs

  HasRewards-DState : HasRewards DState
  HasRewards-DState .RewardsOf = DState.rewards

  HasPools-PState : HasPools PState
  HasPools-PState .PoolsOf = PState.pools

  HasRetiring-PState : HasRetiring PState
  HasRetiring-PState .RetiringOf = PState.retiring

  HasDReps-GState : HasDReps GState
  HasDReps-GState .DRepsOf = GState.dreps

  HasCCHotKeys-GState : HasCCHotKeys GState
  HasCCHotKeys-GState .CCHotKeysOf = GState.ccHotKeys

  HasDState-CertState : HasDState CertState
  HasDState-CertState .DStateOf = CertState.dState

  HasPState-CertState : HasPState CertState
  HasPState-CertState .PStateOf = CertState.pState

  HasGState-CertState : HasGState CertState
  HasGState-CertState .GStateOf = CertState.gState

  HasRewards-CertState : HasRewards CertState
  HasRewards-CertState .RewardsOf = RewardsOf ∘ DStateOf

  HasDReps-CertState : HasDReps CertState
  HasDReps-CertState .DRepsOf = DRepsOf ∘ GStateOf

  HasPools-CertState : HasPools CertState
  HasPools-CertState .PoolsOf = PoolsOf ∘ PStateOf

  HasVoteDelegs-CertState : HasVoteDelegs CertState
  HasVoteDelegs-CertState .VoteDelegsOf = VoteDelegsOf ∘ DStateOf

rewardsBalance : DState → Coin
rewardsBalance ds = ∑[ x ← RewardsOf ds ] x

instance
  HasCoin-CertState : HasCoin CertState
  HasCoin-CertState .getCoin = rewardsBalance ∘ DStateOf

  unquoteDecl HasCast-CertEnv HasCast-DState HasCast-PState HasCast-GState HasCast-CertState HasCast-DelegEnv = derive-HasCast
    (   (quote CertEnv , HasCast-CertEnv)
    ∷   (quote DState , HasCast-DState)
    ∷   (quote PState , HasCast-PState)
    ∷   (quote GState , HasCast-GState)
    ∷   (quote CertState , HasCast-CertState)
    ∷ [ (quote DelegEnv , HasCast-DelegEnv) ])

private variable
  rwds rewards           : Rewards
  dReps                  : DReps
  sDelegs stakeDelegs    : StakeDelegs
  ccKeys ccHotKeys       : CCHotKeys
  vDelegs voteDelegs     : VoteDelegs
  pools                  : Pools
  retiring               : Retiring
  wdrls                  : Withdrawals

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

  stᵈ stᵈ' : DState
  stᵍ stᵍ' : GState
  stᵖ stᵖ' : PState
  cc : ℙ Credential


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

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

data _⊢_⇀⦇_,GOVCERT⦈_   : CertEnv   → GState     → DCert  → GState     → Type

data _⊢_⇀⦇_,CERT⦈_      : CertEnv   → CertState  → DCert  → CertState  → Type

data _⊢_⇀⦇_,CERTBASE⦈_  : CertEnv   → CertState  → ⊤      → CertState  → Type

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


data _⊢_⇀⦇_,DELEG⦈_ -- : DelegEnv → DState → DCert → DState → Type
  where

  DELEG-delegate :
    let Γ = $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Certs.html#7555}{\htmlId{8362}{\htmlClass{Generalizable}{\text{pp}}}}\, \\ \,\href{Ledger.Conway.Specification.Certs.html#7103}{\htmlId{8367}{\htmlClass{Generalizable}{\text{pools}}}}\, \\ \,\href{Ledger.Conway.Specification.Certs.html#7367}{\htmlId{8375}{\htmlClass{Generalizable}{\text{delegatees}}}}\, \end{pmatrix}$
    in
    ∙ (c ∉ dom rwds → d ≡ pp .keyDeposit)
    ∙ (c ∈ dom rwds → d ≡ 0)
    ∙ mv ∈ mapˢ (just ∘ credVoter DRep) delegatees ∪
        fromList ( nothing ∷ just abstainRep ∷ just noConfidenceRep ∷ [] )
    ∙ mkh ∈ mapˢ just (dom pools) ∪ ❴ nothing ❵
      ────────────────────────────────
      Γ ⊢ $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Certs.html#7065}{\htmlId{8693}{\htmlClass{Generalizable}{\text{vDelegs}}}}\, \\ \,\href{Ledger.Conway.Specification.Certs.html#6989}{\htmlId{8703}{\htmlClass{Generalizable}{\text{sDelegs}}}}\, \\ \,\href{Ledger.Conway.Specification.Certs.html#6921}{\htmlId{8713}{\htmlClass{Generalizable}{\text{rwds}}}}\, \end{pmatrix}$ ⇀⦇ delegate c mv mkh d ,DELEG⦈ $\begin{pmatrix} \,\href{Axiom.Set.Map.html#7168}{\htmlId{8753}{\htmlClass{Function}{\text{insertIfJust}}}}\, \,\href{Ledger.Conway.Specification.Certs.html#7307}{\htmlId{8766}{\htmlClass{Generalizable}{\text{c}}}}\, \,\href{Ledger.Conway.Specification.Certs.html#7579}{\htmlId{8768}{\htmlClass{Generalizable}{\text{mv}}}}\, \,\href{Ledger.Conway.Specification.Certs.html#7065}{\htmlId{8771}{\htmlClass{Generalizable}{\text{vDelegs}}}}\, \\ \,\href{Axiom.Set.Map.html#7168}{\htmlId{8781}{\htmlClass{Function}{\text{insertIfJust}}}}\, \,\href{Ledger.Conway.Specification.Certs.html#7307}{\htmlId{8794}{\htmlClass{Generalizable}{\text{c}}}}\, \,\href{Ledger.Conway.Specification.Certs.html#7493}{\htmlId{8796}{\htmlClass{Generalizable}{\text{mkh}}}}\, \,\href{Ledger.Conway.Specification.Certs.html#6989}{\htmlId{8800}{\htmlClass{Generalizable}{\text{sDelegs}}}}\, \\ \,\href{Ledger.Conway.Specification.Certs.html#6921}{\htmlId{8810}{\htmlClass{Generalizable}{\text{rwds}}}}\, \,\href{Axiom.Set.Map.html#6320}{\htmlId{8815}{\htmlClass{Function Operator}{\text{∪ˡ}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{8818}{\htmlClass{Field Operator}{\text{❴}}}}\, \,\href{Ledger.Conway.Specification.Certs.html#7307}{\htmlId{8820}{\htmlClass{Generalizable}{\text{c}}}}\, , \,\htmlId{8824}{\htmlClass{Number}{\text{0}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{8826}{\htmlClass{Field Operator}{\text{❵}}}}\, \end{pmatrix}$

  DELEG-dereg :
    ∙ (c , 0) ∈ rwds
      ────────────────────────────────
      $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Certs.html#7555}{\htmlId{8915}{\htmlClass{Generalizable}{\text{pp}}}}\, \\ \,\href{Ledger.Conway.Specification.Certs.html#7103}{\htmlId{8920}{\htmlClass{Generalizable}{\text{pools}}}}\, \\ \,\href{Ledger.Conway.Specification.Certs.html#7367}{\htmlId{8928}{\htmlClass{Generalizable}{\text{delegatees}}}}\, \end{pmatrix}$ ⊢ $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Certs.html#7065}{\htmlId{8945}{\htmlClass{Generalizable}{\text{vDelegs}}}}\, \\ \,\href{Ledger.Conway.Specification.Certs.html#6989}{\htmlId{8955}{\htmlClass{Generalizable}{\text{sDelegs}}}}\, \\ \,\href{Ledger.Conway.Specification.Certs.html#6921}{\htmlId{8965}{\htmlClass{Generalizable}{\text{rwds}}}}\, \end{pmatrix}$ ⇀⦇ dereg c md ,DELEG⦈ $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Certs.html#7065}{\htmlId{8996}{\htmlClass{Generalizable}{\text{vDelegs}}}}\, \,\href{Axiom.Set.Map.html#10748}{\htmlId{9004}{\htmlClass{Function Operator}{\text{∣}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{9006}{\htmlClass{Field Operator}{\text{❴}}}}\, \,\href{Ledger.Conway.Specification.Certs.html#7307}{\htmlId{9008}{\htmlClass{Generalizable}{\text{c}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{9010}{\htmlClass{Field Operator}{\text{❵}}}}\, \,\href{Axiom.Set.Map.html#10748}{\htmlId{9012}{\htmlClass{Function Operator}{\text{ᶜ}}}}\, \\ \,\href{Ledger.Conway.Specification.Certs.html#6989}{\htmlId{9016}{\htmlClass{Generalizable}{\text{sDelegs}}}}\, \,\href{Axiom.Set.Map.html#10748}{\htmlId{9024}{\htmlClass{Function Operator}{\text{∣}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{9026}{\htmlClass{Field Operator}{\text{❴}}}}\, \,\href{Ledger.Conway.Specification.Certs.html#7307}{\htmlId{9028}{\htmlClass{Generalizable}{\text{c}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{9030}{\htmlClass{Field Operator}{\text{❵}}}}\, \,\href{Axiom.Set.Map.html#10748}{\htmlId{9032}{\htmlClass{Function Operator}{\text{ᶜ}}}}\, \\ \,\href{Ledger.Conway.Specification.Certs.html#6921}{\htmlId{9036}{\htmlClass{Generalizable}{\text{rwds}}}}\, \,\href{Axiom.Set.Map.html#10748}{\htmlId{9041}{\htmlClass{Function Operator}{\text{∣}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{9043}{\htmlClass{Field Operator}{\text{❴}}}}\, \,\href{Ledger.Conway.Specification.Certs.html#7307}{\htmlId{9045}{\htmlClass{Generalizable}{\text{c}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{9047}{\htmlClass{Field Operator}{\text{❵}}}}\, \,\href{Axiom.Set.Map.html#10748}{\htmlId{9049}{\htmlClass{Function Operator}{\text{ᶜ}}}}\, \end{pmatrix}$

  DELEG-reg :
    ∙ c ∉ dom rwds
    ∙ d ≡ pp .keyDeposit ⊎ d ≡ 0
      ────────────────────────────────
      $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Certs.html#7555}{\htmlId{9167}{\htmlClass{Generalizable}{\text{pp}}}}\, \\ \,\href{Ledger.Conway.Specification.Certs.html#7103}{\htmlId{9172}{\htmlClass{Generalizable}{\text{pools}}}}\, \\ \,\href{Ledger.Conway.Specification.Certs.html#7367}{\htmlId{9180}{\htmlClass{Generalizable}{\text{delegatees}}}}\, \end{pmatrix}$ ⊢ $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Certs.html#7065}{\htmlId{9197}{\htmlClass{Generalizable}{\text{vDelegs}}}}\, \\ \,\href{Ledger.Conway.Specification.Certs.html#6989}{\htmlId{9207}{\htmlClass{Generalizable}{\text{sDelegs}}}}\, \\ \,\href{Ledger.Conway.Specification.Certs.html#6921}{\htmlId{9217}{\htmlClass{Generalizable}{\text{rwds}}}}\, \end{pmatrix}$ ⇀⦇ reg c d ,DELEG⦈ $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Certs.html#7065}{\htmlId{9245}{\htmlClass{Generalizable}{\text{vDelegs}}}}\, \\ \,\href{Ledger.Conway.Specification.Certs.html#6989}{\htmlId{9255}{\htmlClass{Generalizable}{\text{sDelegs}}}}\, \\ \,\href{Ledger.Conway.Specification.Certs.html#6921}{\htmlId{9265}{\htmlClass{Generalizable}{\text{rwds}}}}\, \,\href{Axiom.Set.Map.html#6320}{\htmlId{9270}{\htmlClass{Function Operator}{\text{∪ˡ}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{9273}{\htmlClass{Field Operator}{\text{❴}}}}\, \,\href{Ledger.Conway.Specification.Certs.html#7307}{\htmlId{9275}{\htmlClass{Generalizable}{\text{c}}}}\, , \,\htmlId{9279}{\htmlClass{Number}{\text{0}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{9281}{\htmlClass{Field Operator}{\text{❵}}}}\, \end{pmatrix}$



data _⊢_⇀⦇_,POOL⦈_ -- : PoolEnv → PState → DCert → PState → Type
  where

  POOL-regpool :
    ∙ kh ∉ dom pools
      ────────────────────────────────
      pp ⊢ $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Certs.html#7103}{\htmlId{9452}{\htmlClass{Generalizable}{\text{pools}}}}\, \\ \,\href{Ledger.Conway.Specification.Certs.html#7136}{\htmlId{9460}{\htmlClass{Generalizable}{\text{retiring}}}}\, \end{pmatrix}$ ⇀⦇ regpool kh poolParams ,POOL⦈ $\begin{pmatrix} \,\href{Class.HasSingleton.html#288}{\htmlId{9505}{\htmlClass{Field Operator}{\text{❴}}}}\, \,\href{Ledger.Conway.Specification.Certs.html#7469}{\htmlId{9507}{\htmlClass{Generalizable}{\text{kh}}}}\, , \,\href{Ledger.Conway.Specification.Certs.html#7523}{\htmlId{9512}{\htmlClass{Generalizable}{\text{poolParams}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{9523}{\htmlClass{Field Operator}{\text{❵}}}}\, \,\href{Axiom.Set.Map.html#6320}{\htmlId{9525}{\htmlClass{Function Operator}{\text{∪ˡ}}}}\, \,\href{Ledger.Conway.Specification.Certs.html#7103}{\htmlId{9528}{\htmlClass{Generalizable}{\text{pools}}}}\, \\ \,\href{Ledger.Conway.Specification.Certs.html#7136}{\htmlId{9536}{\htmlClass{Generalizable}{\text{retiring}}}}\, \end{pmatrix}$

  POOL-retirepool :
    ────────────────────────────────
    pp ⊢ $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Certs.html#7103}{\htmlId{9616}{\htmlClass{Generalizable}{\text{pools}}}}\, \\ \,\href{Ledger.Conway.Specification.Certs.html#7136}{\htmlId{9624}{\htmlClass{Generalizable}{\text{retiring}}}}\, \end{pmatrix}$ ⇀⦇ retirepool kh e ,POOL⦈ $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Certs.html#7103}{\htmlId{9663}{\htmlClass{Generalizable}{\text{pools}}}}\, \\ \,\href{Class.HasSingleton.html#288}{\htmlId{9671}{\htmlClass{Field Operator}{\text{❴}}}}\, \,\href{Ledger.Conway.Specification.Certs.html#7469}{\htmlId{9673}{\htmlClass{Generalizable}{\text{kh}}}}\, , \,\href{Ledger.Conway.Specification.Certs.html#7418}{\htmlId{9678}{\htmlClass{Generalizable}{\text{e}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{9680}{\htmlClass{Field Operator}{\text{❵}}}}\, \,\href{Axiom.Set.Map.html#6320}{\htmlId{9682}{\htmlClass{Function Operator}{\text{∪ˡ}}}}\, \,\href{Ledger.Conway.Specification.Certs.html#7136}{\htmlId{9685}{\htmlClass{Generalizable}{\text{retiring}}}}\, \end{pmatrix}$


data _⊢_⇀⦇_,GOVCERT⦈_ -- : CertEnv → GState → DCert → GState → Type
  where

  GOVCERT-regdrep :
    let Γ = $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Certs.html#7418}{\htmlId{9809}{\htmlClass{Generalizable}{\text{e}}}}\, \\ \,\href{Ledger.Conway.Specification.Certs.html#7555}{\htmlId{9813}{\htmlClass{Generalizable}{\text{pp}}}}\, \\ \,\href{Ledger.Conway.Specification.Certs.html#7440}{\htmlId{9818}{\htmlClass{Generalizable}{\text{vs}}}}\, \\ \,\href{Ledger.Conway.Specification.Certs.html#7172}{\htmlId{9823}{\htmlClass{Generalizable}{\text{wdrls}}}}\, \\ \,\href{Ledger.Conway.Specification.Certs.html#7669}{\htmlId{9831}{\htmlClass{Generalizable}{\text{cc}}}}\, \end{pmatrix}$
    in
    ∙ (d ≡ pp .drepDeposit × c ∉ dom dReps) ⊎ (d ≡ 0 × c ∈ dom dReps)
      ────────────────────────────────
      Γ ⊢ $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Certs.html#6956}{\htmlId{9964}{\htmlClass{Generalizable}{\text{dReps}}}}\, \\ \,\href{Ledger.Conway.Specification.Certs.html#7028}{\htmlId{9972}{\htmlClass{Generalizable}{\text{ccKeys}}}}\, \end{pmatrix}$ ⇀⦇ regdrep c d an ,GOVCERT⦈ $\begin{pmatrix} \,\href{Class.HasSingleton.html#288}{\htmlId{10011}{\htmlClass{Field Operator}{\text{❴}}}}\, \,\href{Ledger.Conway.Specification.Certs.html#7307}{\htmlId{10013}{\htmlClass{Generalizable}{\text{c}}}}\, , \,\href{Ledger.Conway.Specification.Certs.html#7418}{\htmlId{10017}{\htmlClass{Generalizable}{\text{e}}}}\, \,\href{Class.HasAdd.Core.html#162}{\htmlId{10019}{\htmlClass{Field Operator}{\text{+}}}}\, \,\href{Ledger.Conway.Specification.Certs.html#7555}{\htmlId{10021}{\htmlClass{Generalizable}{\text{pp}}}}\, \,\htmlId{10024}{\htmlClass{Symbol}{\text{.}}}\,\,\href{Ledger.Conway.Specification.PParams.html#3442}{\htmlId{10025}{\htmlClass{Field}{\text{drepActivity}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{10038}{\htmlClass{Field Operator}{\text{❵}}}}\, \,\href{Axiom.Set.Map.html#6320}{\htmlId{10040}{\htmlClass{Function Operator}{\text{∪ˡ}}}}\, \,\href{Ledger.Conway.Specification.Certs.html#6956}{\htmlId{10043}{\htmlClass{Generalizable}{\text{dReps}}}}\, \\ \,\href{Ledger.Conway.Specification.Certs.html#7028}{\htmlId{10051}{\htmlClass{Generalizable}{\text{ccKeys}}}}\, \end{pmatrix}$

  GOVCERT-deregdrep :
    ∙ c ∈ dom dReps
      ────────────────────────────────
      $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Certs.html#7418}{\htmlId{10150}{\htmlClass{Generalizable}{\text{e}}}}\, \\ \,\href{Ledger.Conway.Specification.Certs.html#7555}{\htmlId{10154}{\htmlClass{Generalizable}{\text{pp}}}}\, \\ \,\href{Ledger.Conway.Specification.Certs.html#7440}{\htmlId{10159}{\htmlClass{Generalizable}{\text{vs}}}}\, \\ \,\href{Ledger.Conway.Specification.Certs.html#7172}{\htmlId{10164}{\htmlClass{Generalizable}{\text{wdrls}}}}\, \\ \,\href{Ledger.Conway.Specification.Certs.html#7669}{\htmlId{10172}{\htmlClass{Generalizable}{\text{cc}}}}\, \end{pmatrix}$ ⊢ $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Certs.html#6956}{\htmlId{10181}{\htmlClass{Generalizable}{\text{dReps}}}}\, \\ \,\href{Ledger.Conway.Specification.Certs.html#7028}{\htmlId{10189}{\htmlClass{Generalizable}{\text{ccKeys}}}}\, \end{pmatrix}$ ⇀⦇ deregdrep c d ,GOVCERT⦈ $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Certs.html#6956}{\htmlId{10227}{\htmlClass{Generalizable}{\text{dReps}}}}\, \,\href{Axiom.Set.Map.html#10748}{\htmlId{10233}{\htmlClass{Function Operator}{\text{∣}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{10235}{\htmlClass{Field Operator}{\text{❴}}}}\, \,\href{Ledger.Conway.Specification.Certs.html#7307}{\htmlId{10237}{\htmlClass{Generalizable}{\text{c}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{10239}{\htmlClass{Field Operator}{\text{❵}}}}\, \,\href{Axiom.Set.Map.html#10748}{\htmlId{10241}{\htmlClass{Function Operator}{\text{ᶜ}}}}\, \\ \,\href{Ledger.Conway.Specification.Certs.html#7028}{\htmlId{10245}{\htmlClass{Generalizable}{\text{ccKeys}}}}\, \end{pmatrix}$

  GOVCERT-ccreghot :
    ∙ (c , nothing) ∉ ccKeys
    ∙ c ∈ cc
      ────────────────────────────────
      $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Certs.html#7418}{\htmlId{10365}{\htmlClass{Generalizable}{\text{e}}}}\, \\ \,\href{Ledger.Conway.Specification.Certs.html#7555}{\htmlId{10369}{\htmlClass{Generalizable}{\text{pp}}}}\, \\ \,\href{Ledger.Conway.Specification.Certs.html#7440}{\htmlId{10374}{\htmlClass{Generalizable}{\text{vs}}}}\, \\ \,\href{Ledger.Conway.Specification.Certs.html#7172}{\htmlId{10379}{\htmlClass{Generalizable}{\text{wdrls}}}}\, \\ \,\href{Ledger.Conway.Specification.Certs.html#7669}{\htmlId{10387}{\htmlClass{Generalizable}{\text{cc}}}}\, \end{pmatrix}$ ⊢ $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Certs.html#6956}{\htmlId{10396}{\htmlClass{Generalizable}{\text{dReps}}}}\, \\ \,\href{Ledger.Conway.Specification.Certs.html#7028}{\htmlId{10404}{\htmlClass{Generalizable}{\text{ccKeys}}}}\, \end{pmatrix}$ ⇀⦇ ccreghot c mc ,GOVCERT⦈ $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Certs.html#6956}{\htmlId{10442}{\htmlClass{Generalizable}{\text{dReps}}}}\, \\ \,\href{Class.HasSingleton.html#288}{\htmlId{10450}{\htmlClass{Field Operator}{\text{❴}}}}\, \,\href{Ledger.Conway.Specification.Certs.html#7307}{\htmlId{10452}{\htmlClass{Generalizable}{\text{c}}}}\, , \,\href{Ledger.Conway.Specification.Certs.html#7334}{\htmlId{10456}{\htmlClass{Generalizable}{\text{mc}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{10459}{\htmlClass{Field Operator}{\text{❵}}}}\, \,\href{Axiom.Set.Map.html#6320}{\htmlId{10461}{\htmlClass{Function Operator}{\text{∪ˡ}}}}\, \,\href{Ledger.Conway.Specification.Certs.html#7028}{\htmlId{10464}{\htmlClass{Generalizable}{\text{ccKeys}}}}\, \end{pmatrix}$



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

  CERT-deleg :
    ∙ $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Certs.html#7555}{\htmlId{10585}{\htmlClass{Generalizable}{\text{pp}}}}\, \\ \,\href{Ledger.Conway.Specification.Certs.html#3901}{\htmlId{10590}{\htmlClass{Field}{\text{PState.pools}}}}\, \,\href{Ledger.Conway.Specification.Certs.html#7649}{\htmlId{10603}{\htmlClass{Generalizable}{\text{stᵖ}}}}\, \\ \,\href{Class.IsSet.html#916}{\htmlId{10609}{\htmlClass{Function}{\text{dom}}}}\, \,\htmlId{10613}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Conway.Specification.Certs.html#4016}{\htmlId{10614}{\htmlClass{Field}{\text{GState.dreps}}}}\, \,\href{Ledger.Conway.Specification.Certs.html#7629}{\htmlId{10627}{\htmlClass{Generalizable}{\text{stᵍ}}}}\,\,\htmlId{10630}{\htmlClass{Symbol}{\text{)}}}\, \end{pmatrix}$ ⊢ stᵈ ⇀⦇ dCert ,DELEG⦈ stᵈ'
      ────────────────────────────────
      $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Certs.html#7418}{\htmlId{10709}{\htmlClass{Generalizable}{\text{e}}}}\, \\ \,\href{Ledger.Conway.Specification.Certs.html#7555}{\htmlId{10713}{\htmlClass{Generalizable}{\text{pp}}}}\, \\ \,\href{Ledger.Conway.Specification.Certs.html#7440}{\htmlId{10718}{\htmlClass{Generalizable}{\text{vs}}}}\, \\ \,\href{Ledger.Conway.Specification.Certs.html#7172}{\htmlId{10723}{\htmlClass{Generalizable}{\text{wdrls}}}}\, \\ \,\href{Ledger.Conway.Specification.Certs.html#7669}{\htmlId{10731}{\htmlClass{Generalizable}{\text{cc}}}}\, \end{pmatrix}$ ⊢ $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Certs.html#7609}{\htmlId{10740}{\htmlClass{Generalizable}{\text{stᵈ}}}}\, \\ \,\href{Ledger.Conway.Specification.Certs.html#7649}{\htmlId{10746}{\htmlClass{Generalizable}{\text{stᵖ}}}}\, \\ \,\href{Ledger.Conway.Specification.Certs.html#7629}{\htmlId{10752}{\htmlClass{Generalizable}{\text{stᵍ}}}}\, \end{pmatrix}$ ⇀⦇ dCert ,CERT⦈ $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Certs.html#7613}{\htmlId{10776}{\htmlClass{Generalizable}{\text{stᵈ'}}}}\, \\ \,\href{Ledger.Conway.Specification.Certs.html#7649}{\htmlId{10783}{\htmlClass{Generalizable}{\text{stᵖ}}}}\, \\ \,\href{Ledger.Conway.Specification.Certs.html#7629}{\htmlId{10789}{\htmlClass{Generalizable}{\text{stᵍ}}}}\, \end{pmatrix}$

  CERT-pool :
    ∙ pp ⊢ stᵖ ⇀⦇ dCert ,POOL⦈ stᵖ'
      ────────────────────────────────
      $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Certs.html#7418}{\htmlId{10893}{\htmlClass{Generalizable}{\text{e}}}}\, \\ \,\href{Ledger.Conway.Specification.Certs.html#7555}{\htmlId{10897}{\htmlClass{Generalizable}{\text{pp}}}}\, \\ \,\href{Ledger.Conway.Specification.Certs.html#7440}{\htmlId{10902}{\htmlClass{Generalizable}{\text{vs}}}}\, \\ \,\href{Ledger.Conway.Specification.Certs.html#7172}{\htmlId{10907}{\htmlClass{Generalizable}{\text{wdrls}}}}\, \\ \,\href{Ledger.Conway.Specification.Certs.html#7669}{\htmlId{10915}{\htmlClass{Generalizable}{\text{cc}}}}\, \end{pmatrix}$ ⊢ $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Certs.html#7609}{\htmlId{10924}{\htmlClass{Generalizable}{\text{stᵈ}}}}\, \\ \,\href{Ledger.Conway.Specification.Certs.html#7649}{\htmlId{10930}{\htmlClass{Generalizable}{\text{stᵖ}}}}\, \\ \,\href{Ledger.Conway.Specification.Certs.html#7629}{\htmlId{10936}{\htmlClass{Generalizable}{\text{stᵍ}}}}\, \end{pmatrix}$ ⇀⦇ dCert ,CERT⦈ $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Certs.html#7609}{\htmlId{10960}{\htmlClass{Generalizable}{\text{stᵈ}}}}\, \\ \,\href{Ledger.Conway.Specification.Certs.html#7653}{\htmlId{10966}{\htmlClass{Generalizable}{\text{stᵖ'}}}}\, \\ \,\href{Ledger.Conway.Specification.Certs.html#7629}{\htmlId{10973}{\htmlClass{Generalizable}{\text{stᵍ}}}}\, \end{pmatrix}$

  CERT-vdel :
    ∙ Γ ⊢ stᵍ ⇀⦇ dCert ,GOVCERT⦈ stᵍ'
      ────────────────────────────────
      Γ ⊢ $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Certs.html#7609}{\htmlId{11083}{\htmlClass{Generalizable}{\text{stᵈ}}}}\, \\ \,\href{Ledger.Conway.Specification.Certs.html#7649}{\htmlId{11089}{\htmlClass{Generalizable}{\text{stᵖ}}}}\, \\ \,\href{Ledger.Conway.Specification.Certs.html#7629}{\htmlId{11095}{\htmlClass{Generalizable}{\text{stᵍ}}}}\, \end{pmatrix}$ ⇀⦇ dCert ,CERT⦈ $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Certs.html#7609}{\htmlId{11119}{\htmlClass{Generalizable}{\text{stᵈ}}}}\, \\ \,\href{Ledger.Conway.Specification.Certs.html#7649}{\htmlId{11125}{\htmlClass{Generalizable}{\text{stᵖ}}}}\, \\ \,\href{Ledger.Conway.Specification.Certs.html#7633}{\htmlId{11131}{\htmlClass{Generalizable}{\text{stᵍ'}}}}\, \end{pmatrix}$


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

  CERT-base :
    let refresh          = mapPartial getDRepVote (fromList vs)
        refreshedDReps   = mapValueRestricted (const (e + pp .drepActivity)) dReps refresh
        wdrlCreds        = mapˢ stake (dom wdrls)
        validVoteDelegs  = voteDelegs ∣^ (  mapˢ (credVoter DRep) (dom dReps)
                                            ∪ fromList (noConfidenceRep ∷ abstainRep ∷ [])
                                         )
    in
    ∙ filter isKeyHash wdrlCreds ⊆ dom voteDelegs
    ∙ mapˢ (map₁ stake) (wdrls ˢ) ⊆ rewards ˢ
      ────────────────────────────────
      $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Certs.html#7418}{\htmlId{11812}{\htmlClass{Generalizable}{\text{e}}}}\, \\ \,\href{Ledger.Conway.Specification.Certs.html#7555}{\htmlId{11816}{\htmlClass{Generalizable}{\text{pp}}}}\, \\ \,\href{Ledger.Conway.Specification.Certs.html#7440}{\htmlId{11821}{\htmlClass{Generalizable}{\text{vs}}}}\, \\ \,\href{Ledger.Conway.Specification.Certs.html#7172}{\htmlId{11826}{\htmlClass{Generalizable}{\text{wdrls}}}}\, \\ \,\href{Ledger.Conway.Specification.Certs.html#7669}{\htmlId{11834}{\htmlClass{Generalizable}{\text{cc}}}}\, \end{pmatrix}$ ⊢ $\begin{pmatrix} \begin{pmatrix} \,\href{Ledger.Conway.Specification.Certs.html#7073}{\htmlId{11845}{\htmlClass{Generalizable}{\text{voteDelegs}}}}\, \\ \,\href{Ledger.Conway.Specification.Certs.html#6997}{\htmlId{11858}{\htmlClass{Generalizable}{\text{stakeDelegs}}}}\, \\ \,\href{Ledger.Conway.Specification.Certs.html#6926}{\htmlId{11872}{\htmlClass{Generalizable}{\text{rewards}}}}\, \end{pmatrix} \\ \,\href{Ledger.Conway.Specification.Certs.html#7649}{\htmlId{11884}{\htmlClass{Generalizable}{\text{stᵖ}}}}\, \\ \begin{pmatrix} \,\href{Ledger.Conway.Specification.Certs.html#6956}{\htmlId{11892}{\htmlClass{Generalizable}{\text{dReps}}}}\, \\ \,\href{Ledger.Conway.Specification.Certs.html#7035}{\htmlId{11900}{\htmlClass{Generalizable}{\text{ccHotKeys}}}}\, \end{pmatrix} \end{pmatrix}$ ⇀⦇ _ ,CERTBASE⦈ $\begin{pmatrix} \begin{pmatrix} \,\href{Ledger.Conway.Specification.Certs.html#11458}{\htmlId{11934}{\htmlClass{Bound}{\text{validVoteDelegs}}}}\, \\ \,\href{Ledger.Conway.Specification.Certs.html#6997}{\htmlId{11952}{\htmlClass{Generalizable}{\text{stakeDelegs}}}}\, \\ \,\href{Axiom.Set.Map.html#9130}{\htmlId{11966}{\htmlClass{Function}{\text{constMap}}}}\, \,\href{Ledger.Conway.Specification.Certs.html#11408}{\htmlId{11975}{\htmlClass{Bound}{\text{wdrlCreds}}}}\, \,\htmlId{11985}{\htmlClass{Number}{\text{0}}}\, \,\href{Axiom.Set.Map.html#6320}{\htmlId{11987}{\htmlClass{Function Operator}{\text{∪ˡ}}}}\, \,\href{Ledger.Conway.Specification.Certs.html#6926}{\htmlId{11990}{\htmlClass{Generalizable}{\text{rewards}}}}\, \end{pmatrix} \\ \,\href{Ledger.Conway.Specification.Certs.html#7649}{\htmlId{12002}{\htmlClass{Generalizable}{\text{stᵖ}}}}\, \\ \begin{pmatrix} \,\href{Ledger.Conway.Specification.Certs.html#11317}{\htmlId{12010}{\htmlClass{Bound}{\text{refreshedDReps}}}}\, \\ \,\href{Ledger.Conway.Specification.Certs.html#7035}{\htmlId{12027}{\htmlClass{Generalizable}{\text{ccHotKeys}}}}\, \end{pmatrix} \end{pmatrix}$