{-# 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 Stake StakeDelegs : Type
CCHotKeys    = Credential  Maybe Credential
DReps        = Credential  Epoch
PoolEnv      = PParams
Pools        = KeyHash  StakePoolParams
Retiring     = KeyHash  Epoch
Rewards      = Credential  Coin
Stake        = 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 HasStake {a} (A : Type a) : Type a where
  field StakeOf : A -> Stake

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 HasStake ⦃...⦄ 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

  HasCCHotKeys-CertState : HasCCHotKeys CertState
  HasCCHotKeys-CertState .CCHotKeysOf = CCHotKeysOf  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
  mvd         : 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#7813}{\htmlId{8620}{\htmlClass{Generalizable}{\text{pp}}}}\, \\ \,\href{Ledger.Conway.Specification.Certs.html#7361}{\htmlId{8625}{\htmlClass{Generalizable}{\text{pools}}}}\, \\ \,\href{Ledger.Conway.Specification.Certs.html#7625}{\htmlId{8633}{\htmlClass{Generalizable}{\text{delegatees}}}}\, \end{pmatrix}$
    in
     (c  dom rwds  d  pp .keyDeposit)
     (c  dom rwds  d  0)
     mvd  mapˢ (just  vDelegCredential) delegatees 
            fromList ( nothing  just vDelegAbstain  just vDelegNoConfidence  [] )
     mkh  mapˢ just (dom pools)   nothing 
      ────────────────────────────────
      Γ  $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Certs.html#7323}{\htmlId{8964}{\htmlClass{Generalizable}{\text{vDelegs}}}}\, \\ \,\href{Ledger.Conway.Specification.Certs.html#7247}{\htmlId{8974}{\htmlClass{Generalizable}{\text{sDelegs}}}}\, \\ \,\href{Ledger.Conway.Specification.Certs.html#7179}{\htmlId{8984}{\htmlClass{Generalizable}{\text{rwds}}}}\, \end{pmatrix}$ ⇀⦇ delegate c mvd mkh d ,DELEG⦈ $\begin{pmatrix} \,\href{Axiom.Set.Map.html#7168}{\htmlId{9025}{\htmlClass{Function}{\text{insertIfJust}}}}\, \,\href{Ledger.Conway.Specification.Certs.html#7565}{\htmlId{9038}{\htmlClass{Generalizable}{\text{c}}}}\, \,\href{Ledger.Conway.Specification.Certs.html#7837}{\htmlId{9040}{\htmlClass{Generalizable}{\text{mvd}}}}\, \,\href{Ledger.Conway.Specification.Certs.html#7323}{\htmlId{9044}{\htmlClass{Generalizable}{\text{vDelegs}}}}\, \\ \,\href{Axiom.Set.Map.html#7168}{\htmlId{9054}{\htmlClass{Function}{\text{insertIfJust}}}}\, \,\href{Ledger.Conway.Specification.Certs.html#7565}{\htmlId{9067}{\htmlClass{Generalizable}{\text{c}}}}\, \,\href{Ledger.Conway.Specification.Certs.html#7751}{\htmlId{9069}{\htmlClass{Generalizable}{\text{mkh}}}}\, \,\href{Ledger.Conway.Specification.Certs.html#7247}{\htmlId{9073}{\htmlClass{Generalizable}{\text{sDelegs}}}}\, \\ \,\href{Ledger.Conway.Specification.Certs.html#7179}{\htmlId{9083}{\htmlClass{Generalizable}{\text{rwds}}}}\, \,\href{Axiom.Set.Map.html#6320}{\htmlId{9088}{\htmlClass{Function Operator}{\text{∪ˡ}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{9091}{\htmlClass{Field Operator}{\text{❴}}}}\, \,\href{Ledger.Conway.Specification.Certs.html#7565}{\htmlId{9093}{\htmlClass{Generalizable}{\text{c}}}}\, , \,\htmlId{9097}{\htmlClass{Number}{\text{0}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{9099}{\htmlClass{Field Operator}{\text{❵}}}}\, \end{pmatrix}$

  DELEG-dereg :
     (c , 0)  rwds
      ────────────────────────────────
      $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Certs.html#7813}{\htmlId{9188}{\htmlClass{Generalizable}{\text{pp}}}}\, \\ \,\href{Ledger.Conway.Specification.Certs.html#7361}{\htmlId{9193}{\htmlClass{Generalizable}{\text{pools}}}}\, \\ \,\href{Ledger.Conway.Specification.Certs.html#7625}{\htmlId{9201}{\htmlClass{Generalizable}{\text{delegatees}}}}\, \end{pmatrix}$  $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Certs.html#7323}{\htmlId{9218}{\htmlClass{Generalizable}{\text{vDelegs}}}}\, \\ \,\href{Ledger.Conway.Specification.Certs.html#7247}{\htmlId{9228}{\htmlClass{Generalizable}{\text{sDelegs}}}}\, \\ \,\href{Ledger.Conway.Specification.Certs.html#7179}{\htmlId{9238}{\htmlClass{Generalizable}{\text{rwds}}}}\, \end{pmatrix}$ ⇀⦇ dereg c md ,DELEG⦈ $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Certs.html#7323}{\htmlId{9269}{\htmlClass{Generalizable}{\text{vDelegs}}}}\, \,\href{Axiom.Set.Map.html#10748}{\htmlId{9277}{\htmlClass{Function Operator}{\text{∣}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{9279}{\htmlClass{Field Operator}{\text{❴}}}}\, \,\href{Ledger.Conway.Specification.Certs.html#7565}{\htmlId{9281}{\htmlClass{Generalizable}{\text{c}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{9283}{\htmlClass{Field Operator}{\text{❵}}}}\, \,\href{Axiom.Set.Map.html#10748}{\htmlId{9285}{\htmlClass{Function Operator}{\text{ᶜ}}}}\, \\ \,\href{Ledger.Conway.Specification.Certs.html#7247}{\htmlId{9289}{\htmlClass{Generalizable}{\text{sDelegs}}}}\, \,\href{Axiom.Set.Map.html#10748}{\htmlId{9297}{\htmlClass{Function Operator}{\text{∣}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{9299}{\htmlClass{Field Operator}{\text{❴}}}}\, \,\href{Ledger.Conway.Specification.Certs.html#7565}{\htmlId{9301}{\htmlClass{Generalizable}{\text{c}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{9303}{\htmlClass{Field Operator}{\text{❵}}}}\, \,\href{Axiom.Set.Map.html#10748}{\htmlId{9305}{\htmlClass{Function Operator}{\text{ᶜ}}}}\, \\ \,\href{Ledger.Conway.Specification.Certs.html#7179}{\htmlId{9309}{\htmlClass{Generalizable}{\text{rwds}}}}\, \,\href{Axiom.Set.Map.html#10748}{\htmlId{9314}{\htmlClass{Function Operator}{\text{∣}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{9316}{\htmlClass{Field Operator}{\text{❴}}}}\, \,\href{Ledger.Conway.Specification.Certs.html#7565}{\htmlId{9318}{\htmlClass{Generalizable}{\text{c}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{9320}{\htmlClass{Field Operator}{\text{❵}}}}\, \,\href{Axiom.Set.Map.html#10748}{\htmlId{9322}{\htmlClass{Function Operator}{\text{ᶜ}}}}\, \end{pmatrix}$

  DELEG-reg :
     c  dom rwds
     d  pp .keyDeposit  d  0
      ────────────────────────────────
      $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Certs.html#7813}{\htmlId{9440}{\htmlClass{Generalizable}{\text{pp}}}}\, \\ \,\href{Ledger.Conway.Specification.Certs.html#7361}{\htmlId{9445}{\htmlClass{Generalizable}{\text{pools}}}}\, \\ \,\href{Ledger.Conway.Specification.Certs.html#7625}{\htmlId{9453}{\htmlClass{Generalizable}{\text{delegatees}}}}\, \end{pmatrix}$  $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Certs.html#7323}{\htmlId{9470}{\htmlClass{Generalizable}{\text{vDelegs}}}}\, \\ \,\href{Ledger.Conway.Specification.Certs.html#7247}{\htmlId{9480}{\htmlClass{Generalizable}{\text{sDelegs}}}}\, \\ \,\href{Ledger.Conway.Specification.Certs.html#7179}{\htmlId{9490}{\htmlClass{Generalizable}{\text{rwds}}}}\, \end{pmatrix}$ ⇀⦇ reg c d ,DELEG⦈ $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Certs.html#7323}{\htmlId{9518}{\htmlClass{Generalizable}{\text{vDelegs}}}}\, \\ \,\href{Ledger.Conway.Specification.Certs.html#7247}{\htmlId{9528}{\htmlClass{Generalizable}{\text{sDelegs}}}}\, \\ \,\href{Ledger.Conway.Specification.Certs.html#7179}{\htmlId{9538}{\htmlClass{Generalizable}{\text{rwds}}}}\, \,\href{Axiom.Set.Map.html#6320}{\htmlId{9543}{\htmlClass{Function Operator}{\text{∪ˡ}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{9546}{\htmlClass{Field Operator}{\text{❴}}}}\, \,\href{Ledger.Conway.Specification.Certs.html#7565}{\htmlId{9548}{\htmlClass{Generalizable}{\text{c}}}}\, , \,\htmlId{9552}{\htmlClass{Number}{\text{0}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{9554}{\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#7361}{\htmlId{9725}{\htmlClass{Generalizable}{\text{pools}}}}\, \\ \,\href{Ledger.Conway.Specification.Certs.html#7394}{\htmlId{9733}{\htmlClass{Generalizable}{\text{retiring}}}}\, \end{pmatrix}$ ⇀⦇ regpool kh poolParams ,POOL⦈ $\begin{pmatrix} \,\href{Class.HasSingleton.html#288}{\htmlId{9778}{\htmlClass{Field Operator}{\text{❴}}}}\, \,\href{Ledger.Conway.Specification.Certs.html#7727}{\htmlId{9780}{\htmlClass{Generalizable}{\text{kh}}}}\, , \,\href{Ledger.Conway.Specification.Certs.html#7781}{\htmlId{9785}{\htmlClass{Generalizable}{\text{poolParams}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{9796}{\htmlClass{Field Operator}{\text{❵}}}}\, \,\href{Axiom.Set.Map.html#6320}{\htmlId{9798}{\htmlClass{Function Operator}{\text{∪ˡ}}}}\, \,\href{Ledger.Conway.Specification.Certs.html#7361}{\htmlId{9801}{\htmlClass{Generalizable}{\text{pools}}}}\, \\ \,\href{Ledger.Conway.Specification.Certs.html#7394}{\htmlId{9809}{\htmlClass{Generalizable}{\text{retiring}}}}\, \end{pmatrix}$

  POOL-retirepool :
    ────────────────────────────────
    pp  $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Certs.html#7361}{\htmlId{9889}{\htmlClass{Generalizable}{\text{pools}}}}\, \\ \,\href{Ledger.Conway.Specification.Certs.html#7394}{\htmlId{9897}{\htmlClass{Generalizable}{\text{retiring}}}}\, \end{pmatrix}$ ⇀⦇ retirepool kh e ,POOL⦈ $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Certs.html#7361}{\htmlId{9936}{\htmlClass{Generalizable}{\text{pools}}}}\, \\ \,\href{Class.HasSingleton.html#288}{\htmlId{9944}{\htmlClass{Field Operator}{\text{❴}}}}\, \,\href{Ledger.Conway.Specification.Certs.html#7727}{\htmlId{9946}{\htmlClass{Generalizable}{\text{kh}}}}\, , \,\href{Ledger.Conway.Specification.Certs.html#7676}{\htmlId{9951}{\htmlClass{Generalizable}{\text{e}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{9953}{\htmlClass{Field Operator}{\text{❵}}}}\, \,\href{Axiom.Set.Map.html#6320}{\htmlId{9955}{\htmlClass{Function Operator}{\text{∪ˡ}}}}\, \,\href{Ledger.Conway.Specification.Certs.html#7394}{\htmlId{9958}{\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#7676}{\htmlId{10082}{\htmlClass{Generalizable}{\text{e}}}}\, \\ \,\href{Ledger.Conway.Specification.Certs.html#7813}{\htmlId{10086}{\htmlClass{Generalizable}{\text{pp}}}}\, \\ \,\href{Ledger.Conway.Specification.Certs.html#7698}{\htmlId{10091}{\htmlClass{Generalizable}{\text{vs}}}}\, \\ \,\href{Ledger.Conway.Specification.Certs.html#7430}{\htmlId{10096}{\htmlClass{Generalizable}{\text{wdrls}}}}\, \\ \,\href{Ledger.Conway.Specification.Certs.html#7927}{\htmlId{10104}{\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#7214}{\htmlId{10237}{\htmlClass{Generalizable}{\text{dReps}}}}\, \\ \,\href{Ledger.Conway.Specification.Certs.html#7286}{\htmlId{10245}{\htmlClass{Generalizable}{\text{ccKeys}}}}\, \end{pmatrix}$ ⇀⦇ regdrep c d an ,GOVCERT⦈ $\begin{pmatrix} \,\href{Class.HasSingleton.html#288}{\htmlId{10284}{\htmlClass{Field Operator}{\text{❴}}}}\, \,\href{Ledger.Conway.Specification.Certs.html#7565}{\htmlId{10286}{\htmlClass{Generalizable}{\text{c}}}}\, , \,\href{Ledger.Conway.Specification.Certs.html#7676}{\htmlId{10290}{\htmlClass{Generalizable}{\text{e}}}}\, \,\href{Class.HasAdd.Core.html#162}{\htmlId{10292}{\htmlClass{Field Operator}{\text{+}}}}\, \,\href{Ledger.Conway.Specification.Certs.html#7813}{\htmlId{10294}{\htmlClass{Generalizable}{\text{pp}}}}\, \,\htmlId{10297}{\htmlClass{Symbol}{\text{.}}}\,\,\href{Ledger.Conway.Specification.PParams.html#3442}{\htmlId{10298}{\htmlClass{Field}{\text{drepActivity}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{10311}{\htmlClass{Field Operator}{\text{❵}}}}\, \,\href{Axiom.Set.Map.html#6320}{\htmlId{10313}{\htmlClass{Function Operator}{\text{∪ˡ}}}}\, \,\href{Ledger.Conway.Specification.Certs.html#7214}{\htmlId{10316}{\htmlClass{Generalizable}{\text{dReps}}}}\, \\ \,\href{Ledger.Conway.Specification.Certs.html#7286}{\htmlId{10324}{\htmlClass{Generalizable}{\text{ccKeys}}}}\, \end{pmatrix}$

  GOVCERT-deregdrep :
     c  dom dReps
      ────────────────────────────────
      $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Certs.html#7676}{\htmlId{10423}{\htmlClass{Generalizable}{\text{e}}}}\, \\ \,\href{Ledger.Conway.Specification.Certs.html#7813}{\htmlId{10427}{\htmlClass{Generalizable}{\text{pp}}}}\, \\ \,\href{Ledger.Conway.Specification.Certs.html#7698}{\htmlId{10432}{\htmlClass{Generalizable}{\text{vs}}}}\, \\ \,\href{Ledger.Conway.Specification.Certs.html#7430}{\htmlId{10437}{\htmlClass{Generalizable}{\text{wdrls}}}}\, \\ \,\href{Ledger.Conway.Specification.Certs.html#7927}{\htmlId{10445}{\htmlClass{Generalizable}{\text{cc}}}}\, \end{pmatrix}$  $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Certs.html#7214}{\htmlId{10454}{\htmlClass{Generalizable}{\text{dReps}}}}\, \\ \,\href{Ledger.Conway.Specification.Certs.html#7286}{\htmlId{10462}{\htmlClass{Generalizable}{\text{ccKeys}}}}\, \end{pmatrix}$ ⇀⦇ deregdrep c d ,GOVCERT⦈ $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Certs.html#7214}{\htmlId{10500}{\htmlClass{Generalizable}{\text{dReps}}}}\, \,\href{Axiom.Set.Map.html#10748}{\htmlId{10506}{\htmlClass{Function Operator}{\text{∣}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{10508}{\htmlClass{Field Operator}{\text{❴}}}}\, \,\href{Ledger.Conway.Specification.Certs.html#7565}{\htmlId{10510}{\htmlClass{Generalizable}{\text{c}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{10512}{\htmlClass{Field Operator}{\text{❵}}}}\, \,\href{Axiom.Set.Map.html#10748}{\htmlId{10514}{\htmlClass{Function Operator}{\text{ᶜ}}}}\, \\ \,\href{Ledger.Conway.Specification.Certs.html#7286}{\htmlId{10518}{\htmlClass{Generalizable}{\text{ccKeys}}}}\, \end{pmatrix}$

  GOVCERT-ccreghot :
     (c , nothing)  ccKeys
     c  cc
      ────────────────────────────────
      $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Certs.html#7676}{\htmlId{10638}{\htmlClass{Generalizable}{\text{e}}}}\, \\ \,\href{Ledger.Conway.Specification.Certs.html#7813}{\htmlId{10642}{\htmlClass{Generalizable}{\text{pp}}}}\, \\ \,\href{Ledger.Conway.Specification.Certs.html#7698}{\htmlId{10647}{\htmlClass{Generalizable}{\text{vs}}}}\, \\ \,\href{Ledger.Conway.Specification.Certs.html#7430}{\htmlId{10652}{\htmlClass{Generalizable}{\text{wdrls}}}}\, \\ \,\href{Ledger.Conway.Specification.Certs.html#7927}{\htmlId{10660}{\htmlClass{Generalizable}{\text{cc}}}}\, \end{pmatrix}$  $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Certs.html#7214}{\htmlId{10669}{\htmlClass{Generalizable}{\text{dReps}}}}\, \\ \,\href{Ledger.Conway.Specification.Certs.html#7286}{\htmlId{10677}{\htmlClass{Generalizable}{\text{ccKeys}}}}\, \end{pmatrix}$ ⇀⦇ ccreghot c mc ,GOVCERT⦈ $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Certs.html#7214}{\htmlId{10715}{\htmlClass{Generalizable}{\text{dReps}}}}\, \\ \,\href{Class.HasSingleton.html#288}{\htmlId{10723}{\htmlClass{Field Operator}{\text{❴}}}}\, \,\href{Ledger.Conway.Specification.Certs.html#7565}{\htmlId{10725}{\htmlClass{Generalizable}{\text{c}}}}\, , \,\href{Ledger.Conway.Specification.Certs.html#7592}{\htmlId{10729}{\htmlClass{Generalizable}{\text{mc}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{10732}{\htmlClass{Field Operator}{\text{❵}}}}\, \,\href{Axiom.Set.Map.html#6320}{\htmlId{10734}{\htmlClass{Function Operator}{\text{∪ˡ}}}}\, \,\href{Ledger.Conway.Specification.Certs.html#7286}{\htmlId{10737}{\htmlClass{Generalizable}{\text{ccKeys}}}}\, \end{pmatrix}$



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

  CERT-deleg :
     $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Certs.html#7813}{\htmlId{10858}{\htmlClass{Generalizable}{\text{pp}}}}\, \\ \,\href{Ledger.Conway.Specification.Certs.html#4045}{\htmlId{10863}{\htmlClass{Field}{\text{PState.pools}}}}\, \,\href{Ledger.Conway.Specification.Certs.html#7907}{\htmlId{10876}{\htmlClass{Generalizable}{\text{stᵖ}}}}\, \\ \,\href{Class.IsSet.html#916}{\htmlId{10882}{\htmlClass{Function}{\text{dom}}}}\, \,\htmlId{10886}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Conway.Specification.Certs.html#4160}{\htmlId{10887}{\htmlClass{Field}{\text{GState.dreps}}}}\, \,\href{Ledger.Conway.Specification.Certs.html#7887}{\htmlId{10900}{\htmlClass{Generalizable}{\text{stᵍ}}}}\,\,\htmlId{10903}{\htmlClass{Symbol}{\text{)}}}\, \end{pmatrix}$  stᵈ ⇀⦇ dCert ,DELEG⦈ stᵈ'
      ────────────────────────────────
      $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Certs.html#7676}{\htmlId{10982}{\htmlClass{Generalizable}{\text{e}}}}\, \\ \,\href{Ledger.Conway.Specification.Certs.html#7813}{\htmlId{10986}{\htmlClass{Generalizable}{\text{pp}}}}\, \\ \,\href{Ledger.Conway.Specification.Certs.html#7698}{\htmlId{10991}{\htmlClass{Generalizable}{\text{vs}}}}\, \\ \,\href{Ledger.Conway.Specification.Certs.html#7430}{\htmlId{10996}{\htmlClass{Generalizable}{\text{wdrls}}}}\, \\ \,\href{Ledger.Conway.Specification.Certs.html#7927}{\htmlId{11004}{\htmlClass{Generalizable}{\text{cc}}}}\, \end{pmatrix}$  $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Certs.html#7867}{\htmlId{11013}{\htmlClass{Generalizable}{\text{stᵈ}}}}\, \\ \,\href{Ledger.Conway.Specification.Certs.html#7907}{\htmlId{11019}{\htmlClass{Generalizable}{\text{stᵖ}}}}\, \\ \,\href{Ledger.Conway.Specification.Certs.html#7887}{\htmlId{11025}{\htmlClass{Generalizable}{\text{stᵍ}}}}\, \end{pmatrix}$ ⇀⦇ dCert ,CERT⦈ $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Certs.html#7871}{\htmlId{11049}{\htmlClass{Generalizable}{\text{stᵈ'}}}}\, \\ \,\href{Ledger.Conway.Specification.Certs.html#7907}{\htmlId{11056}{\htmlClass{Generalizable}{\text{stᵖ}}}}\, \\ \,\href{Ledger.Conway.Specification.Certs.html#7887}{\htmlId{11062}{\htmlClass{Generalizable}{\text{stᵍ}}}}\, \end{pmatrix}$

  CERT-pool :
     pp  stᵖ ⇀⦇ dCert ,POOL⦈ stᵖ'
      ────────────────────────────────
      $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Certs.html#7676}{\htmlId{11166}{\htmlClass{Generalizable}{\text{e}}}}\, \\ \,\href{Ledger.Conway.Specification.Certs.html#7813}{\htmlId{11170}{\htmlClass{Generalizable}{\text{pp}}}}\, \\ \,\href{Ledger.Conway.Specification.Certs.html#7698}{\htmlId{11175}{\htmlClass{Generalizable}{\text{vs}}}}\, \\ \,\href{Ledger.Conway.Specification.Certs.html#7430}{\htmlId{11180}{\htmlClass{Generalizable}{\text{wdrls}}}}\, \\ \,\href{Ledger.Conway.Specification.Certs.html#7927}{\htmlId{11188}{\htmlClass{Generalizable}{\text{cc}}}}\, \end{pmatrix}$  $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Certs.html#7867}{\htmlId{11197}{\htmlClass{Generalizable}{\text{stᵈ}}}}\, \\ \,\href{Ledger.Conway.Specification.Certs.html#7907}{\htmlId{11203}{\htmlClass{Generalizable}{\text{stᵖ}}}}\, \\ \,\href{Ledger.Conway.Specification.Certs.html#7887}{\htmlId{11209}{\htmlClass{Generalizable}{\text{stᵍ}}}}\, \end{pmatrix}$ ⇀⦇ dCert ,CERT⦈ $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Certs.html#7867}{\htmlId{11233}{\htmlClass{Generalizable}{\text{stᵈ}}}}\, \\ \,\href{Ledger.Conway.Specification.Certs.html#7911}{\htmlId{11239}{\htmlClass{Generalizable}{\text{stᵖ'}}}}\, \\ \,\href{Ledger.Conway.Specification.Certs.html#7887}{\htmlId{11246}{\htmlClass{Generalizable}{\text{stᵍ}}}}\, \end{pmatrix}$

  CERT-vdel :
     Γ  stᵍ ⇀⦇ dCert ,GOVCERT⦈ stᵍ'
      ────────────────────────────────
      Γ  $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Certs.html#7867}{\htmlId{11356}{\htmlClass{Generalizable}{\text{stᵈ}}}}\, \\ \,\href{Ledger.Conway.Specification.Certs.html#7907}{\htmlId{11362}{\htmlClass{Generalizable}{\text{stᵖ}}}}\, \\ \,\href{Ledger.Conway.Specification.Certs.html#7887}{\htmlId{11368}{\htmlClass{Generalizable}{\text{stᵍ}}}}\, \end{pmatrix}$ ⇀⦇ dCert ,CERT⦈ $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Certs.html#7867}{\htmlId{11392}{\htmlClass{Generalizable}{\text{stᵈ}}}}\, \\ \,\href{Ledger.Conway.Specification.Certs.html#7907}{\htmlId{11398}{\htmlClass{Generalizable}{\text{stᵖ}}}}\, \\ \,\href{Ledger.Conway.Specification.Certs.html#7891}{\htmlId{11404}{\htmlClass{Generalizable}{\text{stᵍ'}}}}\, \end{pmatrix}$



open GovVote using (voter)
data _⊢_⇀⦇_,CERTBASE⦈_ where


  CERT-base :
    let refresh          = mapPartial (isGovVoterDRep  voter) (fromList vs)
        refreshedDReps   = mapValueRestricted (const (e + pp .drepActivity)) dReps refresh
        wdrlCreds        = mapˢ stake (dom wdrls)
        validVoteDelegs  = voteDelegs ∣^ (  mapˢ vDelegCredential (dom dReps)
                                         fromList (vDelegNoConfidence  vDelegAbstain  []) )
    in
     filter isKeyHash wdrlCreds  dom voteDelegs
     mapˢ (map₁ stake) (wdrls ˢ)  rewards ˢ
      ────────────────────────────────
      $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Certs.html#7676}{\htmlId{12027}{\htmlClass{Generalizable}{\text{e}}}}\, \\ \,\href{Ledger.Conway.Specification.Certs.html#7813}{\htmlId{12031}{\htmlClass{Generalizable}{\text{pp}}}}\, \\ \,\href{Ledger.Conway.Specification.Certs.html#7698}{\htmlId{12036}{\htmlClass{Generalizable}{\text{vs}}}}\, \\ \,\href{Ledger.Conway.Specification.Certs.html#7430}{\htmlId{12041}{\htmlClass{Generalizable}{\text{wdrls}}}}\, \\ \,\href{Ledger.Conway.Specification.Certs.html#7927}{\htmlId{12049}{\htmlClass{Generalizable}{\text{cc}}}}\, \end{pmatrix}$  $\begin{pmatrix} \begin{pmatrix} \,\href{Ledger.Conway.Specification.Certs.html#7331}{\htmlId{12060}{\htmlClass{Generalizable}{\text{voteDelegs}}}}\, \\ \,\href{Ledger.Conway.Specification.Certs.html#7255}{\htmlId{12073}{\htmlClass{Generalizable}{\text{stakeDelegs}}}}\, \\ \,\href{Ledger.Conway.Specification.Certs.html#7184}{\htmlId{12087}{\htmlClass{Generalizable}{\text{rewards}}}}\, \end{pmatrix} \\ \,\href{Ledger.Conway.Specification.Certs.html#7907}{\htmlId{12099}{\htmlClass{Generalizable}{\text{stᵖ}}}}\, \\ \begin{pmatrix} \,\href{Ledger.Conway.Specification.Certs.html#7214}{\htmlId{12107}{\htmlClass{Generalizable}{\text{dReps}}}}\, \\ \,\href{Ledger.Conway.Specification.Certs.html#7293}{\htmlId{12115}{\htmlClass{Generalizable}{\text{ccHotKeys}}}}\, \end{pmatrix} \end{pmatrix}$ ⇀⦇ _ ,CERTBASE⦈ $\begin{pmatrix} \begin{pmatrix} \,\href{Ledger.Conway.Specification.Certs.html#11712}{\htmlId{12149}{\htmlClass{Bound}{\text{validVoteDelegs}}}}\, \\ \,\href{Ledger.Conway.Specification.Certs.html#7255}{\htmlId{12167}{\htmlClass{Generalizable}{\text{stakeDelegs}}}}\, \\ \,\href{Axiom.Set.Map.html#9130}{\htmlId{12181}{\htmlClass{Function}{\text{constMap}}}}\, \,\href{Ledger.Conway.Specification.Certs.html#11662}{\htmlId{12190}{\htmlClass{Bound}{\text{wdrlCreds}}}}\, \,\htmlId{12200}{\htmlClass{Number}{\text{0}}}\, \,\href{Axiom.Set.Map.html#6320}{\htmlId{12202}{\htmlClass{Function Operator}{\text{∪ˡ}}}}\, \,\href{Ledger.Conway.Specification.Certs.html#7184}{\htmlId{12205}{\htmlClass{Generalizable}{\text{rewards}}}}\, \end{pmatrix} \\ \,\href{Ledger.Conway.Specification.Certs.html#7907}{\htmlId{12217}{\htmlClass{Generalizable}{\text{stᵖ}}}}\, \\ \begin{pmatrix} \,\href{Ledger.Conway.Specification.Certs.html#11571}{\htmlId{12225}{\htmlClass{Bound}{\text{refreshedDReps}}}}\, \\ \,\href{Ledger.Conway.Specification.Certs.html#7293}{\htmlId{12242}{\htmlClass{Generalizable}{\text{ccHotKeys}}}}\, \end{pmatrix} \end{pmatrix}$