From 1900f2908b42585e33a46d62e14207ebb39b69cc Mon Sep 17 00:00:00 2001 From: Maximilian Algehed Date: Tue, 17 Dec 2024 19:55:05 +0100 Subject: [PATCH] Constrained generators for `EPOCH` rule (#4740) --- .../Test/Cardano/Ledger/Conway/Arbitrary.hs | 9 +- .../Conformance/ExecSpecRule/Conway/Base.hs | 35 ++++---- .../Ledger/Constrained/Conway/Epoch.hs | 90 +++++++++++++++++-- .../Cardano/Ledger/Constrained/Conway/Gov.hs | 19 ++-- .../Constrained/Conway/Instances/Ledger.hs | 56 +++++++----- .../Constrained/Conway/Instances/TxBody.hs | 2 +- .../Cardano/Ledger/Constrained/Conway/Utxo.hs | 2 +- .../src/Test/Cardano/Ledger/STS.hs | 57 +++++++++--- .../constrained-generators/src/Constrained.hs | 1 + .../src/Constrained/Base.hs | 66 +++++++++++--- .../src/Constrained/Spec/Generics.hs | 4 +- .../src/Constrained/Spec/Map.hs | 2 +- 12 files changed, 257 insertions(+), 86 deletions(-) diff --git a/eras/conway/impl/testlib/Test/Cardano/Ledger/Conway/Arbitrary.hs b/eras/conway/impl/testlib/Test/Cardano/Ledger/Conway/Arbitrary.hs index 9b2d9656606..3d54e5b0124 100644 --- a/eras/conway/impl/testlib/Test/Cardano/Ledger/Conway/Arbitrary.hs +++ b/eras/conway/impl/testlib/Test/Cardano/Ledger/Conway/Arbitrary.hs @@ -346,10 +346,17 @@ instance pure $ ProposalsNewActions ps gass instance - (EraPParams era, Arbitrary (PParamsUpdate era), Arbitrary (PParamsHKD StrictMaybe era)) => + (EraPParams era, Arbitrary (PParamsHKD StrictMaybe era)) => Arbitrary (Proposals era) where arbitrary = genProposals (0, 30) + shrink ps = + [ ps' + | gais' <- shrink gais + , let (ps', _) = proposalsRemoveWithDescendants (gais Set.\\ gais') ps + ] + where + gais = Set.fromList (toList $ proposalsIds ps) genProposals :: forall era. 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 6f123b3364d..f692ce73fa8 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 @@ -14,6 +14,7 @@ {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TypeApplications #-} {-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE TypeOperators #-} {-# LANGUAGE UndecidableInstances #-} {-# LANGUAGE ViewPatterns #-} {-# OPTIONS_GHC -Wno-orphans #-} @@ -30,6 +31,8 @@ module Test.Cardano.Ledger.Conformance.ExecSpecRule.Conway.Base ( externalFunctions, ) where +import Cardano.Crypto.DSIGN (SignedDSIGN (..), verifySignedDSIGN) +import Cardano.Ledger.Address (RewardAccount) import Cardano.Ledger.BaseTypes ( EpochInterval (..), EpochNo (..), @@ -72,14 +75,18 @@ import Cardano.Ledger.Conway.Rules ( spoAccepted, spoAcceptedRatio, ) +import Cardano.Ledger.Credential (Credential) import Cardano.Ledger.DRep (DRep (..)) import Cardano.Ledger.PoolDistr (IndividualPoolStake (..)) import Constrained hiding (inject) +import Data.Either (isRight) import Data.Foldable (Foldable (..)) import Data.Map.Strict (Map) import qualified Data.Map.Strict as Map +import Data.Maybe (fromMaybe) import Data.Ratio (denominator, numerator, (%)) import qualified Data.Sequence.Strict as SSeq +import Data.Set (Set) import qualified Data.Set as Set import GHC.Generics (Generic) import Lens.Micro (Lens', lens, (^.)) @@ -103,29 +110,19 @@ import Test.Cardano.Ledger.Conformance.SpecTranslate.Conway.Base ( signatureFromInteger, ) import Test.Cardano.Ledger.Constrained.Conway ( - EpochExecEnv, - IsConwayUniv, - coerce_, - epochEnvSpec, - epochSignalSpec, - epochStateSpec, newEpochStateSpec, ) +import Test.Cardano.Ledger.Constrained.Conway.Epoch +import Test.Cardano.Ledger.Constrained.Conway.Instances.Ledger import Test.Cardano.Ledger.Constrained.Conway.Instances.PParams ( committeeMaxTermLength_, committeeMinSize_, protocolVersion_, ) -import Cardano.Crypto.DSIGN (SignedDSIGN (..), verifySignedDSIGN) import Cardano.Crypto.Hash (ByteString, Hash) -import Cardano.Ledger.Address (RewardAccount) -import Cardano.Ledger.Credential (Credential) import Cardano.Ledger.Crypto (DSIGN, HASH) import Cardano.Ledger.Keys (KeyRole (..), VKey (..)) -import Data.Either (isRight) -import Data.Maybe (fromMaybe) -import Data.Set (Set) import Test.Cardano.Ledger.Conway.Arbitrary () import Test.Cardano.Ledger.Imp.Common hiding (arbitrary, forAll, prop, var) @@ -572,15 +569,17 @@ nameGovAction UpdateCommittee {} = "UpdateCommittee" nameGovAction NewConstitution {} = "NewConstitution" nameGovAction InfoAction {} = "InfoAction" -instance IsConwayUniv fn => ExecSpecRule fn "EPOCH" ConwayEra where +-- The `fn ~ ConwayFn` thing here is because `ConwayFn` is a type alias +-- and those shouldn't go in instance heads apparently. +instance fn ~ ConwayFn => ExecSpecRule fn "EPOCH" ConwayEra where type ExecContext fn "EPOCH" ConwayEra = [GovActionState ConwayEra] type ExecEnvironment fn "EPOCH" ConwayEra = EpochExecEnv ConwayEra environmentSpec _ = epochEnvSpec - stateSpec _ _ = epochStateSpec + stateSpec _ = epochStateSpec . lit . eeeEpochNo - signalSpec _ _ _ = epochSignalSpec + signalSpec _ env _ = epochSignalSpec (eeeEpochNo env) runAgdaRule env st sig = unComputationResult_ $ Agda.epochStep env st sig @@ -589,7 +588,9 @@ instance IsConwayUniv fn => ExecSpecRule fn "EPOCH" ConwayEra where nameEpoch :: EpochNo -> String nameEpoch x = show x -instance IsConwayUniv fn => ExecSpecRule fn "NEWEPOCH" ConwayEra where +-- The `fn ~ ConwayFn` thing here is because `ConwayFn` is a type alias +-- and those shouldn't go in instance heads apparently. +instance fn ~ ConwayFn => ExecSpecRule fn "NEWEPOCH" ConwayEra where type ExecContext fn "NEWEPOCH" ConwayEra = [GovActionState ConwayEra] type ExecEnvironment fn "NEWEPOCH" ConwayEra = EpochExecEnv ConwayEra @@ -597,7 +598,7 @@ instance IsConwayUniv fn => ExecSpecRule fn "NEWEPOCH" ConwayEra where stateSpec _ _ = newEpochStateSpec - signalSpec _ _ _ = epochSignalSpec + signalSpec _ env _ = epochSignalSpec (eeeEpochNo env) runAgdaRule env st sig = unComputationResult_ $ Agda.newEpochStep env st sig diff --git a/libs/cardano-ledger-test/src/Test/Cardano/Ledger/Constrained/Conway/Epoch.hs b/libs/cardano-ledger-test/src/Test/Cardano/Ledger/Constrained/Conway/Epoch.hs index ba9340ac97b..fcf640bc9cf 100644 --- a/libs/cardano-ledger-test/src/Test/Cardano/Ledger/Constrained/Conway/Epoch.hs +++ b/libs/cardano-ledger-test/src/Test/Cardano/Ledger/Constrained/Conway/Epoch.hs @@ -1,8 +1,11 @@ {-# LANGUAGE DataKinds #-} {-# LANGUAGE DeriveGeneric #-} {-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE QuasiQuotes #-} {-# LANGUAGE RankNTypes #-} +{-# LANGUAGE RecordWildCards #-} {-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE ViewPatterns #-} -- | Specs necessary to generate, environment, state, and signal -- for the EPOCH rule @@ -11,21 +14,96 @@ module Test.Cardano.Ledger.Constrained.Conway.Epoch where import Cardano.Ledger.BaseTypes import Cardano.Ledger.Coin import Cardano.Ledger.Conway (ConwayEra) +import Cardano.Ledger.Conway.Governance import Cardano.Ledger.Shelley.API.Types import Constrained -import Data.Map.Strict +import Data.Foldable +import Data.Map.Strict (Map) import GHC.Generics (Generic) +import Lens.Micro.Extras +import Test.Cardano.Ledger.Constrained.Conway.Gov +import Test.Cardano.Ledger.Constrained.Conway.Instances -newtype EpochExecEnv era = EpochExecEnv +data EpochExecEnv era = EpochExecEnv { eeeStakeDistr :: Map (Credential 'Staking) (CompactForm Coin) + , eeeEpochNo :: EpochNo } deriving (Generic, Eq, Show) epochEnvSpec :: Specification fn (EpochExecEnv ConwayEra) epochEnvSpec = TrueSpec -epochStateSpec :: Specification fn (EpochState ConwayEra) -epochStateSpec = TrueSpec +epochStateSpec :: + Term ConwayFn EpochNo -> + Specification ConwayFn (EpochState ConwayEra) +epochStateSpec epochNo = constrained $ \es -> + match es $ \_accountState ledgerState _snapShots _nonMyopic -> + match ledgerState $ \utxoState certState -> + match utxoState $ \_utxo _deposited _fees govState _stakeDistr _donation -> + match govState $ \ [var| proposals |] _committee constitution _curPParams _prevPParams _futPParams drepPulsingState -> + [ match constitution $ \_ policy -> + proposals `satisfies` proposalsSpec epochNo policy certState + , caseOn + drepPulsingState + -- DRPulsing + ( branch $ \pulser -> + match pulser $ \_size _stakeMap _index _stakeDistr _stakePoolDistr _drepDistr _drepState pulseEpoch _committeeState _enactState pulseProposals _proposalDeposits _poolParams -> + [ assert $ pulseEpoch ==. epochNo + , forAll pulseProposals $ \gas -> + match gas $ \gasId _ _ _ _ _ _ -> + proposalExists gasId proposals + , -- TODO: something is wrong in this case and I haven't figured out what yet + assert False + ] + ) + -- DRComplete + ( branch $ \_snap ratifyState -> + match ratifyState $ \enactState [var| enacted |] expired _delayed -> + [ forAll expired $ \ [var| gasId |] -> + proposalExists gasId proposals + , -- TODO: this isn't enough, we need to ensure it's at most + -- one of each type of action that's being enacted + forAll enacted $ \govact -> + [ reify proposals enactableProposals $ \enactable -> govact `elem_` enactable + , assert $ not_ $ gasId_ govact `member_` expired + ] + , -- TODO: this is a hack to get around the todo above! + assert $ sizeOf_ enacted <=. 1 + , match enactState $ + \_cc _con _cpp _ppp _tr _wth prevGACTIDS -> + reify proposals (toPrevGovActionIds . view pRootsL) (prevGACTIDS ==.) + ] + ) + ] -epochSignalSpec :: Specification fn EpochNo -epochSignalSpec = TrueSpec +proposalExists :: + Term ConwayFn GovActionId -> + Term ConwayFn (Proposals ConwayEra) -> + Pred ConwayFn +proposalExists gasId proposals = + reify proposals proposalsActionsMap $ \actionMap -> + gasId `member_` dom_ actionMap + +epochSignalSpec :: EpochNo -> Specification ConwayFn EpochNo +epochSignalSpec curEpoch = constrained $ \e -> + elem_ e (lit [curEpoch, succ curEpoch]) + +enactableProposals :: Proposals era -> [GovActionState era] +enactableProposals proposals = + [ gact' + | gact <- toList (proposalsActions proposals) + , gact' <- withGovActionParent gact [gact] $ + \_ mparent _ -> + case mparent of + SNothing -> [gact] + SJust (GovPurposeId gpid') + | isRoot gpid' proposals -> [gact] + | otherwise -> [] + ] + +isRoot :: GovActionId -> Proposals era -> Bool +isRoot gid (view pRootsL -> GovRelation {..}) = + SJust gid + `elem` [getGID grPParamUpdate, getGID grHardFork, getGID grCommittee, getGID grConstitution] + where + getGID = fmap unGovPurposeId . prRoot diff --git a/libs/cardano-ledger-test/src/Test/Cardano/Ledger/Constrained/Conway/Gov.hs b/libs/cardano-ledger-test/src/Test/Cardano/Ledger/Constrained/Conway/Gov.hs index 6620e87b411..975df7acf2b 100644 --- a/libs/cardano-ledger-test/src/Test/Cardano/Ledger/Constrained/Conway/Gov.hs +++ b/libs/cardano-ledger-test/src/Test/Cardano/Ledger/Constrained/Conway/Gov.hs @@ -47,13 +47,13 @@ govProposalsSpec :: GovEnv ConwayEra -> Specification fn (Proposals ConwayEra) govProposalsSpec GovEnv {geEpoch, gePPolicy, geCertState} = - proposalsSpec (lit geEpoch) (lit gePPolicy) geCertState + proposalsSpec (lit geEpoch) (lit gePPolicy) (lit geCertState) proposalsSpec :: IsConwayUniv fn => Term fn EpochNo -> Term fn (StrictMaybe ScriptHash) -> - CertState ConwayEra -> + Term fn (CertState ConwayEra) -> Specification fn (Proposals ConwayEra) proposalsSpec geEpoch gePPolicy geCertState = constrained $ \ [var|props|] -> @@ -155,11 +155,14 @@ proposalsSpec geEpoch gePPolicy geCertState = Explain (pure "TreasuryWithdrawal fails") $ Block [ dependsOn gasOther withdrawMap - , forAll (dom_ withdrawMap) $ \ [var|rewAcnt|] -> - match rewAcnt $ \ [var|network|] [var|credential|] -> - [ network ==. lit Testnet - , credential `member_` lit registeredCredentials - ] + , match geCertState $ \_vState _pState [var|dState|] -> + match dState $ \ [var|rewardMap|] _ _ _ -> + reify rewardMap (Map.keysSet . umElems) $ \ [var|registeredCredentials|] -> + forAll (dom_ withdrawMap) $ \ [var|rewAcnt|] -> + match rewAcnt $ \ [var|network|] [var|credential|] -> + [ network ==. lit Testnet + , credential `member_` registeredCredentials + ] , assert $ policy ==. gePPolicy ] ) @@ -173,7 +176,6 @@ proposalsSpec geEpoch gePPolicy geCertState = where treeGenHint = (Just 2, 10) listSizeHint = 5 - registeredCredentials = Map.keysSet $ umElems $ dsUnified $ certDState geCertState allGASInTree :: (IsConwayUniv fn, IsPred p fn) => @@ -279,6 +281,7 @@ withPrevActId gas k = -- InfoAction (branch $ \_ -> True) ] + onHardFork :: (IsConwayUniv fn, IsPred p fn) => Term fn (GovActionState ConwayEra) -> diff --git a/libs/cardano-ledger-test/src/Test/Cardano/Ledger/Constrained/Conway/Instances/Ledger.hs b/libs/cardano-ledger-test/src/Test/Cardano/Ledger/Constrained/Conway/Instances/Ledger.hs index 8e8cd0dfdf6..b0a97386c22 100644 --- a/libs/cardano-ledger-test/src/Test/Cardano/Ledger/Constrained/Conway/Instances/Ledger.hs +++ b/libs/cardano-ledger-test/src/Test/Cardano/Ledger/Constrained/Conway/Instances/Ledger.hs @@ -18,6 +18,7 @@ {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE TypeOperators #-} {-# LANGUAGE UndecidableInstances #-} +{-# LANGUAGE ViewPatterns #-} {-# OPTIONS_GHC -Wno-orphans #-} {-# OPTIONS_GHC -Wno-redundant-constraints #-} @@ -53,6 +54,7 @@ module Test.Cardano.Ledger.Constrained.Conway.Instances.Ledger ( gasCommitteeVotes_, gasDRepVotes_, gasProposalProcedure_, + psPParamUpdate_, ProposalsSplit (..), genProposalsSplit, proposalSplitSum, @@ -132,7 +134,7 @@ import Cardano.Ledger.TxIn (TxId (..), TxIn (..)) import Cardano.Ledger.UMap import Cardano.Ledger.UTxO import Cardano.Ledger.Val (Val) -import Constrained hiding (Value) +import Constrained hiding (Sized, Value) import Constrained qualified as C import Constrained.Base (Binder (..), HasGenHint (..), Pred (..), Term (..)) import Constrained.Spec.Map @@ -168,6 +170,7 @@ import PlutusLedgerApi.V1 qualified as PV1 import Test.Cardano.Ledger.Allegra.Arbitrary () import Test.Cardano.Ledger.Alonzo.Arbitrary () import Test.Cardano.Ledger.Constrained.Conway.Instances.Basic +import Test.Cardano.Ledger.Conway.Arbitrary () import Test.Cardano.Ledger.Core.Utils import Test.Cardano.Ledger.Shelley.Utils import Test.Cardano.Ledger.TreeDiff (ToExpr) @@ -219,7 +222,7 @@ type ConwayTxBodyTypes = instance (EraSpecPParams ConwayEra, IsConwayUniv fn) => HasSpec fn (ConwayTxBody ConwayEra) instance HasSimpleRep (ConwayTxBody ConwayEra) where - type SimpleRep (ConwayTxBody ConwayEra) = SOP '["ConwayTxBody" ::: ConwayTxBodyTypes] + type TheSop (ConwayTxBody ConwayEra) = '["ConwayTxBody" ::: ConwayTxBodyTypes] toSimpleRep ConwayTxBody {..} = inject @"ConwayTxBody" @'["ConwayTxBody" ::: ConwayTxBodyTypes] ctbSpendInputs @@ -294,12 +297,15 @@ instance HasSimpleRep (StrictSeq a) where toSimpleRep = toList fromSimpleRep = StrictSeq.fromList instance (IsConwayUniv fn, HasSpec fn a) => HasSpec fn (StrictSeq a) +instance Forallable (StrictSeq a) a instance HasSimpleRep (Seq a) where type SimpleRep (Seq a) = [a] toSimpleRep = toList fromSimpleRep = Seq.fromList -instance (IsConwayUniv fn, HasSpec fn a) => HasSpec fn (Seq a) +instance HasSpec fn a => HasSpec fn (Seq a) +instance Forallable (Seq a) a +instance HasSpec fn a => C.Sized fn (Seq a) instance HasSimpleRep (Sized a) instance (IsConwayUniv fn, HasSpec fn a) => HasSpec fn (Sized a) @@ -321,7 +327,6 @@ type ShelleyTxOutTypes era = , Value era ] instance (Era era, Val (Value era)) => HasSimpleRep (ShelleyTxOut era) where - -- type SimpleRep (ShelleyTxOut era) = SOP '["ShelleyTxOut" ::: ShelleyTxOutTypes era] type TheSop (ShelleyTxOut era) = '["ShelleyTxOut" ::: ShelleyTxOutTypes era] toSimpleRep (ShelleyTxOut addr val) = inject @"ShelleyTxOut" @'["ShelleyTxOut" ::: ShelleyTxOutTypes era] @@ -338,7 +343,6 @@ type AlonzoTxOutTypes era = , StrictMaybe DataHash ] instance (Era era, Val (Value era)) => HasSimpleRep (AlonzoTxOut era) where - -- type SimpleRep (AlonzoTxOut era) = SOP '["AlonzoTxOut" ::: AlonzoTxOutTypes era] type TheSop (AlonzoTxOut era) = '["AlonzoTxOut" ::: AlonzoTxOutTypes era] toSimpleRep (AlonzoTxOut addr val mdat) = inject @"AlonzoTxOut" @'["AlonzoTxOut" ::: AlonzoTxOutTypes era] @@ -974,13 +978,13 @@ type UMapTypes = , Map (Credential 'Staking) DRep ] instance HasSimpleRep UMap where - type SimpleRep UMap = SOP '["UMap" ::: UMapTypes] + type TheSop UMap = '["UMap" ::: UMapTypes] toSimpleRep um = inject @"UMap" @'["UMap" ::: UMapTypes] (rdPairMap um) (ptrMap um) (sPoolMap um) (dRepMap um) fromSimpleRep rep = algebra @'["UMap" ::: UMapTypes] rep unify instance IsConwayUniv fn => HasSpec fn UMap instance HasSimpleRep RDPair where - type SimpleRep RDPair = SOP '["RDPair" ::: '[SimpleRep Coin, SimpleRep Coin]] + type TheSop RDPair = '["RDPair" ::: '[SimpleRep Coin, SimpleRep Coin]] toSimpleRep (RDPair rew dep) = inject @"RDPair" @@ -1072,7 +1076,7 @@ type ProposalsType era = -- this right now. ] instance EraPParams era => HasSimpleRep (Proposals era) where - type SimpleRep (Proposals era) = SOP '["Proposals" ::: ProposalsType era] + type TheSop (Proposals era) = '["Proposals" ::: ProposalsType era] toSimpleRep props = inject @"Proposals" @'["Proposals" ::: ProposalsType era] (buildProposalTree $ coerce grPParamUpdate) @@ -1116,7 +1120,13 @@ instance EraPParams era => HasSimpleRep (Proposals era) where where mkOMap (Node a ts) = a OMap.<| foldMap mkOMap ts -instance (EraSpecPParams era, IsConwayUniv fn) => HasSpec fn (Proposals era) +instance (EraSpecPParams era, IsConwayUniv fn, Arbitrary (Proposals era)) => HasSpec fn (Proposals era) where + shrinkWithTypeSpec _ props = shrink props + +psPParamUpdate_ :: + (EraSpecPParams era, Arbitrary (Proposals era), IsConwayUniv fn) => + Term fn (Proposals era) -> Term fn (ProposalTree era) +psPParamUpdate_ = sel @0 data ProposalsSplit = ProposalsSplit { psPPChange :: Integer @@ -1343,8 +1353,8 @@ instance (DRepPulser ConwayEra Identity (RatifyState ConwayEra)) where type - SimpleRep (DRepPulser ConwayEra Identity (RatifyState ConwayEra)) = - SOP '["DRepPulser" ::: DRepPulserTypes] + TheSop (DRepPulser ConwayEra Identity (RatifyState ConwayEra)) = + '["DRepPulser" ::: DRepPulserTypes] toSimpleRep DRepPulser {..} = inject @"DRepPulser" @'["DRepPulser" ::: DRepPulserTypes] dpPulseSize @@ -1408,7 +1418,7 @@ instance HasSpec fn (ShelleyTx era) instance EraSpecPParams era => HasSimpleRep (ShelleyTx era) where - type SimpleRep (ShelleyTx era) = SOP '["ShelleyTx" ::: ShelleyTxTypes era] + type TheSop (ShelleyTx era) = '["ShelleyTx" ::: ShelleyTxTypes era] toSimpleRep (ShelleyTx body wits auxdata) = inject @"ShelleyTx" @'["ShelleyTx" ::: ShelleyTxTypes era] body @@ -1432,8 +1442,8 @@ type AlonzoTxAuxDataTypes era = ] instance AlonzoEraScript era => HasSimpleRep (AlonzoTxAuxData era) where type - SimpleRep (AlonzoTxAuxData era) = - SOP '["AlonzoTxOutData" ::: AlonzoTxAuxDataTypes era] + TheSop (AlonzoTxAuxData era) = + '["AlonzoTxOutData" ::: AlonzoTxAuxDataTypes era] toSimpleRep (AlonzoTxAuxData metaMap tsSeq _) = inject @"AlonzoTxAuxData" @'["AlonzoTxAuxData" ::: AlonzoTxAuxDataTypes era] metaMap @@ -1456,8 +1466,8 @@ type AllegraTxAuxDataTypes era = ] instance Era era => HasSimpleRep (AllegraTxAuxData era) where type - SimpleRep (AllegraTxAuxData era) = - SOP '["AllegraTxOutData" ::: AllegraTxAuxDataTypes era] + TheSop (AllegraTxAuxData era) = + '["AllegraTxOutData" ::: AllegraTxAuxDataTypes era] toSimpleRep (AllegraTxAuxData metaMap tsSeq) = inject @"AllegraTxAuxData" @'["AllegraTxAuxData" ::: AllegraTxAuxDataTypes era] metaMap @@ -1479,8 +1489,8 @@ type ShelleyTxAuxDataTypes era = ] instance Era era => HasSimpleRep (ShelleyTxAuxData era) where type - SimpleRep (ShelleyTxAuxData era) = - SOP '["ShelleyTxAuxData" ::: ShelleyTxAuxDataTypes era] + TheSop (ShelleyTxAuxData era) = + '["ShelleyTxAuxData" ::: ShelleyTxAuxDataTypes era] toSimpleRep (ShelleyTxAuxData metaMap) = inject @"ShelleyTxAuxData" @'["ShelleyTxAuxData" ::: ShelleyTxAuxDataTypes era] metaMap @@ -1508,8 +1518,8 @@ type AlonzoTxWitsTypes = ] instance AlonzoEraScript era => HasSimpleRep (AlonzoTxWits era) where type - SimpleRep (AlonzoTxWits era) = - SOP '["AlonzoTxWits" ::: AlonzoTxWitsTypes] + TheSop (AlonzoTxWits era) = + '["AlonzoTxWits" ::: AlonzoTxWitsTypes] toSimpleRep (AlonzoTxWits vkeyWits bootstrapWits _ _ _) = inject @"AlonzoTxWits" @'["AlonzoTxWits" ::: AlonzoTxWitsTypes] vkeyWits @@ -1525,8 +1535,8 @@ type ShelleyTxWitsTypes era = ] instance EraScript era => HasSimpleRep (ShelleyTxWits era) where type - SimpleRep (ShelleyTxWits era) = - SOP '["ShelleyTxWits" ::: ShelleyTxWitsTypes era] + TheSop (ShelleyTxWits era) = + '["ShelleyTxWits" ::: ShelleyTxWitsTypes era] toSimpleRep (ShelleyTxWits vkeyWits _ bootstrapWits) = inject @"ShelleyTxWits" @'["ShelleyTxWits" ::: ShelleyTxWitsTypes era] vkeyWits @@ -1644,7 +1654,7 @@ type PulserTypes = , RewardAns ] instance HasSimpleRep Pulser where - type SimpleRep Pulser = SOP '["Pulser" ::: PulserTypes] + type TheSop Pulser = '["Pulser" ::: PulserTypes] toSimpleRep (RSLP n free bal ans) = inject @"Pulser" @'["Pulser" ::: PulserTypes] n diff --git a/libs/cardano-ledger-test/src/Test/Cardano/Ledger/Constrained/Conway/Instances/TxBody.hs b/libs/cardano-ledger-test/src/Test/Cardano/Ledger/Constrained/Conway/Instances/TxBody.hs index 59417686abe..0abf8534b5c 100644 --- a/libs/cardano-ledger-test/src/Test/Cardano/Ledger/Constrained/Conway/Instances/TxBody.hs +++ b/libs/cardano-ledger-test/src/Test/Cardano/Ledger/Constrained/Conway/Instances/TxBody.hs @@ -29,7 +29,7 @@ import Cardano.Ledger.Mary.Value (MultiAsset (..)) import Cardano.Ledger.Shelley.PParams (Update (..)) import Cardano.Ledger.Shelley.TxBody (ShelleyTxBody (..)) import Cardano.Ledger.TxIn (TxIn (..)) -import Constrained hiding (Value) +import Constrained hiding (Sized, Value) import Data.Foldable (toList) import Data.Map.Strict (Map) import qualified Data.Sequence.Strict as SS (fromList) diff --git a/libs/cardano-ledger-test/src/Test/Cardano/Ledger/Constrained/Conway/Utxo.hs b/libs/cardano-ledger-test/src/Test/Cardano/Ledger/Constrained/Conway/Utxo.hs index 002c4ef25a4..715ca983f61 100644 --- a/libs/cardano-ledger-test/src/Test/Cardano/Ledger/Constrained/Conway/Utxo.hs +++ b/libs/cardano-ledger-test/src/Test/Cardano/Ledger/Constrained/Conway/Utxo.hs @@ -123,7 +123,7 @@ utxoStateSpec UtxoExecContext {uecUTxO} UtxoEnv {ueSlot, ueCertState} = [ assert $ utxosUtxo ==. lit uecUTxO , match utxosGovState $ \props _ constitution _ _ _ _ -> match constitution $ \_ policy -> - satisfies props $ proposalsSpec (lit curEpoch) policy ueCertState + satisfies props $ proposalsSpec (lit curEpoch) policy (lit ueCertState) ] where curEpoch = runReader (epochFromSlot ueSlot) testGlobals diff --git a/libs/cardano-ledger-test/src/Test/Cardano/Ledger/STS.hs b/libs/cardano-ledger-test/src/Test/Cardano/Ledger/STS.hs index f666fa997a7..12dbf052e6f 100644 --- a/libs/cardano-ledger-test/src/Test/Cardano/Ledger/STS.hs +++ b/libs/cardano-ledger-test/src/Test/Cardano/Ledger/STS.hs @@ -22,6 +22,7 @@ import Constrained import Test.Cardano.Ledger.Constrained.Conway.Cert import Test.Cardano.Ledger.Constrained.Conway.Deleg +import Test.Cardano.Ledger.Constrained.Conway.Epoch import Test.Cardano.Ledger.Constrained.Conway.Gov import Test.Cardano.Ledger.Constrained.Conway.GovCert import Test.Cardano.Ledger.Constrained.Conway.Instances @@ -67,6 +68,34 @@ stsPropertyV2 :: (env -> st -> sig -> st -> p) -> Property stsPropertyV2 specEnv specState specSig prop = + stsPropertyV2' @r specEnv specState specSig (\env _ _ -> specState env) prop + +stsPropertyV2' :: + forall r fn env st sig fail p. + ( Environment (EraRule r ConwayEra) ~ env + , State (EraRule r ConwayEra) ~ st + , Signal (EraRule r ConwayEra) ~ sig + , PredicateFailure (EraRule r ConwayEra) ~ fail + , STS (EraRule r ConwayEra) + , BaseM (EraRule r ConwayEra) ~ ReaderT Globals Identity + , PrettyA st + , PrettyA sig + , PrettyA env + , PrettyA fail + , Testable p + , HasSpec fn env + , HasSpec fn st + , HasSpec fn sig + ) => + Specification fn env -> + (env -> Specification fn st) -> + (env -> st -> Specification fn sig) -> + -- This allows you to write a separate spec for the state after the transition + -- and thus e.g. loosening requirements set only for the sake of generation + (env -> st -> sig -> Specification fn st) -> + (env -> st -> sig -> st -> p) -> + Property +stsPropertyV2' specEnv specState specSig specPostState prop = uncurry forAllShrinkBlind (genShrinkFromSpec specEnv) $ \env -> counterexample (show $ ppString "env = " <> prettyA env) $ uncurry forAllShrinkBlind (genShrinkFromSpec $ specState env) $ \st -> @@ -74,7 +103,7 @@ stsPropertyV2 specEnv specState specSig prop = uncurry forAllShrinkBlind (genShrinkFromSpec $ specSig env st) $ \sig -> counterexample (show $ ppString "sig = " <> prettyA sig) $ runShelleyBase $ do - res <- applySTS @(EraRule r era) $ TRC (env, st, sig) + res <- applySTS @(EraRule r ConwayEra) $ TRC (env, st, sig) pure $ case res of Left pfailures -> counterexample (show $ prettyA pfailures) $ property False Right st' -> @@ -84,7 +113,7 @@ stsPropertyV2 specEnv specState specSig prop = <> prettyA st' <> ppString ("\nspec = \n" ++ show (specState env)) ) - $ conformsToSpec @fn st' (specState env) .&&. prop env st sig st' + $ conformsToSpecProp @fn st' (specPostState env st sig) .&&. prop env st sig st' -- STS properties --------------------------------------------------------- @@ -105,12 +134,14 @@ prop_GOV = -- (\_env _st -> TrueSpec) -- $ \_env _st _sig _st' -> True -prop_EPOCH :: Property -prop_EPOCH = - stsPropertyV2 @"EPOCH" @ConwayFn +prop_EPOCH :: EpochNo -> Property +prop_EPOCH epochNo = + stsPropertyV2' @"EPOCH" @ConwayFn TrueSpec - (\_env -> TrueSpec) - (\_env _st -> TrueSpec) + (\_env -> epochStateSpec (lit epochNo)) + (\_env _st -> epochSignalSpec epochNo) + (\_env _st _newEpoch -> TrueSpec) + -- (\_env _st newEpoch -> epochStateSpec (lit newEpoch)) $ \_env _st _sig _st' -> True prop_ENACT :: Property @@ -266,12 +297,12 @@ tests_STS = testGroup "STS property tests" [ govTests - -- , utxoTests - -- TODO: this is probably one of the last things we want to - -- get passing as it depends on being able to generate a complete - -- `EpochState era` - -- , testProperty "prop_EPOCH" prop_EPOCH - -- , testProperty "prop_LEDGER" prop_LEDGER + , -- , utxoTests + -- TODO: this is probably one of the last things we want to + -- get passing as it depends on being able to generate a complete + -- `EpochState era` + testProperty "prop_EPOCH" prop_EPOCH + -- , testProperty "prop_LEDGER" prop_LEDGER ] govTests :: TestTree diff --git a/libs/constrained-generators/src/Constrained.hs b/libs/constrained-generators/src/Constrained.hs index 8b5c0f4bbeb..24389acfdf3 100644 --- a/libs/constrained-generators/src/Constrained.hs +++ b/libs/constrained-generators/src/Constrained.hs @@ -36,6 +36,7 @@ module Constrained ( NumSpec (..), MapSpec (..), FoldSpec (..), + Sized (..), simplifySpec, addToErrorSpec, genFromSpecT, diff --git a/libs/constrained-generators/src/Constrained/Base.hs b/libs/constrained-generators/src/Constrained/Base.hs index 6df2ce57b9d..2c128cc1619 100644 --- a/libs/constrained-generators/src/Constrained/Base.hs +++ b/libs/constrained-generators/src/Constrained/Base.hs @@ -51,6 +51,7 @@ module Constrained.Base where import Control.Applicative import Control.Arrow (first) +import Control.Exception (SomeException, catch) import Control.Monad import Control.Monad.Identity import Control.Monad.Writer (Writer, runWriter, tell) @@ -75,6 +76,7 @@ import GHC.Real import GHC.Stack import GHC.TypeLits import Prettyprinter +import System.IO.Unsafe import System.Random import System.Random.Stateful import Test.QuickCheck hiding (Args, Fun, forAll) @@ -1278,7 +1280,11 @@ envFromPred env p = case p of -- | A version of `genFromSpecT` that simply errors if the generator fails genFromSpec :: forall fn a. (HasCallStack, HasSpec fn a) => Specification fn a -> Gen a genFromSpec spec = do - res <- strictGen $ explain1 "Calling genFromSpec" $ genFromSpecT spec + res <- strictGen $ explain1 "Calling genFromSpec" $ do + r <- genFromSpecT spec + unsafePerformIO $ + r `seq` + pure (pure r) `catch` \(e :: SomeException) -> pure (fatalError (pure $ show e)) errorGE $ fmap pure res -- | A version of `genFromSpecT` that takes a seed and a size and gives you a result @@ -1375,7 +1381,7 @@ data SolverStage fn where instance Pretty (SolverStage fn) where pretty SolverStage {..} = - ("\nSolving for variable " <+> viaShow stageVar) + viaShow stageVar <+> "<-" /> vsep' ( [pretty stageSpec | not $ isTrueSpec stageSpec] @@ -5197,7 +5203,7 @@ fromList_ = app fromListFn sizeOf_ :: forall a fn. - (HasSpec fn a, Sized a) => + (HasSpec fn a, Sized fn a) => Term fn a -> Term fn Integer sizeOf_ = app sizeOfFn @@ -5218,7 +5224,7 @@ length_ :: Term fn Integer length_ = app sizeOfFn -null_ :: (HasSpec fn a, Sized a) => Term fn a -> Term fn Bool +null_ :: (HasSpec fn a, Sized fn a) => Term fn a -> Term fn Bool null_ xs = sizeOf_ xs ==. 0 -- ##### @@ -5690,15 +5696,15 @@ genFromSizeSpec :: (BaseUniverse fn, MonadGenError m) => Specification fn Intege genFromSizeSpec integerSpec = genFromSpecT (integerSpec <> geqSpec 0) data SizeFn (fn :: [Type] -> Type -> Type) as b where - SizeOf :: forall fn a. (Sized a, HasSpec fn a) => SizeFn fn '[a] Integer + SizeOf :: forall fn a. (Sized fn a, HasSpec fn a) => SizeFn fn '[a] Integer deriving instance Eq (SizeFn fn as b) deriving instance Show (SizeFn fn as b) instance FunctionLike (SizeFn fn) where - sem SizeOf = sizeOf -- From the Sized class + sem SizeOf = sizeOf @fn -- From the Sized class -sizeOfFn :: forall fn a. (HasSpec fn a, Member (SizeFn fn) fn, Sized a) => fn '[a] Integer +sizeOfFn :: forall fn a. (HasSpec fn a, Member (SizeFn fn) fn, Sized fn a) => fn '[a] Integer sizeOfFn = injectFn $ SizeOf @fn @a -- Operations on Size (specified in SizeFn) by the Functions instance @@ -5745,13 +5751,45 @@ maxSpec (TypeSpec (NumSpecInterval _ hi) bad) = TypeSpec (NumSpecInterval Nothin -- Sized -- ================ -class Sized t where +class Sized fn t where sizeOf :: t -> Integer + default sizeOf :: (HasSimpleRep t, Sized fn (SimpleRep t)) => t -> Integer + sizeOf = sizeOf @fn . toSimpleRep + liftSizeSpec :: HasSpec fn t => SizeSpec fn -> [Integer] -> Specification fn t + default liftSizeSpec :: + ( HasSpec fn t + , HasSimpleRep t + , Sized fn (SimpleRep t) + , HasSpec fn (SimpleRep t) + , TypeSpec fn t ~ TypeSpec fn (SimpleRep t) + ) => + SizeSpec fn -> [Integer] -> Specification fn t + liftSizeSpec sz cant = fromSimpleRepSpec $ liftSizeSpec sz cant + liftMemberSpec :: HasSpec fn t => OrdSet Integer -> Specification fn t + default liftMemberSpec :: + ( HasSpec fn t + , HasSpec fn (SimpleRep t) + , HasSimpleRep t + , Sized fn (SimpleRep t) + , TypeSpec fn t ~ TypeSpec fn (SimpleRep t) + ) => + OrdSet Integer -> Specification fn t + liftMemberSpec = fromSimpleRepSpec . liftMemberSpec + sizeOfTypeSpec :: HasSpec fn t => TypeSpec fn t -> Specification fn Integer + default sizeOfTypeSpec :: + ( HasSpec fn t + , HasSpec fn (SimpleRep t) + , HasSimpleRep t + , Sized fn (SimpleRep t) + , TypeSpec fn t ~ TypeSpec fn (SimpleRep t) + ) => + TypeSpec fn t -> Specification fn Integer + sizeOfTypeSpec = sizeOfTypeSpec @fn @(SimpleRep t) -instance Ord a => Sized (Set.Set a) where +instance Ord a => Sized fn (Set.Set a) where sizeOf = toInteger . Set.size liftSizeSpec spec cant = typeSpec (SetSpec mempty TrueSpec (TypeSpec spec cant)) liftMemberSpec xs = case NE.nonEmpty xs of @@ -5759,7 +5797,7 @@ instance Ord a => Sized (Set.Set a) where Just zs -> typeSpec (SetSpec mempty TrueSpec (MemberSpec zs)) sizeOfTypeSpec (SetSpec must _ sz) = sz <> geqSpec (sizeOf must) -instance Sized [a] where +instance Sized fn [a] where sizeOf = toInteger . length liftSizeSpec spec cant = typeSpec (ListSpec Nothing mempty (TypeSpec spec cant) TrueSpec NoFold) liftMemberSpec xs = case NE.nonEmpty xs of @@ -5769,7 +5807,7 @@ instance Sized [a] where sizeOfTypeSpec (ListSpec _ must sizespec _ _) = sizespec <> geqSpec (sizeOf must) -- How to constrain the size of any type, with a Sized instance -hasSize :: (HasSpec fn t, Sized t) => SizeSpec fn -> Specification fn t +hasSize :: (HasSpec fn t, Sized fn t) => SizeSpec fn -> Specification fn t hasSize sz = liftSizeSpec sz [] -- ================================================================================== @@ -6034,17 +6072,17 @@ multT PosInf (Ok _) = PosInf -- Because many (TypeSpec fn t)'s contain (Specification fn s), for types 's' different from 't' sizeOfSpec :: forall fn t. - (BaseUniverse fn, Sized t, HasSpec fn t) => Specification fn t -> Specification fn Integer + (BaseUniverse fn, Sized fn t, HasSpec fn t) => Specification fn t -> Specification fn Integer sizeOfSpec (ExplainSpec _ s) = sizeOfSpec s sizeOfSpec TrueSpec = TrueSpec -sizeOfSpec s@(MemberSpec xs) = nubOrdMemberSpec ("call to (sizeOfSpec " ++ show s ++ ")") (map sizeOf (NE.toList xs)) +sizeOfSpec s@(MemberSpec xs) = nubOrdMemberSpec ("call to (sizeOfSpec " ++ show s ++ ")") (map (sizeOf @fn) (NE.toList xs)) sizeOfSpec (ErrorSpec xs) = ErrorSpec xs sizeOfSpec (SuspendedSpec x p) = constrained $ \len -> Exists (\_ -> fatalError1 "sizeOfSpec: Exists") (x :-> (Explain (pure "sizeOfSpec") $ Assert (len ==. sizeOf_ (V x)) <> p)) -sizeOfSpec (TypeSpec x _) = sizeOfTypeSpec @t @fn x +sizeOfSpec (TypeSpec x _) = sizeOfTypeSpec @fn @t x -- | Turn a Size spec into an ErrorSpec if it has negative numbers. checkForNegativeSize :: Specification fn Integer -> Specification fn Integer diff --git a/libs/constrained-generators/src/Constrained/Spec/Generics.hs b/libs/constrained-generators/src/Constrained/Spec/Generics.hs index 07c69bd55ca..b38b14a646d 100644 --- a/libs/constrained-generators/src/Constrained/Spec/Generics.hs +++ b/libs/constrained-generators/src/Constrained/Spec/Generics.hs @@ -389,7 +389,9 @@ cNothing_ = con @"Nothing" (lit ()) sel :: forall n fn a c as. ( SimpleRep a ~ ProdOver as - , TheSop a ~ '[c ::: as] + , -- TODO: possibly investigate deriving this from the actual SOP of SimpleRep, as currently it's buggy if you define + -- your own custom SOP-like SimpleRep by defining SimpleRep rather than TheSop (it's stupid I know) + TheSop a ~ '[c ::: as] , TypeSpec fn a ~ TypeSpec fn (ProdOver as) , Select fn n as , HasSpec fn a diff --git a/libs/constrained-generators/src/Constrained/Spec/Map.hs b/libs/constrained-generators/src/Constrained/Spec/Map.hs index 0e91ecc1453..69818bee51d 100644 --- a/libs/constrained-generators/src/Constrained/Spec/Map.hs +++ b/libs/constrained-generators/src/Constrained/Spec/Map.hs @@ -48,7 +48,7 @@ import Test.QuickCheck (Arbitrary (..), frequency, genericShrink, shrinkList) -- HasSpec ------------------------------------------------------------------------ -instance Ord a => Sized (Map.Map a b) where +instance Ord a => Sized fn (Map.Map a b) where sizeOf = toInteger . Map.size liftSizeSpec sz cant = typeSpec $ defaultMapSpec {mapSpecSize = TypeSpec sz cant} liftMemberSpec xs = case NE.nonEmpty (nubOrd xs) of