Add governance thresholds (#134)

src/Ledger/Foreign/HSLedger.agda

@@ -254,7 +254,12 @@ instance
         ; Emax              = Emax
         ; collateralPercent = 0
         ; pv                = coerce pv
-        ; votingThresholds  = ℚ.0ℚ , ℚ.0ℚ -- TODO: translate once this is implemented in F.PParams
+         -- TODO: translate these once they are implemented in F.PParams
+        ; drepThresholds    = record
+          { P1  = ℚ.½ ; P2a = ℚ.½ ; P2b = ℚ.½ ; P3  = ℚ.½ ; P4 = ℚ.½
+          ; P5a = ℚ.½ ; P5b = ℚ.½ ; P5c = ℚ.½ ; P5d = ℚ.½ ; P6 = ℚ.½}
+        ; poolThresholds    = record
+          { Q1 = ℚ.½ ; Q2a = ℚ.½ ; Q2b = ℚ.½ ; Q4 = ℚ.½ }
         ; minCCSize         = minCCSize
         ; ccTermLimit       = ccTermLimit
         ; govExpiration     = govExpiration

src/Ledger/GovernanceActions.lagda

@@ -9,10 +9,9 @@ open import Ledger.Epoch
 
 import Ledger.PParams as PP
 
-open import Data.Rational using (ℚ)
 open import Data.Nat using (_≤_)
-open import Data.Nat.Properties using (+-0-commutativeMonoid ; +-0-monoid)
-open import Data.These
+open import Data.Nat.Properties using (+-0-commutativeMonoid; +-0-monoid)
+open import Data.Rational using (ℚ; 0ℚ; 1ℚ)
 
 module Ledger.GovernanceActions (TxId Network DocHash : Set)
                                 (es : EpochStructure)
@@ -32,6 +31,8 @@ open isHashableSet ppHashable renaming (THash to PPHash)
 open import Tactic.Derive.DecEq
 open import MyDebugOptions
 
+2ℚ = 1ℚ Data.Rational.+ 1ℚ
+
 \end{code}
 \begin{figure*}[h]
 \begin{code}
@@ -53,8 +54,8 @@ record Anchor : Set where
          hash  : DocHash
 
 data GovAction : Set where
-  NoConfidence     :                                   GovAction
-  NewCommittee     : KeyHash ⇀ Epoch → ℙ KeyHash → ℚ → GovAction
+  NoConfidence     :                                    GovAction
+  NewCommittee     : KeyHash ⇀ Epoch → ℙ KeyHash → ℚ  → GovAction
   NewConstitution  : DocHash                          → GovAction
   TriggerHF        : ProtVer                          → GovAction
   ChangePParams    : UpdateT → PPHash                 → GovAction
@@ -65,6 +66,44 @@ actionWellFormed : GovAction → Bool
 actionWellFormed (ChangePParams x _) = ppdWellFormed x
 actionWellFormed _                   = true
 
+maximum : ℙ ℚ → ℚ
+maximum x = foldl Data.Rational._⊔_ 0ℚ (proj₁ $ finiteness x)
+
+module _ (pp : PParams) (ccThreshold' : Maybe ℚ) where
+  open PParams pp
+  open DrepThresholds drepThresholds
+  open PoolThresholds poolThresholds
+
+  -- Here, 2 can just be any number strictly greater than one. It just
+  -- means that a threshold can never be cleared, i.e. that the action
+  -- cannot be enacted.
+
+  private
+    ccThreshold : ℚ
+    ccThreshold = case ccThreshold' of λ where
+      (just x) → x
+      nothing  → 2ℚ
+
+    pparamThreshold : PParamGroup → ℚ
+    pparamThreshold NetworkGroup    = P5a
+    pparamThreshold EconomicGroup   = P5b
+    pparamThreshold TechnicalGroup  = P5c
+    pparamThreshold GovernanceGroup = P5d
+
+    P5 : UpdateT → ℚ
+    P5 ppu = maximum $ map pparamThreshold (updateGroups ppu)
+
+  threshold : GovAction → GovRole → ℚ
+  threshold NoConfidence         = λ { CC → 0ℚ          ; DRep → P1   ; SPO → Q1 }
+  threshold (NewCommittee _ _ _) = case ccThreshold' of λ where
+                        (just _) → λ { CC → 0ℚ          ; DRep → P2a  ; SPO → Q2a }
+                        nothing  → λ { CC → 0ℚ          ; DRep → P2b  ; SPO → Q2b }
+  threshold (NewConstitution _)  = λ { CC → ccThreshold ; DRep → P3   ; SPO → 0ℚ }
+  threshold (TriggerHF _)        = λ { CC → ccThreshold ; DRep → P4   ; SPO → Q4 }
+  threshold (ChangePParams x _)  = λ { CC → ccThreshold ; DRep → P5 x ; SPO → 0ℚ }
+  threshold (TreasuryWdrl _)     = λ { CC → ccThreshold ; DRep → P6   ; SPO → 0ℚ }
+  threshold Info                 = λ { CC → 2ℚ          ; DRep → 2ℚ   ; SPO → 2ℚ }
+
 NeedsHash : GovAction → Set
 NeedsHash NoConfidence         = GovActionID
 NeedsHash (NewCommittee _ _ _) = GovActionID

src/Ledger/PParams.lagda

@@ -31,6 +31,12 @@ record Acnt : Set where
 data PParamGroup : Set where
   NetworkGroup EconomicGroup TechnicalGroup GovernanceGroup : PParamGroup
 
+record DrepThresholds : Set where
+  field P1 P2a P2b P3 P4 P5a P5b P5c P5d P6 : ℚ
+
+record PoolThresholds : Set where
+  field Q1 Q2a Q2b Q4 : ℚ
+
 record PParams : Set where
   field -- Network group
         maxBlockSize      : ℕ
@@ -50,7 +56,8 @@ record PParams : Set where
         collateralPercent : ℕ
 
         -- Governance group
-        votingThresholds  : ℚ × ℚ
+        drepThresholds    : DrepThresholds
+        poolThresholds    : PoolThresholds
         minCCSize         : ℕ
         ccTermLimit       : ℕ
         govExpiration     : ℕ
@@ -69,7 +76,9 @@ paramsWellFormed pp = ⌊ ¬? (0 ∈? setFromList
 \end{figure*}
 \begin{code}[hide]
 instance
-  unquoteDecl DecEq-PParams = derive-DecEq ((quote PParams , DecEq-PParams) ∷ [])
+  unquoteDecl DecEq-DrepThresholds = derive-DecEq ((quote DrepThresholds , DecEq-DrepThresholds) ∷ [])
+  unquoteDecl DecEq-PoolThresholds = derive-DecEq ((quote PoolThresholds , DecEq-PoolThresholds) ∷ [])
+  unquoteDecl DecEq-PParams        = derive-DecEq ((quote PParams , DecEq-PParams) ∷ [])
 
 record PParamsDiff : Set₁ where
   field UpdateT : Set

src/Ledger/Ratify.lagda

@@ -14,6 +14,7 @@ open import Ledger.Tally TxId Network ADHash epochStructure ppUpd ppHashingSchem
 open import Ledger.PParams epochStructure
 
 import Data.Integer as Z
+import Data.Maybe
 import Data.Rational as R
 open import Data.Nat hiding (_≟_)
 open import Data.Nat.Properties hiding (_≟_)
@@ -164,6 +165,10 @@ votedAbstainHashes = votedHashes Vote.abstain
 participatingHashes : (VDeleg ⇀ Vote) → GovRole → ℙ VDeleg
 participatingHashes votes r = votedYesHashes votes r ∪ votedHashes Vote.no votes r
 
+isCC : VDeleg → Bool
+isCC (credVoter CC _) = true
+isCC _                = false
+
 isDRep : VDeleg → Bool
 isDRep (credVoter DRep _) = true
 isDRep (credVoter _ _)    = false
@@ -174,48 +179,43 @@ isSPO : VDeleg → Bool
 isSPO (credVoter SPO _) = true
 isSPO _                 = false
 
+isCCProp : specProperty λ x → isCC x ≡ true
+isCCProp = to-sp (λ x → isCC x ≟ true)
+
 isDRepProp : specProperty λ x → isDRep x ≡ true
 isDRepProp = to-sp (λ x → isDRep x ≟ true)
 
 isSPOProp : specProperty λ x → isSPO x ≡ true
 isSPOProp = to-sp (λ x → isSPO x ≟ true)
 
-getStakeDist : GovRole → StakeDistrs → VDeleg ⇀ Coin
-getStakeDist CC   _                              = ∅ᵐ
-getStakeDist DRep s@record { stakeDistr = dist } = filterᵐ (sp-∘ isDRepProp proj₁) dist
-getStakeDist SPO  s@record { stakeDistr = dist } = filterᵐ (sp-∘ isSPOProp proj₁) dist
-
-acceptedStake : GovRole → StakeDistrs → (VDeleg ⇀ Vote) → Coin
-acceptedStake r dists votes =
-  Σᵐᵛ[ x ← (getStakeDist r dists ∣ votedYesHashes votes r) ᶠᵐ ] x
+getStakeDist : GovRole → ℙ VDeleg → StakeDistrs → VDeleg ⇀ Coin
+getStakeDist CC   cc _                            = constMap (filterˢ isCCProp cc) 1
+getStakeDist DRep _  record { stakeDistr = dist } = filterᵐ (sp-∘ isDRepProp proj₁) dist
+getStakeDist SPO  _  record { stakeDistr = dist } = filterᵐ (sp-∘ isSPOProp proj₁) dist
 
-totalStake : GovRole → StakeDistrs → (VDeleg ⇀ Vote) → Coin
-totalStake r dists votes = Σᵐᵛ[ x ← getStakeDist r dists ∣ votedAbstainHashes votes r ᶜ ᶠᵐ ] x
+acceptedStake : GovRole → ℙ VDeleg → StakeDistrs → (VDeleg ⇀ Vote) → Coin
+acceptedStake r cc dists votes =
+  Σᵐᵛ[ x ← (getStakeDist r cc dists ∣ votedYesHashes votes r) ᶠᵐ ] x
 
-acceptedR : RatifyEnv → (VDeleg ⇀ Vote) → GovRole → R.ℚ → Set
-acceptedR Γ votes role t =
-  let open RatifyEnv Γ
-      redStakeDistr = restrictedDists coinThreshold rankThreshold stakeDistrs
-      totalStake = totalStake role redStakeDistr votes
-  in
-  case totalStake of λ where
-    0         → ⊥ -- if there's no stake, never accept
-    x@(suc _) → Z.+ acceptedStake role redStakeDistr votes R./ x R.> t
-
-ccThreshold : CCData → Maybe R.ℚ
-ccThreshold nothing         = nothing
-ccThreshold (just (cc , q)) = just q
+totalStake : GovRole → ℙ VDeleg → StakeDistrs → (VDeleg ⇀ Vote) → Coin
+totalStake r cc dists votes = Σᵐᵛ[ x ← getStakeDist r cc dists ∣ votedAbstainHashes votes r ᶜ ᶠᵐ ] x
 
 -- for now, consider a proposal as accepted if the CC and half of the SPOs and DReps agree
 accepted' : RatifyEnv → EnactState → GovActionState → Set
-accepted' Γ es@record { cc = cc , _ ; pparams = record { votingThresholds = drepThreshold , spoThreshold } , _ }
-         s@record  { votes = votes ; action = action } =
-  let open RatifyEnv Γ; votes = actualVotes Γ cc votes action in
-  acceptedR Γ votes SPO spoThreshold
-  ∧ acceptedR Γ votes DRep drepThreshold
-  ∧ (case lengthˢ (participatingHashes votes CC) , ccThreshold cc of λ where
-      (s@(suc _) , just q) → Z.+ lengthˢ (votedYesHashes votes CC) R./ s R.> q
-      _                    → ⊥)
+accepted' Γ es@record { cc = cc , _    ; pparams = pparams , _ }
+            s@record  { votes = votes' ; action = action } =
+  acceptedBy CC ∧ acceptedBy DRep ∧ acceptedBy SPO
+  where
+    open RatifyEnv Γ
+    votes = actualVotes Γ cc votes' action
+    cc' = dom (votes ˢ)
+    redStakeDistr = restrictedDists coinThreshold rankThreshold stakeDistrs
+
+    acceptedBy : GovRole → Set
+    acceptedBy role = let t = threshold pparams (Data.Maybe.map proj₂ cc) action role in
+      case totalStake role cc' redStakeDistr votes of λ where
+        0         → t ≡ R.0ℚ -- if there's no stake, accept only if the threshold is zero
+        x@(suc _) → Z.+ acceptedStake role cc' redStakeDistr votes R./ x R.≥ t
 
 expired : Epoch → GovActionState → Set
 expired current record { expiresIn = expiresIn } = expiresIn <ᵉ current