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 343a5c3ee17..13df2cd58e6 100644 --- a/eras/conway/impl/testlib/Test/Cardano/Ledger/Conway/Arbitrary.hs +++ b/eras/conway/impl/testlib/Test/Cardano/Ledger/Conway/Arbitrary.hs @@ -347,10 +347,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-test/cardano-ledger-test.cabal b/libs/cardano-ledger-test/cardano-ledger-test.cabal index 5f2a1fec5dd..5065b06cb7e 100644 --- a/libs/cardano-ledger-test/cardano-ledger-test.cabal +++ b/libs/cardano-ledger-test/cardano-ledger-test.cabal @@ -168,7 +168,8 @@ library vector, constrained-generators, random, - FailT + FailT, + lens test-suite cardano-ledger-test type: exitcode-stdio-1.0 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 fe7befad3a6..e91a6028ac0 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,12 +14,17 @@ module Test.Cardano.Ledger.Constrained.Conway.Epoch where import Cardano.Ledger.BaseTypes import Cardano.Ledger.Coin import Cardano.Ledger.Conway (Conway, ConwayEra) +import Cardano.Ledger.Conway.Governance import Cardano.Ledger.Core import Cardano.Ledger.Crypto (StandardCrypto) import Cardano.Ledger.Shelley.API.Types import Constrained -import Data.Map.Strict +import Control.Lens +import Data.Foldable +import Data.Map.Strict (Map) import GHC.Generics (Generic) +import Test.Cardano.Ledger.Constrained.Conway.Gov +import Test.Cardano.Ledger.Constrained.Conway.Instances newtype EpochExecEnv era = EpochExecEnv { eeeStakeDistr :: Map (Credential 'Staking (EraCrypto era)) (CompactForm Coin) @@ -26,8 +34,77 @@ newtype EpochExecEnv era = EpochExecEnv epochEnvSpec :: Specification fn (EpochExecEnv Conway) epochEnvSpec = TrueSpec -epochStateSpec :: Specification fn (EpochState (ConwayEra StandardCrypto)) -epochStateSpec = TrueSpec +epochStateSpec :: + Term ConwayFn EpochNo -> + Specification ConwayFn (EpochState (ConwayEra StandardCrypto)) +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 StandardCrypto) -> + Term ConwayFn (Proposals Conway) -> + 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 (EraCrypto era) -> 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 b7b79c74c18..70967825601 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 @@ -48,13 +48,13 @@ govProposalsSpec :: GovEnv (ConwayEra StandardCrypto) -> Specification fn (Proposals (ConwayEra StandardCrypto)) 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 StandardCrypto)) -> - CertState Conway -> + Term fn (CertState Conway) -> Specification fn (Proposals Conway) proposalsSpec geEpoch gePPolicy geCertState = constrained $ \ [var|props|] -> @@ -156,11 +156,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 ] ) @@ -174,7 +177,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) => @@ -280,6 +282,7 @@ withPrevActId gas k = -- InfoAction (branch $ \_ -> True) ] + onHardFork :: (IsConwayUniv fn, IsPred p fn) => Term fn (GovActionState (ConwayEra StandardCrypto)) -> 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 bcc71927cce..d89be7783f5 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 @@ -19,6 +19,7 @@ {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE TypeOperators #-} {-# LANGUAGE UndecidableInstances #-} +{-# LANGUAGE ViewPatterns #-} {-# OPTIONS_GHC -Wno-orphans #-} {-# OPTIONS_GHC -Wno-redundant-constraints #-} @@ -54,6 +55,7 @@ module Test.Cardano.Ledger.Constrained.Conway.Instances.Ledger ( gasCommitteeVotes_, gasDRepVotes_, gasProposalProcedure_, + psPParamUpdate_, ProposalsSplit (..), genProposalsSplit, proposalSplitSum, @@ -134,7 +136,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 @@ -170,6 +172,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) @@ -221,7 +224,7 @@ type ConwayTxBodyTypes c = instance (EraSpecPParams (ConwayEra c), IsConwayUniv fn, Crypto c) => HasSpec fn (ConwayTxBody (ConwayEra c)) instance Crypto c => HasSimpleRep (ConwayTxBody (ConwayEra c)) where - type SimpleRep (ConwayTxBody (ConwayEra c)) = SOP '["ConwayTxBody" ::: ConwayTxBodyTypes c] + type TheSop (ConwayTxBody (ConwayEra c)) = '["ConwayTxBody" ::: ConwayTxBodyTypes c] toSimpleRep ConwayTxBody {..} = inject @"ConwayTxBody" @'["ConwayTxBody" ::: ConwayTxBodyTypes c] ctbSpendInputs @@ -296,12 +299,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) @@ -323,7 +329,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] @@ -340,7 +345,6 @@ type AlonzoTxOutTypes era = , StrictMaybe (DataHash (EraCrypto era)) ] 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] @@ -978,13 +982,13 @@ type UMapTypes c = , Map (Credential 'Staking c) (DRep c) ] instance Crypto c => HasSimpleRep (UMap c) where - type SimpleRep (UMap c) = SOP '["UMap" ::: UMapTypes c] + type TheSop (UMap c) = '["UMap" ::: UMapTypes c] toSimpleRep um = inject @"UMap" @'["UMap" ::: UMapTypes c] (rdPairMap um) (ptrMap um) (sPoolMap um) (dRepMap um) fromSimpleRep rep = algebra @'["UMap" ::: UMapTypes c] rep unify instance (IsConwayUniv fn, Crypto c) => HasSpec fn (UMap c) 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" @@ -1076,7 +1080,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) @@ -1120,7 +1124,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 @@ -1347,8 +1357,8 @@ instance (DRepPulser Conway Identity (RatifyState Conway)) where type - SimpleRep (DRepPulser Conway Identity (RatifyState Conway)) = - SOP '["DRepPulser" ::: DRepPulserTypes] + TheSop (DRepPulser Conway Identity (RatifyState Conway)) = + '["DRepPulser" ::: DRepPulserTypes] toSimpleRep DRepPulser {..} = inject @"DRepPulser" @'["DRepPulser" ::: DRepPulserTypes] dpPulseSize @@ -1412,7 +1422,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 @@ -1436,8 +1446,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 @@ -1460,8 +1470,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 @@ -1483,8 +1493,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 @@ -1512,8 +1522,8 @@ type AlonzoTxWitsTypes c = ] instance AlonzoEraScript era => HasSimpleRep (AlonzoTxWits era) where type - SimpleRep (AlonzoTxWits era) = - SOP '["AlonzoTxWits" ::: AlonzoTxWitsTypes (EraCrypto era)] + TheSop (AlonzoTxWits era) = + '["AlonzoTxWits" ::: AlonzoTxWitsTypes (EraCrypto era)] toSimpleRep (AlonzoTxWits vkeyWits bootstrapWits _ _ _) = inject @"AlonzoTxWits" @'["AlonzoTxWits" ::: AlonzoTxWitsTypes (EraCrypto era)] vkeyWits @@ -1529,8 +1539,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 @@ -1648,7 +1658,7 @@ type PulserTypes c = , RewardAns c ] instance HasSimpleRep (Pulser c) where - type SimpleRep (Pulser c) = SOP '["Pulser" ::: PulserTypes c] + type TheSop (Pulser c) = '["Pulser" ::: PulserTypes c] toSimpleRep (RSLP n free bal ans) = inject @"Pulser" @'["Pulser" ::: PulserTypes c] 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 f2f64885577..30ac164ee16 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 1bd816670fd..698b61641c1 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 @@ -125,7 +125,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 4620535269d..13fa224b764 100644 --- a/libs/cardano-ledger-test/src/Test/Cardano/Ledger/STS.hs +++ b/libs/cardano-ledger-test/src/Test/Cardano/Ledger/STS.hs @@ -23,6 +23,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 @@ -68,6 +69,33 @@ 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 era env st sig fail p. + ( era ~ ConwayEra StandardCrypto + , Environment (EraRule r era) ~ env + , State (EraRule r era) ~ st + , Signal (EraRule r era) ~ sig + , PredicateFailure (EraRule r era) ~ fail + , STS (EraRule r era) + , BaseM (EraRule r era) ~ 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) -> + (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 -> @@ -85,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 --------------------------------------------------------- @@ -106,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 @@ -267,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