Certificates

This section is part of the Ledger.Conway.Certs module of the formal ledger specification.

{-# OPTIONS --safe #-}

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

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


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

Deposit types

Derived types

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

Deposits  = DepositPurpose ⇀ Coin
Rewards   = Credential ⇀ Coin
DReps     = Credential ⇀ Epoch

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

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

record HasDReps {a} (A : Type a) : Type a where
  field DRepsOf : A → DReps
open HasDReps    ⦃...⦄ public

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

Stake pool parameter definitions

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

Delegation definitions

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

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

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

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

Types used for CERTS transition system

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

record HasWdrls {a} (A : Type a) : Type a where
  field wdrlsOf : A → RwdAddr ⇀ Coin
open HasWdrls ⦃...⦄ public

instance
  HasWdrls-CertEnv : HasWdrls CertEnv
  HasWdrls-CertEnv .wdrlsOf = CertEnv.wdrls

record DState : Type where

  constructor ⟦_,_,_⟧ᵈ

  field
    voteDelegs   : Credential ⇀ VDeleg
    stakeDelegs  : Credential ⇀ KeyHash
    rewards      : Credential ⇀ Coin

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

record HasVDelegs {a} (A : Type a) : Type a where
  field voteDelegsOf : A → Credential ⇀ VDeleg
open HasVDelegs ⦃...⦄ public

instance
  HasVDelegs-DState : HasVDelegs DState
  HasVDelegs-DState .voteDelegsOf = DState.voteDelegs

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

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

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

record GState : Type where

  constructor ⟦_,_⟧ᵛ

  field
    dreps      : DReps
    ccHotKeys  : Credential ⇀ Maybe Credential

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

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

record CertState : Type where

  constructor ⟦_,_,_⟧ᶜˢ

  field
    dState : DState
    pState : PState
    gState : GState

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

instance
  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

record DelegEnv : Type where
  field
    pparams       : PParams
    pools         : KeyHash ⇀ PoolParams
    delegatees    : ℙ Credential

GovCertEnv  = CertEnv
PoolEnv     = PParams

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

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

instance
  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    : Credential ⇀ KeyHash
  ccKeys ccHotKeys       : Credential ⇀ Maybe Credential
  vDelegs voteDelegs     : Credential ⇀ VDeleg
  pools                  : KeyHash ⇀ PoolParams
  retiring               : KeyHash ⇀ Epoch
  wdrls                  : RwdAddr ⇀ 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  : PoolParams
  pp          : PParams
  mv          : Maybe VDeleg

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

Changes Introduced in Conway Era

Delegation

Registered credentials can now delegate to a DRep as well as to a stake pool. This is achieved by giving the delegate certificate two optional fields, corresponding to a DRep and stake pool.

Stake can be delegated for voting and block production simultaneously, since these are two separate features. In fact, preventing this could weaken the security of the chain, since security relies on high participation of honest stake holders.

Removal of Pointer Addresses, Genesis Delegations and MIR Certificates

Support for pointer addresses, genesis delegations and MIR certificates is removed (see CIP-1694 and ). In DState, this means that the four fields relating to those features are no longer present, and DelegEnv contains none of the fields it used to in the Shelley era (see ).

Note that pointer addresses are still usable, only their staking functionality has been retired. So all funds locked behind pointer addresses are still accessible, they just don’t count towards the stake distribution anymore. Genesis delegations and MIR certificates have been superceded by the new governance mechanisms, in particular the TreasuryWdrl governance action in case of the MIR certificates.

Explicit Deposits

Registration and deregistration of staking credentials are now required to explicitly state the deposit that is being paid or refunded. This deposit is used for checking correctness of transactions with certificates. Including the deposit aligns better with other design decisions such as having explicit transaction fees and helps make this information visible to light clients and hardware wallets.

While not shown in the figures, the old certificates without explicit deposits will still be supported for some time for backwards compatibility.

Governance Certificate Rules

The rules for transition systems dealing with individual certificates are defined in Figure 'Auxiliary-DELEG-transition-system' and Figure 'Auxiliary-POOL-transition-system' and Figure 'Auxiliary-GOVCERT-transition-system'.

Conway specifics

Figure 'Auxiliary-DELEG-transition-system' and Figure 'Auxiliary-GOVCERT-transition-system'.

GOVCERT deals with the new certificates relating to DReps and the constitutional committee.

• GOVCERTregdrep registers (or re-registers) a DRep. In case of registration, a deposit needs to be paid. Either way, the activity period of the DRep is reset.

• GOVCERTderegdrep deregisters a DRep.

• GOVCERTccreghot registers a “hot” credential for constitutional committee members.¹ We check that the cold key did not previously resign from the committee. We allow this delegation for any cold credential that is either part of EnactState or is is a proposal. This allows a newly elected member of the constitutional committee to immediately delegate their vote to a hot key and use it to vote. Since votes are counted after previous actions have been enacted, this allows constitutional committee members to act without a delay of one epoch.

Types for the transition systems relating to certificates

data

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

data

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

data

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

data

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

data

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

module _ where  -- achieves uniform (but perhaps misleading) alignment of type signatures in fig

  _⊢_⇀⦇_,CERTS⦈_     : CertEnv     → CertState  → List DCert  → CertState  → Type

  _⊢_⇀⦇_,CERTS⦈_ = ReflexiveTransitiveClosureᵇ' {_⊢_⇀⟦_⟧ᵇ_ = _⊢_⇀⦇_,CERTBASE⦈_} {_⊢_⇀⦇_,CERT⦈_}

Auxiliary DELEG transition system

data _⊢_⇀⦇_,DELEG⦈_ where

  DELEG-delegate :
    let Γ = $\begin{pmatrix} \,\href{Ledger.Conway.Certs.html#7456}{\htmlId{12412}{\htmlClass{Generalizable}{\text{pp}}}}\, \\ \,\href{Ledger.Conway.Certs.html#6984}{\htmlId{12417}{\htmlClass{Generalizable}{\text{pools}}}}\, \\ \,\href{Ledger.Conway.Certs.html#7273}{\htmlId{12425}{\htmlClass{Generalizable}{\text{delegatees}}}}\, \end{pmatrix}$
    in
    ∙ (c ∉ dom rwds → d ≡ pp .keyDeposit)
    ∙ (c ∈ dom rwds → d ≡ )
    ∙ mv ∈ mapˢ (just ∘ credVoter DRep) delegatees ∪
        fromList ( nothing ∷ just abstainRep ∷ just noConfidenceRep ∷ [] )
    ∙ mkh ∈ mapˢ just (dom pools) ∪ ❴ nothing ❵
      ────────────────────────────────
      Γ ⊢  $\begin{pmatrix} \,\href{Ledger.Conway.Certs.html#6937}{\htmlId{12744}{\htmlClass{Generalizable}{\text{vDelegs}}}}\, \\ \,\href{Ledger.Conway.Certs.html#6832}{\htmlId{12754}{\htmlClass{Generalizable}{\text{sDelegs}}}}\, \\ \,\href{Ledger.Conway.Certs.html#6764}{\htmlId{12764}{\htmlClass{Generalizable}{\text{rwds}}}}\, \end{pmatrix}$ ⇀⦇ delegate c mv mkh d ,DELEG⦈
           $\begin{pmatrix} \,\href{Axiom.Set.Map.html#7168}{\htmlId{12815}{\htmlClass{Function}{\text{insertIfJust}}}}\, \,\href{Ledger.Conway.Certs.html#7213}{\htmlId{12828}{\htmlClass{Generalizable}{\text{c}}}}\, \,\href{Ledger.Conway.Certs.html#7480}{\htmlId{12830}{\htmlClass{Generalizable}{\text{mv}}}}\, \,\href{Ledger.Conway.Certs.html#6937}{\htmlId{12833}{\htmlClass{Generalizable}{\text{vDelegs}}}}\, \\ \,\href{Axiom.Set.Map.html#7168}{\htmlId{12843}{\htmlClass{Function}{\text{insertIfJust}}}}\, \,\href{Ledger.Conway.Certs.html#7213}{\htmlId{12856}{\htmlClass{Generalizable}{\text{c}}}}\, \,\href{Ledger.Conway.Certs.html#7399}{\htmlId{12858}{\htmlClass{Generalizable}{\text{mkh}}}}\, \,\href{Ledger.Conway.Certs.html#6832}{\htmlId{12862}{\htmlClass{Generalizable}{\text{sDelegs}}}}\, \\ \,\href{Ledger.Conway.Certs.html#6764}{\htmlId{12872}{\htmlClass{Generalizable}{\text{rwds}}}}\, \,\href{Axiom.Set.Map.html#6320}{\htmlId{12877}{\htmlClass{Function Operator}{\text{∪ˡ}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{12880}{\htmlClass{Field Operator}{\text{❴}}}}\, \,\href{Ledger.Conway.Certs.html#7213}{\htmlId{12882}{\htmlClass{Generalizable}{\text{c}}}}\, \\ \,\htmlId{12886}{\htmlClass{Number}{\text{0}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{12888}{\htmlClass{Field Operator}{\text{❵}}}}\, \end{pmatrix}$

  DELEG-dereg :
    ∙ (c , ) ∈ rwds
      ────────────────────────────────
      $\begin{pmatrix} \,\href{Ledger.Conway.Certs.html#7456}{\htmlId{12977}{\htmlClass{Generalizable}{\text{pp}}}}\, \\ \,\href{Ledger.Conway.Certs.html#6984}{\htmlId{12982}{\htmlClass{Generalizable}{\text{pools}}}}\, \\ \,\href{Ledger.Conway.Certs.html#7273}{\htmlId{12990}{\htmlClass{Generalizable}{\text{delegatees}}}}\, \end{pmatrix}$ ⊢ $\begin{pmatrix} \,\href{Ledger.Conway.Certs.html#6937}{\htmlId{13007}{\htmlClass{Generalizable}{\text{vDelegs}}}}\, \\ \,\href{Ledger.Conway.Certs.html#6832}{\htmlId{13017}{\htmlClass{Generalizable}{\text{sDelegs}}}}\, \\ \,\href{Ledger.Conway.Certs.html#6764}{\htmlId{13027}{\htmlClass{Generalizable}{\text{rwds}}}}\, \end{pmatrix}$ ⇀⦇ dereg c md ,DELEG⦈
        $\begin{pmatrix} \,\href{Ledger.Conway.Certs.html#6937}{\htmlId{13066}{\htmlClass{Generalizable}{\text{vDelegs}}}}\, \,\href{Axiom.Set.Map.html#10748}{\htmlId{13074}{\htmlClass{Function Operator}{\text{∣}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{13076}{\htmlClass{Field Operator}{\text{❴}}}}\, \,\href{Ledger.Conway.Certs.html#7213}{\htmlId{13078}{\htmlClass{Generalizable}{\text{c}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{13080}{\htmlClass{Field Operator}{\text{❵}}}}\, \,\href{Axiom.Set.Map.html#10748}{\htmlId{13082}{\htmlClass{Function Operator}{\text{ᶜ}}}}\, \\ \,\href{Ledger.Conway.Certs.html#6832}{\htmlId{13086}{\htmlClass{Generalizable}{\text{sDelegs}}}}\, \,\href{Axiom.Set.Map.html#10748}{\htmlId{13094}{\htmlClass{Function Operator}{\text{∣}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{13096}{\htmlClass{Field Operator}{\text{❴}}}}\, \,\href{Ledger.Conway.Certs.html#7213}{\htmlId{13098}{\htmlClass{Generalizable}{\text{c}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{13100}{\htmlClass{Field Operator}{\text{❵}}}}\, \,\href{Axiom.Set.Map.html#10748}{\htmlId{13102}{\htmlClass{Function Operator}{\text{ᶜ}}}}\, \\ \,\href{Ledger.Conway.Certs.html#6764}{\htmlId{13106}{\htmlClass{Generalizable}{\text{rwds}}}}\, \,\href{Axiom.Set.Map.html#10748}{\htmlId{13111}{\htmlClass{Function Operator}{\text{∣}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{13113}{\htmlClass{Field Operator}{\text{❴}}}}\, \,\href{Ledger.Conway.Certs.html#7213}{\htmlId{13115}{\htmlClass{Generalizable}{\text{c}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{13117}{\htmlClass{Field Operator}{\text{❵}}}}\, \,\href{Axiom.Set.Map.html#10748}{\htmlId{13119}{\htmlClass{Function Operator}{\text{ᶜ}}}}\, \end{pmatrix}$

  DELEG-reg :
    ∙ c ∉ dom rwds
    ∙ d ≡ pp .keyDeposit ⊎ d ≡ 
      ────────────────────────────────
      $\begin{pmatrix} \,\href{Ledger.Conway.Certs.html#7456}{\htmlId{13237}{\htmlClass{Generalizable}{\text{pp}}}}\, \\ \,\href{Ledger.Conway.Certs.html#6984}{\htmlId{13242}{\htmlClass{Generalizable}{\text{pools}}}}\, \\ \,\href{Ledger.Conway.Certs.html#7273}{\htmlId{13250}{\htmlClass{Generalizable}{\text{delegatees}}}}\, \end{pmatrix}$ ⊢
        $\begin{pmatrix} \,\href{Ledger.Conway.Certs.html#6937}{\htmlId{13275}{\htmlClass{Generalizable}{\text{vDelegs}}}}\, \\ \,\href{Ledger.Conway.Certs.html#6832}{\htmlId{13285}{\htmlClass{Generalizable}{\text{sDelegs}}}}\, \\ \,\href{Ledger.Conway.Certs.html#6764}{\htmlId{13295}{\htmlClass{Generalizable}{\text{rwds}}}}\, \end{pmatrix}$ ⇀⦇ reg c d ,DELEG⦈
        $\begin{pmatrix} \,\href{Ledger.Conway.Certs.html#6937}{\htmlId{13331}{\htmlClass{Generalizable}{\text{vDelegs}}}}\, \\ \,\href{Ledger.Conway.Certs.html#6832}{\htmlId{13341}{\htmlClass{Generalizable}{\text{sDelegs}}}}\, \\ \,\href{Ledger.Conway.Certs.html#6764}{\htmlId{13351}{\htmlClass{Generalizable}{\text{rwds}}}}\, \,\href{Axiom.Set.Map.html#6320}{\htmlId{13356}{\htmlClass{Function Operator}{\text{∪ˡ}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{13359}{\htmlClass{Field Operator}{\text{❴}}}}\, \,\href{Ledger.Conway.Certs.html#7213}{\htmlId{13361}{\htmlClass{Generalizable}{\text{c}}}}\, \\ \,\htmlId{13365}{\htmlClass{Number}{\text{0}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{13367}{\htmlClass{Field Operator}{\text{❵}}}}\, \end{pmatrix}$

Auxiliary POOL transition system

data _⊢_⇀⦇_,POOL⦈_ where

  POOL-regpool :
    ∙ kh ∉ dom pools
      ────────────────────────────────
      pp ⊢  $\begin{pmatrix} \,\href{Ledger.Conway.Certs.html#6984}{\htmlId{13609}{\htmlClass{Generalizable}{\text{pools}}}}\, \\ \,\href{Ledger.Conway.Certs.html#7032}{\htmlId{13617}{\htmlClass{Generalizable}{\text{retiring}}}}\, \end{pmatrix}$ ⇀⦇ regpool kh poolParams ,POOL⦈
            $\begin{pmatrix} \,\href{Class.HasSingleton.html#288}{\htmlId{13674}{\htmlClass{Field Operator}{\text{❴}}}}\, \,\href{Ledger.Conway.Certs.html#7375}{\htmlId{13676}{\htmlClass{Generalizable}{\text{kh}}}}\, \\ \,\href{Ledger.Conway.Certs.html#7429}{\htmlId{13681}{\htmlClass{Generalizable}{\text{poolParams}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{13692}{\htmlClass{Field Operator}{\text{❵}}}}\, \,\href{Axiom.Set.Map.html#6320}{\htmlId{13694}{\htmlClass{Function Operator}{\text{∪ˡ}}}}\, \,\href{Ledger.Conway.Certs.html#6984}{\htmlId{13697}{\htmlClass{Generalizable}{\text{pools}}}}\, \\ \,\href{Ledger.Conway.Certs.html#7032}{\htmlId{13705}{\htmlClass{Generalizable}{\text{retiring}}}}\, \end{pmatrix}$

  POOL-retirepool :
    ────────────────────────────────
    pp ⊢ $\begin{pmatrix} \,\href{Ledger.Conway.Certs.html#6984}{\htmlId{13785}{\htmlClass{Generalizable}{\text{pools}}}}\, \\ \,\href{Ledger.Conway.Certs.html#7032}{\htmlId{13793}{\htmlClass{Generalizable}{\text{retiring}}}}\, \end{pmatrix}$ ⇀⦇ retirepool kh e ,POOL⦈ $\begin{pmatrix} \,\href{Ledger.Conway.Certs.html#6984}{\htmlId{13832}{\htmlClass{Generalizable}{\text{pools}}}}\, \\ \,\href{Class.HasSingleton.html#288}{\htmlId{13840}{\htmlClass{Field Operator}{\text{❴}}}}\, \,\href{Ledger.Conway.Certs.html#7375}{\htmlId{13842}{\htmlClass{Generalizable}{\text{kh}}}}\, \\ \,\href{Ledger.Conway.Certs.html#7324}{\htmlId{13847}{\htmlClass{Generalizable}{\text{e}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{13849}{\htmlClass{Field Operator}{\text{❵}}}}\, \,\href{Axiom.Set.Map.html#6320}{\htmlId{13851}{\htmlClass{Function Operator}{\text{∪ˡ}}}}\, \,\href{Ledger.Conway.Certs.html#7032}{\htmlId{13854}{\htmlClass{Generalizable}{\text{retiring}}}}\, \end{pmatrix}$

Auxiliary GOVCERT transition system

data _⊢_⇀⦇_,GOVCERT⦈_ where

  GOVCERT-regdrep :
    let Γ = $\begin{pmatrix} \,\href{Ledger.Conway.Certs.html#7324}{\htmlId{14052}{\htmlClass{Generalizable}{\text{e}}}}\, \\ \,\href{Ledger.Conway.Certs.html#7456}{\htmlId{14056}{\htmlClass{Generalizable}{\text{pp}}}}\, \\ \,\href{Ledger.Conway.Certs.html#7346}{\htmlId{14061}{\htmlClass{Generalizable}{\text{vs}}}}\, \\ \,\href{Ledger.Conway.Certs.html#7075}{\htmlId{14066}{\htmlClass{Generalizable}{\text{wdrls}}}}\, \\ \,\href{Ledger.Conway.Certs.html#7570}{\htmlId{14074}{\htmlClass{Generalizable}{\text{cc}}}}\, \end{pmatrix}$
    in
    ∙ (d ≡ pp .drepDeposit × c ∉ dom dReps) ⊎ (d ≡  × c ∈ dom dReps)
      ────────────────────────────────
      Γ ⊢ $\begin{pmatrix} \,\href{Ledger.Conway.Certs.html#6799}{\htmlId{14207}{\htmlClass{Generalizable}{\text{dReps}}}}\, \\ \,\href{Ledger.Conway.Certs.html#6880}{\htmlId{14215}{\htmlClass{Generalizable}{\text{ccKeys}}}}\, \end{pmatrix}$ ⇀⦇ regdrep c d an ,GOVCERT⦈
          $\begin{pmatrix} \,\href{Class.HasSingleton.html#288}{\htmlId{14264}{\htmlClass{Field Operator}{\text{❴}}}}\, \,\href{Ledger.Conway.Certs.html#7213}{\htmlId{14266}{\htmlClass{Generalizable}{\text{c}}}}\, \\ \,\href{Ledger.Conway.Certs.html#7324}{\htmlId{14270}{\htmlClass{Generalizable}{\text{e}}}}\, \,\href{Class.HasAdd.Core.html#162}{\htmlId{14272}{\htmlClass{Field Operator}{\text{+}}}}\, \,\href{Ledger.Conway.Certs.html#7456}{\htmlId{14274}{\htmlClass{Generalizable}{\text{pp}}}}\, \,\htmlId{14277}{\htmlClass{Symbol}{\text{.}}}\,\,\href{Ledger.Conway.PParams.html#4746}{\htmlId{14278}{\htmlClass{Field}{\text{drepActivity}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{14291}{\htmlClass{Field Operator}{\text{❵}}}}\, \,\href{Axiom.Set.Map.html#6320}{\htmlId{14293}{\htmlClass{Function Operator}{\text{∪ˡ}}}}\, \,\href{Ledger.Conway.Certs.html#6799}{\htmlId{14296}{\htmlClass{Generalizable}{\text{dReps}}}}\, \\ \,\href{Ledger.Conway.Certs.html#6880}{\htmlId{14304}{\htmlClass{Generalizable}{\text{ccKeys}}}}\, \end{pmatrix}$

  GOVCERT-deregdrep :
    ∙ c ∈ dom dReps
      ────────────────────────────────
      $\begin{pmatrix} \,\href{Ledger.Conway.Certs.html#7324}{\htmlId{14403}{\htmlClass{Generalizable}{\text{e}}}}\, \\ \,\href{Ledger.Conway.Certs.html#7456}{\htmlId{14407}{\htmlClass{Generalizable}{\text{pp}}}}\, \\ \,\href{Ledger.Conway.Certs.html#7346}{\htmlId{14412}{\htmlClass{Generalizable}{\text{vs}}}}\, \\ \,\href{Ledger.Conway.Certs.html#7075}{\htmlId{14417}{\htmlClass{Generalizable}{\text{wdrls}}}}\, \\ \,\href{Ledger.Conway.Certs.html#7570}{\htmlId{14425}{\htmlClass{Generalizable}{\text{cc}}}}\, \end{pmatrix}$ ⊢ $\begin{pmatrix} \,\href{Ledger.Conway.Certs.html#6799}{\htmlId{14434}{\htmlClass{Generalizable}{\text{dReps}}}}\, \\ \,\href{Ledger.Conway.Certs.html#6880}{\htmlId{14442}{\htmlClass{Generalizable}{\text{ccKeys}}}}\, \end{pmatrix}$ ⇀⦇ deregdrep c d ,GOVCERT⦈ $\begin{pmatrix} \,\href{Ledger.Conway.Certs.html#6799}{\htmlId{14480}{\htmlClass{Generalizable}{\text{dReps}}}}\, \,\href{Axiom.Set.Map.html#10748}{\htmlId{14486}{\htmlClass{Function Operator}{\text{∣}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{14488}{\htmlClass{Field Operator}{\text{❴}}}}\, \,\href{Ledger.Conway.Certs.html#7213}{\htmlId{14490}{\htmlClass{Generalizable}{\text{c}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{14492}{\htmlClass{Field Operator}{\text{❵}}}}\, \,\href{Axiom.Set.Map.html#10748}{\htmlId{14494}{\htmlClass{Function Operator}{\text{ᶜ}}}}\, \\ \,\href{Ledger.Conway.Certs.html#6880}{\htmlId{14498}{\htmlClass{Generalizable}{\text{ccKeys}}}}\, \end{pmatrix}$

  GOVCERT-ccreghot :
    ∙ (c , nothing) ∉ ccKeys
    ∙ c ∈ cc
      ────────────────────────────────
      $\begin{pmatrix} \,\href{Ledger.Conway.Certs.html#7324}{\htmlId{14618}{\htmlClass{Generalizable}{\text{e}}}}\, \\ \,\href{Ledger.Conway.Certs.html#7456}{\htmlId{14622}{\htmlClass{Generalizable}{\text{pp}}}}\, \\ \,\href{Ledger.Conway.Certs.html#7346}{\htmlId{14627}{\htmlClass{Generalizable}{\text{vs}}}}\, \\ \,\href{Ledger.Conway.Certs.html#7075}{\htmlId{14632}{\htmlClass{Generalizable}{\text{wdrls}}}}\, \\ \,\href{Ledger.Conway.Certs.html#7570}{\htmlId{14640}{\htmlClass{Generalizable}{\text{cc}}}}\, \end{pmatrix}$ ⊢ $\begin{pmatrix} \,\href{Ledger.Conway.Certs.html#6799}{\htmlId{14649}{\htmlClass{Generalizable}{\text{dReps}}}}\, \\ \,\href{Ledger.Conway.Certs.html#6880}{\htmlId{14657}{\htmlClass{Generalizable}{\text{ccKeys}}}}\, \end{pmatrix}$ ⇀⦇ ccreghot c mc ,GOVCERT⦈ $\begin{pmatrix} \,\href{Ledger.Conway.Certs.html#6799}{\htmlId{14695}{\htmlClass{Generalizable}{\text{dReps}}}}\, \\ \,\href{Class.HasSingleton.html#288}{\htmlId{14703}{\htmlClass{Field Operator}{\text{❴}}}}\, \,\href{Ledger.Conway.Certs.html#7213}{\htmlId{14705}{\htmlClass{Generalizable}{\text{c}}}}\, \\ \,\href{Ledger.Conway.Certs.html#7240}{\htmlId{14709}{\htmlClass{Generalizable}{\text{mc}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{14712}{\htmlClass{Field Operator}{\text{❵}}}}\, \,\href{Axiom.Set.Map.html#6320}{\htmlId{14714}{\htmlClass{Function Operator}{\text{∪ˡ}}}}\, \,\href{Ledger.Conway.Certs.html#6880}{\htmlId{14717}{\htmlClass{Generalizable}{\text{ccKeys}}}}\, \end{pmatrix}$

Figure 'CERTS-rules' assembles the CERTS transition system by bundling the previously defined pieces together into the CERT system, and then taking the reflexive-transitive closure of CERT together with CERTBASE as the base case. CERTBASE does the following:

• check the correctness of withdrawals and ensure that withdrawals only happen from credentials that have delegated their voting power;

• set the rewards of the credentials that withdrew funds to zero;

• and set the activity timer of all DReps that voted to drepActivity epochs in the future.

CERTS rules

CERT transitions

data _⊢_⇀⦇_,CERT⦈_ where

  CERT-deleg :
    ∙ $\begin{pmatrix} \,\href{Ledger.Conway.Certs.html#7456}{\htmlId{15506}{\htmlClass{Generalizable}{\text{pp}}}}\, \\ \,\href{Ledger.Conway.Certs.html#4501}{\htmlId{15511}{\htmlClass{Field}{\text{PState.pools}}}}\, \,\href{Ledger.Conway.Certs.html#7550}{\htmlId{15524}{\htmlClass{Generalizable}{\text{stᵖ}}}}\, \\ \,\href{Class.IsSet.html#916}{\htmlId{15530}{\htmlClass{Function}{\text{dom}}}}\, (\,\href{Ledger.Conway.Certs.html#4812}{\htmlId{15535}{\htmlClass{Field}{\text{GState.dreps}}}}\, \,\href{Ledger.Conway.Certs.html#7530}{\htmlId{15548}{\htmlClass{Generalizable}{\text{stᵍ}}}}\,) \end{pmatrix}$ ⊢ stᵈ ⇀⦇ dCert ,DELEG⦈ stᵈ'
      ────────────────────────────────
      $\begin{pmatrix} \,\href{Ledger.Conway.Certs.html#7324}{\htmlId{15630}{\htmlClass{Generalizable}{\text{e}}}}\, \\ \,\href{Ledger.Conway.Certs.html#7456}{\htmlId{15634}{\htmlClass{Generalizable}{\text{pp}}}}\, \\ \,\href{Ledger.Conway.Certs.html#7346}{\htmlId{15639}{\htmlClass{Generalizable}{\text{vs}}}}\, \\ \,\href{Ledger.Conway.Certs.html#7075}{\htmlId{15644}{\htmlClass{Generalizable}{\text{wdrls}}}}\, \\ \,\href{Ledger.Conway.Certs.html#7570}{\htmlId{15652}{\htmlClass{Generalizable}{\text{cc}}}}\, \end{pmatrix}$ ⊢ $\begin{pmatrix} \,\href{Ledger.Conway.Certs.html#7510}{\htmlId{15661}{\htmlClass{Generalizable}{\text{stᵈ}}}}\, \\ \,\href{Ledger.Conway.Certs.html#7550}{\htmlId{15667}{\htmlClass{Generalizable}{\text{stᵖ}}}}\, \\ \,\href{Ledger.Conway.Certs.html#7530}{\htmlId{15673}{\htmlClass{Generalizable}{\text{stᵍ}}}}\, \end{pmatrix}$ ⇀⦇ dCert ,CERT⦈ $\begin{pmatrix} \,\href{Ledger.Conway.Certs.html#7514}{\htmlId{15697}{\htmlClass{Generalizable}{\text{stᵈ'}}}}\, \\ \,\href{Ledger.Conway.Certs.html#7550}{\htmlId{15704}{\htmlClass{Generalizable}{\text{stᵖ}}}}\, \\ \,\href{Ledger.Conway.Certs.html#7530}{\htmlId{15710}{\htmlClass{Generalizable}{\text{stᵍ}}}}\, \end{pmatrix}$

  CERT-pool :
    ∙ pp ⊢ stᵖ ⇀⦇ dCert ,POOL⦈ stᵖ'
      ────────────────────────────────
      $\begin{pmatrix} \,\href{Ledger.Conway.Certs.html#7324}{\htmlId{15814}{\htmlClass{Generalizable}{\text{e}}}}\, \\ \,\href{Ledger.Conway.Certs.html#7456}{\htmlId{15818}{\htmlClass{Generalizable}{\text{pp}}}}\, \\ \,\href{Ledger.Conway.Certs.html#7346}{\htmlId{15823}{\htmlClass{Generalizable}{\text{vs}}}}\, \\ \,\href{Ledger.Conway.Certs.html#7075}{\htmlId{15828}{\htmlClass{Generalizable}{\text{wdrls}}}}\, \\ \,\href{Ledger.Conway.Certs.html#7570}{\htmlId{15836}{\htmlClass{Generalizable}{\text{cc}}}}\, \end{pmatrix}$ ⊢ $\begin{pmatrix} \,\href{Ledger.Conway.Certs.html#7510}{\htmlId{15845}{\htmlClass{Generalizable}{\text{stᵈ}}}}\, \\ \,\href{Ledger.Conway.Certs.html#7550}{\htmlId{15851}{\htmlClass{Generalizable}{\text{stᵖ}}}}\, \\ \,\href{Ledger.Conway.Certs.html#7530}{\htmlId{15857}{\htmlClass{Generalizable}{\text{stᵍ}}}}\, \end{pmatrix}$ ⇀⦇ dCert ,CERT⦈ $\begin{pmatrix} \,\href{Ledger.Conway.Certs.html#7510}{\htmlId{15881}{\htmlClass{Generalizable}{\text{stᵈ}}}}\, \\ \,\href{Ledger.Conway.Certs.html#7554}{\htmlId{15887}{\htmlClass{Generalizable}{\text{stᵖ'}}}}\, \\ \,\href{Ledger.Conway.Certs.html#7530}{\htmlId{15894}{\htmlClass{Generalizable}{\text{stᵍ}}}}\, \end{pmatrix}$

  CERT-vdel :
    ∙ Γ ⊢ stᵍ ⇀⦇ dCert ,GOVCERT⦈ stᵍ'
      ────────────────────────────────
      Γ ⊢ $\begin{pmatrix} \,\href{Ledger.Conway.Certs.html#7510}{\htmlId{16004}{\htmlClass{Generalizable}{\text{stᵈ}}}}\, \\ \,\href{Ledger.Conway.Certs.html#7550}{\htmlId{16010}{\htmlClass{Generalizable}{\text{stᵖ}}}}\, \\ \,\href{Ledger.Conway.Certs.html#7530}{\htmlId{16016}{\htmlClass{Generalizable}{\text{stᵍ}}}}\, \end{pmatrix}$ ⇀⦇ dCert ,CERT⦈ $\begin{pmatrix} \,\href{Ledger.Conway.Certs.html#7510}{\htmlId{16040}{\htmlClass{Generalizable}{\text{stᵈ}}}}\, \\ \,\href{Ledger.Conway.Certs.html#7550}{\htmlId{16046}{\htmlClass{Generalizable}{\text{stᵖ}}}}\, \\ \,\href{Ledger.Conway.Certs.html#7534}{\htmlId{16052}{\htmlClass{Generalizable}{\text{stᵍ'}}}}\, \end{pmatrix}$

CERTBASE transition

data _⊢_⇀⦇_,CERTBASE⦈_ where

  CERT-base :
    let refresh          = mapPartial getDRepVote (fromList vs)
        refreshedDReps   = mapValueRestricted (const (e + pp .drepActivity)) dReps refresh
        wdrlCreds        = mapˢ stake (dom wdrls)
        validVoteDelegs  = voteDelegs ∣^ (  mapˢ (credVoter DRep) (dom dReps)
                                        ∪ fromList (noConfidenceRep ∷ abstainRep ∷ []) )
    in
    ∙ filter isKeyHash wdrlCreds ⊆ dom voteDelegs
    ∙ mapˢ (map₁ stake) (wdrls ˢ) ⊆ rewards ˢ
      ────────────────────────────────
      $\begin{pmatrix} \,\href{Ledger.Conway.Certs.html#7324}{\htmlId{16728}{\htmlClass{Generalizable}{\text{e}}}}\, \\ \,\href{Ledger.Conway.Certs.html#7456}{\htmlId{16732}{\htmlClass{Generalizable}{\text{pp}}}}\, \\ \,\href{Ledger.Conway.Certs.html#7346}{\htmlId{16737}{\htmlClass{Generalizable}{\text{vs}}}}\, \\ \,\href{Ledger.Conway.Certs.html#7075}{\htmlId{16742}{\htmlClass{Generalizable}{\text{wdrls}}}}\, \\ \,\href{Ledger.Conway.Certs.html#7570}{\htmlId{16750}{\htmlClass{Generalizable}{\text{cc}}}}\, \end{pmatrix}$ ⊢
        $\begin{pmatrix} \begin{pmatrix} \,\href{Ledger.Conway.Certs.html#6945}{\htmlId{16769}{\htmlClass{Generalizable}{\text{voteDelegs}}}}\, \\ \,\href{Ledger.Conway.Certs.html#6840}{\htmlId{16782}{\htmlClass{Generalizable}{\text{stakeDelegs}}}}\, \\ \,\href{Ledger.Conway.Certs.html#6769}{\htmlId{16796}{\htmlClass{Generalizable}{\text{rewards}}}}\, \end{pmatrix}
        \\ \,\href{Ledger.Conway.Certs.html#7550}{\htmlId{16816}{\htmlClass{Generalizable}{\text{stᵖ}}}}\,
        \\ \begin{pmatrix} \,\href{Ledger.Conway.Certs.html#6799}{\htmlId{16832}{\htmlClass{Generalizable}{\text{dReps}}}}\, \\ \,\href{Ledger.Conway.Certs.html#6887}{\htmlId{16840}{\htmlClass{Generalizable}{\text{ccHotKeys}}}}\, \end{pmatrix}
        \end{pmatrix}$ ⇀⦇ _ ,CERTBASE⦈
        $\begin{pmatrix} \begin{pmatrix} \,\href{Ledger.Conway.Certs.html#16419}{\htmlId{16890}{\htmlClass{Bound}{\text{validVoteDelegs}}}}\, \\ \,\href{Ledger.Conway.Certs.html#6840}{\htmlId{16908}{\htmlClass{Generalizable}{\text{stakeDelegs}}}}\, \\ \,\href{Axiom.Set.Map.html#9130}{\htmlId{16922}{\htmlClass{Function}{\text{constMap}}}}\, \,\href{Ledger.Conway.Certs.html#16369}{\htmlId{16931}{\htmlClass{Bound}{\text{wdrlCreds}}}}\, \,\htmlId{16941}{\htmlClass{Number}{\text{0}}}\, \,\href{Axiom.Set.Map.html#6320}{\htmlId{16943}{\htmlClass{Function Operator}{\text{∪ˡ}}}}\, \,\href{Ledger.Conway.Certs.html#6769}{\htmlId{16946}{\htmlClass{Generalizable}{\text{rewards}}}}\, \end{pmatrix}
        \\ \,\href{Ledger.Conway.Certs.html#7550}{\htmlId{16966}{\htmlClass{Generalizable}{\text{stᵖ}}}}\,
        \\ \begin{pmatrix} \,\href{Ledger.Conway.Certs.html#16278}{\htmlId{16982}{\htmlClass{Bound}{\text{refreshedDReps}}}}\, \\ \,\href{Ledger.Conway.Certs.html#6887}{\htmlId{16999}{\htmlClass{Generalizable}{\text{ccHotKeys}}}}\, \end{pmatrix}
        \end{pmatrix}$

---

1. By “hot” and “cold” credentials we mean the following: a cold credential is used to register a hot credential, and then the hot credential is used for voting. The idea is that the access to the cold credential is kept in a secure location, while the hot credential is more conveniently accessed. If the hot credential is compromised, it can be changed using the cold credential. ↩