Governance

This section is part of the Ledger.Conway.Gov module of the formal ledger specification, where we define the types required for ledger governance.

The behavior of GovState is similar to that of a queue. New proposals are appended at the end, but any proposal can be removed at the epoch boundary. However, for the purposes of enactment, earlier proposals take priority. Note that EnactState used in GovEnv is defined in 'sec:enactment' (unresolved reference).

• addVote inserts (and potentially overrides) a vote made for a particular governance action (identified by its ID) by a credential with a role.

• addAction adds a new proposed action at the end of a given GovState.

• The validHFAction property indicates whether a given proposal, if it is a TriggerHF action, can potentially be enacted in the future. For this to be the case, its prevAction needs to exist, be another TriggerHF action and have a compatible version.

{-# OPTIONS --safe #-}

open import Ledger.Conway.Gov.Base
open import Ledger.Conway.Transaction using (TransactionStructure)

module Ledger.Conway.Gov (txs : _) (open TransactionStructure txs hiding (epoch)) where

open import Ledger.Prelude hiding (any?; Any; all?; All; Rel; lookup; ∈-filter)

open import Axiom.Set.Properties th using (∃-sublist-⇔)

open import Ledger.Conway.Gov.Actions govStructure using (Vote)
open import Ledger.Conway.Enact govStructure
open import Ledger.Conway.Ratify txs hiding (vote)
open import Ledger.Conway.Certs govStructure

open import stdlib.Data.List.Subpermutations using (subpermutations; sublists)
open import stdlib.Data.List.Subpermutations.Properties
open import Data.List.Membership.Propositional.Properties using (Any↔; ∈-filter⁻; ∈-filter⁺)
open import Data.List.Relation.Binary.Subset.Propositional using () renaming (_⊆_ to _⊆ˡ_)
open import Data.List.Relation.Unary.All using (all?; All)
open import Data.List.Relation.Unary.Any using (any?; Any)
open import Data.List.Relation.Unary.Unique.DecPropositional using (unique?)
open import Data.List.Relation.Unary.Unique.Propositional using (Unique)
open import Relation.Nullary.Decidable using () renaming (map to map-Dec)
open import Function.Properties.Equivalence using () renaming (sym to sym-Equiv)
open import Function.Related.Propositional using (↔⇒)

open GovActionState

Types used in the GOV transition system

Derived types

GovState : Type

GovState = List (GovActionID × GovActionState)

record HasGovState {a} (A : Type a) : Type a where
  field GovStateOf : A → GovState
open HasGovState ⦃...⦄ public

record GovEnv : Type where
  field
    txid        : TxId
    epoch       : Epoch
    pparams     : PParams
    ppolicy     : Maybe ScriptHash
    enactState  : EnactState
    certState   : CertState
    rewardCreds : ℙ Credential

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

private variable
  Γ : GovEnv
  s s' : GovState
  aid : GovActionID
  voter : Voter
  vote : GovVote
  v : Vote
  d : Coin
  addr : RwdAddr
  a : GovAction
  prev : NeedsHash (gaType a)
  k : ℕ
  p : Maybe ScriptHash

open GState
open PState

Functions used in the GOV transition system

govActionPriority : GovActionType → ℕ
govActionPriority NoConfidence     = 
govActionPriority UpdateCommittee  = 
govActionPriority NewConstitution  = 
govActionPriority TriggerHF        = 
govActionPriority ChangePParams    = 
govActionPriority TreasuryWdrl     = 
govActionPriority Info             = 

Overlap : GovActionType → GovActionType → Type
Overlap NoConfidence    UpdateCommittee  = ⊤
Overlap UpdateCommittee NoConfidence     = ⊤
Overlap a               a'               = a ≡ a'

-- TODO: cleanup this
Overlap? : (a a' : GovActionType) → Dec (Overlap a a')
Overlap? NoConfidence    UpdateCommittee  = Dec-⊤ .dec
Overlap? UpdateCommittee NoConfidence     = Dec-⊤ .dec
Overlap? NoConfidence NoConfidence = yes refl
Overlap? NoConfidence NewConstitution = no (λ ())
Overlap? NoConfidence TriggerHF = no (λ ())
Overlap? NoConfidence ChangePParams = no (λ ())
Overlap? NoConfidence TreasuryWdrl = no (λ ())
Overlap? NoConfidence Info = no (λ ())
Overlap? UpdateCommittee UpdateCommittee = yes refl
Overlap? UpdateCommittee NewConstitution = no (λ ())
Overlap? UpdateCommittee TriggerHF = no (λ ())
Overlap? UpdateCommittee ChangePParams = no (λ ())
Overlap? UpdateCommittee TreasuryWdrl = no (λ ())
Overlap? UpdateCommittee Info = no (λ ())
Overlap? NewConstitution NoConfidence = no (λ ())
Overlap? NewConstitution UpdateCommittee = no (λ ())
Overlap? NewConstitution NewConstitution = yes refl
Overlap? NewConstitution TriggerHF = no (λ ())
Overlap? NewConstitution ChangePParams = no (λ ())
Overlap? NewConstitution TreasuryWdrl = no (λ ())
Overlap? NewConstitution Info = no (λ ())
Overlap? TriggerHF NoConfidence = no (λ ())
Overlap? TriggerHF UpdateCommittee = no (λ ())
Overlap? TriggerHF NewConstitution = no (λ ())
Overlap? TriggerHF TriggerHF = yes refl
Overlap? TriggerHF ChangePParams = no (λ ())
Overlap? TriggerHF TreasuryWdrl = no (λ ())
Overlap? TriggerHF Info = no (λ ())
Overlap? ChangePParams NoConfidence = no (λ ())
Overlap? ChangePParams UpdateCommittee = no (λ ())
Overlap? ChangePParams NewConstitution = no (λ ())
Overlap? ChangePParams TriggerHF = no (λ ())
Overlap? ChangePParams ChangePParams = yes refl
Overlap? ChangePParams TreasuryWdrl = no (λ ())
Overlap? ChangePParams Info = no (λ ())
Overlap? TreasuryWdrl NoConfidence = no (λ ())
Overlap? TreasuryWdrl UpdateCommittee = no (λ ())
Overlap? TreasuryWdrl NewConstitution = no (λ ())
Overlap? TreasuryWdrl TriggerHF = no (λ ())
Overlap? TreasuryWdrl ChangePParams = no (λ ())
Overlap? TreasuryWdrl TreasuryWdrl = yes refl
Overlap? TreasuryWdrl Info = no (λ ())
Overlap? Info NoConfidence = no (λ ())
Overlap? Info UpdateCommittee = no (λ ())
Overlap? Info NewConstitution = no (λ ())
Overlap? Info TriggerHF = no (λ ())
Overlap? Info ChangePParams = no (λ ())
Overlap? Info TreasuryWdrl = no (λ ())
Overlap? Info Info = yes refl

insertGovAction : GovState → GovActionID × GovActionState → GovState
insertGovAction [] gaPr = [ gaPr ]
insertGovAction ((gaID₀ , gaSt₀) ∷ gaPrs) (gaID₁ , gaSt₁)
  =  if govActionPriority (action gaSt₀ .gaType) ≤ govActionPriority (action gaSt₁ .gaType)
     then (gaID₀ , gaSt₀) ∷ insertGovAction gaPrs (gaID₁ , gaSt₁)
     else (gaID₁ , gaSt₁) ∷ (gaID₀ , gaSt₀) ∷ gaPrs

mkGovStatePair : Epoch → GovActionID → RwdAddr → (a : GovAction) → NeedsHash (a .gaType)
                 → GovActionID × GovActionState
mkGovStatePair e aid addr a prev = (aid , record
  { votes = ∅ ; returnAddr = addr ; expiresIn = e ; action = a ; prevAction = prev })

addAction : GovState
          → Epoch → GovActionID → RwdAddr → (a : GovAction) → NeedsHash (a .gaType)
          → GovState
addAction s e aid addr a prev = insertGovAction s (mkGovStatePair e aid addr a prev)

opaque

  addVote : GovState → GovActionID → Voter → Vote → GovState
  addVote s aid voter v = map modifyVotes s
    where modifyVotes : GovActionID × GovActionState → GovActionID × GovActionState
          modifyVotes = λ (gid , s') → gid , record s'
            { votes = if gid ≡ aid then insert (votes s') voter v else votes s'}

  isRegistered : GovEnv → Voter → Type
  isRegistered Γ (r , c) = case r of

    λ where

      CC    → just c ∈ range (gState .ccHotKeys)
      DRep  → c ∈ dom (gState .dreps)
      SPO   → c ∈ mapˢ KeyHashObj (dom (pState .pools))
        where
          open CertState (GovEnv.certState Γ) using (gState; pState)

  validHFAction : GovProposal → GovState → EnactState → Type
  validHFAction (record { action = $\begin{pmatrix} \,\href{Ledger.Conway.Gov.Actions.html#1525}{\htmlId{8264}{\htmlClass{InductiveConstructor}{\text{TriggerHF}}}}\, \\ \,\href{Ledger.Conway.Gov.html#8276}{\htmlId{8276}{\htmlClass{Bound}{\text{v}}}}\, \end{pmatrix}$ ; prevAction = prev }) s e =
    (let (v' , aid) = EnactState.pv e in aid ≡ prev × pvCanFollow v' v)
    ⊎ ∃₂[ x , v' ] (prev , x) ∈ fromList s × x .action ≡ $\begin{pmatrix} \,\href{Ledger.Conway.Gov.Actions.html#1525}{\htmlId{8442}{\htmlClass{InductiveConstructor}{\text{TriggerHF}}}}\, \\ \,\href{Ledger.Conway.Gov.html#8397}{\htmlId{8454}{\htmlClass{Bound}{\text{v'}}}}\, \end{pmatrix}$ × pvCanFollow v' v
  validHFAction _ _ _ = ⊤

Type signature of the transition relation of the GOV transition system

Transition relation types

data

  _⊢_⇀⦇_,GOV⦈_  : GovEnv × ℕ → GovState → GovVote ⊎ GovProposal → GovState → Type

_⊢_⇀⦇_,GOVS⦈_   : GovEnv → GovState → List (GovVote ⊎ GovProposal) → GovState → Type

Section 'Enactability-predicate' shows some of the functions used to determine whether certain actions are enactable in a given state. Specifically, allEnactable passes the GovState to getAidPairsList to obtain a list of GovActionID-pairs which is then passed to enactable. The latter uses the @@AgdaTerm@@basename=connectsto function to check whether the list of GovActionID-pairs connects the proposed action to a previously enacted one.

The function govActionPriority assigns a priority to the various types of governance actions. This is useful for ordering lists of governance actions (see insertGovAction in Section 'Functions-used-in-the-GOV-transition-system'). Priority is also used to check if two actions Overlap; that is, they would modify the same piece of EnactState.

Enactability predicate

-- Convert list of (GovActionID,GovActionState)-pairs to list of GovActionID pairs.
getAidPairsList : GovState → List (GovActionID × GovActionID)
getAidPairsList aid×states =
  mapMaybe (λ (aid , aState) → (aid ,_) <$> getHash (prevAction aState)) $ aid×states

-- A list of GovActionID pairs connects the first GovActionID to the second.
_connects_to_ : List (GovActionID × GovActionID) → GovActionID → GovActionID → Type
[] connects aidNew to aidOld = aidNew ≡ aidOld
((aid , aidPrev) ∷ s) connects aidNew to aidOld  =
  aid ≡ aidNew × s connects aidPrev to aidOld ⊎ s connects aidNew to aidOld

enactable  : EnactState → List (GovActionID × GovActionID)
           → GovActionID × GovActionState → Type
enactable e aidPairs = λ (aidNew , as) → case getHashES e (action as .gaType) of

  λ where

   nothing        → ⊤
   (just aidOld)  → ∃[ t ]  fromList t ⊆ fromList aidPairs
                            × Unique t × t connects aidNew to aidOld

allEnactable : EnactState → GovState → Type
allEnactable e aid×states = All (enactable e (getAidPairsList aid×states)) aid×states

hasParentE : EnactState → GovActionID → GovActionType → Type
hasParentE e aid gaTy = case getHashES e gaTy of

  λ where

   nothing    → ⊤
   (just id)  → id ≡ aid

hasParent : EnactState → GovState → (gaTy : GovActionType) → NeedsHash gaTy → Type
hasParent e s gaTy aid = case getHash aid of

  λ where

    nothing      → ⊤
    (just aid')  → hasParentE e aid' gaTy
                   ⊎ Any (λ (gid , gas) → gid ≡ aid' × Overlap (gas .action .gaType) gaTy) s

open Equivalence

hasParentE? : ∀ e aid a → Dec (hasParentE e aid a)
hasParentE? e aid gaTy with getHashES e gaTy
... | nothing   = yes _
... | (just id) = id ≟ aid

hasParent? : ∀ e s a aid → Dec (hasParent e s a aid)
hasParent? e s gaTy aid with getHash aid
... | just aid' = hasParentE? e aid' gaTy
                  ⊎-dec any? (λ (gid , gas) → gid ≟ aid' ×-dec Overlap? (gas .action .gaType) gaTy) s
... | nothing = yes _

-- newtype to make the instance resolution work
data hasParent' : EnactState → GovState → (gaTy : GovActionType) → NeedsHash gaTy → Type where
  HasParent' : ∀ {x y z w} → hasParent x y z w → hasParent' x y z w

instance
  hasParent?' : ∀ {x y z w} → hasParent' x y z w ⁇
  hasParent?' = ⁇ map′ HasParent' (λ where (HasParent' x) → x) (hasParent? _ _ _ _)

[_connects_to_?] : ∀ l aidNew aidOld → Dec (l connects aidNew to aidOld)
[ [] connects aidNew to aidOld ?] = aidNew ≟ aidOld

[ (aid , aidPrev) ∷ s connects aidNew to aidOld ?] =
  ((aid ≟ aidNew) ×-dec [ s connects aidPrev to aidOld ?]) ⊎-dec [ s connects aidNew to aidOld ?]

any?-connecting-subperm : ∀ {u} {v} → ∀ L → Dec (Any(λ l → Unique l × l connects u to v) (subpermutations L))
any?-connecting-subperm {u} {v} L = any? (λ l → unique? _≟_ l ×-dec [ l connects u to v ?]) (subpermutations L)

∃?-connecting-subperm : ∀ {u} {v} → ∀ L → Dec (∃[ l ] l ∈ˡ subpermutations L × Unique l × l connects u to v)
∃?-connecting-subperm L = map-Dec (sym-Equiv (↔⇒ Any↔)) (any?-connecting-subperm L)

∃?-connecting-subset : ∀ {u} {v} → ∀ L → Dec (∃[ l ] l ⊆ˡ L × Unique l × l connects u to v)
∃?-connecting-subset L = map-Dec (sym-Equiv ∃uniqueSubset⇔∃uniqueSubperm) (∃?-connecting-subperm L)

enactable? : ∀ eState aidPairs aidNew×st → Dec (enactable eState aidPairs aidNew×st)
enactable? eState aidPairs (aidNew , as) with getHashES eState (GovActionState.action as .gaType)
... | nothing = yes tt
... | just aidOld = map-Dec (sym-Equiv ∃-sublist-⇔) (∃?-connecting-subset aidPairs)

allEnactable? : ∀ eState aid×states → Dec (allEnactable eState aid×states)
allEnactable? eState aid×states =
  all? (λ aid×st → enactable? eState (getAidPairsList aid×states) aid×st) aid×states

-- newtype to make the instance resolution work
data allEnactable' : EnactState → GovState → Type where
  AllEnactable' : ∀ {x y} → allEnactable x y → allEnactable' x y

instance
  allEnactable?' : ∀ {x y} → allEnactable' x y ⁇
  allEnactable?' = ⁇ map′ AllEnactable' (λ where (AllEnactable' x) → x) (allEnactable? _ _)

-- `maxAllEnactable` returns a list `ls` of sublists of the given
-- list (`aid×states : List (GovActionID × GovActionState)`) such that
--    (i) each sublist `l ∈ ls` satisfies `allEnactable e l` and
--   (ii) each sublist `l ∈ ls` is of maximal length among sublists of `aid×states` satisfying `allEnactable`.
maxAllEnactable : EnactState → List (GovActionID × GovActionState) → List (List (GovActionID × GovActionState))
maxAllEnactable e = maxsublists⊧P (allEnactable? e)

-- Every sublist returned by `maxAllEnactable` satisfies (i).
∈-maxAllEnactable→allEnactable : ∀ {e} {aid×states} l
  → l ∈ˡ maxAllEnactable e aid×states → allEnactable e l
∈-maxAllEnactable→allEnactable {e} {aid×states} l l∈ =
  proj₂ (∈-filter⁻ (allEnactable? e) {l} {sublists aid×states}
          (proj₁ (∈-filter⁻ (λ l → length l ≟ maxlen (sublists⊧P (allEnactable? e) aid×states)) l∈)))

-- Every sublist returned by `maxAllEnactable` satisfies (ii).
∈-maxAllEnactable→maxLength : ∀ {e aid×states l l'}
                              → l ∈ˡ sublists aid×states → allEnactable e l
                              → l' ∈ˡ maxAllEnactable e aid×states
                              → length l ≤ length l'
∈-maxAllEnactable→maxLength {e} {aid×states} {l} {l'} l∈ el l'∈ =
  let ls = sublists⊧P (allEnactable? e) aid×states in
    subst (length l ≤_)
          (sym (proj₂ (∈-filter⁻ (λ l → length l ≟ maxlen ls) {xs = ls} l'∈)))
          (∈-maxlen-≤ l (∈-filter⁺ (allEnactable? e) l∈ el))

Validity and wellformedness predicates

actionValid : ℙ Credential → Maybe ScriptHash → Maybe ScriptHash → Epoch → GovAction → Type
actionValid rewardCreds p ppolicy epoch $\begin{pmatrix} \,\href{Ledger.Conway.Gov.Actions.html#1560}{\htmlId{15797}{\htmlClass{InductiveConstructor}{\text{ChangePParams}}}}\, \\ \,\htmlId{15813}{\htmlClass{Symbol}{\text{\_}}}\, \end{pmatrix}$ =
  p ≡ ppolicy
actionValid rewardCreds p ppolicy epoch $\begin{pmatrix} \,\href{Ledger.Conway.Gov.Actions.html#1595}{\htmlId{15877}{\htmlClass{InductiveConstructor}{\text{TreasuryWdrl}}}}\,  \\ \,\href{Ledger.Conway.Gov.html#15893}{\htmlId{15893}{\htmlClass{Bound}{\text{x}}}}\, \end{pmatrix}$ =
  p ≡ ppolicy × mapˢ RwdAddr.stake (dom x) ⊆ rewardCreds
actionValid rewardCreds p ppolicy epoch $\begin{pmatrix} \,\href{Ledger.Conway.Gov.Actions.html#1455}{\htmlId{16000}{\htmlClass{InductiveConstructor}{\text{UpdateCommittee}}}}\, \\ (\,\href{Ledger.Conway.Gov.html#16019}{\htmlId{16019}{\htmlClass{Bound}{\text{new}}}}\, , \,\href{Ledger.Conway.Gov.html#16025}{\htmlId{16025}{\htmlClass{Bound}{\text{rem}}}}\, , \,\href{Ledger.Conway.Gov.html#16031}{\htmlId{16031}{\htmlClass{Bound}{\text{q}}}}\,) \end{pmatrix}$ =
  p ≡ nothing × (∀[ e ∈ range new ]  epoch < e) × (dom new ∩ rem ≡ᵉ ∅)
actionValid rewardCreds p ppolicy epoch _ =
  p ≡ nothing

actionWellFormed : GovAction → Type
actionWellFormed $\begin{pmatrix} \,\href{Ledger.Conway.Gov.Actions.html#1560}{\htmlId{16225}{\htmlClass{InductiveConstructor}{\text{ChangePParams}}}}\, \\ \,\href{Ledger.Conway.Gov.html#16241}{\htmlId{16241}{\htmlClass{Bound}{\text{x}}}}\, \end{pmatrix}$ = ppdWellFormed x
actionWellFormed $\begin{pmatrix} \,\href{Ledger.Conway.Gov.Actions.html#1595}{\htmlId{16284}{\htmlClass{InductiveConstructor}{\text{TreasuryWdrl}}}}\,  \\ \,\href{Ledger.Conway.Gov.html#16300}{\htmlId{16300}{\htmlClass{Bound}{\text{x}}}}\, \end{pmatrix}$ =
  (∀[ a ∈ dom x ] NetworkIdOf a ≡ NetworkId) × (∃[ v ∈ range x ] ¬ (v ≡ ))
actionWellFormed _                 = ⊤

Figure 'Validity-and-wellformedness-predicates' defines predicates used in the GOVPropose case of the GOV rule to ensure that a governance action is valid and well-formed.

• actionValid ensures that the proposed action is valid given the current state of the system:

• a ChangePParams action is valid if the proposal policy is provided;

• a TreasuryWdrl action is valid if the proposal policy is provided and the reward stake credential is registered;

• an UpdateCommittee action is valid if credentials of proposed candidates have not expired, and the action does not propose to both add and remove the same candidate.

• actionWellFormed ensures that the proposed action is well-formed:

• a ChangePParams action must preserves well-formedness of the protocol parameters;

• a TreasuryWdrl action is well-formed if the network ID is correct and there is at least one non-zero withdrawal amount in the given RwdAddrToCoinMap map.

actionValid? : ∀ {rewardCreds p ppolicy epoch a} → actionValid rewardCreds p ppolicy epoch a ⁇
actionValid? {a = $\begin{pmatrix} \,\href{Ledger.Conway.Gov.Actions.html#1420}{\htmlId{17826}{\htmlClass{InductiveConstructor}{\text{NoConfidence}}}}\,    \\ \,\htmlId{17844}{\htmlClass{Symbol}{\text{\_}}}\, \end{pmatrix}$} = it
actionValid? {a = $\begin{pmatrix} \,\href{Ledger.Conway.Gov.Actions.html#1455}{\htmlId{17876}{\htmlClass{InductiveConstructor}{\text{UpdateCommittee}}}}\, \\ \,\htmlId{17894}{\htmlClass{Symbol}{\text{\_}}}\, \end{pmatrix}$} = it
actionValid? {a = $\begin{pmatrix} \,\href{Ledger.Conway.Gov.Actions.html#1490}{\htmlId{17926}{\htmlClass{InductiveConstructor}{\text{NewConstitution}}}}\, \\ \,\htmlId{17944}{\htmlClass{Symbol}{\text{\_}}}\, \end{pmatrix}$} = it
actionValid? {a = $\begin{pmatrix} \,\href{Ledger.Conway.Gov.Actions.html#1525}{\htmlId{17976}{\htmlClass{InductiveConstructor}{\text{TriggerHF}}}}\,       \\ \,\htmlId{17994}{\htmlClass{Symbol}{\text{\_}}}\, \end{pmatrix}$} = it
actionValid? {a = $\begin{pmatrix} \,\href{Ledger.Conway.Gov.Actions.html#1560}{\htmlId{18026}{\htmlClass{InductiveConstructor}{\text{ChangePParams}}}}\,   \\ \,\htmlId{18044}{\htmlClass{Symbol}{\text{\_}}}\, \end{pmatrix}$} = it
actionValid? {a = $\begin{pmatrix} \,\href{Ledger.Conway.Gov.Actions.html#1595}{\htmlId{18076}{\htmlClass{InductiveConstructor}{\text{TreasuryWdrl}}}}\,    \\ \,\htmlId{18094}{\htmlClass{Symbol}{\text{\_}}}\, \end{pmatrix}$} = it
actionValid? {a = $\begin{pmatrix} \,\href{Ledger.Conway.Gov.Actions.html#1630}{\htmlId{18126}{\htmlClass{InductiveConstructor}{\text{Info}}}}\,            \\ \,\htmlId{18144}{\htmlClass{Symbol}{\text{\_}}}\, \end{pmatrix}$} = it

actionWellFormed? : ∀ {a} → actionWellFormed a ⁇
actionWellFormed? {$\begin{pmatrix} \,\href{Ledger.Conway.Gov.Actions.html#1420}{\htmlId{18227}{\htmlClass{InductiveConstructor}{\text{NoConfidence}}}}\,    \\ \,\htmlId{18245}{\htmlClass{Symbol}{\text{\_}}}\, \end{pmatrix}$} = it
actionWellFormed? {$\begin{pmatrix} \,\href{Ledger.Conway.Gov.Actions.html#1455}{\htmlId{18278}{\htmlClass{InductiveConstructor}{\text{UpdateCommittee}}}}\, \\ \,\htmlId{18296}{\htmlClass{Symbol}{\text{\_}}}\, \end{pmatrix}$} = it
actionWellFormed? {$\begin{pmatrix} \,\href{Ledger.Conway.Gov.Actions.html#1490}{\htmlId{18329}{\htmlClass{InductiveConstructor}{\text{NewConstitution}}}}\, \\ \,\htmlId{18347}{\htmlClass{Symbol}{\text{\_}}}\, \end{pmatrix}$} = it
actionWellFormed? {$\begin{pmatrix} \,\href{Ledger.Conway.Gov.Actions.html#1525}{\htmlId{18380}{\htmlClass{InductiveConstructor}{\text{TriggerHF}}}}\,       \\ \,\htmlId{18398}{\htmlClass{Symbol}{\text{\_}}}\, \end{pmatrix}$} = it
actionWellFormed? {$\begin{pmatrix} \,\href{Ledger.Conway.Gov.Actions.html#1560}{\htmlId{18431}{\htmlClass{InductiveConstructor}{\text{ChangePParams}}}}\,   \\ \,\htmlId{18449}{\htmlClass{Symbol}{\text{\_}}}\, \end{pmatrix}$} = it
actionWellFormed? {$\begin{pmatrix} \,\href{Ledger.Conway.Gov.Actions.html#1595}{\htmlId{18482}{\htmlClass{InductiveConstructor}{\text{TreasuryWdrl}}}}\,    \\ \,\htmlId{18500}{\htmlClass{Symbol}{\text{\_}}}\, \end{pmatrix}$} = it
actionWellFormed? {$\begin{pmatrix} \,\href{Ledger.Conway.Gov.Actions.html#1630}{\htmlId{18533}{\htmlClass{InductiveConstructor}{\text{Info}}}}\,            \\ \,\htmlId{18551}{\htmlClass{Symbol}{\text{\_}}}\, \end{pmatrix}$} = it

open GovEnv
open PParams hiding (a)

variable
  machr : Maybe Anchor
  achr : Anchor
  ast  : GovActionState

Rules for the GOV transition system

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

  GOV-Vote :
    ∙ (aid , ast) ∈ fromList s
    ∙ canVote (Γ .pparams) (action ast) (proj₁ voter)
    ∙ isRegistered Γ voter
    ∙ ¬ expired (Γ .epoch) ast
      ───────────────────────────────────────
      (Γ , k) ⊢ s ⇀⦇ inj₁ $\begin{pmatrix} \,\href{Ledger.Conway.Gov.html#3454}{\htmlId{19029}{\htmlClass{Generalizable}{\text{aid}}}}\, \\ \,\href{Ledger.Conway.Gov.html#3474}{\htmlId{19035}{\htmlClass{Generalizable}{\text{voter}}}}\, \\ \,\href{Ledger.Conway.Gov.html#3507}{\htmlId{19043}{\htmlClass{Generalizable}{\text{v}}}}\, \\ \,\href{Ledger.Conway.Gov.html#18636}{\htmlId{19047}{\htmlClass{Generalizable}{\text{machr}}}}\, \end{pmatrix}$ ,GOV⦈ addVote s aid voter v

  GOV-Propose :
    let pp           = Γ .pparams
        e            = Γ .epoch
        enactState   = Γ .enactState
        rewardCreds  = Γ .rewardCreds
        prop         = record { returnAddr = addr ; action = a ; anchor = achr
                              ; policy = p ; deposit = d ; prevAction = prev }
    in
    ∙ actionWellFormed a
    ∙ actionValid rewardCreds p (Γ .ppolicy) e a
    ∙ d ≡ pp .govActionDeposit
    ∙ validHFAction prop s enactState
    ∙ hasParent enactState s (a .gaType) prev
    ∙ NetworkIdOf addr ≡ NetworkId
    ∙ CredentialOf addr ∈ rewardCreds
      ───────────────────────────────────────
      (Γ , k) ⊢ s ⇀⦇ inj₂ prop ,GOV⦈ addAction s (pp .govActionLifetime +ᵉ e)
                                                 (Γ .txid , k) addr a prev

_⊢_⇀⦇_,GOVS⦈_ = ReflexiveTransitiveClosureᵢ {sts = _⊢_⇀⦇_,GOV⦈_}

The GOVS transition system is now given as the reflexitive-transitive closure of the system GOV, described in Section 'Rules-for-the-GOV-transition-system'.

For GOVVote, we check that the governance action being voted on exists; that the voter’s role is allowed to vote (see canVote in Figure 'Functions-related-to-voting'); and that the voter’s credential is actually associated with their role (see isRegistered in Section 'Type-signature-of-the-transition-relation-of-the-GOV-transition-system').

For GOVPropose, we check the correctness of the deposit along with some and some conditions that ensure the action is well-formed and valid; naturally, these checks depend on the type of action being proposed (see Figure 'Validity-and-wellformedness-predicates').