Ratification

{-# OPTIONS --safe #-}

open import Ledger.Conway.Specification.Transaction hiding (Vote)

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

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

This section 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 a column for each of the three governing bodies (or "governance roles")—CC, DRep and SPO, in that order.

The meaning of the symbols are as follows.

• 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 governance role 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—namely, the UpdateCommittee and ChangePParams rows.

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 the 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 Px and Qx 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₃ }

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       , update  ) → ∣ ✓   ∥ P/Q5 update             ∣
        (TreasuryWithdrawal  , _       ) → ∣ ✓   ∣ vote P6      ∣ ─        ∣
        (Info                , _       ) → ∣ ✓†  ∣ ✓†           ∣ ✓†       ∣
          where

          open PParams pp
          open DrepThresholds drepThresholds
          open PoolThresholds poolThresholds

          vote : ℚ → Maybe ℚ
          vote = just

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

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

          ─ ✓ ✓† : Maybe ℚ
          ─  = nothing
          ✓  = maybe just ✓† ccThreshold
          ✓† = vote defer

          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 Types and Functions

This section defines types and functions used in 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

  HasDReps-RatifyEnv : HasDReps RatifyEnv
  HasDReps-RatifyEnv .DRepsOf = RatifyEnv.dreps

  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 the 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.

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

Vote Counting

This section defines the acceptedBy predicate for each of the governing 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 Committee (CC) Vote Counting

This subsection defines the acceptedByCC predicate, which utilizes the following auxiliary definitions.

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

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

• actualVote: This function sets the default vote for CC members. If the given CC member's term has expired, if they have not yet registered a hot key, or if they have resigned, then actualVote 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 no is returned.

• actualVotes: This map contains the actual votes of the CC. 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 a single vote with that hot key the power of those multiple voting stakes.

• acceptedStake: This is the portion of CC stake that voted yes.

• totalStake: This is the portion of CC stake that voted either yes or no.

In addition, it must be the case that either

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

• the threshold function returns nothing.

module AcceptedByCC (currentEpoch : Epoch)
                    (ccHotKeys : Credential ⇀ Maybe Credential)
                    (eSt : EnactState)
                    (gaSt : GovActionState)
                    where

  open EnactState eSt using (cc)
  open PParams (PParamsOf eSt)
  open GovActionState gaSt
  open GovVotes votes using (gvCC)

  sizeActiveCC : ℕ
  sizeActiveCC = case proj₁ cc of λ where
    (just ((ccMembers , _) , _)) → lengthˢ (filterˢ (activeInEpoch currentEpoch) ccMembers)
    nothing → 

  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 (PParamsOf eSt) (proj₂ <$> (proj₁ cc)) action CC

  t : ℚ
  t = maybe id 0ℚ mT

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

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

  accepted = (acceptedStake /₀ totalStake) ≥ t
    × (sizeActiveCC ≥ ccMinSize ⊎ (Is-nothing mT × ccMinSize ≡ ))

acceptedByCC
  : RatifyEnv
  → EnactState
  → GovActionState
  → Type
acceptedByCC Γ = AcceptedByCC.accepted currentEpoch ccHotKeys
  where open RatifyEnv Γ using (currentEpoch; ccHotKeys)

DRep Vote Counting

This section defines the predicate acceptedByDRep, which depends on the following 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 votes cast, the default votes and the predetermined votes.

• acceptedStake: This is the portion of DRep voting stake that voted yes.

• totalStake: This the portion of DRep voting stake that voted yes or no.

module AcceptedByDRep (Γ : RatifyEnv)
                      (eSt : EnactState)
                      (gaSt : GovActionState)
                      where

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

  castVotes : VDeleg ⇀ Vote
  castVotes = mapKeys vDelegCredential gvDRep

  activeDReps : ℙ Credential
  activeDReps = dom (activeDRepsOf Γ currentEpoch)

  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 (PParamsOf eSt) (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

  accepted = (acceptedStake /₀ totalStake) ≥ t

acceptedByDRep
  : RatifyEnv
  → EnactState
  → GovActionState
  → Type
acceptedByDRep = AcceptedByDRep.accepted

Stake Pool Operator (SPO) Vote Counting

This section 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 number is the threshold used to calculate whether the action is ratified by the SPO body.

• acceptedStake: This is the portion of SPO stake that voted yes; it is computed using the stake distribution stakeDistrPools provided in the environment.

• totalStake: This is the portion of SPO stake that voted either yes or no; it is computed using the stake distribution stakeDistrPools provided in the environment.

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 configure default voting behavior is the credential used to withdraw staking rewards, which is not the same as the credential that is used for standard voting.

Vote Counting Methodology

The way SPO votes are counted 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 the section on Bootstrapping the Governance System.)

module AcceptedBySPO (delegatees : VoteDelegs)
                     (pools : Pools)
                     (stakeDistrPools : KeyHash ⇀ Coin)
                     (eSt : EnactState)
                     (gaSt : GovActionState)
                     where

  open EnactState eSt using (cc)
  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 (PParamsOf eSt) (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

  accepted : Type
  accepted = (acceptedStake /₀ totalStake) ≥ t

acceptedBySPO
  : RatifyEnv
  → EnactState
  → GovActionState
  → Type
acceptedBySPO Γ = AcceptedBySPO.accepted delegatees pools stakeDistrPools
  where open RatifyEnv Γ
        open StakeDistrs stakeDistrs

Ratification Functions

We first define the accepted and expired functions, which are used in the rules of the RATIFY transition system.

opaque

  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

Next, we define 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; specifically, whenever a delayingAction is accepted all future actions are delayed. delayed then expresses 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.

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#24679}{\htmlId{24775}{\htmlClass{Bound}{\text{id}}}}\, \\ \,\href{Ledger.Conway.Specification.Ratify.html#7983}{\htmlId{24780}{\htmlClass{Function}{\text{treasury}}}}\, \\ \,\href{Ledger.Conway.Specification.Ratify.html#7868}{\htmlId{24791}{\htmlClass{Function}{\text{currentEpoch}}}}\, \end{pmatrix}$ ⊢ es ⇀⦇ action ,ENACT⦈ es'

    where open RatifyEnv Γ
          open RatifyState stʳ
          open GovActionState st

opaque
  unfolding accepted

  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? ×-dec ¿ _ ¿))

    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 ¿

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

open RatifyEnv
open GovActionState

The RATIFY Transition System

We now define the RATIFY transition system, which is constructed via three rules.

• 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 continue to be checked every epoch until it expires.

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

  RATIFY-Accept :
    let treasury       = TreasuryOf Γ
        e              = Γ .currentEpoch
        (gaId , gaSt)  = a
        action         = GovActionOf gaSt
    in
    ∙ acceptConds Γ $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Ratify.html#26239}{\htmlId{28093}{\htmlClass{Generalizable}{\text{es}}}}\, \\ \,\href{Ledger.Conway.Specification.Ratify.html#26296}{\htmlId{28098}{\htmlClass{Generalizable}{\text{removed}}}}\, \\ \,\href{Ledger.Conway.Specification.Ratify.html#26341}{\htmlId{28108}{\htmlClass{Generalizable}{\text{d}}}}\, \end{pmatrix}$ a
    ∙ $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Ratify.html#28004}{\htmlId{28122}{\htmlClass{Bound}{\text{gaId}}}}\, \\ \,\href{Ledger.Conway.Specification.Ratify.html#27924}{\htmlId{28129}{\htmlClass{Bound}{\text{treasury}}}}\, \\ \,\href{Ledger.Conway.Specification.Ratify.html#27962}{\htmlId{28140}{\htmlClass{Bound}{\text{e}}}}\, \end{pmatrix}$ ⊢ es ⇀⦇ action ,ENACT⦈ es'
      ────────────────────────────────
      Γ ⊢ $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Ratify.html#26239}{\htmlId{28222}{\htmlClass{Generalizable}{\text{es}}}}\, \\ \,\href{Ledger.Conway.Specification.Ratify.html#26296}{\htmlId{28227}{\htmlClass{Generalizable}{\text{removed}}}}\, \\ \,\href{Ledger.Conway.Specification.Ratify.html#26341}{\htmlId{28237}{\htmlClass{Generalizable}{\text{d}}}}\, \end{pmatrix}$ ⇀⦇ a ,RATIFY⦈ $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Ratify.html#26242}{\htmlId{28257}{\htmlClass{Generalizable}{\text{es'}}}}\, \\ \,\href{Class.HasSingleton.html#288}{\htmlId{28263}{\htmlClass{Field Operator}{\text{❴}}}}\, \,\href{Ledger.Conway.Specification.Ratify.html#26261}{\htmlId{28265}{\htmlClass{Generalizable}{\text{a}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{28267}{\htmlClass{Field Operator}{\text{❵}}}}\, \,\href{Axiom.Set.html#9137}{\htmlId{28269}{\htmlClass{Function Operator}{\text{∪}}}}\, \,\href{Ledger.Conway.Specification.Ratify.html#26296}{\htmlId{28271}{\htmlClass{Generalizable}{\text{removed}}}}\, \\ \,\href{Ledger.Conway.Specification.Ratify.html#24120}{\htmlId{28281}{\htmlClass{Function}{\text{delayingAction}}}}\, \,\htmlId{28296}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Conway.Specification.Gov.Actions.html#4046}{\htmlId{28297}{\htmlClass{Field}{\text{gaType}}}}\, \,\href{Ledger.Conway.Specification.Ratify.html#28030}{\htmlId{28304}{\htmlClass{Bound}{\text{action}}}}\,\,\htmlId{28310}{\htmlClass{Symbol}{\text{)}}}\, \end{pmatrix}$

  RATIFY-Reject :
    let e              = Γ .currentEpoch
        (gaId , gaSt)  = a
    in
    ∙ ¬ acceptConds Γ $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Ratify.html#26239}{\htmlId{28432}{\htmlClass{Generalizable}{\text{es}}}}\, \\ \,\href{Ledger.Conway.Specification.Ratify.html#26296}{\htmlId{28437}{\htmlClass{Generalizable}{\text{removed}}}}\, \\ \,\href{Ledger.Conway.Specification.Ratify.html#26341}{\htmlId{28447}{\htmlClass{Generalizable}{\text{d}}}}\, \end{pmatrix}$ a
    ∙ expired e gaSt
      ────────────────────────────────
      Γ ⊢ $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Ratify.html#26239}{\htmlId{28525}{\htmlClass{Generalizable}{\text{es}}}}\, \\ \,\href{Ledger.Conway.Specification.Ratify.html#26296}{\htmlId{28530}{\htmlClass{Generalizable}{\text{removed}}}}\, \\ \,\href{Ledger.Conway.Specification.Ratify.html#26341}{\htmlId{28540}{\htmlClass{Generalizable}{\text{d}}}}\, \end{pmatrix}$ ⇀⦇ a ,RATIFY⦈ $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Ratify.html#26239}{\htmlId{28560}{\htmlClass{Generalizable}{\text{es}}}}\, \\ \,\href{Class.HasSingleton.html#288}{\htmlId{28565}{\htmlClass{Field Operator}{\text{❴}}}}\, \,\href{Ledger.Conway.Specification.Ratify.html#26261}{\htmlId{28567}{\htmlClass{Generalizable}{\text{a}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{28569}{\htmlClass{Field Operator}{\text{❵}}}}\, \,\href{Axiom.Set.html#9137}{\htmlId{28571}{\htmlClass{Function Operator}{\text{∪}}}}\, \,\href{Ledger.Conway.Specification.Ratify.html#26296}{\htmlId{28573}{\htmlClass{Generalizable}{\text{removed}}}}\, \\ \,\href{Ledger.Conway.Specification.Ratify.html#26341}{\htmlId{28583}{\htmlClass{Generalizable}{\text{d}}}}\, \end{pmatrix}$

  RATIFY-Continue :
     let e              = Γ .currentEpoch
         (gaId , gaSt)  = a
     in
     ∙ ¬ acceptConds Γ $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Ratify.html#26239}{\htmlId{28711}{\htmlClass{Generalizable}{\text{es}}}}\, \\ \,\href{Ledger.Conway.Specification.Ratify.html#26296}{\htmlId{28716}{\htmlClass{Generalizable}{\text{removed}}}}\, \\ \,\href{Ledger.Conway.Specification.Ratify.html#26341}{\htmlId{28726}{\htmlClass{Generalizable}{\text{d}}}}\, \end{pmatrix}$ a
     ∙ ¬ expired e gaSt
       ────────────────────────────────
       Γ ⊢ $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Ratify.html#26239}{\htmlId{28809}{\htmlClass{Generalizable}{\text{es}}}}\, \\ \,\href{Ledger.Conway.Specification.Ratify.html#26296}{\htmlId{28814}{\htmlClass{Generalizable}{\text{removed}}}}\, \\ \,\href{Ledger.Conway.Specification.Ratify.html#26341}{\htmlId{28824}{\htmlClass{Generalizable}{\text{d}}}}\, \end{pmatrix}$ ⇀⦇ a ,RATIFY⦈ $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Ratify.html#26239}{\htmlId{28844}{\htmlClass{Generalizable}{\text{es}}}}\, \\ \,\href{Ledger.Conway.Specification.Ratify.html#26296}{\htmlId{28849}{\htmlClass{Generalizable}{\text{removed}}}}\, \\ \,\href{Ledger.Conway.Specification.Ratify.html#26341}{\htmlId{28859}{\htmlClass{Generalizable}{\text{d}}}}\, \end{pmatrix}$

Finally, the RATIFIES transition system is defined as the "reflexive transitive closure" of the RATIFY rule.

_⊢_⇀⦇_,RATIFIES⦈_ : RatifyEnv → RatifyState → List (GovActionID × GovActionState) → RatifyState → Type
_⊢_⇀⦇_,RATIFIES⦈_ = ReflexiveTransitiveClosure {sts = _⊢_⇀⦇_,RATIFY⦈_}