WIP

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: 324fafa887b7b6b38e15d2b505c4eec5a3247176
-  --sha256: sha256-zpQToGA04NQ3TfkeWBJXIzisvoGLfYdWNbVQ/2BfeEI=
+  tag: 9233cb9f0e15dcdb5ef7ba49a21ee3820ee9aa76
+  --sha256: sha256-ea99nQ/j62FJkVdACKffVgLZ5mR1ZKwakSlNcSi5fJA=
 
 index-state:
   -- Bump this if you need newer packages from Hackage

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

@@ -577,6 +577,17 @@ newtype ImpTestM era a = ImpTestM {unImpTestM :: ReaderT (ImpTestEnv era) (GenT
     , MonadReader (ImpTestEnv era)
     )
 
+instance
+  ( Testable a
+  , ShelleyEraImp era
+  ) =>
+  Testable (ImpTestM era a)
+  where
+  property m = property . fmap ioProperty . runGenT $ do
+    st <- liftIO mkImpState
+    res <- liftGen $ runImpTestGenM st m
+    liftIO $ fst <$> res
+
 instance MonadWriter [SomeSTSEvent era] (ImpTestM era) where
   writer (x, evs) = (impEventsL %= (<> evs)) $> x
   listen act = do
@@ -1079,26 +1090,21 @@ logEntry e = impLogL %= (<> pretty loc <> "\t" <> pretty e <> line)
 logToExpr :: (HasCallStack, ToExpr a) => a -> ImpTestM era ()
 logToExpr e = logEntry (showExpr e)
 
-withImpState ::
-  forall era.
-  ShelleyEraImp era =>
-  SpecWith (ImpTestState era) ->
-  Spec
-withImpState =
-  beforeAll $
-    execStateT addRootTxOut $
-      ImpTestState
-        { impNES = initImpNES
-        , impRootTxIn = rootTxIn
-        , impKeyPairs = mempty
-        , impByronKeyPairs = mempty
-        , impNativeScripts = mempty
-        , impLastTick = 0
-        , impGlobals = testGlobals
-        , impLog = mempty
-        , impGen = qcGen
-        , impEvents = mempty
-        }
+mkImpState :: ShelleyEraImp era => IO (ImpTestState era)
+mkImpState =
+  execStateT addRootTxOut $
+    ImpTestState
+      { impNES = initImpNES
+      , impRootTxIn = rootTxIn
+      , impKeyPairs = mempty
+      , impByronKeyPairs = mempty
+      , impNativeScripts = mempty
+      , impLastTick = 0
+      , impGlobals = testGlobals
+      , impLog = mempty
+      , impGen = qcGen
+      , impEvents = mempty
+      }
   where
     rootCoin = Coin 1_000_000_000
     rootTxIn = TxIn (mkTxId 0) minBound
@@ -1110,6 +1116,13 @@ withImpState =
       impNESL . nesEsL . esLStateL . lsUTxOStateL . utxosUtxoL
         %= (<> UTxO (Map.singleton rootTxIn rootTxOut))
 
+withImpState ::
+  forall era.
+  ShelleyEraImp era =>
+  SpecWith (ImpTestState era) ->
+  Spec
+withImpState = beforeAll mkImpState
+
 -- | Creates a fresh @SafeHash@
 freshSafeHash :: Era era => ImpTestM era (SafeHash (EraCrypto era) a)
 freshSafeHash = arbitrary

libs/cardano-data/testlib/Test/Cardano/Data/TreeDiff.hs

@@ -5,12 +5,14 @@
 
 module Test.Cardano.Data.TreeDiff where
 
+import Data.Foldable (Foldable (..))
 import Data.Foldable qualified as F
 import Data.OMap.Strict
 import Data.OSet.Strict
-import Test.Cardano.Ledger.Binary.TreeDiff (ToExpr (..))
+import Test.Cardano.Ledger.Binary.TreeDiff (Expr (..), ToExpr (..))
 
-deriving instance ToExpr a => ToExpr (OSet a)
+instance ToExpr a => ToExpr (OSet a) where
+  toExpr x = App "OSet.fromList" [toExpr $ toList x]
 
 instance (HasOKey k v, ToExpr v) => ToExpr (OMap k v) where
   listToExpr = listToExpr . F.toList

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

@@ -41,6 +41,7 @@ library
         base >=4.14 && <5,
         cardano-data,
         cardano-strict-containers,
+        data-default-class,
         microlens,
         mtl,
         cardano-ledger-binary,

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

@@ -15,17 +15,19 @@
 
 module Test.Cardano.Ledger.Conformance.ExecSpecRule.Conway () where
 
-import Cardano.Ledger.BaseTypes (Inject (..))
+import Cardano.Ledger.BaseTypes (Inject (..), StrictMaybe (..))
 import Cardano.Ledger.Conway (Conway)
-import Cardano.Ledger.Conway.Core (Era (..), EraPParams)
-import Cardano.Ledger.Conway.Governance (EnactState)
+import Cardano.Ledger.Conway.Core (Era (..), EraPParams, PParamsUpdate)
+import Cardano.Ledger.Conway.Governance (EnactState, GovProcedures)
+import Cardano.Ledger.Conway.PParams (THKD (..))
 import Cardano.Ledger.Conway.Rules (ConwayGovPredFailure)
 import Cardano.Ledger.Conway.Tx (AlonzoTx)
 import Constrained
 import Control.DeepSeq (NFData)
 import Data.Bifunctor (Bifunctor (..))
 import qualified Data.List.NonEmpty as NE
 import qualified Data.Text as T
+import Data.Typeable (Typeable)
 import GHC.Generics (Generic)
 import qualified Lib as Agda
 import Test.Cardano.Ledger.Conformance (
@@ -72,6 +74,102 @@ instance c ~ EraCrypto era => Inject (ConwayGovExecContext era) (GovProceduresSp
 instance Inject (ConwayGovExecContext era) (EnactState era) where
   inject (ConwayGovExecContext _ x) = x
 
+agdaCompatiblePPU :: IsConwayUniv fn => Term fn (PParamsUpdate Conway) -> Pred fn
+agdaCompatiblePPU ppup =
+  match ppup $
+    \cppMinFeeA
+     cppMinFeeB
+     cppMaxBBSize
+     cppMaxTxSize
+     cppMaxBHSize
+     cppKeyDeposit
+     cppPoolDeposit
+     cppEMax
+     cppNOpt
+     cppA0
+     cppRho
+     cppTau
+     _cppProtocolVersion
+     cppMinPoolCost
+     cppCoinsPerUTxOByte
+     cppCostModels
+     cppPrices
+     cppMaxTxExUnits
+     cppMaxBlockExUnits
+     cppMaxValSize
+     cppCollateralPercentage
+     cppMaxCollateralInputs
+     cppPoolVotingThresholds
+     cppDRepVotingThresholds
+     cppCommitteeMinSize
+     cppCommitteeMaxTermLength
+     cppGovActionLifetime
+     cppGovActionDeposit
+     cppDRepDeposit
+     cppDRepActivity
+     cppMinFeeRefScriptCostPerByte ->
+        -- TODO enable pparam updates once they're properly
+        -- implemented in the spec
+        mconcat
+          [ isModified cppMinFeeA
+          , isUnmodified cppMinFeeB
+          , isUnmodified cppMaxBBSize
+          , isUnmodified cppMaxTxSize
+          , isUnmodified cppMaxBHSize
+          , isUnmodified cppKeyDeposit
+          , isUnmodified cppPoolDeposit
+          , isUnmodified cppEMax
+          , isUnmodified cppNOpt
+          , isUnmodified cppA0
+          , isUnmodified cppRho
+          , isUnmodified cppTau
+          , isUnmodified cppMinPoolCost
+          , isUnmodified cppCoinsPerUTxOByte
+          , isUnmodified cppCostModels
+          , isUnmodified cppPrices
+          , isUnmodified cppMaxTxExUnits
+          , isUnmodified cppMaxBlockExUnits
+          , isUnmodified cppMaxValSize
+          , isUnmodified cppCollateralPercentage
+          , isUnmodified cppMaxCollateralInputs
+          , isUnmodified cppPoolVotingThresholds
+          , isUnmodified cppDRepVotingThresholds
+          , isUnmodified cppCommitteeMinSize
+          , isUnmodified cppCommitteeMaxTermLength
+          , isUnmodified cppGovActionLifetime
+          , isUnmodified cppGovActionDeposit
+          , isUnmodified cppDRepDeposit
+          , isUnmodified cppDRepActivity
+          , isUnmodified cppMinFeeRefScriptCostPerByte
+          ]
+  where
+    isUnmodified ::
+      ( HasSpec fn a
+      , Typeable gs
+      , IsNormalType a
+      , IsConwayUniv fn
+      ) =>
+      Term fn (THKD gs StrictMaybe a) ->
+      Pred fn
+    isUnmodified x =
+      caseOn
+        x
+        (branch $ const True)
+        (branch $ const False)
+    isModified ::
+      ( HasSpec fn a
+      , Typeable gs
+      , IsNormalType a
+      , IsConwayUniv fn
+      ) =>
+      Term fn (THKD gs StrictMaybe a) ->
+      Pred fn
+    isModified x =
+      caseOn
+        x
+        (branch $ const False)
+        (branch $ const True)
+
 instance
   ( NFData (SpecRep (ConwayGovPredFailure Conway))
   , IsConwayUniv fn
@@ -84,7 +182,21 @@ instance
 
   stateSpec = govProposalsSpec
 
-  signalSpec = govProceduresSpec
+  signalSpec env st = govProceduresSpec env st <> constrained agdaConstraints
+    where
+      agdaConstraints :: Term fn (GovProcedures Conway) -> Pred fn
+      agdaConstraints procs = match @fn procs $ \_ props ->
+        forAll props $ \prop ->
+          match prop $ \_ _ govAction _ ->
+            caseOn
+              govAction
+              (branch $ \_ ppup _ -> agdaCompatiblePPU ppup)
+              (branch $ \_ _ -> True)
+              (branch $ \_ _ -> True)
+              (branch $ const True)
+              (branch $ \_ _ _ _ -> True)
+              (branch $ \_ _ -> True)
+              (branch $ const True)
 
   execContextSpec = TrueSpec
 

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

@@ -19,7 +19,7 @@ module Test.Cardano.Ledger.Conformance.ExecSpecRule.Core (
 import Cardano.Ledger.BaseTypes (Inject, ShelleyBase)
 import Cardano.Ledger.Core (EraRule)
 import qualified Constrained as CV2
-import Constrained.Base (Spec (..))
+import Constrained.Base (Spec (..), shrinkWithSpec)
 import Control.State.Transition.Extended (STS (..))
 import Data.Bifunctor (Bifunctor (..))
 import Data.Bitraversable (bimapM)
@@ -31,15 +31,19 @@ import Test.Cardano.Ledger.Conformance.SpecTranslate.Core (SpecTranslate (..), r
 import Test.Cardano.Ledger.Imp.Common (
   MonadGen (..),
   NFData,
+  Property,
   ToExpr,
+  counterexample,
+  diffExpr,
   expectRightExpr,
-  shouldBeExpr,
+  forAllShrinkShow,
+  showExpr,
  )
 import Test.Cardano.Ledger.Shelley.ImpTest (
   ImpTestM,
+  ShelleyEraImp,
   impAnn,
   logEntry,
-  logToExpr,
   tryRunImpRule,
  )
 
@@ -98,25 +102,40 @@ class
       (NonEmpty (SpecRep (PredicateFailure (EraRule rule era))))
       (SpecRep (State (EraRule rule era)))
 
-conformsToImpl ::
-  forall (rule :: Symbol) fn era.
+impSpecTrans ::
+  SpecTranslate ctx a =>
+  ctx ->
+  a ->
+  ImpTestM era (SpecRep a)
+impSpecTrans ctx x = do
+  let res = runSpecTransM ctx $ toSpecRep x
+  expectRightExpr res
+
+runConformance ::
+  forall (rule :: Symbol) (fn :: [Type] -> Type -> Type) era.
   ( ExecSpecRule fn rule era
-  , NFData (SpecRep (PredicateFailure (EraRule rule era)))
+  , NFData (SpecRep (Environment (EraRule rule era)))
   , NFData (SpecRep (State (EraRule rule era)))
+  , NFData (SpecRep (Signal (EraRule rule era)))
   ) =>
-  ImpTestM era ()
-conformsToImpl = impAnn "conformsToImpl" . resize 5 $ do
-  env <- liftGen . CV2.genFromSpec_ $ environmentSpec @fn @rule @era
-  logToExpr env
-  st <- liftGen . CV2.genFromSpec_ $ stateSpec @fn @rule @era env
-  logToExpr st
-  sig <- liftGen . CV2.genFromSpec_ $ signalSpec @fn @rule @era env st
-  logToExpr sig
-  logEntry . show $ signalSpec @fn @rule @era env st
+  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)))
+    , Either
+        (NonEmpty (TestRep (PredicateFailure (EraRule rule era))))
+        (TestRep (State (EraRule rule era)))
+    )
+runConformance env st sig = do
   (execContext :: ctx) <- liftGen . CV2.genFromSpec_ $ execContextSpec @fn @rule @era
-  agdaRes <-
-    impAnn "Translating spec values to SpecRep" . expectRightExpr . runSpecTransM execContext $
-      runAgdaRule @fn @rule @era <$> toSpecRep env <*> toSpecRep st <*> toSpecRep sig
+  specEnv <- impAnn "Translating the environment" $ impSpecTrans execContext env
+  specSt <- impAnn "Translating the state" $ impSpecTrans execContext st
+  specSig <- impAnn "Translating the signal" $ impSpecTrans execContext sig
+  let agdaRes = runAgdaRule @fn @rule @era specEnv specSt specSig
   implRes <- fmap fst <$> tryRunImpRule @rule @era env st sig
   implResTest <-
     impAnn "Translating implementation values to SpecRep" . expectRightExpr . runSpecTransM execContext $
@@ -127,7 +146,39 @@ conformsToImpl = impAnn "conformsToImpl" . resize 5 $ do
         (fmap $ specToTestRep @ctx @(PredicateFailure (EraRule rule era)))
         (specToTestRep @ctx @(State (EraRule rule era)))
         agdaRes
-  agdaResTest `shouldBeExpr` implResTest
+  pure (implResTest, agdaResTest)
+
+conformsToImpl ::
+  forall (rule :: Symbol) fn era.
+  ( ShelleyEraImp era
+  , ExecSpecRule fn rule era
+  , NFData (SpecRep (Environment (EraRule rule era)))
+  , NFData (SpecRep (State (EraRule rule era)))
+  , NFData (SpecRep (Signal (EraRule rule era)))
+  ) =>
+  Property
+conformsToImpl =
+  let envSpec = environmentSpec @fn @rule @era
+   in forAllShrinkShow (CV2.genFromSpec_ envSpec) (shrinkWithSpec envSpec) showExpr $ \env ->
+        let stSpec = stateSpec @fn @rule @era env
+         in forAllShrinkShow (CV2.genFromSpec_ stSpec) (shrinkWithSpec stSpec) showExpr $ \st ->
+              let sigSpec = signalSpec @fn @rule @era env st
+               in forAllShrinkShow (CV2.genFromSpec_ sigSpec) (shrinkWithSpec sigSpec) showExpr $ \sig ->
+                    resize 5 $ do
+                      logEntry @era . show $ signalSpec @fn @rule @era env st
+                      (implResTest, agdaResTest) <- runConformance @rule @fn env st sig
+                      let
+                        failMsg =
+                          unlines
+                            [ ""
+                            , "===== DIFF ====="
+                            , diffExpr implResTest agdaResTest
+                            , ""
+                            , "Legend:"
+                            , "\t\ESC[91mImplemenation"
+                            , "\t\ESC[92mSpecification\ESC[39m"
+                            ]
+                      pure . counterexample failMsg $ implResTest == agdaResTest
 
 computationResultToEither :: Agda.ComputationResult e a -> Either e a
 computationResultToEither (Agda.Success x) = Right x