Certificates

{-# 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

In the Dijkstra era, the Rewards map represents account balances, not just staking rewards. An account's balance may increase via staking rewards (at epoch boundaries) or via direct deposits (CIP-159). Withdrawals decrease the balance. The name Rewards is retained for backwards compatibility.

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

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
  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 }

The LEDGER rule will call applyDirectDeposits to credit direct deposits to account balances as part of processing a transaction batch.

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.

In the Dijkstra era, CIP-159 allows partial withdrawals: a transaction may withdraw any amount up to the current account balance. applyWithdrawals subtracts each withdrawal amount from the corresponding account balance. Full withdrawals remain valid as a special case (where the withdrawn amount equals the balance, leaving a zero balance).

The PRE-CERT rule calls applyWithdrawals to process withdrawals as part of certificate processing.

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

-- 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#7626}{\htmlId{10005}{\htmlClass{Generalizable}{\text{pp}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#7106}{\htmlId{10010}{\htmlClass{Generalizable}{\text{pools}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#7438}{\htmlId{10018}{\htmlClass{Generalizable}{\text{delegatees}}}}\, \end{pmatrix}$ ⊢ $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Certs.html#7068}{\htmlId{10035}{\htmlClass{Generalizable}{\text{vDelegs}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#6992}{\htmlId{10045}{\htmlClass{Generalizable}{\text{sDelegs}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#6924}{\htmlId{10055}{\htmlClass{Generalizable}{\text{rwds}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#7246}{\htmlId{10062}{\htmlClass{Generalizable}{\text{deposits}}}}\, \end{pmatrix}$ ⇀⦇ delegate c mvd mkh d ,DELEG⦈ $\begin{pmatrix} \,\href{Axiom.Set.Map.html#9262}{\htmlId{10107}{\htmlClass{Function}{\text{insertIfJust}}}}\, \,\href{Ledger.Dijkstra.Specification.Certs.html#7378}{\htmlId{10120}{\htmlClass{Generalizable}{\text{c}}}}\, \,\href{Ledger.Dijkstra.Specification.Certs.html#7650}{\htmlId{10122}{\htmlClass{Generalizable}{\text{mvd}}}}\, \,\href{Ledger.Dijkstra.Specification.Certs.html#7068}{\htmlId{10126}{\htmlClass{Generalizable}{\text{vDelegs}}}}\, \\ \,\href{Axiom.Set.Map.html#9262}{\htmlId{10136}{\htmlClass{Function}{\text{insertIfJust}}}}\, \,\href{Ledger.Dijkstra.Specification.Certs.html#7378}{\htmlId{10149}{\htmlClass{Generalizable}{\text{c}}}}\, \,\href{Ledger.Dijkstra.Specification.Certs.html#7564}{\htmlId{10151}{\htmlClass{Generalizable}{\text{mkh}}}}\, \,\href{Ledger.Dijkstra.Specification.Certs.html#6992}{\htmlId{10155}{\htmlClass{Generalizable}{\text{sDelegs}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#6924}{\htmlId{10165}{\htmlClass{Generalizable}{\text{rwds}}}}\, \,\href{Axiom.Set.Map.html#7640}{\htmlId{10170}{\htmlClass{Function Operator}{\text{∪ˡ}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{10173}{\htmlClass{Field Operator}{\text{❴}}}}\, \,\href{Ledger.Dijkstra.Specification.Certs.html#7378}{\htmlId{10175}{\htmlClass{Generalizable}{\text{c}}}}\, , \,\htmlId{10179}{\htmlClass{Number}{\text{0}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{10181}{\htmlClass{Field Operator}{\text{❵}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#7246}{\htmlId{10185}{\htmlClass{Generalizable}{\text{deposits}}}}\, \,\href{Axiom.Set.Map.Dec.html#2149}{\htmlId{10194}{\htmlClass{Function Operator}{\text{∪⁺}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{10197}{\htmlClass{Field Operator}{\text{❴}}}}\, \,\href{Ledger.Dijkstra.Specification.Certs.html#7378}{\htmlId{10199}{\htmlClass{Generalizable}{\text{c}}}}\, , \,\href{Ledger.Dijkstra.Specification.Certs.html#7330}{\htmlId{10203}{\htmlClass{Generalizable}{\text{d}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{10205}{\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#7626}{\htmlId{10352}{\htmlClass{Generalizable}{\text{pp}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#7106}{\htmlId{10357}{\htmlClass{Generalizable}{\text{pools}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#7438}{\htmlId{10365}{\htmlClass{Generalizable}{\text{delegatees}}}}\, \end{pmatrix}$ ⊢ $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Certs.html#7068}{\htmlId{10382}{\htmlClass{Generalizable}{\text{vDelegs}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#6992}{\htmlId{10392}{\htmlClass{Generalizable}{\text{sDelegs}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#6924}{\htmlId{10402}{\htmlClass{Generalizable}{\text{rwds}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#7246}{\htmlId{10409}{\htmlClass{Generalizable}{\text{deposits}}}}\, \end{pmatrix}$ ⇀⦇ dereg c md ,DELEG⦈ $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Certs.html#7068}{\htmlId{10444}{\htmlClass{Generalizable}{\text{vDelegs}}}}\, \,\href{Axiom.Set.Map.html#13606}{\htmlId{10452}{\htmlClass{Function Operator}{\text{∣}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{10454}{\htmlClass{Field Operator}{\text{❴}}}}\, \,\href{Ledger.Dijkstra.Specification.Certs.html#7378}{\htmlId{10456}{\htmlClass{Generalizable}{\text{c}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{10458}{\htmlClass{Field Operator}{\text{❵}}}}\, \,\href{Axiom.Set.Map.html#13606}{\htmlId{10460}{\htmlClass{Function Operator}{\text{ᶜ}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#6992}{\htmlId{10464}{\htmlClass{Generalizable}{\text{sDelegs}}}}\, \,\href{Axiom.Set.Map.html#13606}{\htmlId{10472}{\htmlClass{Function Operator}{\text{∣}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{10474}{\htmlClass{Field Operator}{\text{❴}}}}\, \,\href{Ledger.Dijkstra.Specification.Certs.html#7378}{\htmlId{10476}{\htmlClass{Generalizable}{\text{c}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{10478}{\htmlClass{Field Operator}{\text{❵}}}}\, \,\href{Axiom.Set.Map.html#13606}{\htmlId{10480}{\htmlClass{Function Operator}{\text{ᶜ}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#6924}{\htmlId{10484}{\htmlClass{Generalizable}{\text{rwds}}}}\, \,\href{Axiom.Set.Map.html#13606}{\htmlId{10489}{\htmlClass{Function Operator}{\text{∣}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{10491}{\htmlClass{Field Operator}{\text{❴}}}}\, \,\href{Ledger.Dijkstra.Specification.Certs.html#7378}{\htmlId{10493}{\htmlClass{Generalizable}{\text{c}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{10495}{\htmlClass{Field Operator}{\text{❵}}}}\, \,\href{Axiom.Set.Map.html#13606}{\htmlId{10497}{\htmlClass{Function Operator}{\text{ᶜ}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#7246}{\htmlId{10501}{\htmlClass{Generalizable}{\text{deposits}}}}\, \,\href{Axiom.Set.Map.html#13606}{\htmlId{10510}{\htmlClass{Function Operator}{\text{∣}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{10512}{\htmlClass{Field Operator}{\text{❴}}}}\, \,\href{Ledger.Dijkstra.Specification.Certs.html#7378}{\htmlId{10514}{\htmlClass{Generalizable}{\text{c}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{10516}{\htmlClass{Field Operator}{\text{❵}}}}\, \,\href{Axiom.Set.Map.html#13606}{\htmlId{10518}{\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#7106}{\htmlId{10840}{\htmlClass{Generalizable}{\text{pools}}}}\,
         \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#7112}{\htmlId{10857}{\htmlClass{Generalizable}{\text{fPools}}}}\,
         \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#7139}{\htmlId{10875}{\htmlClass{Generalizable}{\text{retiring}}}}\,
         \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#7246}{\htmlId{10895}{\htmlClass{Generalizable}{\text{deposits}}}}\,
         \end{pmatrix}$ ⇀⦇ regpool kh poolParams ,POOL⦈ $\begin{pmatrix}
           \,\href{Ledger.Dijkstra.Specification.Certs.html#7106}{\htmlId{10960}{\htmlClass{Generalizable}{\text{pools}}}}\, \,\href{Axiom.Set.Map.html#7640}{\htmlId{10966}{\htmlClass{Function Operator}{\text{∪ˡ}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{10969}{\htmlClass{Field Operator}{\text{❴}}}}\, \,\href{Ledger.Dijkstra.Specification.Certs.html#7540}{\htmlId{10971}{\htmlClass{Generalizable}{\text{kh}}}}\, , \,\href{Ledger.Dijkstra.Specification.Certs.html#7594}{\htmlId{10976}{\htmlClass{Generalizable}{\text{poolParams}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{10987}{\htmlClass{Field Operator}{\text{❵}}}}\,
         \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#7112}{\htmlId{11000}{\htmlClass{Generalizable}{\text{fPools}}}}\,
         \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#7139}{\htmlId{11018}{\htmlClass{Generalizable}{\text{retiring}}}}\,
         \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#7246}{\htmlId{11038}{\htmlClass{Generalizable}{\text{deposits}}}}\, \,\href{Axiom.Set.Map.html#7640}{\htmlId{11047}{\htmlClass{Function Operator}{\text{∪ˡ}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{11050}{\htmlClass{Field Operator}{\text{❴}}}}\, \,\href{Ledger.Dijkstra.Specification.Certs.html#7540}{\htmlId{11052}{\htmlClass{Generalizable}{\text{kh}}}}\, , \,\href{Ledger.Dijkstra.Specification.Certs.html#7626}{\htmlId{11057}{\htmlClass{Generalizable}{\text{pp}}}}\, \,\htmlId{11060}{\htmlClass{Symbol}{\text{.}}}\,\,\href{Ledger.Dijkstra.Specification.PParams.html#3051}{\htmlId{11061}{\htmlClass{Field}{\text{poolDeposit}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{11073}{\htmlClass{Field Operator}{\text{❵}}}}\,
         \end{pmatrix}$

  POOL-rereg :
    ∙ Is-just (isPoolRegistered pools kh)
    ────────────────────────────────
    pp ⊢ $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Certs.html#7106}{\htmlId{11192}{\htmlClass{Generalizable}{\text{pools}}}}\,
         \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#7112}{\htmlId{11209}{\htmlClass{Generalizable}{\text{fPools}}}}\,
         \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#7139}{\htmlId{11227}{\htmlClass{Generalizable}{\text{retiring}}}}\,
         \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#7246}{\htmlId{11247}{\htmlClass{Generalizable}{\text{deposits}}}}\,
         \end{pmatrix}$ ⇀⦇ regpool kh poolParams ,POOL⦈ $\begin{pmatrix}
           \,\href{Ledger.Dijkstra.Specification.Certs.html#7106}{\htmlId{11312}{\htmlClass{Generalizable}{\text{pools}}}}\,
         \\ \,\href{Class.HasSingleton.html#288}{\htmlId{11329}{\htmlClass{Field Operator}{\text{❴}}}}\, \,\href{Ledger.Dijkstra.Specification.Certs.html#7540}{\htmlId{11331}{\htmlClass{Generalizable}{\text{kh}}}}\, , \,\href{Ledger.Dijkstra.Specification.Certs.html#7594}{\htmlId{11336}{\htmlClass{Generalizable}{\text{poolParams}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{11347}{\htmlClass{Field Operator}{\text{❵}}}}\, \,\href{Axiom.Set.Map.html#7640}{\htmlId{11349}{\htmlClass{Function Operator}{\text{∪ˡ}}}}\, \,\href{Ledger.Dijkstra.Specification.Certs.html#7112}{\htmlId{11352}{\htmlClass{Generalizable}{\text{fPools}}}}\,
         \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#7139}{\htmlId{11370}{\htmlClass{Generalizable}{\text{retiring}}}}\, \,\href{Axiom.Set.Map.html#13606}{\htmlId{11379}{\htmlClass{Function Operator}{\text{∣}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{11381}{\htmlClass{Field Operator}{\text{❴}}}}\, \,\href{Ledger.Dijkstra.Specification.Certs.html#7540}{\htmlId{11383}{\htmlClass{Generalizable}{\text{kh}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{11386}{\htmlClass{Field Operator}{\text{❵}}}}\, \,\href{Axiom.Set.Map.html#13606}{\htmlId{11388}{\htmlClass{Function Operator}{\text{ᶜ}}}}\,
         \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#7246}{\htmlId{11401}{\htmlClass{Generalizable}{\text{deposits}}}}\,
         \end{pmatrix}$

  POOL-retirepool :
    ────────────────────────────────
    pp ⊢ $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Certs.html#7106}{\htmlId{11490}{\htmlClass{Generalizable}{\text{pools}}}}\,
         \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#7112}{\htmlId{11507}{\htmlClass{Generalizable}{\text{fPools}}}}\,
         \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#7139}{\htmlId{11525}{\htmlClass{Generalizable}{\text{retiring}}}}\,
         \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#7246}{\htmlId{11545}{\htmlClass{Generalizable}{\text{deposits}}}}\,
         \end{pmatrix}$ ⇀⦇ retirepool kh e ,POOL⦈ $\begin{pmatrix}
           \,\href{Ledger.Dijkstra.Specification.Certs.html#7106}{\htmlId{11604}{\htmlClass{Generalizable}{\text{pools}}}}\,
         \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#7112}{\htmlId{11621}{\htmlClass{Generalizable}{\text{fPools}}}}\,
         \\ \,\href{Class.HasSingleton.html#288}{\htmlId{11639}{\htmlClass{Field Operator}{\text{❴}}}}\, \,\href{Ledger.Dijkstra.Specification.Certs.html#7540}{\htmlId{11641}{\htmlClass{Generalizable}{\text{kh}}}}\, , \,\href{Ledger.Dijkstra.Specification.Certs.html#7489}{\htmlId{11646}{\htmlClass{Generalizable}{\text{e}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{11648}{\htmlClass{Field Operator}{\text{❵}}}}\, \,\href{Axiom.Set.Map.html#7640}{\htmlId{11650}{\htmlClass{Function Operator}{\text{∪ˡ}}}}\, \,\href{Ledger.Dijkstra.Specification.Certs.html#7139}{\htmlId{11653}{\htmlClass{Generalizable}{\text{retiring}}}}\,
         \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#7246}{\htmlId{11673}{\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#7489}{\htmlId{11946}{\htmlClass{Generalizable}{\text{e}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#7626}{\htmlId{11950}{\htmlClass{Generalizable}{\text{pp}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#7511}{\htmlId{11955}{\htmlClass{Generalizable}{\text{vs}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#7175}{\htmlId{11960}{\htmlClass{Generalizable}{\text{wdrls}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#7740}{\htmlId{11968}{\htmlClass{Generalizable}{\text{cc}}}}\, \end{pmatrix}$ ⊢ $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Certs.html#6959}{\htmlId{11977}{\htmlClass{Generalizable}{\text{dReps}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#7031}{\htmlId{11985}{\htmlClass{Generalizable}{\text{ccKeys}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#7246}{\htmlId{11994}{\htmlClass{Generalizable}{\text{deposits}}}}\, \end{pmatrix}$ ⇀⦇ regdrep c d an ,GOVCERT⦈ $\begin{pmatrix} \,\href{Class.HasSingleton.html#288}{\htmlId{12035}{\htmlClass{Field Operator}{\text{❴}}}}\, \,\href{Ledger.Dijkstra.Specification.Certs.html#7378}{\htmlId{12037}{\htmlClass{Generalizable}{\text{c}}}}\, , \,\href{Ledger.Dijkstra.Specification.Certs.html#7489}{\htmlId{12041}{\htmlClass{Generalizable}{\text{e}}}}\, \,\href{Class.HasAdd.Core.html#162}{\htmlId{12043}{\htmlClass{Field Operator}{\text{+}}}}\, \,\href{Ledger.Dijkstra.Specification.Certs.html#7626}{\htmlId{12045}{\htmlClass{Generalizable}{\text{pp}}}}\, \,\htmlId{12048}{\htmlClass{Symbol}{\text{.}}}\,\,\href{Ledger.Dijkstra.Specification.PParams.html#4181}{\htmlId{12049}{\htmlClass{Field}{\text{drepActivity}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{12062}{\htmlClass{Field Operator}{\text{❵}}}}\, \,\href{Axiom.Set.Map.html#7640}{\htmlId{12064}{\htmlClass{Function Operator}{\text{∪ˡ}}}}\, \,\href{Ledger.Dijkstra.Specification.Certs.html#6959}{\htmlId{12067}{\htmlClass{Generalizable}{\text{dReps}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#7031}{\htmlId{12075}{\htmlClass{Generalizable}{\text{ccKeys}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#7246}{\htmlId{12084}{\htmlClass{Generalizable}{\text{deposits}}}}\, \,\href{Axiom.Set.Map.Dec.html#2149}{\htmlId{12093}{\htmlClass{Function Operator}{\text{∪⁺}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{12096}{\htmlClass{Field Operator}{\text{❴}}}}\, \,\href{Ledger.Dijkstra.Specification.Certs.html#7378}{\htmlId{12098}{\htmlClass{Generalizable}{\text{c}}}}\, , \,\href{Ledger.Dijkstra.Specification.Certs.html#7330}{\htmlId{12102}{\htmlClass{Generalizable}{\text{d}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{12104}{\htmlClass{Field Operator}{\text{❵}}}}\, \end{pmatrix}$

  GOVCERT-deregdrep :
    ∙ c ∈ dom dReps
    ∙ (c , d) ∈ deposits
      ────────────────────────────────
      $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Certs.html#7489}{\htmlId{12223}{\htmlClass{Generalizable}{\text{e}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#7626}{\htmlId{12227}{\htmlClass{Generalizable}{\text{pp}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#7511}{\htmlId{12232}{\htmlClass{Generalizable}{\text{vs}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#7175}{\htmlId{12237}{\htmlClass{Generalizable}{\text{wdrls}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#7740}{\htmlId{12245}{\htmlClass{Generalizable}{\text{cc}}}}\, \end{pmatrix}$ ⊢ $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Certs.html#6959}{\htmlId{12254}{\htmlClass{Generalizable}{\text{dReps}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#7031}{\htmlId{12262}{\htmlClass{Generalizable}{\text{ccKeys}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#7246}{\htmlId{12271}{\htmlClass{Generalizable}{\text{deposits}}}}\, \end{pmatrix}$ ⇀⦇ deregdrep c d ,GOVCERT⦈ $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Certs.html#6959}{\htmlId{12311}{\htmlClass{Generalizable}{\text{dReps}}}}\, \,\href{Axiom.Set.Map.html#13606}{\htmlId{12317}{\htmlClass{Function Operator}{\text{∣}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{12319}{\htmlClass{Field Operator}{\text{❴}}}}\, \,\href{Ledger.Dijkstra.Specification.Certs.html#7378}{\htmlId{12321}{\htmlClass{Generalizable}{\text{c}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{12323}{\htmlClass{Field Operator}{\text{❵}}}}\, \,\href{Axiom.Set.Map.html#13606}{\htmlId{12325}{\htmlClass{Function Operator}{\text{ᶜ}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#7031}{\htmlId{12329}{\htmlClass{Generalizable}{\text{ccKeys}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#7246}{\htmlId{12338}{\htmlClass{Generalizable}{\text{deposits}}}}\, \,\href{Axiom.Set.Map.html#13606}{\htmlId{12347}{\htmlClass{Function Operator}{\text{∣}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{12349}{\htmlClass{Field Operator}{\text{❴}}}}\, \,\href{Ledger.Dijkstra.Specification.Certs.html#7378}{\htmlId{12351}{\htmlClass{Generalizable}{\text{c}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{12353}{\htmlClass{Field Operator}{\text{❵}}}}\, \,\href{Axiom.Set.Map.html#13606}{\htmlId{12355}{\htmlClass{Function Operator}{\text{ᶜ}}}}\, \end{pmatrix}$

  GOVCERT-ccreghot :
    ∙ (c , nothing) ∉ ccKeys
    ∙ c ∈ cc
      ────────────────────────────────
      $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Certs.html#7489}{\htmlId{12470}{\htmlClass{Generalizable}{\text{e}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#7626}{\htmlId{12474}{\htmlClass{Generalizable}{\text{pp}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#7511}{\htmlId{12479}{\htmlClass{Generalizable}{\text{vs}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#7175}{\htmlId{12484}{\htmlClass{Generalizable}{\text{wdrls}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#7740}{\htmlId{12492}{\htmlClass{Generalizable}{\text{cc}}}}\, \end{pmatrix}$ ⊢ $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Certs.html#6959}{\htmlId{12501}{\htmlClass{Generalizable}{\text{dReps}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#7031}{\htmlId{12509}{\htmlClass{Generalizable}{\text{ccKeys}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#7246}{\htmlId{12518}{\htmlClass{Generalizable}{\text{deposits}}}}\, \end{pmatrix}$ ⇀⦇ ccreghot c mc ,GOVCERT⦈ $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Certs.html#6959}{\htmlId{12558}{\htmlClass{Generalizable}{\text{dReps}}}}\, \\ \,\href{Class.HasSingleton.html#288}{\htmlId{12566}{\htmlClass{Field Operator}{\text{❴}}}}\, \,\href{Ledger.Dijkstra.Specification.Certs.html#7378}{\htmlId{12568}{\htmlClass{Generalizable}{\text{c}}}}\, , \,\href{Ledger.Dijkstra.Specification.Certs.html#7405}{\htmlId{12572}{\htmlClass{Generalizable}{\text{mc}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{12575}{\htmlClass{Field Operator}{\text{❵}}}}\, \,\href{Axiom.Set.Map.html#7640}{\htmlId{12577}{\htmlClass{Function Operator}{\text{∪ˡ}}}}\, \,\href{Ledger.Dijkstra.Specification.Certs.html#7031}{\htmlId{12580}{\htmlClass{Generalizable}{\text{ccKeys}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#7246}{\htmlId{12589}{\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#7626}{\htmlId{12729}{\htmlClass{Generalizable}{\text{pp}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#2663}{\htmlId{12734}{\htmlClass{Field}{\text{PState.pools}}}}\, \,\href{Ledger.Dijkstra.Specification.Certs.html#7720}{\htmlId{12747}{\htmlClass{Generalizable}{\text{stᵖ}}}}\, \\ \,\href{Class.IsSet.html#916}{\htmlId{12753}{\htmlClass{Function}{\text{dom}}}}\, \,\htmlId{12757}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Dijkstra.Specification.Certs.html#2829}{\htmlId{12758}{\htmlClass{Field}{\text{GState.dreps}}}}\, \,\href{Ledger.Dijkstra.Specification.Certs.html#7700}{\htmlId{12771}{\htmlClass{Generalizable}{\text{stᵍ}}}}\,\,\htmlId{12774}{\htmlClass{Symbol}{\text{)}}}\, \end{pmatrix}$ ⊢ stᵈ ⇀⦇ dCert ,DELEG⦈ stᵈ'
      ────────────────────────────────
      $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Certs.html#7489}{\htmlId{12853}{\htmlClass{Generalizable}{\text{e}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#7626}{\htmlId{12857}{\htmlClass{Generalizable}{\text{pp}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#7511}{\htmlId{12862}{\htmlClass{Generalizable}{\text{vs}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#7175}{\htmlId{12867}{\htmlClass{Generalizable}{\text{wdrls}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#7740}{\htmlId{12875}{\htmlClass{Generalizable}{\text{cc}}}}\, \end{pmatrix}$ ⊢ $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Certs.html#7680}{\htmlId{12884}{\htmlClass{Generalizable}{\text{stᵈ}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#7720}{\htmlId{12890}{\htmlClass{Generalizable}{\text{stᵖ}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#7700}{\htmlId{12896}{\htmlClass{Generalizable}{\text{stᵍ}}}}\, \end{pmatrix}$ ⇀⦇ dCert ,CERT⦈ $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Certs.html#7684}{\htmlId{12920}{\htmlClass{Generalizable}{\text{stᵈ'}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#7720}{\htmlId{12927}{\htmlClass{Generalizable}{\text{stᵖ}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#7700}{\htmlId{12933}{\htmlClass{Generalizable}{\text{stᵍ}}}}\, \end{pmatrix}$

  CERT-pool :
    ∙ pp ⊢ stᵖ ⇀⦇ dCert ,POOL⦈ stᵖ'
      ────────────────────────────────
      $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Certs.html#7489}{\htmlId{13037}{\htmlClass{Generalizable}{\text{e}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#7626}{\htmlId{13041}{\htmlClass{Generalizable}{\text{pp}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#7511}{\htmlId{13046}{\htmlClass{Generalizable}{\text{vs}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#7175}{\htmlId{13051}{\htmlClass{Generalizable}{\text{wdrls}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#7740}{\htmlId{13059}{\htmlClass{Generalizable}{\text{cc}}}}\, \end{pmatrix}$ ⊢ $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Certs.html#7680}{\htmlId{13068}{\htmlClass{Generalizable}{\text{stᵈ}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#7720}{\htmlId{13074}{\htmlClass{Generalizable}{\text{stᵖ}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#7700}{\htmlId{13080}{\htmlClass{Generalizable}{\text{stᵍ}}}}\, \end{pmatrix}$ ⇀⦇ dCert ,CERT⦈ $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Certs.html#7680}{\htmlId{13104}{\htmlClass{Generalizable}{\text{stᵈ}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#7724}{\htmlId{13110}{\htmlClass{Generalizable}{\text{stᵖ'}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#7700}{\htmlId{13117}{\htmlClass{Generalizable}{\text{stᵍ}}}}\, \end{pmatrix}$

  CERT-gov :
    ∙ Γ ⊢ stᵍ ⇀⦇ dCert ,GOVCERT⦈ stᵍ'
      ────────────────────────────────
      Γ ⊢ $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Certs.html#7680}{\htmlId{13226}{\htmlClass{Generalizable}{\text{stᵈ}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#7720}{\htmlId{13232}{\htmlClass{Generalizable}{\text{stᵖ}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#7700}{\htmlId{13238}{\htmlClass{Generalizable}{\text{stᵍ}}}}\, \end{pmatrix}$ ⇀⦇ dCert ,CERT⦈ $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Certs.html#7680}{\htmlId{13262}{\htmlClass{Generalizable}{\text{stᵈ}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#7720}{\htmlId{13268}{\htmlClass{Generalizable}{\text{stᵖ}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#7704}{\htmlId{13274}{\htmlClass{Generalizable}{\text{stᵍ'}}}}\, \end{pmatrix}$

PRE-CERT Transition Rule

Withdrawal Processing

The PRE-CERT rule processes withdrawals before certificate evaluation. In the Dijkstra era, CIP-159 extends the withdrawal semantics from an "all-or-nothing" model (where the withdrawn amount must equal the full account balance) to a "partial withdrawal" model (where any amount up to the full balance may be withdrawn).

The precondition checks that each withdrawal targets a registered account and that the withdrawal amount does not exceed the account's current balance. The effect subtracts the withdrawal amounts from the corresponding account balances via applyWithdrawals.

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#7489}{\htmlId{14536}{\htmlClass{Generalizable}{\text{e}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#7626}{\htmlId{14540}{\htmlClass{Generalizable}{\text{pp}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#7511}{\htmlId{14545}{\htmlClass{Generalizable}{\text{vs}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#7175}{\htmlId{14550}{\htmlClass{Generalizable}{\text{wdrls}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#7740}{\htmlId{14558}{\htmlClass{Generalizable}{\text{cc}}}}\, \end{pmatrix}$ ⊢ $\begin{pmatrix} \begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Certs.html#7076}{\htmlId{14569}{\htmlClass{Generalizable}{\text{voteDelegs}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#7000}{\htmlId{14582}{\htmlClass{Generalizable}{\text{stakeDelegs}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#6929}{\htmlId{14596}{\htmlClass{Generalizable}{\text{rewards}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#7246}{\htmlId{14606}{\htmlClass{Generalizable}{\text{deposits}}}}\, \end{pmatrix} \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#7720}{\htmlId{14619}{\htmlClass{Generalizable}{\text{stᵖ}}}}\, \\ \begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Certs.html#6959}{\htmlId{14627}{\htmlClass{Generalizable}{\text{dReps}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#7038}{\htmlId{14635}{\htmlClass{Generalizable}{\text{ccHotKeys}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#7255}{\htmlId{14647}{\htmlClass{Generalizable}{\text{deposits'}}}}\, \end{pmatrix} \end{pmatrix}$ ⇀⦇ _ ,PRE-CERT⦈ $\begin{pmatrix} \begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Certs.html#7076}{\htmlId{14681}{\htmlClass{Generalizable}{\text{voteDelegs}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#7000}{\htmlId{14694}{\htmlClass{Generalizable}{\text{stakeDelegs}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#8161}{\htmlId{14708}{\htmlClass{Function}{\text{applyWithdrawals}}}}\, \,\href{Ledger.Dijkstra.Specification.Certs.html#7175}{\htmlId{14725}{\htmlClass{Generalizable}{\text{wdrls}}}}\, \,\href{Ledger.Dijkstra.Specification.Certs.html#6929}{\htmlId{14731}{\htmlClass{Generalizable}{\text{rewards}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#7246}{\htmlId{14741}{\htmlClass{Generalizable}{\text{deposits}}}}\, \end{pmatrix} \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#7720}{\htmlId{14754}{\htmlClass{Generalizable}{\text{stᵖ}}}}\, \\ \begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Certs.html#14188}{\htmlId{14762}{\htmlClass{Bound}{\text{refreshedDReps}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#7038}{\htmlId{14779}{\htmlClass{Generalizable}{\text{ccHotKeys}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#7255}{\htmlId{14791}{\htmlClass{Generalizable}{\text{deposits'}}}}\, \end{pmatrix} \end{pmatrix}$

TODO: Version restriction (deferred). CIP-159 specifies that partial withdrawals are only permitted in transactions without Plutus v1–v3 scripts (i.e., legacyMode ≡ false). Enforcing this requires threading legacyMode into CertEnv, which in turn requires changes to the SUBLEDGER and LEDGER rules. This restriction will be added in a follow-up issue.

POST-CERT Transition Rule

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.Dijkstra.Specification.Certs.html#7489}{\htmlId{15465}{\htmlClass{Generalizable}{\text{e}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#7626}{\htmlId{15469}{\htmlClass{Generalizable}{\text{pp}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#7511}{\htmlId{15474}{\htmlClass{Generalizable}{\text{vs}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#7175}{\htmlId{15479}{\htmlClass{Generalizable}{\text{wdrls}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#7740}{\htmlId{15487}{\htmlClass{Generalizable}{\text{cc}}}}\, \end{pmatrix}$ ⊢ $\begin{pmatrix} \begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Certs.html#7076}{\htmlId{15498}{\htmlClass{Generalizable}{\text{voteDelegs}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#7000}{\htmlId{15511}{\htmlClass{Generalizable}{\text{stakeDelegs}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#6929}{\htmlId{15525}{\htmlClass{Generalizable}{\text{rewards}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#7246}{\htmlId{15535}{\htmlClass{Generalizable}{\text{deposits}}}}\, \end{pmatrix} \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#7720}{\htmlId{15548}{\htmlClass{Generalizable}{\text{stᵖ}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#7700}{\htmlId{15554}{\htmlClass{Generalizable}{\text{stᵍ}}}}\, \end{pmatrix}$ ⇀⦇ _ ,POST-CERT⦈ $\begin{pmatrix} \begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Certs.html#7076}{\htmlId{15581}{\htmlClass{Generalizable}{\text{voteDelegs}}}}\, \,\href{Axiom.Set.Map.html#17775}{\htmlId{15592}{\htmlClass{Function Operator}{\text{∣\^{}}}}}\, \,\href{Ledger.Dijkstra.Specification.Certs.html#15314}{\htmlId{15595}{\htmlClass{Bound}{\text{activeVDelegs}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#7000}{\htmlId{15611}{\htmlClass{Generalizable}{\text{stakeDelegs}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#6929}{\htmlId{15625}{\htmlClass{Generalizable}{\text{rewards}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#7246}{\htmlId{15635}{\htmlClass{Generalizable}{\text{deposits}}}}\, \end{pmatrix} \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#7720}{\htmlId{15648}{\htmlClass{Generalizable}{\text{stᵖ}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Certs.html#7700}{\htmlId{15654}{\htmlClass{Generalizable}{\text{stᵍ}}}}\, \end{pmatrix}$


-- CERTS Transition System --

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