Skip to content

Commit

Permalink
improve organization of ratify functions and their docs
Browse files Browse the repository at this point in the history
  • Loading branch information
@williamdemeo
williamdemeo committed Oct 17, 2023
1 parent d93aed0 commit 4148822
Show file tree
Hide file tree
Showing 2 changed files with 69 additions and 61 deletions.
129 changes: 68 additions & 61 deletions src/Ledger/Ratify.lagda
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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;
Expand All @@ -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
Expand Down Expand Up @@ -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
Expand Down Expand Up @@ -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')
Expand Down
1 change: 1 addition & 0 deletions src/latex/agda-latex-macros.sty
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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}
Expand Down

0 comments on commit 4148822

Please sign in to comment.