PParamsWellFormed

{-# OPTIONS --safe #-}

open import Ledger.Conway.Specification.Abstract
open import Ledger.Conway.Specification.Transaction

module Ledger.Conway.Specification.Chain.Properties.PParamsWellFormed
  (txs : _) (open TransactionStructure txs)
  (abs : AbstractFunctions txs)
  where

open import Ledger.Conway.Specification.Chain txs abs
open import Ledger.Prelude

Claim (Well-formedness of PParams is a CHAIN invariant).

Informally.

We say the PParams of a chain state are well-formed if each of the following parameters is non-zero: maxBlockSize, maxTxSize, maxHeaderSize, maxValSize, refScriptCostStride, coinsPerUTxOByte, poolDeposit, collateralPercentage, ccMaxTermLength, govActionLifetime, govActionDeposit, drepDeposit.

We claim that pp-wellFormed is a chain invariant. That is, if cs and cs' are chain states such that cs ⇀⦇ tx ,CHAIN⦈ cs', and if the PParams of cs are well-formed, then so are the PParams of cs' .

Formally.

pp-wellFormed : ChainState → Type
pp-wellFormed = paramsWellFormed ∘ PParamsOf

pp-wellFormed-invariant : Type
pp-wellFormed-invariant = LedgerInvariant _⊢_⇀⦇_,CHAIN⦈_ pp-wellFormed

Proof. (coming soon)