Add Conformance.Imp: imptests with conformance.

With a new `iteHook` field added to `ImpTestEnv`, we get an overridable function that can be executed within `trySubmitTx` for every submitted transaction. To override this hook we have `modifyImpInitHook` and `withHook` functions. We add a new `Conformance.Imp` module to `cardano-ledger-conformance` package, to import `Conway.Imp` and run those tests with a modified "hook" that runs the `LEDGER` rule from Agda on the Tx and `checkConformance` on the results. Additions: - `iteHook` field to `ImpTestEnv`. - `modifyImpInitHook` function to override the hook. - `withHook` helper function to use a different hook locally. - `impInitEnvL` and `impInitStateL` lenses. Changes: - Change `trySubmitTx` to run the hook for every submitted Tx.
IntersectMBO · Nov 19, 2024 · d7c9778 · d7c9778
1 parent 4ae42f5
commit d7c9778
Show file tree

Hide file tree

Showing 12 changed files with 306 additions and 41 deletions.
diff --git a/eras/conway/impl/testlib/Test/Cardano/Ledger/Conway/Imp.hs b/eras/conway/impl/testlib/Test/Cardano/Ledger/Conway/Imp.hs
@@ -6,7 +6,7 @@
 {-# LANGUAGE TypeFamilies #-}
 {-# LANGUAGE TypeOperators #-}
 
-module Test.Cardano.Ledger.Conway.Imp (spec) where
+module Test.Cardano.Ledger.Conway.Imp (spec, conwaySpec) where
 
 import Cardano.Ledger.Alonzo.Plutus.Context (EraPlutusContext (..))
 import Cardano.Ledger.Alonzo.Rules (
@@ -54,18 +54,23 @@ import qualified Test.Cardano.Ledger.Conway.Imp.LedgerSpec as Ledger
 import qualified Test.Cardano.Ledger.Conway.Imp.RatifySpec as Ratify
 import qualified Test.Cardano.Ledger.Conway.Imp.UtxoSpec as Utxo
 import qualified Test.Cardano.Ledger.Conway.Imp.UtxosSpec as Utxos
-import Test.Cardano.Ledger.Conway.ImpTest (ConwayEraImp, LedgerSpec, modifyImpInitProtVer)
+import Test.Cardano.Ledger.Conway.ImpTest (
+  ConwayEraImp,
+  LedgerSpec,
+  modifyImpInitProtVer,
+ )
 import Test.Cardano.Ledger.Imp.Common
+import Test.Cardano.Ledger.Shelley.ImpTest (ImpInit)
 
 spec ::
   forall era.
   ( Arbitrary (TxAuxData era)
   , ConwayEraImp era
   , EraSegWits era
-  , InjectRuleFailure "LEDGER" ConwayGovPredFailure era
-  , InjectRuleFailure "LEDGER" ConwayCertsPredFailure era
   , Inject (BabbageContextError era) (ContextError era)
   , Inject (ConwayContextError era) (ContextError era)
+  , InjectRuleFailure "LEDGER" ConwayGovPredFailure era
+  , InjectRuleFailure "LEDGER" ConwayCertsPredFailure era
   , InjectRuleFailure "LEDGER" BabbageUtxoPredFailure era
   , InjectRuleFailure "LEDGER" BabbageUtxowPredFailure era
   , InjectRuleFailure "LEDGER" AlonzoUtxoPredFailure era
@@ -77,38 +82,74 @@ spec ::
   , InjectRuleFailure "LEDGER" ConwayGovCertPredFailure era
   , InjectRuleFailure "LEDGER" ConwayLedgerPredFailure era
   , InjectRuleFailure "BBODY" ConwayBbodyPredFailure era
+  , InjectRuleEvent "TICK" ConwayEpochEvent era
+  , Event (EraRule "EPOCH" era) ~ ConwayEpochEvent era
+  , Event (EraRule "NEWEPOCH" era) ~ ConwayNewEpochEvent era
+  , Event (EraRule "MEMPOOL" era) ~ ConwayMempoolEvent era
+  , Event (EraRule "LEDGERS" era) ~ ShelleyLedgersEvent era
+  , Event (EraRule "LEDGER" era) ~ ConwayLedgerEvent era
+  , Event (EraRule "HARDFORK" era) ~ ConwayHardForkEvent era
+  , BaseM (EraRule "LEDGERS" era) ~ ShelleyBase
+  , Environment (EraRule "LEDGERS" era) ~ ShelleyLedgersEnv era
+  , Signal (EraRule "LEDGERS" era) ~ Seq (Tx era)
+  , STS (EraRule "LEDGERS" era)
+  , ApplyTx era
   , NFData (Event (EraRule "ENACT" era))
   , ToExpr (Event (EraRule "ENACT" era))
   , Eq (Event (EraRule "ENACT" era))
   , Typeable (Event (EraRule "ENACT" era))
+  ) =>
+  Spec
+spec = do
+  BabbageImp.spec @era
+  withImpInit @(LedgerSpec era) $ conwaySpec @era
+
+conwaySpec ::
+  forall era.
+  ( ConwayEraImp era
+  , EraSegWits era
+  , Inject (BabbageContextError era) (ContextError era)
+  , Inject (ConwayContextError era) (ContextError era)
+  , InjectRuleFailure "LEDGER" ConwayGovPredFailure era
+  , InjectRuleFailure "LEDGER" ConwayCertsPredFailure era
+  , InjectRuleFailure "LEDGER" BabbageUtxoPredFailure era
+  , InjectRuleFailure "LEDGER" AlonzoUtxosPredFailure era
+  , InjectRuleFailure "LEDGER" AlonzoUtxowPredFailure era
+  , InjectRuleFailure "LEDGER" ShelleyUtxowPredFailure era
+  , InjectRuleFailure "LEDGER" ConwayDelegPredFailure era
+  , InjectRuleFailure "LEDGER" ConwayGovCertPredFailure era
+  , InjectRuleFailure "LEDGER" ConwayLedgerPredFailure era
+  , InjectRuleFailure "BBODY" ConwayBbodyPredFailure era
   , InjectRuleEvent "TICK" ConwayEpochEvent era
   , Event (EraRule "EPOCH" era) ~ ConwayEpochEvent era
   , Event (EraRule "NEWEPOCH" era) ~ ConwayNewEpochEvent era
   , Event (EraRule "MEMPOOL" era) ~ ConwayMempoolEvent era
   , Event (EraRule "LEDGERS" era) ~ ShelleyLedgersEvent era
   , Event (EraRule "LEDGER" era) ~ ConwayLedgerEvent era
+  , Event (EraRule "HARDFORK" era) ~ ConwayHardForkEvent era
   , BaseM (EraRule "LEDGERS" era) ~ ShelleyBase
   , Environment (EraRule "LEDGERS" era) ~ ShelleyLedgersEnv era
   , Signal (EraRule "LEDGERS" era) ~ Seq (Tx era)
   , STS (EraRule "LEDGERS" era)
   , ApplyTx era
-  , Event (EraRule "HARDFORK" era) ~ ConwayHardForkEvent era
+  , NFData (Event (EraRule "ENACT" era))
+  , ToExpr (Event (EraRule "ENACT" era))
+  , Eq (Event (EraRule "ENACT" era))
+  , Typeable (Event (EraRule "ENACT" era))
   ) =>
-  Spec
-spec = do
-  BabbageImp.spec @era
-  withImpInit @(LedgerSpec era) $
-    forM_ (eraProtVersions @era) $ \protVer ->
-      describe ("ConwayImpSpec - " <> show protVer) $
-        modifyImpInitProtVer protVer $ do
-          describe "BBODY" Bbody.spec
-          describe "CERTS" Certs.spec
-          describe "DELEG" Deleg.spec
-          describe "ENACT" Enact.spec
-          describe "EPOCH" Epoch.spec
-          describe "GOV" Gov.spec
-          describe "GOVCERT" GovCert.spec
-          describe "LEDGER" Ledger.spec
-          describe "RATIFY" Ratify.spec
-          describe "UTXO" Utxo.spec
-          describe "UTXOS" Utxos.spec
+  SpecWith (ImpInit (LedgerSpec era))
+conwaySpec = do
+  forM_ (eraProtVersions @era) $ \protVer ->
+    describe ("ConwayImpSpec - " <> show protVer) $
+      modifyImpInitProtVer protVer $ do
+        describe "BBODY" Bbody.spec
+        describe "CERTS" Certs.spec
+        describe "DELEG" Deleg.spec
+        describe "ENACT" Enact.spec
+        describe "EPOCH" Epoch.spec
+        describe "GOV" Gov.spec
+        describe "GOVCERT" GovCert.spec
+        describe "LEDGER" Ledger.spec
+        describe "RATIFY" Ratify.spec
+        describe "UTXO" Utxo.spec
+        describe "UTXOS" Utxos.spec
diff --git a/eras/shelley/impl/CHANGELOG.md b/eras/shelley/impl/CHANGELOG.md
@@ -35,6 +35,10 @@
 
 ### `testlib`
 
+* Add `iteHook` to `ImpTesEnv` for additionally checking conformance with ImpTests. #4748
+  * Add lens `iteHookL`.
+  * Add `withHook` modifier for `ImpTestM era a`
+  * Add `modifyImpInitHook`.
 * Switch to using `ImpSpec` package
 * Remove: `runImpTestM`, `runImpTestM_`, `evalImpTestM`, `execImpTestM`, `runImpTestGenM`, `runImpTestGenM_`, `evalImpTestGenM`, `execImpTestGenM`, `withImpState` and `withImpStateModified`.
 * Add `LedgerSpec`, `modifyImpInitProtVer`.

diff --git a/eras/shelley/impl/testlib/Test/Cardano/Ledger/Shelley/ImpTest.hs b/eras/shelley/impl/testlib/Test/Cardano/Ledger/Shelley/ImpTest.hs
@@ -99,6 +99,7 @@ module Test.Cardano.Ledger.Shelley.ImpTest (
   impEraStartEpochNo,
   impSetSeed,
   modifyImpInitProtVer,
+  modifyImpInitHook,
 
   -- * Logging
   Doc,
@@ -117,6 +118,7 @@ module Test.Cardano.Ledger.Shelley.ImpTest (
   withPostFixup,
   withPreFixup,
   withCborRoundTripFailures,
+  withHook,
   impNESL,
   impGlobalsL,
   impLastTickG,
@@ -302,6 +304,7 @@ instance ShelleyEraImp era => ImpSpec (LedgerSpec era) where
             ImpTestEnv
               { iteFixup = fixupTx
               , iteCborRoundTripFailures = True
+              , iteHook = \_ _ _ _ -> pure ()
               }
         , impInitState = initState
         }
@@ -618,16 +621,30 @@ modifyImpInitProtVer ::
   SpecWith (ImpInit (LedgerSpec era)) ->
   SpecWith (ImpInit (LedgerSpec era))
 modifyImpInitProtVer ver =
-  modifyImpInit $ \impInit ->
-    impInit
-      { impInitState =
-          impInitState impInit
-            & impNESL
-              . nesEsL
-              . curPParamsEpochStateL
-              . ppProtocolVersionL
-              .~ ProtVer ver 0
-      }
+  modifyImpInit
+    ( impInitStateL
+        . impNESL
+        . nesEsL
+        . curPParamsEpochStateL @era
+        . ppProtocolVersionL
+        .~ ProtVer ver 0
+    )
+
+modifyImpInitHook ::
+  forall era.
+  ShelleyEraImp era =>
+  ( Either
+      (NonEmpty (PredicateFailure (EraRule "LEDGER" era)))
+      (State (EraRule "LEDGER" era), [Event (EraRule "LEDGER" era)]) ->
+    LedgerEnv era ->
+    LedgerState era ->
+    Tx era ->
+    ImpTestM era ()
+  ) ->
+  SpecWith (ImpInit (LedgerSpec era)) ->
+  SpecWith (ImpInit (LedgerSpec era))
+modifyImpInitHook f =
+  modifyImpInit (impInitEnvL . iteHookL .~ f)
 
 impLedgerEnv :: EraGov era => NewEpochState era -> ImpTestM era (LedgerEnv era)
 impLedgerEnv nes = do
@@ -767,13 +784,34 @@ impWitsVKeyNeeded txBody = do
 
 data ImpTestEnv era = ImpTestEnv
   { iteFixup :: Tx era -> ImpTestM era (Tx era)
+  , iteHook ::
+      Either
+        (NonEmpty (PredicateFailure (EraRule "LEDGER" era)))
+        (State (EraRule "LEDGER" era), [Event (EraRule "LEDGER" era)]) ->
+      LedgerEnv era ->
+      LedgerState era ->
+      Tx era ->
+      ImpTestM era ()
   , iteCborRoundTripFailures :: !Bool
   -- ^ Expect failures in CBOR round trip serialization tests for predicate failures
   }
 
 iteFixupL :: Lens' (ImpTestEnv era) (Tx era -> ImpTestM era (Tx era))
 iteFixupL = lens iteFixup (\x y -> x {iteFixup = y})
 
+iteHookL ::
+  Lens'
+    (ImpTestEnv era)
+    ( Either
+        (NonEmpty (PredicateFailure (EraRule "LEDGER" era)))
+        (State (EraRule "LEDGER" era), [Event (EraRule "LEDGER" era)]) ->
+      LedgerEnv era ->
+      LedgerState era ->
+      Tx era ->
+      ImpTestM era ()
+    )
+iteHookL = lens iteHook (\x y -> x {iteHook = y})
+
 iteCborRoundTripFailuresL :: Lens' (ImpTestEnv era) Bool
 iteCborRoundTripFailuresL = lens iteCborRoundTripFailures (\x y -> x {iteCborRoundTripFailures = y})
 
@@ -1032,6 +1070,10 @@ trySubmitTx tx = do
   ImpTestState {impRootTxIn} <- get
   res <- tryRunImpRule @"LEDGER" lEnv (st ^. nesEsL . esLStateL) txFixed
   roundTripCheck <- asks iteCborRoundTripFailures
+
+  -- Check for conformance
+  asks iteHook >>= (\f -> f res lEnv (st ^. nesEsL . esLStateL) txFixed)
+
   case res of
     Left predFailures -> do
       -- Verify that produced predicate failures are ready for the node-to-client protocol
@@ -1551,6 +1593,20 @@ withPostFixup ::
   ImpTestM era a
 withPostFixup f = withCustomFixup (>=> f)
 
+-- | Replace the hook with the given hook
+withHook ::
+  ( Either
+      (NonEmpty (PredicateFailure (EraRule "LEDGER" era)))
+      (State (EraRule "LEDGER" era), [Event (EraRule "LEDGER" era)]) ->
+    LedgerEnv era ->
+    LedgerState era ->
+    Tx era ->
+    ImpTestM era ()
+  ) ->
+  ImpTestM era a ->
+  ImpTestM era a
+withHook f = local $ iteHookL .~ f
+
 expectUTxOContent ::
   (HasCallStack, ToExpr (TxOut era)) =>
   UTxO era -> [(TxIn (EraCrypto era), Maybe (TxOut era) -> Bool)] -> ImpTestM era ()

diff --git a/libs/ImpSpec/ImpSpec.cabal b/libs/ImpSpec/ImpSpec.cabal
@@ -47,7 +47,8 @@ library
         prettyprinter-ansi-terminal,
         random,
         text,
-        unliftio
+        unliftio,
+        microlens
 
 test-suite tests
     type:             exitcode-stdio-1.0

diff --git a/libs/ImpSpec/src/Test/ImpSpec/Internal.hs b/libs/ImpSpec/src/Test/ImpSpec/Internal.hs
@@ -25,6 +25,7 @@ import Data.Proxy (Proxy (..))
 import Data.Text (Text)
 import qualified Data.Text.Lazy as TL
 import GHC.Stack (CallStack, HasCallStack, SrcLoc (..), getCallStack)
+import Lens.Micro
 import Prettyprinter (
   Doc,
   Pretty (..),
@@ -97,6 +98,12 @@ deriving instance (Eq (ImpSpecEnv t), Eq (ImpSpecState t)) => Eq (ImpInit t)
 deriving instance (Ord (ImpSpecEnv t), Ord (ImpSpecState t)) => Ord (ImpInit t)
 deriving instance (Show (ImpSpecEnv t), Show (ImpSpecState t)) => Show (ImpInit t)
 
+impInitEnvL :: Lens' (ImpInit t) (ImpSpecEnv t)
+impInitEnvL = lens impInitEnv $ \x y -> x {impInitEnv = y}
+
+impInitStateL :: Lens' (ImpInit t) (ImpSpecState t)
+impInitStateL = lens impInitState $ \x y -> x {impInitState = y}
+
 -- | Stores extra information about the failure of the unit test
 data ImpException = ImpException
   { ieAnnotation :: [Doc AnsiStyle]

diff --git a/libs/cardano-ledger-conformance/cardano-ledger-conformance.cabal b/libs/cardano-ledger-conformance/cardano-ledger-conformance.cabal
@@ -22,13 +22,13 @@ library
     exposed-modules:
         Test.Cardano.Ledger.Conformance
         Test.Cardano.Ledger.Conformance.ExecSpecRule.Core
+        Test.Cardano.Ledger.Conformance.SpecTranslate.Core
         Test.Cardano.Ledger.Conformance.ExecSpecRule.Conway
         Test.Cardano.Ledger.Conformance.ExecSpecRule.Conway.Base
         Test.Cardano.Ledger.Conformance.SpecTranslate.Conway
 
     hs-source-dirs:   src
     other-modules:
-        Test.Cardano.Ledger.Conformance.SpecTranslate.Core
         Test.Cardano.Ledger.Conformance.SpecTranslate.Conway.Base
         Test.Cardano.Ledger.Conformance.SpecTranslate.Conway.Deleg
         Test.Cardano.Ledger.Conformance.SpecTranslate.Conway.Pool
@@ -106,6 +106,7 @@ test-suite tests
         Test.Cardano.Ledger.Conformance.Spec.Conway
         Test.Cardano.Ledger.Conformance.ExecSpecRule.MiniTrace
         Test.Cardano.Ledger.Conformance.Imp.Ratify
+        Test.Cardano.Ledger.Conformance.Imp
 
     default-language: Haskell2010
     ghc-options:
@@ -116,14 +117,18 @@ test-suite tests
     build-depends:
         base >=4.14 && <5,
         containers,
+        data-default,
         cardano-data,
         constrained-generators,
         small-steps,
+        cardano-ledger-binary,
         cardano-ledger-conformance,
         cardano-ledger-core:{cardano-ledger-core, testlib},
         cardano-strict-containers,
         cardano-ledger-shelley,
         cardano-ledger-alonzo,
         cardano-ledger-conway:{cardano-ledger-conway, testlib},
         cardano-ledger-test,
-        microlens
+        microlens,
+        microlens-mtl,
+        unliftio
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
@@ -1,6 +1,7 @@
 module Test.Cardano.Ledger.Conformance.ExecSpecRule.Conway (
   module X,
   ConwayRatifyExecContext (..),
+  ConwayLedgerExecContext (..),
 ) where
 
 import Test.Cardano.Ledger.Conformance.ExecSpecRule.Conway.Base as X (
@@ -16,7 +17,9 @@ import Test.Cardano.Ledger.Conformance.ExecSpecRule.Conway.Certs as X (nameCerts
 import Test.Cardano.Ledger.Conformance.ExecSpecRule.Conway.Deleg as X (nameDelegCert)
 import Test.Cardano.Ledger.Conformance.ExecSpecRule.Conway.Gov as X ()
 import Test.Cardano.Ledger.Conformance.ExecSpecRule.Conway.GovCert as X (nameGovCert)
-import Test.Cardano.Ledger.Conformance.ExecSpecRule.Conway.Ledger as X ()
+import Test.Cardano.Ledger.Conformance.ExecSpecRule.Conway.Ledger as X (
+  ConwayLedgerExecContext (..),
+ )
 import Test.Cardano.Ledger.Conformance.ExecSpecRule.Conway.Ledgers as X ()
 import Test.Cardano.Ledger.Conformance.ExecSpecRule.Conway.Pool as X (namePoolCert)
 import Test.Cardano.Ledger.Conformance.ExecSpecRule.Conway.Utxo as X ()

diff --git a/...dano-ledger-conformance/src/Test/Cardano/Ledger/Conformance/ExecSpecRule/Conway/Ledger.hs b/...dano-ledger-conformance/src/Test/Cardano/Ledger/Conformance/ExecSpecRule/Conway/Ledger.hs
@@ -13,7 +13,7 @@
 {-# LANGUAGE UndecidableInstances #-}
 {-# OPTIONS_GHC -Wno-orphans #-}
 
-module Test.Cardano.Ledger.Conformance.ExecSpecRule.Conway.Ledger () where
+module Test.Cardano.Ledger.Conformance.ExecSpecRule.Conway.Ledger (ConwayLedgerExecContext (..)) where
 
 import Data.Bifunctor (Bifunctor (..))
 import Data.Functor.Identity (Identity)

diff --git a/libs/cardano-ledger-conformance/src/Test/Cardano/Ledger/Conformance/ExecSpecRule/Core.hs b/libs/cardano-ledger-conformance/src/Test/Cardano/Ledger/Conformance/ExecSpecRule/Core.hs
@@ -21,6 +21,8 @@ module Test.Cardano.Ledger.Conformance.ExecSpecRule.Core (
   checkConformance,
   defaultTestConformance,
   translateWithContext,
+  ForAllExecSpecRep,
+  ForAllExecTypes,
 ) where
 
 import Cardano.Ledger.BaseTypes (Inject (..), ShelleyBase)

diff --git a/libs/cardano-ledger-conformance/test/Main.hs b/libs/cardano-ledger-conformance/test/Main.hs
@@ -1,5 +1,4 @@
 {-# LANGUAGE DataKinds #-}
-{-# LANGUAGE TypeApplications #-}
 
 module Main (main) where