Added conformance test for ENACT

IntersectMBO · May 27, 2024 · d02e935 · d02e935
1 parent fd46bf1
commit d02e935
Show file tree

Hide file tree

Showing 13 changed files with 210 additions and 106 deletions.
diff --git a/eras/alonzo/impl/CHANGELOG.md b/eras/alonzo/impl/CHANGELOG.md
@@ -3,6 +3,7 @@
 ## 1.8.1.0
 
 * Add `AllegraEraScript` and `ShelleyEraScript` instances for `AlonzoEra`
+* Add `Inject` instance for `AlonzoTx`
 
 ## testlib
 

diff --git a/eras/conway/impl/CHANGELOG.md b/eras/conway/impl/CHANGELOG.md
@@ -2,6 +2,9 @@
 
 ## 1.14.1.0
 
+* Add `NFData` instances for:
+  * `RatifySignal`
+  * `EnactSignal`
 * Add instances for `ConwayGovCertEnv`. #4348
   * `NFData`
   * `ToExpr`
@@ -10,7 +13,9 @@
 
 ### `testlib`
 
-* Add `ToExpr` instance for `RatifySignal`
+* Add `ToExpr` instances for:
+  * `RatifySignal`
+  * `EnactSignal`
 
 ## 1.14.0.0
 

diff --git a/eras/conway/impl/src/Cardano/Ledger/Conway/Governance/Internal.hs b/eras/conway/impl/src/Cardano/Ledger/Conway/Governance/Internal.hs
@@ -5,6 +5,7 @@
 {-# LANGUAGE FlexibleInstances #-}
 {-# LANGUAGE LambdaCase #-}
 {-# LANGUAGE MonoLocalBinds #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
 {-# LANGUAGE NamedFieldPuns #-}
 {-# LANGUAGE OverloadedStrings #-}
 {-# LANGUAGE RecordWildCards #-}

diff --git a/eras/conway/impl/src/Cardano/Ledger/Conway/Rules/Enact.hs b/eras/conway/impl/src/Cardano/Ledger/Conway/Rules/Enact.hs
@@ -36,6 +36,7 @@ import Cardano.Ledger.Conway.Governance (
 import Cardano.Ledger.Credential (Credential)
 import Cardano.Ledger.Keys (KeyRole (..))
 import Cardano.Ledger.Val (Val (..))
+import Control.DeepSeq (NFData)
 import Control.State.Transition.Extended (
   STS (..),
   TRC (..),
@@ -57,6 +58,8 @@ data EnactSignal era = EnactSignal
   }
   deriving (Eq, Show, Generic)
 
+instance EraPParams era => NFData (EnactSignal era)
+
 instance EraGov era => STS (ConwayENACT era) where
   type Environment (ConwayENACT era) = ()
   type PredicateFailure (ConwayENACT era) = Void

diff --git a/eras/conway/impl/src/Cardano/Ledger/Conway/TxCert.hs b/eras/conway/impl/src/Cardano/Ledger/Conway/TxCert.hs
@@ -3,6 +3,7 @@
 {-# LANGUAGE DeriveGeneric #-}
 {-# LANGUAGE FlexibleContexts #-}
 {-# LANGUAGE LambdaCase #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
 {-# LANGUAGE OverloadedStrings #-}
 {-# LANGUAGE PatternSynonyms #-}
 {-# LANGUAGE ScopedTypeVariables #-}

diff --git a/eras/conway/impl/testlib/Test/Cardano/Ledger/Conway/TreeDiff.hs b/eras/conway/impl/testlib/Test/Cardano/Ledger/Conway/TreeDiff.hs
@@ -257,3 +257,5 @@ instance ToExpr (PParams era) => ToExpr (CertEnv era)
 instance ToExpr (PParams era) => ToExpr (ConwayDelegEnv era)
 
 instance ToExpr (PParamsHKD StrictMaybe era) => ToExpr (RatifySignal era)
+
+instance ToExpr (PParamsHKD StrictMaybe era) => ToExpr (EnactSignal era)
diff --git a/eras/shelley/impl/CHANGELOG.md b/eras/shelley/impl/CHANGELOG.md
@@ -12,6 +12,9 @@
 * Change signatures of `evalMultiSig` and `validateMultiSig`:
   * replace `Era` constraint with `ShelleyEraScript`
   * replace `MultiSig` with `NativeScript`
+* Add `Inject` instances for:
+  * `UTxOState`
+  * `UtxoEnv`
 
 ### testlib
 * Add `withCborRoundTripFailures`

diff --git a/libs/cardano-ledger-conformance/src/Test/Cardano/Ledger/Conformance/ExecSpecRule/Conway.hs b/libs/cardano-ledger-conformance/src/Test/Cardano/Ledger/Conformance/ExecSpecRule/Conway.hs
@@ -25,6 +25,7 @@ import Cardano.Ledger.Conway (Conway)
 import Cardano.Ledger.Conway.Core (Era (..), EraPParams (..), PParamsUpdate)
 import Cardano.Ledger.Conway.Governance (
   EnactState,
+  GovAction,
   GovActionState (..),
   GovProcedures (..),
   ProposalProcedure,
@@ -37,7 +38,7 @@ import Cardano.Ledger.Conway.Governance (
   toPrevGovActionIds,
  )
 import Cardano.Ledger.Conway.PParams (THKD (..))
-import Cardano.Ledger.Conway.Rules (ConwayGovPredFailure, RatifyState)
+import Cardano.Ledger.Conway.Rules (ConwayGovPredFailure, EnactSignal, RatifyState)
 import Cardano.Ledger.Conway.Tx (AlonzoTx)
 import Cardano.Ledger.Conway.TxCert (ConwayGovCert, ConwayTxCert)
 import Cardano.Ledger.Credential (Credential)
@@ -67,7 +68,7 @@ import Test.Cardano.Ledger.Conformance (
   runConformance,
   runSpecTransM,
  )
-import Test.Cardano.Ledger.Conformance.SpecTranslate.Conway ()
+import Test.Cardano.Ledger.Conformance.SpecTranslate.Conway (ConwayExecEnactEnv)
 import Test.Cardano.Ledger.Constrained.Conway (
   IsConwayUniv,
   ProposalsSplit,
@@ -220,20 +221,27 @@ agdaCompatiblePPU ppup =
         (branch $ \_ -> False)
         (branch $ \_ -> True)
 
+agdaCompatibleGovAction ::
+  IsConwayUniv fn =>
+  Term fn (GovAction Conway) ->
+  Pred fn
+agdaCompatibleGovAction govAction =
+  caseOn
+    govAction
+    (branch $ \_ ppup _ -> agdaCompatiblePPU ppup)
+    (branch $ \_ _ -> True)
+    (branch $ \_ _ -> True)
+    (branch $ const True)
+    (branch $ \_ _ _ _ -> True)
+    (branch $ \_ _ -> True)
+    (branch $ const True)
+
 agdaCompatibleProposal ::
   IsConwayUniv fn =>
   Term fn (ProposalProcedure Conway) ->
   Pred fn
 agdaCompatibleProposal prop =
-  match prop $ \_ _ govAction _ ->
-    (caseOn govAction)
-      (branch $ \_ ppup _ -> agdaCompatiblePPU ppup)
-      (branch $ \_ _ -> True)
-      (branch $ \_ _ -> True)
-      (branch $ \_ -> True)
-      (branch $ \_ _ _ _ -> True)
-      (branch $ \_ _ -> True)
-      (branch $ \_ -> True)
+  match prop $ \_ _ govAction _ -> agdaCompatibleGovAction govAction
 
 agdaCompatibleGAS ::
   IsConwayUniv fn =>
@@ -529,3 +537,18 @@ instance IsConwayUniv fn => ExecSpecRule fn "GOVCERT" Conway where
     first (\e -> OpaqueErrorString (T.unpack e) NE.:| [])
       . computationResultToEither
       $ Agda.govCertStep env st sig
+
+instance IsConwayUniv fn => ExecSpecRule fn "ENACT" Conway where
+  type ExecEnvironment fn "ENACT" Conway = ConwayExecEnactEnv Conway
+
+  environmentSpec _ = TrueSpec
+  stateSpec _ _ = TrueSpec
+  signalSpec _ _ _ = onlyMinFeeAUpdates
+    where
+      onlyMinFeeAUpdates :: Specification fn (EnactSignal Conway)
+      onlyMinFeeAUpdates = constrained $ \sig ->
+        match sig $ \_ ga -> agdaCompatibleGovAction ga
+  runAgdaRule env st sig =
+    first (error "ENACT failed")
+      . computationResultToEither
+      $ Agda.enactStep env st sig