From 80cb218752bf8cfbadb52e8358769db45dd335e7 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Joosep=20J=C3=A4=C3=A4ger?= Date: Tue, 13 Aug 2024 17:27:33 +0300 Subject: [PATCH] Print out the exception when an ImpTestM example fails --- cabal.project | 6 +- .../src/Cardano/Ledger/Conway/Governance.hs | 1 + .../Ledger/Conway/Governance/Procedures.hs | 10 +++ .../src/Cardano/Ledger/Conway/Rules/Ratify.hs | 17 ++++- .../Test/Cardano/Ledger/Shelley/ImpTest.hs | 11 +-- .../src/Test/Cardano/Ledger/Conformance.hs | 14 ++-- .../Conformance/ExecSpecRule/Conway/Base.hs | 33 ++++++--- .../Cardano/Ledger/Conformance/Imp/Ratify.hs | 70 ++++++++++++++----- .../Ledger/Constrained/Conway/Instances.hs | 2 +- 9 files changed, 118 insertions(+), 46 deletions(-) diff --git a/cabal.project b/cabal.project index 5300e3ca408..171d90dedea 100644 --- a/cabal.project +++ b/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 diff --git a/eras/conway/impl/src/Cardano/Ledger/Conway/Governance.hs b/eras/conway/impl/src/Cardano/Ledger/Conway/Governance.hs index 4cdef191794..7b2c210d1d9 100644 --- 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 index e62c0337430..4f37bd429bf 100644 --- 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 index 6156251b97f..996e549221a 100644 --- 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,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) $ diff --git a/eras/shelley/impl/testlib/Test/Cardano/Ledger/Shelley/ImpTest.hs b/eras/shelley/impl/testlib/Test/Cardano/Ledger/Shelley/ImpTest.hs index 16eeccfc55f..3889729d5a5 100644 --- 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,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 diff --git a/libs/cardano-ledger-conformance/src/Test/Cardano/Ledger/Conformance.hs b/libs/cardano-ledger-conformance/src/Test/Cardano/Ledger/Conformance.hs index 087a89f11be..699f888ad40 100644 --- 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/libs/cardano-ledger-conformance/src/Test/Cardano/Ledger/Conformance/ExecSpecRule/Conway/Base.hs b/libs/cardano-ledger-conformance/src/Test/Cardano/Ledger/Conformance/ExecSpecRule/Conway/Base.hs index aef1201f375..0f3144e14a0 100644 --- a/libs/cardano-ledger-conformance/src/Test/Cardano/Ledger/Conformance/ExecSpecRule/Conway/Base.hs +++ b/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 diff --git a/libs/cardano-ledger-conformance/test/Test/Cardano/Ledger/Conformance/Imp/Ratify.hs b/libs/cardano-ledger-conformance/test/Test/Cardano/Ledger/Conformance/Imp/Ratify.hs index 8f3f4e72d69..d63a36af570 100644 --- a/libs/cardano-ledger-conformance/test/Test/Cardano/Ledger/Conformance/Imp/Ratify.hs +++ b/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,13 +73,22 @@ 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 @@ -83,14 +96,19 @@ spec = describe "RATIFY" . withImpStateWithProtVer @Conway (natVersion @10) $ do 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 diff --git a/libs/cardano-ledger-test/src/Test/Cardano/Ledger/Constrained/Conway/Instances.hs b/libs/cardano-ledger-test/src/Test/Cardano/Ledger/Constrained/Conway/Instances.hs index 75d668caa42..0315b60a9cd 100644 --- a/libs/cardano-ledger-test/src/Test/Cardano/Ledger/Constrained/Conway/Instances.hs +++ b/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