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
the Enact module.
Governance Types¶
Derived types
GovState : Type GovState = List (GovActionID × GovActionState)
record GovEnv : Type where field txid : TxId epoch : Epoch pparams : PParams ppolicy : Maybe ScriptHash enactState : EnactState certState : CertState rewardCreds : ℙ Credential
Governance Functions¶
The function definitions worth highlighting in this section are the following:
-
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 givenGovState
. -
The
validHFAction
property indicates whether a given proposal, if it is aTriggerHardFork
action, can potentially be enacted in the future. For this to be the case, itsprevAction
needs to exist, be anotherTriggerHardFork
action and have a compatible version.
govActionPriority : GovActionType → ℕ govActionPriority NoConfidence = 0 govActionPriority UpdateCommittee = 1 govActionPriority NewConstitution = 2 govActionPriority TriggerHardFork = 3 govActionPriority ChangePParams = 4 govActionPriority TreasuryWithdrawal = 5 govActionPriority Info = 6 Overlap : GovActionType → GovActionType → Type Overlap NoConfidence UpdateCommittee = ⊤ Overlap UpdateCommittee NoConfidence = ⊤ Overlap a a' = a ≡ a'
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 , gas) where gas : GovActionState gas = record { votes = record { gvCC = ∅ ; gvDRep = ∅ ; gvSPO = ∅ } ; 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)
addVote : GovState → GovActionID → GovVoter → Vote → GovState addVote gSt aid voter v = map modifyVotes gSt where modifyVotes : GovActionID × GovActionState → GovActionID × GovActionState modifyVotes (gid , gaSt) = gid , (if gid ≡ aid then record gaSt { votes = votes' voter } else gaSt) where open GovVotes (votes gaSt) votes' : GovVoter → GovVotes votes' $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#1200}{\htmlId{8508}{\htmlClass{InductiveConstructor}{\text{CC}}}}\, \\ \,\href{Ledger.Conway.Specification.Gov.html#8513}{\htmlId{8513}{\htmlClass{Bound}{\text{c}}}}\, \end{pmatrix}$ = record { gvCC = insert gvCC c v ; gvDRep = gvDRep ; gvSPO = gvSPO } votes' $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#1203}{\htmlId{8604}{\htmlClass{InductiveConstructor}{\text{DRep}}}}\, \\ \,\href{Ledger.Conway.Specification.Gov.html#8611}{\htmlId{8611}{\htmlClass{Bound}{\text{c}}}}\, \end{pmatrix}$ = record { gvCC = gvCC ; gvDRep = insert gvDRep c v ; gvSPO = gvSPO } votes' $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#1208}{\htmlId{8702}{\htmlClass{InductiveConstructor}{\text{SPO}}}}\, \\ \,\href{Ledger.Conway.Specification.Gov.html#8708}{\htmlId{8708}{\htmlClass{Bound}{\text{kh}}}}\, \end{pmatrix}$ = record { gvCC = gvCC ; gvDRep = gvDRep ; gvSPO = insert gvSPO kh v } isRegistered : GovEnv → GovVoter → Type isRegistered Γ v = case v of λ where $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#1200}{\htmlId{8880}{\htmlClass{InductiveConstructor}{\text{CC}}}}\, \\ \,\href{Ledger.Conway.Specification.Gov.html#8887}{\htmlId{8887}{\htmlClass{Bound}{\text{c}}}}\, \end{pmatrix}$ → just c ∈ range (CCHotKeysOf (CertStateOf Γ)) $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#1203}{\htmlId{8949}{\htmlClass{InductiveConstructor}{\text{DRep}}}}\, \\ \,\href{Ledger.Conway.Specification.Gov.html#8956}{\htmlId{8956}{\htmlClass{Bound}{\text{c}}}}\, \end{pmatrix}$ → c ∈ dom (DRepsOf (CertStateOf Γ)) $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#1208}{\htmlId{9007}{\htmlClass{InductiveConstructor}{\text{SPO}}}}\, \\ \,\href{Ledger.Conway.Specification.Gov.html#9014}{\htmlId{9014}{\htmlClass{Bound}{\text{kh}}}}\, \end{pmatrix}$ → kh ∈ dom (PoolsOf (CertStateOf Γ)) validHFAction : GovProposal → GovState → EnactState → Type validHFAction (record { action = $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#1991}{\htmlId{9157}{\htmlClass{InductiveConstructor}{\text{TriggerHardFork}}}}\, \\ \,\href{Ledger.Conway.Specification.Gov.html#9175}{\htmlId{9175}{\htmlClass{Bound}{\text{v}}}}\, \end{pmatrix}$ ; prevAction = prev }) s e = (aid' ≡ prev × pvCanFollow ver v) ⊎ ∃₂[ x , v' ] (prev , x) ∈ fromList s × x .action ≡ $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#1991}{\htmlId{9358}{\htmlClass{InductiveConstructor}{\text{TriggerHardFork}}}}\, \\ \,\href{Ledger.Conway.Specification.Gov.html#9258}{\htmlId{9376}{\htmlClass{Bound}{\text{v'}}}}\, \end{pmatrix}$ × pvCanFollow v' v where ver : ProtVer ver = EnactState.pv e .proj₁ aid' : GovActionID aid' = EnactState.pv e .proj₂ validHFAction _ _ _ = ⊤
Enactability Predicate¶
This section contains 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 _connects_to_
function to check whether the list
of GovActionID
-pairs connects the proposed action to a previously
enacted one.1
The function govActionPriority
assigns a priority to
the various types of governance actions. This is useful for ordering
lists of governance actions (see the definition of the
insertGovAction
function in the section on
Functions of the GOV Transition System
Priority is also used to check if two actions Overlap
; that is,
they would modify the same piece of EnactState
.
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 (GovActionTypeOf gas) gaTy) s
Validity and Wellformedness Predicates¶
This section defines predicates used in the GOVPropose
case
of the GOV rule to ensure that a governance action is valid and well-formed.
actionValid : ℙ Credential → Maybe ScriptHash → Maybe ScriptHash → Epoch → GovAction → Type actionValid rewardCreds p ppolicy epoch $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#2029}{\htmlId{16482}{\htmlClass{InductiveConstructor}{\text{ChangePParams}}}}\, \\ \,\htmlId{16498}{\htmlClass{Symbol}{\text{\_}}}\, \end{pmatrix}$ = p ≡ ppolicy actionValid rewardCreds p ppolicy epoch $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#2067}{\htmlId{16562}{\htmlClass{InductiveConstructor}{\text{TreasuryWithdrawal}}}}\, \\ \,\href{Ledger.Conway.Specification.Gov.html#16584}{\htmlId{16584}{\htmlClass{Bound}{\text{x}}}}\, \end{pmatrix}$ = p ≡ ppolicy × mapˢ RwdAddr.stake (dom x) ⊆ rewardCreds actionValid rewardCreds p ppolicy epoch $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#1915}{\htmlId{16691}{\htmlClass{InductiveConstructor}{\text{UpdateCommittee}}}}\, \\ \,\htmlId{16709}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Conway.Specification.Gov.html#16710}{\htmlId{16710}{\htmlClass{Bound}{\text{new}}}}\, , \,\href{Ledger.Conway.Specification.Gov.html#16716}{\htmlId{16716}{\htmlClass{Bound}{\text{rem}}}}\, , \,\href{Ledger.Conway.Specification.Gov.html#16722}{\htmlId{16722}{\htmlClass{Bound}{\text{q}}}}\,\,\htmlId{16723}{\htmlClass{Symbol}{\text{)}}}\, \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.Specification.Gov.Actions.html#2029}{\htmlId{16916}{\htmlClass{InductiveConstructor}{\text{ChangePParams}}}}\, \\ \,\href{Ledger.Conway.Specification.Gov.html#16932}{\htmlId{16932}{\htmlClass{Bound}{\text{x}}}}\, \end{pmatrix}$ = ppdWellFormed x actionWellFormed $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#2067}{\htmlId{16975}{\htmlClass{InductiveConstructor}{\text{TreasuryWithdrawal}}}}\, \\ \,\href{Ledger.Conway.Specification.Gov.html#16997}{\htmlId{16997}{\htmlClass{Bound}{\text{x}}}}\, \end{pmatrix}$ = (∀[ a ∈ dom x ] NetworkIdOf a ≡ NetworkId) × (∃[ v ∈ range x ] ¬ (v ≡ 0)) actionWellFormed _ = ⊤
-
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
TreasuryWithdrawal
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
TreasuryWithdrawal
action is well-formed if the network ID is correct and there is at least one non-zero withdrawal amount in the givenRwdAddrToCoinMap
map.
The GOV Transition System¶
The GOV
transition rule has the following type signature:
data _⊢_⇀⦇_,GOV⦈_ : GovEnv × ℕ → GovState → GovVote ⊎ GovProposal → GovState → Type where GOV-Vote : ∙ (aid , ast) ∈ fromList s ∙ canVote (PParamsOf Γ) (action ast) (gvRole voter) ∙ isRegistered Γ voter ∙ ¬ expired (Γ .epoch) ast ─────────────────────────────────────── (Γ , k) ⊢ s ⇀⦇ inj₁ $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.html#2968}{\htmlId{19729}{\htmlClass{Generalizable}{\text{aid}}}}\, \\ \,\href{Ledger.Conway.Specification.Gov.html#2991}{\htmlId{19735}{\htmlClass{Generalizable}{\text{voter}}}}\, \\ \,\href{Ledger.Conway.Specification.Gov.html#3030}{\htmlId{19743}{\htmlClass{Generalizable}{\text{v}}}}\, \\ \,\href{Ledger.Conway.Specification.Gov.html#19158}{\htmlId{19747}{\htmlClass{Generalizable}{\text{machr}}}}\, \end{pmatrix}$ ,GOV⦈ addVote s aid voter v GOV-Propose : let pp = PParamsOf Γ e = Γ .epoch enactState = EnactStateOf Γ 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 (GovActionTypeOf a) prev ∙ NetworkIdOf addr ≡ NetworkId ∙ CredentialOf addr ∈ rewardCreds ─────────────────────────────────────── (Γ , k) ⊢ s ⇀⦇ inj₂ prop ,GOV⦈ addAction s (pp .govActionLifetime +ᵉ e) (Γ .txid , k) addr a prev
The GOVS
transition rule is actually a function with following signature:
_⊢_⇀⦇_,GOVS⦈_ : GovEnv → GovState → List (GovVote ⊎ GovProposal) → GovState → Type
Specifically, it is defined as a reduction combinator that applies the
GOV
rule at each step.2
_⊢_⇀⦇_,GOVS⦈_ = ReflexiveTransitiveClosureᵢ {sts = _⊢_⇀⦇_,GOV⦈_}
For GOVVote
, we check that the governance
action being voted on exists; that the voter’s role is allowed to vote
(see canVote
in Section Functions related to voting; and
that the voter’s credential is actually associated with their role (see
isRegistered
in the section on the
Type signature of the GOV transition relation.
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
the section on Validity and Wellformedness Predicates.