Print out the exception when an ImpTestM example fails

IntersectMBO · Aug 22, 2024 · 5aba417 · 5aba417
1 parent af23a85
commit 5aba417
Show file tree

Hide file tree

Showing 10 changed files with 160 additions and 66 deletions.
diff --git a/cabal.project b/cabal.project
@@ -23,9 +23,9 @@ source-repository-package
   location: https://github.com/IntersectMBO/formal-ledger-specifications.git
   -- !WARNING!:
   -- MAKE SURE THIS POINTS TO A COMMIT IN `MAlonzo-code` BEFORE MERGE!
-  subdir: ledgerSrc/haskell/Ledger
-  tag: 9ce7ccb948abd12b46ebff9e03f320768f05c139
-  --sha256: sha256-ZspaY2eMk47LZ54x70yjtFslDE8gjoiUJ7oVXUvQMDw=
+  subdir: generated
+  tag: b5a8d47aebbdad92773be96c459f241d773d4771
+  --sha256: sha256-iEqucpja/0/5Tvnjr2drFlz58f3x3kUpInVjZfcePBQ=
 -- 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

diff --git a/eras/conway/impl/src/Cardano/Ledger/Conway/Governance.hs b/eras/conway/impl/src/Cardano/Ledger/Conway/Governance.hs
@@ -161,6 +161,7 @@ module Cardano.Ledger.Conway.Governance (
   TreeMaybe (..),
   toGovRelationTree,
   toGovRelationTreeEither,
+  showGovActionType,
 ) where
 
 import Cardano.Ledger.BaseTypes (

diff --git a/eras/conway/impl/src/Cardano/Ledger/Conway/Governance/Procedures.hs b/eras/conway/impl/src/Cardano/Ledger/Conway/Governance/Procedures.hs
@@ -53,6 +53,7 @@ module Cardano.Ledger.Conway.Governance.Procedures (
   Constitution (..),
   constitutionAnchorL,
   constitutionScriptL,
+  showGovActionType,
   -- Lenses
   pProcDepositL,
   pProcGovActionL,
@@ -823,6 +824,15 @@ data GovAction era
   | InfoAction
   deriving (Generic, Ord)
 
+showGovActionType :: GovAction era -> String
+showGovActionType NewConstitution {} = "NewConstitution"
+showGovActionType ParameterChange {} = "ParameterChange"
+showGovActionType HardForkInitiation {} = "HardForkInitiation"
+showGovActionType TreasuryWithdrawals {} = "TreasuryWithdrawals"
+showGovActionType NoConfidence {} = "NoConfidence"
+showGovActionType UpdateCommittee {} = "UpdateCommittee"
+showGovActionType InfoAction {} = "InfoAction"
+
 deriving instance EraPParams era => Show (GovAction era)
 
 deriving instance EraPParams era => Eq (GovAction era)

diff --git a/eras/conway/impl/src/Cardano/Ledger/Conway/Rules/Ratify.hs b/eras/conway/impl/src/Cardano/Ledger/Conway/Rules/Ratify.hs
@@ -20,6 +20,7 @@ module Cardano.Ledger.Conway.Rules.Ratify (
   spoAcceptedRatio,
   dRepAccepted,
   dRepAcceptedRatio,
+  acceptedByEveryone,
   -- Testing
   prevActionAsExpected,
   validCommitteeTerm,
@@ -280,6 +281,17 @@ withdrawalCanWithdraw (TreasuryWithdrawals m _) treasury =
   Map.foldr' (<+>) zero m <= treasury
 withdrawalCanWithdraw _ _ = True
 
+acceptedByEveryone ::
+  ConwayEraPParams era =>
+  RatifyEnv era ->
+  RatifyState era ->
+  GovActionState era ->
+  Bool
+acceptedByEveryone env st gas =
+  committeeAccepted env st gas
+    && spoAccepted env st gas
+    && dRepAccepted env st gas
+
 ratifyTransition ::
   forall era.
   ( Embed (EraRule "ENACT" era) (ConwayRATIFY era)
@@ -312,9 +324,7 @@ ratifyTransition = do
         && validCommitteeTerm govAction ensCurPParams reCurrentEpoch
         && not rsDelayed
         && withdrawalCanWithdraw govAction ensTreasury
-        && committeeAccepted env st gas
-        && spoAccepted env st gas
-        && dRepAccepted env st gas
+        && acceptedByEveryone env st gas
         then do
           newEnactState <-
             trans @(EraRule "ENACT" era) $

diff --git a/eras/shelley/impl/testlib/Test/Cardano/Ledger/Shelley/ImpTest.hs b/eras/shelley/impl/testlib/Test/Cardano/Ledger/Shelley/ImpTest.hs
@@ -253,7 +253,17 @@ import GHC.TypeLits (KnownSymbol, Symbol, symbolVal)
 import Lens.Micro (Lens', SimpleGetter, lens, to, (%~), (&), (.~), (<>~), (^.))
 import Lens.Micro.Mtl (use, view, (%=), (+=), (.=))
 import Numeric.Natural (Natural)
-import Prettyprinter (Doc, Pretty (..), annotate, defaultLayoutOptions, indent, layoutPretty, line)
+import Prettyprinter (
+  Doc,
+  Pretty (..),
+  annotate,
+  defaultLayoutOptions,
+  indent,
+  layoutPretty,
+  layoutSmart,
+  line,
+ )
+import Prettyprinter.Render.String (renderString)
 import Prettyprinter.Render.Terminal (AnsiStyle, Color (..), color, renderStrict)
 import System.Random
 import qualified System.Random as Random
@@ -788,13 +798,20 @@ instance (ShelleyEraImp era, Arbitrary a, Show a, Testable prop) => Example (a -
   evaluateExample impTest params hook progressCallback =
     let runImpTestExample s = property $ \x -> do
           let args = paramsQuickCheckArgs params
-          (r, testable) <- uncurry evalImpTestM (applyParamsQCGen params s) $ do
+          (r, testable, logs) <- uncurry evalImpTestM (applyParamsQCGen params s) $ do
             t <- impTest x
             qcSize <- asks iteQuickCheckSize
             StateGen qcGen <- subStateM split
-            pure (Just (qcGen, qcSize), t)
+            logs <- gets impLog
+            pure (Just (qcGen, qcSize), t, logs)
           let params' = params {paramsQuickCheckArgs = args {replay = r, chatty = False}}
-          res <- evaluateExample (property testable) params' (\f -> hook (\_st -> f ())) progressCallback
+          let logString = renderString $ layoutSmart defaultLayoutOptions logs
+          res <-
+            evaluateExample
+              (counterexample logString testable)
+              params'
+              (\f -> hook (\_st -> f ()))
+              progressCallback
           void $ throwIO $ resultStatus res
      in evaluateExample runImpTestExample params hook progressCallback
 

diff --git a/libs/cardano-ledger-conformance/src/Test/Cardano/Ledger/Conformance.hs b/libs/cardano-ledger-conformance/src/Test/Cardano/Ledger/Conformance.hs
@@ -1,10 +1,6 @@
-module Test.Cardano.Ledger.Conformance (
-  module Test.Cardano.Ledger.Conformance.ExecSpecRule.Core,
-  module Test.Cardano.Ledger.Conformance.SpecTranslate.Core,
-  module Test.Cardano.Ledger.Conformance.Utils,
-) where
+module Test.Cardano.Ledger.Conformance (module X) where
 
-import Test.Cardano.Ledger.Conformance.ExecSpecRule.Core
-import Test.Cardano.Ledger.Conformance.Orphans ()
-import Test.Cardano.Ledger.Conformance.SpecTranslate.Core
-import Test.Cardano.Ledger.Conformance.Utils
+import Test.Cardano.Ledger.Conformance.ExecSpecRule.Core as X
+import Test.Cardano.Ledger.Conformance.Orphans as X ()
+import Test.Cardano.Ledger.Conformance.SpecTranslate.Core as X
+import Test.Cardano.Ledger.Conformance.Utils as X
diff --git a/...ardano-ledger-conformance/src/Test/Cardano/Ledger/Conformance/ExecSpecRule/Conway/Base.hs b/...ardano-ledger-conformance/src/Test/Cardano/Ledger/Conformance/ExecSpecRule/Conway/Base.hs
@@ -37,7 +37,6 @@ import Cardano.Ledger.BaseTypes (
 import Cardano.Ledger.CertState (
   CommitteeAuthorization (..),
   CommitteeState (..),
-  authorizedHotCommitteeCredentials,
  )
 import Cardano.Ledger.Coin (Coin (..), CompactForm (..))
 import Cardano.Ledger.Conway (Conway)
@@ -52,9 +51,11 @@ import Cardano.Ledger.Conway.Governance (
   RatifyState (..),
   VotingProcedures,
   gasAction,
+  showGovActionType,
  )
 import Cardano.Ledger.Conway.Rules (
   EnactSignal (..),
+  acceptedByEveryone,
   committeeAccepted,
   committeeAcceptedRatio,
   dRepAccepted,
@@ -267,12 +268,8 @@ ratifyEnvSpec ConwayRatifyExecContext {crecGovActionMap} =
         exists
           ( \eval ->
               pure $
-                Set.map
-                  CommitteeHotCredential
-                  ( Set.intersection
-                      (authorizedHotCommitteeCredentials (eval committeeState))
-                      ccVotes
-                  )
+                Set.map CommitteeHotCredential ccVotes
+                  `Set.intersection` foldr' Set.insert mempty (eval cs)
           )
           ( \ [var| common |] ->
               [ assert $ common `subset_` fromList_ (rng_ cs)
@@ -338,6 +335,7 @@ ratifyStateSpec _ RatifyEnv {..} =
                     )
               )
           , disableBootstrap pp
+          , preferSmallerCCMinSizeValues pp
           ]
       ]
   where
@@ -349,6 +347,18 @@ ratifyStateSpec _ RatifyEnv {..} =
     disableBootstrap pp = match pp $ \pp' ->
       match (sel @12 pp') $ \major _ ->
         assert $ not_ (major ==. lit (natVersion @9))
+    preferSmallerCCMinSizeValues ::
+      IsConwayUniv fn =>
+      Term fn (PParams Conway) ->
+      Pred fn
+    preferSmallerCCMinSizeValues pp = match pp $ \pp' ->
+      match (sel @24 pp') $ \ccMinSize ->
+        satisfies ccMinSize $
+          chooseSpec
+            (1, TrueSpec)
+            (1, constrained (<=. committeeSize))
+      where
+        committeeSize = lit . fromIntegral . Set.size $ ccColdKeys
 
 ratifySignalSpec ::
   IsConwayUniv fn =>
@@ -378,11 +388,21 @@ instance IsConwayUniv fn => ExecSpecRule fn "RATIFY" Conway where
       $ Agda.ratifyStep env st sig
 
   extraInfo ctx env@RatifyEnv {..} st sig@(RatifySignal actions) =
-    unlines . toList $ actionAcceptedRatio <$> actions
+    unlines $ specExtraInfo : (actionAcceptedRatio <$> toList actions)
     where
       members = foldMap' (committeeMembers @Conway) $ ensCommittee (rsEnactState st)
       showAccepted True = "✓"
       showAccepted False = "×"
+      specExtraInfo =
+        unlines
+          [ "Spec extra info:"
+          , either show T.unpack . runSpecTransM ctx $
+              Agda.ratifyDebug
+                <$> toSpecRep env
+                <*> toSpecRep st
+                <*> toSpecRep sig
+          , ""
+          ]
       actionAcceptedRatio gas@GovActionState {..} =
         unlines
           [ "Acceptance ratios (impl):"
@@ -399,19 +419,11 @@ instance IsConwayUniv fn => ExecSpecRule fn "RATIFY" Conway where
               <> show (committeeAcceptedRatio members gasCommitteeVotes reCommitteeState reCurrentEpoch)
               <> "\t"
               <> showAccepted (committeeAccepted env st gas)
-          , ""
-          , "Spec extra info:"
-          , either show T.unpack . runSpecTransM ctx $
-              Agda.ratifyDebug
-                <$> toSpecRep env
-                <*> toSpecRep st
-                <*> toSpecRep sig
           ]
 
   testConformance ctx env st@(RatifyState {rsEnactState}) sig@(RatifySignal actions) =
-    labelRatios
-      . property
-      $ defaultTestConformance @fn @Conway @"RATIFY" ctx env st sig
+    labelRatios $
+      defaultTestConformance @fn @Conway @"RATIFY" ctx env st sig
     where
       bucket r
         | r == 0 % 1 = "=0%"
@@ -441,11 +453,17 @@ instance IsConwayUniv fn => ExecSpecRule fn "RATIFY" Conway where
         "SPO yes votes ratio \t"
           <> bucket
             (spoAcceptedRatio env a)
+      acceptedActions = fmap gasAction . filter (acceptedByEveryone env st) $ toList actions
+      acceptedActionTypes = Set.fromList $ showGovActionType <$> acceptedActions
       labelRatios
         | Just x <- SSeq.lookup 0 actions =
             label (ccBucket x)
               . label (drepBucket x)
               . label (spoBucket x)
+              . foldr'
+                (\a f -> label ("Accepted at least one " <> a) . f)
+                id
+                (toList acceptedActionTypes)
         | otherwise = id
 
 instance IsConwayUniv fn => ExecSpecRule fn "ENACT" Conway where

diff --git a/libs/cardano-ledger-conformance/src/Test/Cardano/Ledger/Conformance/ExecSpecRule/Core.hs b/libs/cardano-ledger-conformance/src/Test/Cardano/Ledger/Conformance/ExecSpecRule/Core.hs
@@ -354,8 +354,7 @@ conformsToImpl = property @(ImpTestM era Property) . (`runContT` pure) $ do
         case classOf @fn @rule @era sig of
           Nothing -> classify False "None"
           Just c -> classify True c
-  lift $ logEntry extra
-  pure . classification $
+  pure . counterexample extra . classification $
     testConformance @fn @rule @era ctx env st sig
 
 generatesWithin ::