Fixed issues with Imp conformance testing

cabal.project

@@ -20,12 +20,12 @@ repository cardano-haskell-packages
 -- $ nix-prefetch-git https://github.com/intersectmbo/formal-ledger-specifications --rev <GIT_SHA> | jq .hash
 source-repository-package
   type: git
-  location: https://github.com/IntersectMBO/formal-ledger-specifications.git
+  location: https://github.com/Soupstraw/exec-spec-temporary.git
   -- !WARNING!:
   -- MAKE SURE THIS POINTS TO A COMMIT IN `MAlonzo-code` BEFORE MERGE!
-  subdir: generated
-  tag: cc93692f5a57a9a66956b232662152676f659954
-  --sha256: sha256-s9ikqfXmz1wBrk4qEFR/iOloKvMOPGTB5IpHO34NSLE=
+  --subdir: generated
+  tag: 504e735a709fd7704409b2d76a3fe3abb7483061
+  --sha256: sha256-8xgfT5KCfzKjry3RSjn9u/oqZbbKIAZzBNPcCdkfYT4=
 -- NOTE: If you would like to update the above, look for the `MAlonzo-code`
 -- branch in the `formal-ledger-specifications` repo and copy the SHA of
 -- the commit you need. The `MAlonzo-code` branch functions like an alternative

eras/shelley/impl/CHANGELOG.md

@@ -48,6 +48,7 @@
 
 ### `testlib`
 
+* Add `runSTS`
 * Add `iteExpectLedgerRuleConformance` to `ImpTestEnv` for additionally checking conformance with ImpTests. #4748
   * Add lens `iteExpectLedgerRuleConformanceL`.
   * Add `modifyImpInitExpectLedgerRuleConformance`.

eras/shelley/impl/testlib/Test/Cardano/Ledger/Shelley/ImpTest.hs

@@ -6,6 +6,7 @@
 {-# LANGUAGE FunctionalDependencies #-}
 {-# LANGUAGE GADTs #-}
 {-# LANGUAGE ImplicitParams #-}
+{-# LANGUAGE ImpredicativeTypes #-}
 {-# LANGUAGE LambdaCase #-}
 {-# LANGUAGE NamedFieldPuns #-}
 {-# LANGUAGE NumericUnderscores #-}
@@ -632,14 +633,14 @@ modifyImpInitProtVer ver =
 
 modifyImpInitExpectLedgerRuleConformance ::
   forall era.
-  ShelleyEraImp era =>
-  ( Either
+  ( forall t.
+    Either
       (NonEmpty (PredicateFailure (EraRule "LEDGER" era)))
       (State (EraRule "LEDGER" era), [Event (EraRule "LEDGER" era)]) ->
     LedgerEnv era ->
     LedgerState era ->
     Tx era ->
-    Expectation
+    ImpM t ()
   ) ->
   SpecWith (ImpInit (LedgerSpec era)) ->
   SpecWith (ImpInit (LedgerSpec era))
@@ -702,7 +703,7 @@ instance
           , sgNetworkId = Testnet
           , sgActiveSlotsCoeff = 20 %! 100 -- Mainnet value: 5 %! 100
           , sgSecurityParam = 108 -- Mainnet value: 2160
-          , sgEpochLength = 4320 -- Mainnet value: 432000
+          , sgEpochLength = 100 -- Mainnet value: 432000
           , sgSlotsPerKESPeriod = 129600
           , sgMaxKESEvolutions = 62
           , sgSlotLength = 1
@@ -792,13 +793,18 @@ impWitsVKeyNeeded txBody = do
 data ImpTestEnv era = ImpTestEnv
   { iteFixup :: Tx era -> ImpTestM era (Tx era)
   , iteExpectLedgerRuleConformance ::
+      forall t.
       Either
         (NonEmpty (PredicateFailure (EraRule "LEDGER" era)))
         (State (EraRule "LEDGER" era), [Event (EraRule "LEDGER" era)]) ->
       LedgerEnv era ->
       LedgerState era ->
       Tx era ->
-      Expectation
+      ImpM t ()
+      -- ^ Note the use of higher ranked types here. This prevents the hook from
+      -- accessing the state while still permitting the use of more general
+      -- functions that return some `ImpM t a` and that don't constrain the
+      -- state in any way (e.g. `logString`, `shouldBe` are still fine to use).
   , iteCborRoundTripFailures :: !Bool
   -- ^ Expect failures in CBOR round trip serialization tests for predicate failures
   }
@@ -807,15 +813,17 @@ iteFixupL :: Lens' (ImpTestEnv era) (Tx era -> ImpTestM era (Tx era))
 iteFixupL = lens iteFixup (\x y -> x {iteFixup = y})
 
 iteExpectLedgerRuleConformanceL ::
+  forall era.
   Lens'
     (ImpTestEnv era)
-    ( Either
+    ( forall t.
+      Either
         (NonEmpty (PredicateFailure (EraRule "LEDGER" era)))
         (State (EraRule "LEDGER" era), [Event (EraRule "LEDGER" era)]) ->
       LedgerEnv era ->
       LedgerState era ->
       Tx era ->
-      Expectation
+      ImpM t ()
     )
 iteExpectLedgerRuleConformanceL = lens iteExpectLedgerRuleConformance (\x y -> x {iteExpectLedgerRuleConformance = y})
 
@@ -1080,7 +1088,7 @@ trySubmitTx tx = do
 
   -- Check for conformance
   asks iteExpectLedgerRuleConformance
-    >>= (\f -> liftIO $ f res lEnv (st ^. nesEsL . esLStateL) txFixed)
+    >>= (\f -> f res lEnv (st ^. nesEsL . esLStateL) txFixed)
 
   case res of
     Left predFailures -> do
@@ -1291,7 +1299,7 @@ passNEpochsChecking n checks =
   replicateM_ (fromIntegral n) $ passEpoch >> checks
 
 -- | Adds a ToExpr to the log, which is only shown if the test fails
-logToExpr :: (HasCallStack, ToExpr a) => a -> ImpTestM era ()
+logToExpr :: (HasCallStack, ToExpr a) => a -> ImpM t ()
 logToExpr = logWithCallStack ?callStack . ansiWlExpr . toExpr
 
 -- | Adds the result of an action to the log, which is only shown if the test fails

eras/shelley/test-suite/src/Test/Cardano/Ledger/Shelley/Utils.hs

@@ -28,6 +28,7 @@ module Test.Cardano.Ledger.Shelley.Utils (
   runShelleyBase,
   maxKESIterations,
   slotsPerKESIteration,
+  runSTS,
   testSTS,
   maxLLSupply,
   applySTSTest,
@@ -85,7 +86,7 @@ import Cardano.Slotting.EpochInfo (
   epochInfoSize,
  )
 import Control.Monad.Reader.Class (asks)
-import Control.Monad.Trans.Reader (runReaderT)
+import Control.Monad.Trans.Reader (runReader, runReaderT)
 import Control.State.Transition.Extended hiding (Assertion)
 import Data.Coerce (Coercible, coerce)
 import Data.Functor.Identity (runIdentity)
@@ -237,6 +238,29 @@ slotsPerKESIteration = runShelleyBase (asks slotsPerKESPeriod)
 maxLLSupply :: Coin
 maxLLSupply = Coin $ fromIntegral $ runShelleyBase (asks maxLovelaceSupply)
 
+runSTS ::
+  forall rule era.
+  ( BaseM (EraRule rule era) ~ ShelleyBase
+  , STS (EraRule rule era)
+  ) =>
+  Globals ->
+  Environment (EraRule rule era) ->
+  State (EraRule rule era) ->
+  Signal (EraRule rule era) ->
+  Either
+    (NonEmpty (PredicateFailure (EraRule rule era)))
+    (State (EraRule rule era), [Event (EraRule rule era)])
+runSTS globals env st sig =
+  let
+    stsOpts =
+      ApplySTSOpts
+        { asoValidation = ValidateAll
+        , asoEvents = EPReturn
+        , asoAssertions = AssertionsAll
+        }
+   in
+    (`runReader` globals) (applySTSOptsEither @(EraRule rule era) stsOpts (TRC (env, st, sig)))
+
 testSTS ::
   forall s.
   (BaseM s ~ ShelleyBase, STS s, Eq (State s), Show (State s), ToExpr (State s)) =>

libs/cardano-ledger-conformance/cardano-ledger-conformance.cabal

@@ -26,10 +26,11 @@ library
         Test.Cardano.Ledger.Conformance.ExecSpecRule.Conway
         Test.Cardano.Ledger.Conformance.ExecSpecRule.Conway.Base
         Test.Cardano.Ledger.Conformance.SpecTranslate.Conway
+        Test.Cardano.Ledger.Conformance.Utils
+        Test.Cardano.Ledger.Conformance.SpecTranslate.Conway.Base
 
     hs-source-dirs:   src
     other-modules:
-        Test.Cardano.Ledger.Conformance.SpecTranslate.Conway.Base
         Test.Cardano.Ledger.Conformance.SpecTranslate.Conway.Deleg
         Test.Cardano.Ledger.Conformance.SpecTranslate.Conway.Pool
         Test.Cardano.Ledger.Conformance.SpecTranslate.Conway.Cert
@@ -51,7 +52,6 @@ library
         Test.Cardano.Ledger.Conformance.ExecSpecRule.Conway.Ledger
         Test.Cardano.Ledger.Conformance.ExecSpecRule.Conway.Ledgers
         Test.Cardano.Ledger.Conformance.Orphans
-        Test.Cardano.Ledger.Conformance.Utils
 
     default-language: Haskell2010
     ghc-options:
@@ -123,11 +123,11 @@ test-suite tests
         cardano-ledger-conformance,
         cardano-ledger-core:{cardano-ledger-core, testlib},
         cardano-strict-containers,
+        cardano-ledger-executable-spec,
         cardano-ledger-shelley,
         cardano-ledger-alonzo,
         cardano-ledger-conway:{cardano-ledger-conway, testlib},
         cardano-ledger-test,
         cardano-ledger-executable-spec,
         microlens,
-        unliftio,
-        text
+        unliftio

libs/cardano-ledger-conformance/src/Test/Cardano/Ledger/Conformance/ExecSpecRule/Conway/Ledger.hs

@@ -3,6 +3,7 @@
 {-# LANGUAGE FlexibleContexts #-}
 {-# LANGUAGE FlexibleInstances #-}
 {-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE NamedFieldPuns #-}
 {-# LANGUAGE OverloadedStrings #-}
 {-# LANGUAGE RankNTypes #-}
 {-# LANGUAGE RecordWildCards #-}
@@ -59,14 +60,16 @@ import Constrained (
 
 import Cardano.Ledger.Binary (EncCBOR (..))
 import Cardano.Ledger.Binary.Coders (Encode (..), encode, (!>))
-import Cardano.Ledger.Shelley.Rules (UtxoEnv (..))
+import Cardano.Ledger.Shelley.LedgerState (LedgerState (..))
+import Cardano.Ledger.Shelley.Rules (LedgerEnv (..), UtxoEnv (..))
 import Data.Bitraversable (bimapM)
 import qualified Data.Text as T
 import GHC.Generics (Generic)
 import qualified Lib as Agda
 import Test.Cardano.Ledger.Common (Arbitrary (..), NFData, Testable (..), ToExpr, ansiExpr)
 import Test.Cardano.Ledger.Conformance.ExecSpecRule.Conway.Base (enactStateSpec)
 import Test.Cardano.Ledger.Conformance.ExecSpecRule.Conway.Utxo (genUtxoExecContext)
+import Test.Cardano.Ledger.Conformance.ExecSpecRule.Conway.Utxow ()
 import Test.Cardano.Ledger.Conway.ImpTest (impAnn, logDoc, tryRunImpRuleNoAssertions)
 import Test.Cardano.Ledger.Imp.Common (expectRightExpr)
 import UnliftIO (evaluateDeep)
@@ -151,6 +154,22 @@ instance
       . computationResultToEither
       $ Agda.ledgerStep env st sig
 
+  extraInfo
+    ConwayLedgerExecContext {..}
+    LedgerEnv {..}
+    LedgerState {..}
+    sig
+    _ =
+      extraInfo @fn @"UTXOW" @Conway
+        clecUtxoExecContext
+        utxoEnv
+        lsUTxOState
+        sig
+        stFinal
+      where
+        utxoEnv = UtxoEnv ledgerSlotNo ledgerPp lsCertState
+        stFinal = runSTS @"UTXOW" @Conway testGlobals utxoEnv lsUTxOState sig
+
   testConformance ctx env st sig = property $ do
     (specEnv, specSt, specSig) <-
       impAnn "Translating the inputs" $

libs/cardano-ledger-conformance/src/Test/Cardano/Ledger/Conformance/ExecSpecRule/Conway/Utxow.hs

@@ -4,7 +4,7 @@
 {-# LANGUAGE FlexibleInstances #-}
 {-# LANGUAGE MultiParamTypeClasses #-}
 {-# LANGUAGE OverloadedStrings #-}
-{-# LANGUAGE RecordWildCards #-}
+{-# LANGUAGE ScopedTypeVariables #-}
 {-# LANGUAGE TypeApplications #-}
 {-# LANGUAGE TypeFamilies #-}
 {-# LANGUAGE UndecidableInstances #-}
@@ -19,11 +19,14 @@ import Data.Bifunctor (Bifunctor (..))
 import qualified Data.List.NonEmpty as NE
 import qualified Data.Text as T
 import qualified Lib as Agda
+import qualified Prettyprinter as PP
 import Test.Cardano.Ledger.Conformance (
   ExecSpecRule (..),
   OpaqueErrorString (..),
   SpecTranslate,
   computationResultToEither,
+  runSpecTransM,
+  toSpecRep,
  )
 import Test.Cardano.Ledger.Conformance.ExecSpecRule.Conway.Base (externalFunctions)
 import Test.Cardano.Ledger.Conformance.ExecSpecRule.Conway.Utxo (genUtxoExecContext)
@@ -38,6 +41,8 @@ import Test.Cardano.Ledger.Constrained.Conway (
   utxoStateSpec,
   utxoTxSpec,
  )
+import qualified Test.Cardano.Ledger.Generic.PrettyCore as PP
+import Test.Cardano.Ledger.Shelley.Utils (runSTS, testGlobals)
 
 instance
   ( IsConwayUniv fn
@@ -55,3 +60,21 @@ instance
     first (\e -> OpaqueErrorString (T.unpack e) NE.:| [])
       . computationResultToEither
       $ Agda.utxowStep externalFunctions env st sig
+  extraInfo ctx env st sig _ =
+    let
+      result =
+        either show T.unpack . runSpecTransM ctx $
+          Agda.utxowDebug externalFunctions
+            <$> toSpecRep env
+            <*> toSpecRep st
+            <*> toSpecRep sig
+      stFinal = runSTS @"UTXO" @Conway testGlobals env st sig
+      utxoInfo = extraInfo @fn @"UTXO" @Conway ctx env st sig stFinal
+     in
+      PP.vcat
+        [ "UTXOW"
+        , PP.ppString result
+        , mempty
+        , "UTXO"
+        , utxoInfo
+        ]

libs/cardano-ledger-conformance/src/Test/Cardano/Ledger/Conformance/ExecSpecRule/Core.hs

@@ -23,6 +23,7 @@ module Test.Cardano.Ledger.Conformance.ExecSpecRule.Core (
   translateWithContext,
   ForAllExecSpecRep,
   ForAllExecTypes,
+  diffConformance,
 ) where
 
 import Cardano.Ledger.BaseTypes (Inject (..), ShelleyBase)
@@ -234,6 +235,18 @@ dumpCbor path x name = do
   fullPath <- makeAbsolute $ path <> "/" <> name <.> "cbor"
   writeCBOR (eraProtVerLow @era) fullPath x
 
+diffConformance :: ToExpr a => a -> a -> Doc AnsiStyle
+diffConformance implRes agdaRes =
+  ppEditExpr conformancePretty (ediff implRes agdaRes)
+  where
+    delColor = Red
+    insColor = Magenta
+    conformancePretty =
+      ansiWlPretty
+        { ppDel = annotate (color delColor) . parens . ("Impl: " <>)
+        , ppIns = annotate (color insColor) . parens . ("Agda: " <>)
+        }
+
 checkConformance ::
   forall rule era fn.
   ( Era era
@@ -260,17 +273,10 @@ checkConformance ::
   ImpTestM era ()
 checkConformance ctx env st sig implResTest agdaResTest = do
   let
-    delColor = Red
-    insColor = Magenta
-    conformancePretty =
-      ansiWlPretty
-        { ppDel = annotate (color delColor) . parens . ("Impl: " <>)
-        , ppIns = annotate (color insColor) . parens . ("Agda: " <>)
-        }
     failMsg =
       annotate (color Yellow) . vsep $
         [ "===== DIFF ====="
-        , ppEditExpr conformancePretty (ediff implResTest agdaResTest)
+        , diffConformance implResTest agdaResTest
         ]
   unless (implResTest == agdaResTest) $ do
     let envVarName = "CONFORMANCE_CBOR_DUMP_PATH"

libs/cardano-ledger-conformance/src/Test/Cardano/Ledger/Conformance/Orphans.hs

@@ -98,6 +98,8 @@ instance NFData TxBody
 
 instance NFData Tag
 
+instance NFData HSVKey
+
 instance NFData TxWitnesses
 
 instance NFData Tx
@@ -196,6 +198,8 @@ instance ToExpr TxBody
 
 instance ToExpr Tag
 
+instance ToExpr HSVKey
+
 instance ToExpr TxWitnesses
 
 instance ToExpr Tx

libs/cardano-ledger-conformance/src/Test/Cardano/Ledger/Conformance/SpecTranslate/Conway/Base.hs

@@ -448,18 +448,20 @@ signatureFromInteger :: DSIGNAlgorithm v => Integer -> Maybe (SigDSIGN v)
 signatureFromInteger = rawDeserialiseSigDSIGN . naturalToBytes 64 . fromInteger
 
 instance Crypto c => SpecTranslate ctx (VKey k c) where
-  type SpecRep (VKey k c) = Integer
+  type SpecRep (VKey k c) = Agda.HSVKey
 
-  toSpecRep = pure . vkeyToInteger
+  toSpecRep x = do
+    let hvkVKey = vkeyToInteger x
+    hvkStoredHash <- toSpecRep (hashVerKeyDSIGN @_ @(ADDRHASH c) $ unVKey x)
+    pure Agda.MkHSVKey {..}
 
 instance DSIGNAlgorithm v => SpecTranslate ctx (SignedDSIGN v a) where
   type SpecRep (SignedDSIGN v a) = Integer
 
-  toSpecRep (SignedDSIGN x) =
-    pure . toInteger . bytesToNatural $ rawSerialiseSigDSIGN x
+  toSpecRep (SignedDSIGN x) = pure $ signatureToInteger x
 
 instance (Crypto c, Typeable k) => SpecTranslate ctx (WitVKey k c) where
-  type SpecRep (WitVKey k c) = (Integer, Integer)
+  type SpecRep (WitVKey k c) = (SpecRep (VKey k c), Integer)
 
   toSpecRep (WitVKey vk sk) = toSpecRep (vk, sk)