From e0e084acbffb9b81ea6d93a95fe32d0d96bd13cd Mon Sep 17 00:00:00 2001 From: Andre Knispel Date: Thu, 29 Jun 2023 17:11:33 +0200 Subject: [PATCH] Add governance thresholds (#134) --- src/Ledger/Foreign/HSLedger.agda | 7 +++- src/Ledger/GovernanceActions.lagda | 49 ++++++++++++++++++++--- src/Ledger/PParams.lagda | 13 ++++++- src/Ledger/Ratify.lagda | 62 +++++++++++++++--------------- 4 files changed, 92 insertions(+), 39 deletions(-) diff --git a/src/Ledger/Foreign/HSLedger.agda b/src/Ledger/Foreign/HSLedger.agda index 567e31117..af6db4ae0 100644 --- a/src/Ledger/Foreign/HSLedger.agda +++ b/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 diff --git a/src/Ledger/GovernanceActions.lagda b/src/Ledger/GovernanceActions.lagda index 00b1bda2d..286c69711 100644 --- a/src/Ledger/GovernanceActions.lagda +++ b/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 diff --git a/src/Ledger/PParams.lagda b/src/Ledger/PParams.lagda index b3ffb87bc..dd6d92f05 100644 --- a/src/Ledger/PParams.lagda +++ b/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 diff --git a/src/Ledger/Ratify.lagda b/src/Ledger/Ratify.lagda index a141fa056..04e3854b9 100644 --- a/src/Ledger/Ratify.lagda +++ b/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