From acae025e64f646ca4c9b71310081c9640d3aea35 Mon Sep 17 00:00:00 2001 From: William DeMeo Date: Wed, 26 Jul 2023 21:45:43 -0600 Subject: [PATCH] Conway spec prose: GovernanceActions This addresses the GovernanceActions, Voting, and Enactment items in issue #145 --- src/Ledger/GovernanceActions.lagda | 196 +++++++++++++++++++++++++---- src/Ledger/PDF.lagda | 6 +- 2 files changed, 174 insertions(+), 28 deletions(-) diff --git a/src/Ledger/GovernanceActions.lagda b/src/Ledger/GovernanceActions.lagda index 286c69711..acf8a2181 100644 --- a/src/Ledger/GovernanceActions.lagda +++ b/src/Ledger/GovernanceActions.lagda @@ -1,4 +1,25 @@ -\section{Governance actions} +\section{Governance actions\protect\footnotemark} +\label{sec:governance-actions} +\footnotetext{See also: \href{https://github.com/cardano-foundation/CIPs/tree/master/CIP-1694}{github.com/cardano-foundation/CIPs/CIP-1694}} +%%\textit{Any Cardano user} will be allowed to submit a \defn{governance action}. +We introduce three distinct bodies that have specific functions in the new governance framework: +\begin{enumerate} +\item + a constitutional committee +\item + a group of delegate representatives (henceforth called \defn{DReps}) +\item + the stake pool operators (henceforth called \defn{SPOs}) +\end{enumerate} +Every governance action must be ratified by at least two of these three bodies using their on-chain \defn{votes}. +The type of action and the state of the governance system determines which bodies must ratify it. +Ratified actions are then \defn{enacted} on-chain, following a set of well-defined rules. +\\[4pt] +As with stake pools, any Ada holder may register to be a DRep and so choose to represent themselves and/or others. +Also, as with stake pools, Ada holders may instead delegate their voting rights to any other DRep. +Voting rights will be based on the total Ada that is delegated, as a whole number of Lovelace. +\\[4pt] +The most crucial aspect of this proposal is the notion of ``\textit{one Lovelace = one vote}''. \begin{code}[hide] {-# OPTIONS --safe #-} @@ -32,8 +53,53 @@ open import Tactic.Derive.DecEq open import MyDebugOptions 2ℚ = 1ℚ Data.Rational.+ 1ℚ - \end{code} + +Figure~\ref{defs:governance} defines several data types used to represent governance actions including: +\begin{itemize} + \item %%% \defn{identifier} (\AgdaSymbol{:}\, + \AgdaDatatype{GovActionId}---a pair consisting of a transaction id (\AgdaSymbol{:}\,\AgdaDatatype{TxId}) and a natural number (\AgdaSymbol{:}\,\AgdaDatatype{ℕ}); + \item %%% \defn{role} (\AgdaSymbol{:}\, + \AgdaDatatype{GovRole}---enumerates the available voter roles: \AgdaInductiveConstructor{CC}, \AgdaInductiveConstructor{DRep}, \AgdaInductiveConstructor{SPO}; + \item %%% \defn{voter delegation type} (\AgdaSymbol{:}\, + \AgdaDatatype{VDeleg}---enumerates the available ways to delegate votes: by a credential + (\AgdaInductiveConstructor{credVoter}), abstention (\AgdaInductiveConstructor{abstainRep}), or expressing no confidence (\AgdaInductiveConstructor{noConfidenceRep}); + \item %%% \defn{anchor} (\AgdaSymbol{:}\, + \AgdaRecord{Anchor}---an anchor with fields \AgdaField{url} (\AgdaSymbol{:}\,\AgdaDatatype{String}) and a document \AgdaField{hash} (\AgdaSymbol{:}\,\AgdaDatatype{DocHash}); + \item %%% \defn{governance action} (\AgdaSymbol{:}\, + \AgdaDatatype{GovAction}---enumerates the available governance actions + (\AgdaInductiveConstructor{NoConfidence}, \AgdaInductiveConstructor{NewCommittee}, + \AgdaInductiveConstructor{NewConstitution}, \AgdaInductiveConstructor{TriggerHF}, + \AgdaInductiveConstructor{ChangePParams}, \AgdaInductiveConstructor{TreasuryWdrl}, or + \AgdaInductiveConstructor{Info}). +\end{itemize} +The \AgdaDatatype{GovAction} type represents the seven available \defn{governance actions} described in Table~\ref{fig:types-of-governance-actions}. +\begin{table}[h] +\begin{longtable}[]{@{} + >{\raggedright\arraybackslash}p{(\columnwidth - 2\tabcolsep) * \real{0.35}} + >{\raggedright\arraybackslash}p{(\columnwidth - 2\tabcolsep) * \real{0.35}} + >{\raggedright\arraybackslash}p{(\columnwidth - 2\tabcolsep) * \real{0.15}}@{}} +\hline +\textbf{Action} & \textbf{Description} & \textbf{Agda type}\\ +\hline +\endhead +1. Motion of no-confidence & A motion to create a \defn{state of no-confidence} in the current constitutional committee & \AgdaInductiveConstructor{NoConfidence}\\ +2. New constitutional committee and/or threshold and/or term limits & Changes to the members of the constitutional committee and/or to its signature threshold and/or term limits & \AgdaInductiveConstructor{NewCommittee}\\ +3. Updates to the Constitution & A modification to the off-chain Constitution, recorded as an on-chain hash of the text document & \AgdaInductiveConstructor{NewConstitution}\\ +4. Hard fork\footnotemark & + Initiation triggers a non-backwards compatible upgrade of the network; requires a prior software upgrade & \AgdaInductiveConstructor{TriggerHF} \\ +5. Protocol Parameter Changes & Any change to \textit{one or more} updatable protocol parameters, excluding changes to major protocol versions (``hard forks'') & \AgdaInductiveConstructor{ChangePParams}\\ +6. Treasury Withdrawals & Movements from the treasury, sub-categorized into small, medium or large withdrawals (based on the amount of Lovelace to be withdrawn). The thresholds for treasury withdrawals are discussed below. & \AgdaInductiveConstructor{TreasuryWdrl} \\ +7. Info & An action that has no effect on-chain, other than an on-chain record. & \AgdaInductiveConstructor{Info}\\ +\hline +\end{longtable} +\caption{Types of governance actions} +\label{tab:types-of-governance-actions} +\end{table} +\footnotetext{There are many varying definitions of the term ``hard fork'' in the blockchain industry. Hard forks typically refer + to non-backwards compatible updates of a network. In Cardano, we formalize the definition slightly more by calling any upgrade that + would lead to \emph{more blocks} being validated a ``hard fork'' and force nodes to comply with the new protocol version, effectively + obsoleting nodes that are unable to handle the upgrade.} \begin{figure*}[h] \begin{code} GovActionID : Set @@ -61,10 +127,15 @@ data GovAction : Set where ChangePParams : UpdateT → PPHash → GovAction TreasuryWdrl : (Credential ⇀ Coin) → GovAction Info : GovAction +\end{code} +\caption{Governance actions} +\label{defs:governance} +\end{figure*} +\begin{code}[hide] actionWellFormed : GovAction → Bool -actionWellFormed (ChangePParams x _) = ppdWellFormed x -actionWellFormed _ = true +actionWellFormed (ChangePParams x _) = ppdWellFormed x +actionWellFormed _ = true maximum : ℙ ℚ → ℚ maximum x = foldl Data.Rational._⊔_ 0ℚ (proj₁ $ finiteness x) @@ -85,10 +156,10 @@ module _ (pp : PParams) (ccThreshold' : Maybe ℚ) where nothing → 2ℚ pparamThreshold : PParamGroup → ℚ - pparamThreshold NetworkGroup = P5a - pparamThreshold EconomicGroup = P5b - pparamThreshold TechnicalGroup = P5c - pparamThreshold GovernanceGroup = P5d + pparamThreshold NetworkGroup = P5a + pparamThreshold EconomicGroup = P5b + pparamThreshold TechnicalGroup = P5c + pparamThreshold GovernanceGroup = P5d P5 : UpdateT → ℚ P5 ppu = maximum $ map pparamThreshold (updateGroups ppu) @@ -112,7 +183,48 @@ NeedsHash (TriggerHF _) = GovActionID NeedsHash (ChangePParams _ _) = GovActionID NeedsHash (TreasuryWdrl _) = ⊤ NeedsHash Info = ⊤ +\end{code} +A governance action is an on-chain event that is triggered by a transaction, and there is a deadline after which +the governance action cannot be enacted. +\begin{itemize} +\item + \defn{Ratification}. An action is said to be \defn{ratified} when it gathers enough votes in its favor (through the rules and parameters that are detailed + below). +\item + \defn{Expiration}. An action that doesn't collect sufficient \AgdaField{yes} votes before its deadline is said to have \defn{expired}. +\item + \defn{Enactment}. An action that has been ratified is said to be \defn{enacted} once it has been activated on the network. +\end{itemize} + + +\subsection{Voting and ratification} +\label{sec:voting-and-ratification} +A governance action is an on-chain event that is triggered by a transaction. There is a deadline after which +the governance action cannot be enacted. +\begin{itemize} +\item + A governance action is said to be \defn{ratified} when it gathers enough votes in its favor + (through the rules and parameters that are detailed elsewhere [TODO: insert reference]). +\item + A governance action is said to have \defn{expired} if it does not collect sufficient \AgdaField{yes} votes before the deadline. +\item + An action that has been ratified is said to be \defn{enacted} once it has been activated on the network. +\end{itemize} + +The data type \AgdaDatatype{Vote} represents the different voting options: \AgdaInductiveConstructor{yes}, \AgdaInductiveConstructor{no}, or \AgdaInductiveConstructor{abstain}. +Each \AgdaField{vote} is recorded in a \AgdaRecord{GovVote} record along with the following meta-data: +\begin{itemize} +\item \FieldTyped{gid}{GovActionID} (governance action identifier), +\item \FieldTyped{role}{GovRole}, +\item \FieldTyped{credential}{Credential}, +\item \FieldTyped{anchor}{Maybe~Anchor}. +\end{itemize} +A \defn{governance action proposal} is recorded in a \AgdaRecord{GovProposal} record which includes fields for +a return address (\FieldTyped{returnAddr}{RwdAddr}), the proposed governance action (\FieldTyped{action}{GovAction}), +a hash of the previous governance action (\FieldTyped{prevAction}{NeedsHash action}), and an anchor. (See Figure~\ref{defs:governance-votes}.) +\begin{figure*}[h] +\begin{code} data Vote : Set where yes : Vote no : Vote @@ -131,18 +243,44 @@ record GovProposal : Set where prevAction : NeedsHash action anchor : Anchor \end{code} -\begin{code}[hide] +\caption{Governance action proposals and votes} +\label{defs:governance-votes} +\end{figure*} +\emph{Any Ada holder} can submit a governance action to the chain. +They must provide a deposit of \AgdaBound{govDeposit} Lovelace, which will be returned when the action is finalized (whether it is \defn{ratified} or has \defn{expired}). +The deposit amount will be added to the \defn{deposit pot}, similar to stake key deposits. It will also be counted towards the stake of the reward address it will be paid +back to, to not reduce the submitter's voting power to vote on their own (and competing) actions. +\\[4pt] +\textbf{Remarks}. +\begin{enumerate} +\item A motion of no-confidence is an extreme measure that enables Ada holders to revoke the power that has been granted to the current constitutional committee. +\item A \emph{single} governance action might contain \emph{multiple} protocol parameter updates. Many parameters are inter-connected and might require moving in lockstep. +\end{enumerate} +\begin{code}[hide] instance _ = +-0-commutativeMonoid 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) ∷ []) \end{code} -\caption{Governance actions and votes} -\label{defs:governance} -\end{figure*} +See Section~\ref{sec:ratification} for more on the ratification process. + +\subsection{Enactment} +\label{sec:enactment} +\defn{Enactment} of a governance action is carried out as an \defn{enact transition} +which requires an \defn{enact environment} (\AgdaSymbol{:}\,\AgdaRecord{EnactEnv}), an \defn{enact state} +(\AgdaSymbol{:}\,\AgdaRecord{EnactState}) representing the existing state (prior to enactment), the voted on +governance action (that achieved enough votes to enact), and the state that results from enacting the given +governance action (\AgdaSymbol{:}\,\AgdaRecord{EnactState}). (See Figure~\ref{fig:enactment-types}.) + +The \AgdaRecord{EnactEnv} record type represents the environment for enacting a governance action. %; the type has only one field, \FieldTyped{gid}{GovActionID}. + +The \AgdaRecord{EnactState} record type represents the state for enacting a governance action. +It contains various fields such as \AgdaField{cc} (constitutional committee), \AgdaField{constitution}, +\AgdaField{pv} (protocol version), \AgdaField{pparams} (protocol parameters), \AgdaField{withdrawals} +(withdrawals from treasury), and \AgdaField{treasury} (treasury balance). \begin{figure*}[h] \begin{code} HashProtected : Set → Set @@ -160,6 +298,9 @@ record EnactState : Set where withdrawals : Credential ⇀ Coin treasury : Coin \end{code} +\caption{Enactment types} +\label{fig:enactment-types} +\end{figure*} \begin{code}[hide] open EnactState @@ -178,25 +319,24 @@ private variable instance _ = +-0-monoid - -data -\end{code} -\begin{code} - _⊢_⇀⦇_,ENACT⦈_ : EnactEnv → EnactState → GovAction → EnactState → Set \end{code} -\begin{code}[hide] -data _⊢_⇀⦇_,ENACT⦈_ where -\end{code} -\begin{code} - Enact-NoConf : ⟦ gid ⟧ᵉ ⊢ s ⇀⦇ NoConfidence ,ENACT⦈ record s { cc = nothing , gid } - Enact-NewComm : ⟦ gid ⟧ᵉ ⊢ s ⇀⦇ NewCommittee new rem q ,ENACT⦈ let +The data type \verb!_⊢_⇀⦇_,ENACT⦈_! defines the transition relation for enacting a governance action. +It represents how the \AgdaBound{EnactState} changes when a specific governance action is enacted. +(See Figure~\ref{fig:enact-transition-system}.) + +\begin{figure*}[h] +{\small +\begin{code} +data _⊢_⇀⦇_,ENACT⦈_ : EnactEnv → EnactState → GovAction → EnactState → Set where + Enact-NoConf : ⟦ gid ⟧ᵉ ⊢ s ⇀⦇ NoConfidence ,ENACT⦈ record s { cc = nothing , gid } + Enact-NewComm : ⟦ gid ⟧ᵉ ⊢ s ⇀⦇ NewCommittee new rem q ,ENACT⦈ let old = maybe proj₁ ∅ᵐ (proj₁ (EnactState.cc s)) in record s { cc = just ((new ∪ᵐˡ old) ∣ rem ᶜ , q) , gid } - Enact-NewConst : ⟦ gid ⟧ᵉ ⊢ s ⇀⦇ NewConstitution dh ,ENACT⦈ record s { constitution = dh , gid } - Enact-HF : ⟦ gid ⟧ᵉ ⊢ s ⇀⦇ TriggerHF v ,ENACT⦈ record s { pv = v , gid } - Enact-PParams : - ⟦ gid ⟧ᵉ ⊢ s ⇀⦇ ChangePParams up h ,ENACT⦈ record s { pparams = applyUpdate (proj₁ (s .pparams)) up , gid } + Enact-NewConst : ⟦ gid ⟧ᵉ ⊢ s ⇀⦇ NewConstitution dh ,ENACT⦈ record s { constitution = dh , gid } + Enact-HF : ⟦ gid ⟧ᵉ ⊢ s ⇀⦇ TriggerHF v ,ENACT⦈ record s { pv = v , gid } + Enact-PParams : ⟦ gid ⟧ᵉ ⊢ s ⇀⦇ ChangePParams up h ,ENACT⦈ + record s { pparams = applyUpdate (proj₁ (s .pparams)) up , gid } Enact-Wdrl : let newWdrls = Σᵐᵛ[ x ← wdrl ᶠᵐ ] x in newWdrls ≤ s .treasury @@ -207,4 +347,6 @@ data _⊢_⇀⦇_,ENACT⦈_ where Enact-Info : ⟦ gid ⟧ᵉ ⊢ s ⇀⦇ Info ,ENACT⦈ s \end{code} \caption{ENACT transition system} +\label{fig:enact-transition-system} +} \end{figure*} diff --git a/src/Ledger/PDF.lagda b/src/Ledger/PDF.lagda index e235d0738..637d526e9 100644 --- a/src/Ledger/PDF.lagda +++ b/src/Ledger/PDF.lagda @@ -3,6 +3,7 @@ \setsansfont{XITSMath-Regular.otf} \usepackage{newunicodechar} +\usepackage{longtable} \newunicodechar{ᵇ}{\ensuremath{^b}} \newunicodechar{ᶜ}{\ensuremath{^c}} \newunicodechar{ᵈ}{\ensuremath{^d}} @@ -65,12 +66,15 @@ \newtheorem{property}{Property}[section] -%% -- DEFINITIONS ---------------------------------------------------- +%% -- DEFINITIONS ----------------------------------------------------------- %% Set the desired typeface of defined terms here and, at the %% first occurrence of such a term, enclose it in `\defn{...}`. \newcommand{\defn}[1]{\textit{#1}} % defined terms are typeset in italics %% \newcommand{\defn}[1]{\textbf{#1}} % defined terms are typeset in bold +%% -- For typesetting an Agda field name along with its type ----------------- +\newcommand{\FieldTyped}[2]{\AgdaField{#1}\,\AgdaSymbol{:}\,\AgdaDatatype{#2}} + \begin{document} \tableofcontents