Skip to content

Gov Actions

This section is part of the Ledger.Conway.Specification.Gov.Actions module of the formal ledger specification.

We introduce the following distinct bodies with specific functions in the new governance framework:

  1. a constitutional committee (henceforth called CC);

  2. a group of delegate representatives (henceforth called );

  3. the stake pool operators (henceforth called SPOs).

{-# OPTIONS --safe #-}

open import Data.Nat.Properties using (+-0-monoid)
open import Data.Rational using (ℚ; 0ℚ; 1ℚ)

open import Tactic.Derive.Show

open import Ledger.Prelude as P hiding (yes; no)
open import Ledger.Conway.Specification.Gov.Base

module Ledger.Conway.Specification.Gov.Actions (gs : _) (open GovStructure gs) where

Gov actions

data GovRole : Type where
  CC DRep SPO : GovRole

GovRoleCredential : GovRole → Type
GovRoleCredential CC   = Credential
GovRoleCredential DRep = Credential
GovRoleCredential SPO  = KeyHash

record GovVoter : Type where

  constructor ⟦_,_⟧ᵍᵛ

  field
    gvRole       : GovRole
    gvCredential : GovRoleCredential gvRole


data VDeleg : Type where
  vDelegCredential   : Credential → VDeleg
  vDelegAbstain      : VDeleg
  vDelegNoConfidence : VDeleg

GovActionID VoteDelegs : Type
GovActionID  = TxId × ℕ
VoteDelegs   = Credential ⇀ VDeleg

record Anchor : Type where
  field
    url   : String
    hash  : DocHash

data GovActionType : Type where
  NoConfidence        : GovActionType
  UpdateCommittee     : GovActionType
  NewConstitution     : GovActionType
  TriggerHardFork     : GovActionType
  ChangePParams       : GovActionType
  TreasuryWithdrawal  : GovActionType
  Info                : GovActionType

record HasVoteDelegs {a} (A : Type a) : Type a where
  field VoteDelegsOf : A → VoteDelegs
open HasVoteDelegs ⦃...⦄ public

record HasGovActionType (A : Type) : Type where
  field GovActionTypeOf : A → GovActionType
open HasGovActionType ⦃...⦄ public


GovActionData : GovActionType → Type
GovActionData NoConfidence        = ⊤
GovActionData UpdateCommittee     = (Credential ⇀ Epoch) × ℙ Credential × ℚ
GovActionData NewConstitution     = DocHash × Maybe ScriptHash
GovActionData TriggerHardFork     = ProtVer
GovActionData ChangePParams       = PParamsUpdate
GovActionData TreasuryWithdrawal  = Withdrawals
GovActionData Info                = ⊤

record GovAction : Type where

  constructor ⟦_,_⟧ᵍᵃ

  field
    gaType : GovActionType
    gaData : GovActionData gaType

open GovAction public

record HasGovAction (A : Type) : Type where
  field GovActionOf : A → GovAction
open HasGovAction ⦃...⦄ public

instance
  HasGovActionType-GovAction : HasGovActionType GovAction
  HasGovActionType-GovAction .GovActionTypeOf = GovAction.gaType

instance
  HasCast-GovAction-Sigma : HasCast GovAction (Σ GovActionType GovActionData)
  HasCast-GovAction-Sigma .cast x = x .gaType , x .gaData

  unquoteDecl Show-GovRole = derive-Show [ (quote GovRole , Show-GovRole) ]

Section Gov actions defines several data types used to represent governance actions. The type DocHash is abstract but in the implementation it will be instantiated with a 32-bit hash type (like e.g. ScriptHash). We keep it separate because it is used for a different purpose.

  • GovActionID: a unique identifier for a governance action, consisting of the TxId of the proposing transaction and an index to identify a proposal within a transaction;

  • GovRole (governance role): one of three available voter roles defined above (CC, DRep, SPO);

  • VDeleg (voter delegation): one of three ways to delegate votes: by credential (vDelegCredential), abstention (vDelegAbstain), or no confidence (vDelegNoConfidence);

  • Anchor: a url and a document hash;

  • GovAction (governance action): one of seven possible actions (see Section Gov Actions for definitions);

The governance actions carry the following information:

  • UpdateCommittee: a map of credentials and terms to add and a set of credentials to remove from the committee;

  • NewConstitution: a hash of the new constitution document and an optional proposal policy;

  • TriggerHardFork: the protocol version of the epoch to hard fork into;

  • ChangePParams: the updates to the parameters; and

  • TreasuryWithdrawal: a map of withdrawals.

Table: Types of governance actions

Action Description
NoConfidence a motion to create a state of no-confidence in the current constitutional committee
UpdateCommittee changes to the members of the constitutional committee and/or to its signature threshold and/or terms
NewConstitution a modification to the off-chain Constitution and the proposal policy script
TriggerHardFork triggers a non-backwards compatible upgrade of the network; requires a prior software upgrade
ChangePParams a change to one or more updatable protocol parameters, excluding changes to major protocol versions (“hard forks”)
TreasuryWithdrawal movements from the treasury
Info an action that has no effect on-chain, other than an on-chain record

Hash Protection

For some governance actions, in addition to obtaining the necessary votes, enactment requires that the following condition is also satisfied: the state obtained by enacting the proposal is in fact the state that was intended when the proposal was submitted. This is achieved by requiring actions to unambiguously link to the state they are modifying via a pointer to the previous modification. A proposal can only be enacted if it contains the of the previously enacted proposal modifying the same piece of state. NoConfidence and UpdateCommittee modify the same state, while every other type of governance action has its own state that isn’t shared with any other action. This means that the enactibility of a proposal can change when other proposals are enacted.

However, not all types of governance actions require this strict protection. For TreasuryWithdrawal and Info, enacting them does not change the state in non-commutative ways, so they can always be enacted.

Types related to this hash protection scheme are defined in Section NeedsHash and HashProtected types.

NeedsHash and HashProtected types

NeedsHash : GovActionType → Type
NeedsHash NoConfidence        = GovActionID
NeedsHash UpdateCommittee     = GovActionID
NeedsHash NewConstitution     = GovActionID
NeedsHash TriggerHardFork     = GovActionID
NeedsHash ChangePParams       = GovActionID
NeedsHash TreasuryWithdrawal  = ⊤
NeedsHash Info                = ⊤

HashProtected : Type → Type
HashProtected A = A × GovActionID

instance
  HasCast-HashProtected : ∀ {A : Type} → HasCast (HashProtected A) A
  HasCast-HashProtected .cast = proj₁

  HasCast-HashProtected-MaybeScriptHash : HasCast (HashProtected (DocHash × Maybe ScriptHash)) (Maybe ScriptHash)
  HasCast-HashProtected-MaybeScriptHash .cast = proj₂ ∘ proj₁

Vote and proposal types

data Vote : Type where
  yes no abstain  : Vote

record GovVote : Type where
  field
    gid         : GovActionID
    voter       : GovVoter
    vote        : Vote
    anchor      : Maybe Anchor

record GovProposal : Type where
  field
    action      : GovAction
    prevAction  : NeedsHash (gaType action)
    policy      : Maybe ScriptHash
    deposit     : Coin
    returnAddr  : RwdAddr
    anchor      : Anchor

record GovVotes : Type where
  field
    gvCC   : Credential ⇀ Vote
    gvDRep : Credential ⇀ Vote
    gvSPO  : KeyHash ⇀ Vote

record GovActionState : Type where
  field
    votes       : GovVotes
    returnAddr  : RwdAddr
    expiresIn   : Epoch
    action      : GovAction
    prevAction  : NeedsHash (gaType action)

instance
  HasGovAction-GovProposal : HasGovAction GovProposal
  HasGovAction-GovProposal .GovActionOf = GovProposal.action

  HasGovAction-GovActionState : HasGovAction GovActionState
  HasGovAction-GovActionState .GovActionOf = GovActionState.action

  HasGovActionType-GovProposal : HasGovActionType GovProposal
  HasGovActionType-GovProposal .GovActionTypeOf = GovActionTypeOf ∘ GovActionOf

  HasGovActionType-GovActionState : HasGovActionType GovActionState
  HasGovActionType-GovActionState .GovActionTypeOf = GovActionTypeOf ∘ GovActionOf

instance
  unquoteDecl DecEq-GovActionType = derive-DecEq ((quote GovActionType , DecEq-GovActionType) ∷ [])
  unquoteDecl DecEq-GovRole       = derive-DecEq ((quote GovRole , DecEq-GovRole) ∷ [])
  unquoteDecl DecEq-Vote          = derive-DecEq ((quote Vote    , DecEq-Vote)    ∷ [])
  unquoteDecl DecEq-VDeleg        = derive-DecEq ((quote VDeleg  , DecEq-VDeleg)  ∷ [])

  DecEq-GovVoter : DecEq GovVoter
  DecEq-GovVoter ._≟_ $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#1200}{\htmlId{10327}{\htmlClass{InductiveConstructor}{\text{CC}}}}\,   \\ \,\href{Ledger.Conway.Specification.Gov.Actions.html#10334}{\htmlId{10334}{\htmlClass{Bound}{\text{c}}}}\, \end{pmatrix}$ $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#1200}{\htmlId{10342}{\htmlClass{InductiveConstructor}{\text{CC}}}}\,   \\ \,\href{Ledger.Conway.Specification.Gov.Actions.html#10349}{\htmlId{10349}{\htmlClass{Bound}{\text{c'}}}}\, \end{pmatrix}$
    with c ≟ c'
  ... | P.yes p = P.yes (cong $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#1200}{\htmlId{10404}{\htmlClass{InductiveConstructor}{\text{CC}}}}\, \\ \,\href{Ledger.Conway.Specification.Gov.Actions.html#10386}{\htmlId{10413}{\htmlClass{Bound}{\text{p}}}}\,\,\htmlId{10414}{\htmlClass{Symbol}{\text{)}}}\,
  \,\htmlId{10418}{\htmlClass{Symbol}{\text{...}}}\, \,\htmlId{10422}{\htmlClass{Symbol}{\text{|}}}\, \,\href{Relation.Nullary.Decidable.Core.html#2136}{\htmlId{10424}{\htmlClass{InductiveConstructor}{\text{P.no}}}}\, \,\href{Ledger.Conway.Specification.Gov.Actions.html#10429}{\htmlId{10429}{\htmlClass{Bound}{\text{¬p}}}}\, \,\htmlId{10432}{\htmlClass{Symbol}{\text{=}}}\, \,\href{Relation.Nullary.Decidable.Core.html#2136}{\htmlId{10434}{\htmlClass{InductiveConstructor}{\text{P.no}}}}\, \,\htmlId{10439}{\htmlClass{Symbol}{\text{(λ}}}\, \,\htmlId{10442}{\htmlClass{Symbol}{\text{{}}}\, \,\href{Agda.Builtin.Equality.html#207}{\htmlId{10444}{\htmlClass{InductiveConstructor}{\text{refl}}}}\, \,\htmlId{10449}{\htmlClass{Symbol}{\text{→}}}\, \,\href{Ledger.Conway.Specification.Gov.Actions.html#10429}{\htmlId{10451}{\htmlClass{Bound}{\text{¬p}}}}\, \,\href{Agda.Builtin.Equality.html#207}{\htmlId{10454}{\htmlClass{InductiveConstructor}{\text{refl}}}}\,\,\htmlId{10458}{\htmlClass{Symbol}{\text{})}}}\,
  \,\href{Ledger.Conway.Specification.Gov.Actions.html#10271}{\htmlId{10463}{\htmlClass{Function}{\text{DecEq-GovVoter}}}}\, \,\htmlId{10478}{\htmlClass{Symbol}{\text{.}}}\,\,\href{Class.DecEq.Core.html#168}{\htmlId{10479}{\htmlClass{Field Operator}{\text{\_≟\_}}}}\, \begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#1200}{\htmlId{10485}{\htmlClass{InductiveConstructor}{\text{CC}}}}\,   \\ \,\href{Ledger.Conway.Specification.Gov.Actions.html#10492}{\htmlId{10492}{\htmlClass{Bound}{\text{c}}}}\, \end{pmatrix} \begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#1203}{\htmlId{10500}{\htmlClass{InductiveConstructor}{\text{DRep}}}}\, \\ \,\href{Ledger.Conway.Specification.Gov.Actions.html#10507}{\htmlId{10507}{\htmlClass{Bound}{\text{c'}}}}\, \end{pmatrix} \,\htmlId{10514}{\htmlClass{Symbol}{\text{=}}}\, \,\href{Relation.Nullary.Decidable.Core.html#2136}{\htmlId{10516}{\htmlClass{InductiveConstructor}{\text{P.no}}}}\, \,\htmlId{10521}{\htmlClass{Symbol}{\text{λ}}}\, \,\htmlId{10523}{\htmlClass{Symbol}{\text{()}}}\,
  \,\href{Ledger.Conway.Specification.Gov.Actions.html#10271}{\htmlId{10528}{\htmlClass{Function}{\text{DecEq-GovVoter}}}}\, \,\htmlId{10543}{\htmlClass{Symbol}{\text{.}}}\,\,\href{Class.DecEq.Core.html#168}{\htmlId{10544}{\htmlClass{Field Operator}{\text{\_≟\_}}}}\, \begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#1200}{\htmlId{10550}{\htmlClass{InductiveConstructor}{\text{CC}}}}\,   , \,\href{Ledger.Conway.Specification.Gov.Actions.html#10557}{\htmlId{10557}{\htmlClass{Bound}{\text{c}}}}\, \end{pmatrix} \begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#1208}{\htmlId{10565}{\htmlClass{InductiveConstructor}{\text{SPO}}}}\,  , \,\href{Ledger.Conway.Specification.Gov.Actions.html#10572}{\htmlId{10572}{\htmlClass{Bound}{\text{c'}}}}\, \end{pmatrix} \,\htmlId{10579}{\htmlClass{Symbol}{\text{=}}}\, \,\href{Relation.Nullary.Decidable.Core.html#2136}{\htmlId{10581}{\htmlClass{InductiveConstructor}{\text{P.no}}}}\, \,\htmlId{10586}{\htmlClass{Symbol}{\text{λ}}}\, \,\htmlId{10588}{\htmlClass{Symbol}{\text{()}}}\,
  \,\href{Ledger.Conway.Specification.Gov.Actions.html#10271}{\htmlId{10593}{\htmlClass{Function}{\text{DecEq-GovVoter}}}}\, \,\htmlId{10608}{\htmlClass{Symbol}{\text{.}}}\,\,\href{Class.DecEq.Core.html#168}{\htmlId{10609}{\htmlClass{Field Operator}{\text{\_≟\_}}}}\, \begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#1203}{\htmlId{10615}{\htmlClass{InductiveConstructor}{\text{DRep}}}}\, , \,\href{Ledger.Conway.Specification.Gov.Actions.html#10622}{\htmlId{10622}{\htmlClass{Bound}{\text{c}}}}\, \end{pmatrix} \begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#1200}{\htmlId{10630}{\htmlClass{InductiveConstructor}{\text{CC}}}}\,   , \,\href{Ledger.Conway.Specification.Gov.Actions.html#10637}{\htmlId{10637}{\htmlClass{Bound}{\text{c'}}}}\, \end{pmatrix} \,\htmlId{10644}{\htmlClass{Symbol}{\text{=}}}\, \,\href{Relation.Nullary.Decidable.Core.html#2136}{\htmlId{10646}{\htmlClass{InductiveConstructor}{\text{P.no}}}}\, \,\htmlId{10651}{\htmlClass{Symbol}{\text{λ}}}\, \,\htmlId{10653}{\htmlClass{Symbol}{\text{()}}}\,
  \,\href{Ledger.Conway.Specification.Gov.Actions.html#10271}{\htmlId{10658}{\htmlClass{Function}{\text{DecEq-GovVoter}}}}\, \,\htmlId{10673}{\htmlClass{Symbol}{\text{.}}}\,\,\href{Class.DecEq.Core.html#168}{\htmlId{10674}{\htmlClass{Field Operator}{\text{\_≟\_}}}}\, \begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#1203}{\htmlId{10680}{\htmlClass{InductiveConstructor}{\text{DRep}}}}\, , \,\href{Ledger.Conway.Specification.Gov.Actions.html#10687}{\htmlId{10687}{\htmlClass{Bound}{\text{c}}}}\, \end{pmatrix} \begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#1203}{\htmlId{10695}{\htmlClass{InductiveConstructor}{\text{DRep}}}}\, , \,\href{Ledger.Conway.Specification.Gov.Actions.html#10702}{\htmlId{10702}{\htmlClass{Bound}{\text{c'}}}}\, \end{pmatrix}
    \,\htmlId{10713}{\htmlClass{Keyword}{\text{with}}}\, \,\href{Ledger.Conway.Specification.Gov.Actions.html#10687}{\htmlId{10718}{\htmlClass{Bound}{\text{c}}}}\, \,\href{Class.DecEq.Core.html#168}{\htmlId{10720}{\htmlClass{Field Operator}{\text{≟}}}}\, \,\href{Ledger.Conway.Specification.Gov.Actions.html#10702}{\htmlId{10722}{\htmlClass{Bound}{\text{c'}}}}\,
  \,\htmlId{10727}{\htmlClass{Symbol}{\text{...}}}\, \,\htmlId{10731}{\htmlClass{Symbol}{\text{|}}}\, \,\href{Relation.Nullary.Decidable.Core.html#2099}{\htmlId{10733}{\htmlClass{InductiveConstructor}{\text{P.yes}}}}\, \,\href{Ledger.Conway.Specification.Gov.Actions.html#10739}{\htmlId{10739}{\htmlClass{Bound}{\text{p}}}}\, \,\htmlId{10741}{\htmlClass{Symbol}{\text{=}}}\, \,\href{Relation.Nullary.Decidable.Core.html#2099}{\htmlId{10743}{\htmlClass{InductiveConstructor}{\text{P.yes}}}}\, \,\htmlId{10749}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Relation.Binary.PropositionalEquality.Core.html#1481}{\htmlId{10750}{\htmlClass{Function}{\text{cong}}}}\, \begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#1203}{\htmlId{10757}{\htmlClass{InductiveConstructor}{\text{DRep}}}}\, , \,\href{Ledger.Conway.Specification.Gov.Actions.html#10739}{\htmlId{10768}{\htmlClass{Bound}{\text{p}}}}\,\,\htmlId{10769}{\htmlClass{Symbol}{\text{)}}}\,
  \,\htmlId{10773}{\htmlClass{Symbol}{\text{...}}}\, \,\htmlId{10777}{\htmlClass{Symbol}{\text{|}}}\, \,\href{Relation.Nullary.Decidable.Core.html#2136}{\htmlId{10779}{\htmlClass{InductiveConstructor}{\text{P.no}}}}\, \,\href{Ledger.Conway.Specification.Gov.Actions.html#10784}{\htmlId{10784}{\htmlClass{Bound}{\text{¬p}}}}\, \,\htmlId{10787}{\htmlClass{Symbol}{\text{=}}}\, \,\href{Relation.Nullary.Decidable.Core.html#2136}{\htmlId{10789}{\htmlClass{InductiveConstructor}{\text{P.no}}}}\, \,\htmlId{10794}{\htmlClass{Symbol}{\text{(λ}}}\, \,\htmlId{10797}{\htmlClass{Symbol}{\text{{}}}\, \,\href{Agda.Builtin.Equality.html#207}{\htmlId{10799}{\htmlClass{InductiveConstructor}{\text{refl}}}}\, \,\htmlId{10804}{\htmlClass{Symbol}{\text{→}}}\, \,\href{Ledger.Conway.Specification.Gov.Actions.html#10784}{\htmlId{10806}{\htmlClass{Bound}{\text{¬p}}}}\, \,\href{Agda.Builtin.Equality.html#207}{\htmlId{10809}{\htmlClass{InductiveConstructor}{\text{refl}}}}\,\,\htmlId{10813}{\htmlClass{Symbol}{\text{})}}}\,
  \,\href{Ledger.Conway.Specification.Gov.Actions.html#10271}{\htmlId{10818}{\htmlClass{Function}{\text{DecEq-GovVoter}}}}\, \,\htmlId{10833}{\htmlClass{Symbol}{\text{.}}}\,\,\href{Class.DecEq.Core.html#168}{\htmlId{10834}{\htmlClass{Field Operator}{\text{\_≟\_}}}}\, \begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#1203}{\htmlId{10840}{\htmlClass{InductiveConstructor}{\text{DRep}}}}\, , \,\href{Ledger.Conway.Specification.Gov.Actions.html#10847}{\htmlId{10847}{\htmlClass{Bound}{\text{c}}}}\, \end{pmatrix} \begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#1208}{\htmlId{10855}{\htmlClass{InductiveConstructor}{\text{SPO}}}}\,  , \,\href{Ledger.Conway.Specification.Gov.Actions.html#10862}{\htmlId{10862}{\htmlClass{Bound}{\text{c'}}}}\, \end{pmatrix} \,\htmlId{10869}{\htmlClass{Symbol}{\text{=}}}\, \,\href{Relation.Nullary.Decidable.Core.html#2136}{\htmlId{10871}{\htmlClass{InductiveConstructor}{\text{P.no}}}}\, \,\htmlId{10876}{\htmlClass{Symbol}{\text{λ}}}\, \,\htmlId{10878}{\htmlClass{Symbol}{\text{()}}}\,
  \,\href{Ledger.Conway.Specification.Gov.Actions.html#10271}{\htmlId{10883}{\htmlClass{Function}{\text{DecEq-GovVoter}}}}\, \,\htmlId{10898}{\htmlClass{Symbol}{\text{.}}}\,\,\href{Class.DecEq.Core.html#168}{\htmlId{10899}{\htmlClass{Field Operator}{\text{\_≟\_}}}}\, \begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#1208}{\htmlId{10905}{\htmlClass{InductiveConstructor}{\text{SPO}}}}\,  , \,\href{Ledger.Conway.Specification.Gov.Actions.html#10912}{\htmlId{10912}{\htmlClass{Bound}{\text{c}}}}\, \end{pmatrix} \begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#1200}{\htmlId{10920}{\htmlClass{InductiveConstructor}{\text{CC}}}}\,   , \,\href{Ledger.Conway.Specification.Gov.Actions.html#10927}{\htmlId{10927}{\htmlClass{Bound}{\text{c'}}}}\, \end{pmatrix} \,\htmlId{10934}{\htmlClass{Symbol}{\text{=}}}\, \,\href{Relation.Nullary.Decidable.Core.html#2136}{\htmlId{10936}{\htmlClass{InductiveConstructor}{\text{P.no}}}}\, \,\htmlId{10941}{\htmlClass{Symbol}{\text{λ}}}\, \,\htmlId{10943}{\htmlClass{Symbol}{\text{()}}}\,
  \,\href{Ledger.Conway.Specification.Gov.Actions.html#10271}{\htmlId{10948}{\htmlClass{Function}{\text{DecEq-GovVoter}}}}\, \,\htmlId{10963}{\htmlClass{Symbol}{\text{.}}}\,\,\href{Class.DecEq.Core.html#168}{\htmlId{10964}{\htmlClass{Field Operator}{\text{\_≟\_}}}}\, \begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#1208}{\htmlId{10970}{\htmlClass{InductiveConstructor}{\text{SPO}}}}\,  , \,\href{Ledger.Conway.Specification.Gov.Actions.html#10977}{\htmlId{10977}{\htmlClass{Bound}{\text{c}}}}\, \end{pmatrix} \begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#1203}{\htmlId{10985}{\htmlClass{InductiveConstructor}{\text{DRep}}}}\, , \,\href{Ledger.Conway.Specification.Gov.Actions.html#10992}{\htmlId{10992}{\htmlClass{Bound}{\text{c'}}}}\, \end{pmatrix} \,\htmlId{10999}{\htmlClass{Symbol}{\text{=}}}\, \,\href{Relation.Nullary.Decidable.Core.html#2136}{\htmlId{11001}{\htmlClass{InductiveConstructor}{\text{P.no}}}}\, \,\htmlId{11006}{\htmlClass{Symbol}{\text{λ}}}\, \,\htmlId{11008}{\htmlClass{Symbol}{\text{()}}}\,
  \,\href{Ledger.Conway.Specification.Gov.Actions.html#10271}{\htmlId{11013}{\htmlClass{Function}{\text{DecEq-GovVoter}}}}\, \,\htmlId{11028}{\htmlClass{Symbol}{\text{.}}}\,\,\href{Class.DecEq.Core.html#168}{\htmlId{11029}{\htmlClass{Field Operator}{\text{\_≟\_}}}}\, \begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#1208}{\htmlId{11035}{\htmlClass{InductiveConstructor}{\text{SPO}}}}\,  , \,\href{Ledger.Conway.Specification.Gov.Actions.html#11042}{\htmlId{11042}{\htmlClass{Bound}{\text{c}}}}\, \end{pmatrix} \begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#1208}{\htmlId{11050}{\htmlClass{InductiveConstructor}{\text{SPO}}}}\,  , \,\href{Ledger.Conway.Specification.Gov.Actions.html#11057}{\htmlId{11057}{\htmlClass{Bound}{\text{c'}}}}\, \end{pmatrix}
    \,\htmlId{11068}{\htmlClass{Keyword}{\text{with}}}\, \,\href{Ledger.Conway.Specification.Gov.Actions.html#11042}{\htmlId{11073}{\htmlClass{Bound}{\text{c}}}}\, \,\href{Class.DecEq.Core.html#168}{\htmlId{11075}{\htmlClass{Field Operator}{\text{≟}}}}\, \,\href{Ledger.Conway.Specification.Gov.Actions.html#11057}{\htmlId{11077}{\htmlClass{Bound}{\text{c'}}}}\,
  \,\htmlId{11082}{\htmlClass{Symbol}{\text{...}}}\, \,\htmlId{11086}{\htmlClass{Symbol}{\text{|}}}\, \,\href{Relation.Nullary.Decidable.Core.html#2099}{\htmlId{11088}{\htmlClass{InductiveConstructor}{\text{P.yes}}}}\, \,\href{Ledger.Conway.Specification.Gov.Actions.html#11094}{\htmlId{11094}{\htmlClass{Bound}{\text{p}}}}\, \,\htmlId{11096}{\htmlClass{Symbol}{\text{=}}}\, \,\href{Relation.Nullary.Decidable.Core.html#2099}{\htmlId{11098}{\htmlClass{InductiveConstructor}{\text{P.yes}}}}\, \,\htmlId{11104}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Relation.Binary.PropositionalEquality.Core.html#1481}{\htmlId{11105}{\htmlClass{Function}{\text{cong}}}}\, \begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#1208}{\htmlId{11112}{\htmlClass{InductiveConstructor}{\text{SPO}}}}\, , \,\href{Ledger.Conway.Specification.Gov.Actions.html#11094}{\htmlId{11122}{\htmlClass{Bound}{\text{p}}}}\,\,\htmlId{11123}{\htmlClass{Symbol}{\text{)}}}\,
  \,\htmlId{11127}{\htmlClass{Symbol}{\text{...}}}\, \,\htmlId{11131}{\htmlClass{Symbol}{\text{|}}}\, \,\href{Relation.Nullary.Decidable.Core.html#2136}{\htmlId{11133}{\htmlClass{InductiveConstructor}{\text{P.no}}}}\, \,\href{Ledger.Conway.Specification.Gov.Actions.html#11138}{\htmlId{11138}{\htmlClass{Bound}{\text{¬p}}}}\, \,\htmlId{11141}{\htmlClass{Symbol}{\text{=}}}\, \,\href{Relation.Nullary.Decidable.Core.html#2136}{\htmlId{11143}{\htmlClass{InductiveConstructor}{\text{P.no}}}}\, \,\htmlId{11148}{\htmlClass{Symbol}{\text{(λ}}}\, \,\htmlId{11151}{\htmlClass{Symbol}{\text{{}}}\, \,\href{Agda.Builtin.Equality.html#207}{\htmlId{11153}{\htmlClass{InductiveConstructor}{\text{refl}}}}\, \,\htmlId{11158}{\htmlClass{Symbol}{\text{→}}}\, \,\href{Ledger.Conway.Specification.Gov.Actions.html#11138}{\htmlId{11160}{\htmlClass{Bound}{\text{¬p}}}}\, \,\href{Agda.Builtin.Equality.html#207}{\htmlId{11163}{\htmlClass{InductiveConstructor}{\text{refl}}}}\,\,\htmlId{11167}{\htmlClass{Symbol}{\text{})}}}\,

  \,\htmlId{11173}{\htmlClass{Keyword}{\text{unquoteDecl}}}\, \,\href{Ledger.Conway.Specification.Gov.Actions.html#11185}{\htmlId{11185}{\htmlClass{Function}{\text{HasCast-GovVote}}}}\, \,\htmlId{11201}{\htmlClass{Symbol}{\text{=}}}\, \,\href{stdlib-classes.Class.HasCast.Derive.html#2690}{\htmlId{11203}{\htmlClass{Function}{\text{derive-HasCast}}}}\, \,\href{Data.List.Base.html#4907}{\htmlId{11218}{\htmlClass{Function Operator}{\text{[}}}}\, \,\htmlId{11220}{\htmlClass{Symbol}{\text{(}}}\,\,\htmlId{11221}{\htmlClass{Keyword}{\text{quote}}}\, \,\href{Ledger.Conway.Specification.Gov.Actions.html#8644}{\htmlId{11227}{\htmlClass{Record}{\text{GovVote}}}}\, , \,\href{Ledger.Conway.Specification.Gov.Actions.html#11185}{\htmlId{11237}{\htmlClass{Function}{\text{HasCast-GovVote}}}}\,\,\htmlId{11252}{\htmlClass{Symbol}{\text{)}}}\, \,\href{Data.List.Base.html#4907}{\htmlId{11254}{\htmlClass{Function Operator}{\text{]}}}}\,

  \,\htmlId{11259}{\htmlClass{Keyword}{\text{unquoteDecl}}}\, \,\href{Ledger.Conway.Specification.Gov.Actions.html#11271}{\htmlId{11271}{\htmlClass{Function}{\text{Show-VDeleg}}}}\, \,\htmlId{11283}{\htmlClass{Symbol}{\text{=}}}\, \,\href{Tactic.Derive.Show.html#2038}{\htmlId{11285}{\htmlClass{Function}{\text{derive-Show}}}}\, \,\href{Data.List.Base.html#4907}{\htmlId{11297}{\htmlClass{Function Operator}{\text{[}}}}\, \,\htmlId{11299}{\htmlClass{Symbol}{\text{(}}}\,\,\htmlId{11300}{\htmlClass{Keyword}{\text{quote}}}\, \,\href{Ledger.Conway.Specification.Gov.Actions.html#1554}{\htmlId{11306}{\htmlClass{Datatype}{\text{VDeleg}}}}\, , \,\href{Ledger.Conway.Specification.Gov.Actions.html#11271}{\htmlId{11315}{\htmlClass{Function}{\text{Show-VDeleg}}}}\,\,\htmlId{11326}{\htmlClass{Symbol}{\text{)}}}\, \,\href{Data.List.Base.html#4907}{\htmlId{11328}{\htmlClass{Function Operator}{\text{]}}}}\,

Votes and Proposals

Gov helper function

isGovVoterDRep : GovVoter → Maybe Credential
isGovVoterDRep $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#1203}{\htmlId{11463}{\htmlClass{InductiveConstructor}{\text{DRep}}}}\, \\ \,\href{Ledger.Conway.Specification.Gov.Actions.html#11470}{\htmlId{11470}{\htmlClass{Bound}{\text{c}}}}\, \end{pmatrix}$ = just c
isGovVoterDRep _              = nothing

isGovVoterCredential : GovVoter → Maybe Credential
isGovVoterCredential $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#1200}{\htmlId{11600}{\htmlClass{InductiveConstructor}{\text{CC}}}}\,   \\ \,\href{Ledger.Conway.Specification.Gov.Actions.html#11607}{\htmlId{11607}{\htmlClass{Bound}{\text{c}}}}\, \end{pmatrix}$ = just c
isGovVoterCredential $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#1203}{\htmlId{11645}{\htmlClass{InductiveConstructor}{\text{DRep}}}}\, \\ \,\href{Ledger.Conway.Specification.Gov.Actions.html#11652}{\htmlId{11652}{\htmlClass{Bound}{\text{c}}}}\, \end{pmatrix}$ = just c
isGovVoterCredential _              = nothing

proposedCC : GovAction → ℙ Credential
proposedCC $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Gov.Actions.html#1915}{\htmlId{11765}{\htmlClass{InductiveConstructor}{\text{UpdateCommittee}}}}\, \\ \,\htmlId{11783}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Conway.Specification.Gov.Actions.html#11784}{\htmlId{11784}{\htmlClass{Bound}{\text{x}}}}\, , \,\htmlId{11788}{\htmlClass{Symbol}{\text{\_}}}\, , \,\htmlId{11792}{\htmlClass{Symbol}{\text{\_)}}}\, \end{pmatrix}$  = dom x
proposedCC _                                    = ∅

The data type Vote represents the different voting options: yes, no, or abstain. For a Vote to be cast, it must be packaged together with further information, such as who votes and for which governance action. This information is combined in the GovVote record. An optional Anchor can be provided to give context about why a vote was cast in a certain manner.

To propose a governance action, a GovProposal needs to be submitted. Beside the proposed action, it contains:

  • a pointer to the previous action if required (see Section Gov Actions),

  • a pointer to the proposal policy if one is required,

  • a deposit, which will be returned to returnAddr, and

  • an Anchor, providing further information about the proposal.

While the deposit is held, it is added to the deposit pot, similar to stake key deposits. It is also counted towards the voting stake (but not the block production stake) of the reward address to which it will be returned, so as not to reduce the submitter’s voting power when voting on their own (and competing) actions. For a proposal to be valid, the deposit must be set to the current value of govActionDeposit. The deposit will be returned when the action is removed from the state in any way.

GovActionState is the state of an individual governance action. It contains the individual votes, its lifetime, and information necessary to enact the action and to repay the deposit.