From 87cad22bd4640989aae0bbbef5efe9d63c2a84ba Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Joosep=20J=C3=A4=C3=A4ger?= <joosep.jaager@iohk.io>
Date: Mon, 15 Apr 2024 17:15:03 +0300
Subject: [PATCH] Made it possible to update PParams

---
 src/Ledger/Foreign/HSLedger.agda    | 19 +++++++++++++------
 src/Ledger/Foreign/LedgerTypes.agda |  9 +++++----
 src/Ledger/PParams.lagda            |  2 ++
 3 files changed, 20 insertions(+), 10 deletions(-)

diff --git a/src/Ledger/Foreign/HSLedger.agda b/src/Ledger/Foreign/HSLedger.agda
index fc5f422d9..6b6938fe9 100644
--- a/src/Ledger/Foreign/HSLedger.agda
+++ b/src/Ledger/Foreign/HSLedger.agda
@@ -65,7 +65,7 @@ module Implementation where
     }) where open import Algebra.PairOp ℕ zero _≡_ _+_
   _≥ᵉ_ : ExUnits → ExUnits → Set
   _≥ᵉ_ = _≡_
-  CostModel    = ⊥
+  CostModel    = ⊤
   Language     = ⊤
   LangDepView  = ⊤
   Prices       = ⊤
@@ -142,16 +142,23 @@ HSScriptStructure = record
 instance _ = HSScriptStructure
 
 open import Ledger.PParams it it it hiding (PParams)
+open import Axiom.Set.Properties List-Model using (∉-∅)
+
+opaque 
+  unfolding List-Model
+
+  singleton-≢-∅ : ∀ {a} {x : a} → ⦃ DecEq a ⦄ → singleton x ≢ ∅
+  singleton-≢-∅ {x = x} ()
 
 HsGovParams : GovParams
 HsGovParams = record
   { Implementation
   ; ppUpd = let open PParamsDiff in λ where
-      .UpdateT                → ⊤
-      .updateGroups           → λ _ → ∅
-      .applyUpdate            → λ p _ → p
-      .ppdWellFormed          → λ _ → false
-      .ppdWellFormed⇒hasGroup → λ ()
+      .UpdateT                → ℕ -- cost parameter `a`
+      .updateGroups           → λ _ → ❴ EconomicGroup ❵
+      .applyUpdate            → λ p a → record p { a = a }
+      .ppdWellFormed          → λ _ → true
+      .ppdWellFormed⇒hasGroup → λ _ → singleton-≢-∅
       .ppdWellFormed⇒WF       → λ _ _ x → x
   ; ppHashingScheme = it
   }
diff --git a/src/Ledger/Foreign/LedgerTypes.agda b/src/Ledger/Foreign/LedgerTypes.agda
index 616c622c3..9108f7ee5 100644
--- a/src/Ledger/Foreign/LedgerTypes.agda
+++ b/src/Ledger/Foreign/LedgerTypes.agda
@@ -66,7 +66,7 @@ Datum         = ⊤
 Redeemer      = ⊤
 Anchor        = ⊤
 Network       = ⊤
-PParamsUpdate = ⊤
+PParamsUpdate = ℕ
 Script        = ⊤
 
 TxIn          = Pair TxId Ix
@@ -94,6 +94,7 @@ ProtVer = Pair ℕ ℕ
   type Ix      = Integer
   type Epoch   = Integer
   type ScriptHash    = Integer
+  type PParamsUpdate = Integer
 
   type AuxiliaryData = ()
   type DataHash      = ()
@@ -265,7 +266,7 @@ record PParams : Set where
         drepActivity        : Epoch
         ccMinSize           : ℕ
         ccMaxTermLength     : ℕ
-        costmdls            : Empty
+        costmdls            : ⊤
         prices              : ⊤
         maxTxExUnits        : ExUnits
         maxBlockExUnits     : ExUnits
@@ -292,7 +293,7 @@ record PParams : Set where
     , drepActivity        :: Epoch
     , ccMinSize           :: Integer
     , ccMaxTermLength     :: Integer
-    , costmdls            :: AgdaEmpty
+    , costmdls            :: ()
     , prices              :: ()
     , maxTxExUnits        :: ExUnits
     , maxBlockExUnits     :: ExUnits
@@ -412,7 +413,7 @@ GovState = List (Pair GovActionID GovActionState)
     | NewCommittee [(Credential, Epoch)] [Credential] Rational
     | NewConstitution DataHash (Maybe ScriptHash)
     | TriggerHF ProtVer
-    | ChangePParams ()
+    | ChangePParams PParamsUpdate
     | TreasuryWdrl [(RwdAddr, Coin)]
     | Info
 
diff --git a/src/Ledger/PParams.lagda b/src/Ledger/PParams.lagda
index 526a2e324..0ad0f68df 100644
--- a/src/Ledger/PParams.lagda
+++ b/src/Ledger/PParams.lagda
@@ -168,6 +168,8 @@ instance
     ((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')