Skip to content

Ratification

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

{-# OPTIONS --safe #-}

import Data.Integer as ℤ
open import Data.Rational as ℚ using (ℚ; 0ℚ; _⊔_)
open import Data.Nat.Properties hiding (_≟_; _≤?_)

open import Ledger.Prelude hiding (_∧_; _⊔_) renaming (filterᵐ to filter; ∣_∣ to _↓)
open import Ledger.Conway.Specification.Transaction hiding (Vote)

module Ledger.Conway.Specification.Ratify (txs : _) (open TransactionStructure txs) where

open import Ledger.Conway.Specification.Certs govStructure
open import Ledger.Conway.Specification.Enact govStructure
open import Ledger.Conway.Specification.Gov.Actions govStructure using (Vote)

Governance actions are ratified through on-chain votes. Different kinds of governance actions have different ratification requirements but always involve at least two of the three governance bodies.

A successful motion of no-confidence, election of a new constitutional committee, a constitutional change, or a hard-fork delays ratification of all other governance actions until the first epoch after their enactment. This gives a new constitutional committee enough time to vote on current proposals, re-evaluate existing proposals with respect to a new constitution, and ensures that the (in principle arbitrary) semantic changes caused by enacting a hard-fork do not have unintended consequences in combination with other actions.

Ratification Requirements

Section Functions related to voting details the ratification requirements for each governance action scenario. For a governance action to be ratified, all of these requirements must be satisfied, on top of other conditions that are explained further down. The threshold function is defined as a table, with a row for each type of GovAction and the colums representing the CC, DRep and SPO roles in that order.

The symbols mean the following:

  • vote x: For an action to pass, the fraction of stake associated with yes votes with respect to that associated with yes and no votes must exceed the threshold x.

  • ─: The body of governance does not participate in voting.

  • ✓: The constitutional committee needs to approve an action, with the threshold assigned to it.

  • ✓†: Voting is possible, but the action will never be enacted. This is equivalent to vote 2 (or any other number above 1).

Two rows in this table contain functions that compute the DRep and SPO thresholds simultaneously: the rows for UpdateCommittee and ChangePParams.

For UpdateCommittee, there can be different thresholds depending on whether the system is in a state of no-confidence or not. This information is provided via the ccThreshold argument: if the system is in a state of no-confidence, then ccThreshold is set to nothing.

In case of the ChangePParams action, the thresholds further depend on what groups that action is associated with. pparamThreshold associates a pair of thresholds to each individual group. Since an individual update can contain multiple groups, the actual thresholds are then given by taking the maximum of all those thresholds.

Note that each protocol parameter belongs to exactly one of the four groups that have a DRep threshold, so a DRep vote will always be required. A protocol parameter may or may not be in the SecurityGroup, so an SPO vote may not be required.

Finally, each of the P\(_x\) and Q\(_x\) in Section Functions related to voting are protocol parameters.

private
  ∣_∣_∣_∣ : {A : Type} → A → A → A → GovRole → A
  ∣ q₁ ∣ q₂ ∣ q₃ ∣ = λ { CC → q₁ ; DRep → q₂ ; SPO → q₃ }

  ∣_∥_∣ : {A : Type} → A → A × A → GovRole → A
  ∣ q₁ ∥ (q₂ , q₃) ∣ = λ { CC → q₁ ; DRep → q₂ ; SPO → q₃ }

vote : ℚ → Maybe ℚ
vote = just

defer : ℚ
defer = ℚ.1ℚ ℚ.+ ℚ.1ℚ

maxThreshold : ℙ (Maybe ℚ) → Maybe ℚ
maxThreshold x = foldl comb nothing (proj₁ $ finiteness x)
  where
    comb : Maybe ℚ → Maybe ℚ → Maybe ℚ
    comb (just x) (just y) = just (x ⊔ y)
    comb (just x) nothing  = just x
    comb nothing  (just y) = just y
    comb nothing  nothing  = nothing

─ : Maybe ℚ
─ = nothing
✓† = vote defer

threshold : PParams → Maybe ℚ → GovAction → GovRole → Maybe ℚ
threshold pp ccThreshold ga =
  case  ga ↓ of

        λ where

        (NoConfidence     , _) → ∣ ─   ∣ vote P1      ∣ vote Q1  ∣
        (UpdateCommittee  , _) → ∣ ─   ∥ P/Q2a/b                 ∣
        (NewConstitution  , _) → ∣ ✓   ∣ vote P3      ∣ ─        ∣
        (TriggerHardFork        , _) → ∣ ✓   ∣ vote P4      ∣ vote Q4  ∣
        (ChangePParams    , x) → ∣ ✓   ∥ P/Q5 x                  ∣
        (TreasuryWithdrawal     , _) → ∣ ✓   ∣ vote P6      ∣ ─        ∣
        (Info             , _) → ∣ ✓†  ∣ ✓†           ∣ ✓†       ∣
          where

          open PParams pp
          open DrepThresholds drepThresholds
          open PoolThresholds poolThresholds

          ✓ = maybe just ✓† ccThreshold

          P/Q2a/b : Maybe ℚ × Maybe ℚ
          P/Q2a/b =  case ccThreshold of

            λ where

                     (just _)  → (vote P2a , vote Q2a)
                     nothing   → (vote P2b , vote Q2b)

          pparamThreshold : PParamGroup → Maybe ℚ × Maybe ℚ
          pparamThreshold NetworkGroup     = (vote P5a  , ─         )
          pparamThreshold EconomicGroup    = (vote P5b  , ─         )
          pparamThreshold TechnicalGroup   = (vote P5c  , ─         )
          pparamThreshold GovernanceGroup  = (vote P5d  , ─         )
          pparamThreshold SecurityGroup    = (─         , vote Q5   )

          P/Q5 : PParamsUpdate → Maybe ℚ × Maybe ℚ
          P/Q5 ppu = maxThreshold (mapˢ (proj₁ ∘ pparamThreshold) (updateGroups ppu))
                   , maxThreshold (mapˢ (proj₂ ∘ pparamThreshold) (updateGroups ppu))

canVote : PParams → GovAction → GovRole → Type
canVote pp a r = Is-just (threshold pp nothing a r)

Protocol Parameters and Governance Actions

Voting thresholds for protocol parameters can be set by group, and we do not require that each protocol parameter governance action be confined to a single group. In case a governance action carries updates for multiple parameters from different groups, the maximum threshold of all the groups involved will apply to any given such governance action.

The purpose of the SecurityGroup is to add an additional check to security-relevant protocol parameters. Any proposal that includes a change to a security-relevant protocol parameter must also be accepted by at least half of the SPO stake.

Ratification Restrictions

Types and functions for the RATIFY transition system

record StakeDistrs : Type where
  field
    stakeDistrVDeleg  : VDeleg  ⇀ Coin
    stakeDistrPools   : KeyHash ⇀ Coin

record RatifyEnv : Type where
  field
    stakeDistrs   : StakeDistrs
    currentEpoch  : Epoch
    dreps         : Credential ⇀ Epoch
    ccHotKeys     : Credential ⇀ Maybe Credential
    treasury      : Treasury
    pools         : KeyHash ⇀ StakePoolParams
    delegatees    : VoteDelegs

record RatifyState : Type where
  field
    es              : EnactState
    removed         : ℙ (GovActionID × GovActionState)
    delay           : Bool

record HasRatifyState {a} (A : Type a) : Type a where
  field RatifyStateOf : A → RatifyState
open HasRatifyState ⦃...⦄ public

instance
  HasEnactState-RatifyState : HasEnactState RatifyState
  HasEnactState-RatifyState .EnactStateOf = RatifyState.es

  HasTreasury-RatifyEnv : HasTreasury RatifyEnv
  HasTreasury-RatifyEnv .TreasuryOf = RatifyEnv.treasury

As mentioned earlier, most governance actions must include a GovActionID for the most recently enacted action of its given type. Consequently, two actions of the same type can be enacted at the same time, but they must be deliberately designed to do so.

Section Types and functions for the RATIFY transition system defines some types and functions used in the RATIFY transition system.

instance
  unquoteDecl HasCast-StakeDistrs HasCast-RatifyEnv HasCast-RatifyState = derive-HasCast
    (   (quote StakeDistrs , HasCast-StakeDistrs)
    ∷   (quote RatifyEnv , HasCast-RatifyEnv)
    ∷ [ (quote RatifyState , HasCast-RatifyState) ])

Vote Counting

Section Vote counting for CC and Section Vote counting for DReps and Section Vote counting for SPOs define the acceptedBy predicate for each of the governance bodies. Given the current state of the votes and other parts of the system these functions calculate whether a governance action is ratified by the corresponding body.

Constitutional Commitee

Vote counting for CC

acceptedByCC
  : RatifyEnv
  → EnactState
  → GovActionState
  → Type
acceptedByCC Γ eSt gaSt = (acceptedStake /₀ totalStake) ≥ t
  × (maybe (λ (m , _) → lengthˢ m) 0 (proj₁ cc) ≥ ccMinSize ⊎ Is-nothing mT)
  where

    open EnactState eSt using (cc; pparams)
    open RatifyEnv Γ
    open PParams (proj₁ pparams)
    open GovActionState gaSt
    open GovVotes votes using (gvCC)

    castVotes : Credential ⇀ Vote
    castVotes = gvCC

    getCCHotCred : Credential × Epoch → Maybe Credential
    getCCHotCred (c , e) =
      if currentEpoch > e
        then nothing -- credential has expired
        else case lookupᵐ? ccHotKeys c of

          λ where

          (just (just c'))  → just c'
          _                 → nothing -- hot key not registered or resigned

    actualVote : Credential → Epoch → Vote
    actualVote c e = case getCCHotCred (c , e) of

      λ where

        (just c')  → maybe id Vote.no (lookupᵐ? castVotes c')
        _          → Vote.abstain

    actualVotes : Credential ⇀ Vote
    actualVotes = case proj₁ cc of

      λ where

        nothing         →  ∅
        (just (m , _))  →  if ccMinSize ≤ lengthˢ (mapFromPartialFun getCCHotCred (m ˢ))
                           then mapWithKey actualVote m
                           else constMap (dom m) Vote.no

    mT : Maybe ℚ
    mT = threshold (proj₁ pparams) (proj₂ <$> (proj₁ cc)) action CC

    t : ℚ
    t = maybe id 0ℚ mT

    stakeDistr : Credential ⇀ Coin
    stakeDistr = constMap (dom actualVotes) 1

    acceptedStake totalStake : Coin
    acceptedStake  = ∑[ x ← stakeDistr ∣ actualVotes ⁻¹ Vote.yes                           ] x
    totalStake     = ∑[ x ← stakeDistr ∣ dom (actualVotes ∣^ (❴ Vote.yes ❵ ∪ ❴ Vote.no ❵))  ] x

Section Vote counting for CC defines the acceptedByCC predicate. This predicate utilizes the following auxiliary definitions:

  • castVotes: This map contains the votes that have been cast by members of the CC body and are part of the GovActionState gaSt.

  • getCCHotCred: This function maps a Credential and an Epoch to the hot key corresponding with the given credential, in case this has not expired.

  • actualVote: This function sets the default vote for CC members. If the given CC member term has expired, they have not yet registered a hot key, or they have resigned, then returns abstain; if none of these conditions is met, then

  • if the CC member has voted, then that vote is returned;

  • if the CC member has not voted, then the default value of no is returned.

  • actualVotes: This map contains the actual votes of the CC body. If the commitee does not exists then it is the empty map, otherwise if

  • the number of CC members with a registered hot key is greater than the protocol parameter ccMinSize, then actualVote is returned (as a map), otherwise;

  • all commitee members vote no

  • mT: This is the threshold of the CC. It may be nothing.

  • stakeDistr computes the stake distribution. Note that every constitutional committe member has a stake of 1, giving them equal voting power. However, just as with other delegation, multiple CC members can delegate to the same hot key, giving that hot key the power of those multiple votes with a single actual vote.

  • acceptedStake and totalStake: These amounts correspond to the portion of the stake from the CC members that has voted yes and that which has voted yes or no.

In addition, it has to be the case that either

  • the size of the CC is greater than ccMinSize, or

  • the threshold function returns nothing

Delegated Representatives

Vote counting for DReps

acceptedByDRep
  : RatifyEnv
  → EnactState
  → GovActionState
  → Type
acceptedByDRep Γ eSt gaSt = (acceptedStake /₀ totalStake) ≥ t
  where

    open EnactState eSt using (cc; pparams)
    open RatifyEnv Γ
    open PParams (proj₁ pparams)
    open StakeDistrs stakeDistrs
    open GovActionState gaSt
    open GovVotes votes using (gvDRep)

    castVotes : VDeleg ⇀ Vote
    castVotes = mapKeys vDelegCredential gvDRep

    activeDReps : ℙ Credential
    activeDReps = dom (filter (λ (_ , e) → currentEpoch ≤ e) dreps)

    predeterminedDRepVotes : VDeleg ⇀ Vote
    predeterminedDRepVotes = case gaType action of

      λ where

        NoConfidence → ❴ vDelegAbstain , Vote.abstain ❵ ∪ˡ ❴ vDelegNoConfidence , Vote.yes ❵
        _            → ❴ vDelegAbstain , Vote.abstain ❵ ∪ˡ ❴ vDelegNoConfidence , Vote.no  ❵

    defaultDRepCredentialVotes : VDeleg ⇀ Vote
    defaultDRepCredentialVotes = constMap (mapˢ vDelegCredential activeDReps) Vote.no

    actualVotes : VDeleg ⇀ Vote
    actualVotes  = castVotes ∪ˡ defaultDRepCredentialVotes
                               ∪ˡ predeterminedDRepVotes

    t : ℚ
    t = maybe id 0ℚ (threshold (proj₁ pparams) (proj₂ <$> (proj₁ cc)) action DRep)

    acceptedStake totalStake : Coin
    acceptedStake  = ∑[ x ← stakeDistrVDeleg ∣ actualVotes ⁻¹ Vote.yes                          ] x
    totalStake     = ∑[ x ← stakeDistrVDeleg ∣ dom (actualVotes ∣^ (❴ Vote.yes ❵ ∪ ❴ Vote.no ❵)) ] x

Section Vote counting for DReps defines the predicate acceptedByDRep. This predicate is defined using some auxiliary definitions:

  • activeDReps: This set contains all DReps whose term has not expired.

  • predeterminedDRepVotes: This map collects the predetermined votes for the VDeleg. It depends on the governance action at hand.

  • defaultDRepCredentialVote: This map sets the default vote to no for all the active DReps.

  • actualVotes: This map joins together in order of preference: the cast votes, the default votes and the predetermined votes.

  • acceptedStake and totalStake: These amounts correspond to the portion of the stake from the DRep members that has voted yes and that which has voted yes or no.

Stake Pool Operators

Vote counting for SPOs

acceptedBySPO
  : RatifyEnv
  → EnactState
  → GovActionState
  → Type
acceptedBySPO Γ eSt gaSt = (acceptedStake /₀ totalStake) ≥ t
  where

    open EnactState eSt using (cc; pparams)
    open RatifyEnv Γ
    open StakeDistrs stakeDistrs
    open GovActionState gaSt
    open GovVotes votes using (gvSPO)

    castVotes : KeyHash ⇀ Vote
    castVotes = gvSPO

    defaultVote : KeyHash → Vote
    defaultVote kh = case lookupᵐ? pools kh of

      λ where

      nothing   → Vote.no
      (just  p) → case lookupᵐ? delegatees (StakePoolParams.rewardAccount p) , gaType action of

             λ where

             (_                       , TriggerHardFork)  → Vote.no
             (just vDelegNoConfidence , NoConfidence   )  → Vote.yes
             (just vDelegAbstain      , _              )  → Vote.abstain
             _                                            → Vote.no

    actualVotes : KeyHash ⇀ Vote
    actualVotes = castVotes ∪ˡ mapFromFun defaultVote (dom stakeDistrPools)

    t : ℚ
    t = maybe id 0ℚ (threshold (proj₁ pparams) (proj₂ <$> (proj₁ cc)) action SPO)

    acceptedStake totalStake : Coin
    acceptedStake  = ∑[ x ← stakeDistrPools ∣ actualVotes ⁻¹ Vote.yes                          ] x
    totalStake     = ∑[ x ← stakeDistrPools ∣ dom (actualVotes ∣^ (❴ Vote.yes ❵ ∪ ❴ Vote.no ❵)) ] x

Section Vote counting for SPOs, defines the predicate acceptedBySPO, which uses the following auxiliary definitions:

  • castVotes: This map contains the votes that have been cast by members of the SPO body and have been collected as part of the GovActionState gaSt.

  • defaultVote: This map sets a default vote to all SPOs who didn’t vote, with the default depending on the given action, and whether the SPO has delegated their vote to one of the default DReps.

  • actualVotes: This map combines the votes cast by SPOs with defaultVote using a left-biased union making cast votes take precedence over default votes.

  • t: This rational is the threshold used to calculate if the action is ratified by the SPO body.

  • acceptedStake and totalStake: These amounts correspond to the portion of the stake from the SPOs that has voted yes and that which has voted yes or no. Note that it uses the stake distribution stakeDistrPools as provided in the environment.

Let us discuss in more detail the way SPO votes are counted, as the ledger specification’s handling of this has evolved in response to community feedback. Previously, if an SPO did not vote, then it would be counted as having voted abstain by default. Members of the SPO community found this behavior counterintuitive and requested that non-voters be assigned a no vote by default, with the caveat that an SPO could change its default setting by delegating its reward account credential to an AlwaysNoConfidence DRep or an AlwaysAbstain DRep. (This change applies only after the bootstrap period; during the bootstrap period the logic is unchanged; see Section Bootstrapping the Governance System.) To be precise, the agreed upon specification is the following: an SPO that did not vote is assumed to have voted no, except under the following circumstances:

  • if the SPO has delegated its reward credential to an AlwaysNoConfidence DRep, then their default vote is yes for NoConfidence proposals and no for other proposals;

  • if the SPO has delegated its reward credential to an AlwaysAbstain DRep, then its default vote is abstain for all proposals.

It is important to note that the credential that can now be used to set a default voting behavior is the credential used to withdraw staking rewards, which is not (in general) the same as the credential used for voting.

abstract

  accepted : RatifyEnv → EnactState → GovActionState → Type
  accepted Γ es gs = acceptedByCC Γ es gs × acceptedByDRep Γ es gs × acceptedBySPO Γ es gs

  expired : Epoch → GovActionState → Type
  expired current record { expiresIn = expiresIn } = expiresIn < current

The accepted and expired functions just defined are used in the rules of RATIFY.

open EnactState

verifyPrev : (a : GovActionType) → NeedsHash a → EnactState → Type
verifyPrev NoConfidence        h es  = h ≡ es .cc .proj₂
verifyPrev UpdateCommittee     h es  = h ≡ es .cc .proj₂
verifyPrev NewConstitution     h es  = h ≡ es .constitution .proj₂
verifyPrev TriggerHardFork     h es  = h ≡ es .pv .proj₂
verifyPrev ChangePParams       h es  = h ≡ es .pparams .proj₂
verifyPrev TreasuryWithdrawal  _ _   = ⊤
verifyPrev Info                _ _   = ⊤

delayingAction : GovActionType → Bool
delayingAction NoConfidence        = true
delayingAction UpdateCommittee     = true
delayingAction NewConstitution     = true
delayingAction TriggerHardFork     = true
delayingAction ChangePParams       = false
delayingAction TreasuryWithdrawal  = false
delayingAction Info                = false

delayed : (a : GovActionType) → NeedsHash a → EnactState → Bool → Type
delayed gaTy h es d = ¬ verifyPrev gaTy h es ⊎ d ≡ true

acceptConds : RatifyEnv → RatifyState → GovActionID × GovActionState → Type
acceptConds Γ stʳ (id , st) =
       accepted Γ es st
    ×  ¬ delayed (gaType action) prevAction es delay
    × ∃[ es' ]  $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Ratify.html#23692}{\htmlId{23798}{\htmlClass{Bound}{\text{id}}}}\, \\ \,\href{Ledger.Conway.Specification.Ratify.html#8276}{\htmlId{23803}{\htmlClass{Function}{\text{treasury}}}}\, \\ \,\href{Ledger.Conway.Specification.Ratify.html#8161}{\htmlId{23814}{\htmlClass{Function}{\text{currentEpoch}}}}\, \end{pmatrix}$ ⊢ es ⇀⦇ action ,ENACT⦈ es'

    where open RatifyEnv Γ
          open RatifyState stʳ
          open GovActionState st

abstract
  verifyPrev? : ∀ a h es → Dec (verifyPrev a h es)
  verifyPrev? NoConfidence        h es = dec
  verifyPrev? UpdateCommittee     h es = dec
  verifyPrev? NewConstitution     h es = dec
  verifyPrev? TriggerHardFork     h es = dec
  verifyPrev? ChangePParams       h es = dec
  verifyPrev? TreasuryWithdrawal  h es = dec
  verifyPrev? Info                h es = dec

  delayed? : ∀ a h es d → Dec (delayed a h es d)
  delayed? a h es d = let instance _ = ⁇ verifyPrev? a h es in dec

  Is-nothing? : ∀ {A : Set} {x : Maybe A} → Dec (Is-nothing x)
  Is-nothing? {x = x} = All.dec (const $ no id) x
    where
        import Data.Maybe.Relation.Unary.All as All

  accepted? : ∀ Γ es st → Dec (accepted Γ es st)
  accepted? Γ es st = acceptedByCC? Γ es st ×-dec acceptedByDRep? Γ es st ×-dec acceptedBySPO? Γ es st
    where
     acceptedByCC? : ∀ Γ es st → Dec (acceptedByCC Γ es st)
     acceptedByCC? _ _ _ = _ ℚ.≤? _ ×-dec (_ ≥? _ ⊎-dec Is-nothing?)

     acceptedByDRep? : ∀ Γ es st → Dec (acceptedByDRep Γ es st)
     acceptedByDRep? _ _ _ = _ ℚ.≤? _

     acceptedBySPO? : ∀ Γ es st → Dec (acceptedBySPO Γ es st)
     acceptedBySPO? _ _ _ = _ ℚ.≤? _

  expired? : ∀ e st → Dec (expired e st)
  expired? e st = ¿ expired e st ¿

The functions defined above deal with delays and the acceptance criterion for ratification. A given action can either be delayed if the action contained in EnactState isn’t the one the given action is building on top of, which is checked by verifyPrev, or if a previous action was a delayingAction. Note that delayingAction affects the future: whenever a delayingAction is accepted all future actions are delayed. delayed then expresses the condition whether an action is delayed. This happens either because the previous action doesn’t match the current one, or because the previous action was a delaying one. This information is passed in as an argument.

private variable
  Γ : RatifyEnv
  es es' : EnactState
  a : GovActionID × GovActionState
  removed : ℙ (GovActionID × GovActionState)
  d : Bool

open RatifyEnv
open GovActionState

Types of the RATIFY and RATIFIES transition systems

data

  _⊢_⇀⦇_,RATIFY⦈_ : RatifyEnv → RatifyState → GovActionID × GovActionState → RatifyState → Type

_⊢_⇀⦇_,RATIFIES⦈_  : RatifyEnv → RatifyState → List (GovActionID × GovActionState)
                   → RatifyState → Type

The RATIFY transition system

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

  RATIFY-Accept :
    let treasury       = TreasuryOf Γ
        e              = Γ .currentEpoch
        (gaId , gaSt)  = a
        action         = GovActionOf gaSt
    in
    ∙ acceptConds Γ $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Ratify.html#26025}{\htmlId{26831}{\htmlClass{Generalizable}{\text{es}}}}\, \\ \,\href{Ledger.Conway.Specification.Ratify.html#26082}{\htmlId{26836}{\htmlClass{Generalizable}{\text{removed}}}}\, \\ \,\href{Ledger.Conway.Specification.Ratify.html#26127}{\htmlId{26846}{\htmlClass{Generalizable}{\text{d}}}}\, \end{pmatrix}$ a
    ∙ $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Ratify.html#26742}{\htmlId{26860}{\htmlClass{Bound}{\text{gaId}}}}\, \\ \,\href{Ledger.Conway.Specification.Ratify.html#26662}{\htmlId{26867}{\htmlClass{Bound}{\text{treasury}}}}\, \\ \,\href{Ledger.Conway.Specification.Ratify.html#26700}{\htmlId{26878}{\htmlClass{Bound}{\text{e}}}}\, \end{pmatrix}$ ⊢ es ⇀⦇ action ,ENACT⦈ es'
      ────────────────────────────────
      Γ ⊢ $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Ratify.html#26025}{\htmlId{26960}{\htmlClass{Generalizable}{\text{es}}}}\,  \\ \,\href{Ledger.Conway.Specification.Ratify.html#26082}{\htmlId{26966}{\htmlClass{Generalizable}{\text{removed}}}}\,         \\ \,\href{Ledger.Conway.Specification.Ratify.html#26127}{\htmlId{26984}{\htmlClass{Generalizable}{\text{d}}}}\,                     \end{pmatrix}$ ⇀⦇ a ,RATIFY⦈
          $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Ratify.html#26028}{\htmlId{27034}{\htmlClass{Generalizable}{\text{es'}}}}\, \\ \,\href{Class.HasSingleton.html#288}{\htmlId{27040}{\htmlClass{Field Operator}{\text{❴}}}}\, \,\href{Ledger.Conway.Specification.Ratify.html#26047}{\htmlId{27042}{\htmlClass{Generalizable}{\text{a}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{27044}{\htmlClass{Field Operator}{\text{❵}}}}\, \,\href{Axiom.Set.html#8952}{\htmlId{27046}{\htmlClass{Function Operator}{\text{∪}}}}\, \,\href{Ledger.Conway.Specification.Ratify.html#26082}{\htmlId{27048}{\htmlClass{Generalizable}{\text{removed}}}}\, \\ \,\href{Ledger.Conway.Specification.Ratify.html#23133}{\htmlId{27058}{\htmlClass{Function}{\text{delayingAction}}}}\, \,\htmlId{27073}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Conway.Specification.Gov.Actions.html#2930}{\htmlId{27074}{\htmlClass{Field}{\text{gaType}}}}\, \,\href{Ledger.Conway.Specification.Ratify.html#26768}{\htmlId{27081}{\htmlClass{Bound}{\text{action}}}}\,\,\htmlId{27087}{\htmlClass{Symbol}{\text{)}}}\, \end{pmatrix}$

  RATIFY-Reject :
    let e              = Γ .currentEpoch
        (gaId , gaSt)  = a
    in
    ∙ ¬ acceptConds Γ $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Ratify.html#26025}{\htmlId{27209}{\htmlClass{Generalizable}{\text{es}}}}\, \\ \,\href{Ledger.Conway.Specification.Ratify.html#26082}{\htmlId{27214}{\htmlClass{Generalizable}{\text{removed}}}}\, \\ \,\href{Ledger.Conway.Specification.Ratify.html#26127}{\htmlId{27224}{\htmlClass{Generalizable}{\text{d}}}}\, \end{pmatrix}$ a
    ∙ expired e gaSt
      ────────────────────────────────
      Γ ⊢ $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Ratify.html#26025}{\htmlId{27302}{\htmlClass{Generalizable}{\text{es}}}}\, \\ \,\href{Ledger.Conway.Specification.Ratify.html#26082}{\htmlId{27307}{\htmlClass{Generalizable}{\text{removed}}}}\, \\ \,\href{Ledger.Conway.Specification.Ratify.html#26127}{\htmlId{27317}{\htmlClass{Generalizable}{\text{d}}}}\, \end{pmatrix}$ ⇀⦇ a ,RATIFY⦈ $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Ratify.html#26025}{\htmlId{27337}{\htmlClass{Generalizable}{\text{es}}}}\, \\ \,\href{Class.HasSingleton.html#288}{\htmlId{27342}{\htmlClass{Field Operator}{\text{❴}}}}\, \,\href{Ledger.Conway.Specification.Ratify.html#26047}{\htmlId{27344}{\htmlClass{Generalizable}{\text{a}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{27346}{\htmlClass{Field Operator}{\text{❵}}}}\, \,\href{Axiom.Set.html#8952}{\htmlId{27348}{\htmlClass{Function Operator}{\text{∪}}}}\, \,\href{Ledger.Conway.Specification.Ratify.html#26082}{\htmlId{27350}{\htmlClass{Generalizable}{\text{removed}}}}\, \\ \,\href{Ledger.Conway.Specification.Ratify.html#26127}{\htmlId{27360}{\htmlClass{Generalizable}{\text{d}}}}\, \end{pmatrix}$

  RATIFY-Continue :
     let e              = Γ .currentEpoch
         (gaId , gaSt)  = a
     in
     ∙ ¬ acceptConds Γ $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Ratify.html#26025}{\htmlId{27488}{\htmlClass{Generalizable}{\text{es}}}}\, \\ \,\href{Ledger.Conway.Specification.Ratify.html#26082}{\htmlId{27493}{\htmlClass{Generalizable}{\text{removed}}}}\, \\ \,\href{Ledger.Conway.Specification.Ratify.html#26127}{\htmlId{27503}{\htmlClass{Generalizable}{\text{d}}}}\, \end{pmatrix}$ a
     ∙ ¬ expired e gaSt
       ────────────────────────────────
       Γ ⊢ $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Ratify.html#26025}{\htmlId{27586}{\htmlClass{Generalizable}{\text{es}}}}\, \\ \,\href{Ledger.Conway.Specification.Ratify.html#26082}{\htmlId{27591}{\htmlClass{Generalizable}{\text{removed}}}}\, \\ \,\href{Ledger.Conway.Specification.Ratify.html#26127}{\htmlId{27601}{\htmlClass{Generalizable}{\text{d}}}}\, \end{pmatrix}$ ⇀⦇ a ,RATIFY⦈ $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Ratify.html#26025}{\htmlId{27621}{\htmlClass{Generalizable}{\text{es}}}}\, \\ \,\href{Ledger.Conway.Specification.Ratify.html#26082}{\htmlId{27626}{\htmlClass{Generalizable}{\text{removed}}}}\, \\ \,\href{Ledger.Conway.Specification.Ratify.html#26127}{\htmlId{27636}{\htmlClass{Generalizable}{\text{d}}}}\, \end{pmatrix}$

_⊢_⇀⦇_,RATIFIES⦈_ = ReflexiveTransitiveClosure {sts = _⊢_⇀⦇_,RATIFY⦈_}

The RATIFIES transition system is defined as the reflexive-transitive closure of RATIFY, which is defined via three rules, defined in Section The RATIFY transition system.

  • RATIFYAccept checks if the votes for a given GovAction meet the threshold required for acceptance, that the action is accepted and not delayed, and RATIFYAccept ratifies the action.

  • RATIFYReject asserts that the given GovAction is not accepted and expired; it removes the governance action.

  • RATIFYContinue covers the remaining cases and keeps the GovAction around for further voting.

Note that all governance actions eventually either get accepted and enacted via RATIFYAccept or rejected via RATIFYReject. If an action satisfies all criteria to be accepted but cannot be enacted anyway, it is kept around and tried again at the next epoch boundary.

We never remove actions that do not attract sufficient yes votes before they expire, even if it is clear to an outside observer that this action will never be enacted. Such an action will simply keep getting checked every epoch until it expires.