{-# OPTIONS --safe #-}

open import Ledger.Dijkstra.Specification.Gov.Base using (GovStructure)

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

open import Ledger.Prelude renaming (filterˢ to filter)
open import Ledger.Prelude.Numeric.UnitInterval
open import Ledger.Dijkstra.Specification.Gov.Actions gs hiding (yes; no)
open import Ledger.Dijkstra.Specification.Account gs
open RewardAddress
open PParams


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

-- Miscellaneous Type Aliases

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

-- Delegation Definitions
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

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

-- Certification Types
record CertEnv : Type where
  field
    epoch           : Epoch
    pp              : PParams
    votes           : List GovVote
    wdrls           : Withdrawals
    coldCreds       : ℙ Credential
    directDeposits  : DirectDeposits

record DState : Type where
  constructor ⟦_,_,_,_⟧ᵈ
  field
    voteDelegs   : VoteDelegs
    stakeDelegs  : StakeDelegs
    rewards      : Rewards
    deposits     : Credential ⇀ Coin

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

record GState : Type where
  constructor ⟦_,_,_⟧ᵛ
  field
    dreps      : DReps
    ccHotKeys  : Credential ⇀ Maybe Credential
    deposits   : Credential ⇀ Coin

record CertState : Type where
  constructor ⟦_,_,_⟧ᶜˢ
  field
    dState : DState
    pState : PState
    gState : GState

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


record HasDeposits (A : Type) {K : Type} : Type where
  field DepositsOf : A → K ⇀ Coin
open HasDeposits ⦃...⦄ public

record HasCCHotKeys {a} (A : Type a) : Type a where
  field CCHotKeysOf : A → CCHotKeys
open HasCCHotKeys ⦃...⦄ public

record HasPools {a} (A : Type a) : Type a where
  field PoolsOf : A → Pools
open HasPools ⦃...⦄ public

record HasRetiring {a} (A : Type a) : Type a where
  field RetiringOf : A → Retiring
open HasRetiring ⦃...⦄ public

record HasRewards {a} (A : Type a) : Type a where
  field RewardsOf : A → Rewards
open HasRewards ⦃...⦄ public

record HasStake {a} (A : Type a) : Type a where
  field StakeOf : A -> Stake
open HasStake ⦃...⦄ public

record HasStakeDelegs {a} (A : Type a) : Type a where
  field StakeDelegsOf : A -> StakeDelegs
open HasStakeDelegs ⦃...⦄ public

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

  HasDeposits-DState : HasDeposits DState
  HasDeposits-DState .DepositsOf = DState.deposits

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

  HasDeposits-PState : HasDeposits PState
  HasDeposits-PState .DepositsOf = PState.deposits

  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

  HasDeposits-GState : HasDeposits GState
  HasDeposits-GState .DepositsOf = GState.deposits

  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

  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
  dd                     : DirectDeposits
  A                      : Type
  deposits deposits'     : A ⇀ Coin

  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


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

applyDirectDeposits : DirectDeposits → DState → DState
applyDirectDeposits dd ds = record ds { rewards = RewardsOf ds ∪⁺ dd }


applyWithdrawals : Withdrawals → Rewards → Rewards
applyWithdrawals wdrls rwds =
  foldl applyOne rwds (setToList (wdrls ˢ))
  where
    -- For each withdrawal entry `(addr, amt)`, look up `stake addr` in the acc,
    -- compute `bal ∸ amt`, create a singleton map with the new balance, and
    -- merge it with the rest (complement-restricted, to remove the old entry).
    applyOne : Rewards → RewardAddress × Coin → Rewards
    applyOne acc (addr , amt) =
      case lookupᵐ? acc (stake addr) of λ where
        (just bal) → ❴ stake addr , bal ∸ amt ❵ ∪ˡ (acc ∣ ❴ stake addr ❵ ᶜ)
        nothing    → acc
        -- `nothing` case is defensive; the PRE-CERT precondition guarantees the
        -- credential is registered, but handling it makes the function total.


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

  unquoteDecl DecEq-StakePoolParams = derive-DecEq
    ((quote StakePoolParams , DecEq-StakePoolParams) ∷ [])
  unquoteDecl DecEq-DCert = derive-DecEq
    ((quote DCert , DecEq-DCert) ∷ [])


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

  DELEG-delegate :
    ∙ (c ∉ dom rwds → d ≡ pp .keyDeposit)
    ∙ (c ∈ dom rwds → d ≡ )
    ∙ mvd ∈ mapˢ (just ∘ vDelegCredential) delegatees ∪
            fromList ( nothing ∷ just vDelegAbstain ∷ just vDelegNoConfidence ∷ [] )
    ∙ mkh ∈ mapˢ just (dom pools) ∪ ❴ nothing ❵
      ────────────────────────────────
      $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Certs.html#7228}{\htmlId{9072}{\htmlClass{Generalizable}{\text{pp}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#6666}{\htmlId{9077}{\htmlClass{Generalizable}{\text{pools}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#7040}{\htmlId{9085}{\htmlClass{Generalizable}{\text{delegatees}}}}\, \end{pmatrix}$ ⊢ $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Certs.html#6628}{\htmlId{9102}{\htmlClass{Generalizable}{\text{vDelegs}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#6552}{\htmlId{9112}{\htmlClass{Generalizable}{\text{sDelegs}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#6484}{\htmlId{9122}{\htmlClass{Generalizable}{\text{rwds}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#6848}{\htmlId{9129}{\htmlClass{Generalizable}{\text{deposits}}}}\, \end{pmatrix}$ ⇀⦇ delegate c mvd mkh d ,DELEG⦈ $\begin{pmatrix} \,\href{Axiom.Set.Map.html#9262}{\htmlId{9174}{\htmlClass{Function}{\text{insertIfJust}}}}\, \,\href{Ledger.Dijkstra.Specification.Certs.html#6980}{\htmlId{9187}{\htmlClass{Generalizable}{\text{c}}}}\, \,\href{Ledger.Dijkstra.Specification.Certs.html#7252}{\htmlId{9189}{\htmlClass{Generalizable}{\text{mvd}}}}\, \,\href{Ledger.Dijkstra.Specification.Certs.html#6628}{\htmlId{9193}{\htmlClass{Generalizable}{\text{vDelegs}}}}\, \\ \,\href{Axiom.Set.Map.html#9262}{\htmlId{9203}{\htmlClass{Function}{\text{insertIfJust}}}}\, \,\href{Ledger.Dijkstra.Specification.Certs.html#6980}{\htmlId{9216}{\htmlClass{Generalizable}{\text{c}}}}\, \,\href{Ledger.Dijkstra.Specification.Certs.html#7166}{\htmlId{9218}{\htmlClass{Generalizable}{\text{mkh}}}}\, \,\href{Ledger.Dijkstra.Specification.Certs.html#6552}{\htmlId{9222}{\htmlClass{Generalizable}{\text{sDelegs}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#6484}{\htmlId{9232}{\htmlClass{Generalizable}{\text{rwds}}}}\, \,\href{Axiom.Set.Map.html#7640}{\htmlId{9237}{\htmlClass{Function Operator}{\text{∪ˡ}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{9240}{\htmlClass{Field Operator}{\text{❴}}}}\, \,\href{Ledger.Dijkstra.Specification.Certs.html#6980}{\htmlId{9242}{\htmlClass{Generalizable}{\text{c}}}}\, , \,\htmlId{9246}{\htmlClass{Number}{\text{0}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{9248}{\htmlClass{Field Operator}{\text{❵}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#6848}{\htmlId{9252}{\htmlClass{Generalizable}{\text{deposits}}}}\, \,\href{Axiom.Set.Map.Dec.html#2149}{\htmlId{9261}{\htmlClass{Function Operator}{\text{∪⁺}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{9264}{\htmlClass{Field Operator}{\text{❴}}}}\, \,\href{Ledger.Dijkstra.Specification.Certs.html#6980}{\htmlId{9266}{\htmlClass{Generalizable}{\text{c}}}}\, , \,\href{Ledger.Dijkstra.Specification.Certs.html#6932}{\htmlId{9270}{\htmlClass{Generalizable}{\text{d}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{9272}{\htmlClass{Field Operator}{\text{❵}}}}\, \end{pmatrix}$

  DELEG-dereg :
    ∙ (c , ) ∈ rwds
    ∙ (c , d) ∈ deposits
    ∙ md ≡ nothing ⊎ md ≡ just d
      ────────────────────────────────
      $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Certs.html#7228}{\htmlId{9419}{\htmlClass{Generalizable}{\text{pp}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#6666}{\htmlId{9424}{\htmlClass{Generalizable}{\text{pools}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#7040}{\htmlId{9432}{\htmlClass{Generalizable}{\text{delegatees}}}}\, \end{pmatrix}$ ⊢ $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Certs.html#6628}{\htmlId{9449}{\htmlClass{Generalizable}{\text{vDelegs}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#6552}{\htmlId{9459}{\htmlClass{Generalizable}{\text{sDelegs}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#6484}{\htmlId{9469}{\htmlClass{Generalizable}{\text{rwds}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#6848}{\htmlId{9476}{\htmlClass{Generalizable}{\text{deposits}}}}\, \end{pmatrix}$ ⇀⦇ dereg c md ,DELEG⦈ $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Certs.html#6628}{\htmlId{9511}{\htmlClass{Generalizable}{\text{vDelegs}}}}\, \,\href{Axiom.Set.Map.html#13606}{\htmlId{9519}{\htmlClass{Function Operator}{\text{∣}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{9521}{\htmlClass{Field Operator}{\text{❴}}}}\, \,\href{Ledger.Dijkstra.Specification.Certs.html#6980}{\htmlId{9523}{\htmlClass{Generalizable}{\text{c}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{9525}{\htmlClass{Field Operator}{\text{❵}}}}\, \,\href{Axiom.Set.Map.html#13606}{\htmlId{9527}{\htmlClass{Function Operator}{\text{ᶜ}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#6552}{\htmlId{9531}{\htmlClass{Generalizable}{\text{sDelegs}}}}\, \,\href{Axiom.Set.Map.html#13606}{\htmlId{9539}{\htmlClass{Function Operator}{\text{∣}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{9541}{\htmlClass{Field Operator}{\text{❴}}}}\, \,\href{Ledger.Dijkstra.Specification.Certs.html#6980}{\htmlId{9543}{\htmlClass{Generalizable}{\text{c}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{9545}{\htmlClass{Field Operator}{\text{❵}}}}\, \,\href{Axiom.Set.Map.html#13606}{\htmlId{9547}{\htmlClass{Function Operator}{\text{ᶜ}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#6484}{\htmlId{9551}{\htmlClass{Generalizable}{\text{rwds}}}}\, \,\href{Axiom.Set.Map.html#13606}{\htmlId{9556}{\htmlClass{Function Operator}{\text{∣}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{9558}{\htmlClass{Field Operator}{\text{❴}}}}\, \,\href{Ledger.Dijkstra.Specification.Certs.html#6980}{\htmlId{9560}{\htmlClass{Generalizable}{\text{c}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{9562}{\htmlClass{Field Operator}{\text{❵}}}}\, \,\href{Axiom.Set.Map.html#13606}{\htmlId{9564}{\htmlClass{Function Operator}{\text{ᶜ}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#6848}{\htmlId{9568}{\htmlClass{Generalizable}{\text{deposits}}}}\, \,\href{Axiom.Set.Map.html#13606}{\htmlId{9577}{\htmlClass{Function Operator}{\text{∣}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{9579}{\htmlClass{Field Operator}{\text{❴}}}}\, \,\href{Ledger.Dijkstra.Specification.Certs.html#6980}{\htmlId{9581}{\htmlClass{Generalizable}{\text{c}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{9583}{\htmlClass{Field Operator}{\text{❵}}}}\, \,\href{Axiom.Set.Map.html#13606}{\htmlId{9585}{\htmlClass{Function Operator}{\text{ᶜ}}}}\, \end{pmatrix}$


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

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

  POOL-reg :
    ∙ Is-nothing (isPoolRegistered pools kh)
    ────────────────────────────────
    pp ⊢ $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Certs.html#6666}{\htmlId{9907}{\htmlClass{Generalizable}{\text{pools}}}}\,
         \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#6672}{\htmlId{9924}{\htmlClass{Generalizable}{\text{fPools}}}}\,
         \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#6699}{\htmlId{9942}{\htmlClass{Generalizable}{\text{retiring}}}}\,
         \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#6848}{\htmlId{9962}{\htmlClass{Generalizable}{\text{deposits}}}}\,
         \end{pmatrix}$ ⇀⦇ regpool kh poolParams ,POOL⦈ $\begin{pmatrix}
           \,\href{Ledger.Dijkstra.Specification.Certs.html#6666}{\htmlId{10027}{\htmlClass{Generalizable}{\text{pools}}}}\, \,\href{Axiom.Set.Map.html#7640}{\htmlId{10033}{\htmlClass{Function Operator}{\text{∪ˡ}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{10036}{\htmlClass{Field Operator}{\text{❴}}}}\, \,\href{Ledger.Dijkstra.Specification.Certs.html#7142}{\htmlId{10038}{\htmlClass{Generalizable}{\text{kh}}}}\, , \,\href{Ledger.Dijkstra.Specification.Certs.html#7196}{\htmlId{10043}{\htmlClass{Generalizable}{\text{poolParams}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{10054}{\htmlClass{Field Operator}{\text{❵}}}}\,
         \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#6672}{\htmlId{10067}{\htmlClass{Generalizable}{\text{fPools}}}}\,
         \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#6699}{\htmlId{10085}{\htmlClass{Generalizable}{\text{retiring}}}}\,
         \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#6848}{\htmlId{10105}{\htmlClass{Generalizable}{\text{deposits}}}}\, \,\href{Axiom.Set.Map.html#7640}{\htmlId{10114}{\htmlClass{Function Operator}{\text{∪ˡ}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{10117}{\htmlClass{Field Operator}{\text{❴}}}}\, \,\href{Ledger.Dijkstra.Specification.Certs.html#7142}{\htmlId{10119}{\htmlClass{Generalizable}{\text{kh}}}}\, , \,\href{Ledger.Dijkstra.Specification.Certs.html#7228}{\htmlId{10124}{\htmlClass{Generalizable}{\text{pp}}}}\, \,\htmlId{10127}{\htmlClass{Symbol}{\text{.}}}\,\,\href{Ledger.Dijkstra.Specification.PParams.html#2442}{\htmlId{10128}{\htmlClass{Field}{\text{poolDeposit}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{10140}{\htmlClass{Field Operator}{\text{❵}}}}\,
         \end{pmatrix}$

  POOL-rereg :
    ∙ Is-just (isPoolRegistered pools kh)
    ────────────────────────────────
    pp ⊢ $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Certs.html#6666}{\htmlId{10259}{\htmlClass{Generalizable}{\text{pools}}}}\,
         \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#6672}{\htmlId{10276}{\htmlClass{Generalizable}{\text{fPools}}}}\,
         \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#6699}{\htmlId{10294}{\htmlClass{Generalizable}{\text{retiring}}}}\,
         \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#6848}{\htmlId{10314}{\htmlClass{Generalizable}{\text{deposits}}}}\,
         \end{pmatrix}$ ⇀⦇ regpool kh poolParams ,POOL⦈ $\begin{pmatrix}
           \,\href{Ledger.Dijkstra.Specification.Certs.html#6666}{\htmlId{10379}{\htmlClass{Generalizable}{\text{pools}}}}\,
         \\ \,\href{Class.HasSingleton.html#288}{\htmlId{10396}{\htmlClass{Field Operator}{\text{❴}}}}\, \,\href{Ledger.Dijkstra.Specification.Certs.html#7142}{\htmlId{10398}{\htmlClass{Generalizable}{\text{kh}}}}\, , \,\href{Ledger.Dijkstra.Specification.Certs.html#7196}{\htmlId{10403}{\htmlClass{Generalizable}{\text{poolParams}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{10414}{\htmlClass{Field Operator}{\text{❵}}}}\, \,\href{Axiom.Set.Map.html#7640}{\htmlId{10416}{\htmlClass{Function Operator}{\text{∪ˡ}}}}\, \,\href{Ledger.Dijkstra.Specification.Certs.html#6672}{\htmlId{10419}{\htmlClass{Generalizable}{\text{fPools}}}}\,
         \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#6699}{\htmlId{10437}{\htmlClass{Generalizable}{\text{retiring}}}}\, \,\href{Axiom.Set.Map.html#13606}{\htmlId{10446}{\htmlClass{Function Operator}{\text{∣}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{10448}{\htmlClass{Field Operator}{\text{❴}}}}\, \,\href{Ledger.Dijkstra.Specification.Certs.html#7142}{\htmlId{10450}{\htmlClass{Generalizable}{\text{kh}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{10453}{\htmlClass{Field Operator}{\text{❵}}}}\, \,\href{Axiom.Set.Map.html#13606}{\htmlId{10455}{\htmlClass{Function Operator}{\text{ᶜ}}}}\,
         \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#6848}{\htmlId{10468}{\htmlClass{Generalizable}{\text{deposits}}}}\,
         \end{pmatrix}$

  POOL-retirepool :
    ────────────────────────────────
    pp ⊢ $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Certs.html#6666}{\htmlId{10557}{\htmlClass{Generalizable}{\text{pools}}}}\,
         \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#6672}{\htmlId{10574}{\htmlClass{Generalizable}{\text{fPools}}}}\,
         \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#6699}{\htmlId{10592}{\htmlClass{Generalizable}{\text{retiring}}}}\,
         \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#6848}{\htmlId{10612}{\htmlClass{Generalizable}{\text{deposits}}}}\,
         \end{pmatrix}$ ⇀⦇ retirepool kh e ,POOL⦈ $\begin{pmatrix}
           \,\href{Ledger.Dijkstra.Specification.Certs.html#6666}{\htmlId{10671}{\htmlClass{Generalizable}{\text{pools}}}}\,
         \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#6672}{\htmlId{10688}{\htmlClass{Generalizable}{\text{fPools}}}}\,
         \\ \,\href{Class.HasSingleton.html#288}{\htmlId{10706}{\htmlClass{Field Operator}{\text{❴}}}}\, \,\href{Ledger.Dijkstra.Specification.Certs.html#7142}{\htmlId{10708}{\htmlClass{Generalizable}{\text{kh}}}}\, , \,\href{Ledger.Dijkstra.Specification.Certs.html#7091}{\htmlId{10713}{\htmlClass{Generalizable}{\text{e}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{10715}{\htmlClass{Field Operator}{\text{❵}}}}\, \,\href{Axiom.Set.Map.html#7640}{\htmlId{10717}{\htmlClass{Function Operator}{\text{∪ˡ}}}}\, \,\href{Ledger.Dijkstra.Specification.Certs.html#6699}{\htmlId{10720}{\htmlClass{Generalizable}{\text{retiring}}}}\,
         \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#6848}{\htmlId{10740}{\htmlClass{Generalizable}{\text{deposits}}}}\,
         \end{pmatrix}$


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

  GOVCERT-regdrep :
    ∙ (d ≡ pp .drepDeposit × c ∉ dom dReps) ⊎ (d ≡  × c ∈ dom dReps)
      ────────────────────────────────
      $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Certs.html#7091}{\htmlId{11013}{\htmlClass{Generalizable}{\text{e}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#7228}{\htmlId{11017}{\htmlClass{Generalizable}{\text{pp}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#7113}{\htmlId{11022}{\htmlClass{Generalizable}{\text{vs}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#6735}{\htmlId{11027}{\htmlClass{Generalizable}{\text{wdrls}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#7342}{\htmlId{11035}{\htmlClass{Generalizable}{\text{cc}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#6774}{\htmlId{11040}{\htmlClass{Generalizable}{\text{dd}}}}\, \end{pmatrix}$ ⊢ $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Certs.html#6519}{\htmlId{11049}{\htmlClass{Generalizable}{\text{dReps}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#6591}{\htmlId{11057}{\htmlClass{Generalizable}{\text{ccKeys}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#6848}{\htmlId{11066}{\htmlClass{Generalizable}{\text{deposits}}}}\, \end{pmatrix}$ ⇀⦇ regdrep c d an ,GOVCERT⦈ $\begin{pmatrix} \,\href{Class.HasSingleton.html#288}{\htmlId{11107}{\htmlClass{Field Operator}{\text{❴}}}}\, \,\href{Ledger.Dijkstra.Specification.Certs.html#6980}{\htmlId{11109}{\htmlClass{Generalizable}{\text{c}}}}\, , \,\href{Ledger.Dijkstra.Specification.Certs.html#7091}{\htmlId{11113}{\htmlClass{Generalizable}{\text{e}}}}\, \,\href{Class.HasAdd.Core.html#162}{\htmlId{11115}{\htmlClass{Field Operator}{\text{+}}}}\, \,\href{Ledger.Dijkstra.Specification.Certs.html#7228}{\htmlId{11117}{\htmlClass{Generalizable}{\text{pp}}}}\, \,\htmlId{11120}{\htmlClass{Symbol}{\text{.}}}\,\,\href{Ledger.Dijkstra.Specification.PParams.html#3572}{\htmlId{11121}{\htmlClass{Field}{\text{drepActivity}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{11134}{\htmlClass{Field Operator}{\text{❵}}}}\, \,\href{Axiom.Set.Map.html#7640}{\htmlId{11136}{\htmlClass{Function Operator}{\text{∪ˡ}}}}\, \,\href{Ledger.Dijkstra.Specification.Certs.html#6519}{\htmlId{11139}{\htmlClass{Generalizable}{\text{dReps}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#6591}{\htmlId{11147}{\htmlClass{Generalizable}{\text{ccKeys}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#6848}{\htmlId{11156}{\htmlClass{Generalizable}{\text{deposits}}}}\, \,\href{Axiom.Set.Map.Dec.html#2149}{\htmlId{11165}{\htmlClass{Function Operator}{\text{∪⁺}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{11168}{\htmlClass{Field Operator}{\text{❴}}}}\, \,\href{Ledger.Dijkstra.Specification.Certs.html#6980}{\htmlId{11170}{\htmlClass{Generalizable}{\text{c}}}}\, , \,\href{Ledger.Dijkstra.Specification.Certs.html#6932}{\htmlId{11174}{\htmlClass{Generalizable}{\text{d}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{11176}{\htmlClass{Field Operator}{\text{❵}}}}\, \end{pmatrix}$

  GOVCERT-deregdrep :
    ∙ c ∈ dom dReps
    ∙ (c , d) ∈ deposits
      ────────────────────────────────
      $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Certs.html#7091}{\htmlId{11295}{\htmlClass{Generalizable}{\text{e}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#7228}{\htmlId{11299}{\htmlClass{Generalizable}{\text{pp}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#7113}{\htmlId{11304}{\htmlClass{Generalizable}{\text{vs}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#6735}{\htmlId{11309}{\htmlClass{Generalizable}{\text{wdrls}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#7342}{\htmlId{11317}{\htmlClass{Generalizable}{\text{cc}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#6774}{\htmlId{11322}{\htmlClass{Generalizable}{\text{dd}}}}\, \end{pmatrix}$ ⊢ $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Certs.html#6519}{\htmlId{11331}{\htmlClass{Generalizable}{\text{dReps}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#6591}{\htmlId{11339}{\htmlClass{Generalizable}{\text{ccKeys}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#6848}{\htmlId{11348}{\htmlClass{Generalizable}{\text{deposits}}}}\, \end{pmatrix}$ ⇀⦇ deregdrep c d ,GOVCERT⦈ $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Certs.html#6519}{\htmlId{11388}{\htmlClass{Generalizable}{\text{dReps}}}}\, \,\href{Axiom.Set.Map.html#13606}{\htmlId{11394}{\htmlClass{Function Operator}{\text{∣}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{11396}{\htmlClass{Field Operator}{\text{❴}}}}\, \,\href{Ledger.Dijkstra.Specification.Certs.html#6980}{\htmlId{11398}{\htmlClass{Generalizable}{\text{c}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{11400}{\htmlClass{Field Operator}{\text{❵}}}}\, \,\href{Axiom.Set.Map.html#13606}{\htmlId{11402}{\htmlClass{Function Operator}{\text{ᶜ}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#6591}{\htmlId{11406}{\htmlClass{Generalizable}{\text{ccKeys}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#6848}{\htmlId{11415}{\htmlClass{Generalizable}{\text{deposits}}}}\, \,\href{Axiom.Set.Map.html#13606}{\htmlId{11424}{\htmlClass{Function Operator}{\text{∣}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{11426}{\htmlClass{Field Operator}{\text{❴}}}}\, \,\href{Ledger.Dijkstra.Specification.Certs.html#6980}{\htmlId{11428}{\htmlClass{Generalizable}{\text{c}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{11430}{\htmlClass{Field Operator}{\text{❵}}}}\, \,\href{Axiom.Set.Map.html#13606}{\htmlId{11432}{\htmlClass{Function Operator}{\text{ᶜ}}}}\, \end{pmatrix}$

  GOVCERT-ccreghot :
    ∙ (c , nothing) ∉ ccKeys
    ∙ c ∈ cc
      ────────────────────────────────
      $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Certs.html#7091}{\htmlId{11547}{\htmlClass{Generalizable}{\text{e}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#7228}{\htmlId{11551}{\htmlClass{Generalizable}{\text{pp}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#7113}{\htmlId{11556}{\htmlClass{Generalizable}{\text{vs}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#6735}{\htmlId{11561}{\htmlClass{Generalizable}{\text{wdrls}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#7342}{\htmlId{11569}{\htmlClass{Generalizable}{\text{cc}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#6774}{\htmlId{11574}{\htmlClass{Generalizable}{\text{dd}}}}\, \end{pmatrix}$ ⊢ $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Certs.html#6519}{\htmlId{11583}{\htmlClass{Generalizable}{\text{dReps}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#6591}{\htmlId{11591}{\htmlClass{Generalizable}{\text{ccKeys}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#6848}{\htmlId{11600}{\htmlClass{Generalizable}{\text{deposits}}}}\, \end{pmatrix}$ ⇀⦇ ccreghot c mc ,GOVCERT⦈ $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Certs.html#6519}{\htmlId{11640}{\htmlClass{Generalizable}{\text{dReps}}}}\, \\ \,\href{Class.HasSingleton.html#288}{\htmlId{11648}{\htmlClass{Field Operator}{\text{❴}}}}\, \,\href{Ledger.Dijkstra.Specification.Certs.html#6980}{\htmlId{11650}{\htmlClass{Generalizable}{\text{c}}}}\, , \,\href{Ledger.Dijkstra.Specification.Certs.html#7007}{\htmlId{11654}{\htmlClass{Generalizable}{\text{mc}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{11657}{\htmlClass{Field Operator}{\text{❵}}}}\, \,\href{Axiom.Set.Map.html#7640}{\htmlId{11659}{\htmlClass{Function Operator}{\text{∪ˡ}}}}\, \,\href{Ledger.Dijkstra.Specification.Certs.html#6591}{\htmlId{11662}{\htmlClass{Generalizable}{\text{ccKeys}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#6848}{\htmlId{11671}{\htmlClass{Generalizable}{\text{deposits}}}}\, \end{pmatrix}$

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

  CERT-deleg :
    ∙ $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Certs.html#7228}{\htmlId{11811}{\htmlClass{Generalizable}{\text{pp}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#2239}{\htmlId{11816}{\htmlClass{Field}{\text{PState.pools}}}}\, \,\href{Ledger.Dijkstra.Specification.Certs.html#7322}{\htmlId{11829}{\htmlClass{Generalizable}{\text{stᵖ}}}}\, \\ \,\href{Class.IsSet.html#916}{\htmlId{11835}{\htmlClass{Function}{\text{dom}}}}\, \,\htmlId{11839}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Dijkstra.Specification.Certs.html#2405}{\htmlId{11840}{\htmlClass{Field}{\text{GState.dreps}}}}\, \,\href{Ledger.Dijkstra.Specification.Certs.html#7302}{\htmlId{11853}{\htmlClass{Generalizable}{\text{stᵍ}}}}\,\,\htmlId{11856}{\htmlClass{Symbol}{\text{)}}}\, \end{pmatrix}$ ⊢ stᵈ ⇀⦇ dCert ,DELEG⦈ stᵈ'
      ────────────────────────────────
      $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Certs.html#7091}{\htmlId{11935}{\htmlClass{Generalizable}{\text{e}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#7228}{\htmlId{11939}{\htmlClass{Generalizable}{\text{pp}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#7113}{\htmlId{11944}{\htmlClass{Generalizable}{\text{vs}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#6735}{\htmlId{11949}{\htmlClass{Generalizable}{\text{wdrls}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#7342}{\htmlId{11957}{\htmlClass{Generalizable}{\text{cc}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#6774}{\htmlId{11962}{\htmlClass{Generalizable}{\text{dd}}}}\, \end{pmatrix}$ ⊢ $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Certs.html#7282}{\htmlId{11971}{\htmlClass{Generalizable}{\text{stᵈ}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#7322}{\htmlId{11977}{\htmlClass{Generalizable}{\text{stᵖ}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#7302}{\htmlId{11983}{\htmlClass{Generalizable}{\text{stᵍ}}}}\, \end{pmatrix}$ ⇀⦇ dCert ,CERT⦈ $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Certs.html#7286}{\htmlId{12007}{\htmlClass{Generalizable}{\text{stᵈ'}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#7322}{\htmlId{12014}{\htmlClass{Generalizable}{\text{stᵖ}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#7302}{\htmlId{12020}{\htmlClass{Generalizable}{\text{stᵍ}}}}\, \end{pmatrix}$

  CERT-pool :
    ∙ pp ⊢ stᵖ ⇀⦇ dCert ,POOL⦈ stᵖ'
      ────────────────────────────────
      $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Certs.html#7091}{\htmlId{12124}{\htmlClass{Generalizable}{\text{e}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#7228}{\htmlId{12128}{\htmlClass{Generalizable}{\text{pp}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#7113}{\htmlId{12133}{\htmlClass{Generalizable}{\text{vs}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#6735}{\htmlId{12138}{\htmlClass{Generalizable}{\text{wdrls}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#7342}{\htmlId{12146}{\htmlClass{Generalizable}{\text{cc}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#6774}{\htmlId{12151}{\htmlClass{Generalizable}{\text{dd}}}}\, \end{pmatrix}$ ⊢ $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Certs.html#7282}{\htmlId{12160}{\htmlClass{Generalizable}{\text{stᵈ}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#7322}{\htmlId{12166}{\htmlClass{Generalizable}{\text{stᵖ}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#7302}{\htmlId{12172}{\htmlClass{Generalizable}{\text{stᵍ}}}}\, \end{pmatrix}$ ⇀⦇ dCert ,CERT⦈ $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Certs.html#7282}{\htmlId{12196}{\htmlClass{Generalizable}{\text{stᵈ}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#7326}{\htmlId{12202}{\htmlClass{Generalizable}{\text{stᵖ'}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#7302}{\htmlId{12209}{\htmlClass{Generalizable}{\text{stᵍ}}}}\, \end{pmatrix}$

  CERT-gov :
    ∙ Γ ⊢ stᵍ ⇀⦇ dCert ,GOVCERT⦈ stᵍ'
      ────────────────────────────────
      Γ ⊢ $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Certs.html#7282}{\htmlId{12318}{\htmlClass{Generalizable}{\text{stᵈ}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#7322}{\htmlId{12324}{\htmlClass{Generalizable}{\text{stᵖ}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#7302}{\htmlId{12330}{\htmlClass{Generalizable}{\text{stᵍ}}}}\, \end{pmatrix}$ ⇀⦇ dCert ,CERT⦈ $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Certs.html#7282}{\htmlId{12354}{\htmlClass{Generalizable}{\text{stᵈ}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#7322}{\htmlId{12360}{\htmlClass{Generalizable}{\text{stᵖ}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#7306}{\htmlId{12366}{\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
    ∙ wdrlCreds ⊆ dom rewards
    ∙ ∀[ (addr , amt) ∈ wdrls ˢ ] amt ≤ maybe id  (lookupᵐ? rewards (stake addr))
      ────────────────────────────────
      $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Certs.html#7091}{\htmlId{12924}{\htmlClass{Generalizable}{\text{e}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#7228}{\htmlId{12928}{\htmlClass{Generalizable}{\text{pp}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#7113}{\htmlId{12933}{\htmlClass{Generalizable}{\text{vs}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#6735}{\htmlId{12938}{\htmlClass{Generalizable}{\text{wdrls}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#7342}{\htmlId{12946}{\htmlClass{Generalizable}{\text{cc}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#6774}{\htmlId{12951}{\htmlClass{Generalizable}{\text{dd}}}}\, \end{pmatrix}$ ⊢ $\begin{pmatrix} \begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Certs.html#6636}{\htmlId{12962}{\htmlClass{Generalizable}{\text{voteDelegs}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#6560}{\htmlId{12975}{\htmlClass{Generalizable}{\text{stakeDelegs}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#6489}{\htmlId{12989}{\htmlClass{Generalizable}{\text{rewards}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#6848}{\htmlId{12999}{\htmlClass{Generalizable}{\text{deposits}}}}\, \end{pmatrix} \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#7322}{\htmlId{13012}{\htmlClass{Generalizable}{\text{stᵖ}}}}\, \\ \begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Certs.html#6519}{\htmlId{13020}{\htmlClass{Generalizable}{\text{dReps}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#6598}{\htmlId{13028}{\htmlClass{Generalizable}{\text{ccHotKeys}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#6857}{\htmlId{13040}{\htmlClass{Generalizable}{\text{deposits'}}}}\, \end{pmatrix} \end{pmatrix}$ ⇀⦇ _ ,PRE-CERT⦈ $\begin{pmatrix} \begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Certs.html#6636}{\htmlId{13074}{\htmlClass{Generalizable}{\text{voteDelegs}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#6560}{\htmlId{13087}{\htmlClass{Generalizable}{\text{stakeDelegs}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#7566}{\htmlId{13101}{\htmlClass{Function}{\text{applyWithdrawals}}}}\, \,\href{Ledger.Dijkstra.Specification.Certs.html#6735}{\htmlId{13118}{\htmlClass{Generalizable}{\text{wdrls}}}}\, \,\href{Ledger.Dijkstra.Specification.Certs.html#6489}{\htmlId{13124}{\htmlClass{Generalizable}{\text{rewards}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#6848}{\htmlId{13134}{\htmlClass{Generalizable}{\text{deposits}}}}\, \end{pmatrix} \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#7322}{\htmlId{13147}{\htmlClass{Generalizable}{\text{stᵖ}}}}\, \\ \begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Certs.html#12576}{\htmlId{13155}{\htmlClass{Bound}{\text{refreshedDReps}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#6598}{\htmlId{13172}{\htmlClass{Generalizable}{\text{ccHotKeys}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#6857}{\htmlId{13184}{\htmlClass{Generalizable}{\text{deposits'}}}}\, \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
    ∙ dom dd ⊆ dom rewards
      ────────────────────────────────
      $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Certs.html#7091}{\htmlId{13515}{\htmlClass{Generalizable}{\text{e}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#7228}{\htmlId{13519}{\htmlClass{Generalizable}{\text{pp}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#7113}{\htmlId{13524}{\htmlClass{Generalizable}{\text{vs}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#6735}{\htmlId{13529}{\htmlClass{Generalizable}{\text{wdrls}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#7342}{\htmlId{13537}{\htmlClass{Generalizable}{\text{cc}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#6774}{\htmlId{13542}{\htmlClass{Generalizable}{\text{dd}}}}\, \end{pmatrix}$ ⊢ $\begin{pmatrix} \begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Certs.html#6636}{\htmlId{13553}{\htmlClass{Generalizable}{\text{voteDelegs}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#6560}{\htmlId{13566}{\htmlClass{Generalizable}{\text{stakeDelegs}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#6489}{\htmlId{13580}{\htmlClass{Generalizable}{\text{rewards}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#6848}{\htmlId{13590}{\htmlClass{Generalizable}{\text{deposits}}}}\, \end{pmatrix} \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#7322}{\htmlId{13603}{\htmlClass{Generalizable}{\text{stᵖ}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#7302}{\htmlId{13609}{\htmlClass{Generalizable}{\text{stᵍ}}}}\, \end{pmatrix}$ ⇀⦇ _ ,POST-CERT⦈ $\begin{pmatrix} \begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Certs.html#6636}{\htmlId{13636}{\htmlClass{Generalizable}{\text{voteDelegs}}}}\, \,\href{Axiom.Set.Map.html#17775}{\htmlId{13647}{\htmlClass{Function Operator}{\text{∣\^{}}}}}\, \,\href{Ledger.Dijkstra.Specification.Certs.html#13298}{\htmlId{13650}{\htmlClass{Bound}{\text{activeVDelegs}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#6560}{\htmlId{13666}{\htmlClass{Generalizable}{\text{stakeDelegs}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#6489}{\htmlId{13680}{\htmlClass{Generalizable}{\text{rewards}}}}\, \,\href{Axiom.Set.Map.Dec.html#2149}{\htmlId{13688}{\htmlClass{Function Operator}{\text{∪⁺}}}}\, \,\href{Ledger.Dijkstra.Specification.Certs.html#6774}{\htmlId{13691}{\htmlClass{Generalizable}{\text{dd}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#6848}{\htmlId{13696}{\htmlClass{Generalizable}{\text{deposits}}}}\, \end{pmatrix} \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#7322}{\htmlId{13709}{\htmlClass{Generalizable}{\text{stᵖ}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#7302}{\htmlId{13715}{\htmlClass{Generalizable}{\text{stᵍ}}}}\, \end{pmatrix}$



-- CERTS Transition System --

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