Print out the exception when an ImpTestM example fails

IntersectMBO · Aug 30, 2024 · a6d10e2 · a6d10e2
1 parent c12a19d
commit a6d10e2
Show file tree

Hide file tree

Showing 10 changed files with 164 additions and 68 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: 0b269ddbab4044a834554e94b3f9d1311a6ae06b
+  --sha256: sha256-M0ikZWKH8JCY+sSuujDILeFIsTzOsOfc9EilskHdWTU=
 -- 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/CHANGELOG.md b/eras/conway/impl/CHANGELOG.md
@@ -2,6 +2,7 @@
 
 ## 1.16.2.0
 
+* Add `showGovActionType`, `acceptedByEveryone`
 * Added `unRatifySignal`
 * Added lenses:
   * `ratifySignalL`

diff --git a/eras/conway/impl/src/Cardano/Ledger/Conway/Governance.hs b/eras/conway/impl/src/Cardano/Ledger/Conway/Governance.hs
@@ -167,6 +167,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
@@ -41,7 +41,6 @@ import Cardano.Ledger.Binary.Coders (Decode (From, RecD), Encode (..), decode, e
 import Cardano.Ledger.CertState (
   CommitteeAuthorization (..),
   CommitteeState (..),
-  authorizedHotCommitteeCredentials,
  )
 import Cardano.Ledger.Coin (Coin (..), CompactForm (..))
 import Cardano.Ledger.Conway (Conway)
@@ -56,9 +55,11 @@ import Cardano.Ledger.Conway.Governance (
   RatifyState (..),
   VotingProcedures,
   gasAction,
+  showGovActionType,
  )
 import Cardano.Ledger.Conway.Rules (
   EnactSignal (..),
+  acceptedByEveryone,
   committeeAccepted,
   committeeAcceptedRatio,
   dRepAccepted,
@@ -308,12 +309,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)
@@ -379,6 +376,7 @@ ratifyStateSpec _ RatifyEnv {..} =
                     )
               )
           , disableBootstrap pp
+          , preferSmallerCCMinSizeValues pp
           ]
       ]
   where
@@ -389,7 +387,19 @@ ratifyStateSpec _ RatifyEnv {..} =
     disableBootstrap :: IsConwayUniv fn => Term fn (PParams Conway) -> Pred fn
     disableBootstrap pp = match pp $ \pp' ->
       match (sel @12 pp') $ \major _ ->
-        assert $ not_ (major ==. lit (natVersion @9))
+        assert $ major ==. lit (natVersion @10)
+    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 =>
@@ -419,20 +429,21 @@ instance IsConwayUniv fn => ExecSpecRule fn "RATIFY" Conway where
       $ Agda.ratifyStep env st sig
 
   extraInfo ctx env@RatifyEnv {..} st sig@(RatifySignal actions) =
-    unlines $
-      [ "Spec extra info:"
-      , either show T.unpack . runSpecTransM ctx $
-          Agda.ratifyDebug
-            <$> toSpecRep env
-            <*> toSpecRep st
-            <*> toSpecRep sig
-      , "\nImpl extra info:"
-      ]
-        <> 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
           [ "GovActionId: \t" <> showExpr gasId
@@ -448,13 +459,11 @@ instance IsConwayUniv fn => ExecSpecRule fn "RATIFY" Conway where
               <> show (committeeAcceptedRatio members gasCommitteeVotes reCommitteeState reCurrentEpoch)
               <> "\t"
               <> showAccepted (committeeAccepted env st gas)
-          , ""
           ]
 
   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%"
@@ -484,11 +493,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