From 4148822023440d9f9cfa2794c385560421ab1b0d Mon Sep 17 00:00:00 2001 From: William DeMeo Date: Tue, 17 Oct 2023 14:13:57 -0600 Subject: [PATCH] improve organization of ratify functions and their docs --- src/Ledger/Ratify.lagda | 129 +++++++++++++++++--------------- src/latex/agda-latex-macros.sty | 1 + 2 files changed, 69 insertions(+), 61 deletions(-) diff --git a/src/Ledger/Ratify.lagda b/src/Ledger/Ratify.lagda index 34c0ef4a5..bc358c6aa 100644 --- a/src/Ledger/Ratify.lagda +++ b/src/Ledger/Ratify.lagda @@ -231,77 +231,82 @@ restrictedDists coins rank dists = dists restrict : Credential ⇀ Coin → Credential ⇀ Coin restrict dist = topNDRepDist rank dist ∪ᵐˡ mostStakeDRepDist dist coins \end{code} +\begin{code}[hide] +module _ (Γ : RatifyEnv)(pparams : PParams) where + + open RatifyEnv Γ + open PParams pparams +\end{code} + \begin{figure*}[h!] +\begin{AgdaAlign} {\small \begin{code} -actualVotes : RatifyEnv → CCData → (GovRole × Credential) ⇀ Vote → GovAction → PParams - → VDeleg ⇀ Vote -actualVotes Γ cc votes ga pparams - = mapKeys (credVoter CC) actualCCVotes - ∪ᵐˡ actualPDRepVotes ∪ᵐˡ actualDRepVotes - ∪ᵐˡ actualSPOVotes - where - open RatifyEnv Γ - open PParams pparams + activeDReps : ℙ Credential + activeDReps = dom $ filterᵐ? (λ x → currentEpoch ≤? (proj₂ x)) dreps + + activeCC : CCData → ℙ Credential + activeCC (just (cc , _)) = dom $ filterᵐᵇ (is-just ∘ proj₂) (ccHotKeys ∣ dom cc) + activeCC nothing = ∅ + + actualPDRepVotes : GovAction → VDeleg ⇀ Vote + actualPDRepVotes NoConfidence = ❴ abstainRep , Vote.abstain ❵ᵐ + ∪ᵐˡ ❴ noConfidenceRep , Vote.yes ❵ᵐ + actualPDRepVotes _ = ❴ abstainRep , Vote.abstain ❵ᵐ + ∪ᵐˡ ❴ noConfidenceRep , Vote.no ❵ᵐ + + actualVotes : CCData → GovAction → (GovRole × Credential) ⇀ Vote → VDeleg ⇀ Vote + actualVotes cc ga votes = mapKeys (credVoter CC) (actualCCVotes cc) + ∪ᵐˡ actualPDRepVotes ga + ∪ᵐˡ actualDRepVotes + ∪ᵐˡ actualSPOVotes ga + where + spos : ℙ VDeleg + spos = filterˢ isSPOProp $ dom (StakeDistrs.stakeDistr stakeDistrs) - roleVotes : GovRole → VDeleg ⇀ Vote - roleVotes r = mapKeys (uncurry credVoter) (filterᵐ? ((r ≟_) ∘ proj₁ ∘ proj₁) votes) + actualCCVote : Credential → Epoch → Vote + actualCCVote c e = + case ¿ currentEpoch ≤ e ¿ᵇ , lookupᵐ? ccHotKeys c of + λ where (true , just (just c')) → maybe id Vote.no $ lookupᵐ? votes (CC , c') + _ → Vote.abstain -- expired, no hot key or resigned - activeCC activeDReps : ℙ Credential - activeCC = case cc of λ where - (just (cc , _)) → dom (filterᵐᵇ (is-just ∘ proj₂) (ccHotKeys ∣ dom cc)) - nothing → ∅ + actualCCVotes : CCData → Credential ⇀ Vote + actualCCVotes nothing = ∅ᵐ + actualCCVotes (just (cc , q)) = + case ¿ ccMinSize ≤ lengthˢ (activeCC $ just (cc , q)) ¿ᵇ of + λ where true → mapWithKey actualCCVote cc + false → constMap (dom cc) Vote.no - activeDReps = dom (filterᵐ? (λ x → currentEpoch ≤? (proj₂ x)) dreps) + roleVotes : GovRole → VDeleg ⇀ Vote + roleVotes r = mapKeys (uncurry credVoter) $ filterᵐ? ((r ≟_) ∘ proj₁ ∘ proj₁) votes - actualCCVote : Credential → Epoch → Vote - actualCCVote c e = - case ¿ currentEpoch ≤ e ¿ᵇ , lookupᵐ? ccHotKeys c of λ where - (true , just (just c')) → maybe id Vote.no $ lookupᵐ? votes (CC , c') - _ → Vote.abstain -- expired, no hot key or resigned - - actualCCVotes : Credential ⇀ Vote - actualCCVotes = case cc , ¿ ccMinSize ≤ lengthˢ activeCC ¿ᵇ of λ where - (just (cc , _) , true) → mapWithKey actualCCVote cc - (just (cc , _) , false) → constMap (dom cc) Vote.no - (nothing , _) → ∅ᵐ - - actualPDRepVotes - = ❴ abstainRep , Vote.abstain ❵ᵐ - ∪ᵐˡ ❴ noConfidenceRep , (case ga of λ where NoConfidence → Vote.yes - _ → Vote.no) ❵ᵐ - - actualDRepVotes - = roleVotes GovRole.DRep - ∪ᵐˡ constMap (mapˢ (credVoter DRep) activeDReps) Vote.no - - actualSPOVotes - = roleVotes GovRole.SPO - ∪ᵐˡ constMap spos (if isHF then Vote.no else Vote.abstain) - where - spos : ℙ VDeleg - spos = filterˢ isSPOProp $ dom (StakeDistrs.stakeDistr stakeDistrs) - - isHF : Bool - isHF = case ga of λ where - (TriggerHF _) → true - _ → false + actualSPOVotes : GovAction → VDeleg ⇀ Vote + actualSPOVotes (TriggerHF _) = roleVotes GovRole.SPO ∪ᵐˡ constMap spos Vote.no + actualSPOVotes _ = roleVotes GovRole.SPO ∪ᵐˡ constMap spos Vote.abstain + + actualDRepVotes : VDeleg ⇀ Vote + actualDRepVotes = roleVotes GovRole.DRep + ∪ᵐˡ constMap (mapˢ (credVoter DRep) activeDReps) Vote.no \end{code} -} %% end small +} % End: small +\end{AgdaAlign} \caption{%Ratify i: Types and proofs for the ratification of governance actions} \label{fig:defs:ratify-i} \end{figure*} -The code in Figure~\ref{fig:defs:ratify-i} defines some of the types required for ratification of a governance action. +The code in Figure~\ref{fig:defs:ratify-i} defines some of the functions required for ratification of a governance action. \begin{itemize} - \item Assuming a ratification environment \AgdaPostulate{Γ}, + \item We assume a ratification environment \AgdaPostulate{Γ} and define essential vote-counting functions whose behaviors + depend on \AgdaPostulate{Γ} as well as other inputs such as \begin{itemize} - \item \agdaboundcc contains constitutional committee data; - \item \agdaboundvotes is a relation associating each role-credential pair with the vote cast by the individual denoted by that pair; - \item \agdaboundga denotes the governance action being voted upon. + \item \agdaboundcc (of type \CCData), constitutional committee data; + \item \agdaboundvotes, a relation associating each role-credential pair with the vote cast by the individual denoted by that pair; + \item \agdaboundga (of type \GovAction), the governance action being voted upon. \end{itemize} - \item \roleVotes filters the votes based on the given governance role. + \item \actualPDRepVotes determines how the votes will be counted for \DReps; + here, \abstainRep is mapped to \abstain and \noConfidenceRep is mapped to either \yes or \no, + depending on the value of \agdaboundga. \item \actualCCVote determines how the vote of each \CC member will be counted; specifically, if a \CC member has not yet registered a hot key, has \expired, or has resigned, then \actualCCVote returns \abstain; @@ -313,14 +318,16 @@ The code in Figure~\ref{fig:defs:ratify-i} defines some of the types required fo \item \actualCCVotes uses \actualCCVote to determine how the votes of all \CC members will be counted. - \item \actualPDRepVotes determines how the votes will be counted for \DReps; - here, \abstainRep is mapped to \abstain and \noConfidenceRep is mapped to either \yes or \no, - depending on the value of \agdaboundga. + \item \roleVotes filters the votes based on the given governance role and is essentially a helper function for + \actualSPOVotes and \actualDRepVotes. + + \item \actualSPOVotes determines how the votes of \SPOs will be counted; \SPOs that didn't vote count as + \abstain, unless the action to be voted upon is a hard-fork in which case the default vote is \no. \item \actualDRepVotes determines how the votes of \DReps will be counted; \activeDReps that didn't vote count as a \no. \item \actualVotes is a partial function relating delegates to the actual vote that will be counted on their behalf; - it accomplishes this by aggregating the results of \actualCCVotes, \actualPDRepVotes, and \actualDRepVotes. + it accomplishes this by aggregating the results of \actualCCVotes, \actualPDRepVotes, \actualSPOVotes, and \actualDRepVotes. \end{itemize} \begin{figure*}[h!] {\small @@ -367,7 +374,7 @@ abstract acceptedBy : (Γ : RatifyEnv) (es : EnactState) (gs : GovActionState) → GovRole → Set acceptedBy Γ (record { cc = cc , _; pparams = pparams , _ }) gs role = let open RatifyEnv Γ; open GovActionState gs; open PParams pparams - votes' = actualVotes Γ cc votes action pparams + votes' = actualVotes Γ pparams cc action votes cc' = dom votes' redStakeDistr = restrictedDists coinThreshold rankThreshold stakeDistrs t = maybe id ℚ.0ℚ $ threshold pparams (proj₂ <$> cc) action role in @@ -440,7 +447,7 @@ abstract acceptedBy? : ∀ Γ es st role → Dec (acceptedBy Γ es st role) acceptedBy? Γ record{ cc = cc , _ ; pparams = pparams , _ } st role with (let open RatifyEnv Γ; open GovActionState st; open PParams pparams - votes' = actualVotes Γ cc votes action pparams + votes' = actualVotes Γ pparams cc action votes cc' = dom votes' redStakeDistr = restrictedDists coinThreshold rankThreshold stakeDistrs in totalStake role cc' redStakeDistr votes') diff --git a/src/latex/agda-latex-macros.sty b/src/latex/agda-latex-macros.sty index a22c880c2..81256f133 100644 --- a/src/latex/agda-latex-macros.sty +++ b/src/latex/agda-latex-macros.sty @@ -15,6 +15,7 @@ \newcommand{\activeVotingStake}{\AgdaFunction{activeVotingStake}\xspace} \newcommand{\actualCCVote}{\AgdaFunction{actualCCVote}\xspace} \newcommand{\actualCCVotes}{\AgdaFunction{actualCCVotes}\xspace} +\newcommand{\actualSPOVotes}{\AgdaFunction{actualSPOVotes}\xspace} \newcommand{\actualDRepVotes}{\AgdaFunction{actualDRepVotes}\xspace} \newcommand{\actualPDRepVotes}{\AgdaFunction{actualPDRepVotes}\xspace} \newcommand{\actualVotes}{\AgdaFunction{actualVotes}\xspace}