Change the way SPO votes are counted (Fix)

CHANGELOG.md

@@ -32,6 +32,7 @@
 - Only consider matching GAs in `hasParent`
 - Fix `ccMinSize` check not properly accounting for double delegations
 - Check `proposal ≡ nothing` if action not `ChangePParams` or `TreasuryWdrl`
+- Implement proper vote counting for SPOs
 
 ### V0.9
 

src/Ledger/Conway/Conformance/Epoch.agda

@@ -185,7 +185,8 @@ data _⊢_⇀⦇_,EPOCH⦈_ : ⊤ → EpochState → Epoch → EpochState → Ty
     record { currentEpoch = e
            ; stakeDistrs = mkStakeDistrs  (Snapshots.mark ss') govSt'
                                           (utxoSt' .deposits) (voteDelegs dState)
-           ; treasury = acnt .treasury ; GState gState }
+           ; treasury = acnt .treasury ; GState gState
+           ; pools = pState .pools ; delegatees = dState .voteDelegs }
         ⊢ ⟦ es , ∅ , false ⟧ʳ ⇀⦇ govSt' ,RATIFY⦈ fut'
       → ls ⊢ ss ⇀⦇ tt ,SNAP⦈ ss'
     ────────────────────────────────

src/Ledger/Conway/Conformance/Ratify.agda

@@ -11,6 +11,7 @@ open import Ledger.Transaction hiding (Vote)
 
 module Ledger.Conway.Conformance.Ratify (txs : _) (open TransactionStructure txs) where
 
+open import Ledger.Certs govStructure
 open import Ledger.Enact govStructure
 open import Ledger.GovernanceActions govStructure using (Vote)
 
@@ -103,6 +104,8 @@ record RatifyEnv : Type where
     dreps         : Credential ⇀ Epoch
     ccHotKeys     : Credential ⇀ Maybe Credential
     treasury      : Coin
+    pools         : KeyHash ⇀ PoolParams
+    delegatees    : Credential ⇀ VDeleg
 
 record RatifyState : Type where
 
@@ -152,6 +155,18 @@ actualVotes Γ pparams cc ga votes
       (true , just (just c'))  → just c'
       _                        → nothing -- expired, no hot key or resigned
 
+  SPODefaultVote : GovAction → VDeleg → Vote
+  SPODefaultVote ga (credVoter SPO (KeyHashObj kh)) = case lookupᵐ? pools kh of
+      λ where
+        nothing → Vote.no
+        (just  p) → case lookupᵐ? delegatees (PoolParams.rewardAddr p) , ga of
+               λ where
+               (just noConfidenceRep , NoConfidence)  → Vote.yes
+               (_ , TriggerHF _)                      → Vote.no
+               (just abstainRep , _)                  → Vote.abstain
+               _                                      → Vote.no
+  SPODefaultVote _ _ = Vote.no
+
   actualCCVote : Credential → Epoch → Vote
   actualCCVote c e = case getCCHotCred (c , e) of
 
@@ -180,8 +195,7 @@ actualVotes Γ pparams cc ga votes
                    ∪ˡ  constMap (mapˢ (credVoter DRep) activeDReps) Vote.no
 
   actualSPOVotes : GovAction → VDeleg ⇀ Vote
-  actualSPOVotes (TriggerHF _)  = roleVotes SPO ∪ˡ constMap spos Vote.no
-  actualSPOVotes _              = roleVotes SPO ∪ˡ constMap spos Vote.abstain
+  actualSPOVotes a = roleVotes SPO ∪ˡ mapFromFun (SPODefaultVote a) spos
 
 open RatifyEnv using (stakeDistrs)
 

src/Ledger/Conway/Foreign/HSLedger/Ratify.agda

@@ -2,6 +2,7 @@ module Ledger.Conway.Foreign.HSLedger.Ratify where
 
 open import Ledger.Conway.Foreign.HSLedger.Address
 open import Ledger.Conway.Foreign.HSLedger.BaseTypes
+open import Ledger.Conway.Foreign.HSLedger.Certs
 open import Ledger.Conway.Foreign.HSLedger.Enact
 open import Ledger.Conway.Foreign.HSLedger.Gov
 

src/Ledger/Epoch.lagda

@@ -261,7 +261,8 @@ its results by carrying out each of the following tasks.
     record { currentEpoch = e
            ; stakeDistrs = mkStakeDistrs  (Snapshots.mark ss') govSt'
                                           (utxoSt' .deposits) (voteDelegs dState)
-           ; treasury = acnt .treasury ; GState gState }
+           ; treasury = acnt .treasury ; GState gState
+           ; pools = pState .pools ; delegatees = dState .voteDelegs }
         ⊢ ⟦ es , ∅ , false ⟧ʳ ⇀⦇ govSt' ,RATIFY⦈ fut'
       → ls ⊢ ss ⇀⦇ tt ,SNAP⦈ ss'
     ────────────────────────────────

src/Ledger/PDF/ConwayBootstrap.lagda

@@ -1,4 +1,5 @@
 \section{Bootstrapping the Governance System}
+\label{sec:conway-bootstrap}
 
 \begin{code}[hide]
 {-# OPTIONS --safe #-}
@@ -16,6 +17,7 @@ be made to the ledger described in this document.
       a \SPO vote on a \TriggerHF action or any vote on an \Info
       action will be rejected.
 \item \Qfour, \Pfive and \Qfivee are set to $0$.
+\item An SPO that does not vote is assumed to have voted \abstain.
 \end{itemize}
 
 This allows for a governance mechanism similar to the old, Shelley-era

src/Ledger/Ratify.lagda

@@ -13,6 +13,7 @@ open import Ledger.Transaction hiding (Vote)
 
 module Ledger.Ratify (txs : _) (open TransactionStructure txs) where
 
+open import Ledger.Certs govStructure
 open import Ledger.Enact govStructure
 open import Ledger.GovernanceActions govStructure using (Vote)
 
@@ -202,6 +203,8 @@ record RatifyEnv : Type where
     dreps         : Credential ⇀ Epoch
     ccHotKeys     : Credential ⇀ Maybe Credential
     treasury      : Coin
+    pools         : KeyHash ⇀ PoolParams
+    delegatees    : Credential ⇀ VDeleg
 
 record RatifyState : Type where
 \end{code}
@@ -241,11 +244,11 @@ defines some types and functions used in the RATIFY transition
 system. \CCData is simply an alias to define some functions more
 easily.
 
+\begin{figure*}[h!]
+\begin{AgdaMultiCode}
 \begin{code}[hide]
 open StakeDistrs
 \end{code}
-\begin{figure*}[h!]
-\begin{AgdaMultiCode}
 \begin{code}
 actualVotes  : RatifyEnv → PParams → CCData → GovAction
              → (GovRole × Credential ⇀ Vote) → (VDeleg ⇀ Vote)
@@ -263,39 +266,61 @@ actualVotes Γ pparams cc ga votes
   roleVotes r = mapKeys (uncurry credVoter) (filter (λ (x , _) → r ≡ proj₁ x) votes)
 
   activeDReps = dom (filter (λ (_ , e) → currentEpoch ≤ e) dreps)
-  spos = filterˢ IsSPO (dom (stakeDistr stakeDistrs))
+  spos  = filterˢ IsSPO (dom (stakeDistr stakeDistrs))
+\end{code}
+\begin{code}
 
   getCCHotCred : Credential × Epoch → Maybe Credential
   getCCHotCred (c , e) = case ¿ currentEpoch ≤ e ¿ᵇ , lookupᵐ? ccHotKeys c of
 \end{code}
 \begin{code}[hide]
-    λ where
+      λ where
+\end{code}
+\begin{code}
+        (true , just (just c'))  → just c'
+        _                        → nothing -- expired, no hot key or resigned
+
+  SPODefaultVote : GovAction → VDeleg → Vote
+  SPODefaultVote ga (credVoter SPO (KeyHashObj kh)) = case lookupᵐ? pools kh of
+\end{code}
+\begin{code}[hide]
+      λ where
 \end{code}
 \begin{code}
-      (true , just (just c'))  → just c'
-      _                        → nothing -- expired, no hot key or resigned
+        nothing → Vote.no
+        (just  p) → case lookupᵐ? delegatees (PoolParams.rewardAddr p) , ga of
+\end{code}
+\begin{code}[hide]
+               λ where
+\end{code}
+\begin{code}
+               (_                     , TriggerHF _   )  → Vote.no
+               (just noConfidenceRep  , NoConfidence  )  → Vote.yes
+               (just abstainRep       , _             )  → Vote.abstain
+               _                                         → Vote.no
+  SPODefaultVote _ _ = Vote.no
 
   actualCCVote : Credential → Epoch → Vote
   actualCCVote c e = case getCCHotCred (c , e) of
 \end{code}
 \begin{code}[hide]
-    λ where
+      λ where
 \end{code}
 \begin{code}
-      (just c')  → maybe id Vote.no (lookupᵐ? votes (CC , c'))
-      _          → Vote.abstain
+        (just c')  → maybe id Vote.no (lookupᵐ? votes (CC , c'))
+        _          → Vote.abstain
 
   actualCCVotes : Credential ⇀ Vote
   actualCCVotes = case cc of
 \end{code}
 \begin{code}[hide]
-    λ where
+      λ where
 \end{code}
 \begin{code}
-      nothing         → ∅
-      (just (m , q))  → if ccMinSize ≤ lengthˢ (mapFromPartialFun getCCHotCred (m ˢ))
-                          then mapWithKey actualCCVote m
-                          else constMap (dom m) Vote.no
+        nothing         →  ∅
+        (just (m , q))  →  if ccMinSize ≤ lengthˢ (mapFromPartialFun getCCHotCred (m ˢ))
+                           then mapWithKey actualCCVote m
+                           else constMap (dom m) Vote.no
 
   actualPDRepVotes : GovAction → VDeleg ⇀ Vote
   actualPDRepVotes NoConfidence
@@ -307,8 +332,7 @@ actualVotes Γ pparams cc ga votes
                    ∪ˡ  constMap (mapˢ (credVoter DRep) activeDReps) Vote.no
 
   actualSPOVotes : GovAction → VDeleg ⇀ Vote
-  actualSPOVotes (TriggerHF _)  = roleVotes SPO ∪ˡ constMap spos Vote.no
-  actualSPOVotes _              = roleVotes SPO ∪ˡ constMap spos Vote.abstain
+  actualSPOVotes a = roleVotes SPO ∪ˡ mapFromFun (SPODefaultVote a) spos
 \end{code}
 \end{AgdaMultiCode}
 \caption{Vote counting}
@@ -345,6 +369,29 @@ DReps, regular DReps and SPOs.
   with the default depending on the action.
 \end{itemize}
 
+Let us discuss the last item above---the way SPO votes are counted---as the ledger
+specification's handling of this has evolved in response to community feedback.
+Previously, if an SPO did not vote, then it would be counted as having voted
+\abstain by default.  Members of the SPO community found this behavior counterintuitive
+and requested that non-voters be assigned a \no vote by default, with the caveat that
+an SPO could change its default setting by delegating its reward account credential
+to an \texttt{AlwaysNoConfidence} DRep or an \texttt{AlwaysAbstain} DRep.
+(This change applies only after the bootstrap period; during the bootstrap period
+the logic is unchanged; see Appendix Section~\ref{sec:conway-bootstrap}.)
+To be precise, the agreed upon specification is the following: an SPO that did
+not vote is assumed to have vote \no, except under the following circumstances:
+\begin{itemize}
+\item if the SPO has delegated its reward credential to an \texttt{AlwaysNoConfidence}
+DRep, then their default vote is \yes for \NoConfidence proposals and \no for other proposals;
+\item if the SPO has delegated its reward credential to an \texttt{AlwaysAbstain} DRep,
+then its default vote is \abstain for all proposals.
+\end{itemize}
+It is important to note that the credential that can now be used to set a default
+voting behavior is the credential used to withdraw staking rewards, which is not
+(in general) the same as the credential used for voting.
+%% And as a second layer, this means that if that credential is a script, it may need
+%% to have explicit logic written to be able to set a default at all.
+
 \begin{figure*}[h!]
 \begin{code}[hide]
 open RatifyEnv using (stakeDistrs)