Fix issues that prevent basic sumbitTx from passing conformance

cabal.project

@@ -24,8 +24,8 @@ source-repository-package
   -- !WARNING!:
   -- MAKE SURE THIS POINTS TO A COMMIT IN `MAlonzo-code` BEFORE MERGE!
   subdir: generated
-  tag: cc93692f5a57a9a66956b232662152676f659954
-  --sha256: sha256-s9ikqfXmz1wBrk4qEFR/iOloKvMOPGTB5IpHO34NSLE=
+  tag: be51adff014214c15fed718d396bb8a6d955f9e1
+  --sha256: sha256-by921yC1MaZI58kyrtEGGKqmt9jMnVsPLfQtP4raJPw=
 -- 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

@@ -302,7 +302,7 @@ instance ShelleyEraImp era => ImpSpec (LedgerSpec era) where
             ImpTestEnv
               { iteFixup = fixupTx
               , iteCborRoundTripFailures = True
-              , iteExpectLedgerRuleConformance = \_ _ _ _ -> pure ()
+              , iteExpectLedgerRuleConformance = \_ _ _ _ _ -> pure ()
               }
         , impInitState = initState
         }
@@ -632,8 +632,8 @@ modifyImpInitProtVer ver =
 
 modifyImpInitExpectLedgerRuleConformance ::
   forall era.
-  ShelleyEraImp era =>
-  ( Either
+  ( Globals ->
+    Either
       (NonEmpty (PredicateFailure (EraRule "LEDGER" era)))
       (State (EraRule "LEDGER" era), [Event (EraRule "LEDGER" era)]) ->
     LedgerEnv era ->
@@ -792,13 +792,18 @@ impWitsVKeyNeeded txBody = do
 data ImpTestEnv era = ImpTestEnv
   { iteFixup :: Tx era -> ImpTestM era (Tx era)
   , iteExpectLedgerRuleConformance ::
+      Globals ->
       Either
         (NonEmpty (PredicateFailure (EraRule "LEDGER" era)))
         (State (EraRule "LEDGER" era), [Event (EraRule "LEDGER" era)]) ->
       LedgerEnv era ->
       LedgerState era ->
       Tx era ->
       Expectation
+  -- ^ 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,9 +812,11 @@ 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
+    ( Globals ->
+      Either
         (NonEmpty (PredicateFailure (EraRule "LEDGER" era)))
         (State (EraRule "LEDGER" era), [Event (EraRule "LEDGER" era)]) ->
       LedgerEnv era ->
@@ -1077,10 +1084,11 @@ trySubmitTx tx = do
   ImpTestState {impRootTxIn} <- get
   res <- tryRunImpRule @"LEDGER" lEnv (st ^. nesEsL . esLStateL) txFixed
   roundTripCheck <- asks iteCborRoundTripFailures
+  globals <- use impGlobalsL
 
   -- Check for conformance
   asks iteExpectLedgerRuleConformance
-    >>= (\f -> liftIO $ f res lEnv (st ^. nesEsL . esLStateL) txFixed)
+    >>= (\f -> liftIO $ f globals 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:
@@ -66,6 +66,7 @@ library
         cardano-strict-containers,
         data-default,
         microlens,
+        microlens-mtl,
         mtl,
         cardano-ledger-api:testlib,
         cardano-ledger-binary:{cardano-ledger-binary, testlib},
@@ -123,11 +124,12 @@ 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
+        microlens-mtl,
+        unliftio

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

@@ -408,7 +408,7 @@ instance IsConwayUniv fn => ExecSpecRule fn "RATIFY" Conway where
       . computationResultToEither
       $ Agda.ratifyStep env st sig
 
-  extraInfo ctx env@RatifyEnv {..} st sig@(RatifySignal actions) _ =
+  extraInfo _ ctx env@RatifyEnv {..} st sig@(RatifySignal actions) _ =
     PP.vsep $ specExtraInfo : (actionAcceptedRatio <$> toList actions)
     where
       members = foldMap' (committeeMembers @Conway) $ ensCommittee (rsEnactState st)

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

@@ -59,16 +59,20 @@ 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 Lens.Micro.Mtl (use)
 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.Conway.ImpTest (impAnn, logDoc, tryRunImpRuleNoAssertions)
+import Test.Cardano.Ledger.Conformance.ExecSpecRule.Conway.Utxow ()
+import Test.Cardano.Ledger.Conway.ImpTest (impAnn, impGlobalsL, logDoc, tryRunImpRuleNoAssertions)
 import Test.Cardano.Ledger.Imp.Common (expectRightExpr)
+import Test.Cardano.Ledger.Shelley.Utils (runSTS)
 import UnliftIO (evaluateDeep)
 
 data ConwayLedgerExecContext era
@@ -151,6 +155,24 @@ instance
       . computationResultToEither
       $ Agda.ledgerStep env st sig
 
+  extraInfo
+    globals
+    ConwayLedgerExecContext {..}
+    LedgerEnv {..}
+    LedgerState {..}
+    sig
+    _ =
+      extraInfo @fn @"UTXOW" @Conway
+        globals
+        clecUtxoExecContext
+        utxoEnv
+        lsUTxOState
+        sig
+        stFinal
+      where
+        utxoEnv = UtxoEnv ledgerSlotNo ledgerPp lsCertState
+        stFinal = runSTS @"UTXOW" @Conway globals utxoEnv lsUTxOState sig
+
   testConformance ctx env st sig = property $ do
     (specEnv, specSt, specSig) <-
       impAnn "Translating the inputs" $
@@ -175,7 +197,8 @@ instance
         expectRightExpr $
           runSpecTransM ctx $
             bimapM (traverse toTestRep) (toTestRep . inject @_ @(ExecState fn "LEDGER" Conway) . fst) implRes
-    let extra = extraInfo @fn @"LEDGER" @Conway ctx (inject env) (inject st) (inject sig) implRes
+    globals <- use impGlobalsL
+    let extra = extraInfo @fn @"LEDGER" @Conway globals ctx (inject env) (inject st) (inject sig) implRes
     logDoc extra
     checkConformance @"LEDGER" @Conway @fn
       ctx

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

@@ -103,7 +103,7 @@ instance
       . computationResultToEither
       $ Agda.utxoStep externalFunctions env st sig
 
-  extraInfo ctx env@UtxoEnv {..} st@UTxOState {..} sig st' =
+  extraInfo _ ctx env@UtxoEnv {..} st@UTxOState {..} sig st' =
     PP.vcat
       [ "Impl:"
       , PP.ppString (showConwayTxBalance uePParams ueCertState utxosUtxo sig)

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)
 
 instance
   ( IsConwayUniv fn
@@ -55,3 +60,21 @@ instance
     first (\e -> OpaqueErrorString (T.unpack e) NE.:| [])
       . computationResultToEither
       $ Agda.utxowStep externalFunctions env st sig
+  extraInfo globals 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 globals env st sig
+      utxoInfo = extraInfo @fn @"UTXO" @Conway globals 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,9 +23,10 @@ module Test.Cardano.Ledger.Conformance.ExecSpecRule.Core (
   translateWithContext,
   ForAllExecSpecRep,
   ForAllExecTypes,
+  diffConformance,
 ) where
 
-import Cardano.Ledger.BaseTypes (Inject (..), ShelleyBase)
+import Cardano.Ledger.BaseTypes (Globals, Inject (..), ShelleyBase)
 import Cardano.Ledger.Binary (EncCBOR)
 import Cardano.Ledger.Core (Era, EraRule, eraProtVerLow)
 import qualified Constrained as CV2
@@ -42,6 +43,7 @@ import qualified Data.Text as T
 import Data.Typeable (Proxy (..), Typeable, typeRep)
 import GHC.Base (Constraint, NonEmpty, Symbol, Type)
 import GHC.TypeLits (KnownSymbol)
+import Lens.Micro.Mtl (use)
 import Prettyprinter
 import Prettyprinter.Render.Terminal
 import System.FilePath ((<.>))
@@ -58,6 +60,7 @@ import Test.Cardano.Ledger.Shelley.ImpTest (
   ImpTestM,
   ShelleyEraImp,
   impAnn,
+  impGlobalsL,
   logDoc,
   tryRunImpRule,
  )
@@ -211,6 +214,7 @@ class
 
   extraInfo ::
     HasCallStack =>
+    Globals ->
     ExecContext fn rule era ->
     Environment (EraRule rule era) ->
     State (EraRule rule era) ->
@@ -234,6 +238,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 +276,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"
@@ -317,7 +326,8 @@ defaultTestConformance ::
   Property
 defaultTestConformance ctx env st sig = property $ do
   (implResTest, agdaResTest, implRes) <- runConformance @rule @fn @era ctx env st sig
-  let extra = extraInfo @fn @rule @era ctx (inject env) (inject st) (inject sig) implRes
+  globals <- use impGlobalsL
+  let extra = extraInfo @fn @rule @era globals ctx (inject env) (inject st) (inject sig) implRes
   logDoc extra
   checkConformance @rule @_ @fn ctx (inject env) (inject st) (inject sig) implResTest agdaResTest