Protocol Parameters
This section is part of the
Ledger.Conway.PParams
module of the formal ledger
specification,
in which we define the adjustable protocol parameters of the Cardano
ledger.
Protocol parameters are used in block validation and can affect various
features of the system, such as minimum fees, maximum and minimum sizes
of certain components, and more.
{-# OPTIONS --safe #-}
open import Data.Product.Properties
open import Data.Nat.Properties using (m+1+n≢m)
open import Data.Rational using (ℚ)
open import Relation.Nullary.Decidable
open import Data.List.Relation.Unary.Any using (Any; here; there)
open import Tactic.Derive.Show
open import Ledger.Prelude
open import Ledger.Conway.Crypto
open import Ledger.Conway.Script.Base
open import Ledger.Conway.Types.Epoch
open import Ledger.Conway.Types.Numeric using (UnitInterval; ℕ⁺)
module Ledger.Conway.PParams
(crypto : Crypto )
(es : _) (open EpochStructure es)
(ss : ScriptStructure crypto es) (open ScriptStructure ss)
where
private variable
m n : ℕ
The Acnt record has two fields,
treasury and reserves, so the field in
NewEpochState keeps track of the total assets that remain
in treasury and reserves.
record Acnt : Type where
constructor ⟦_,_⟧ᵃ
field
treasury reserves : Coin
record Hastreasury {a} (A : Type a) : Type a where
field treasuryOf : A → Coin
open Hastreasury ⦃...⦄ public
record Hasreserves {a} (A : Type a) : Type a where
field reservesOf : A → Coin
open Hasreserves ⦃...⦄ public
ProtVer : Type
ProtVer = ℕ × ℕ
instance
Show-ProtVer : Show ProtVer
Show-ProtVer = Show-×
data pvCanFollow : ProtVer → ProtVer → Type where
canFollowMajor : pvCanFollow (m , n) (m + 1 , 0)
canFollowMinor : pvCanFollow (m , n) (m , n + 1)
instance
unquoteDecl HasCast-Acnt = derive-HasCast
[ (quote Acnt , HasCast-Acnt) ]
Protocol parameter group definition
data PParamGroup : Type where
NetworkGroup : PParamGroup
EconomicGroup : PParamGroup
TechnicalGroup : PParamGroup
GovernanceGroup : PParamGroup
SecurityGroup : PParamGroup
Protocol parameter threshold definitions
record DrepThresholds : Type where
field
P1 P2a P2b P3 P4 P5a P5b P5c P5d P6 : ℚ
record PoolThresholds : Type where
field
Q1 Q2a Q2b Q4 Q5 : ℚ
Protocol parameter definitions
record PParams : Type where
field
Network group
maxBlockSize : ℕ
maxTxSize : ℕ
maxHeaderSize : ℕ
maxTxExUnits : ExUnits
maxBlockExUnits : ExUnits
maxValSize : ℕ
maxCollateralInputs : ℕ
pv : ProtVer
Economic group
a : ℕ
b : ℕ
keyDeposit : Coin
poolDeposit : Coin
monetaryExpansion : UnitInterval
treasuryCut : UnitInterval
coinsPerUTxOByte : Coin
prices : Prices
minFeeRefScriptCoinsPerByte : ℚ
maxRefScriptSizePerTx : ℕ
maxRefScriptSizePerBlock : ℕ
refScriptCostStride : ℕ⁺
refScriptCostMultiplier : ℚ
minUTxOValue : Coin
Technical group
Emax : Epoch
nopt : ℕ
a0 : ℚ
collateralPercentage : ℕ
costmdls : CostModel
Governance group
poolThresholds : PoolThresholds
drepThresholds : DrepThresholds
ccMinSize : ℕ
ccMaxTermLength : ℕ
govActionLifetime : ℕ
govActionDeposit : Coin
drepDeposit : Coin
drepActivity : Epoch
Security group
maxBlockSize maxTxSize
maxHeaderSize maxValSize
maxBlockExUnits a b
minFeeRefScriptCoinsPerByte coinsPerUTxOByte
govActionDeposit
record HasPParams {a} (A : Type a) : Type a where
field PParamsOf : A → PParams
open HasPParams ⦃...⦄ public
record HasgovActionDeposit {a} (A : Type a) : Type a where
field govActionDepositOf : A → Coin
open HasgovActionDeposit ⦃...⦄ public
record HasccMaxTermLength {a} (A : Type a) : Type a where
field ccMaxTermLengthOf : A → ℕ
open HasccMaxTermLength ⦃...⦄ public
instance
HasgovActionDeposit-PParams : HasgovActionDeposit PParams
HasgovActionDeposit-PParams .govActionDepositOf = PParams.govActionDeposit
positivePParams : PParams → List ℕ
positivePParams pp = ( maxBlockSize ∷ maxTxSize ∷ maxHeaderSize
∷ maxValSize ∷ coinsPerUTxOByte
∷ poolDeposit ∷ collateralPercentage ∷ ccMaxTermLength
∷ govActionLifetime ∷ govActionDeposit ∷ drepDeposit ∷ [] )
where open PParams pp
paramsWellFormed : PParams → Type
paramsWellFormed pp = 0 ∉ fromList (positivePParams pp)
paramsWF-elim : (pp : PParams) → paramsWellFormed pp → (n : ℕ) → n ∈ˡ (positivePParams pp) → n > 0
paramsWF-elim pp pwf (suc n) x = z<s
paramsWF-elim pp pwf 0 0∈ = ⊥-elim (pwf (to ∈-fromList 0∈))
where open Equivalence
instance
unquoteDecl DecEq-DrepThresholds = derive-DecEq
((quote DrepThresholds , DecEq-DrepThresholds) ∷ [])
unquoteDecl DecEq-PoolThresholds = derive-DecEq
((quote PoolThresholds , DecEq-PoolThresholds) ∷ [])
unquoteDecl DecEq-PParams = derive-DecEq
((quote PParams , DecEq-PParams) ∷ [])
unquoteDecl DecEq-PParamGroup = derive-DecEq
((quote PParamGroup , DecEq-PParamGroup) ∷ [])
unquoteDecl Show-DrepThresholds = derive-Show
((quote DrepThresholds , Show-DrepThresholds) ∷ [])
unquoteDecl Show-PoolThresholds = derive-Show
((quote PoolThresholds , Show-PoolThresholds) ∷ [])
unquoteDecl Show-PParams = derive-Show
((quote PParams , Show-PParams) ∷ [])
module PParamsUpdate where
record PParamsUpdate : Type where
field
maxBlockSize maxTxSize : Maybe ℕ
maxHeaderSize maxValSize : Maybe ℕ
maxCollateralInputs : Maybe ℕ
maxTxExUnits maxBlockExUnits : Maybe ExUnits
pv : Maybe ProtVer
a b : Maybe ℕ
keyDeposit : Maybe Coin
poolDeposit : Maybe Coin
monetaryExpansion : Maybe UnitInterval
treasuryCut : Maybe UnitInterval
coinsPerUTxOByte : Maybe Coin
prices : Maybe Prices
minFeeRefScriptCoinsPerByte : Maybe ℚ
maxRefScriptSizePerTx : Maybe ℕ
maxRefScriptSizePerBlock : Maybe ℕ
refScriptCostStride : Maybe ℕ⁺
refScriptCostMultiplier : Maybe ℚ
minUTxOValue : Maybe Coin
a0 : Maybe ℚ
Emax : Maybe Epoch
nopt : Maybe ℕ
collateralPercentage : Maybe ℕ
costmdls : Maybe CostModel
drepThresholds : Maybe DrepThresholds
poolThresholds : Maybe PoolThresholds
govActionLifetime : Maybe ℕ
govActionDeposit drepDeposit : Maybe Coin
drepActivity : Maybe Epoch
ccMinSize ccMaxTermLength : Maybe ℕ
paramsUpdateWellFormed : PParamsUpdate → Type
paramsUpdateWellFormed ppu =
just 0 ∉ fromList ( maxBlockSize ∷ maxTxSize ∷ maxHeaderSize ∷ maxValSize
∷ coinsPerUTxOByte ∷ poolDeposit ∷ collateralPercentage ∷ ccMaxTermLength
∷ govActionLifetime ∷ govActionDeposit ∷ drepDeposit ∷ [] )
where open PParamsUpdate ppu
paramsUpdateWellFormed? : ( u : PParamsUpdate ) → Dec (paramsUpdateWellFormed u)
paramsUpdateWellFormed? u = ¿ paramsUpdateWellFormed u ¿
modifiesNetworkGroup : PParamsUpdate → Bool
modifiesNetworkGroup ppu = let open PParamsUpdate ppu in
or
( is-just maxBlockSize
∷ is-just maxTxSize
∷ is-just maxHeaderSize
∷ is-just maxValSize
∷ is-just maxCollateralInputs
∷ is-just maxTxExUnits
∷ is-just maxBlockExUnits
∷ is-just pv
∷ [])
modifiesEconomicGroup : PParamsUpdate → Bool
modifiesEconomicGroup ppu = let open PParamsUpdate ppu in
or
( is-just a
∷ is-just b
∷ is-just keyDeposit
∷ is-just poolDeposit
∷ is-just monetaryExpansion
∷ is-just treasuryCut
∷ is-just coinsPerUTxOByte
∷ is-just minFeeRefScriptCoinsPerByte
∷ is-just maxRefScriptSizePerTx
∷ is-just maxRefScriptSizePerBlock
∷ is-just refScriptCostStride
∷ is-just refScriptCostMultiplier
∷ is-just prices
∷ is-just minUTxOValue
∷ [])
modifiesTechnicalGroup : PParamsUpdate → Bool
modifiesTechnicalGroup ppu = let open PParamsUpdate ppu in
or
( is-just a0
∷ is-just Emax
∷ is-just nopt
∷ is-just collateralPercentage
∷ is-just costmdls
∷ [])
modifiesGovernanceGroup : PParamsUpdate → Bool
modifiesGovernanceGroup ppu = let open PParamsUpdate ppu in
or
( is-just drepThresholds
∷ is-just poolThresholds
∷ is-just govActionLifetime
∷ is-just govActionDeposit
∷ is-just drepDeposit
∷ is-just drepActivity
∷ is-just ccMinSize
∷ is-just ccMaxTermLength
∷ [])
modifiesSecurityGroup : PParamsUpdate → Bool
modifiesSecurityGroup ppu = let open PParamsUpdate ppu in
or
( is-just maxBlockSize
∷ is-just maxTxSize
∷ is-just maxHeaderSize
∷ is-just maxValSize
∷ is-just maxBlockExUnits
∷ is-just b
∷ is-just a
∷ is-just coinsPerUTxOByte
∷ is-just govActionDeposit
∷ is-just minFeeRefScriptCoinsPerByte
∷ []
)
modifiedUpdateGroups : PParamsUpdate → ℙ PParamGroup
modifiedUpdateGroups ppu =
( modifiesNetworkGroup ?═⇒ NetworkGroup
∪ modifiesEconomicGroup ?═⇒ EconomicGroup
∪ modifiesTechnicalGroup ?═⇒ TechnicalGroup
∪ modifiesGovernanceGroup ?═⇒ GovernanceGroup
∪ modifiesSecurityGroup ?═⇒ SecurityGroup
)
where
_?═⇒_ : (PParamsUpdate → Bool) → PParamGroup → ℙ PParamGroup
pred ?═⇒ grp = if pred ppu then ❴ grp ❵ else ∅
_?↗_ : ∀ {A : Type} → Maybe A → A → A
just x ?↗ _ = x
nothing ?↗ x = x
≡-update : ∀ {A : Type} {u : Maybe A} {p : A} {x : A} → u ?↗ p ≡ x ⇔ (u ≡ just x ⊎ (p ≡ x × u ≡ nothing))
≡-update {u} {p} {x} = mk⇔ to from
where
to : ∀ {A} {u : Maybe A} {p : A} {x : A} → u ?↗ p ≡ x → (u ≡ just x ⊎ (p ≡ x × u ≡ nothing))
to {u = just x} refl = inj₁ refl
to {u = nothing} refl = inj₂ (refl , refl)
from : ∀ {A} {u : Maybe A} {p : A} {x : A} → u ≡ just x ⊎ (p ≡ x × u ≡ nothing) → u ?↗ p ≡ x
from (inj₁ refl) = refl
from (inj₂ (refl , refl)) = refl
applyPParamsUpdate : PParams → PParamsUpdate → PParams
applyPParamsUpdate pp ppu =
record
{ maxBlockSize = U.maxBlockSize ?↗ P.maxBlockSize
; maxTxSize = U.maxTxSize ?↗ P.maxTxSize
; maxHeaderSize = U.maxHeaderSize ?↗ P.maxHeaderSize
; maxValSize = U.maxValSize ?↗ P.maxValSize
; maxCollateralInputs = U.maxCollateralInputs ?↗ P.maxCollateralInputs
; maxTxExUnits = U.maxTxExUnits ?↗ P.maxTxExUnits
; maxBlockExUnits = U.maxBlockExUnits ?↗ P.maxBlockExUnits
; pv = U.pv ?↗ P.pv
; a = U.a ?↗ P.a
; b = U.b ?↗ P.b
; keyDeposit = U.keyDeposit ?↗ P.keyDeposit
; poolDeposit = U.poolDeposit ?↗ P.poolDeposit
; monetaryExpansion = U.monetaryExpansion ?↗ P.monetaryExpansion
; treasuryCut = U.treasuryCut ?↗ P.treasuryCut
; coinsPerUTxOByte = U.coinsPerUTxOByte ?↗ P.coinsPerUTxOByte
; minFeeRefScriptCoinsPerByte = U.minFeeRefScriptCoinsPerByte ?↗ P.minFeeRefScriptCoinsPerByte
; maxRefScriptSizePerTx = U.maxRefScriptSizePerTx ?↗ P.maxRefScriptSizePerTx
; maxRefScriptSizePerBlock = U.maxRefScriptSizePerBlock ?↗ P.maxRefScriptSizePerBlock
; refScriptCostStride = U.refScriptCostStride ?↗ P.refScriptCostStride
; refScriptCostMultiplier = U.refScriptCostMultiplier ?↗ P.refScriptCostMultiplier
; prices = U.prices ?↗ P.prices
; minUTxOValue = U.minUTxOValue ?↗ P.minUTxOValue
; a0 = U.a0 ?↗ P.a0
; Emax = U.Emax ?↗ P.Emax
; nopt = U.nopt ?↗ P.nopt
; collateralPercentage = U.collateralPercentage ?↗ P.collateralPercentage
; costmdls = U.costmdls ?↗ P.costmdls
; drepThresholds = U.drepThresholds ?↗ P.drepThresholds
; poolThresholds = U.poolThresholds ?↗ P.poolThresholds
; govActionLifetime = U.govActionLifetime ?↗ P.govActionLifetime
; govActionDeposit = U.govActionDeposit ?↗ P.govActionDeposit
; drepDeposit = U.drepDeposit ?↗ P.drepDeposit
; drepActivity = U.drepActivity ?↗ P.drepActivity
; ccMinSize = U.ccMinSize ?↗ P.ccMinSize
; ccMaxTermLength = U.ccMaxTermLength ?↗ P.ccMaxTermLength
}
where
open module P = PParams pp
open module U = PParamsUpdate ppu
instance
unquoteDecl DecEq-PParamsUpdate = derive-DecEq
((quote PParamsUpdate , DecEq-PParamsUpdate) ∷ [])
PParams contains parameters used in the Cardano ledger,
which we group according to the general purpose that each parameter
serves.
-
NetworkGroup: parameters related to the
network settings;
-
EconomicGroup: parameters related to the
economic aspects of the ledger;
-
TechnicalGroup: parameters related to
technical settings;
-
GovernanceGroup: parameters related to
governance settings;
-
SecurityGroup: parameters that can impact
the security of the system.
The purpose of these groups is to determine voting thresholds for
proposals aiming to change parameters. Given a proposal to change a
certain set of parameters, we look at which groups those parameters fall
into and from this we determine the voting threshold for that proposal.
(The voting threshold calculation is described in detail in
'sec:ratification-requirements' (unresolved reference); in
particular, the definition of the threshold function
appears in
Figure 'Functions-related-to-voting'.)
The first four groups have the property that every protocol parameter is
associated to precisely one of these groups. The
SecurityGroup is special: a protocol
parameter may or may not be in the
SecurityGroup. So, each protocol parameter
belongs to at least one and at most two groups. Note that in
CIP-1694 there is no
SecurityGroup, but there is the concept of
security-relevant protocol parameters (see ). The difference between
these notions is only social, so we implement security-relevant protocol
parameters as a group.
The new protocol parameters are declared in
Figure 'Protocol-parameter-definitions'
and denote the following concepts:
-
drepThresholds: governance thresholds for ; these are
rational numbers named Pone, Ptwoa,
Ptwob, Pthree, Pfour,
Pfivea, Pfiveb, Pfivec,
Pfived, and Psix;
-
: pool-related governance thresholds; these are rational numbers named
Qone, Qtwoa, Qtwob,
Qfour and Qfive;
-
ccMinSize: minimum constitutional committee size;
-
ccMaxTermLength: maximum term limit (in epochs) of
constitutional committee members;
-
govActionLifetime: governance action expiration;
-
govActionDeposit: governance action deposit;
-
drepDeposit: DRep deposit
amount;
-
drepActivity: DRep activity
period;
-
minimumAVS: the minimum active voting threshold.
Figure 'Protocol-parameter-definitions'
also defines the function paramsWellFormed which
performs some sanity checks on protocol parameters.
Figure 'Abstract-type-for-parameter-updates' defines types
and functions to update parameters. These consist of an abstract type
UpdateT and two functions applyUpdate and
updateGroups. The type UpdateT is to be
instantiated by a type that
-
can be used to update parameters, via the function
applyUpdate
-
can be queried about what parameter groups it updates, via the
function updateGroups
An element of the type UpdateT is well formed if it
updates at least one group and applying the update preserves
well-formedness.
instance
pvCanFollow? : ∀ {pv} {pv'} → Dec (pvCanFollow pv pv')
pvCanFollow? {m , n} {pv} with pv ≟ (m + 1 , 0) | pv ≟ (m , n + 1)
... | no ¬p | no ¬p₁ = no $ λ where canFollowMajor → ¬p refl
canFollowMinor → ¬p₁ refl
... | no ¬p | yes refl = yes canFollowMinor
... | yes refl | no ¬p = yes canFollowMajor
... | yes refl | yes p = ⊥-elim $ m+1+n≢m m $ ×-≡,≡←≡ p .proj₁
Abstract type for parameter updates
record PParamsDiff : Type₁ where
field
Abstract types & functions
UpdateT : Type
applyUpdate : PParams → UpdateT → PParams
updateGroups : UpdateT → ℙ PParamGroup
⦃ ppWF? ⦄ : ∀ {u} → (∀ pp → paramsWellFormed pp → paramsWellFormed (applyUpdate pp u)) ⁇
Well-formedness condition
ppdWellFormed : UpdateT → Type
ppdWellFormed u = updateGroups u ≢ ∅
× ∀ pp → paramsWellFormed pp → paramsWellFormed (applyUpdate pp u)
record GovParams : Type₁ where
field ppUpd : PParamsDiff
open PParamsDiff ppUpd renaming (UpdateT to PParamsUpdate) public
field ⦃ DecEq-UpdT ⦄ : DecEq PParamsUpdate