Ratification

This section is part of the Ledger.Conway.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.Transaction hiding (Vote)

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

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

infixr  _∧_
_∧_ = _×_

instance
  _ = +-0-commutativeMonoid

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

Figure '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 argument: if the system is in a state of no-confidence, then 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 Figure 'Functions-related-to-voting' are protocol parameters.

Functions related to voting

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      ∣ ─        ∣
        (TriggerHF        , _) → ∣ ✓   ∣ vote P4      ∣ vote Q4  ∣
        (ChangePParams    , x) → ∣ ✓   ∥ P/Q5 x                  ∣
        (TreasuryWdrl     , _) → ∣ ✓   ∣ 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
    stakeDistr  : VDeleg ⇀ Coin

record RatifyEnv : Type where
  field
    stakeDistrs   : StakeDistrs
    currentEpoch  : Epoch
    dreps         : Credential ⇀ Epoch
    ccHotKeys     : Credential ⇀ Maybe Credential
    treasury      : Coin
    pools         : KeyHash ⇀ PoolParams
    delegatees    : Credential ⇀ VDeleg

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

CCData : Type
CCData = Maybe ((Credential ⇀ Epoch) × ℚ)

govRole : VDeleg → GovRole
govRole (credVoter gv _)  = gv
govRole abstainRep        = DRep
govRole noConfidenceRep   = DRep

IsCC IsDRep IsSPO : VDeleg → Type
IsCC    v = govRole v ≡ CC
IsDRep  v = govRole v ≡ DRep
IsSPO   v = govRole v ≡ SPO

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.

Figure 'Types-and-functions-for-the-RATIFY-transition-system' defines some types and functions used in the RATIFY transition system. CCData is simply an alias to define some functions more easily.

Vote counting

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

open StakeDistrs

actualVotes  : RatifyEnv → PParams → CCData → GovActionType
             → (GovRole × Credential ⇀ Vote) → (VDeleg ⇀ Vote)
actualVotes Γ pparams cc gaTy votes
  =   mapKeys (credVoter CC) actualCCVotes  ∪ˡ actualPDRepVotes gaTy
  ∪ˡ  actualDRepVotes                       ∪ˡ actualSPOVotes gaTy
  where

  open RatifyEnv Γ
  open PParams pparams

  roleVotes : GovRole → VDeleg ⇀ Vote
  roleVotes r = mapKeys (uncurry credVoter) (filter (λ (x , _) → r ≡ proj₁ x) votes)

  activeDReps = dom (filter (λ (_ , e) → currentEpoch ≤ e) dreps)
  spos  = filterˢ IsSPO (dom (stakeDistr stakeDistrs))

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

      λ where

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

  SPODefaultVote : GovActionType → VDeleg → Vote
  SPODefaultVote gaT (credVoter SPO (KeyHashObj kh)) = case lookupᵐ? pools kh of

      λ where

        nothing → Vote.no
        (just  p) → case lookupᵐ? delegatees (PoolParams.rewardAccount p) , gaTy of

               λ where

               (_                     , TriggerHF)     → Vote.no
               (just noConfidenceRep  , NoConfidence)  → Vote.yes
               (just abstainRep       , _           )  → Vote.abstain
               _                                       → Vote.no
  SPODefaultVote _ _ = Vote.no

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

      λ where

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

  actualCCVotes : Credential ⇀ Vote
  actualCCVotes = case cc of

      λ where

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

  actualPDRepVotes : GovActionType → VDeleg ⇀ Vote
  actualPDRepVotes NoConfidence
                      = ❴ abstainRep , Vote.abstain ❵ ∪ˡ ❴ noConfidenceRep , Vote.yes ❵
  actualPDRepVotes _  = ❴ abstainRep , Vote.abstain ❵ ∪ˡ ❴ noConfidenceRep , Vote.no ❵

  actualDRepVotes : VDeleg ⇀ Vote
  actualDRepVotes  =   roleVotes DRep
                   ∪ˡ  constMap (mapˢ (credVoter DRep) activeDReps) Vote.no

  actualSPOVotes : GovActionType → VDeleg ⇀ Vote
  actualSPOVotes gaTy = roleVotes SPO ∪ˡ mapFromFun (SPODefaultVote gaTy) spos

Figure 'Vote-counting' defines the actualVotes function. Given the current state about votes and other parts of the system it calculates a new mapping of votes, which is the mapping that will actually be used during ratification. Things such as default votes or resignation/expiry are implemented in this way.

actualVotes is defined as the union of four voting maps, corresponding to the constitutional committee, predefined (or auto) DReps, regular DReps and SPOs.

• roleVotes filters the votes based on the given governance role and is a helper for definitions further down.

• if a CC member has not yet registered a hot key, has expired, or has resigned, then actualCCVote 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.

• actualDRepVotes adds a default vote of no to all active DReps that didn’t vote.

• actualSPOVotes adds a default vote to all SPOs who didn’t vote, with the default depending on the action.

Let us discuss the last item above—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 'sec:conway-bootstrap-gov' (unresolved reference).) To be precise, the agreed upon specification is the following: an SPO that did not vote is assumed to have vote 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.

Functions related to ratification

open RatifyEnv using (stakeDistrs)

abstract
  -- unused, keep until we know for sure that there'll be no minimum AVS
  -- activeVotingStake : ℙ VDeleg → StakeDistrs → (VDeleg ⇀ Vote) → Coin
  -- activeVotingStake cc dists votes =
  --   ∑[ x  ← getStakeDist DRep cc dists ∣ dom votes ᶜ ᶠᵐ ] x

--  _/₀_ : ℕ → ℕ → ℚ
--  x /₀ 0 = 0ℚ
--  x /₀ y@(suc _) = ℤ.+ x ℚ./ y

  getStakeDist : GovRole → ℙ VDeleg → StakeDistrs → VDeleg ⇀ Coin
  getStakeDist CC    cc  sd  = constMap (filterˢ IsCC cc) 
  getStakeDist DRep  _   sd  = filterKeys IsDRep  (sd .stakeDistr)
  getStakeDist SPO   _   sd  = filterKeys IsSPO   (sd .stakeDistr)

  acceptedStakeRatio : GovRole → ℙ VDeleg → StakeDistrs → (VDeleg ⇀ Vote) → ℚ
  acceptedStakeRatio r cc dists votes = acceptedStake /₀ totalStake
    where
      dist : VDeleg ⇀ Coin
      dist = getStakeDist r cc dists
      acceptedStake totalStake : Coin
      acceptedStake  = ∑[ x ← dist ∣ votes ⁻¹ Vote.yes                              ] x
      totalStake     = ∑[ x ← dist ∣ dom (votes ∣^ (❴ Vote.yes ❵ ∪ ❴ Vote.no ❵))  ] x

  acceptedBy : RatifyEnv → EnactState → GovActionState → GovRole → Type
  acceptedBy Γ (record { cc = cc , _; pparams = pparams , _ }) gs role =
    let open GovActionState gs; open PParams pparams
        votes'  = actualVotes Γ pparams cc (gaType action) votes
        mbyT    = threshold pparams (proj₂ <$> cc) action role
        t       = maybe id 0ℚ mbyT
    in acceptedStakeRatio role (dom votes') (stakeDistrs Γ) votes' ≥ t
     ∧ (role ≡ CC → maybe (λ (m , _) → lengthˢ m)  cc ≥ ccMinSize ⊎ Is-nothing mbyT)

  accepted : RatifyEnv → EnactState → GovActionState → Type
  accepted Γ es gs = acceptedBy Γ es gs CC ∧ acceptedBy Γ es gs DRep ∧ acceptedBy Γ es gs SPO

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

Figure 'Functions-related-to-ratification' defines the accepted and expired functions (together with some helpers) that are used in the rules of RATIFY.

• getStakeDist computes the stake distribution based on the given governance role and the corresponding delegations. 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.

• acceptedStakeRatio is the ratio of accepted stake. It is computed as the ratio of yes votes over the votes that didn’t abstain. The latter is equivalent to the sum of yes and no votes. The special division symbol /₀ indicates that in case of a division by 0, the numbers 0 should be returned. This implies that in the absence of stake, an action can only pass if the threshold is also set to 0.

• acceptedBy looks up the threshold in the threshold table and compares it to the result of acceptedStakeRatio.

• accepted then checks if an action is accepted by all roles; and

• expired checks whether a governance action is expired in a given epoch.

Functions related to ratification, continued

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 TriggerHF        h es  = h ≡ es .pv .proj₂
verifyPrev ChangePParams    h es  = h ≡ es .pparams .proj₂
verifyPrev TreasuryWdrl     _ _   = ⊤
verifyPrev Info             _ _   = ⊤

delayingAction : GovActionType → Bool
delayingAction NoConfidence     = true
delayingAction UpdateCommittee  = true
delayingAction NewConstitution  = true
delayingAction TriggerHF        = true
delayingAction ChangePParams    = false
delayingAction TreasuryWdrl     = 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.Ratify.html#19960}{\htmlId{20066}{\htmlClass{Bound}{\text{id}}}}\, \\ \,\href{Ledger.Conway.Ratify.html#8004}{\htmlId{20071}{\htmlClass{Function}{\text{treasury}}}}\, \\ \,\href{Ledger.Conway.Ratify.html#7889}{\htmlId{20082}{\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? TriggerHF       h es = dec
  verifyPrev? ChangePParams   h es = dec
  verifyPrev? TreasuryWdrl    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

  acceptedBy? : ∀ Γ es st role → Dec (acceptedBy Γ es st role)
  acceptedBy? _ _ _ _ = _ ℚ.≤? _ ×-dec _ ≟ _ →-dec (_ ≥? _ ⊎-dec Is-nothing?)
    where
      import Relation.Nullary.Decidable as Dec

  accepted? : ∀ Γ es st → Dec (accepted Γ es st)
  accepted? Γ es st = let a = λ {x} → acceptedBy? Γ es st x in a ×-dec a ×-dec a

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

Figure 'Functions-related-to-ratification,-continued' defines functions that 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       = Γ .treasury
        e              = Γ .currentEpoch
        (gaId , gaSt)  = a
        action         = gaSt .action
    in
    ∙ acceptConds Γ $\begin{pmatrix} \,\href{Ledger.Conway.Ratify.html#22229}{\htmlId{23030}{\htmlClass{Generalizable}{\text{es}}}}\, \\ \,\href{Ledger.Conway.Ratify.html#22286}{\htmlId{23035}{\htmlClass{Generalizable}{\text{removed}}}}\, \\ \,\href{Ledger.Conway.Ratify.html#22331}{\htmlId{23045}{\htmlClass{Generalizable}{\text{d}}}}\, \end{pmatrix}$ a
    ∙ $\begin{pmatrix} \,\href{Ledger.Conway.Ratify.html#22945}{\htmlId{23059}{\htmlClass{Bound}{\text{gaId}}}}\, \\ \,\href{Ledger.Conway.Ratify.html#22866}{\htmlId{23066}{\htmlClass{Bound}{\text{treasury}}}}\, \\ \,\href{Ledger.Conway.Ratify.html#22903}{\htmlId{23077}{\htmlClass{Bound}{\text{e}}}}\, \end{pmatrix}$ ⊢ es ⇀⦇ action ,ENACT⦈ es'
      ────────────────────────────────
      Γ ⊢ $\begin{pmatrix} \,\href{Ledger.Conway.Ratify.html#22229}{\htmlId{23159}{\htmlClass{Generalizable}{\text{es}}}}\,  \\ \,\href{Ledger.Conway.Ratify.html#22286}{\htmlId{23165}{\htmlClass{Generalizable}{\text{removed}}}}\,         \\ \,\href{Ledger.Conway.Ratify.html#22331}{\htmlId{23183}{\htmlClass{Generalizable}{\text{d}}}}\,                     \end{pmatrix}$ ⇀⦇ a ,RATIFY⦈
          $\begin{pmatrix} \,\href{Ledger.Conway.Ratify.html#22232}{\htmlId{23233}{\htmlClass{Generalizable}{\text{es'}}}}\, \\ \,\href{Class.HasSingleton.html#288}{\htmlId{23239}{\htmlClass{Field Operator}{\text{❴}}}}\, \,\href{Ledger.Conway.Ratify.html#22251}{\htmlId{23241}{\htmlClass{Generalizable}{\text{a}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{23243}{\htmlClass{Field Operator}{\text{❵}}}}\, \,\href{Axiom.Set.html#8952}{\htmlId{23245}{\htmlClass{Function Operator}{\text{∪}}}}\, \,\href{Ledger.Conway.Ratify.html#22286}{\htmlId{23247}{\htmlClass{Generalizable}{\text{removed}}}}\, \\ \,\href{Ledger.Conway.Ratify.html#19422}{\htmlId{23257}{\htmlClass{Function}{\text{delayingAction}}}}\, (\,\href{Ledger.Conway.Gov.Actions.html#2144}{\htmlId{23273}{\htmlClass{Field}{\text{gaType}}}}\, \,\href{Ledger.Conway.Ratify.html#22971}{\htmlId{23280}{\htmlClass{Bound}{\text{action}}}}\,) \end{pmatrix}$

  RATIFY-Reject :
    let e              = Γ .currentEpoch
        (gaId , gaSt)  = a
    in
    ∙ ¬ acceptConds Γ $\begin{pmatrix} \,\href{Ledger.Conway.Ratify.html#22229}{\htmlId{23408}{\htmlClass{Generalizable}{\text{es}}}}\, \\ \,\href{Ledger.Conway.Ratify.html#22286}{\htmlId{23413}{\htmlClass{Generalizable}{\text{removed}}}}\, \\ \,\href{Ledger.Conway.Ratify.html#22331}{\htmlId{23423}{\htmlClass{Generalizable}{\text{d}}}}\, \end{pmatrix}$ a
    ∙ expired e gaSt
      ────────────────────────────────
      Γ ⊢ $\begin{pmatrix} \,\href{Ledger.Conway.Ratify.html#22229}{\htmlId{23501}{\htmlClass{Generalizable}{\text{es}}}}\, \\ \,\href{Ledger.Conway.Ratify.html#22286}{\htmlId{23506}{\htmlClass{Generalizable}{\text{removed}}}}\, \\ \,\href{Ledger.Conway.Ratify.html#22331}{\htmlId{23516}{\htmlClass{Generalizable}{\text{d}}}}\, \end{pmatrix}$ ⇀⦇ a ,RATIFY⦈ $\begin{pmatrix} \,\href{Ledger.Conway.Ratify.html#22229}{\htmlId{23536}{\htmlClass{Generalizable}{\text{es}}}}\, \\ \,\href{Class.HasSingleton.html#288}{\htmlId{23541}{\htmlClass{Field Operator}{\text{❴}}}}\, \,\href{Ledger.Conway.Ratify.html#22251}{\htmlId{23543}{\htmlClass{Generalizable}{\text{a}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{23545}{\htmlClass{Field Operator}{\text{❵}}}}\, \,\href{Axiom.Set.html#8952}{\htmlId{23547}{\htmlClass{Function Operator}{\text{∪}}}}\, \,\href{Ledger.Conway.Ratify.html#22286}{\htmlId{23549}{\htmlClass{Generalizable}{\text{removed}}}}\, \\ \,\href{Ledger.Conway.Ratify.html#22331}{\htmlId{23559}{\htmlClass{Generalizable}{\text{d}}}}\, \end{pmatrix}$

  RATIFY-Continue :
     let e              = Γ .currentEpoch
         (gaId , gaSt)  = a
     in
     ∙ ¬ acceptConds Γ $\begin{pmatrix} \,\href{Ledger.Conway.Ratify.html#22229}{\htmlId{23687}{\htmlClass{Generalizable}{\text{es}}}}\, \\ \,\href{Ledger.Conway.Ratify.html#22286}{\htmlId{23692}{\htmlClass{Generalizable}{\text{removed}}}}\, \\ \,\href{Ledger.Conway.Ratify.html#22331}{\htmlId{23702}{\htmlClass{Generalizable}{\text{d}}}}\, \end{pmatrix}$ a
     ∙ ¬ expired e gaSt
       ────────────────────────────────
       Γ ⊢ $\begin{pmatrix} \,\href{Ledger.Conway.Ratify.html#22229}{\htmlId{23785}{\htmlClass{Generalizable}{\text{es}}}}\, \\ \,\href{Ledger.Conway.Ratify.html#22286}{\htmlId{23790}{\htmlClass{Generalizable}{\text{removed}}}}\, \\ \,\href{Ledger.Conway.Ratify.html#22331}{\htmlId{23800}{\htmlClass{Generalizable}{\text{d}}}}\, \end{pmatrix}$ ⇀⦇ a ,RATIFY⦈ $\begin{pmatrix} \,\href{Ledger.Conway.Ratify.html#22229}{\htmlId{23820}{\htmlClass{Generalizable}{\text{es}}}}\, \\ \,\href{Ledger.Conway.Ratify.html#22286}{\htmlId{23825}{\htmlClass{Generalizable}{\text{removed}}}}\, \\ \,\href{Ledger.Conway.Ratify.html#22331}{\htmlId{23835}{\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 Figure '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.