Ratification
{-# OPTIONS --safe #-}
open import Ledger.Dijkstra.Specification.Gov.Base
module Ledger.Dijkstra.Specification.Ratify (govStructure : GovStructure) where
import Data.Integer as ℤ
open import Data.Rational as ℚ using (ℚ; 0ℚ; _⊔_)
open import Data.Nat.Properties hiding (_≟_; _≤?_)
open import Ledger.Prelude hiding (_∧_; _∨_; _⊔_) renaming (filterᵐ to filter; ∣_∣ to _↓)
open import Ledger.Dijkstra.Specification.Certs govStructure
open import Ledger.Dijkstra.Specification.Enact govStructure
open import Ledger.Dijkstra.Specification.Gov.Actions govStructure hiding (yes; no)
open GovStructure govStructure
private
∣_∣_∣_∣ : {A : Type} → A → A → A → GovRole → A
∣ q₁ ∣ q₂ ∣ q₃ ∣ = λ { CC → q₁ ; DRep → q₂ ; SPO → q₃ }
∣_∥_∣ : {A : Type} → A → A × A → GovRole → A
∣ q₁ ∥ (q₂ , q₃) ∣ = λ { CC → q₁ ; DRep → q₂ ; SPO → q₃ }
threshold : PParams → Maybe ℚ → GovAction → GovRole → Maybe ℚ
threshold pp ccThreshold ga =
case ga ↓ of λ where
(NoConfidence , _ ) → ∣ ─ ∣ vote P1 ∣ vote Q1 ∣
(UpdateCommittee , _ ) → ∣ ─ ∥ P/Q2a/b ∣
(NewConstitution , _ ) → ∣ ✓ ∣ vote P3 ∣ ─ ∣
(TriggerHardFork , _ ) → ∣ ✓ ∣ vote P4 ∣ vote Q4 ∣
(ChangePParams , update ) → ∣ ✓ ∥ P/Q5 update ∣
(TreasuryWithdrawal , _ ) → ∣ ✓ ∣ vote P6 ∣ ─ ∣
(Info , _ ) → ∣ ✓† ∣ ✓† ∣ ✓† ∣
where
open PParams pp
open DrepThresholds drepThresholds
open PoolThresholds poolThresholds
vote : ℚ → Maybe ℚ
vote = just
defer : ℚ
defer = ℚ.1ℚ ℚ.+ ℚ.1ℚ
maxThreshold : ℙ (Maybe ℚ) → Maybe ℚ
maxThreshold x = foldl _∨_ nothing (proj₁ $ finiteness x)
where
_∨_ : Maybe ℚ → Maybe ℚ → Maybe ℚ
just x ∨ just y = just (x ⊔ y)
just x ∨ nothing = just x
nothing ∨ just y = just y
nothing ∨ nothing = nothing
─ ✓ ✓† : Maybe ℚ
─ = nothing
✓ = maybe just ✓† ccThreshold
✓† = vote defer
P/Q2a/b : Maybe ℚ × Maybe ℚ
P/Q2a/b = case ccThreshold of λ where
(just _) → (vote P2a , vote Q2a)
nothing → (vote P2b , vote Q2b)
pparamThreshold : PParamGroup → Maybe ℚ × Maybe ℚ
pparamThreshold NetworkGroup = (vote P5a , ─ )
pparamThreshold EconomicGroup = (vote P5b , ─ )
pparamThreshold TechnicalGroup = (vote P5c , ─ )
pparamThreshold GovernanceGroup = (vote P5d , ─ )
pparamThreshold SecurityGroup = (─ , vote Q5 )
P/Q5 : PParamsUpdate → Maybe ℚ × Maybe ℚ
P/Q5 ppu = maxThreshold (mapˢ (proj₁ ∘ pparamThreshold) (updateGroups ppu))
, maxThreshold (mapˢ (proj₂ ∘ pparamThreshold) (updateGroups ppu))
canVote : PParams → GovAction → GovRole → Type
canVote pp a r = Is-just (threshold pp nothing a r)
record RatifyEnv : Type where
field
stakeDistrVDeleg : VDeleg ⇀ Coin
stakeDistrPools : KeyHash ⇀ Coin
currentEpoch : Epoch
dreps : Credential ⇀ Epoch
ccHotKeys : Credential ⇀ Maybe Credential
treasury : Treasury
pools : KeyHash ⇀ StakePoolState
delegatees : VoteDelegs
record RatifyState : Type where
field
es : EnactState
removed : ℙ (GovActionID × GovActionState)
delay : Bool
record HasRatifyState {a} (A : Type a) : Type a where
field RatifyStateOf : A → RatifyState
open HasRatifyState ⦃...⦄ public
instance
HasEnactState-RatifyState : HasEnactState RatifyState
HasEnactState-RatifyState .EnactStateOf = RatifyState.es
HasDReps-RatifyEnv : HasDReps RatifyEnv
HasDReps-RatifyEnv .DRepsOf = RatifyEnv.dreps
HasTreasury-RatifyEnv : HasTreasury RatifyEnv
HasTreasury-RatifyEnv .TreasuryOf = RatifyEnv.treasury
unquoteDecl HasCast-RatifyEnv HasCast-RatifyState = derive-HasCast
( (quote RatifyEnv , HasCast-RatifyEnv)
∷ [ (quote RatifyState , HasCast-RatifyState) ])
Vote Counting
module AcceptedByCC (currentEpoch : Epoch)
(ccHotKeys : Credential ⇀ Maybe Credential)
(eSt : EnactState)
(gaSt : GovActionState)
where
open EnactState eSt using (cc)
open PParams (PParamsOf eSt)
open GovActionState gaSt
open GovVotes votes using (gvCC)
castVotes : Credential ⇀ Vote
castVotes = gvCC
getCCHotCredential : Credential → Epoch → Maybe Credential
getCCHotCredential c e =
if currentEpoch > e
then nothing
else case lookupᵐ? ccHotKeys c of λ where
(just (just c')) → just c'
_ → nothing
activeCC : Credential ⇀ Credential
activeCC = case proj₁ cc of λ where
(just (ccMembers , _)) → mapMaybeWithKeyᵐ getCCHotCredential ccMembers
nothing → ∅
sizeActiveCC : ℕ
sizeActiveCC = lengthˢ (dom activeCC)
actualVotes : Credential ⇀ Vote
actualVotes =
mapValues (λ hotCredential → maybe id Vote.no (lookupᵐ? castVotes hotCredential))
activeCC
mT : Maybe ℚ
mT = threshold (PParamsOf eSt) (proj₂ <$> (proj₁ cc)) action CC
stakeDistr : Credential ⇀ Coin
stakeDistr = constMap (dom actualVotes) 1
acceptedStake totalStake : Coin
acceptedStake = ∑[ x ← stakeDistr ∣ actualVotes ⁻¹ Vote.yes ] x
totalStake = ∑[ x ← stakeDistr ∣ dom (actualVotes ∣^ (❴ Vote.yes ❵ ∪ ❴ Vote.no ❵)) ] x
accepted : Type
accepted = case mT of λ where
(just t) → sizeActiveCC ≥ ccMinSize × (acceptedStake /₀ totalStake) ≥ t
nothing → ⊤
acceptedByCC : RatifyEnv → EnactState → GovActionState → Type
acceptedByCC Γ = AcceptedByCC.accepted currentEpoch ccHotKeys
where open RatifyEnv Γ using (currentEpoch; ccHotKeys)
module AcceptedByDRep (Γ : RatifyEnv)
(eSt : EnactState)
(gaSt : GovActionState)
where
open EnactState eSt using (cc)
open RatifyEnv Γ using (currentEpoch; stakeDistrVDeleg)
open GovActionState gaSt
open GovVotes votes using (gvDRep)
castVotes : VDeleg ⇀ Vote
castVotes = mapKeys vDelegCredential gvDRep
activeDReps : ℙ Credential
activeDReps = dom (activeDRepsOf Γ currentEpoch)
predeterminedDRepVotes : VDeleg ⇀ Vote
predeterminedDRepVotes = case gaType action of λ where
NoConfidence → ❴ vDelegAbstain , Vote.abstain ❵ ∪ˡ ❴ vDelegNoConfidence , Vote.yes ❵
_ → ❴ vDelegAbstain , Vote.abstain ❵ ∪ˡ ❴ vDelegNoConfidence , Vote.no ❵
defaultDRepCredentialVotes : VDeleg ⇀ Vote
defaultDRepCredentialVotes = constMap (mapˢ vDelegCredential activeDReps) Vote.no
actualVotes : VDeleg ⇀ Vote
actualVotes = castVotes ∪ˡ defaultDRepCredentialVotes
∪ˡ predeterminedDRepVotes
t : ℚ
t = maybe id 0ℚ (threshold (PParamsOf eSt) (proj₂ <$> (proj₁ cc)) action DRep)
acceptedStake totalStake : Coin
acceptedStake = ∑[ x ← stakeDistrVDeleg ∣ actualVotes ⁻¹ Vote.yes ] x
totalStake = ∑[ x ← stakeDistrVDeleg ∣ dom (actualVotes ∣^ (❴ Vote.yes ❵ ∪ ❴ Vote.no ❵)) ] x
accepted = (acceptedStake /₀ totalStake) ≥ t
acceptedByDRep : RatifyEnv → EnactState → GovActionState → Type
acceptedByDRep = AcceptedByDRep.accepted
module AcceptedBySPO (delegatees : VoteDelegs)
(pools : Pools)
(stakeDistrPools : KeyHash ⇀ Coin)
(eSt : EnactState)
(gaSt : GovActionState)
where
open EnactState eSt using (cc)
open GovActionState gaSt
open GovVotes votes using (gvSPO)
castVotes : KeyHash ⇀ Vote
castVotes = gvSPO
defaultVote : KeyHash → Vote
defaultVote kh = case lookupᵐ? pools kh of λ where
nothing → Vote.no
(just p) → case lookupᵐ? delegatees (CredentialOf (StakePoolState.rewardAccount p)) , gaType action of
λ where
( _ , TriggerHardFork ) → Vote.no
( just vDelegNoConfidence , NoConfidence ) → Vote.yes
( just vDelegAbstain , _ ) → Vote.abstain
_ → Vote.no
actualVotes : KeyHash ⇀ Vote
actualVotes = castVotes ∪ˡ mapFromFun defaultVote (dom stakeDistrPools)
t : ℚ
t = maybe id 0ℚ (threshold (PParamsOf eSt) (proj₂ <$> (proj₁ cc)) action SPO)
acceptedStake totalStake : Coin
acceptedStake = ∑[ x ← stakeDistrPools ∣ actualVotes ⁻¹ Vote.yes ] x
totalStake = ∑[ x ← stakeDistrPools ∣ dom (actualVotes ∣^ (❴ Vote.yes ❵ ∪ ❴ Vote.no ❵)) ] x
accepted : Type
accepted = (acceptedStake /₀ totalStake) ≥ t
acceptedBySPO : RatifyEnv → EnactState → GovActionState → Type
acceptedBySPO Γ = AcceptedBySPO.accepted delegatees pools stakeDistrPools
where open RatifyEnv Γ
opaque
accepted : RatifyEnv → EnactState → GovActionState → Type
accepted Γ es gs = acceptedByCC Γ es gs × acceptedByDRep Γ es gs × acceptedBySPO Γ es gs
expired : Epoch → GovActionState → Type
expired current record { expiresIn = expiresIn } = expiresIn < current
open EnactState
verifyPrev : (a : GovActionType) → NeedsHash a → EnactState → Type
verifyPrev NoConfidence h es = h ≡ es .cc .proj₂
verifyPrev UpdateCommittee h es = h ≡ es .cc .proj₂
verifyPrev NewConstitution h es = h ≡ es .constitution .proj₂
verifyPrev TriggerHardFork h es = h ≡ es .pv .proj₂
verifyPrev ChangePParams h es = h ≡ es .pparams .proj₂
verifyPrev TreasuryWithdrawal _ _ = ⊤
verifyPrev Info _ _ = ⊤
delayingAction : GovActionType → Bool
delayingAction NoConfidence = true
delayingAction UpdateCommittee = true
delayingAction NewConstitution = true
delayingAction TriggerHardFork = true
delayingAction ChangePParams = false
delayingAction TreasuryWithdrawal = false
delayingAction Info = false
delayed : (a : GovActionType) → NeedsHash a → EnactState → Bool → Type
delayed gaTy h es d = ¬ verifyPrev gaTy h es ⊎ d ≡ true
acceptConds : RatifyEnv → RatifyState → GovActionID × GovActionState → Type
acceptConds Γ stʳ (id , st) =
accepted Γ es st
× ¬ delayed (gaType action) prevAction es delay
× ∃[ es' ] $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Ratify.html#10654}{\htmlId{10750}{\htmlClass{Bound}{\text{id}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ratify.html#3523}{\htmlId{10755}{\htmlClass{Function}{\text{treasury}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ratify.html#3399}{\htmlId{10766}{\htmlClass{Function}{\text{currentEpoch}}}}\, \end{pmatrix}$ ⊢ es ⇀⦇ action ,ENACT⦈ es'
where open RatifyEnv Γ
open RatifyState stʳ
open GovActionState st
opaque
unfolding accepted
verifyPrev? : ∀ a h es → Dec (verifyPrev a h es)
verifyPrev? NoConfidence h es = dec
verifyPrev? UpdateCommittee h es = dec
verifyPrev? NewConstitution h es = dec
verifyPrev? TriggerHardFork h es = dec
verifyPrev? ChangePParams h es = dec
verifyPrev? TreasuryWithdrawal h es = dec
verifyPrev? Info h es = dec
delayed? : ∀ a h es d → Dec (delayed a h es d)
delayed? a h es d = let instance _ = ⁇ verifyPrev? a h es in dec
Is-nothing? : ∀ {A : Set} {x : Maybe A} → Dec (Is-nothing x)
Is-nothing? {x = x} = All.dec (const $ no id) x
where import Data.Maybe.Relation.Unary.All as All
Is-just? : ∀ {A : Set} {x : Maybe A} → Dec (Is-just x)
Is-just? {x = x} = Any.dec (const $ yes tt) x
where import Data.Maybe.Relation.Unary.Any as Any
acceptedByCC? : ∀ Γ es st → Dec (acceptedByCC Γ es st)
acceptedByCC? Γ es st = d
where
open RatifyEnv Γ using (currentEpoch; ccHotKeys)
module acbCC = AcceptedByCC currentEpoch ccHotKeys es st
d : Dec acbCC.accepted
d with acbCC.mT
... | just t = _ ≤? acbCC.sizeActiveCC ×-dec t ≤? _
... | nothing = yes tt
acceptedByDRep? : ∀ Γ es st → Dec (acceptedByDRep Γ es st)
acceptedByDRep? _ _ _ = _ ℚ.≤? _
acceptedBySPO? : ∀ Γ es st → Dec (acceptedBySPO Γ es st)
acceptedBySPO? _ _ _ = _ ℚ.≤? _
accepted? : ∀ Γ es st → Dec (accepted Γ es st)
accepted? Γ es st = acceptedByCC? Γ es st ×-dec acceptedByDRep? Γ es st ×-dec acceptedBySPO? Γ es st
expired? : ∀ e st → Dec (expired e st)
expired? e st = ¿ expired e st ¿
private variable
Γ : RatifyEnv
es es' : EnactState
a : GovActionID × GovActionState
removed : ℙ (GovActionID × GovActionState)
d : Bool
open RatifyEnv
open GovActionState
The RATIFY Transition System
data _⊢_⇀⦇_,RATIFY⦈_ : RatifyEnv → RatifyState → GovActionID × GovActionState → RatifyState → Type
where
RATIFY-Accept :
let treasury = TreasuryOf Γ
e = Γ .currentEpoch
(gaId , gaSt) = a
action = GovActionOf gaSt
in
∙ acceptConds Γ $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Ratify.html#12576}{\htmlId{13127}{\htmlClass{Generalizable}{\text{es}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ratify.html#12642}{\htmlId{13132}{\htmlClass{Generalizable}{\text{removed}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ratify.html#12688}{\htmlId{13142}{\htmlClass{Generalizable}{\text{d}}}}\, \end{pmatrix}$ a
∙ $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Ratify.html#13038}{\htmlId{13156}{\htmlClass{Bound}{\text{gaId}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ratify.html#12958}{\htmlId{13163}{\htmlClass{Bound}{\text{treasury}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ratify.html#12996}{\htmlId{13174}{\htmlClass{Bound}{\text{e}}}}\, \end{pmatrix}$ ⊢ es ⇀⦇ action ,ENACT⦈ es'
────────────────────────────────
Γ ⊢ $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Ratify.html#12576}{\htmlId{13256}{\htmlClass{Generalizable}{\text{es}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ratify.html#12642}{\htmlId{13261}{\htmlClass{Generalizable}{\text{removed}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ratify.html#12688}{\htmlId{13271}{\htmlClass{Generalizable}{\text{d}}}}\, \end{pmatrix}$ ⇀⦇ a ,RATIFY⦈ $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Ratify.html#12579}{\htmlId{13291}{\htmlClass{Generalizable}{\text{es'}}}}\, \\ \,\href{Class.HasSingleton.html#288}{\htmlId{13297}{\htmlClass{Field Operator}{\text{❴}}}}\, \,\href{Ledger.Dijkstra.Specification.Ratify.html#12600}{\htmlId{13299}{\htmlClass{Generalizable}{\text{a}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{13301}{\htmlClass{Field Operator}{\text{❵}}}}\, \,\href{Axiom.Set.html#9137}{\htmlId{13303}{\htmlClass{Function Operator}{\text{∪}}}}\, \,\href{Ledger.Dijkstra.Specification.Ratify.html#12642}{\htmlId{13305}{\htmlClass{Generalizable}{\text{removed}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ratify.html#10095}{\htmlId{13315}{\htmlClass{Function}{\text{delayingAction}}}}\, \,\htmlId{13330}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Dijkstra.Specification.Gov.Actions.html#1773}{\htmlId{13331}{\htmlClass{Field}{\text{gaType}}}}\, \,\href{Ledger.Dijkstra.Specification.Ratify.html#13064}{\htmlId{13338}{\htmlClass{Bound}{\text{action}}}}\,\,\htmlId{13344}{\htmlClass{Symbol}{\text{)}}}\, \end{pmatrix}$
RATIFY-Reject :
let e = Γ .currentEpoch
(gaId , gaSt) = a
in
∙ ¬ acceptConds Γ $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Ratify.html#12576}{\htmlId{13466}{\htmlClass{Generalizable}{\text{es}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ratify.html#12642}{\htmlId{13471}{\htmlClass{Generalizable}{\text{removed}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ratify.html#12688}{\htmlId{13481}{\htmlClass{Generalizable}{\text{d}}}}\, \end{pmatrix}$ a
∙ expired e gaSt
────────────────────────────────
Γ ⊢ $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Ratify.html#12576}{\htmlId{13559}{\htmlClass{Generalizable}{\text{es}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ratify.html#12642}{\htmlId{13564}{\htmlClass{Generalizable}{\text{removed}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ratify.html#12688}{\htmlId{13574}{\htmlClass{Generalizable}{\text{d}}}}\, \end{pmatrix}$ ⇀⦇ a ,RATIFY⦈ $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Ratify.html#12576}{\htmlId{13594}{\htmlClass{Generalizable}{\text{es}}}}\, \\ \,\href{Class.HasSingleton.html#288}{\htmlId{13599}{\htmlClass{Field Operator}{\text{❴}}}}\, \,\href{Ledger.Dijkstra.Specification.Ratify.html#12600}{\htmlId{13601}{\htmlClass{Generalizable}{\text{a}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{13603}{\htmlClass{Field Operator}{\text{❵}}}}\, \,\href{Axiom.Set.html#9137}{\htmlId{13605}{\htmlClass{Function Operator}{\text{∪}}}}\, \,\href{Ledger.Dijkstra.Specification.Ratify.html#12642}{\htmlId{13607}{\htmlClass{Generalizable}{\text{removed}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ratify.html#12688}{\htmlId{13617}{\htmlClass{Generalizable}{\text{d}}}}\, \end{pmatrix}$
RATIFY-Continue :
let e = Γ .currentEpoch
(gaId , gaSt) = a
in
∙ ¬ acceptConds Γ $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Ratify.html#12576}{\htmlId{13745}{\htmlClass{Generalizable}{\text{es}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ratify.html#12642}{\htmlId{13750}{\htmlClass{Generalizable}{\text{removed}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ratify.html#12688}{\htmlId{13760}{\htmlClass{Generalizable}{\text{d}}}}\, \end{pmatrix}$ a
∙ ¬ expired e gaSt
────────────────────────────────
Γ ⊢ $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Ratify.html#12576}{\htmlId{13843}{\htmlClass{Generalizable}{\text{es}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ratify.html#12642}{\htmlId{13848}{\htmlClass{Generalizable}{\text{removed}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ratify.html#12688}{\htmlId{13858}{\htmlClass{Generalizable}{\text{d}}}}\, \end{pmatrix}$ ⇀⦇ a ,RATIFY⦈ $\begin{pmatrix} \,\href{Ledger.Dijkstra.Specification.Ratify.html#12576}{\htmlId{13878}{\htmlClass{Generalizable}{\text{es}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ratify.html#12642}{\htmlId{13883}{\htmlClass{Generalizable}{\text{removed}}}}\, \\ \,\href{Ledger.Dijkstra.Specification.Ratify.html#12688}{\htmlId{13893}{\htmlClass{Generalizable}{\text{d}}}}\, \end{pmatrix}$
_⊢_⇀⦇_,RATIFIES⦈_ : RatifyEnv → RatifyState → List (GovActionID × GovActionState) → RatifyState → Type
_⊢_⇀⦇_,RATIFIES⦈_ = ReflexiveTransitiveClosure {sts = _⊢_⇀⦇_,RATIFY⦈_}