From 31a523f3f05163841cc7668f7a6b8a1201040847 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Joosep=20J=C3=A4=C3=A4ger?= Date: Thu, 6 Jun 2024 16:05:44 +0000 Subject: [PATCH] Add PParamsUpdate (#443) --- src/Ledger/Foreign/HSLedger/BaseTypes.agda | 63 +++++++- src/Ledger/Foreign/HSLedger/Core.agda | 33 +++- src/Ledger/Foreign/LedgerTypes.agda | 166 ++++++++++++------- src/Ledger/PParams.lagda | 175 +++++++++++++++++++-- src/Ledger/hs-src/test/UtxowSpec.hs | 24 +-- 5 files changed, 379 insertions(+), 82 deletions(-) diff --git a/src/Ledger/Foreign/HSLedger/BaseTypes.agda b/src/Ledger/Foreign/HSLedger/BaseTypes.agda index aba7a0b28..975c9c92c 100644 --- a/src/Ledger/Foreign/HSLedger/BaseTypes.agda +++ b/src/Ledger/Foreign/HSLedger/BaseTypes.agda @@ -155,7 +155,68 @@ instance Convertible-RwdAddr = autoConvertible Convertible-PParamsUpdate : Convertible PParamsUpdate F.PParamsUpdate - Convertible-PParamsUpdate = record { to = id ; from = id } + Convertible-PParamsUpdate = λ where + .to x → let open PParamsUpdate.PParamsUpdate x in + record + { a = to a + ; b = to b + ; maxBlockSize = to maxBlockSize + ; maxTxSize = to maxTxSize + ; maxHeaderSize = to maxHeaderSize + ; maxValSize = to maxValSize + ; minUTxOValue = to minUTxOValue + ; poolDeposit = to poolDeposit + ; keyDeposit = to keyDeposit + ; Emax = to Emax + ; nopt = to nopt + ; pv = to pv + ; poolVotingThresholds = to poolThresholds + ; drepVotingThresholds = to drepThresholds + ; govActionLifetime = to govActionLifetime + ; govActionDeposit = to govActionDeposit + ; drepDeposit = to drepDeposit + ; drepActivity = to drepActivity + ; ccMinSize = to ccMinSize + ; ccMaxTermLength = to ccMaxTermLength + ; costmdls = to costmdls + ; prices = to prices + ; maxTxExUnits = to maxTxExUnits + ; maxBlockExUnits = to maxBlockExUnits + ; coinsPerUTxOByte = to coinsPerUTxOByte + ; maxCollateralInputs = to maxCollateralInputs + } + .from x → let open F.PParamsUpdate x in + record + { maxBlockSize = from maxBlockSize + ; maxTxSize = from maxTxSize + ; maxHeaderSize = from maxHeaderSize + ; maxValSize = from maxValSize + ; maxCollateralInputs = from maxCollateralInputs + ; maxTxExUnits = from maxTxExUnits + ; maxBlockExUnits = from maxBlockExUnits + ; pv = from pv + ; a = from a + ; b = from b + ; keyDeposit = from keyDeposit + ; poolDeposit = from poolDeposit + ; coinsPerUTxOByte = from coinsPerUTxOByte + ; minFeeRefScriptCoinsPerByte = nothing + ; prices = from prices + ; minUTxOValue = from minUTxOValue + ; a0 = nothing + ; Emax = from Emax + ; nopt = from nopt + ; collateralPercentage = nothing + ; costmdls = from costmdls + ; drepThresholds = from drepVotingThresholds + ; poolThresholds = from poolVotingThresholds + ; govActionLifetime = from govActionLifetime + ; govActionDeposit = from govActionDeposit + ; drepDeposit = from drepDeposit + ; drepActivity = from drepActivity + ; ccMinSize = from ccMinSize + ; ccMaxTermLength = from ccMaxTermLength + } open import Ledger.Certs.Properties govStructure diff --git a/src/Ledger/Foreign/HSLedger/Core.agda b/src/Ledger/Foreign/HSLedger/Core.agda index b02463914..fd7cd300f 100644 --- a/src/Ledger/Foreign/HSLedger/Core.agda +++ b/src/Ledger/Foreign/HSLedger/Core.agda @@ -140,18 +140,41 @@ HSScriptStructure = record instance _ = HSScriptStructure -open import Ledger.PParams it it it hiding (PParams; Acnt; DrepThresholds; PoolThresholds) +open import Ledger.PParams it it it hiding (Acnt; DrepThresholds; PoolThresholds) HsGovParams : GovParams HsGovParams = record { Implementation ; ppUpd = let open PParamsDiff in λ where - .UpdateT → ℕ -- cost parameter `a` - .updateGroups → λ _ → ❴ EconomicGroup ❵ - .applyUpdate → λ p a → record p { a = a } - .ppWF? → ⁇ yes (λ _ h → h) + .UpdateT → PParamsUpdate + .updateGroups → modifiedUpdateGroups + .applyUpdate → applyPParamsUpdate + .ppWF? {u} → ppWF u ; ppHashingScheme = it } + where + open PParamsUpdate + -- FIXME Replace `trustMe` with an actual proof + ppWF : (u : PParamsUpdate) → + ((pp : PParams) → + paramsWellFormed pp → + paramsWellFormed (applyPParamsUpdate pp u)) + ⁇ + ppWF u with paramsUpdateWellFormed? u + ... | yes _ = ⁇ (yes trustMe) + where + postulate + trustMe : + ((pp : PParams) → + paramsWellFormed pp → + paramsWellFormed (applyPParamsUpdate pp u)) + ... | no _ = ⁇ (no trustMe) + where + postulate + trustMe : + ¬((pp : PParams) → + paramsWellFormed pp → + paramsWellFormed (applyPParamsUpdate pp u)) HSTransactionStructure : TransactionStructure HSTransactionStructure = record diff --git a/src/Ledger/Foreign/LedgerTypes.agda b/src/Ledger/Foreign/LedgerTypes.agda index ef4331dcb..a8062ed05 100644 --- a/src/Ledger/Foreign/LedgerTypes.agda +++ b/src/Ledger/Foreign/LedgerTypes.agda @@ -64,7 +64,6 @@ Ix = ℕ Epoch = ℕ ScriptHash = ℕ Slot = ℕ -PParamsUpdate = ℕ Anchor = ⊤ AuxiliaryData = ⊤ @@ -104,7 +103,6 @@ ProtVer = Pair ℕ ℕ type Ix = Integer type Epoch = Integer type ScriptHash = Integer - type PParamsUpdate = Integer type Slot = Integer type AuxiliaryData = () @@ -260,33 +258,63 @@ record PoolThresholds : Set where field Q1 Q2a Q2b Q4 Q5e : Rational record PParams : Set where - field a : ℕ - b : ℕ - maxBlockSize : ℕ - maxTxSize : ℕ - maxHeaderSize : ℕ - maxValSize : ℕ - minUTxOValue : Coin - poolDeposit : Coin - keyDeposit : Coin - Emax : Epoch - nopt : ℕ - pv : Pair ℕ ℕ - poolVotingThresholds : PoolThresholds - drepVotingThresholds : DrepThresholds - govActionLifetime : ℕ - govActionDeposit : Coin - drepDeposit : Coin - drepActivity : Epoch - ccMinSize : ℕ - ccMaxTermLength : ℕ - costmdls : ⊤ - prices : ⊤ - maxTxExUnits : ExUnits - maxBlockExUnits : ExUnits - coinsPerUTxOByte : Coin + field a : ℕ + b : ℕ + maxBlockSize : ℕ + maxTxSize : ℕ + maxHeaderSize : ℕ + maxValSize : ℕ + minUTxOValue : Coin + poolDeposit : Coin + keyDeposit : Coin + Emax : Epoch + nopt : ℕ + pv : Pair ℕ ℕ + poolVotingThresholds : PoolThresholds + drepVotingThresholds : DrepThresholds + govActionLifetime : ℕ + govActionDeposit : Coin + drepDeposit : Coin + drepActivity : Epoch + ccMinSize : ℕ + ccMaxTermLength : ℕ + costmdls : ⊤ + prices : ⊤ + maxTxExUnits : ExUnits + maxBlockExUnits : ExUnits + coinsPerUTxOByte : Coin -- collateralPercent : ℕ - maxCollateralInputs : ℕ + maxCollateralInputs : ℕ + +record PParamsUpdate : Set where + field a : Maybe ℕ + b : Maybe ℕ + maxBlockSize : Maybe ℕ + maxTxSize : Maybe ℕ + maxHeaderSize : Maybe ℕ + maxValSize : Maybe ℕ + minUTxOValue : Maybe Coin + poolDeposit : Maybe Coin + keyDeposit : Maybe Coin + Emax : Maybe Epoch + nopt : Maybe ℕ + pv : Maybe (Pair ℕ ℕ) + poolVotingThresholds : Maybe PoolThresholds + drepVotingThresholds : Maybe DrepThresholds + govActionLifetime : Maybe ℕ + govActionDeposit : Maybe Coin + drepDeposit : Maybe Coin + drepActivity : Maybe Epoch + ccMinSize : Maybe ℕ + ccMaxTermLength : Maybe ℕ + costmdls : Maybe ⊤ + prices : Maybe ⊤ + maxTxExUnits : Maybe ExUnits + maxBlockExUnits : Maybe ExUnits + coinsPerUTxOByte : Maybe Coin + -- collateralPercent : Maybe ℕ + maxCollateralInputs : Maybe ℕ + {-# FOREIGN GHC data DrepThresholds = MkDrepThresholds { p1 :: Rational @@ -312,37 +340,67 @@ record PParams : Set where deriving Show data PParams = MkPParams - { a :: Integer - , b :: Integer - , maxBlockSize :: Integer - , maxTxSize :: Integer - , maxHeaderSize :: Integer - , maxValSize :: Integer - , minUTxOValue :: Coin - , poolDeposit :: Coin - , keyDeposit :: Coin - , emax :: Epoch - , nopt :: Integer - , pv :: (Integer, Integer) - , poolVotingThresholds :: PoolThresholds - , drepVotingThresholds :: DrepThresholds - , govActionLifetime :: Integer - , govActionDeposit :: Coin - , drepDeposit :: Coin - , drepActivity :: Epoch - , ccMinSize :: Integer - , ccMaxTermLength :: Integer - , costmdls :: () - , prices :: () - , maxTxExUnits :: ExUnits - , maxBlockExUnits :: ExUnits - , coinsPerUTxOByte :: Coin - , maxCollateralInputs :: Integer + { ppA :: Integer + , ppB :: Integer + , ppMaxBlockSize :: Integer + , ppMaxTxSize :: Integer + , ppMaxHeaderSize :: Integer + , ppMaxValSize :: Integer + , ppMinUTxOValue :: Coin + , ppPoolDeposit :: Coin + , ppKeyDeposit :: Coin + , ppEmax :: Epoch + , ppNopt :: Integer + , ppPv :: (Integer, Integer) + , ppPoolVotingThresholds :: PoolThresholds + , ppDrepVotingThresholds :: DrepThresholds + , ppGovActionLifetime :: Integer + , ppGovActionDeposit :: Coin + , ppDrepDeposit :: Coin + , ppDrepActivity :: Epoch + , ppCCMinSize :: Integer + , ppCCMaxTermLength :: Integer + , ppCostmdls :: () + , ppPrices :: () + , ppMaxTxExUnits :: ExUnits + , ppMaxBlockExUnits :: ExUnits + , ppCoinsPerUTxOByte :: Coin + , ppMaxCollateralInputs :: Integer + } deriving (Show, Generic) + + data PParamsUpdate = MkPParamsUpdate + { ppuA :: Maybe Integer + , ppuB :: Maybe Integer + , ppuMaxBlockSize :: Maybe Integer + , ppuMaxTxSize :: Maybe Integer + , ppuMaxHeaderSize :: Maybe Integer + , ppuMaxValSize :: Maybe Integer + , ppuMinUTxOValue :: Maybe Coin + , ppuPoolDeposit :: Maybe Coin + , ppuKeyDeposit :: Maybe Coin + , ppuEmax :: Maybe Epoch + , ppuNopt :: Maybe Integer + , ppuPv :: Maybe (Integer, Integer) + , ppuPoolVotingThresholds :: Maybe PoolThresholds + , ppuDrepVotingThresholds :: Maybe DrepThresholds + , ppuGovActionLifetime :: Maybe Integer + , ppuGovActionDeposit :: Maybe Coin + , ppuDrepDeposit :: Maybe Coin + , ppuDrepActivity :: Maybe Epoch + , ppuCCMinSize :: Maybe Integer + , ppuCCMaxTermLength :: Maybe Integer + , ppuCostmdls :: Maybe () + , ppuPrices :: Maybe () + , ppuMaxTxExUnits :: Maybe ExUnits + , ppuMaxBlockExUnits :: Maybe ExUnits + , ppuCoinsPerUTxOByte :: Maybe Coin + , ppuMaxCollateralInputs :: Maybe Integer } deriving (Show, Generic) #-} {-# COMPILE GHC DrepThresholds = data DrepThresholds (MkDrepThresholds) #-} {-# COMPILE GHC PoolThresholds = data PoolThresholds (MkPoolThresholds) #-} {-# COMPILE GHC PParams = data PParams (MkPParams) #-} +{-# COMPILE GHC PParamsUpdate = data PParamsUpdate (MkPParamsUpdate) #-} record UTxOEnv : Set where field slot : ℕ diff --git a/src/Ledger/PParams.lagda b/src/Ledger/PParams.lagda index 4c2c73001..9b5339995 100644 --- a/src/Ledger/PParams.lagda +++ b/src/Ledger/PParams.lagda @@ -112,6 +112,171 @@ paramsWellFormed pp = ∷ govActionLifetime ∷ govActionDeposit ∷ drepDeposit ∷ [] ) where open PParams pp \end{code} +\begin{code}[hide] +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) ∷ []) + +module PParamsUpdate where + record PParamsUpdate : Set where + field + maxBlockSize maxTxSize : Maybe ℕ + maxHeaderSize maxValSize : Maybe ℕ + maxCollateralInputs : Maybe ℕ + maxTxExUnits maxBlockExUnits : Maybe ExUnits + pv : Maybe ProtVer -- retired, keep for now + a b : Maybe ℕ + keyDeposit : Maybe Coin + poolDeposit : Maybe Coin + coinsPerUTxOByte : Maybe Coin + minFeeRefScriptCoinsPerByte : Maybe ℚ + prices : Maybe Prices + minUTxOValue : Maybe Coin -- retired, keep for now + 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 → Set + paramsUpdateWellFormed ppu = + just 0 ∉ fromList ( maxBlockSize ∷ maxTxSize ∷ maxHeaderSize ∷ maxValSize + ∷ minUTxOValue ∷ 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 coinsPerUTxOByte + ∷ is-just minFeeRefScriptCoinsPerByte + ∷ 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 + ∷ []) + + modifiedUpdateGroups : PParamsUpdate → ℙ PParamGroup + modifiedUpdateGroups ppu = + ( modifiesNetworkGroup ?═⇒ NetworkGroup + ∪ modifiesEconomicGroup ?═⇒ EconomicGroup + ∪ modifiesTechnicalGroup ?═⇒ TechnicalGroup + ∪ modifiesGovernanceGroup ?═⇒ GovernanceGroup + ) + where + _?═⇒_ : (PParamsUpdate → Bool) → PParamGroup → ℙ PParamGroup + pred ?═⇒ grp = if pred ppu then ❴ grp ❵ else ∅ + + _?↗_ : ∀ {A : Set} → Maybe A → A → A + just x ?↗ _ = x + nothing ?↗ x = x + + ≡-update : ∀ {A : Set} {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 + ; coinsPerUTxOByte = U.coinsPerUTxOByte ?↗ P.coinsPerUTxOByte + ; minFeeRefScriptCoinsPerByte = U.minFeeRefScriptCoinsPerByte ?↗ P.minFeeRefScriptCoinsPerByte + ; 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) ∷ []) + +\end{code} \end{AgdaMultiCode} \caption{Protocol parameter declarations} \label{fig:protocol-parameter-declarations} @@ -166,16 +331,6 @@ function \paramsWellFormed. It performs some sanity checks on protocol parameters. \begin{code}[hide] -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) ∷ []) - instance pvCanFollow? : ∀ {pv} {pv'} → Dec (pvCanFollow pv pv') pvCanFollow? {m , n} {pv} with pv ≟ (m + 1 , 0) | pv ≟ (m , n + 1) diff --git a/src/Ledger/hs-src/test/UtxowSpec.hs b/src/Ledger/hs-src/test/UtxowSpec.hs index ed7d15cb5..a0a532717 100644 --- a/src/Ledger/hs-src/test/UtxowSpec.hs +++ b/src/Ledger/hs-src/test/UtxowSpec.hs @@ -16,17 +16,17 @@ import Lib initParams :: PParams initParams = MkPParams - { a = 1 - , b = 5 - , maxBlockSize = 1000 - , maxTxSize = 100 - , maxHeaderSize = 100 - , maxValSize = 1000 - , minUTxOValue = 0 - , poolDeposit = 10 - , emax = 10 - , pv = (1, 0) - , coinsPerUTxOByte = 1 + { ppA = 1 + , ppB = 5 + , ppMaxBlockSize = 1000 + , ppMaxTxSize = 100 + , ppMaxHeaderSize = 100 + , ppMaxValSize = 1000 + , ppMinUTxOValue = 0 + , ppPoolDeposit = 10 + , ppEmax = 10 + , ppPv = (1, 0) + , ppCoinsPerUTxOByte = 1 } initEnv :: UTxOEnv @@ -60,7 +60,7 @@ bodyFromSimple pp stxb = let s = 5 in MkTxBody { txins = stxins stxb , refInputs = srefInputs stxb , txouts = stxouts stxb - , txfee = (a pp) * s + (b pp) + , txfee = (ppA pp) * s + (ppB pp) , txvldt = stxvldt stxb , txsize = s , txid = stxid stxb