Update libs/cardano-ledger-conformance/src/Test/Cardano/Ledger/Confor…

…mance/ExecSpecRule/Core.hs

Co-authored-by: Alexey Kuleshevich <[email protected]>

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

@@ -576,7 +576,7 @@ instance
   Testable (ImpTestM era a)
   where
   property m = property . fmap ioProperty . runGenT $ do
-    res <- liftGen $ runImpTestGenM mkImpState m
+    res <- liftGen $ runImpTestGenM def m
     liftIO $ fst <$> res
 
 instance MonadWriter [SomeSTSEvent era] (ImpTestM era) where
@@ -1117,20 +1117,20 @@ logEntry e = impLogL %= (<> pretty loc <> "\t" <> pretty e <> line)
 logToExpr :: (HasCallStack, ToExpr a) => a -> ImpTestM era ()
 logToExpr e = logEntry (showExpr e)
 
-mkImpState :: ShelleyEraImp era => ImpTestState era
-mkImpState =
-  ImpTestState
-    { impNES = initShelleyImpNES
-    , impRootTxIn = TxIn (mkTxId 0) minBound
-    , impKeyPairs = mempty
-    , impByronKeyPairs = mempty
-    , impNativeScripts = mempty
-    , impLastTick = 0
-    , impGlobals = testGlobals
-    , impLog = mempty
-    , impGen = mkQCGen 2024
-    , impEvents = mempty
-    }
+instance ShelleyEraImp era => Default (ImpTestState era) where
+  def =
+    ImpTestState
+      { impNES = initShelleyImpNES
+      , impRootTxIn = TxIn (mkTxId 0) minBound
+      , impKeyPairs = mempty
+      , impByronKeyPairs = mempty
+      , impNativeScripts = mempty
+      , impLastTick = 0
+      , impGlobals = testGlobals
+      , impLog = mempty
+      , impGen = mkQCGen 2024
+      , impEvents = mempty
+      }
 
 withImpState ::
   ShelleyEraImp era =>
@@ -1146,7 +1146,7 @@ withImpStateModified ::
   Spec
 withImpStateModified f =
   beforeAll $
-    execImpTestM Nothing (f mkImpState) $
+    execImpTestM Nothing (f def) $
       addRootTxOut >> initImpTestState
   where
     rootCoin = Coin 1_000_000_000
@@ -1155,7 +1155,7 @@ withImpStateModified f =
       let rootAddr = Addr Testnet (KeyHashObj rootKeyHash) StakeRefNull
           rootTxOut = mkBasicTxOut rootAddr $ inject rootCoin
       impNESL . nesEsL . esLStateL . lsUTxOStateL . utxosUtxoL
-        %= (<> UTxO (Map.singleton (impRootTxIn @era mkImpState) rootTxOut))
+        %= (<> UTxO (Map.singleton (impRootTxIn @era def) rootTxOut))
 
 -- | Creates a fresh @SafeHash@
 freshSafeHash :: Era era => ImpTestM era (SafeHash (EraCrypto era) a)

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

@@ -21,7 +21,9 @@ flag asserts
 library
     exposed-modules:
         Test.Cardano.Ledger.Conformance
+        Test.Cardano.Ledger.Conformance.ConformanceSpec
         Test.Cardano.Ledger.Conformance.Spec.Conway
+        Test.Cardano.Ledger.Conformance.Utils
 
     hs-source-dirs:   src
     other-modules:
@@ -39,6 +41,7 @@ library
 
     build-depends:
         base >=4.14 && <5,
+        base16-bytestring,
         cardano-data,
         cardano-strict-containers,
         data-default-class,
@@ -80,4 +83,4 @@ test-suite tests
     build-depends:
         base >=4.14 && <5,
         cardano-ledger-conformance,
-        cardano-ledger-core:testlib
+        cardano-ledger-core:{testlib}

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

@@ -0,0 +1,24 @@
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE TypeApplications #-}
+
+module Test.Cardano.Ledger.Conformance.ConformanceSpec (spec) where
+
+import Cardano.Ledger.Crypto (StandardCrypto)
+import Cardano.Ledger.Keys (KeyHash, KeyRole (..))
+import Data.List (isInfixOf)
+import Test.Cardano.Ledger.Common
+import Test.Cardano.Ledger.Conformance (SpecTranslate (..), runSpecTransM)
+import Test.Cardano.Ledger.Conformance.Spec.Conway ()
+import Test.Cardano.Ledger.Conformance.Utils (agdaHashToBytes)
+
+spec :: Spec
+spec =
+  describe "Translation" $ do
+    prop "Hashes are displayed in the same way in the implementation and in the spec" $ do
+      someHash <- arbitrary @(KeyHash 'Staking StandardCrypto)
+      let
+        specRes =
+          case runSpecTransM () (toTestRep someHash) of
+            Left e -> error $ "Failed to translate hash: " <> show e
+            Right x -> agdaHashToBytes x
+      pure $ show specRes `isInfixOf` showExpr someHash

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

@@ -36,8 +36,6 @@ import Cardano.Ledger.Conway.Tx (AlonzoTx)
 import Cardano.Ledger.Crypto (StandardCrypto)
 import Cardano.Ledger.TxIn (TxId)
 import Constrained
-import Control.DeepSeq (NFData)
-import Control.Monad (unless)
 import Control.Monad.Identity (Identity)
 import Data.Bifunctor (Bifunctor (..))
 import Data.Default.Class (Default (..))
@@ -52,6 +50,7 @@ import qualified Lib as Agda
 import Test.Cardano.Ledger.Conformance (
   ExecSpecRule (..),
   SpecTranslate (..),
+  checkConformance,
   computationResultToEither,
   runConformance,
   runSpecTransM,
@@ -71,16 +70,7 @@ import Test.Cardano.Ledger.Constrained.Conway (
   utxoTxSpec,
  )
 import Test.Cardano.Ledger.Conway.ImpTest (impAnn, logEntry)
-import Test.Cardano.Ledger.Imp.Common (
-  Testable (..),
-  ToExpr,
-  arbitrary,
-  diffExpr,
-  expectRight,
-  expectationFailure,
-  label,
-  showExpr,
- )
+import Test.Cardano.Ledger.Imp.Common hiding (forAll, prop)
 
 data ConwayGovTransContext era
   = ConwayGovTransContext
@@ -287,18 +277,7 @@ instance
 
   testConformance env st sig = property $ do
     (implResTest, agdaResTest) <- runConformance @"GOV" @fn @Conway env st sig
-    let
-      failMsg =
-        unlines
-          [ ""
-          , "===== DIFF ====="
-          , diffExpr implResTest agdaResTest
-          , ""
-          , "Legend:"
-          , "\t\ESC[91mImplemenation"
-          , "\t\ESC[92mSpecification\ESC[39m"
-          ]
-    unless (implResTest == agdaResTest) $ expectationFailure failMsg
+    checkConformance @"GOV" implResTest agdaResTest
     let numInputProps = OSet.size $ gpProposalProcedures sig
     pure $ label ("n input proposals = " <> show numInputProps) ()
 

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

@@ -16,6 +16,7 @@ module Test.Cardano.Ledger.Conformance.ExecSpecRule.Core (
   computationResultToEither,
   generatesWithin,
   runConformance,
+  checkConformance,
 ) where
 
 import Cardano.Ledger.BaseTypes (ShelleyBase)
@@ -26,29 +27,12 @@ import Control.State.Transition.Extended (STS (..))
 import Data.Bifunctor (Bifunctor (..))
 import Data.Bitraversable (bimapM)
 import Data.Functor (($>))
-import Data.Typeable (Proxy (..), Typeable, showsTypeRep, typeRep)
+import Data.Typeable (Proxy (..), Typeable, typeRep)
 import GHC.Base (Constraint, NonEmpty, Symbol, Type)
 import GHC.TypeLits (KnownSymbol)
 import qualified Lib as Agda
-import Test.Cardano.Ledger.Common (Arbitrary (..), Gen, Testable (..), forAllShow)
 import Test.Cardano.Ledger.Conformance.SpecTranslate.Core (SpecTranslate (..), runSpecTransM)
-import Test.Cardano.Ledger.Imp.Common (
-  MonadGen (..),
-  NFData,
-  Property,
-  Spec,
-  ToExpr,
-  diffExpr,
-  expectRight,
-  expectRightExpr,
-  expectationFailure,
-  forAllShrinkShow,
-  ioProperty,
-  prop,
-  showExpr,
-  unless,
-  within,
- )
+import Test.Cardano.Ledger.Imp.Common
 import Test.Cardano.Ledger.Shelley.ImpTest (
   ImpTestM,
   ShelleyEraImp,
@@ -162,6 +146,33 @@ class
     Property
   testConformance = defaultTestConformance @fn @era @rule
 
+checkConformance ::
+  ( ToExpr (TestRep (PredicateFailure (EraRule rule era)))
+  , ToExpr (TestRep (State (EraRule rule era)))
+  , Eq (TestRep (PredicateFailure (EraRule rule era)))
+  , Eq (TestRep (State (EraRule rule era)))
+  ) =>
+  Either
+    (NonEmpty (TestRep (PredicateFailure (EraRule rule era))))
+    (TestRep (State (EraRule rule era))) ->
+  Either
+    (NonEmpty (TestRep (PredicateFailure (EraRule rule era))))
+    (TestRep (State (EraRule rule era))) ->
+  ImpTestM era ()
+checkConformance implResTest agdaResTest = do
+  let
+    failMsg =
+      unlines
+        [ ""
+        , "===== DIFF ====="
+        , diffExpr implResTest agdaResTest
+        , ""
+        , "Legend:"
+        , "\t\ESC[91mImplemenation"
+        , "\t\ESC[92mSpecification\ESC[39m"
+        ]
+  unless (implResTest == agdaResTest) $ expectationFailure failMsg
+
 defaultTestConformance ::
   forall fn era rule.
   ( ShelleyEraImp era
@@ -180,18 +191,7 @@ defaultTestConformance ::
   Property
 defaultTestConformance env st sig = property $ do
   (implResTest, agdaResTest) <- runConformance @rule @fn @era env st sig
-  let
-    failMsg =
-      unlines
-        [ ""
-        , "===== DIFF ====="
-        , diffExpr implResTest agdaResTest
-        , ""
-        , "Legend:"
-        , "\t\ESC[91mImplemenation"
-        , "\t\ESC[92mSpecification\ESC[39m"
-        ]
-  unless (implResTest == agdaResTest) $ expectationFailure failMsg
+  checkConformance @rule implResTest agdaResTest
 
 runConformance ::
   forall (rule :: Symbol) (fn :: [Type] -> Type -> Type) era.
@@ -276,7 +276,7 @@ generatesWithin gen timeout =
     . forAllShow gen showExpr
     $ \x -> within timeout $ ioProperty (evaluateDeep x $> ())
   where
-    aName = showsTypeRep (typeRep $ Proxy @a) ""
+    aName = show (typeRep $ Proxy @a)
 
 computationResultToEither :: Agda.ComputationResult e a -> Either e a
 computationResultToEither (Agda.Success x) = Right x

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

@@ -2,12 +2,12 @@
 {-# LANGUAGE StandaloneDeriving #-}
 {-# OPTIONS_GHC -Wno-orphans #-}
 
-module Test.Cardano.Ledger.Conformance.Orphans () where
+module Test.Cardano.Ledger.Conformance.Orphans where
 
 import GHC.Generics (Generic)
 import Lib
-import Numeric (showHex)
 import Test.Cardano.Ledger.Common (NFData, ToExpr)
+import Test.Cardano.Ledger.Conformance.Utils
 import Test.Cardano.Ledger.Conway.TreeDiff (Expr (..), ToExpr (..))
 
 deriving instance Generic GovActionState
@@ -104,14 +104,9 @@ instance NFData Tx
 
 instance NFData UTxOEnv
 
-reverseEndianness :: String -> String
-reverseEndianness (x : y : t) = reverseEndianness t <> [x, y]
-reverseEndianness (x : t) = reverseEndianness t <> ['0', x]
-reverseEndianness [] = []
-
 instance ToExpr Credential where
-  toExpr (KeyHashObj h) = App "KeyHashObj" [toExpr . reverseEndianness $ showHex h ""]
-  toExpr (ScriptObj h) = App "ScriptObj" [toExpr . reverseEndianness $ showHex h ""]
+  toExpr (KeyHashObj h) = App "KeyHashObj" [agdaHashToExpr h]
+  toExpr (ScriptObj h) = App "ScriptObj" [agdaHashToExpr h]
 
 instance ToExpr GovAction
 
@@ -120,7 +115,7 @@ instance ToExpr GovRole
 instance ToExpr Vote
 
 instance ToExpr TxId where
-  toExpr (MkTxId x) = App "TxId" [toExpr . reverseEndianness $ showHex x ""]
+  toExpr (MkTxId x) = App "TxId" [agdaHashToExpr x]
 
 instance ToExpr GovActionState
 

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

@@ -26,6 +26,7 @@ module Test.Cardano.Ledger.Conformance.SpecTranslate.Conway (
 
 import Cardano.Crypto.DSIGN (DSIGNAlgorithm (..), SignedDSIGN (..))
 import Cardano.Crypto.Hash (Hash, hashToBytes)
+import Cardano.Crypto.Util (bytesToNatural)
 import Cardano.Ledger.Address (Addr (..), RewardAccount (..), serialiseAddr)
 import Cardano.Ledger.Alonzo (AlonzoTxAuxData, MaryValue)
 import Cardano.Ledger.Alonzo.PParams (OrdExUnits (OrdExUnits))
@@ -103,7 +104,6 @@ import Cardano.Ledger.PoolParams (PoolParams (..))
 import Cardano.Ledger.SafeHash (SafeHash, extractHash)
 import Cardano.Ledger.Shelley.LedgerState (UTxOState (..))
 import Cardano.Ledger.Shelley.Rules (Identity, UtxoEnv (..))
-import Cardano.Ledger.Tools (byteStringToNum)
 import Cardano.Ledger.TxIn (TxId (..), TxIn (..))
 import Cardano.Ledger.UTxO (UTxO (..))
 import Cardano.Ledger.Val (Val (..))
@@ -167,7 +167,7 @@ instance SpecTranslate ctx (TxIn era) where
 instance SpecTranslate ctx (Addr era) where
   type SpecRep (Addr era) = Agda.Addr
 
-  toSpecRep = pure . byteStringToNum . serialiseAddr
+  toSpecRep = pure . toInteger . bytesToNatural . serialiseAddr
 
 instance SpecTranslate ctx (SafeHash c EraIndependentData) where
   type SpecRep (SafeHash c EraIndependentData) = Agda.DataHash
@@ -401,20 +401,20 @@ instance SpecTranslate ctx ValidityInterval where
 instance SpecTranslate ctx (Hash a b) where
   type SpecRep (Hash a b) = Agda.Hash
 
-  toSpecRep = pure . byteStringToNum . hashToBytes
+  toSpecRep = pure . toInteger . bytesToNatural . hashToBytes
 
 deriving instance SpecTranslate ctx (KeyHash r c)
 
 instance Crypto c => SpecTranslate ctx (VKey k c) where
   type SpecRep (VKey k c) = Integer
 
-  toSpecRep (VKey x) = pure . byteStringToNum $ rawSerialiseVerKeyDSIGN x
+  toSpecRep (VKey x) = pure . toInteger . bytesToNatural $ rawSerialiseVerKeyDSIGN x
 
 instance DSIGNAlgorithm v => SpecTranslate ctx (SignedDSIGN v a) where
   type SpecRep (SignedDSIGN v a) = Integer
 
   toSpecRep (SignedDSIGN x) =
-    pure . byteStringToNum $ rawSerialiseSigDSIGN x
+    pure . toInteger . bytesToNatural $ rawSerialiseSigDSIGN x
 
 instance (Crypto c, Typeable k) => SpecTranslate ctx (WitVKey k c) where
   type SpecRep (WitVKey k c) = (Integer, Integer)

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

@@ -0,0 +1,15 @@
+module Test.Cardano.Ledger.Conformance.Utils where
+
+import Cardano.Crypto.Hash (ByteString)
+import Cardano.Crypto.Util (naturalToBytes)
+import qualified Data.ByteString.Base16 as B16
+import Test.Cardano.Ledger.TreeDiff (Expr, ToExpr (..))
+
+agdaHashToBytes :: Integer -> ByteString
+agdaHashToBytes = B16.encode . naturalToBytes hashSize . fromInteger
+  where
+    -- TODO is there a way to get this from a `Crypto` instead of hard-coding?
+    hashSize = 28
+
+agdaHashToExpr :: Integer -> Expr
+agdaHashToExpr = toExpr . agdaHashToBytes

libs/cardano-ledger-conformance/test/Main.hs

@@ -1,10 +1,15 @@
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE TypeApplications #-}
+
 module Main (main) where
 
 import Test.Cardano.Ledger.Common
+import qualified Test.Cardano.Ledger.Conformance.ConformanceSpec as ConformanceSpec
 import qualified Test.Cardano.Ledger.Conformance.Spec.Conway as Conway
 
 main :: IO ()
 main =
-  ledgerTestMain $
+  ledgerTestMain $ do
     describe "Conformance" $ do
       Conway.spec
+    ConformanceSpec.spec