From 50c739b0e8091f2c1585acec8544497ac6f3fca1 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Joosep=20J=C3=A4=C3=A4ger?= Date: Wed, 17 Apr 2024 14:16:19 +0300 Subject: [PATCH] GOV Conformance --- src/Ledger/Foreign/HSLedger.agda | 32 ++++++++++++++++++++--------- src/Ledger/Foreign/LedgerTypes.agda | 29 +++++++++----------------- src/Ledger/PParams.lagda | 2 ++ 3 files changed, 34 insertions(+), 29 deletions(-) diff --git a/src/Ledger/Foreign/HSLedger.agda b/src/Ledger/Foreign/HSLedger.agda index 7cc5fe542..5b46a6f68 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 } @@ -255,6 +262,11 @@ 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 @@ -264,7 +276,7 @@ instance ; txfee = txfee ; txvldt = to txvldt ; txsize = txsize - ; txid = txid + ; txid = to txid ; collateral = to collateral ; reqSigHash = to reqSigHash ; scriptIntHash = nothing @@ -283,7 +295,7 @@ instance ; txADhash = nothing ; netwrk = nothing ; txsize = txsize - ; txid = txid + ; txid = from txid ; txvote = [] ; txprop = [] ; txdonation = ε @@ -440,8 +452,8 @@ fromNeedsHash {NewCommittee _ _ _} x = to x fromNeedsHash {NewConstitution _ _} x = to x fromNeedsHash {TriggerHF _} x = to x fromNeedsHash {ChangePParams _} x = to x -fromNeedsHash {TreasuryWdrl _} x = 0 F., 0 -fromNeedsHash {Info} x = 0 F., 0 +fromNeedsHash {TreasuryWdrl _} x = to 0 F., 0 +fromNeedsHash {Info} x = to 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 616c622c3..c5ce6c319 100644 --- a/src/Ledger/Foreign/LedgerTypes.agda +++ b/src/Ledger/Foreign/LedgerTypes.agda @@ -22,7 +22,6 @@ data Empty : Set where {-# FOREIGN GHC data AgdaEmpty deriving (Show, Generic) - instance ToExpr AgdaEmpty #-} data ComputationResult E A : Set where @@ -41,8 +40,6 @@ 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) #-} @@ -52,10 +49,12 @@ 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 = ℕ @@ -66,7 +65,7 @@ Datum = ⊤ Redeemer = ⊤ Anchor = ⊤ Network = ⊤ -PParamsUpdate = ⊤ +PParamsUpdate = ℕ Script = ⊤ TxIn = Pair TxId Ix @@ -94,6 +93,7 @@ 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,7 +141,6 @@ RwdAddr = Pair Network Credential | DRep | SPO deriving (Show, Eq, Generic) - instance ToExpr GovRole #-} data GovRole : Set where CC DRep SPO : GovRole @@ -153,7 +152,6 @@ data GovRole : Set where | AbstainRep | NoConfidenceRep deriving (Show, Eq, Generic) - instance ToExpr VDeleg #-} data VDeleg : Set where CredVoter : GovRole → Credential → VDeleg @@ -171,7 +169,6 @@ 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 @@ -212,7 +209,6 @@ record TxBody : Set where , scriptIntHash :: Maybe Hash , txcerts :: [TxCert] } deriving (Show, Generic) - instance ToExpr TxBody #-} {-# COMPILE GHC TxBody = data TxBody (MkTxBody) #-} @@ -228,7 +224,6 @@ record TxWitnesses : Set where , txdats :: [(DataHash, Datum)] , txrdmrs :: [(RdmrPtr, (Redeemer, ExUnits))] } deriving (Show, Generic) - instance ToExpr TxWitnesses #-} {-# COMPILE GHC TxWitnesses = data TxWitnesses (MkTxWitnesses) #-} @@ -242,7 +237,6 @@ record Tx : Set where , wits :: TxWitnesses , txAD :: Maybe AuxiliaryData } deriving (Show, Generic) - instance ToExpr Tx #-} {-# COMPILE GHC Tx = data Tx (MkTx) #-} @@ -265,7 +259,7 @@ record PParams : Set where drepActivity : Epoch ccMinSize : ℕ ccMaxTermLength : ℕ - costmdls : Empty + costmdls : ⊤ prices : ⊤ maxTxExUnits : ExUnits maxBlockExUnits : ExUnits @@ -292,14 +286,13 @@ record PParams : Set where , drepActivity :: Epoch , ccMinSize :: Integer , ccMaxTermLength :: Integer - , costmdls :: AgdaEmpty + , costmdls :: () , prices :: () , maxTxExUnits :: ExUnits , maxBlockExUnits :: ExUnits , coinsPerUTxOWord :: Coin , maxCollateralInputs :: Integer } deriving (Show, Generic) - instance ToExpr PParams #-} {-# COMPILE GHC PParams = data PParams (MkPParams) #-} @@ -311,7 +304,6 @@ record UTxOEnv : Set where { slot :: Integer , pparams :: PParams } deriving (Show, Generic) - instance ToExpr UTxOEnv #-} {-# COMPILE GHC UTxOEnv = data UTxOEnv (MkUTxOEnv) #-} @@ -323,7 +315,6 @@ record UTxOState : Set where { utxo :: UTxO , fees :: Coin } deriving (Show, Generic) - instance ToExpr UTxOState #-} {-# COMPILE GHC UTxOState = data UTxOState (MkUTxOState) #-} @@ -412,7 +403,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')