TestRep rework

cabal.project

@@ -13,8 +13,8 @@ repository cardano-haskell-packages
 source-repository-package
   type: git
   location: https://github.com/input-output-hk/cardano-ledger-executable-spec.git
-  tag: 0f40403ba3b52a11ac8a44ec3be22ac272c732df
-  --sha256: sha256-8Lcp71PqMP9uBtiUPseyOwvZOSk4blR2+7Y2R6rkJoU=
+  tag: e1e0a33b7a407a79f0cafe6d8efb19a76ccb2ad7
+  --sha256: sha256-7NYvTLgnej23J/SiSH4fIJrtmjG6Y242AknTNsZgGv0=
 
 index-state:
   -- Bump this if you need newer packages from Hackage

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

@@ -7,7 +7,7 @@ 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 (runSpecTransM, toTestRep)
 import Test.Cardano.Ledger.Conformance.Spec.Conway ()
 import Test.Cardano.Ledger.Conformance.Utils (agdaHashToBytes)
 

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

@@ -31,6 +31,7 @@ import Cardano.Ledger.Conway.Governance (
 import Cardano.Ledger.Conway.PParams (THKD (..))
 import Cardano.Ledger.Conway.Rules (ConwayGovPredFailure)
 import Cardano.Ledger.Conway.Tx (AlonzoTx)
+import Cardano.Ledger.Conway.TxCert (ConwayTxCert)
 import Cardano.Ledger.Crypto (StandardCrypto)
 import Cardano.Ledger.TxIn (TxId)
 import Constrained
@@ -47,15 +48,14 @@ import Lens.Micro ((&), (.~), (^.))
 import qualified Lib as Agda
 import Test.Cardano.Ledger.Conformance (
   ExecSpecRule (..),
+  OpaqueErrorString (..),
   SpecTranslate (..),
   checkConformance,
   computationResultToEither,
   runConformance,
   runSpecTransM,
  )
-import Test.Cardano.Ledger.Conformance.SpecTranslate.Conway (
-  OpaqueErrorString (..),
- )
+import Test.Cardano.Ledger.Conformance.SpecTranslate.Conway ()
 import Test.Cardano.Ledger.Constrained.Conway (
   IsConwayUniv,
   ProposalsSplit,
@@ -232,10 +232,12 @@ instance
 
   environmentSpec _ = govEnvSpec
 
-  stateSpec (_, propSplit) env = govProposalsSpec env <> constrained agdaConstraints
+  stateSpec (_, propSplit) env =
+    govProposalsSpec env
+      <> constrained onlyMinFeeAUpdates
     where
-      agdaConstraints :: Term fn (Proposals Conway) -> Pred fn
-      agdaConstraints props =
+      onlyMinFeeAUpdates :: Term fn (Proposals Conway) -> Pred fn
+      onlyMinFeeAUpdates props =
         fold
           [ match @fn props $
               \ppups _ _ _ _ ->
@@ -244,13 +246,15 @@ instance
                       forAll' ppupTree $ \gas _ ->
                         match gas $ \_ _ _ _ prop _ _ -> agdaCompatibleProposal prop
                 ]
-          , genHint propSplit props
+          , genHint propSplit props -- Limit the total number of proposals
           ]
 
-  signalSpec _ env st = govProceduresSpec env st <> constrained agdaConstraints
+  signalSpec _ env st =
+    govProceduresSpec env st
+      <> constrained onlyMinFeeAUpdates
     where
-      agdaConstraints :: Term fn (GovProcedures Conway) -> Pred fn
-      agdaConstraints procs = match @fn procs $ \_ props ->
+      onlyMinFeeAUpdates :: Term fn (GovProcedures Conway) -> Pred fn
+      onlyMinFeeAUpdates procs = match @fn procs $ \_ props ->
         forAll props agdaCompatibleProposal
 
   genExecContext = (,) <$> arbitrary <*> genProposalsSplit 20
@@ -291,10 +295,12 @@ instance
 
   stateSpec _ = utxoStateSpec
 
-  signalSpec _ env st = utxoTxSpec env st <> constrained agdaConstraints
+  signalSpec _ env st =
+    utxoTxSpec env st
+      <> constrained disableInlineDatums
     where
-      agdaConstraints :: Term fn (AlonzoTx Conway) -> Pred fn
-      agdaConstraints tx = match @fn tx $ \txBody _ _ _ ->
+      disableInlineDatums :: Term fn (AlonzoTx Conway) -> Pred fn
+      disableInlineDatums tx = match @fn tx $ \txBody _ _ _ ->
         match txBody $
           \_ctbSpendInputs
            _ctbCollateralInputs
@@ -336,7 +342,22 @@ instance
   where
   environmentSpec _ = certEnvSpec
   stateSpec _ _ = certStateSpec
-  signalSpec _ = txCertSpec
+  signalSpec _ env st =
+    txCertSpec env st
+      <> constrained disableRegCerts
+    where
+      disableRegCerts :: Term fn (ConwayTxCert Conway) -> Pred fn
+      disableRegCerts cert =
+        (caseOn cert)
+          ( branch $ \delegCert ->
+              (caseOn delegCert)
+                (branch $ \_ _ -> False)
+                (branch $ \_ _ -> True)
+                (branch $ \_ _ -> True)
+                (branch $ \_ _ _ -> True)
+          )
+          (branch $ \_ -> True)
+          (branch $ \_ -> True)
 
   runAgdaRule env st sig =
     first (\e -> OpaqueErrorString (T.unpack e) NE.:| [])

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

@@ -31,7 +31,12 @@ 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.Conformance.SpecTranslate.Core (SpecTranslate (..), runSpecTransM)
+import Test.Cardano.Ledger.Conformance.SpecTranslate.Core (
+  Fixup (..),
+  SpecTranslate (..),
+  runSpecTransM,
+  toTestRep,
+ )
 import Test.Cardano.Ledger.Imp.Common
 import Test.Cardano.Ledger.Shelley.ImpTest (
   ImpTestM,
@@ -57,7 +62,6 @@ class
   , KnownSymbol rule
   , STS (EraRule rule era)
   , BaseM (EraRule rule era) ~ ShelleyBase
-  , NFData (TestRep (PredicateFailure (EraRule rule era)))
   , SpecTranslate (ExecContext fn rule era) (PredicateFailure (EraRule rule era))
   ) =>
   ExecSpecRule fn (rule :: Symbol) era
@@ -136,9 +140,15 @@ class
     , NFData (SpecRep (Environment (EraRule rule era)))
     , NFData (SpecRep (State (EraRule rule era)))
     , NFData (SpecRep (Signal (EraRule rule era)))
+    , NFData (SpecRep (PredicateFailure (EraRule rule era)))
     , ToExpr (SpecRep (Environment (EraRule rule era)))
     , ToExpr (SpecRep (State (EraRule rule era)))
     , ToExpr (SpecRep (Signal (EraRule rule era)))
+    , ToExpr (SpecRep (PredicateFailure (EraRule rule era)))
+    , Fixup (SpecRep (PredicateFailure (EraRule rule era)))
+    , Fixup (SpecRep (State (EraRule rule era)))
+    , Eq (SpecRep (PredicateFailure (EraRule rule era)))
+    , Eq (SpecRep (State (EraRule rule era)))
     ) =>
     Environment (EraRule rule era) ->
     State (EraRule rule era) ->
@@ -147,17 +157,17 @@ class
   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)))
+  ( ToExpr (SpecRep (PredicateFailure (EraRule rule era)))
+  , ToExpr (SpecRep (State (EraRule rule era)))
+  , Eq (SpecRep (PredicateFailure (EraRule rule era)))
+  , Eq (SpecRep (State (EraRule rule era)))
   ) =>
   Either
-    (NonEmpty (TestRep (PredicateFailure (EraRule rule era))))
-    (TestRep (State (EraRule rule era))) ->
+    (NonEmpty (SpecRep (PredicateFailure (EraRule rule era))))
+    (SpecRep (State (EraRule rule era))) ->
   Either
-    (NonEmpty (TestRep (PredicateFailure (EraRule rule era))))
-    (TestRep (State (EraRule rule era))) ->
+    (NonEmpty (SpecRep (PredicateFailure (EraRule rule era))))
+    (SpecRep (State (EraRule rule era))) ->
   ImpTestM era ()
 checkConformance implResTest agdaResTest = do
   let
@@ -180,10 +190,16 @@ defaultTestConformance ::
   , NFData (SpecRep (Environment (EraRule rule era)))
   , NFData (SpecRep (State (EraRule rule era)))
   , NFData (SpecRep (Signal (EraRule rule era)))
+  , NFData (SpecRep (PredicateFailure (EraRule rule era)))
   , ToExpr (SpecRep (Environment (EraRule rule era)))
   , ToExpr (SpecRep (State (EraRule rule era)))
   , ToExpr (SpecRep (Signal (EraRule rule era)))
+  , ToExpr (SpecRep (PredicateFailure (EraRule rule era)))
   , ExecSpecRule fn rule era
+  , Fixup (SpecRep (PredicateFailure (EraRule rule era)))
+  , Fixup (SpecRep (State (EraRule rule era)))
+  , Eq (SpecRep (PredicateFailure (EraRule rule era)))
+  , Eq (SpecRep (State (EraRule rule era)))
   ) =>
   Environment (EraRule rule era) ->
   State (EraRule rule era) ->
@@ -199,22 +215,25 @@ runConformance ::
   , NFData (SpecRep (Environment (EraRule rule era)))
   , NFData (SpecRep (State (EraRule rule era)))
   , NFData (SpecRep (Signal (EraRule rule era)))
+  , NFData (SpecRep (PredicateFailure (EraRule rule era)))
   , ToExpr (SpecRep (Environment (EraRule rule era)))
   , ToExpr (SpecRep (State (EraRule rule era)))
   , ToExpr (SpecRep (Signal (EraRule rule era)))
   , SpecTranslate (ExecContext fn rule era) (State (EraRule rule era))
+  , Fixup (SpecRep (PredicateFailure (EraRule rule era)))
+  , Fixup (SpecRep (State (EraRule rule era)))
   ) =>
   Environment (EraRule rule era) ->
   State (EraRule rule era) ->
   Signal (EraRule rule era) ->
   ImpTestM
     era
     ( Either
-        (NonEmpty (TestRep (PredicateFailure (EraRule rule era))))
-        (TestRep (State (EraRule rule era)))
+        (NonEmpty (SpecRep (PredicateFailure (EraRule rule era))))
+        (SpecRep (State (EraRule rule era)))
     , Either
-        (NonEmpty (TestRep (PredicateFailure (EraRule rule era))))
-        (TestRep (State (EraRule rule era)))
+        (NonEmpty (SpecRep (PredicateFailure (EraRule rule era))))
+        (SpecRep (State (EraRule rule era)))
     )
 runConformance env st sig = do
   (execContext :: ctx) <- liftGen $ genExecContext @fn @rule @era
@@ -230,11 +249,7 @@ runConformance env st sig = do
     impAnn "Translating implementation values to SpecRep" . expectRightExpr . runSpecTransM execContext $
       bimapM (traverse toTestRep) toTestRep (fst <$> implRes)
   let
-    agdaResTest =
-      bimap
-        (fmap $ specToTestRep @ctx @(PredicateFailure (EraRule rule era)))
-        (specToTestRep @ctx @(State (EraRule rule era)))
-        agdaRes
+    agdaResTest = bimap (fixup <$>) fixup agdaRes
   pure (implResTest, agdaResTest)
 
 conformsToImpl ::
@@ -244,11 +259,17 @@ conformsToImpl ::
   , NFData (SpecRep (Environment (EraRule rule era)))
   , NFData (SpecRep (State (EraRule rule era)))
   , NFData (SpecRep (Signal (EraRule rule era)))
+  , NFData (SpecRep (PredicateFailure (EraRule rule era)))
   , ToExpr (SpecRep (Environment (EraRule rule era)))
   , ToExpr (SpecRep (State (EraRule rule era)))
   , ToExpr (SpecRep (Signal (EraRule rule era)))
-  , SpecTranslate (ExecContext fn rule era) (State (EraRule rule era))
+  , ToExpr (SpecRep (PredicateFailure (EraRule rule era)))
   , ToExpr (ExecContext fn rule era)
+  , SpecTranslate (ExecContext fn rule era) (State (EraRule rule era))
+  , Fixup (SpecRep (PredicateFailure (EraRule rule era)))
+  , Fixup (SpecRep (State (EraRule rule era)))
+  , Eq (SpecRep (PredicateFailure (EraRule rule era)))
+  , Eq (SpecRep (State (EraRule rule era)))
   ) =>
   Property
 conformsToImpl =

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

@@ -4,9 +4,13 @@
 
 module Test.Cardano.Ledger.Conformance.Orphans where
 
+import Data.Bifunctor (Bifunctor (..))
+import Data.Default.Class (Default)
+import Data.List (sortOn)
 import GHC.Generics (Generic)
 import Lib
 import Test.Cardano.Ledger.Common (NFData, ToExpr)
+import Test.Cardano.Ledger.Conformance.SpecTranslate.Core (Fixup (..), OpaqueErrorString)
 import Test.Cardano.Ledger.Conformance.Utils
 import Test.Cardano.Ledger.Conway.TreeDiff (Expr (..), ToExpr (..))
 
@@ -46,6 +50,8 @@ deriving instance Ord Tag
 
 deriving instance Ord Credential
 
+deriving instance Ord GovRole
+
 deriving instance Eq TxWitnesses
 
 deriving instance Eq Tx
@@ -82,6 +88,8 @@ deriving instance Eq GState
 
 deriving instance Eq CertState
 
+instance (NFData k, NFData v) => NFData (HSMap k v)
+
 instance NFData GovAction
 
 instance NFData TxId
@@ -138,6 +146,8 @@ instance ToExpr Credential where
   toExpr (KeyHashObj h) = App "KeyHashObj" [agdaHashToExpr h]
   toExpr (ScriptObj h) = App "ScriptObj" [agdaHashToExpr h]
 
+instance (ToExpr k, ToExpr v) => ToExpr (HSMap k v)
+
 instance ToExpr GovAction
 
 instance ToExpr GovRole
@@ -188,3 +198,56 @@ instance ToExpr PState
 instance ToExpr GState
 
 instance ToExpr CertState
+
+instance Default (HSMap k v)
+
+instance Fixup OpaqueErrorString
+
+instance Fixup a => Fixup [a]
+
+instance Fixup Char where
+  fixup = id
+
+instance
+  ( Ord k
+  , Fixup k
+  , Fixup v
+  ) =>
+  Fixup (HSMap k v)
+  where
+  fixup (MkHSMap l) = MkHSMap . sortOn fst $ bimap fixup fixup <$> l
+
+instance (Fixup a, Fixup b) => Fixup (a, b)
+
+instance Fixup a => Fixup (Maybe a)
+
+instance (Fixup a, Fixup b) => Fixup (Either a b)
+
+instance Fixup Integer where
+  fixup = id
+
+instance Fixup TxId
+
+instance Fixup ()
+
+instance Fixup UTxOState
+
+instance Fixup Credential
+
+instance Fixup GovRole
+
+instance Fixup VDeleg
+
+instance Fixup DState
+
+instance Fixup PState
+
+instance Fixup GState
+
+instance Fixup CertState
+
+instance Fixup Vote
+
+instance Fixup GovAction
+
+instance Fixup GovActionState