Governance Actions¶

This section defines several concepts and types used to represent governance actions.

{-# OPTIONS --safe #-}

open import Ledger.Conway.Specification.Gov.Base

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

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)

Roles¶

There are three distinct roles with specific functions in the governance framework:

constitutional committee (henceforth called CC);
delegate representatives (henceforth called DReps);
stake pool operators (henceforth called SPOs).

data GovRole : Type where
  CC DRep SPO : GovRole

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

Actors belonging to each governance role are identified by a type of credential:

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

Actions¶

A governance action is one of the seven types described in the table below:

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

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

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

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;
TreasuryWithdrawal: a map of withdrawals.

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                = ⊤

A governance action consist of a type of governance action together with the necessary data:

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

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

Governance actions are uniquely identified by a GovActionID. This type consists of the TxId of the transaction that proposes the governance action together with an index that identifies the proposal within the transaction.

GovActionID : Type
GovActionID  = TxId × ℕ

Votes¶

The Vote type represents the three different voting options: yes, no, and abstain.

data Vote : Type where
  yes no abstain  : Vote

For a Vote to be cast, it must be packaged together with further information, such as who votes GovVoter 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.

record GovVoter : Type where

  constructor ⟦_,_⟧ᵍᵛ

  field
    gvRole       : GovRole
    gvCredential : GovRoleCredential gvRole

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

DocHash

The type DocHash is abstract but in the implementation it is instantiated with a 32-bit hash type (like, e.g., ScriptHash). We keep it separate because it is used for a different purpose.

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

Finally, we define the GovVotes type, an inhabitant of which is comprised of three maps that collect the votes cast by members of each of the three governance roles.

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

Vote Delegation¶

The type VDeleg represents the different ways in which voting stake can be delegated:

to the credential of a DRep (vDelegCredential);
to an abstention (vDelegAbstain);
to a vote of no confidence (vDelegNoConfidence).

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

VoteDelegs : Type
VoteDelegs   = Credential ⇀ VDeleg

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

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

The types we use to represent this hash protection scheme are as follows.

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₁

Governance Proposal Types¶

To propose a governance action, a GovProposal needs to be submitted. Beside the proposed action, it contains five other fields which we now describe.

prevAction: a pointer to the previous action if required (see Hash Protection);
policy: a pointer to the proposal policy if one is required;
deposit: a deposit, which will be returned to returnAddr;
returnAddr: a reward address to which the deposit will be returned when the proposal is removed from the state;
anchor: a placeholder which may be used to provide 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.

Policy : Type
Policy = Maybe ScriptHash

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