Change the way SPO votes are counted (#594)

* Change the way SPO votes are counted

This closes issue #578.

* recorded work in CHANGELOG WIP section

* fix SPO vote count function

* fix TeX error so Conway pdf compiles with Fig 35 looking decent

* change SPO votes calculation to agree with Haskell implementation

* Stop passing in `CertState` to `RatifyEnv`

* Update SPO vote calculation conformance

---------

Co-authored-by: Lucsanszky <[email protected]>

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

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

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

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

src/Ledger/Conway/Conformance/Ratify.lagda

@@ -202,6 +202,9 @@ record RatifyEnv : Type where
     dreps         : Credential ⇀ Epoch
     ccHotKeys     : Credential ⇀ Maybe Credential
     treasury      : Coin
+    pools         : KeyHash ⇀ PoolParams
+    delegatees    : Credential ⇀ VDeleg
+    stakeDelegs   : Credential ⇀ KeyHash
 
 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)
@@ -255,8 +258,7 @@ actualVotes Γ pparams cc ga votes
   where
 \end{code}
 \begin{code}[hide]
-  open RatifyEnv Γ
-  open PParams pparams
+  open RatifyEnv Γ; open PParams pparams
 \end{code}
 \begin{code}
   roleVotes : GovRole → VDeleg ⇀ Vote
@@ -272,18 +274,35 @@ actualVotes Γ pparams cc ga votes
     λ where
 \end{code}
 \begin{code}
-      (true , just (just c'))  → just c'
-      _                        → nothing -- expired, no hot key or resigned
-
-  actualCCVote : Credential → Epoch → Vote
-  actualCCVote c e = case getCCHotCred (c , e) of
+    (true , just (just c'))  → just c'
+    _                        → nothing -- expired, no hot key or resigned
 \end{code}
 \begin{code}[hide]
-    λ where
+  getPoolParams : Credential → Maybe PoolParams
+  getPoolParams c = case lookupᵐ? stakeDelegs c of λ where  nothing → nothing
+                                                            (just kh)  → lookupᵐ? pools kh
 \end{code}
 \begin{code}
-      (just c')  → maybe id Vote.no (lookupᵐ? votes (CC , c'))
-      _          → Vote.abstain
+
+  SPODefaultVote : GovAction → VDeleg → Vote
+  SPODefaultVote (TriggerHF _) _ = Vote.no
+  SPODefaultVote NoConfidence (credVoter SPO c) = case getPoolParams c of λ where
+    nothing → Vote.no
+    (just p) → case lookupᵐ? delegatees (PoolParams.rewardAddr p) of λ where
+      (just noConfidenceRep)  → Vote.yes
+      (just abstainRep)       → Vote.abstain
+      _                       → Vote.no
+  SPODefaultVote _ (credVoter SPO c) = case getPoolParams c of λ where
+    nothing → Vote.no
+    (just p) → case lookupᵐ? delegatees (PoolParams.rewardAddr p) of λ where
+      (just abstainRep)  → Vote.abstain
+      _                  → Vote.no
+  SPODefaultVote _ _ = Vote.no
+
+  actualCCVote : Credential → Epoch → Vote
+  actualCCVote c e = case getCCHotCred (c , e) of λ where
+    (just c')  → maybe id Vote.no (lookupᵐ? votes (CC , c'))
+    _          → Vote.abstain
 
   actualCCVotes : Credential ⇀ Vote
   actualCCVotes = case cc of
@@ -292,10 +311,10 @@ actualVotes Γ pparams cc ga votes
     λ 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 +326,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 +363,26 @@ 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 they 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 their default setting by delegating their stake to an
+\texttt{AlwaysNoConfidence} DRep or an \texttt{AlwaysAbstain} DRep.
+More specifically, the agreed upon specification is the following:
+\begin{itemize}
+\item \textit{during the bootstrap period}: if an SPO didn't vote, then their vote is counted as \no;
+\item \textit{after the bootstrap period}: if an SPO didn't vote, then their vote is counted as \no
+except under the following circumstances:
+  \begin{itemize}
+  \item if the SPO has delegated 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 to an \texttt{AlwaysAbstain} DRep, then their default vote is
+    \abstain for all proposals.
+  \end{itemize}
+\end{itemize}
+
 \begin{figure*}[h!]
 \begin{code}[hide]
 open RatifyEnv using (stakeDistrs)

src/Ledger/Epoch.lagda

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

src/Ledger/Ratify.lagda

@@ -202,6 +202,9 @@ record RatifyEnv : Type where
     dreps         : Credential ⇀ Epoch
     ccHotKeys     : Credential ⇀ Maybe Credential
     treasury      : Coin
+    pools         : KeyHash ⇀ PoolParams
+    delegatees    : Credential ⇀ VDeleg
+    stakeDelegs   : Credential ⇀ KeyHash
 
 record RatifyState : Type where
 \end{code}
@@ -241,22 +244,21 @@ 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)
 actualVotes Γ pparams cc ga votes
-  =   mapKeys (credVoter CC) actualCCVotes  ∪ˡ actualPDRepVotes ga
-  ∪ˡ  actualDRepVotes                       ∪ˡ actualSPOVotes ga
+  =  mapKeys (credVoter CC) actualCCVotes ∪ˡ actualPDRepVotes ga
+  ∪ˡ actualDRepVotes ∪ˡ actualSPOVotes ga
   where
 \end{code}
 \begin{code}[hide]
-  open RatifyEnv Γ
-  open PParams pparams
+  open RatifyEnv Γ; open PParams pparams
 \end{code}
 \begin{code}
   roleVotes : GovRole → VDeleg ⇀ Vote
@@ -272,18 +274,35 @@ actualVotes Γ pparams cc ga votes
     λ where
 \end{code}
 \begin{code}
-      (true , just (just c'))  → just c'
-      _                        → nothing -- expired, no hot key or resigned
-
-  actualCCVote : Credential → Epoch → Vote
-  actualCCVote c e = case getCCHotCred (c , e) of
+    (true , just (just c'))  → just c'
+    _                        → nothing -- expired, no hot key or resigned
 \end{code}
 \begin{code}[hide]
-    λ where
+  getPoolParams : Credential → Maybe PoolParams
+  getPoolParams c = case lookupᵐ? stakeDelegs c of λ where  nothing → nothing
+                                                            (just kh)  → lookupᵐ? pools kh
 \end{code}
 \begin{code}
-      (just c')  → maybe id Vote.no (lookupᵐ? votes (CC , c'))
-      _          → Vote.abstain
+
+  SPODefaultVote : GovAction → VDeleg → Vote
+  SPODefaultVote (TriggerHF _) _ = Vote.no
+  SPODefaultVote NoConfidence (credVoter SPO c) = case getPoolParams c of λ where
+    nothing → Vote.no
+    (just p) → case lookupᵐ? delegatees (PoolParams.rewardAddr p) of λ where
+      (just noConfidenceRep)  → Vote.yes
+      (just abstainRep)       → Vote.abstain
+      _                       → Vote.no
+  SPODefaultVote _ (credVoter SPO c) = case getPoolParams c of λ where
+    nothing → Vote.no
+    (just p) → case lookupᵐ? delegatees (PoolParams.rewardAddr p) of λ where
+      (just abstainRep)  → Vote.abstain
+      _                  → Vote.no
+  SPODefaultVote _ _ = Vote.no
+
+  actualCCVote : Credential → Epoch → Vote
+  actualCCVote c e = case getCCHotCred (c , e) of λ where
+    (just c')  → maybe id Vote.no (lookupᵐ? votes (CC , c'))
+    _          → Vote.abstain
 
   actualCCVotes : Credential ⇀ Vote
   actualCCVotes = case cc of
@@ -292,23 +311,22 @@ actualVotes Γ pparams cc ga votes
     λ 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
                       = ❴ abstainRep , Vote.abstain ❵ ∪ˡ ❴ noConfidenceRep , Vote.yes ❵
   actualPDRepVotes _  = ❴ abstainRep , Vote.abstain ❵ ∪ˡ ❴ noConfidenceRep , Vote.no ❵
 
   actualDRepVotes : VDeleg ⇀ Vote
-  actualDRepVotes  =   roleVotes DRep
-                   ∪ˡ  constMap (mapˢ (credVoter DRep) activeDReps) Vote.no
+  actualDRepVotes  =  roleVotes DRep
+                      ∪ˡ 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 +363,26 @@ 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 they 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 their default setting by delegating their stake to an
+\texttt{AlwaysNoConfidence} DRep or an \texttt{AlwaysAbstain} DRep.
+More specifically, the agreed upon specification is the following:
+\begin{itemize}
+\item \textit{during the bootstrap period}: if an SPO didn't vote, then their vote is counted as \no;
+\item \textit{after the bootstrap period}: if an SPO didn't vote, then their vote is counted as \no
+except under the following circumstances:
+  \begin{itemize}
+  \item if the SPO has delegated 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 to an \texttt{AlwaysAbstain} DRep, then their default vote is
+    \abstain for all proposals.
+  \end{itemize}
+\end{itemize}
+
 \begin{figure*}[h!]
 \begin{code}[hide]
 open RatifyEnv using (stakeDistrs)