{-# 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 hiding (yes; no)
open RewardAddress
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 : Type
CCHotKeys = Credential ⇀ Maybe Credential

PoolEnv : Type
PoolEnv = PParams

Pools : Type
Pools = KeyHash ⇀ StakePoolParams

Retiring : Type
Retiring = KeyHash ⇀ Epoch

Rewards : Type
Rewards = Credential ⇀ Coin

Stake : Type
Stake = Credential ⇀ Coin

StakeDelegs : Type
StakeDelegs = Credential ⇀ KeyHash


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

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 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 docs because it has been deprecated and we want to discourage people
  -- from using it.
  reg         : Credential → Coin → DCert

instance
  unquoteDecl DecEq-StakePoolParams = derive-DecEq
    ((quote StakePoolParams , DecEq-StakePoolParams) ∷ [])
  unquoteDecl DecEq-DCert = derive-DecEq
    ((quote DCert , DecEq-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
    fPools    : 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

  HasStakeDelegs-CertState : HasStakeDelegs CertState
  HasStakeDelegs-CertState .StakeDelegsOf = StakeDelegsOf ∘ 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 fPools           : 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 where

  DELEG-delegate :
    ∙ (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#8057}{\htmlId{8588}{\htmlClass{Generalizable}{\text{pp}}}}\, \\ \,\href{Ledger.Conway.Specification.Certs.html#7605}{\htmlId{8593}{\htmlClass{Generalizable}{\text{pools}}}}\, \\ \,\href{Ledger.Conway.Specification.Certs.html#7869}{\htmlId{8601}{\htmlClass{Generalizable}{\text{delegatees}}}}\, \end{pmatrix}$ ⊢ $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Certs.html#7567}{\htmlId{8618}{\htmlClass{Generalizable}{\text{vDelegs}}}}\, \\ \,\href{Ledger.Conway.Specification.Certs.html#7491}{\htmlId{8628}{\htmlClass{Generalizable}{\text{sDelegs}}}}\, \\ \,\href{Ledger.Conway.Specification.Certs.html#7423}{\htmlId{8638}{\htmlClass{Generalizable}{\text{rwds}}}}\, \end{pmatrix}$ ⇀⦇ delegate c mvd mkh d ,DELEG⦈ $\begin{pmatrix} \,\href{Axiom.Set.Map.html#9262}{\htmlId{8679}{\htmlClass{Function}{\text{insertIfJust}}}}\, \,\href{Ledger.Conway.Specification.Certs.html#7809}{\htmlId{8692}{\htmlClass{Generalizable}{\text{c}}}}\, \,\href{Ledger.Conway.Specification.Certs.html#8081}{\htmlId{8694}{\htmlClass{Generalizable}{\text{mvd}}}}\, \,\href{Ledger.Conway.Specification.Certs.html#7567}{\htmlId{8698}{\htmlClass{Generalizable}{\text{vDelegs}}}}\, \\ \,\href{Axiom.Set.Map.html#9262}{\htmlId{8708}{\htmlClass{Function}{\text{insertIfJust}}}}\, \,\href{Ledger.Conway.Specification.Certs.html#7809}{\htmlId{8721}{\htmlClass{Generalizable}{\text{c}}}}\, \,\href{Ledger.Conway.Specification.Certs.html#7995}{\htmlId{8723}{\htmlClass{Generalizable}{\text{mkh}}}}\, \,\href{Ledger.Conway.Specification.Certs.html#7491}{\htmlId{8727}{\htmlClass{Generalizable}{\text{sDelegs}}}}\, \\ \,\href{Ledger.Conway.Specification.Certs.html#7423}{\htmlId{8737}{\htmlClass{Generalizable}{\text{rwds}}}}\, \,\href{Axiom.Set.Map.html#7640}{\htmlId{8742}{\htmlClass{Function Operator}{\text{∪ˡ}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{8745}{\htmlClass{Field Operator}{\text{❴}}}}\, \,\href{Ledger.Conway.Specification.Certs.html#7809}{\htmlId{8747}{\htmlClass{Generalizable}{\text{c}}}}\, , \,\htmlId{8751}{\htmlClass{Number}{\text{0}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{8753}{\htmlClass{Field Operator}{\text{❵}}}}\, \end{pmatrix}$

  DELEG-dereg :
    ∙ (c , 0) ∈ rwds
      ────────────────────────────────
      $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Certs.html#8057}{\htmlId{8842}{\htmlClass{Generalizable}{\text{pp}}}}\, \\ \,\href{Ledger.Conway.Specification.Certs.html#7605}{\htmlId{8847}{\htmlClass{Generalizable}{\text{pools}}}}\, \\ \,\href{Ledger.Conway.Specification.Certs.html#7869}{\htmlId{8855}{\htmlClass{Generalizable}{\text{delegatees}}}}\, \end{pmatrix}$ ⊢ $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Certs.html#7567}{\htmlId{8872}{\htmlClass{Generalizable}{\text{vDelegs}}}}\, \\ \,\href{Ledger.Conway.Specification.Certs.html#7491}{\htmlId{8882}{\htmlClass{Generalizable}{\text{sDelegs}}}}\, \\ \,\href{Ledger.Conway.Specification.Certs.html#7423}{\htmlId{8892}{\htmlClass{Generalizable}{\text{rwds}}}}\, \end{pmatrix}$ ⇀⦇ dereg c md ,DELEG⦈ $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Certs.html#7567}{\htmlId{8923}{\htmlClass{Generalizable}{\text{vDelegs}}}}\, \,\href{Axiom.Set.Map.html#13606}{\htmlId{8931}{\htmlClass{Function Operator}{\text{∣}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{8933}{\htmlClass{Field Operator}{\text{❴}}}}\, \,\href{Ledger.Conway.Specification.Certs.html#7809}{\htmlId{8935}{\htmlClass{Generalizable}{\text{c}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{8937}{\htmlClass{Field Operator}{\text{❵}}}}\, \,\href{Axiom.Set.Map.html#13606}{\htmlId{8939}{\htmlClass{Function Operator}{\text{ᶜ}}}}\, \\ \,\href{Ledger.Conway.Specification.Certs.html#7491}{\htmlId{8943}{\htmlClass{Generalizable}{\text{sDelegs}}}}\, \,\href{Axiom.Set.Map.html#13606}{\htmlId{8951}{\htmlClass{Function Operator}{\text{∣}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{8953}{\htmlClass{Field Operator}{\text{❴}}}}\, \,\href{Ledger.Conway.Specification.Certs.html#7809}{\htmlId{8955}{\htmlClass{Generalizable}{\text{c}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{8957}{\htmlClass{Field Operator}{\text{❵}}}}\, \,\href{Axiom.Set.Map.html#13606}{\htmlId{8959}{\htmlClass{Function Operator}{\text{ᶜ}}}}\, \\ \,\href{Ledger.Conway.Specification.Certs.html#7423}{\htmlId{8963}{\htmlClass{Generalizable}{\text{rwds}}}}\, \,\href{Axiom.Set.Map.html#13606}{\htmlId{8968}{\htmlClass{Function Operator}{\text{∣}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{8970}{\htmlClass{Field Operator}{\text{❴}}}}\, \,\href{Ledger.Conway.Specification.Certs.html#7809}{\htmlId{8972}{\htmlClass{Generalizable}{\text{c}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{8974}{\htmlClass{Field Operator}{\text{❵}}}}\, \,\href{Axiom.Set.Map.html#13606}{\htmlId{8976}{\htmlClass{Function Operator}{\text{ᶜ}}}}\, \end{pmatrix}$

  DELEG-reg :
    ∙ c ∉ dom rwds
    ∙ d ≡ pp .keyDeposit ⊎ d ≡ 0
      ────────────────────────────────
      $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Certs.html#8057}{\htmlId{9094}{\htmlClass{Generalizable}{\text{pp}}}}\, \\ \,\href{Ledger.Conway.Specification.Certs.html#7605}{\htmlId{9099}{\htmlClass{Generalizable}{\text{pools}}}}\, \\ \,\href{Ledger.Conway.Specification.Certs.html#7869}{\htmlId{9107}{\htmlClass{Generalizable}{\text{delegatees}}}}\, \end{pmatrix}$ ⊢ $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Certs.html#7567}{\htmlId{9124}{\htmlClass{Generalizable}{\text{vDelegs}}}}\, \\ \,\href{Ledger.Conway.Specification.Certs.html#7491}{\htmlId{9134}{\htmlClass{Generalizable}{\text{sDelegs}}}}\, \\ \,\href{Ledger.Conway.Specification.Certs.html#7423}{\htmlId{9144}{\htmlClass{Generalizable}{\text{rwds}}}}\, \end{pmatrix}$ ⇀⦇ reg c d ,DELEG⦈ $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Certs.html#7567}{\htmlId{9172}{\htmlClass{Generalizable}{\text{vDelegs}}}}\, \\ \,\href{Ledger.Conway.Specification.Certs.html#7491}{\htmlId{9182}{\htmlClass{Generalizable}{\text{sDelegs}}}}\, \\ \,\href{Ledger.Conway.Specification.Certs.html#7423}{\htmlId{9192}{\htmlClass{Generalizable}{\text{rwds}}}}\, \,\href{Axiom.Set.Map.html#7640}{\htmlId{9197}{\htmlClass{Function Operator}{\text{∪ˡ}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{9200}{\htmlClass{Field Operator}{\text{❴}}}}\, \,\href{Ledger.Conway.Specification.Certs.html#7809}{\htmlId{9202}{\htmlClass{Generalizable}{\text{c}}}}\, , \,\htmlId{9206}{\htmlClass{Number}{\text{0}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{9208}{\htmlClass{Field Operator}{\text{❵}}}}\, \end{pmatrix}$


isPoolRegistered : Pools -> KeyHash -> Maybe StakePoolParams
isPoolRegistered ps kh = lookupᵐ? ps kh

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

  POOL-regpool :
    let
      fPool' =
        if isPoolRegistered pools kh
          then ❴ kh , poolParams ❵ ∪ˡ fPools
          else fPools
     in
    ────────────────────────────────
    pp ⊢ $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Certs.html#7605}{\htmlId{9585}{\htmlClass{Generalizable}{\text{pools}}}}\,
         \\ \,\href{Ledger.Conway.Specification.Certs.html#7611}{\htmlId{9602}{\htmlClass{Generalizable}{\text{fPools}}}}\,
         \\ \,\href{Ledger.Conway.Specification.Certs.html#7638}{\htmlId{9620}{\htmlClass{Generalizable}{\text{retiring}}}}\,
         \end{pmatrix}$ ⇀⦇ regpool kh poolParams ,POOL⦈ $\begin{pmatrix}
           \,\href{Ledger.Conway.Specification.Certs.html#7605}{\htmlId{9685}{\htmlClass{Generalizable}{\text{pools}}}}\, \,\href{Axiom.Set.Map.html#7640}{\htmlId{9691}{\htmlClass{Function Operator}{\text{∪ˡ}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{9694}{\htmlClass{Field Operator}{\text{❴}}}}\, \,\href{Ledger.Conway.Specification.Certs.html#7971}{\htmlId{9696}{\htmlClass{Generalizable}{\text{kh}}}}\, , \,\href{Ledger.Conway.Specification.Certs.html#8025}{\htmlId{9701}{\htmlClass{Generalizable}{\text{poolParams}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{9712}{\htmlClass{Field Operator}{\text{❵}}}}\,
         \\ \,\href{Ledger.Conway.Specification.Certs.html#9416}{\htmlId{9725}{\htmlClass{Bound}{\text{fPool'}}}}\,
         \\ \,\href{Ledger.Conway.Specification.Certs.html#7638}{\htmlId{9743}{\htmlClass{Generalizable}{\text{retiring}}}}\, \,\href{Axiom.Set.Map.html#13606}{\htmlId{9752}{\htmlClass{Function Operator}{\text{∣}}}}\,  \,\href{Class.HasSingleton.html#288}{\htmlId{9755}{\htmlClass{Field Operator}{\text{❴}}}}\, \,\href{Ledger.Conway.Specification.Certs.html#7971}{\htmlId{9757}{\htmlClass{Generalizable}{\text{kh}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{9760}{\htmlClass{Field Operator}{\text{❵}}}}\, \,\href{Axiom.Set.Map.html#13606}{\htmlId{9762}{\htmlClass{Function Operator}{\text{ᶜ}}}}\,
         \end{pmatrix}$

  POOL-retirepool :
    ────────────────────────────────
    pp ⊢ $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Certs.html#7605}{\htmlId{9844}{\htmlClass{Generalizable}{\text{pools}}}}\,
         \\ \,\href{Ledger.Conway.Specification.Certs.html#7611}{\htmlId{9861}{\htmlClass{Generalizable}{\text{fPools}}}}\,
         \\ \,\href{Ledger.Conway.Specification.Certs.html#7638}{\htmlId{9879}{\htmlClass{Generalizable}{\text{retiring}}}}\,
         \end{pmatrix}$ ⇀⦇ retirepool kh e ,POOL⦈ $\begin{pmatrix}
           \,\href{Ledger.Conway.Specification.Certs.html#7605}{\htmlId{9938}{\htmlClass{Generalizable}{\text{pools}}}}\,
         \\ \,\href{Ledger.Conway.Specification.Certs.html#7611}{\htmlId{9955}{\htmlClass{Generalizable}{\text{fPools}}}}\,
         \\ \,\href{Class.HasSingleton.html#288}{\htmlId{9973}{\htmlClass{Field Operator}{\text{❴}}}}\, \,\href{Ledger.Conway.Specification.Certs.html#7971}{\htmlId{9975}{\htmlClass{Generalizable}{\text{kh}}}}\, , \,\href{Ledger.Conway.Specification.Certs.html#7920}{\htmlId{9980}{\htmlClass{Generalizable}{\text{e}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{9982}{\htmlClass{Field Operator}{\text{❵}}}}\, \,\href{Axiom.Set.Map.html#7640}{\htmlId{9984}{\htmlClass{Function Operator}{\text{∪ˡ}}}}\, \,\href{Ledger.Conway.Specification.Certs.html#7638}{\htmlId{9987}{\htmlClass{Generalizable}{\text{retiring}}}}\,
         \end{pmatrix}$


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

  GOVCERT-regdrep :
    ∙ (d ≡ pp .drepDeposit × c ∉ dom dReps) ⊎ (d ≡ 0 × c ∈ dom dReps)
      ────────────────────────────────
      $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Certs.html#7920}{\htmlId{10218}{\htmlClass{Generalizable}{\text{e}}}}\, \\ \,\href{Ledger.Conway.Specification.Certs.html#8057}{\htmlId{10222}{\htmlClass{Generalizable}{\text{pp}}}}\, \\ \,\href{Ledger.Conway.Specification.Certs.html#7942}{\htmlId{10227}{\htmlClass{Generalizable}{\text{vs}}}}\, \\ \,\href{Ledger.Conway.Specification.Certs.html#7674}{\htmlId{10232}{\htmlClass{Generalizable}{\text{wdrls}}}}\, \\ \,\href{Ledger.Conway.Specification.Certs.html#8171}{\htmlId{10240}{\htmlClass{Generalizable}{\text{cc}}}}\, \end{pmatrix}$ ⊢ $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Certs.html#7458}{\htmlId{10249}{\htmlClass{Generalizable}{\text{dReps}}}}\, \\ \,\href{Ledger.Conway.Specification.Certs.html#7530}{\htmlId{10257}{\htmlClass{Generalizable}{\text{ccKeys}}}}\, \end{pmatrix}$ ⇀⦇ regdrep c d an ,GOVCERT⦈ $\begin{pmatrix} \,\href{Class.HasSingleton.html#288}{\htmlId{10296}{\htmlClass{Field Operator}{\text{❴}}}}\, \,\href{Ledger.Conway.Specification.Certs.html#7809}{\htmlId{10298}{\htmlClass{Generalizable}{\text{c}}}}\, , \,\href{Ledger.Conway.Specification.Certs.html#7920}{\htmlId{10302}{\htmlClass{Generalizable}{\text{e}}}}\, \,\href{Class.HasAdd.Core.html#162}{\htmlId{10304}{\htmlClass{Field Operator}{\text{+}}}}\, \,\href{Ledger.Conway.Specification.Certs.html#8057}{\htmlId{10306}{\htmlClass{Generalizable}{\text{pp}}}}\, \,\htmlId{10309}{\htmlClass{Symbol}{\text{.}}}\,\,\href{Ledger.Conway.Specification.PParams.html#3513}{\htmlId{10310}{\htmlClass{Field}{\text{drepActivity}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{10323}{\htmlClass{Field Operator}{\text{❵}}}}\, \,\href{Axiom.Set.Map.html#7640}{\htmlId{10325}{\htmlClass{Function Operator}{\text{∪ˡ}}}}\, \,\href{Ledger.Conway.Specification.Certs.html#7458}{\htmlId{10328}{\htmlClass{Generalizable}{\text{dReps}}}}\, \\ \,\href{Ledger.Conway.Specification.Certs.html#7530}{\htmlId{10336}{\htmlClass{Generalizable}{\text{ccKeys}}}}\, \end{pmatrix}$

  GOVCERT-deregdrep :
    ∙ c ∈ dom dReps
      ────────────────────────────────
      $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Certs.html#7920}{\htmlId{10435}{\htmlClass{Generalizable}{\text{e}}}}\, \\ \,\href{Ledger.Conway.Specification.Certs.html#8057}{\htmlId{10439}{\htmlClass{Generalizable}{\text{pp}}}}\, \\ \,\href{Ledger.Conway.Specification.Certs.html#7942}{\htmlId{10444}{\htmlClass{Generalizable}{\text{vs}}}}\, \\ \,\href{Ledger.Conway.Specification.Certs.html#7674}{\htmlId{10449}{\htmlClass{Generalizable}{\text{wdrls}}}}\, \\ \,\href{Ledger.Conway.Specification.Certs.html#8171}{\htmlId{10457}{\htmlClass{Generalizable}{\text{cc}}}}\, \end{pmatrix}$ ⊢ $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Certs.html#7458}{\htmlId{10466}{\htmlClass{Generalizable}{\text{dReps}}}}\, \\ \,\href{Ledger.Conway.Specification.Certs.html#7530}{\htmlId{10474}{\htmlClass{Generalizable}{\text{ccKeys}}}}\, \end{pmatrix}$ ⇀⦇ deregdrep c d ,GOVCERT⦈ $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Certs.html#7458}{\htmlId{10512}{\htmlClass{Generalizable}{\text{dReps}}}}\, \,\href{Axiom.Set.Map.html#13606}{\htmlId{10518}{\htmlClass{Function Operator}{\text{∣}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{10520}{\htmlClass{Field Operator}{\text{❴}}}}\, \,\href{Ledger.Conway.Specification.Certs.html#7809}{\htmlId{10522}{\htmlClass{Generalizable}{\text{c}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{10524}{\htmlClass{Field Operator}{\text{❵}}}}\, \,\href{Axiom.Set.Map.html#13606}{\htmlId{10526}{\htmlClass{Function Operator}{\text{ᶜ}}}}\, \\ \,\href{Ledger.Conway.Specification.Certs.html#7530}{\htmlId{10530}{\htmlClass{Generalizable}{\text{ccKeys}}}}\, \end{pmatrix}$

  GOVCERT-ccreghot :
    ∙ (c , nothing) ∉ ccKeys
    ∙ c ∈ cc
      ────────────────────────────────
      $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Certs.html#7920}{\htmlId{10650}{\htmlClass{Generalizable}{\text{e}}}}\, \\ \,\href{Ledger.Conway.Specification.Certs.html#8057}{\htmlId{10654}{\htmlClass{Generalizable}{\text{pp}}}}\, \\ \,\href{Ledger.Conway.Specification.Certs.html#7942}{\htmlId{10659}{\htmlClass{Generalizable}{\text{vs}}}}\, \\ \,\href{Ledger.Conway.Specification.Certs.html#7674}{\htmlId{10664}{\htmlClass{Generalizable}{\text{wdrls}}}}\, \\ \,\href{Ledger.Conway.Specification.Certs.html#8171}{\htmlId{10672}{\htmlClass{Generalizable}{\text{cc}}}}\, \end{pmatrix}$ ⊢ $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Certs.html#7458}{\htmlId{10681}{\htmlClass{Generalizable}{\text{dReps}}}}\, \\ \,\href{Ledger.Conway.Specification.Certs.html#7530}{\htmlId{10689}{\htmlClass{Generalizable}{\text{ccKeys}}}}\, \end{pmatrix}$ ⇀⦇ ccreghot c mc ,GOVCERT⦈ $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Certs.html#7458}{\htmlId{10727}{\htmlClass{Generalizable}{\text{dReps}}}}\, \\ \,\href{Class.HasSingleton.html#288}{\htmlId{10735}{\htmlClass{Field Operator}{\text{❴}}}}\, \,\href{Ledger.Conway.Specification.Certs.html#7809}{\htmlId{10737}{\htmlClass{Generalizable}{\text{c}}}}\, , \,\href{Ledger.Conway.Specification.Certs.html#7836}{\htmlId{10741}{\htmlClass{Generalizable}{\text{mc}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{10744}{\htmlClass{Field Operator}{\text{❵}}}}\, \,\href{Axiom.Set.Map.html#7640}{\htmlId{10746}{\htmlClass{Function Operator}{\text{∪ˡ}}}}\, \,\href{Ledger.Conway.Specification.Certs.html#7530}{\htmlId{10749}{\htmlClass{Generalizable}{\text{ccKeys}}}}\, \end{pmatrix}$


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

  CERT-deleg :
    ∙ $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Certs.html#8057}{\htmlId{10859}{\htmlClass{Generalizable}{\text{pp}}}}\, \\ \,\href{Ledger.Conway.Specification.Certs.html#4141}{\htmlId{10864}{\htmlClass{Field}{\text{PState.pools}}}}\, \,\href{Ledger.Conway.Specification.Certs.html#8151}{\htmlId{10877}{\htmlClass{Generalizable}{\text{stᵖ}}}}\, \\ \,\href{Class.IsSet.html#916}{\htmlId{10883}{\htmlClass{Function}{\text{dom}}}}\, \,\htmlId{10887}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Conway.Specification.Certs.html#4278}{\htmlId{10888}{\htmlClass{Field}{\text{GState.dreps}}}}\, \,\href{Ledger.Conway.Specification.Certs.html#8131}{\htmlId{10901}{\htmlClass{Generalizable}{\text{stᵍ}}}}\,\,\htmlId{10904}{\htmlClass{Symbol}{\text{)}}}\, \end{pmatrix}$ ⊢ stᵈ ⇀⦇ dCert ,DELEG⦈ stᵈ'
      ────────────────────────────────
      $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Certs.html#7920}{\htmlId{10983}{\htmlClass{Generalizable}{\text{e}}}}\, \\ \,\href{Ledger.Conway.Specification.Certs.html#8057}{\htmlId{10987}{\htmlClass{Generalizable}{\text{pp}}}}\, \\ \,\href{Ledger.Conway.Specification.Certs.html#7942}{\htmlId{10992}{\htmlClass{Generalizable}{\text{vs}}}}\, \\ \,\href{Ledger.Conway.Specification.Certs.html#7674}{\htmlId{10997}{\htmlClass{Generalizable}{\text{wdrls}}}}\, \\ \,\href{Ledger.Conway.Specification.Certs.html#8171}{\htmlId{11005}{\htmlClass{Generalizable}{\text{cc}}}}\, \end{pmatrix}$ ⊢ $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Certs.html#8111}{\htmlId{11014}{\htmlClass{Generalizable}{\text{stᵈ}}}}\, \\ \,\href{Ledger.Conway.Specification.Certs.html#8151}{\htmlId{11020}{\htmlClass{Generalizable}{\text{stᵖ}}}}\, \\ \,\href{Ledger.Conway.Specification.Certs.html#8131}{\htmlId{11026}{\htmlClass{Generalizable}{\text{stᵍ}}}}\, \end{pmatrix}$ ⇀⦇ dCert ,CERT⦈ $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Certs.html#8115}{\htmlId{11050}{\htmlClass{Generalizable}{\text{stᵈ'}}}}\, \\ \,\href{Ledger.Conway.Specification.Certs.html#8151}{\htmlId{11057}{\htmlClass{Generalizable}{\text{stᵖ}}}}\, \\ \,\href{Ledger.Conway.Specification.Certs.html#8131}{\htmlId{11063}{\htmlClass{Generalizable}{\text{stᵍ}}}}\, \end{pmatrix}$

  CERT-pool :
    ∙ pp ⊢ stᵖ ⇀⦇ dCert ,POOL⦈ stᵖ'
      ────────────────────────────────
      $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Certs.html#7920}{\htmlId{11167}{\htmlClass{Generalizable}{\text{e}}}}\, \\ \,\href{Ledger.Conway.Specification.Certs.html#8057}{\htmlId{11171}{\htmlClass{Generalizable}{\text{pp}}}}\, \\ \,\href{Ledger.Conway.Specification.Certs.html#7942}{\htmlId{11176}{\htmlClass{Generalizable}{\text{vs}}}}\, \\ \,\href{Ledger.Conway.Specification.Certs.html#7674}{\htmlId{11181}{\htmlClass{Generalizable}{\text{wdrls}}}}\, \\ \,\href{Ledger.Conway.Specification.Certs.html#8171}{\htmlId{11189}{\htmlClass{Generalizable}{\text{cc}}}}\, \end{pmatrix}$ ⊢ $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Certs.html#8111}{\htmlId{11198}{\htmlClass{Generalizable}{\text{stᵈ}}}}\, \\ \,\href{Ledger.Conway.Specification.Certs.html#8151}{\htmlId{11204}{\htmlClass{Generalizable}{\text{stᵖ}}}}\, \\ \,\href{Ledger.Conway.Specification.Certs.html#8131}{\htmlId{11210}{\htmlClass{Generalizable}{\text{stᵍ}}}}\, \end{pmatrix}$ ⇀⦇ dCert ,CERT⦈ $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Certs.html#8111}{\htmlId{11234}{\htmlClass{Generalizable}{\text{stᵈ}}}}\, \\ \,\href{Ledger.Conway.Specification.Certs.html#8155}{\htmlId{11240}{\htmlClass{Generalizable}{\text{stᵖ'}}}}\, \\ \,\href{Ledger.Conway.Specification.Certs.html#8131}{\htmlId{11247}{\htmlClass{Generalizable}{\text{stᵍ}}}}\, \end{pmatrix}$

  CERT-vdel :
    ∙ Γ ⊢ stᵍ ⇀⦇ dCert ,GOVCERT⦈ stᵍ'
      ────────────────────────────────
      Γ ⊢ $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Certs.html#8111}{\htmlId{11357}{\htmlClass{Generalizable}{\text{stᵈ}}}}\, \\ \,\href{Ledger.Conway.Specification.Certs.html#8151}{\htmlId{11363}{\htmlClass{Generalizable}{\text{stᵖ}}}}\, \\ \,\href{Ledger.Conway.Specification.Certs.html#8131}{\htmlId{11369}{\htmlClass{Generalizable}{\text{stᵍ}}}}\, \end{pmatrix}$ ⇀⦇ dCert ,CERT⦈ $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Certs.html#8111}{\htmlId{11393}{\htmlClass{Generalizable}{\text{stᵈ}}}}\, \\ \,\href{Ledger.Conway.Specification.Certs.html#8151}{\htmlId{11399}{\htmlClass{Generalizable}{\text{stᵖ}}}}\, \\ \,\href{Ledger.Conway.Specification.Certs.html#8135}{\htmlId{11405}{\htmlClass{Generalizable}{\text{stᵍ'}}}}\, \end{pmatrix}$


open GovVote using (voter)


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

  CERT-pre :
    let refresh         = mapPartial (isGovVoterDRep ∘ voter) (fromList vs)
        refreshedDReps  = mapValueRestricted (const (e + pp .drepActivity)) dReps refresh
        wdrlCreds       = mapˢ stake (dom wdrls)
    in
    ∙ filter isKeyHash wdrlCreds ⊆ dom voteDelegs
    ∙ mapˢ (map₁ stake) (wdrls ˢ) ⊆ rewards ˢ
      ────────────────────────────────
      $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Certs.html#7920}{\htmlId{11896}{\htmlClass{Generalizable}{\text{e}}}}\, \\ \,\href{Ledger.Conway.Specification.Certs.html#8057}{\htmlId{11900}{\htmlClass{Generalizable}{\text{pp}}}}\, \\ \,\href{Ledger.Conway.Specification.Certs.html#7942}{\htmlId{11905}{\htmlClass{Generalizable}{\text{vs}}}}\, \\ \,\href{Ledger.Conway.Specification.Certs.html#7674}{\htmlId{11910}{\htmlClass{Generalizable}{\text{wdrls}}}}\, \\ \,\href{Ledger.Conway.Specification.Certs.html#8171}{\htmlId{11918}{\htmlClass{Generalizable}{\text{cc}}}}\, \end{pmatrix}$ ⊢ $\begin{pmatrix} \begin{pmatrix} \,\href{Ledger.Conway.Specification.Certs.html#7575}{\htmlId{11929}{\htmlClass{Generalizable}{\text{voteDelegs}}}}\, \\ \,\href{Ledger.Conway.Specification.Certs.html#7499}{\htmlId{11942}{\htmlClass{Generalizable}{\text{stakeDelegs}}}}\, \\ \,\href{Ledger.Conway.Specification.Certs.html#7428}{\htmlId{11956}{\htmlClass{Generalizable}{\text{rewards}}}}\, \end{pmatrix} \\ \,\href{Ledger.Conway.Specification.Certs.html#8151}{\htmlId{11968}{\htmlClass{Generalizable}{\text{stᵖ}}}}\, \\ \begin{pmatrix} \,\href{Ledger.Conway.Specification.Certs.html#7458}{\htmlId{11976}{\htmlClass{Generalizable}{\text{dReps}}}}\, \\ \,\href{Ledger.Conway.Specification.Certs.html#7537}{\htmlId{11984}{\htmlClass{Generalizable}{\text{ccHotKeys}}}}\, \end{pmatrix} \end{pmatrix}$ ⇀⦇ _ ,PRE-CERT⦈ $\begin{pmatrix} \begin{pmatrix} \,\href{Ledger.Conway.Specification.Certs.html#7575}{\htmlId{12018}{\htmlClass{Generalizable}{\text{voteDelegs}}}}\, \\ \,\href{Ledger.Conway.Specification.Certs.html#7499}{\htmlId{12031}{\htmlClass{Generalizable}{\text{stakeDelegs}}}}\, \\ \,\href{Axiom.Set.Map.html#11988}{\htmlId{12045}{\htmlClass{Function}{\text{constMap}}}}\, \,\href{Ledger.Conway.Specification.Certs.html#11705}{\htmlId{12054}{\htmlClass{Bound}{\text{wdrlCreds}}}}\, \,\htmlId{12064}{\htmlClass{Number}{\text{0}}}\, \,\href{Axiom.Set.Map.html#7640}{\htmlId{12066}{\htmlClass{Function Operator}{\text{∪ˡ}}}}\, \,\href{Ledger.Conway.Specification.Certs.html#7428}{\htmlId{12069}{\htmlClass{Generalizable}{\text{rewards}}}}\, \end{pmatrix} \\ \,\href{Ledger.Conway.Specification.Certs.html#8151}{\htmlId{12081}{\htmlClass{Generalizable}{\text{stᵖ}}}}\, \\ \begin{pmatrix} \,\href{Ledger.Conway.Specification.Certs.html#11615}{\htmlId{12089}{\htmlClass{Bound}{\text{refreshedDReps}}}}\, \\ \,\href{Ledger.Conway.Specification.Certs.html#7537}{\htmlId{12106}{\htmlClass{Generalizable}{\text{ccHotKeys}}}}\, \end{pmatrix} \end{pmatrix}$


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

  CERT-post :
    let activeVDelegs = mapˢ vDelegCredential (dom (DRepsOf stᵍ))
                         ∪ fromList (vDelegNoConfidence ∷ vDelegAbstain ∷ [])
    in
      $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Certs.html#7920}{\htmlId{12371}{\htmlClass{Generalizable}{\text{e}}}}\, \\ \,\href{Ledger.Conway.Specification.Certs.html#8057}{\htmlId{12375}{\htmlClass{Generalizable}{\text{pp}}}}\, \\ \,\href{Ledger.Conway.Specification.Certs.html#7942}{\htmlId{12380}{\htmlClass{Generalizable}{\text{vs}}}}\, \\ \,\href{Ledger.Conway.Specification.Certs.html#7674}{\htmlId{12385}{\htmlClass{Generalizable}{\text{wdrls}}}}\, \\ \,\href{Ledger.Conway.Specification.Certs.html#8171}{\htmlId{12393}{\htmlClass{Generalizable}{\text{cc}}}}\, \end{pmatrix}$ ⊢ $\begin{pmatrix} \begin{pmatrix} \,\href{Ledger.Conway.Specification.Certs.html#7575}{\htmlId{12404}{\htmlClass{Generalizable}{\text{voteDelegs}}}}\, \\ \,\href{Ledger.Conway.Specification.Certs.html#7499}{\htmlId{12417}{\htmlClass{Generalizable}{\text{stakeDelegs}}}}\, \\ \,\href{Ledger.Conway.Specification.Certs.html#7428}{\htmlId{12431}{\htmlClass{Generalizable}{\text{rewards}}}}\, \end{pmatrix} \\ \,\href{Ledger.Conway.Specification.Certs.html#8151}{\htmlId{12443}{\htmlClass{Generalizable}{\text{stᵖ}}}}\, \\ \,\href{Ledger.Conway.Specification.Certs.html#8131}{\htmlId{12449}{\htmlClass{Generalizable}{\text{stᵍ}}}}\, \end{pmatrix}$ ⇀⦇ _ ,POST-CERT⦈ $\begin{pmatrix} \begin{pmatrix} \,\href{Ledger.Conway.Specification.Certs.html#7575}{\htmlId{12476}{\htmlClass{Generalizable}{\text{voteDelegs}}}}\, \,\href{Axiom.Set.Map.html#17775}{\htmlId{12487}{\htmlClass{Function Operator}{\text{∣\^{}}}}}\, \,\href{Ledger.Conway.Specification.Certs.html#12220}{\htmlId{12490}{\htmlClass{Bound}{\text{activeVDelegs}}}}\, \\ \,\href{Ledger.Conway.Specification.Certs.html#7499}{\htmlId{12506}{\htmlClass{Generalizable}{\text{stakeDelegs}}}}\, \\ \,\href{Ledger.Conway.Specification.Certs.html#7428}{\htmlId{12520}{\htmlClass{Generalizable}{\text{rewards}}}}\, \end{pmatrix} \\ \,\href{Ledger.Conway.Specification.Certs.html#8151}{\htmlId{12532}{\htmlClass{Generalizable}{\text{stᵖ}}}}\, \\ \,\href{Ledger.Conway.Specification.Certs.html#8131}{\htmlId{12538}{\htmlClass{Generalizable}{\text{stᵍ}}}}\, \end{pmatrix}$

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