PParamsWellFormed

{-# OPTIONS --safe #-}

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

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

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

- *Informally*. We say the `PParams`{.AgdaRecord} 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. Formally,

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

This property asserts that `pp-wellFormed`{.AgdaFunction} is a chain invariant. That is, if and are chain states such that `⇀⦇`{.AgdaDatatype} `,CHAIN⦈`{.AgdaDatatype} , and if the `PParams`{.AgdaRecord} of are well-formed, then so are the `PParams`{.AgdaRecord} of . - *Formally*.

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

- *Proof*. *To appear* (in the module of the [formal ledger repository](\repourl)).