From d06be4490d3bbdcc09dcbe4571bcf94861b9f3f1 Mon Sep 17 00:00:00 2001 From: Andre Knispel Date: Wed, 17 Apr 2024 13:11:09 +0200 Subject: [PATCH] Revert "Made it possible to update PParams (#394)" This reverts commit ccca65058c9ed8934417998dfdb1a7246a37a83b. --- src/Ledger/Foreign/HSLedger.agda | 32 +++++++++-------------------- src/Ledger/Foreign/LedgerTypes.agda | 29 +++++++++++++++++--------- src/Ledger/PParams.lagda | 2 -- 3 files changed, 29 insertions(+), 34 deletions(-) diff --git a/src/Ledger/Foreign/HSLedger.agda b/src/Ledger/Foreign/HSLedger.agda index 5b46a6f6..7cc5fe54 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,23 +142,16 @@ 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 → ℕ -- cost parameter `a` - .updateGroups → λ _ → ❴ EconomicGroup ❵ - .applyUpdate → λ p a → record p { a = a } - .ppdWellFormed → λ _ → true - .ppdWellFormed⇒hasGroup → λ _ → singleton-≢-∅ + .UpdateT → ⊤ + .updateGroups → λ _ → ∅ + .applyUpdate → λ p _ → p + .ppdWellFormed → λ _ → false + .ppdWellFormed⇒hasGroup → λ () .ppdWellFormed⇒WF → λ _ _ x → x ; ppHashingScheme = it } @@ -262,11 +255,6 @@ instance Convertible-DCert : Convertible DCert F.TxCert Convertible-DCert = autoConvertible - Convertible-TxId : Convertible ℕ F.TxId - Convertible-TxId = λ where - .to x → record { txid = x } - .from → F.TxId.txid - Convertible-TxBody : Convertible TxBody F.TxBody Convertible-TxBody = λ where .to txb → let open TxBody txb in record @@ -276,7 +264,7 @@ instance ; txfee = txfee ; txvldt = to txvldt ; txsize = txsize - ; txid = to txid + ; txid = txid ; collateral = to collateral ; reqSigHash = to reqSigHash ; scriptIntHash = nothing @@ -295,7 +283,7 @@ instance ; txADhash = nothing ; netwrk = nothing ; txsize = txsize - ; txid = from txid + ; txid = txid ; txvote = [] ; txprop = [] ; txdonation = ε @@ -452,8 +440,8 @@ fromNeedsHash {NewCommittee _ _ _} x = to x fromNeedsHash {NewConstitution _ _} x = to x fromNeedsHash {TriggerHF _} x = to x fromNeedsHash {ChangePParams _} x = to x -fromNeedsHash {TreasuryWdrl _} x = to 0 F., 0 -fromNeedsHash {Info} x = to 0 F., 0 +fromNeedsHash {TreasuryWdrl _} x = 0 F., 0 +fromNeedsHash {Info} x = 0 F., 0 instance Convertible-GovActionState : Convertible GovActionState F.GovActionState diff --git a/src/Ledger/Foreign/LedgerTypes.agda b/src/Ledger/Foreign/LedgerTypes.agda index c5ce6c31..616c622c 100644 --- a/src/Ledger/Foreign/LedgerTypes.agda +++ b/src/Ledger/Foreign/LedgerTypes.agda @@ -22,6 +22,7 @@ data Empty : Set where {-# FOREIGN GHC data AgdaEmpty deriving (Show, Generic) + instance ToExpr AgdaEmpty #-} data ComputationResult E A : Set where @@ -40,6 +41,8 @@ data ComputationResult E A : Set where return = pure (Success a) >>= m = m a (Failure e) >>= _ = Failure e + + instance (ToExpr e, ToExpr a) => ToExpr (ComputationResult e a) #-} {-# COMPILE GHC ComputationResult = data ComputationResult (Success | Failure) #-} @@ -49,12 +52,10 @@ HSMap : Set → Set → Set HSMap K V = List (Pair K V) Rational = Pair ℤ ℕ -record TxId : Set where - field txid : ℕ - Coin = ℕ Addr = ℕ -- just payment credential +TxId = ℕ Ix = ℕ Epoch = ℕ ScriptHash = ℕ @@ -65,7 +66,7 @@ Datum = ⊤ Redeemer = ⊤ Anchor = ⊤ Network = ⊤ -PParamsUpdate = ℕ +PParamsUpdate = ⊤ Script = ⊤ TxIn = Pair TxId Ix @@ -93,7 +94,6 @@ ProtVer = Pair ℕ ℕ type Ix = Integer type Epoch = Integer type ScriptHash = Integer - type PParamsUpdate = Integer type AuxiliaryData = () type DataHash = () @@ -109,20 +109,20 @@ ProtVer = Pair ℕ ℕ type Hash = Integer data Tag = Spend | Mint | Cert | Rewrd | Vote | Propose deriving (Show, Generic) + instance ToExpr Tag type RdmrPtr = (Tag, Ix) type ExUnits = (Integer, Integer) type ProtVer = (Integer, Integer) type GovActionID = (TxId, Integer) - newtype TxId = MkTxId Integer #-} {-# COMPILE GHC Tag = data Tag (Spend | Mint | Cert | Rewrd | Vote | Propose) #-} -{-# COMPILE GHC TxId = data TxId (MkTxId) #-} {-# FOREIGN GHC data Credential = ScriptObj Integer | KeyHashObj Integer deriving (Show, Eq, Generic) + instance ToExpr Credential #-} data Credential : Set where ScriptObj : Hash → Credential @@ -141,6 +141,7 @@ RwdAddr = Pair Network Credential | DRep | SPO deriving (Show, Eq, Generic) + instance ToExpr GovRole #-} data GovRole : Set where CC DRep SPO : GovRole @@ -152,6 +153,7 @@ data GovRole : Set where | AbstainRep | NoConfidenceRep deriving (Show, Eq, Generic) + instance ToExpr VDeleg #-} data VDeleg : Set where CredVoter : GovRole → Credential → VDeleg @@ -169,6 +171,7 @@ data VDeleg : Set where | DeRegDRep Credential | CCRegHot Credential (Maybe Credential) deriving (Show, Eq, Generic) + instance ToExpr TxCert #-} data TxCert : Set where Delegate : Credential → Maybe VDeleg → Maybe Credential → Coin → TxCert @@ -209,6 +212,7 @@ record TxBody : Set where , scriptIntHash :: Maybe Hash , txcerts :: [TxCert] } deriving (Show, Generic) + instance ToExpr TxBody #-} {-# COMPILE GHC TxBody = data TxBody (MkTxBody) #-} @@ -224,6 +228,7 @@ record TxWitnesses : Set where , txdats :: [(DataHash, Datum)] , txrdmrs :: [(RdmrPtr, (Redeemer, ExUnits))] } deriving (Show, Generic) + instance ToExpr TxWitnesses #-} {-# COMPILE GHC TxWitnesses = data TxWitnesses (MkTxWitnesses) #-} @@ -237,6 +242,7 @@ record Tx : Set where , wits :: TxWitnesses , txAD :: Maybe AuxiliaryData } deriving (Show, Generic) + instance ToExpr Tx #-} {-# COMPILE GHC Tx = data Tx (MkTx) #-} @@ -259,7 +265,7 @@ record PParams : Set where drepActivity : Epoch ccMinSize : ℕ ccMaxTermLength : ℕ - costmdls : ⊤ + costmdls : Empty prices : ⊤ maxTxExUnits : ExUnits maxBlockExUnits : ExUnits @@ -286,13 +292,14 @@ record PParams : Set where , drepActivity :: Epoch , ccMinSize :: Integer , ccMaxTermLength :: Integer - , costmdls :: () + , costmdls :: AgdaEmpty , prices :: () , maxTxExUnits :: ExUnits , maxBlockExUnits :: ExUnits , coinsPerUTxOWord :: Coin , maxCollateralInputs :: Integer } deriving (Show, Generic) + instance ToExpr PParams #-} {-# COMPILE GHC PParams = data PParams (MkPParams) #-} @@ -304,6 +311,7 @@ record UTxOEnv : Set where { slot :: Integer , pparams :: PParams } deriving (Show, Generic) + instance ToExpr UTxOEnv #-} {-# COMPILE GHC UTxOEnv = data UTxOEnv (MkUTxOEnv) #-} @@ -315,6 +323,7 @@ record UTxOState : Set where { utxo :: UTxO , fees :: Coin } deriving (Show, Generic) + instance ToExpr UTxOState #-} {-# COMPILE GHC UTxOState = data UTxOState (MkUTxOState) #-} @@ -403,7 +412,7 @@ GovState = List (Pair GovActionID GovActionState) | NewCommittee [(Credential, Epoch)] [Credential] Rational | NewConstitution DataHash (Maybe ScriptHash) | TriggerHF ProtVer - | ChangePParams PParamsUpdate + | ChangePParams () | TreasuryWdrl [(RwdAddr, Coin)] | Info diff --git a/src/Ledger/PParams.lagda b/src/Ledger/PParams.lagda index 0ad0f68d..526a2e32 100644 --- a/src/Ledger/PParams.lagda +++ b/src/Ledger/PParams.lagda @@ -168,8 +168,6 @@ 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')