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:
-
addVoteinserts (and potentially overrides) a vote made for a particular governance action (identified by its ID) by a credential with a role. -
addActionadds a new proposed action at the end of a givenGovState. -
The
validHFActionproperty indicates whether a given proposal, if it is aTriggerHardForkaction, can potentially be enacted in the future. For this to be the case, itsprevActionneeds to exist, be anotherTriggerHardForkaction 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 → RewardAddress → (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 → RewardAddress → (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#1024}{\htmlId{8532}{\htmlClass{InductiveConstructor}{\text{CC}}}}\, \\ \,\href{Ledger.Conway.Specification.Gov.html#8537}{\htmlId{8537}{\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#1027}{\htmlId{8628}{\htmlClass{InductiveConstructor}{\text{DRep}}}}\, \\ \,\href{Ledger.Conway.Specification.Gov.html#8635}{\htmlId{8635}{\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#1032}{\htmlId{8726}{\htmlClass{InductiveConstructor}{\text{SPO}}}}\, \\ \,\href{Ledger.Conway.Specification.Gov.html#8732}{\htmlId{8732}{\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#1024}{\htmlId{8904}{\htmlClass{InductiveConstructor}{\text{CC}}}}\, \\ \,\href{Ledger.Conway.Specification.Gov.html#8911}{\htmlId{8911}{\htmlClass{Bound}{\text{c}}}}\, \end{pmatrix}$ → just c ∈ range (CCHotKeysOf (CertStateOf Γ) ∣ (ccCreds (cc (EnactStateOf Γ)))) $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#1027}{\htmlId{9007}{\htmlClass{InductiveConstructor}{\text{DRep}}}}\, \\ \,\href{Ledger.Conway.Specification.Gov.html#9014}{\htmlId{9014}{\htmlClass{Bound}{\text{c}}}}\, \end{pmatrix}$ → c ∈ dom (DRepsOf (CertStateOf Γ)) $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#1032}{\htmlId{9065}{\htmlClass{InductiveConstructor}{\text{SPO}}}}\, \\ \,\href{Ledger.Conway.Specification.Gov.html#9072}{\htmlId{9072}{\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#2614}{\htmlId{9215}{\htmlClass{InductiveConstructor}{\text{TriggerHardFork}}}}\, \\ \,\href{Ledger.Conway.Specification.Gov.html#9233}{\htmlId{9233}{\htmlClass{Bound}{\text{v}}}}\, \end{pmatrix}$ ; prevAction = prev }) s e = (aid' ≡ prev × pvCanFollow v ver) ⊎ ∃₂[ x , v' ] (prev , x) ∈ fromList s × x .action ≡ $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#2614}{\htmlId{9416}{\htmlClass{InductiveConstructor}{\text{TriggerHardFork}}}}\, \\ \,\href{Ledger.Conway.Specification.Gov.html#9316}{\htmlId{9434}{\htmlClass{Bound}{\text{v'}}}}\, \end{pmatrix}$ × (if pvCanFollowMajor v' ver then pvCanFollowMinor v v' else 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 Governance Functions section).
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 two predicates used in the GOVPropose case
of the GOV rule to ensure that a governance action is valid and well-formed. To make
sense of these predicates, one must understand how we represent and construct a
governance action. This is explained in the
Governance Actions Section.
actionValid : ℙ Credential → Maybe ScriptHash → Maybe ScriptHash → Epoch → GovAction → Type actionValid _ p ppolicy _ $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#2652}{\htmlId{16911}{\htmlClass{InductiveConstructor}{\text{ChangePParams}}}}\, \\ \,\htmlId{16927}{\htmlClass{Symbol}{\text{\_}}}\, \end{pmatrix}$ = p ≡ ppolicy actionValid rwdCreds p ppolicy _ $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#2690}{\htmlId{16982}{\htmlClass{InductiveConstructor}{\text{TreasuryWithdrawal}}}}\, \\ \,\href{Ledger.Conway.Specification.Gov.html#17003}{\htmlId{17003}{\htmlClass{Bound}{\text{wdrls}}}}\, \end{pmatrix}$ = p ≡ ppolicy × mapˢ CredentialOf (dom wdrls) ⊆ rwdCreds actionValid _ p _ epoch $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#2538}{\htmlId{17096}{\htmlClass{InductiveConstructor}{\text{UpdateCommittee}}}}\, \\ \,\htmlId{17114}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Conway.Specification.Gov.html#17115}{\htmlId{17115}{\htmlClass{Bound}{\text{new}}}}\, , \,\href{Ledger.Conway.Specification.Gov.html#17121}{\htmlId{17121}{\htmlClass{Bound}{\text{rem}}}}\, , \,\href{Ledger.Conway.Specification.Gov.html#17127}{\htmlId{17127}{\htmlClass{Bound}{\text{q}}}}\,\,\htmlId{17128}{\htmlClass{Symbol}{\text{)}}}\, \end{pmatrix}$ = p ≡ nothing × (∀[ e ∈ range new ] epoch < e) × dom new ∩ rem ≡ᵉ ∅ actionValid _ p _ _ _ = p ≡ nothing actionWellFormed : GovAction → Type actionWellFormed $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#2652}{\htmlId{17294}{\htmlClass{InductiveConstructor}{\text{ChangePParams}}}}\, \\ \,\href{Ledger.Conway.Specification.Gov.html#17310}{\htmlId{17310}{\htmlClass{Bound}{\text{ppup}}}}\, \end{pmatrix}$ = ppdWellFormed ppup actionWellFormed $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#2690}{\htmlId{17359}{\htmlClass{InductiveConstructor}{\text{TreasuryWithdrawal}}}}\, \\ \,\href{Ledger.Conway.Specification.Gov.html#17380}{\htmlId{17380}{\htmlClass{Bound}{\text{wdrls}}}}\, \end{pmatrix}$ = (∀[ a ∈ dom wdrls ] NetworkIdOf a ≡ NetworkId) × ∃[ v ∈ range wdrls ] ¬ (v ≡ 0) actionWellFormed _ = ⊤
-
actionValidensures that the proposed action is valid given the current state of the system:-
a
ChangePParamsaction is valid if the proposal policy is provided; -
a
TreasuryWithdrawalaction is valid if the proposal policy is provided and the reward stake credential is registered; -
an
UpdateCommitteeaction is valid if credentials of proposed candidates have not expired and the action does not propose to both add and remove the same candidate.
-
-
actionWellFormedensures that the proposed action is well-formed; there are two cases: -
a
ChangePParamsaction is well-formed if thePParamUpdate,ppup, preserves well-formedness of the protocol parameters, as expressed by theppdWellFormedpredicate (see Abstract Type for Parameter Updates). -
a
TreasuryWithdrawalaction is well-formed if the network ID is correct and theWithdrawalsmap,wdrls, includes at least one non-zero withdrawal amount.
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#2974}{\htmlId{20379}{\htmlClass{Generalizable}{\text{aid}}}}\, \\ \,\href{Ledger.Conway.Specification.Gov.html#2997}{\htmlId{20385}{\htmlClass{Generalizable}{\text{voter}}}}\, \\ \,\href{Ledger.Conway.Specification.Gov.html#3036}{\htmlId{20393}{\htmlClass{Generalizable}{\text{v}}}}\, \\ \,\href{Ledger.Conway.Specification.Gov.html#19808}{\htmlId{20397}{\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 [Voting Functions][]; 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.