Synchronize local copy of PParams with the ledger spec

Author: javierdiaz72

docs/agda-spec/src/Ledger/PParams.lagda

@@ -10,6 +10,7 @@ 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.DecEq
 open import Tactic.Derive.Show
@@ -116,6 +117,10 @@ record PParams : Type where
         coinsPerUTxOByte              : Coin
         prices                        : Prices
         minFeeRefScriptCoinsPerByte   : ℚ
+        maxRefScriptSizePerTx         : ℕ
+        maxRefScriptSizePerBlock      : ℕ
+        refScriptCostStride           : ℕ
+        refScriptCostMultiplier       : ℚ
 \end{code}
 \begin{code}[hide]
         minUTxOValue                  : Coin -- retired, keep for now
@@ -149,14 +154,31 @@ record PParams : Type where
 \label{fig:protocol-parameter-declarations}
 \end{figure*}
 \begin{figure*}
+\begin{AgdaMultiCode}
 \begin{code}
-paramsWellFormed : PParams → Type
-paramsWellFormed pp =
-     0 ∉ fromList  ( maxBlockSize ∷ maxTxSize ∷ maxHeaderSize ∷ maxValSize
-                   ∷ minUTxOValue ∷ poolDeposit ∷ collateralPercentage ∷ ccMaxTermLength
-                   ∷ govActionLifetime ∷ govActionDeposit ∷ drepDeposit ∷ [] )
+positivePParams : PParams → List ℕ
+positivePParams pp =  ( maxBlockSize ∷ maxTxSize ∷ maxHeaderSize ∷ maxValSize ∷ refScriptCostStride
+                      ∷ coinsPerUTxOByte ∷ poolDeposit ∷ collateralPercentage ∷ ccMaxTermLength
+                      ∷ govActionLifetime ∷ govActionDeposit ∷ drepDeposit ∷ [] )
+\end{code}
+\begin{code}[hide]
   where open PParams pp
 \end{code}
+\begin{code}
+
+paramsWellFormed : PParams → Type
+paramsWellFormed pp = 0 ∉ fromList (positivePParams pp)
+\end{code}
+\begin{code}[hide]
+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
+
+refScriptCostStride>0 : (pp : PParams) → paramsWellFormed pp → (PParams.refScriptCostStride pp) > 0
+refScriptCostStride>0 pp pwf = paramsWF-elim pp pwf (PParams.refScriptCostStride pp) (there (there (there (there (here refl)))))
+\end{code}
+\end{AgdaMultiCode}
 \caption{Protocol parameter well-formedness}
 \label{fig:protocol-parameter-well-formedness}
 \end{figure*}
@@ -191,8 +213,12 @@ module PParamsUpdate where
           keyDeposit                    : Maybe Coin
           poolDeposit                   : Maybe Coin
           coinsPerUTxOByte              : Maybe Coin
-          minFeeRefScriptCoinsPerByte   : Maybe ℚ
           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
@@ -209,7 +235,7 @@ module PParamsUpdate where
   paramsUpdateWellFormed : PParamsUpdate → Type
   paramsUpdateWellFormed ppu =
        just 0 ∉ fromList ( maxBlockSize ∷ maxTxSize ∷ maxHeaderSize ∷ maxValSize
-                         ∷ minUTxOValue ∷ poolDeposit ∷ collateralPercentage ∷ ccMaxTermLength
+                         ∷ coinsPerUTxOByte ∷ poolDeposit ∷ collateralPercentage ∷ ccMaxTermLength
                          ∷ govActionLifetime ∷ govActionDeposit ∷ drepDeposit ∷ [] )
     where open PParamsUpdate ppu
 
@@ -238,6 +264,10 @@ module PParamsUpdate where
       ∷ is-just poolDeposit
       ∷ is-just coinsPerUTxOByte
       ∷ is-just minFeeRefScriptCoinsPerByte
+      ∷ is-just maxRefScriptSizePerTx
+      ∷ is-just maxRefScriptSizePerBlock
+      ∷ is-just refScriptCostStride
+      ∷ is-just refScriptCostMultiplier
       ∷ is-just prices
       ∷ is-just minUTxOValue
       ∷ [])
@@ -308,6 +338,10 @@ module PParamsUpdate where
       ; poolDeposit                 = U.poolDeposit ?↗ P.poolDeposit
       ; 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
@@ -331,7 +365,6 @@ module PParamsUpdate where
   instance
     unquoteDecl DecEq-PParamsUpdate  = derive-DecEq
       ((quote PParamsUpdate , DecEq-PParamsUpdate) ∷ [])
-
 \end{code}
 % Retiring ProtVer's documentation since ProtVer is retired.
 % \ProtVer represents the protocol version used in the Cardano ledger.
@@ -432,4 +465,5 @@ record GovParams : Type₁ where
   field ppHashingScheme : isHashableSet PParams
   open isHashableSet ppHashingScheme renaming (THash to PPHash) public
   field ⦃ DecEq-UpdT ⦄ : DecEq PParamsUpdate
+--         ⦃ Show-UpdT ⦄ : Show PParamsUpdate
 \end{code}