Add PParamsUpdate (#443)

IntersectMBO · Jun 6, 2024 · 31a523f · 31a523f
1 parent df4dfc8
commit 31a523f
Show file tree

Hide file tree

Showing 5 changed files with 379 additions and 82 deletions.
diff --git 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
@@ -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
@@ -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    : ℕ