Protocol Parameters¶

This section defines the adjustable protocol parameters of the Cardano ledger.

{-# OPTIONS --safe #-}

open import Ledger.Prelude
open import Ledger.Core.Specification.Crypto using (CryptoStructure)
open import Ledger.Core.Specification.Epoch using (EpochStructure)
open import Ledger.Core.Specification.ProtocolVersion
open import Ledger.Dijkstra.Specification.Script.Base

module Ledger.Dijkstra.Specification.PParams
  (cs : CryptoStructure )
  (es : EpochStructure) (open EpochStructure es)
  (Network : Type) ( DecEq-Network : DecEq Network )
  (ss : ScriptStructure cs es Network DecEq-Network) (open ScriptStructure ss)
  where

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.Core.Specification.Crypto
open import Ledger.Core.Specification.Epoch
-- open import Ledger.Dijkstra.Specification.Script.Base
open import Ledger.Prelude.Numeric using (UnitInterval; ℕ⁺)


private variable
  m n : ℕ

Protocol Parameter Definitions¶

record Acnt : Type where
  constructor ⟦_,_⟧ᵃ
  field
    treasury reserves : Coin

record HasAccount {a} (A : Type a) : Type a where
  field AccountOf : A → Acnt
open HasAccount ⦃...⦄ public

instance
  HasTreasury-Acnt : HasTreasury Acnt
  HasTreasury-Acnt .TreasuryOf = Acnt.treasury

  HasReserves-Acnt : HasReserves Acnt
  HasReserves-Acnt .ReservesOf = Acnt.reserves

  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 Declarations¶

record PParams : Type where
  field

    -- Network group
    maxBlockSize                  : ℕ
    maxTxSize                     : ℕ
    maxHeaderSize                 : ℕ
    maxTxExUnits                  : ExUnits
    maxBlockExUnits               : ExUnits
    maxValSize                    : ℕ
    maxCollateralInputs           : ℕ
    pv                            : ProtVer -- retired, keep for now

    -- Network group (Leios)
    leiosHeaderPeriod             : Milliseconds
    leiosVotingPeriod             : Milliseconds
    leiosDiffusionPeriod          : Milliseconds
    leiosMaxEBSize                : ℕ
    leiosMaxEBTxsSize             : ℕ
    leiosCommitteeSize            : ℕ
    leiosQuorumStakeThreshold     : UnitInterval
    leiosMaxEBExUnits             : ExUnits
    leiosMaxRefScriptSizePerEB    : ℕ

    -- Economic group
    a                             : ℕ
    b                             : ℕ
    keyDeposit                    : Coin
    poolDeposit                   : Coin
    minPoolCost                   : Coin
    monetaryExpansion             : UnitInterval -- formerly: rho
    treasuryCut                   : UnitInterval -- formerly: tau
    coinsPerUTxOByte              : Coin
    prices                        : Prices
    minFeeRefScriptCoinsPerByte   : ℚ
    maxRefScriptSizePerTx         : ℕ
    maxRefScriptSizePerBlock      : ℕ
    refScriptCostStride           : ℕ⁺
    refScriptCostMultiplier       : ℚ
    minUTxOValue                  : Coin -- retired, keep for now

    -- Technical group
    Emax                          : Epoch
    nopt                          : ℕ
    a0                            : ℚ
    collateralPercentage          : ℕ
    -- use an association list instead of a map for DecEq
    costmdlsAssoc                 : LanguageCostModels

    -- Governance group
    poolThresholds                : PoolThresholds
    drepThresholds                : DrepThresholds
    ccMinSize                     : ℕ
    ccMaxTermLength               : ℕ
    govActionLifetime             : ℕ
    govActionDeposit              : Coin
    drepDeposit                   : Coin
    drepActivity                  : Epoch

  costmdls : Language ⇀ CostModel
  costmdls = fromListᵐ (languageCostModels costmdlsAssoc)

Leios parameters

Leios adds the endorser block (EB), an ordered list of transaction references that a block producer announces alongside its ranking block; a committee of stake pools votes on the EB, and a certificate carried by the following ranking block brings the referenced transactions into the ledger. Three of the nine parameters measure a Leios round in wall-clock time (header diffusion, voting, and the additional diffusion that follows voting), four bound an EB (its reference list, the transactions listed, their script execution, and their reference scripts), leiosCommitteeSize (N_c) is the number of committee seats — the committee being the N_c pools with the most active stake — leiosQuorumStakeThreshold (τ) is the fraction of the total active stake a certificate's signers must carry. The voting key age bound is not a parameter: it is derived from the KES setup (maxKeyAgeEpochs in the Epoch module). The ranking block keeps its existing bound maxBlockSize, so Leios adds no field for it. Zero-valued Leios parameters are meaningful: they are the protocol's disabled state during rollout.

Security group

maxBlockSize maxTxSize maxHeaderSize maxValSize maxBlockExUnits a b minFeeRefScriptCoinsPerByte coinsPerUTxOByte govActionDeposit leiosHeaderPeriod leiosVotingPeriod leiosDiffusionPeriod leiosMaxEBSize leiosMaxEBTxsSize leiosCommitteeSize leiosQuorumStakeThreshold leiosMaxEBExUnits leiosMaxRefScriptSizePerEB

Protocol Parameter Well Formedness¶

The Leios parameters are deliberately absent from positivePParams: zero values are the protocol's disabled state, and governance must be able to reach it. CIP-164's quorum constraint τ < σ(N_c) relates the threshold to the stake coverage of the selected committee, a property of the stake distribution rather than of the parameters, so it cannot be imposed here.

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

record HasPParams {a} (A : Type a) : Type a where
  field PParamsOf : A → PParams
open HasPParams ⦃...⦄ public

record HasCCMaxTermLength {a} (A : Type a) : Type a where
  field CCMaxTermLengthOf : A → ℕ
open HasCCMaxTermLength ⦃...⦄ public

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 -- retired, keep for now
          leiosHeaderPeriod             : Maybe Milliseconds
          leiosVotingPeriod             : Maybe Milliseconds
          leiosDiffusionPeriod          : Maybe Milliseconds
          leiosMaxEBSize                : Maybe ℕ
          leiosMaxEBTxsSize             : Maybe ℕ
          leiosCommitteeSize            : Maybe ℕ
          leiosQuorumStakeThreshold     : Maybe UnitInterval
          leiosMaxEBExUnits             : Maybe ExUnits
          leiosMaxRefScriptSizePerEB    : Maybe ℕ
          a b                           : Maybe ℕ
          keyDeposit                    : Maybe Coin
          poolDeposit                   : Maybe Coin
          minPoolCost                   : 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 -- retired, keep for now
          a0                            : Maybe ℚ
          Emax                          : Maybe Epoch
          nopt                          : Maybe ℕ
          collateralPercentage          : Maybe ℕ
          costmdls                      : Maybe LanguageCostModels
          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
      ∷ is-just leiosHeaderPeriod
      ∷ is-just leiosVotingPeriod
      ∷ is-just leiosDiffusionPeriod
      ∷ is-just leiosMaxEBSize
      ∷ is-just leiosMaxEBTxsSize
      ∷ is-just leiosCommitteeSize
      ∷ is-just leiosQuorumStakeThreshold
      ∷ is-just leiosMaxEBExUnits
      ∷ is-just leiosMaxRefScriptSizePerEB
      ∷ [])

  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 minPoolCost
      ∷ 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
      ∷ is-just leiosHeaderPeriod
      ∷ is-just leiosVotingPeriod
      ∷ is-just leiosDiffusionPeriod
      ∷ is-just leiosMaxEBSize
      ∷ is-just leiosMaxEBTxsSize
      ∷ is-just leiosCommitteeSize
      ∷ is-just leiosQuorumStakeThreshold
      ∷ is-just leiosMaxEBExUnits
      ∷ is-just leiosMaxRefScriptSizePerEB
      ∷ []
      )

  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

  _∪ˡᶜᵐ_ : LanguageCostModels → LanguageCostModels → LanguageCostModels
  l ∪ˡᶜᵐ l' = mkLanguageCostModels (setToList (fromListᵐ (languageCostModels l ++ languageCostModels l') ˢ))

  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
      ; leiosHeaderPeriod           = U.leiosHeaderPeriod ?↗ P.leiosHeaderPeriod
      ; leiosVotingPeriod           = U.leiosVotingPeriod ?↗ P.leiosVotingPeriod
      ; leiosDiffusionPeriod        = U.leiosDiffusionPeriod ?↗ P.leiosDiffusionPeriod
      ; leiosMaxEBSize              = U.leiosMaxEBSize ?↗ P.leiosMaxEBSize
      ; leiosMaxEBTxsSize           = U.leiosMaxEBTxsSize ?↗ P.leiosMaxEBTxsSize
      ; leiosCommitteeSize          = U.leiosCommitteeSize ?↗ P.leiosCommitteeSize
      ; leiosQuorumStakeThreshold   = U.leiosQuorumStakeThreshold ?↗ P.leiosQuorumStakeThreshold
      ; leiosMaxEBExUnits           = U.leiosMaxEBExUnits ?↗ P.leiosMaxEBExUnits
      ; leiosMaxRefScriptSizePerEB  = U.leiosMaxRefScriptSizePerEB ?↗ P.leiosMaxRefScriptSizePerEB
      ; a                           = U.a ?↗ P.a
      ; b                           = U.b ?↗ P.b
      ; keyDeposit                  = U.keyDeposit ?↗ P.keyDeposit
      ; poolDeposit                 = U.poolDeposit ?↗ P.poolDeposit
      ; minPoolCost                 = U.minPoolCost ?↗ P.minPoolCost
      ; 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
      ; costmdlsAssoc               = if U.costmdls then (λ {cm} → cm ∪ˡᶜᵐ P.costmdlsAssoc)
                                                    else P.costmdlsAssoc
      ; 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) ∷ [])

Abstract Type for Parameter Updates¶

record PParamsDiff : Type₁ where
  field
    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
--         ⦃ Show-UpdT ⦄ : Show PParamsUpdate

References¶

[CKB+23] Jared Corduan and Andre Knispel and Matthias Benkort and Kevin Hammond and Charles Hoskinson and Samuel Leathers. A First Step Towards On-Chain Decentralized Governance. 2023.