diff --git a/src/Ledger/Conway/Conformance/Equivalence.agda b/src/Ledger/Conway/Conformance/Equivalence.agda index 82f67888f9..6660f3f2f1 100644 --- a/src/Ledger/Conway/Conformance/Equivalence.agda +++ b/src/Ledger/Conway/Conformance/Equivalence.agda @@ -396,8 +396,8 @@ opaque → (record Γ { certState = certState' } , n) ⊢ s ⇀⦇ txgov ,GOVn⦈ s' castGOV deps (BS-base Id-nop) = BS-base Id-nop - castGOV {Γ} deps (BS-ind (C.GOV-Vote {voter = voter} (a , b , c)) rs) = - BS-ind (C.GOV-Vote (a , b , cast-isRegistered Γ deps voter c)) + castGOV {Γ} deps (BS-ind (C.GOV-Vote {voter = voter} (a , b , c , d)) rs) = + BS-ind (C.GOV-Vote (a , b , cast-isRegistered Γ deps voter c , d)) (castGOV deps rs) castGOV deps (BS-ind (C.GOV-Propose h) rs) = BS-ind (C.GOV-Propose h) diff --git a/src/Ledger/Conway/Conformance/Equivalence/Gov.agda b/src/Ledger/Conway/Conformance/Equivalence/Gov.agda index 905da32de6..558b45d007 100644 --- a/src/Ledger/Conway/Conformance/Equivalence/Gov.agda +++ b/src/Ledger/Conway/Conformance/Equivalence/Gov.agda @@ -16,12 +16,12 @@ open import Ledger.Conway.Conformance.Equivalence.Certs txs abs instance GovEnvToConf : L.Deposits × L.Deposits ⊢ L.GovEnv ⭆ C.GovEnv - GovEnvToConf .convⁱ deposits L.⟦ txid , epoch , pp , policy , enactState , certState ⟧ᵍ = - C.⟦ txid , epoch , pp , policy , enactState , deposits ⊢conv certState ⟧ᵍ + GovEnvToConf .convⁱ deposits L.⟦ txid , epoch , pp , policy , enactState , certState , stakeDelegs ⟧ᵍ = + C.⟦ txid , epoch , pp , policy , enactState , deposits ⊢conv certState , stakeDelegs ⟧ᵍ GovEnvFromConf : C.GovEnv ⭆ L.GovEnv - GovEnvFromConf .convⁱ _ C.⟦ txid , epoch , pp , policy , enactState , certState ⟧ᵍ = - L.⟦ txid , epoch , pp , policy , enactState , conv certState ⟧ᵍ + GovEnvFromConf .convⁱ _ C.⟦ txid , epoch , pp , policy , enactState , certState , stakeDelegs ⟧ᵍ = + L.⟦ txid , epoch , pp , policy , enactState , conv certState , stakeDelegs ⟧ᵍ opaque unfolding L.isRegistered C.isRegistered @@ -41,7 +41,7 @@ instance → L.Deposits × L.Deposits ⊢ (Γ , n) L.⊢ s ⇀⦇ votes ,GOV'⦈ s' ⭆ⁱ λ deposits _ → (deposits ⊢conv Γ , n) C.⊢ s ⇀⦇ votes ,GOV'⦈ s' - GOV'ToConf .convⁱ deposits (L.GOV-Vote (a , b , c)) = C.GOV-Vote (a , b , deposits ⊢conv c) + GOV'ToConf .convⁱ deposits (L.GOV-Vote (a , b , c , d)) = C.GOV-Vote (a , b , deposits ⊢conv c , d) GOV'ToConf .convⁱ deposits (L.GOV-Propose h) = C.GOV-Propose h GOVToConf : ∀ {Γ s votes s' n} @@ -53,7 +53,7 @@ instance GOV'FromConf : ∀ {Γ s votes s' n} → (Γ , n) C.⊢ s ⇀⦇ votes ,GOV'⦈ s' ⭆ (conv Γ , n) L.⊢ s ⇀⦇ votes ,GOV'⦈ s' - GOV'FromConf .convⁱ _ (C.GOV-Vote (a , b , c)) = L.GOV-Vote (a , b , conv c) + GOV'FromConf .convⁱ _ (C.GOV-Vote (a , b , c , d)) = L.GOV-Vote (a , b , conv c , d) GOV'FromConf .convⁱ _ (C.GOV-Propose h) = L.GOV-Propose h GOVFromConf : ∀ {Γ s votes s' n} diff --git a/src/Ledger/Conway/Conformance/Gov.agda b/src/Ledger/Conway/Conformance/Gov.agda index 82f5abee49..a95874086c 100644 --- a/src/Ledger/Conway/Conformance/Gov.agda +++ b/src/Ledger/Conway/Conformance/Gov.agda @@ -33,7 +33,7 @@ GovState : Type GovState = List (GovActionID × GovActionState) record GovEnv : Type where - constructor ⟦_,_,_,_,_,_⟧ᵍ + constructor ⟦_,_,_,_,_,_,_⟧ᵍ field txid : TxId @@ -42,6 +42,7 @@ record GovEnv : Type where ppolicy : Maybe ScriptHash enactState : EnactState certState : CertState + rewardCreds : ℙ Credential private variable Γ : GovEnv @@ -62,7 +63,7 @@ open PState opaque isRegistered : GovEnv → Voter → Type - isRegistered ⟦ _ , _ , _ , _ , _ , ⟦ _ , pState , gState ⟧ᶜˢ ⟧ᵍ (r , c) = case r of λ where + isRegistered ⟦ _ , _ , _ , _ , _ , ⟦ _ , pState , gState ⟧ᶜˢ , _ ⟧ᵍ (r , c) = case r of λ where CC → just c ∈ range (gState .ccHotKeys) DRep → c ∈ dom (gState .dreps) SPO → c ∈ mapˢ KeyHashObj (dom (pState .pools)) @@ -76,6 +77,7 @@ data _⊢_⇀⦇_,GOV'⦈_ : GovEnv × ℕ → GovState → GovVote ⊎ GovProp ∙ (aid , ast) ∈ fromList s ∙ canVote pparams (action ast) (proj₁ voter) ∙ isRegistered Γ voter + ∙ ¬ (expired epoch ast) ─────────────────────────────────────── (Γ , k) ⊢ s ⇀⦇ inj₁ vote ,GOV'⦈ L.addVote s aid voter v @@ -85,15 +87,13 @@ data _⊢_⇀⦇_,GOV'⦈_ : GovEnv × ℕ → GovState → GovVote ⊎ GovProp ; policy = p ; deposit = d ; prevAction = prev } s' = L.addAction s (govActionLifetime +ᵉ epoch) (txid , k) addr a prev in - ∙ actionWellFormed a + ∙ L.actionWellFormed a + ∙ L.actionValid rewardCreds p ppolicy epoch a ∙ d ≡ govActionDeposit - ∙ (∃[ u ] a ≡ ChangePParams u ⊎ ∃[ w ] a ≡ TreasuryWdrl w → p ≡ ppolicy) - ∙ (¬ (∃[ u ] a ≡ ChangePParams u ⊎ ∃[ w ] a ≡ TreasuryWdrl w) → p ≡ nothing) - ∙ (∀ {new rem q} → a ≡ UpdateCommittee new rem q - → ∀[ e ∈ range new ] epoch < e × dom new ∩ rem ≡ᵉ ∅) ∙ L.validHFAction prop s enactState ∙ L.hasParent enactState s a prev ∙ addr .RwdAddr.net ≡ NetworkId + ∙ addr .RwdAddr.stake ∈ rewardCreds ─────────────────────────────────────── (Γ , k) ⊢ s ⇀⦇ inj₂ prop ,GOV'⦈ s' diff --git a/src/Ledger/Conway/Conformance/Gov/Properties.agda b/src/Ledger/Conway/Conformance/Gov/Properties.agda index 094c04242d..ff856521a7 100644 --- a/src/Ledger/Conway/Conformance/Gov/Properties.agda +++ b/src/Ledger/Conway/Conformance/Gov/Properties.agda @@ -36,10 +36,6 @@ open GovActionState open Inverse private - lookupActionId : (pparams : PParams) (role : GovRole) (aid : GovActionID) (s : GovState) → - Dec (Any (λ (aid' , ast) → aid ≡ aid' × canVote pparams (action ast) role) s) - lookupActionId pparams role aid = any? λ _ → ¿ _ ¿ - isUpdateCommittee : (a : GovAction) → Dec (∃[ new ] ∃[ rem ] ∃[ q ] a ≡ UpdateCommittee new rem q) isUpdateCommittee NoConfidence = no λ() isUpdateCommittee (UpdateCommittee new rem q) = yes (new , rem , q , refl) @@ -97,16 +93,16 @@ instance module GoVote sig where open GovVote sig - computeProof = case lookupActionId pparams (proj₁ voter) gid s ,′ isRegistered? (proj₁ Γ) voter of λ where + computeProof = case L.lookupActionId pparams (proj₁ voter) gid epoch s ,′ isRegistered? (proj₁ Γ) voter of λ where (yes p , yes p') → case Any↔ .from p of λ where - (_ , mem , refl , cV) → success (_ , GOV-Vote (∈-fromList .to mem , cV , p')) + (_ , mem , refl , cV , ¬exp) → success (_ , GOV-Vote (∈-fromList .to mem , cV , p' , ¬exp)) (yes _ , no ¬p) → failure (genErrors ¬p) (no ¬p , _) → failure (genErrors ¬p) completeness : ∀ s' → Γ ⊢ s ⇀⦇ inj₁ sig ,GOV'⦈ s' → map proj₁ computeProof ≡ success s' - completeness s' (GOV-Vote (mem , cV , reg)) - with lookupActionId pparams (proj₁ voter) gid s | isRegistered? (proj₁ Γ) voter - ... | no ¬p | _ = ⊥-elim (¬p (Any↔ .to (_ , ∈-fromList .from mem , refl , cV))) + completeness s' (GOV-Vote (mem , cV , reg , ¬exp)) + with L.lookupActionId pparams (proj₁ voter) gid epoch s | isRegistered? (proj₁ Γ) voter + ... | no ¬p | _ = ⊥-elim (¬p (Any↔ .to (_ , ∈-fromList .from mem , refl , cV , ¬exp))) ... | yes _ | no ¬p = ⊥-elim $ ¬p reg ... | yes p | yes p' with Any↔ .from p ... | (_ , mem , refl , cV) = refl @@ -117,33 +113,57 @@ instance open PParams pparams hiding (a) instance - Dec-actionWellFormed = actionWellFormed? + Dec-actionWellFormed = L.actionWellFormed? + Dec-actionValid = L.actionValid? {-# INCOHERENT Dec-actionWellFormed #-} + {-# INCOHERENT Dec-actionValid #-} - H = ¿ actionWellFormed a + H = ¿ L.actionWellFormed a + × L.actionValid rewardCreds p ppolicy epoch a × d ≡ govActionDeposit × L.validHFAction prop s enactState - × (∃[ u ] a ≡ ChangePParams u ⊎ ∃[ w ] a ≡ TreasuryWdrl w → p ≡ ppolicy) - × (¬ (∃[ u ] a ≡ ChangePParams u ⊎ ∃[ w ] a ≡ TreasuryWdrl w) → p ≡ nothing) × L.hasParent' enactState s a prev - × addr .RwdAddr.net ≡ NetworkId ¿ + × addr .RwdAddr.net ≡ NetworkId + × addr .RwdAddr.stake ∈ rewardCreds ¿ ,′ isUpdateCommittee a + genErrorsActionWellFormed : ∀ {a} → ¬ (L.actionWellFormed a) → String + genErrorsActionWellFormed {NoConfidence} ¬p = genErrors ¬p + genErrorsActionWellFormed {UpdateCommittee _ _ _} ¬p = genErrors ¬p + genErrorsActionWellFormed {NewConstitution _ _} ¬p = genErrors ¬p + genErrorsActionWellFormed {TriggerHF _} ¬p = genErrors ¬p + genErrorsActionWellFormed {ChangePParams _} ¬p = genErrors ¬p + genErrorsActionWellFormed {TreasuryWdrl _} ¬p = genErrors ¬p + genErrorsActionWellFormed {Info} ¬p = genErrors ¬p + + genErrorsActionValid : ∀ {a} → ¬ (L.actionValid rewardCreds p ppolicy epoch a) → String + genErrorsActionValid {NoConfidence} ¬p = genErrors ¬p + genErrorsActionValid {UpdateCommittee _ _ _} ¬p = genErrors ¬p + genErrorsActionValid {NewConstitution _ _} ¬p = genErrors ¬p + genErrorsActionValid {TriggerHF _} ¬p = genErrors ¬p + genErrorsActionValid {ChangePParams _} ¬p = genErrors ¬p + genErrorsActionValid {TreasuryWdrl _} ¬p = genErrors ¬p + genErrorsActionValid {Info} ¬p = genErrors ¬p + computeProof = case H of λ where - (yes (wf , dep , vHFA , pol , ¬pol , L.HasParent' en , goodAddr) , yes (new , rem , q , refl)) → + (yes (wf , av , dep , vHFA , L.HasParent' en , goodAddr , regReward) , yes (new , rem , q , refl)) → case ¿ ∀[ e ∈ range new ] epoch < e × dom new ∩ rem ≡ᵉ ∅ ¿ of λ where - (yes newOk) → success (_ , GOV-Propose (wf , dep , pol , ¬pol , (λ where refl → newOk) , vHFA , en , goodAddr)) + (yes newOk) → success (_ , GOV-Propose (wf , av , dep , vHFA , en , goodAddr , regReward)) (no ¬p) → failure (genErrors ¬p) - (yes (wf , dep , vHFA , pol , ¬pol , L.HasParent' en , goodAddr) , no notNewComm) → success - (-, GOV-Propose (wf , dep , pol , ¬pol , (λ isNewComm → ⊥-elim (notNewComm (-, -, -, isNewComm))) , vHFA , en , goodAddr)) - (no ¬p , _) → failure (genErrors ¬p) + (yes (wf , av , dep , vHFA , L.HasParent' en , goodAddr) , no notNewComm) → success + (-, GOV-Propose (wf , av , dep , vHFA , en , goodAddr)) + (no ¬p , _) → case dec-de-morgan ¬p of λ where + (inj₁ q) → failure (genErrorsActionWellFormed q) + (inj₂ q) → case dec-de-morgan q of λ where + (inj₁ r) → failure (genErrorsActionValid r) + (inj₂ r) → failure (genErrors r) completeness : ∀ s' → Γ ⊢ s ⇀⦇ inj₂ prop ,GOV'⦈ s' → map proj₁ computeProof ≡ success s' - completeness s' (GOV-Propose (wf , dep , pol , ¬pol , newOk , vHFA , en , goodAddr)) with H - ... | (no ¬p , _) = ⊥-elim (¬p (wf , dep , vHFA , pol , ¬pol , L.HasParent' en , goodAddr)) - ... | (yes (_ , _ , _ , _ , _ , L.HasParent' _ , _) , no notNewComm) = refl - ... | (yes (_ , _ , _ , _ , _ , L.HasParent' _ , _) , yes (new , rem , q , refl)) - rewrite dec-yes ¿ ∀[ e ∈ range new ] epoch < e × dom new ∩ rem ≡ᵉ ∅ ¿ (newOk refl) .proj₂ = refl + completeness s' (GOV-Propose (wf , av , dep , vHFA , en , goodAddr)) with H + ... | (no ¬p , _) = ⊥-elim (¬p (wf , av , dep , vHFA , L.HasParent' en , goodAddr)) + ... | (yes (_ , _ , _ , _ , L.HasParent' _ , _) , no notNewComm) = refl + ... | (yes (_ , (_ , (av₁ , av₂)) , _ , _ , L.HasParent' _ , _) , yes (new , rem , q , refl)) + rewrite dec-yes ¿ ∀[ e ∈ range new ] epoch < e × dom new ∩ rem ≡ᵉ ∅ ¿ (λ { x → av₁ x , av₂ }) .proj₂ = refl computeProof : (sig : GovVote ⊎ GovProposal) → _ computeProof (inj₁ s) = GoVote.computeProof s diff --git a/src/Ledger/Conway/Conformance/Ledger.agda b/src/Ledger/Conway/Conformance/Ledger.agda index c37dc12dc9..54089a7d3d 100644 --- a/src/Ledger/Conway/Conformance/Ledger.agda +++ b/src/Ledger/Conway/Conformance/Ledger.agda @@ -58,8 +58,6 @@ private variable tx : Tx open RwdAddr -open DState -open CertState open UTxOState data @@ -70,12 +68,13 @@ data LEDGER-V : let open LState s; txb = tx .body; open TxBody txb; open LEnv Γ + open CertState certState; open DState dState utxoSt'' = record utxoSt' { deposits = L.updateDeposits pparams txb (deposits utxoSt') } in ∙ isValid tx ≡ true ∙ record { LEnv Γ } ⊢ utxoSt ⇀⦇ tx ,UTXOW⦈ utxoSt' ∙ ⟦ epoch slot , pparams , txvote , txwdrls , allColdCreds govSt enactState ⟧ᶜ ⊢ certState ⇀⦇ txcerts ,CERTS⦈ certState' - ∙ ⟦ txid , epoch slot , pparams , ppolicy , enactState , certState' ⟧ᵍ ⊢ govSt |ᵒ certState' ⇀⦇ txgov txb ,GOV⦈ govSt' + ∙ ⟦ txid , epoch slot , pparams , ppolicy , enactState , certState' , dom rewards ⟧ᵍ ⊢ govSt |ᵒ certState' ⇀⦇ txgov txb ,GOV⦈ govSt' ──────────────────────────────── Γ ⊢ s ⇀⦇ tx ,LEDGER⦈ ⟦ utxoSt'' , govSt' , certState' ⟧ˡ diff --git a/src/Ledger/Conway/Conformance/Ledger/Properties.agda b/src/Ledger/Conway/Conformance/Ledger/Properties.agda index 5f1c6f6833..a3850f80ba 100644 --- a/src/Ledger/Conway/Conformance/Ledger/Properties.agda +++ b/src/Ledger/Conway/Conformance/Ledger/Properties.agda @@ -65,7 +65,7 @@ instance utxoΓ = UTxOEnv ∋ record { LEnv Γ } certΓ = CertEnv ∋ ⟦ epoch slot , pparams , txvote , txwdrls , _ ⟧ᶜ govΓ : CertState → GovEnv - govΓ = ⟦ txid , epoch slot , pparams , ppolicy , enactState ,_⟧ᵍ + govΓ certState = ⟦ txid , epoch slot , pparams , ppolicy , enactState , certState , _ ⟧ᵍ computeProof : ComputationResult String (∃[ s' ] Γ ⊢ s ⇀⦇ tx ,LEDGER⦈ s') computeProof = case isValid ≟ true of λ where diff --git a/src/Ledger/Gov.lagda b/src/Ledger/Gov.lagda index 0f200a6464..99f2c0f6ad 100644 --- a/src/Ledger/Gov.lagda +++ b/src/Ledger/Gov.lagda @@ -31,9 +31,26 @@ open import Function.Related.Propositional using (↔⇒) open GovActionState \end{code} -\begin{figure*}[h] +The behavior of \GovState is similar to that of a queue. New proposals are appended at +the end, but any proposal can be removed at the epoch +boundary. However, for the purposes of enactment, earlier proposals +take priority. Note that \EnactState used in \GovEnv is defined later, +in Section~\ref{sec:enactment}. + +\begin{itemize} +\item \addVote inserts (and potentially overrides) a vote made for a +particular governance action (identified by its ID) by a credential with a role. + +\item \addAction adds a new proposed action at the end of a given \GovState. + +\item The \validHFAction property indicates whether a given proposal, if it is a +\TriggerHF action, can potentially be enacted in the future. For this to be the +case, its \prevAction needs to exist, be another \TriggerHF action and have a +compatible version. +\end{itemize} + +\begin{figure*} \emph{Derived types} -\begin{AgdaMultiCode} \begin{code}[hide] GovState : Type \end{code} @@ -41,7 +58,7 @@ GovState : Type GovState = List (GovActionID × GovActionState) record GovEnv : Type where - constructor ⟦_,_,_,_,_,_⟧ᵍ + constructor ⟦_,_,_,_,_,_,_⟧ᵍ field txid : TxId epoch : Epoch @@ -49,8 +66,12 @@ record GovEnv : Type where ppolicy : Maybe ScriptHash enactState : EnactState certState : CertState + rewardCreds : ℙ Credential \end{code} -\end{AgdaMultiCode} +\caption{Derived used in the GOV transition system} +\label{defs:gov-derived-types} +\end{figure*} + \begin{code}[hide] private variable Γ : GovEnv @@ -69,8 +90,10 @@ private variable open GState open PState \end{code} + +\begin{figure*} +\begin{AgdaMultiCode} \emph{Functions used in the GOV rules} -\begin{AgdaSuppressSpace} \begin{code} govActionPriority : GovAction → ℕ govActionPriority NoConfidence = 0 @@ -124,7 +147,7 @@ opaque { votes = if gid ≡ aid then insert (votes s') voter v else votes s'} isRegistered : GovEnv → Voter → Type - isRegistered ⟦ _ , _ , _ , _ , _ , ⟦ _ , pState , gState ⟧ᶜˢ ⟧ᵍ (r , c) = case r of λ where + isRegistered ⟦ _ , _ , _ , _ , _ , ⟦ _ , pState , gState ⟧ᶜˢ , _ ⟧ᵍ (r , c) = case r of λ where CC → just c ∈ range (gState .ccHotKeys) DRep → c ∈ dom (gState .dreps) SPO → c ∈ mapˢ KeyHashObj (dom (pState .pools)) @@ -135,24 +158,46 @@ opaque ⊎ ∃₂[ x , v' ] (prev , x) ∈ fromList s × x .action ≡ TriggerHF v' × pvCanFollow v' v validHFAction _ _ _ = ⊤ \end{code} -\end{AgdaSuppressSpace} +\end{AgdaMultiCode} +\caption{Functions used in the GOV transition system} +\label{defs:gov-functions} +\end{figure*} + +\begin{figure*} +\begin{AgdaMultiCode} \emph{Transition relation types} \begin{code}[hide] data \end{code} -\begin{AgdaSuppressSpace} \begin{code} _⊢_⇀⦇_,GOV'⦈_ : GovEnv × ℕ → GovState → GovVote ⊎ GovProposal → GovState → Type \end{code} \begin{code} _⊢_⇀⦇_,GOV⦈_ : GovEnv → GovState → List (GovVote ⊎ GovProposal) → GovState → Type \end{code} -\end{AgdaSuppressSpace} -\caption{Types and functions used in the GOV transition system} +\end{AgdaMultiCode} +\caption{Type signature of the transition relation of the GOV transition system} \label{defs:gov-defs} \end{figure*} -\begin{figure*}[ht] +Figure~\ref{defs:enactable} shows some of the functions used to determine whether certain +actions are enactable in a given state. Specifically, \AgdaFunction{allEnactable} passes +the \AgdaFunction{GovState} to \AgdaFunction{getAidPairsList} to obtain a list of +\AgdaFunction{GovActionID}-pairs which is then passed to \AgdaFunction{enactable}. The latter uses the +\AgdaFunction{\AgdaUnderscore{}connects\AgdaUnderscore{}to\AgdaUnderscore{}} function to check +whether the list of \AgdaFunction{GovActionID}-pairs connects the proposed action to a previously +enacted one. + +Additionally, \govActionPriority assigns a priority to the various governance action types. +This is useful for ordering lists of governance actions as well as grouping governance +actions by constructor. In particular, the relations +\AgdaOperator{\AgdaFunction{\AgdaUnderscore{}∼\AgdaUnderscore{}}} and +\AgdaOperator{\AgdaFunction{\AgdaUnderscore{}≈\AgdaUnderscore{}}} defined in +Figure~\ref{defs:enactable} are used for determining whether two actions are of the same +``kind'' in the following sense: either the actions arise from the same constructor, or one +action is \NoConfidence and the other is an \UpdateCommittee action. + +\begin{figure*} \begin{AgdaMultiCode} \begin{code}[hide] -- Convert list of (GovActionID,GovActionState)-pairs to list of GovActionID pairs. @@ -282,43 +327,76 @@ maxAllEnactable e = maxsublists⊧P (allEnactable? e) \label{defs:enactable} \end{figure*} -The behavior of \GovState is similar to that of a queue. New proposals are appended at -the end, but any proposal can be removed at the epoch -boundary. However, for the purposes of enactment, earlier proposals -take priority. Note that \EnactState used in \GovEnv is defined later, -in Section~\ref{sec:enactment}. - -\begin{itemize} -\item \addVote inserts (and potentially overrides) a vote made for a -particular governance action (identified by its ID) by a credential with a role. +\clearpage -\item \addAction adds a new proposed action at the end of a given \GovState. +\begin{figure*} +\begin{code} +actionValid : ℙ Credential → Maybe ScriptHash → Maybe ScriptHash → Epoch → GovAction → Type +actionValid rewardCreds p ppolicy epoch (ChangePParams x) = + p ≡ ppolicy +actionValid rewardCreds p ppolicy epoch (TreasuryWdrl x) = + p ≡ ppolicy × mapˢ RwdAddr.stake (dom x) ⊆ rewardCreds +actionValid rewardCreds p ppolicy epoch (UpdateCommittee new rem q) = + p ≡ nothing × (∀[ e ∈ range new ] epoch < e) × (dom new ∩ rem ≡ᵉ ∅) +actionValid rewardCreds p ppolicy epoch _ = + p ≡ nothing + +actionWellFormed : GovAction → Type +actionWellFormed (ChangePParams x) = ppdWellFormed x +actionWellFormed (TreasuryWdrl x) = + (∀[ a ∈ dom x ] RwdAddr.net a ≡ NetworkId) × (∃[ v ∈ range x ] ¬ (v ≡ 0)) +actionWellFormed _ = ⊤ +\end{code} +\caption{Validity and wellformedness predicates} +\label{fig:valid-and-wellformed} +\end{figure*} -\item The \validHFAction property indicates whether a given proposal, if it is a -\TriggerHF action, can potentially be enacted in the future. For this to be the -case, its \prevAction needs to exist, be another \TriggerHF action and have a -compatible version. +Figure~\ref{fig:valid-and-wellformed} defines predicates used in the \GOVPropose{} case +of the GOV rule to ensure that a governance action is valid and well-formed. +\begin{itemize} + \item \actionValid{} ensures that the proposed action is valid given the current state of the system: + \begin{itemize} + \item a \ChangePParams{} action is valid if the proposal policy is provided; + \item a \TreasuryWdrl{} action is valid if the proposal policy is provided and the reward stake + credential is registered; + \item an \UpdateCommittee{} action is valid if credentials of proposed candidates + have not expired, and the action does not propose to both add and + remove the same candidate. + \end{itemize} + \item \actionWellFormed{} ensures that the proposed action is well-formed: + \begin{itemize} + \item a \ChangePParams{} action must preserves well-formedness of the protocol parameters; + \item a \TreasuryWdrl{} action is well-formed if the network ID is correct and + there is at least one non-zero withdrawal amount in the given \RwdAddrToCoinMap{} map. + \end{itemize} \end{itemize} -Figure~\ref{defs:enactable} shows some of the functions used to determine whether certain -actions are enactable in a given state. Specifically, \AgdaFunction{allEnactable} passes -the \AgdaFunction{GovState} to \AgdaFunction{getAidPairsList} to obtain a list of -\AgdaFunction{GovActionID}-pairs which is then passed to \AgdaFunction{enactable}. The latter uses the -\AgdaFunction{\AgdaUnderscore{}connects\AgdaUnderscore{}to\AgdaUnderscore{}} function to check -whether the list of \AgdaFunction{GovActionID}-pairs connects the proposed action to a previously -enacted one. -Additionally, \govActionPriority assigns a priority to the various governance action types. -This is useful for ordering lists of governance actions as well as grouping governance -actions by constructor. In particular, the relations -\AgdaOperator{\AgdaFunction{\AgdaUnderscore{}∼\AgdaUnderscore{}}} and -\AgdaOperator{\AgdaFunction{\AgdaUnderscore{}≈\AgdaUnderscore{}}} defined in -Figure~\ref{defs:enactable} are used for determining whether two actions are of the same -``kind'' in the following sense: either the actions arise from the same constructor, or one -action is \NoConfidence and the other is an \UpdateCommittee action. +\begin{code}[hide] +actionValid? : ∀ {rewardCreds p ppolicy epoch a} → actionValid rewardCreds p ppolicy epoch a ⁇ +actionValid? {a = NoConfidence} = it +actionValid? {a = UpdateCommittee _ _ _} = it +actionValid? {a = NewConstitution _ _} = it +actionValid? {a = TriggerHF _} = it +actionValid? {a = ChangePParams _} = it +actionValid? {a = TreasuryWdrl _} = it +actionValid? {a = Info} = it + +actionWellFormed? : ∀ {a} → actionWellFormed a ⁇ +actionWellFormed? {NoConfidence} = it +actionWellFormed? {UpdateCommittee _ _ _} = it +actionWellFormed? {NewConstitution _ _} = it +actionWellFormed? {TriggerHF _} = it +actionWellFormed? {ChangePParams _} = it +actionWellFormed? {TreasuryWdrl _} = it +actionWellFormed? {Info} = it +\end{code} + +\clearpage \begin{figure*} -\begin{code}[hide] +\begin{AgdaMultiCode} +\begin{code} data _⊢_⇀⦇_,GOV'⦈_ where \end{code} \begin{code} @@ -329,6 +407,7 @@ data _⊢_⇀⦇_,GOV'⦈_ where ∙ (aid , ast) ∈ fromList s ∙ canVote pparams (action ast) (proj₁ voter) ∙ isRegistered Γ voter + ∙ ¬ (expired epoch ast) ─────────────────────────────────────── (Γ , k) ⊢ s ⇀⦇ inj₁ vote ,GOV'⦈ addVote s aid voter v @@ -339,19 +418,18 @@ data _⊢_⇀⦇_,GOV'⦈_ where s' = addAction s (govActionLifetime +ᵉ epoch) (txid , k) addr a prev in ∙ actionWellFormed a + ∙ actionValid rewardCreds p ppolicy epoch a ∙ d ≡ govActionDeposit - ∙ (∃[ u ] a ≡ ChangePParams u ⊎ ∃[ w ] a ≡ TreasuryWdrl w → p ≡ ppolicy) - ∙ (¬ (∃[ u ] a ≡ ChangePParams u ⊎ ∃[ w ] a ≡ TreasuryWdrl w) → p ≡ nothing) - ∙ (∀ {new rem q} → a ≡ UpdateCommittee new rem q - → ∀[ e ∈ range new ] epoch < e × dom new ∩ rem ≡ᵉ ∅) ∙ validHFAction prop s enactState ∙ hasParent enactState s a prev ∙ addr .RwdAddr.net ≡ NetworkId + ∙ addr .RwdAddr.stake ∈ rewardCreds ─────────────────────────────────────── (Γ , k) ⊢ s ⇀⦇ inj₂ prop ,GOV'⦈ s' _⊢_⇀⦇_,GOV⦈_ = ReflexiveTransitiveClosureᵢ {sts = _⊢_⇀⦇_,GOV'⦈_} \end{code} +\end{AgdaMultiCode} \caption{Rules for the GOV transition system} \label{defs:gov-rules} \end{figure*} @@ -360,19 +438,15 @@ The GOV transition system is now given as the reflexitive-transitive closure of the system GOV', described in Figure~\ref{defs:gov-rules}. -For \GOVVote, we check that the governance action being voted on -exists and the role is allowed to vote. \canVote is defined in +For \GOVVote{}, we check that the governance action being voted on +exists and the role is allowed to vote. \canVote{} is defined in Figure~\ref{fig:ratification-requirements}. Note that there are no checks on whether the credential is actually associated with the -role. This means that anyone can vote for, e.g., the \CC role. However, +role. This means that anyone can vote for, e.g., the \CC{} role. However, during ratification those votes will only carry weight if they are properly associated with members of the constitutional committee. -For \GOVPropose, we check well-formedness, correctness of the deposit -and some conditions depending on the type of the action: -\begin{itemize} -\item for \ChangePParams or \TreasuryWdrl, the proposal policy needs to be provided; -\item for \UpdateCommittee, no proposals with members expiring in the present or past - epoch are allowed, and candidates cannot be added and removed at the same time; -\item and we check the validity of hard-fork actions via \validHFAction. -\end{itemize} +For \GOVPropose{}, we check the correctness of the deposit along with some +and some conditions that ensure the action is well-formed and valid; +naturally, these checks depend on the type of action being proposed +(see Figure~\ref{fig:valid-and-wellformed}). diff --git a/src/Ledger/Gov/Properties.agda b/src/Ledger/Gov/Properties.agda index 19c6c09907..94a5a28dfe 100644 --- a/src/Ledger/Gov/Properties.agda +++ b/src/Ledger/Gov/Properties.agda @@ -31,11 +31,13 @@ open Equivalence open GovActionState open Inverse -private - lookupActionId : (pparams : PParams) (role : GovRole) (aid : GovActionID) (s : GovState) → - Dec (Any (λ (aid' , ast) → aid ≡ aid' × canVote pparams (action ast) role) s) - lookupActionId pparams role aid = any? λ _ → ¿ _ ¿ +lookupActionId : (pparams : PParams) (role : GovRole) (aid : GovActionID) (epoch : Epoch) (s : GovState) → + Dec (Any (λ (aid' , ast) → aid ≡ aid' × canVote pparams (action ast) role × ¬ (expired epoch ast)) s) +lookupActionId pparams role aid epoch = + let instance _ = λ {e ga} → ⁇ (expired? e ga) + in any? λ _ → ¿ _ ¿ +private isUpdateCommittee : (a : GovAction) → Dec (∃[ new ] ∃[ rem ] ∃[ q ] a ≡ UpdateCommittee new rem q) isUpdateCommittee NoConfidence = no λ() isUpdateCommittee (UpdateCommittee new rem q) = yes (new , rem , q , refl) @@ -111,19 +113,19 @@ instance module GoVote sig where open GovVote sig - computeProof = case lookupActionId pparams (proj₁ voter) gid s ,′ isRegistered? (proj₁ Γ) voter of λ where + computeProof = case lookupActionId pparams (proj₁ voter) gid epoch s ,′ isRegistered? (proj₁ Γ) voter of λ where (yes p , yes p') → case Any↔ .from p of λ where - (_ , mem , refl , cV) → success (_ , GOV-Vote (∈-fromList .to mem , cV , p')) + (_ , mem , refl , cV , ¬exp) → success (_ , GOV-Vote (∈-fromList .to mem , cV , p' , ¬exp)) (yes _ , no ¬p) → failure (genErrors ¬p) - (no ¬p , _) → failure (genErrors ¬p) + (no ¬p , _ ) → failure (genErrors ¬p) completeness : ∀ s' → Γ ⊢ s ⇀⦇ inj₁ sig ,GOV'⦈ s' → map proj₁ computeProof ≡ success s' - completeness s' (GOV-Vote (mem , cV , reg)) - with lookupActionId pparams (proj₁ voter) gid s | isRegistered? (proj₁ Γ) voter - ... | no ¬p | _ = ⊥-elim (¬p (Any↔ .to (_ , ∈-fromList .from mem , refl , cV))) + completeness s' (GOV-Vote {ast = ast} (mem , cV , reg , ¬expired)) + with lookupActionId pparams (proj₁ voter) gid epoch s | isRegistered? (proj₁ Γ) voter + ... | no ¬p | _ = ⊥-elim (¬p (Any↔ .to (_ , ∈-fromList .from mem , refl , cV , ¬expired))) ... | yes _ | no ¬p = ⊥-elim $ ¬p reg - ... | yes p | yes p' with Any↔ .from p - ... | (_ , mem , refl , cV) = refl + ... | yes p | yes q with Any↔ .from p + ... | ((_ , ast') , mem , refl , cV) = refl module GoProp prop where open GovProposal prop @@ -132,32 +134,34 @@ instance instance Dec-actionWellFormed = actionWellFormed? + Dec-actionValid = actionValid? {-# INCOHERENT Dec-actionWellFormed #-} + {-# INCOHERENT Dec-actionValid #-} H = ¿ actionWellFormed a + × actionValid rewardCreds p ppolicy epoch a × d ≡ govActionDeposit × validHFAction prop s enactState - × (∃[ u ] a ≡ ChangePParams u ⊎ ∃[ w ] a ≡ TreasuryWdrl w → p ≡ ppolicy) - × (¬ (∃[ u ] a ≡ ChangePParams u ⊎ ∃[ w ] a ≡ TreasuryWdrl w) → p ≡ nothing) × hasParent' enactState s a prev - × addr .RwdAddr.net ≡ NetworkId ¿ + × addr .RwdAddr.net ≡ NetworkId + × addr .RwdAddr.stake ∈ rewardCreds ¿ ,′ isUpdateCommittee a computeProof = case H of λ where - (yes (wf , dep , vHFA , pol , ¬pol , HasParent' en , goodAddr) , yes (new , rem , q , refl)) → + (yes (wf , av , dep , vHFA , HasParent' en , goodAddr , regReturn) , yes (new , rem , q , refl)) → case ¿ ∀[ e ∈ range new ] epoch < e × dom new ∩ rem ≡ᵉ ∅ ¿ of λ where - (yes newOk) → success (_ , GOV-Propose (wf , dep , pol , ¬pol , (λ where refl → newOk) , vHFA , en , goodAddr)) + (yes newOk) → success (_ , GOV-Propose (wf , av , dep , vHFA , en , goodAddr , regReturn)) (no ¬p) → failure (genErrors ¬p) - (yes (wf , dep , vHFA , pol , ¬pol , HasParent' en , goodAddr) , no notNewComm) → success - (-, GOV-Propose (wf , dep , pol , ¬pol , (λ isNewComm → ⊥-elim (notNewComm (-, -, -, isNewComm))) , vHFA , en , goodAddr)) + (yes (wf , av , dep , vHFA , HasParent' en , goodAddr , returnReg) , no notNewComm) → success + (-, GOV-Propose (wf , av , dep , vHFA , en , goodAddr , returnReg)) (no ¬p , _) → failure (genErrors ¬p) completeness : ∀ s' → Γ ⊢ s ⇀⦇ inj₂ prop ,GOV'⦈ s' → map proj₁ computeProof ≡ success s' - completeness s' (GOV-Propose (wf , dep , pol , ¬pol , newOk , vHFA , en , goodAddr)) with H - ... | (no ¬p , _) = ⊥-elim (¬p (wf , dep , vHFA , pol , ¬pol , HasParent' en , goodAddr)) - ... | (yes (_ , _ , _ , _ , _ , HasParent' _ , _) , no notNewComm) = refl - ... | (yes (_ , _ , _ , _ , _ , HasParent' _ , _) , yes (new , rem , q , refl)) - rewrite dec-yes ¿ ∀[ e ∈ range new ] epoch < e × dom new ∩ rem ≡ᵉ ∅ ¿ (newOk refl) .proj₂ = refl + completeness s' (GOV-Propose (wf , av , dep , vHFA , en , goodAddr)) with H + ... | (no ¬p , _) = ⊥-elim (¬p (wf , av , dep , vHFA , HasParent' en , goodAddr)) + ... | (yes (_ , _ , _ , _ , HasParent' _ , _) , no notNewComm) = refl + ... | (yes (_ , (_ , (av₁ , av₂)) , _ , _ , HasParent' _ , _) , yes (new , rem , q , refl)) + rewrite dec-yes ¿ ∀[ e ∈ range new ] epoch < e × dom new ∩ rem ≡ᵉ ∅ ¿ (λ { x → av₁ x , av₂ }) .proj₂ = refl computeProof : (sig : GovVote ⊎ GovProposal) → _ computeProof (inj₁ s) = GoVote.computeProof s diff --git a/src/Ledger/GovernanceActions.lagda b/src/Ledger/GovernanceActions.lagda index d31a906ff7..82bde726a5 100644 --- a/src/Ledger/GovernanceActions.lagda +++ b/src/Ledger/GovernanceActions.lagda @@ -60,23 +60,6 @@ data GovAction : Type where ChangePParams : PParamsUpdate → GovAction TreasuryWdrl : (RwdAddr ⇀ Coin) → GovAction Info : GovAction - -actionWellFormed : GovAction → Type -actionWellFormed (ChangePParams x) = ppdWellFormed x -actionWellFormed (TreasuryWdrl x) = - (∀[ a ∈ dom x ] RwdAddr.net a ≡ NetworkId) - × (∃[ v ∈ range x ] ¬ (v ≡ 0)) -actionWellFormed _ = ⊤ -\end{code} -\begin{code}[hide] -actionWellFormed? : ∀ {a} → actionWellFormed a ⁇ -actionWellFormed? {NoConfidence} = it -actionWellFormed? {UpdateCommittee _ _ _} = it -actionWellFormed? {NewConstitution _ _} = it -actionWellFormed? {TriggerHF _} = it -actionWellFormed? {ChangePParams _} = it -actionWellFormed? {TreasuryWdrl _} = it -actionWellFormed? {Info} = it \end{code} \end{AgdaMultiCode} \caption{Governance actions} @@ -90,10 +73,6 @@ Figure~\ref{defs:governance} defines several data types used to represent govern \item \VDeleg (\defn{voter delegation})---one of three ways to delegate votes: by credential, abstention, or no confidence (\credVoter, \abstainRep, or \noConfidenceRep); \item \Anchor---a url and a document hash; \item \GovAction (\defn{governance action})---one of seven possible actions (see Figure~\ref{fig:types-of-governance-actions} for definitions); - \item \actionWellFormed---in the case of protocol parameter changes, - an action is well-formed if it preserves the well-formedness of parameters. - \ppdWellFormed is effectively the same as \paramsWellFormed, except that it - only applies to the parameters that are being changed. \end{itemize} The governance actions carry the following information: \begin{itemize} diff --git a/src/Ledger/Ledger.lagda b/src/Ledger/Ledger.lagda index 0206ab4b18..604870265a 100644 --- a/src/Ledger/Ledger.lagda +++ b/src/Ledger/Ledger.lagda @@ -83,11 +83,6 @@ private variable \begin{NoConway} \begin{figure*}[h] \begin{code}[hide] -open RwdAddr -open DState -open CertState -open UTxOState - data \end{code} \begin{code} @@ -103,11 +98,19 @@ data \begin{figure*}[htb] \begin{AgdaSuppressSpace} \begin{code} - LEDGER-V : let open LState s; txb = tx .body; open TxBody txb; open LEnv Γ in + LEDGER-V : + let + open LState s + txb = tx .body + open TxBody txb + open LEnv Γ + open CertState certState + open DState dState + in ∙ isValid tx ≡ true ∙ record { LEnv Γ } ⊢ utxoSt ⇀⦇ tx ,UTXOW⦈ utxoSt' ∙ ⟦ epoch slot , pparams , txvote , txwdrls , allColdCreds govSt enactState ⟧ᶜ ⊢ certState ⇀⦇ txcerts ,CERTS⦈ certState' - ∙ ⟦ txid , epoch slot , pparams , ppolicy , enactState , certState' ⟧ᵍ ⊢ govSt |ᵒ certState' ⇀⦇ txgov txb ,GOV⦈ govSt' + ∙ ⟦ txid , epoch slot , pparams , ppolicy , enactState , certState' , dom rewards ⟧ᵍ ⊢ govSt |ᵒ certState' ⇀⦇ txgov txb ,GOV⦈ govSt' ──────────────────────────────── Γ ⊢ s ⇀⦇ tx ,LEDGER⦈ ⟦ utxoSt' , govSt' , certState' ⟧ˡ \end{code} diff --git a/src/Ledger/Ledger/Properties.agda b/src/Ledger/Ledger/Properties.agda index b7ad3f66aa..6bce3a347f 100644 --- a/src/Ledger/Ledger/Properties.agda +++ b/src/Ledger/Ledger/Properties.agda @@ -66,7 +66,7 @@ instance utxoΓ = UTxOEnv ∋ record { LEnv Γ } certΓ = CertEnv ∋ ⟦ epoch slot , pparams , txvote , txwdrls , _ ⟧ᶜ govΓ : CertState → GovEnv - govΓ = ⟦ txid , epoch slot , pparams , ppolicy , enactState ,_⟧ᵍ + govΓ certState = ⟦ txid , epoch slot , pparams , ppolicy , enactState , certState , _ ⟧ᵍ computeProof : ComputationResult String (∃[ s' ] Γ ⊢ s ⇀⦇ tx ,LEDGER⦈ s') computeProof = case isValid ≟ true of λ where @@ -203,6 +203,9 @@ module LEDGER-PROPS (tx : Tx) (Γ : LEnv) (s : LState) where open Tx tx renaming (body to txb); open TxBody txb open LEnv Γ renaming (pparams to pp) open PParams pp using (govActionDeposit) + open LState s + open CertState certState + open DState dState -- initial utxo deposits utxoDeps : DepositPurpose ⇀ Coin @@ -233,10 +236,10 @@ module LEDGER-PROPS (tx : Tx) (Γ : LEnv) (s : LState) where -- updateGovStates faithfully represents a step of the LEDGER sts STS→GovSt≡ : ∀ {s' : LState} → Γ ⊢ s ⇀⦇ tx ,LEDGER⦈ s' → isValid ≡ true → LState.govSt s' ≡ updateGovStates (txgov txb) 0 (LState.govSt s |ᵒ LState.certState s') - STS→GovSt≡ (LEDGER-V x) refl = STS→updateGovSt≡ (txgov txb) 0 (proj₂ (proj₂ (proj₂ x))) + STS→GovSt≡ (LEDGER-V ( _ , _ , _ , x )) refl = STS→updateGovSt≡ (txgov txb) 0 x where STS→updateGovSt≡ : (vps : List (GovVote ⊎ GovProposal)) (k : ℕ) {certSt : CertState} {govSt govSt' : GovState} - → (_⊢_⇀⟦_⟧ᵢ*'_ {_⊢_⇀⟦_⟧ᵇ_ = IdSTS}{_⊢_⇀⦇_,GOV'⦈_} (⟦ txid , epoch slot , pp , ppolicy , enactState , certSt ⟧ᵍ , k) govSt vps govSt') + → (_⊢_⇀⟦_⟧ᵢ*'_ {_⊢_⇀⟦_⟧ᵇ_ = IdSTS}{_⊢_⇀⦇_,GOV'⦈_} (⟦ txid , epoch slot , pp , ppolicy , enactState , certSt , dom rewards ⟧ᵍ , k) govSt vps govSt') → govSt' ≡ updateGovStates vps k govSt STS→updateGovSt≡ [] _ (BS-base Id-nop) = refl STS→updateGovSt≡ (inj₁ v ∷ vps) k (BS-ind (GOV-Vote x) h) diff --git a/src/latex/agda-latex-macros.sty b/src/latex/agda-latex-macros.sty index 3092a3c26b..b18e59f715 100644 --- a/src/latex/agda-latex-macros.sty +++ b/src/latex/agda-latex-macros.sty @@ -12,6 +12,7 @@ \newcommand{\acceptedStakeRatio}{\AgdaFunction{acceptedStakeRatio}\xspace} \newcommand{\action}{\AgdaField{action}\xspace} \newcommand{\actionWellFormed}{\AgdaFunction{actionWellFormed}\xspace} +\newcommand{\actionValid}{\AgdaFunction{actionValid}\xspace} \newcommand{\activeDReps}{\AgdaFunction{activeDReps}\xspace} \newcommand{\activeVotingStake}{\AgdaFunction{activeVotingStake}\xspace} \newcommand{\actualCCVote}{\AgdaFunction{actualCCVote}\xspace} @@ -459,15 +460,16 @@ \newcommand{\role}{\AgdaField{role}\xspace} \newcommand{\roleVotes}{\AgdaFunction{roleVotes}\xspace} -\newcommand{\SPOs}{\AgdaInductiveConstructor{SPOs}\xspace} -\newcommand{\SPO}{\AgdaInductiveConstructor{SPO}\xspace} \newcommand{\RTC}{\AgdaFunction{ReflexiveTransitiveClosure}\xspace} \newcommand{\RTCI}{\AgdaOperator{\AgdaBound{\AgdaUnderscore{}⊢\AgdaUnderscore{}⇀⟦\AgdaUnderscore{}⟧*\AgdaUnderscore{}}}} \newcommand{\RTCB}{\AgdaOperator{\AgdaBound{\AgdaUnderscore{}⊢\AgdaUnderscore{}⇀⟦\AgdaUnderscore{}⟧\AgdaUnderscore{}}}} +\newcommand{\RwdAddrToCoinMap}{\AgdaRecord{RwdAddr}~\AgdaFunction{⇀}~\AgdaFunction{Coin}} \newcommand{\SecurityGroup}{\AgdaInductiveConstructor{SecurityGroup}\xspace} \newcommand{\StakeDistrs}{\AgdaRecord{StakeDistrs}\xspace} \newcommand{\snd}{\AgdaField{proj₂}\xspace} \newcommand{\specProperty}{\AgdaFunction{specProperty}\xspace} +\newcommand{\SPO}{\AgdaInductiveConstructor{SPO}\xspace} +\newcommand{\SPOs}{\AgdaInductiveConstructor{SPOs}\xspace} \newcommand{\sprime}{\AgdaGeneralizable{s'}\xspace} \newcommand{\spring}{\AgdaFunction{sp-∘}\xspace} \newcommand{\stake}{\AgdaField{stake}\xspace}