{-# 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)
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
stakeDistrVDeleg : VDeleg ⇀ Coin
stakeDistrPools : KeyHash ⇀ 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
instance
unquoteDecl HasCast-StakeDistrs HasCast-RatifyEnv HasCast-RatifyState = derive-HasCast
( (quote StakeDistrs , HasCast-StakeDistrs)
∷ (quote RatifyEnv , HasCast-RatifyEnv)
∷ [ (quote RatifyState , HasCast-RatifyState) ])
acceptedByCC
: RatifyEnv
→ EnactState
→ GovActionState
→ Type
acceptedByCC Γ eSt gaSt = (acceptedStake /₀ totalStake) ≥ t
× (maybe (λ (m , _) → lengthˢ m) 0 (proj₁ cc) ≥ ccMinSize ⊎ Is-nothing mT)
where
open EnactState eSt using (cc; pparams)
open RatifyEnv Γ
open PParams (proj₁ pparams)
open GovActionState gaSt
open GovVotes votes using (gvCC)
castVotes : Credential ⇀ Vote
castVotes = gvCC
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
actualVote : Credential → Epoch → Vote
actualVote c e = case getCCHotCred (c , e) of
λ where
(just c') → maybe id Vote.no (lookupᵐ? castVotes c')
_ → Vote.abstain
actualVotes : Credential ⇀ Vote
actualVotes = case proj₁ cc of
λ where
nothing → ∅
(just (m , _)) → if ccMinSize ≤ lengthˢ (mapFromPartialFun getCCHotCred (m ˢ))
then mapWithKey actualVote m
else constMap (dom m) Vote.no
mT : Maybe ℚ
mT = threshold (proj₁ pparams) (proj₂ <$> (proj₁ cc)) action CC
t : ℚ
t = maybe id 0ℚ mT
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
acceptedByDRep
: RatifyEnv
→ EnactState
→ GovActionState
→ Type
acceptedByDRep Γ eSt gaSt = (acceptedStake /₀ totalStake) ≥ t
where
open EnactState eSt using (cc; pparams)
open RatifyEnv Γ
open PParams (proj₁ pparams)
open StakeDistrs stakeDistrs
open GovActionState gaSt
open GovVotes votes using (gvDRep)
castVotes : VDeleg ⇀ Vote
castVotes = mapKeys vDelegCredential gvDRep
activeDReps : ℙ Credential
activeDReps = dom (filter (λ (_ , e) → currentEpoch ≤ e) dreps)
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 (proj₁ pparams) (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
acceptedBySPO
: RatifyEnv
→ EnactState
→ GovActionState
→ Type
acceptedBySPO Γ eSt gaSt = (acceptedStake /₀ totalStake) ≥ t
where
open EnactState eSt using (cc; pparams)
open RatifyEnv Γ
open StakeDistrs stakeDistrs
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 (StakePoolParams.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 (proj₁ pparams) (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
abstract
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.Conway.Specification.Ratify.html#9941}{\htmlId{10047}{\htmlClass{Bound}{\text{id}}}}\, \\ \,\href{Ledger.Conway.Specification.Ratify.html#3264}{\htmlId{10052}{\htmlClass{Function}{\text{treasury}}}}\, \\ \,\href{Ledger.Conway.Specification.Ratify.html#3149}{\htmlId{10063}{\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
accepted? : ∀ Γ es st → Dec (accepted Γ es st)
accepted? Γ es st = acceptedByCC? Γ es st ×-dec acceptedByDRep? Γ es st ×-dec acceptedBySPO? Γ es st
where
acceptedByCC? : ∀ Γ es st → Dec (acceptedByCC Γ es st)
acceptedByCC? _ _ _ = _ ℚ.≤? _ ×-dec (_ ≥? _ ⊎-dec Is-nothing?)
acceptedByDRep? : ∀ Γ es st → Dec (acceptedByDRep Γ es st)
acceptedByDRep? _ _ _ = _ ℚ.≤? _
acceptedBySPO? : ∀ Γ es st → Dec (acceptedBySPO Γ es st)
acceptedBySPO? _ _ _ = _ ℚ.≤? _
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#11476}{\htmlId{12078}{\htmlClass{Generalizable}{\text{es}}}}\, \\ \,\href{Ledger.Conway.Specification.Ratify.html#11533}{\htmlId{12083}{\htmlClass{Generalizable}{\text{removed}}}}\, \\ \,\href{Ledger.Conway.Specification.Ratify.html#11578}{\htmlId{12093}{\htmlClass{Generalizable}{\text{d}}}}\, \end{pmatrix}$ a
∙ $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Ratify.html#11989}{\htmlId{12107}{\htmlClass{Bound}{\text{gaId}}}}\, \\ \,\href{Ledger.Conway.Specification.Ratify.html#11909}{\htmlId{12114}{\htmlClass{Bound}{\text{treasury}}}}\, \\ \,\href{Ledger.Conway.Specification.Ratify.html#11947}{\htmlId{12125}{\htmlClass{Bound}{\text{e}}}}\, \end{pmatrix}$ ⊢ es ⇀⦇ action ,ENACT⦈ es'
────────────────────────────────
Γ ⊢ $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Ratify.html#11476}{\htmlId{12207}{\htmlClass{Generalizable}{\text{es}}}}\, \\ \,\href{Ledger.Conway.Specification.Ratify.html#11533}{\htmlId{12213}{\htmlClass{Generalizable}{\text{removed}}}}\, \\ \,\href{Ledger.Conway.Specification.Ratify.html#11578}{\htmlId{12231}{\htmlClass{Generalizable}{\text{d}}}}\, \end{pmatrix}$ ⇀⦇ a ,RATIFY⦈
$\begin{pmatrix} \,\href{Ledger.Conway.Specification.Ratify.html#11479}{\htmlId{12281}{\htmlClass{Generalizable}{\text{es'}}}}\, \\ \,\href{Class.HasSingleton.html#288}{\htmlId{12287}{\htmlClass{Field Operator}{\text{❴}}}}\, \,\href{Ledger.Conway.Specification.Ratify.html#11498}{\htmlId{12289}{\htmlClass{Generalizable}{\text{a}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{12291}{\htmlClass{Field Operator}{\text{❵}}}}\, \,\href{Axiom.Set.html#8952}{\htmlId{12293}{\htmlClass{Function Operator}{\text{∪}}}}\, \,\href{Ledger.Conway.Specification.Ratify.html#11533}{\htmlId{12295}{\htmlClass{Generalizable}{\text{removed}}}}\, \\ \,\href{Ledger.Conway.Specification.Ratify.html#9382}{\htmlId{12305}{\htmlClass{Function}{\text{delayingAction}}}}\, \,\htmlId{12320}{\htmlClass{Symbol}{\text{(}}}\,\,\href{Ledger.Conway.Specification.Gov.Actions.html#1981}{\htmlId{12321}{\htmlClass{Field}{\text{gaType}}}}\, \,\href{Ledger.Conway.Specification.Ratify.html#12015}{\htmlId{12328}{\htmlClass{Bound}{\text{action}}}}\,\,\htmlId{12334}{\htmlClass{Symbol}{\text{)}}}\, \end{pmatrix}$
RATIFY-Reject :
let e = Γ .currentEpoch
(gaId , gaSt) = a
in
∙ ¬ acceptConds Γ $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Ratify.html#11476}{\htmlId{12456}{\htmlClass{Generalizable}{\text{es}}}}\, \\ \,\href{Ledger.Conway.Specification.Ratify.html#11533}{\htmlId{12461}{\htmlClass{Generalizable}{\text{removed}}}}\, \\ \,\href{Ledger.Conway.Specification.Ratify.html#11578}{\htmlId{12471}{\htmlClass{Generalizable}{\text{d}}}}\, \end{pmatrix}$ a
∙ expired e gaSt
────────────────────────────────
Γ ⊢ $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Ratify.html#11476}{\htmlId{12549}{\htmlClass{Generalizable}{\text{es}}}}\, \\ \,\href{Ledger.Conway.Specification.Ratify.html#11533}{\htmlId{12554}{\htmlClass{Generalizable}{\text{removed}}}}\, \\ \,\href{Ledger.Conway.Specification.Ratify.html#11578}{\htmlId{12564}{\htmlClass{Generalizable}{\text{d}}}}\, \end{pmatrix}$ ⇀⦇ a ,RATIFY⦈ $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Ratify.html#11476}{\htmlId{12584}{\htmlClass{Generalizable}{\text{es}}}}\, \\ \,\href{Class.HasSingleton.html#288}{\htmlId{12589}{\htmlClass{Field Operator}{\text{❴}}}}\, \,\href{Ledger.Conway.Specification.Ratify.html#11498}{\htmlId{12591}{\htmlClass{Generalizable}{\text{a}}}}\, \,\href{Class.HasSingleton.html#288}{\htmlId{12593}{\htmlClass{Field Operator}{\text{❵}}}}\, \,\href{Axiom.Set.html#8952}{\htmlId{12595}{\htmlClass{Function Operator}{\text{∪}}}}\, \,\href{Ledger.Conway.Specification.Ratify.html#11533}{\htmlId{12597}{\htmlClass{Generalizable}{\text{removed}}}}\, \\ \,\href{Ledger.Conway.Specification.Ratify.html#11578}{\htmlId{12607}{\htmlClass{Generalizable}{\text{d}}}}\, \end{pmatrix}$
RATIFY-Continue :
let e = Γ .currentEpoch
(gaId , gaSt) = a
in
∙ ¬ acceptConds Γ $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Ratify.html#11476}{\htmlId{12735}{\htmlClass{Generalizable}{\text{es}}}}\, \\ \,\href{Ledger.Conway.Specification.Ratify.html#11533}{\htmlId{12740}{\htmlClass{Generalizable}{\text{removed}}}}\, \\ \,\href{Ledger.Conway.Specification.Ratify.html#11578}{\htmlId{12750}{\htmlClass{Generalizable}{\text{d}}}}\, \end{pmatrix}$ a
∙ ¬ expired e gaSt
────────────────────────────────
Γ ⊢ $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Ratify.html#11476}{\htmlId{12833}{\htmlClass{Generalizable}{\text{es}}}}\, \\ \,\href{Ledger.Conway.Specification.Ratify.html#11533}{\htmlId{12838}{\htmlClass{Generalizable}{\text{removed}}}}\, \\ \,\href{Ledger.Conway.Specification.Ratify.html#11578}{\htmlId{12848}{\htmlClass{Generalizable}{\text{d}}}}\, \end{pmatrix}$ ⇀⦇ a ,RATIFY⦈ $\begin{pmatrix} \,\href{Ledger.Conway.Specification.Ratify.html#11476}{\htmlId{12868}{\htmlClass{Generalizable}{\text{es}}}}\, \\ \,\href{Ledger.Conway.Specification.Ratify.html#11533}{\htmlId{12873}{\htmlClass{Generalizable}{\text{removed}}}}\, \\ \,\href{Ledger.Conway.Specification.Ratify.html#11578}{\htmlId{12883}{\htmlClass{Generalizable}{\text{d}}}}\, \end{pmatrix}$
_⊢_⇀⦇_,RATIFIES⦈_ = ReflexiveTransitiveClosure {sts = _⊢_⇀⦇_,RATIFY⦈_}