Print out the exception when an ImpTestM example fails

cabal.project

@@ -21,9 +21,9 @@ repository cardano-haskell-packages
 source-repository-package
   type: git
   location: https://github.com/IntersectMBO/formal-ledger-specifications.git
-  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

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 (

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)

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,18 @@ 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 +325,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) $

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

@@ -253,7 +253,7 @@ 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, line, layoutSmart)
 import Prettyprinter.Render.Terminal (AnsiStyle, Color (..), color, renderStrict)
 import System.Random
 import qualified System.Random as Random
@@ -291,6 +291,7 @@ import UnliftIO.Exception (
   evaluateDeep,
   throwIO,
  )
+import Prettyprinter.Render.String (renderString)
 
 data SomeSTSEvent era
   = forall (rule :: Symbol).
@@ -788,13 +789,15 @@ 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
 

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

libs/cardano-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)
@@ -51,7 +50,7 @@ import Cardano.Ledger.Conway.Governance (
   RatifySignal (..),
   RatifyState (..),
   VotingProcedures,
-  gasAction,
+  gasAction, showGovActionType,
  )
 import Cardano.Ledger.Conway.Rules (
   EnactSignal (..),
@@ -60,7 +59,7 @@ import Cardano.Ledger.Conway.Rules (
   dRepAccepted,
   dRepAcceptedRatio,
   spoAccepted,
-  spoAcceptedRatio,
+  spoAcceptedRatio, acceptedByEveryone,
  )
 import Cardano.Ledger.Conway.Tx (AlonzoTx)
 import Cardano.Ledger.Credential (Credential (..))
@@ -267,12 +266,9 @@ 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 +334,7 @@ ratifyStateSpec _ RatifyEnv {..} =
                     )
               )
           , disableBootstrap pp
+          , preferSmallerCCMinSizeValues pp
           ]
       ]
   where
@@ -349,6 +346,17 @@ 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
+          (0, TrueSpec)
+          (1, constrained (<=. committeeSize))
+      where
+        committeeSize = lit . fromIntegral . Set.size $ ccColdKeys
 
 ratifySignalSpec ::
   IsConwayUniv fn =>
@@ -410,7 +418,6 @@ instance IsConwayUniv fn => ExecSpecRule fn "RATIFY" Conway where
 
   testConformance ctx env st@(RatifyState {rsEnactState}) sig@(RatifySignal actions) =
     labelRatios
-      . property
       $ defaultTestConformance @fn @Conway @"RATIFY" ctx env st sig
     where
       bucket r
@@ -441,11 +448,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

libs/cardano-ledger-conformance/test/Test/Cardano/Ledger/Conformance/Imp/Ratify.hs

@@ -1,5 +1,6 @@
 {-# LANGUAGE DataKinds #-}
 {-# LANGUAGE TypeApplications #-}
+{-# LANGUAGE NamedFieldPuns #-}
 
 module Test.Cardano.Ledger.Conformance.Imp.Ratify (spec) where
 
@@ -11,7 +12,7 @@ import Cardano.Ledger.Conway.Governance (
   GovPurposeId (..),
   RatifySignal (..),
   Voter (..),
-  getRatifyState,
+  getRatifyState, committeeGovStateL, Committee (..),
  )
 import Cardano.Ledger.Conway.PParams (
   dvtMotionNoConfidenceL,
@@ -31,13 +32,16 @@ import Lens.Micro ((&), (.~))
 import Test.Cardano.Ledger.Conformance.ExecSpecRule.Conway (
   ConwayRatifyExecContext (..),
  )
-import Test.Cardano.Ledger.Conformance.ExecSpecRule.Core (ExecSpecRule (..))
+import Test.Cardano.Ledger.Conformance.ExecSpecRule.Core (ExecSpecRule (..), runConformance)
 import Test.Cardano.Ledger.Constrained.Conway (ConwayFn)
 import Test.Cardano.Ledger.Conway.ImpTest
 import Test.Cardano.Ledger.Core.Rational (IsRatio (..))
 import Test.Cardano.Ledger.Imp.Common
 import Cardano.Ledger.Credential (Credential(..))
 import qualified Data.Map as Map
+import Cardano.Ledger.Conway.Core (ppCoinsPerUTxOByteL, CoinPerByte (..), ppCommitteeMinSizeL)
+import Cardano.Ledger.Coin (Coin(..))
+import Test.Cardano.Ledger.Conformance ()
 
 spec :: Spec
 spec = describe "RATIFY" . withImpStateWithProtVer @Conway (natVersion @10) $ do
@@ -69,28 +73,42 @@ spec = describe "RATIFY" . withImpStateWithProtVer @Conway (natVersion @10) $ do
         ratSt
         (RatifySignal (noConfidenceGAS SSeq.:<| SSeq.Empty))
   it "Duplicate CC hot keys count as separate votes" $ do
+    logEntry "Setting up a DRep"
     let maxTermLength = EpochInterval 10
     modifyPParams $ \pp ->
       pp
         & ppCommitteeMaxTermLengthL .~ maxTermLength
-    (credDRep, _, _) <- setupSingleDRep 100
+        & ppCoinsPerUTxOByteL .~ CoinPerByte (Coin 1)
+        & ppCommitteeMinSizeL .~ 2
+    (credDRep, _, _) <- setupSingleDRep 300
+    -- Ensure that there is no committee yet
+    SJust (Committee {committeeMembers = oldCommittee}) <-
+      getsNES $ nesEsL . epochStateGovStateL . committeeGovStateL
+
+    logEntry "Electing the committee"
     ccCold0 <- KeyHashObj <$> freshKeyHash
     ccCold1 <- KeyHashObj <$> freshKeyHash
+    ccCold2 <- KeyHashObj <$> freshKeyHash
     hotKey <- KeyHashObj <$> freshKeyHash
     curEpoch <- getsNES nesELL
     let
       ccExpiry = curEpoch `addEpochInterval` maxTermLength
       committee = Map.fromList
         [ (ccCold0, ccExpiry)
         , (ccCold1, ccExpiry)
+        , (ccCold2, ccExpiry)
         ]
-
-    logEntry "Electing the committee"
-    committeeId <- submitGovAction $ UpdateCommittee SNothing mempty committee maxBound
+    committeeId <- submitGovAction $
+      UpdateCommittee
+        SNothing
+        (Map.keysSet oldCommittee) -- Get rid of the initial committee
+        committee
+        (6 %! 10)
     submitYesVote_ (DRepVoter credDRep) committeeId
-    logAcceptedRatio committeeId
-    passNEpochs 2
-    getLastEnactedCommittee `shouldReturn` SJust (GovPurposeId committeeId)
+    impAnn "Waiting for the committee to get elected" $ do
+      logAcceptedRatio committeeId
+      passNEpochs 2
+      getLastEnactedCommittee `shouldReturn` SJust (GovPurposeId committeeId)
 
     logEntry "Registering hotkeys"
     _ <- registerCommitteeHotKeys (pure hotKey) (ccCold0 NE.:| [ccCold1])
@@ -109,10 +127,30 @@ spec = describe "RATIFY" . withImpStateWithProtVer @Conway (natVersion @10) $ do
     govSt <- getsNES $ nesEsL . epochStateGovStateL
     let
       ratSt = getRatifyState govSt
-      result =
-        testConformance @ConwayFn @"RATIFY" @Conway
-          execCtx
-          ratEnv
-          ratSt
-          (RatifySignal (constitutionGAS SSeq.:<| mempty))
-    pure result
+      ratSig = RatifySignal (constitutionGAS SSeq.:<| mempty)
+    (implRes, agdaRes) <-
+      runConformance @"RATIFY" @ConwayFn @Conway
+        execCtx
+        ratEnv
+        ratSt
+        ratSig
+    logEntry "===context==="
+    logToExpr execCtx
+    logEntry "===environment==="
+    logToExpr ratEnv
+    logEntry "===state==="
+    logToExpr ratSt
+    logEntry "===signal==="
+    logToExpr ratSig
+    logEntry "Impl res:"
+    logToExpr implRes
+    logEntry "Agda res:"
+    logToExpr agdaRes
+    logEntry "Extra information:"
+    logEntry $
+      extraInfo @ConwayFn @"RATIFY" @Conway
+        execCtx
+        ratEnv
+        ratSt
+        ratSig
+    impAnn "Conformance failed" $ implRes `shouldBeExpr` agdaRes

libs/cardano-ledger-test/src/Test/Cardano/Ledger/Constrained/Conway/Instances.hs

@@ -300,7 +300,7 @@ instance (IsConwayUniv fn, Typeable r, Crypto c) => HasSpec fn (KeyHash r c) whe
   genFromTypeSpec _ =
     pureGen $
       oneof
-        [ pickFromFixedPool 100
+        [ pickFromFixedPool 5
         , arbitrary
         ]
   cardinalTypeSpec _ = TrueSpec