diff --git a/src/Ledger/Foreign/HSLedger.agda b/src/Ledger/Foreign/HSLedger.agda index 7cc5fe54..5aa0e604 100644 --- a/src/Ledger/Foreign/HSLedger.agda +++ b/src/Ledger/Foreign/HSLedger.agda @@ -147,12 +147,10 @@ HsGovParams : GovParams HsGovParams = record { Implementation ; ppUpd = let open PParamsDiff in λ where - .UpdateT → ⊤ - .updateGroups → λ _ → ∅ - .applyUpdate → λ p _ → p - .ppdWellFormed → λ _ → false - .ppdWellFormed⇒hasGroup → λ () - .ppdWellFormed⇒WF → λ _ _ x → x + .UpdateT → ⊤ + .updateGroups → λ _ → ∅ + .applyUpdate → λ p _ → p + .ppWF? → ⁇ yes (λ _ h → h) ; ppHashingScheme = it } diff --git a/src/Ledger/Gov.lagda b/src/Ledger/Gov.lagda index 7371772d..a2801c09 100644 --- a/src/Ledger/Gov.lagda +++ b/src/Ledger/Gov.lagda @@ -217,7 +217,7 @@ data _⊢_⇀⦇_,GOV'⦈_ where ; policy = p ; deposit = d ; prevAction = prev } s' = addAction s (govActionLifetime +ᵉ epoch) (txid , k) addr a prev in - ∙ actionWellFormed a ≡ true + ∙ actionWellFormed a ∙ d ≡ govActionDeposit ∙ (∃[ u ] a ≡ ChangePParams u ⊎ ∃[ w ] a ≡ TreasuryWdrl w → p ≡ ppolicy) ∙ (∀ {new rem q} → a ≡ NewCommittee new rem q diff --git a/src/Ledger/Gov/Properties.agda b/src/Ledger/Gov/Properties.agda index 7de10ddb..fafe908b 100644 --- a/src/Ledger/Gov/Properties.agda +++ b/src/Ledger/Gov/Properties.agda @@ -111,7 +111,9 @@ instance renaming (action to a; deposit to d; policy to p; returnAddr to addr; prevAction to prev) open PParams pparams hiding (a) - H = ¿ actionWellFormed a ≡ true + instance _ = actionWellFormed? + + H = ¿ actionWellFormed a × d ≡ govActionDeposit × validHFAction prop s enactState × (∃[ u ] a ≡ ChangePParams u ⊎ ∃[ w ] a ≡ TreasuryWdrl w → p ≡ ppolicy) diff --git a/src/Ledger/GovernanceActions.lagda b/src/Ledger/GovernanceActions.lagda index 0fdc3f7d..0083cb14 100644 --- a/src/Ledger/GovernanceActions.lagda +++ b/src/Ledger/GovernanceActions.lagda @@ -9,9 +9,10 @@ We introduce three distinct bodies that have specific functions in the new gover \item the stake pool operators (henceforth called \SPOs) -In the following figure, \DocHash is equal to any other 32-bit hash -type (such as \ScriptHash). We use a different name to avoid -confusion. +In the following figure, \DocHash is abstract but in the +implementation it will be instantiated with a 32-bit hash type (like +e.g. \ScriptHash). We keep it separate because it is used for a +different purpose. \end{enumerate} \begin{code}[hide] @@ -57,9 +58,19 @@ data GovAction : Set where TreasuryWdrl : (RwdAddr ⇀ Coin) → GovAction Info : GovAction -actionWellFormed : GovAction → Bool +actionWellFormed : GovAction → Set actionWellFormed (ChangePParams x) = ppdWellFormed x -actionWellFormed _ = true +actionWellFormed _ = ⊤ +\end{code} +\begin{code}[hide] +actionWellFormed? : ∀ {a} → actionWellFormed a ⁇ +actionWellFormed? {NoConfidence} = Dec-⊤ +actionWellFormed? {NewCommittee _ _ _} = Dec-⊤ +actionWellFormed? {NewConstitution _ _} = Dec-⊤ +actionWellFormed? {TriggerHF _} = Dec-⊤ +actionWellFormed? {ChangePParams x} = Dec-× +actionWellFormed? {TreasuryWdrl _} = Dec-⊤ +actionWellFormed? {Info} = Dec-⊤ \end{code} \caption{Governance actions} \label{defs:governance} diff --git a/src/Ledger/PParams.lagda b/src/Ledger/PParams.lagda index 526a2e32..d87fbba3 100644 --- a/src/Ledger/PParams.lagda +++ b/src/Ledger/PParams.lagda @@ -104,7 +104,6 @@ paramsWellFormed pp = 0 ∉ fromList ( maxBlockSize ∷ maxTxSize ∷ maxHeaderSize ∷ maxValSize ∷ minUTxOValue ∷ poolDeposit ∷ collateralPercentage ∷ ccMaxTermLength ∷ govActionLifetime ∷ govActionDeposit ∷ drepDeposit ∷ [] ) - × ℕtoEpoch govActionLifetime ≤ drepActivity where open PParams pp \end{code} \end{AgdaMultiCode} @@ -168,6 +167,8 @@ instance ((quote PoolThresholds , DecEq-PoolThresholds) ∷ []) unquoteDecl DecEq-PParams = derive-DecEq ((quote PParams , DecEq-PParams) ∷ []) + unquoteDecl DecEq-PParamGroup = derive-DecEq + ((quote PParamGroup , DecEq-PParamGroup) ∷ []) instance pvCanFollow? : ∀ {pv} {pv'} → Dec (pvCanFollow pv pv') @@ -177,17 +178,41 @@ instance ... | no ¬p | yes refl = yes canFollowMinor ... | yes refl | no ¬p = yes canFollowMajor ... | yes refl | yes p = ⊥-elim $ m+1+n≢m m $ ×-≡,≡←≡ p .proj₁ +\end{code} + +Finally, to update parameters we introduce an abstract type. An update +can be applied and it has a set of groups associated with it. An +update is well formed if it has at least one group (i.e. if it updates +something) and if it preserves well-formedness. +\begin{figure*}[h!] +\begin{AgdaMultiCode} +\begin{code}[hide] record PParamsDiff : Set₁ where - field UpdateT : Set - updateGroups : UpdateT → ℙ PParamGroup - applyUpdate : PParams → UpdateT → PParams - ppdWellFormed : UpdateT → Bool - ppdWellFormed⇒hasGroup : ∀ {u} → ppdWellFormed u ≡ true → updateGroups u ≢ ∅ - ppdWellFormed⇒WF : ∀ {u} → ppdWellFormed u ≡ true → ∀ pp - → paramsWellFormed pp - → paramsWellFormed (applyUpdate pp u) + field +\end{code} +\emph{Abstract types \& functions} +\begin{code} + UpdateT : Set + applyUpdate : PParams → UpdateT → PParams + updateGroups : UpdateT → ℙ PParamGroup +\end{code} +\begin{code}[hide] + ⦃ ppWF? ⦄ : ∀ {u} → (∀ pp → paramsWellFormed pp → paramsWellFormed (applyUpdate pp u)) ⁇ +\end{code} +\emph{Well-formedness condition} +\begin{code} + + ppdWellFormed : UpdateT → Set + ppdWellFormed u = updateGroups u ≢ ∅ + × ∀ pp → paramsWellFormed pp → paramsWellFormed (applyUpdate pp u) +\end{code} +\end{AgdaMultiCode} +\caption{Abstract type for parameter updates} +\label{fig:pp-update-type} +\end{figure*} +\begin{code}[hide] record GovParams : Set₁ where field ppUpd : PParamsDiff open PParamsDiff ppUpd renaming (UpdateT to PParamsUpdate) public diff --git a/src/Ledger/Ratify.lagda b/src/Ledger/Ratify.lagda index 959d1112..204f6369 100644 --- a/src/Ledger/Ratify.lagda +++ b/src/Ledger/Ratify.lagda @@ -436,7 +436,12 @@ functions (together with some helpers) that are used in the rules of RATIFY. \begin{itemize} - \item \getStakeDist computes the stake distribution based on the given governance role and the corresponding delegations; + \item \getStakeDist computes the stake distribution based on the + given governance role and the corresponding delegations. Note that + every constitutional committe member has a stake of 1, giving them + equal voting power. However, just as with other delegation, multiple + CC members can delegate to the same hot key, giving that hot key + the power of those multiple votes with a single actual vote. \item \acceptedStakeRatio is the ratio of accepted stake. It is computed as the ratio of \yes votes over the votes that didn't @@ -508,7 +513,14 @@ abstract Figure~\ref{fig:defs:ratify-defs-ii} defines functions that deal with delays. A given action can either be delayed if the action contained in \EnactState isn't the one the given action is building on top -of, or if a previous action was a \delayingAction. +of, which is checked by \verifyPrev, or if a previous action was a +\delayingAction. Note that \delayingAction affects the future: whenever a +\delayingAction is accepted all future actions are delayed. \delayed then +expresses the condition whether an action is delayed. This happens either +because the previous action doesn't match the current one, or because the +previous action was a delaying one. This information is passed in as an +argument. + \begin{code}[hide] private variable Γ : RatifyEnv