Conway spec prose: GovernanceActions

This addresses the GovernanceActions, Voting, and Enactment items in issue #145

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*}

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