{-# OPTIONS --safe #-}
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.Conway.Specification.Transaction hiding (Vote)
module Ledger.Conway.Specification.Ratify (txs : _) (open TransactionStructure txs) where
open import Ledger.Conway.Specification.Certs govStructure
open import Ledger.Conway.Specification.Enact govStructure
open import Ledger.Conway.Specification.Gov.Actions govStructure using (Vote)
infixr 2 _∧_
_∧_ = _×_
instance
_ = +-0-commutativeMonoid
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₃ }
vote : ℚ → Maybe ℚ
vote = just
defer : ℚ
defer = ℚ.1ℚ ℚ.+ ℚ.1ℚ
maxThreshold : ℙ (Maybe ℚ) → Maybe ℚ
maxThreshold x = foldl comb nothing (proj₁ $ finiteness x)
where
comb : Maybe ℚ → Maybe ℚ → Maybe ℚ
comb (just x) (just y) = just (x ⊔ y)
comb (just x) nothing = just x
comb nothing (just y) = just y
comb nothing nothing = nothing
─ : Maybe ℚ
─ = nothing
✓† = vote defer
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 , x) → ∣ ✓ ∥ P/Q5 x ∣
(TreasuryWithdrawal , _) → ∣ ✓ ∣ vote P6 ∣ ─ ∣
(Info , _) → ∣ ✓† ∣ ✓† ∣ ✓† ∣
where
open PParams pp
open DrepThresholds drepThresholds
open PoolThresholds poolThresholds
✓ = maybe just ✓† ccThreshold
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 StakeDistrs : Type where
field
stakeDistr : VDeleg ⇀ Coin
record RatifyEnv : Type where
field
stakeDistrs : StakeDistrs
currentEpoch : Epoch
dreps : Credential ⇀ Epoch
ccHotKeys : Credential ⇀ Maybe Credential
treasury : Treasury
pools : KeyHash ⇀ StakePoolParams
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
HasTreasury-RatifyEnv : HasTreasury RatifyEnv
HasTreasury-RatifyEnv .TreasuryOf = RatifyEnv.treasury
CCData : Type
CCData = Maybe ((Credential ⇀ Epoch) × ℚ)
govRole : VDeleg → GovRole
govRole (credVoter gv _) = gv
govRole abstainRep = DRep
govRole noConfidenceRep = DRep
IsCC IsDRep IsSPO : VDeleg → Type
IsCC v = govRole v ≡ CC
IsDRep v = govRole v ≡ DRep
IsSPO v = govRole v ≡ SPO
instance
unquoteDecl HasCast-RatifyState = derive-HasCast
[ (quote RatifyState , HasCast-RatifyState) ]
open StakeDistrs
actualVotes : RatifyEnv → PParams → CCData → GovActionType
→ (GovRole × Credential ⇀ Vote) → (VDeleg ⇀ Vote)
actualVotes Γ pparams cc gaTy votes
= mapKeys (credVoter CC) actualCCVotes ∪ˡ actualPDRepVotes gaTy
∪ˡ actualDRepVotes ∪ˡ actualSPOVotes gaTy
where
open RatifyEnv Γ
open PParams pparams
roleVotes : GovRole → VDeleg ⇀ Vote
roleVotes r = mapKeys (uncurry credVoter) (filter (λ (x , _) → r ≡ proj₁ x) votes)
activeDReps = dom (filter (λ (_ , e) → currentEpoch ≤ e) dreps)
spos = filterˢ IsSPO (dom (stakeDistr stakeDistrs))
getCCHotCred : Credential × Epoch → Maybe Credential
getCCHotCred (c , e) = if currentEpoch > e then nothing
else case lookupᵐ? ccHotKeys c of
λ where
(just (just c')) → just c'
_ → nothing
SPODefaultVote : GovActionType → VDeleg → Vote
SPODefaultVote gaT (credVoter SPO (KeyHashObj kh)) = case lookupᵐ? pools kh of
λ where
nothing → Vote.no
(just p) → case lookupᵐ? delegatees (StakePoolParams.rewardAccount p) , gaTy of
λ where
(_ , TriggerHardFork) → Vote.no
(just noConfidenceRep , NoConfidence) → Vote.yes
(just abstainRep , _ ) → Vote.abstain
_ → Vote.no
SPODefaultVote _ _ = Vote.no
actualCCVote : Credential → Epoch → Vote
actualCCVote c e = case getCCHotCred (c , e) of
λ where
(just c') → maybe id Vote.no (lookupᵐ? votes (CC , c'))
_ → Vote.abstain
actualCCVotes : Credential ⇀ Vote
actualCCVotes = case cc of
λ where
nothing → ∅
(just (m , q)) → if ccMinSize ≤ lengthˢ (mapFromPartialFun getCCHotCred (m ˢ))
then mapWithKey actualCCVote m
else constMap (dom m) Vote.no
actualPDRepVotes : GovActionType → VDeleg ⇀ Vote
actualPDRepVotes NoConfidence
= ❴ abstainRep , Vote.abstain ❵ ∪ˡ ❴ noConfidenceRep , Vote.yes ❵
actualPDRepVotes _ = ❴ abstainRep , Vote.abstain ❵ ∪ˡ ❴ noConfidenceRep , Vote.no ❵
actualDRepVotes : VDeleg ⇀ Vote
actualDRepVotes = roleVotes DRep
∪ˡ constMap (mapˢ (credVoter DRep) activeDReps) Vote.no
actualSPOVotes : GovActionType → VDeleg ⇀ Vote
actualSPOVotes gaTy = roleVotes SPO ∪ˡ mapFromFun (SPODefaultVote gaTy) spos
open RatifyEnv using (stakeDistrs)
abstract
getStakeDist : GovRole → ℙ VDeleg → StakeDistrs → VDeleg ⇀ Coin
getStakeDist CC cc sd = constMap (filterˢ IsCC cc) 1
getStakeDist DRep _ sd = filterKeys IsDRep (sd .stakeDistr)
getStakeDist SPO _ sd = filterKeys IsSPO (sd .stakeDistr)
acceptedStakeRatio : GovRole → ℙ VDeleg → StakeDistrs → (VDeleg ⇀ Vote) → ℚ
acceptedStakeRatio r cc dists votes = acceptedStake /₀ totalStake
where
dist : VDeleg ⇀ Coin
dist = getStakeDist r cc dists
acceptedStake totalStake : Coin
acceptedStake = ∑[ x ← dist ∣ votes ⁻¹ Vote.yes ] x
totalStake = ∑[ x ← dist ∣ dom (votes ∣^ (❴ Vote.yes ❵ ∪ ❴ Vote.no ❵)) ] x
acceptedBy : RatifyEnv → EnactState → GovActionState → GovRole → Type
acceptedBy Γ (record { cc = cc , _; pparams = pparams , _ }) gs role =
let open GovActionState gs; open PParams pparams
votes' = actualVotes Γ pparams cc (gaType action) votes
mbyT = threshold pparams (proj₂ <$> cc) action role
t = maybe id 0ℚ mbyT
in acceptedStakeRatio role (dom votes') (stakeDistrs Γ) votes' ≥ t
∧ (role ≡ CC → maybe (λ (m , _) → lengthˢ m) 0 cc ≥ ccMinSize ⊎ Is-nothing mbyT)
accepted : RatifyEnv → EnactState → GovActionState → Type
accepted Γ es gs = acceptedBy Γ es gs CC ∧ acceptedBy Γ es gs DRep ∧ acceptedBy Γ es gs SPO
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.Conway.Specification.Ratify.html#9738}{\htmlId{9844}{\htmlClass{Bound}{\text{id}}}}\, \\ \,\href{Ledger.Conway.Specification.Ratify.html#3280}{\htmlId{9849}{\htmlClass{Function}{\text{treasury}}}}\, \\ \,\href{Ledger.Conway.Specification.Ratify.html#3165}{\htmlId{9860}{\htmlClass{Function}{\text{currentEpoch}}}}\, \end{pmatrix}$ ⊢ es ⇀⦇ action ,ENACT⦈ es'
where open RatifyEnv Γ
open RatifyState stʳ
open GovActionState st
abstract
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
acceptedBy? : ∀ Γ es st role → Dec (acceptedBy Γ es st role)
acceptedBy? _ _ _ _ = _ ℚ.≤? _ ×-dec _ ≟ _ →-dec (_ ≥? _ ⊎-dec Is-nothing?)
where
import Relation.Nullary.Decidable as Dec
accepted? : ∀ Γ es st → Dec (accepted Γ es st)
accepted? Γ es st = let a = λ {x} → acceptedBy? Γ es st x in a ×-dec a ×-dec a
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
data
_⊢_⇀⦇_,RATIFY⦈_ : RatifyEnv → RatifyState → GovActionID × GovActionState → RatifyState → Type
_⊢_⇀⦇_,RATIFIES⦈_ : RatifyEnv → RatifyState → List (GovActionID × GovActionState)
→ RatifyState → Type
data _⊢_⇀⦇_,RATIFY⦈_ where
RATIFY-Accept :
let treasury = TreasuryOf Γ
e = Γ .currentEpoch
(gaId , gaSt) = a
action = GovActionOf gaSt
in
∙ acceptConds Γ $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Ratify.html#11107}{\htmlId{11709}{\htmlClass{Generalizable}{\text{es}}}}\, \\ \,\href{Ledger.Conway.Specification.Ratify.html#11164}{\htmlId{11714}{\htmlClass{Generalizable}{\text{removed}}}}\, \\ \,\href{Ledger.Conway.Specification.Ratify.html#11209}{\htmlId{11724}{\htmlClass{Generalizable}{\text{d}}}}\, \end{pmatrix}$ a
∙ $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Ratify.html#11620}{\htmlId{11738}{\htmlClass{Bound}{\text{gaId}}}}\, \\ \,\href{Ledger.Conway.Specification.Ratify.html#11540}{\htmlId{11745}{\htmlClass{Bound}{\text{treasury}}}}\, \\ \,\href{Ledger.Conway.Specification.Ratify.html#11578}{\htmlId{11756}{\htmlClass{Bound}{\text{e}}}}\, \end{pmatrix}$ ⊢ es ⇀⦇ action ,ENACT⦈ es'
────────────────────────────────
Γ ⊢ $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Ratify.html#11107}{\htmlId{11838}{\htmlClass{Generalizable}{\text{es}}}}\, \\ \,\href{Ledger.Conway.Specification.Ratify.html#11164}{\htmlId{11844}{\htmlClass{Generalizable}{\text{removed}}}}\, \\ \,\href{Ledger.Conway.Specification.Ratify.html#11209}{\htmlId{11862}{\htmlClass{Generalizable}{\text{d}}}}\, \end{pmatrix}$ ⇀⦇ a ,RATIFY⦈
$\begin{pmatrix} \,\href{Ledger.Conway.Specification.Ratify.html#11110}{\htmlId{11912}{\htmlClass{Generalizable}{\text{es'}}}}\, \\ \,\href{Class.HasSingleton.html#288}{\htmlId{11918}{\htmlClass{Field Operator}{\text{❴}}}}\, \,\href{Ledger.Conway.Specification.Ratify.html#11129}{\htmlId{11920}{\htmlClass{Generalizable}{\text{a}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{11922}{\htmlClass{Field Operator}{\text{❵}}}}\, \,\href{Axiom.Set.html#8952}{\htmlId{11924}{\htmlClass{Function Operator}{\text{∪}}}}\, \,\href{Ledger.Conway.Specification.Ratify.html#11164}{\htmlId{11926}{\htmlClass{Generalizable}{\text{removed}}}}\, \\ \,\href{Ledger.Conway.Specification.Ratify.html#9179}{\htmlId{11936}{\htmlClass{Function}{\text{delayingAction}}}}\, \,\htmlId{11951}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Conway.Specification.Gov.Actions.html#1793}{\htmlId{11952}{\htmlClass{Field}{\text{gaType}}}}\, \,\href{Ledger.Conway.Specification.Ratify.html#11646}{\htmlId{11959}{\htmlClass{Bound}{\text{action}}}}\,\,\htmlId{11965}{\htmlClass{Symbol}{\text{)}}}\, \end{pmatrix}$
RATIFY-Reject :
let e = Γ .currentEpoch
(gaId , gaSt) = a
in
∙ ¬ acceptConds Γ $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Ratify.html#11107}{\htmlId{12087}{\htmlClass{Generalizable}{\text{es}}}}\, \\ \,\href{Ledger.Conway.Specification.Ratify.html#11164}{\htmlId{12092}{\htmlClass{Generalizable}{\text{removed}}}}\, \\ \,\href{Ledger.Conway.Specification.Ratify.html#11209}{\htmlId{12102}{\htmlClass{Generalizable}{\text{d}}}}\, \end{pmatrix}$ a
∙ expired e gaSt
────────────────────────────────
Γ ⊢ $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Ratify.html#11107}{\htmlId{12180}{\htmlClass{Generalizable}{\text{es}}}}\, \\ \,\href{Ledger.Conway.Specification.Ratify.html#11164}{\htmlId{12185}{\htmlClass{Generalizable}{\text{removed}}}}\, \\ \,\href{Ledger.Conway.Specification.Ratify.html#11209}{\htmlId{12195}{\htmlClass{Generalizable}{\text{d}}}}\, \end{pmatrix}$ ⇀⦇ a ,RATIFY⦈ $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Ratify.html#11107}{\htmlId{12215}{\htmlClass{Generalizable}{\text{es}}}}\, \\ \,\href{Class.HasSingleton.html#288}{\htmlId{12220}{\htmlClass{Field Operator}{\text{❴}}}}\, \,\href{Ledger.Conway.Specification.Ratify.html#11129}{\htmlId{12222}{\htmlClass{Generalizable}{\text{a}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{12224}{\htmlClass{Field Operator}{\text{❵}}}}\, \,\href{Axiom.Set.html#8952}{\htmlId{12226}{\htmlClass{Function Operator}{\text{∪}}}}\, \,\href{Ledger.Conway.Specification.Ratify.html#11164}{\htmlId{12228}{\htmlClass{Generalizable}{\text{removed}}}}\, \\ \,\href{Ledger.Conway.Specification.Ratify.html#11209}{\htmlId{12238}{\htmlClass{Generalizable}{\text{d}}}}\, \end{pmatrix}$
RATIFY-Continue :
let e = Γ .currentEpoch
(gaId , gaSt) = a
in
∙ ¬ acceptConds Γ $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Ratify.html#11107}{\htmlId{12366}{\htmlClass{Generalizable}{\text{es}}}}\, \\ \,\href{Ledger.Conway.Specification.Ratify.html#11164}{\htmlId{12371}{\htmlClass{Generalizable}{\text{removed}}}}\, \\ \,\href{Ledger.Conway.Specification.Ratify.html#11209}{\htmlId{12381}{\htmlClass{Generalizable}{\text{d}}}}\, \end{pmatrix}$ a
∙ ¬ expired e gaSt
────────────────────────────────
Γ ⊢ $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Ratify.html#11107}{\htmlId{12464}{\htmlClass{Generalizable}{\text{es}}}}\, \\ \,\href{Ledger.Conway.Specification.Ratify.html#11164}{\htmlId{12469}{\htmlClass{Generalizable}{\text{removed}}}}\, \\ \,\href{Ledger.Conway.Specification.Ratify.html#11209}{\htmlId{12479}{\htmlClass{Generalizable}{\text{d}}}}\, \end{pmatrix}$ ⇀⦇ a ,RATIFY⦈ $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Ratify.html#11107}{\htmlId{12499}{\htmlClass{Generalizable}{\text{es}}}}\, \\ \,\href{Ledger.Conway.Specification.Ratify.html#11164}{\htmlId{12504}{\htmlClass{Generalizable}{\text{removed}}}}\, \\ \,\href{Ledger.Conway.Specification.Ratify.html#11209}{\htmlId{12514}{\htmlClass{Generalizable}{\text{d}}}}\, \end{pmatrix}$
_⊢_⇀⦇_,RATIFIES⦈_ = ReflexiveTransitiveClosure {sts = _⊢_⇀⦇_,RATIFY⦈_}