diff --git a/CHANGELOG.md b/CHANGELOG.md --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -7,9 +7,13 @@ As a minor extension, we also keep a semantic version for the `UNRELEASED` changes. -## UNRELEASED +## 3.4.0 - 2024-03-01 * Added some lightweight negative-shrinking based on a simple dependency analysis. +* Added the option to return errors from actions by defining `type Error state`. + When this is defined `perform` has return type `m (Either (Error state) (Realized m a))`, + when it is left as the default the type remains `m (Realized m a)`. +* Changed `withGenQ` to _require_ a predicate when defining a `Quantification`. **Note**: This is technically a breaking change as the interface changed ## 3.3.1 diff --git a/quickcheck-dynamic.cabal b/quickcheck-dynamic.cabal --- a/quickcheck-dynamic.cabal +++ b/quickcheck-dynamic.cabal @@ -1,6 +1,6 @@ cabal-version: 2.2 name: quickcheck-dynamic -version: 3.3.1 +version: 3.4.0 license: Apache-2.0 license-files: LICENSE @@ -46,6 +46,7 @@ ImportQualifiedPost LambdaCase MultiParamTypeClasses + MultiWayIf PatternSynonyms QuantifiedConstraints RankNTypes @@ -89,8 +90,10 @@ main-is: Spec.hs hs-source-dirs: test other-modules: + Spec.DynamicLogic.CounterModel Spec.DynamicLogic.Registry Spec.DynamicLogic.RegistryModel + Test.QuickCheck.DynamicLogic.QuantifySpec ghc-options: -rtsopts build-depends: diff --git a/src/Test/QuickCheck/DynamicLogic/Internal.hs b/src/Test/QuickCheck/DynamicLogic/Internal.hs --- a/src/Test/QuickCheck/DynamicLogic/Internal.hs +++ b/src/Test/QuickCheck/DynamicLogic/Internal.hs @@ -162,7 +162,7 @@ instance StateModel s => Eq (FailingAction s) where ErrorFail s == ErrorFail s' = s == s' - ActionFail (a :: ActionWithPolarity s a) == ActionFail (a' :: ActionWithPolarity s a') + ActionFail (a :: ActionWithPolarity s a) == ActionFail (a' :: ActionWithPolarity s' a') | Just Refl <- eqT @a @a' = a == a' _ == _ = False diff --git a/src/Test/QuickCheck/DynamicLogic/Quantify.hs b/src/Test/QuickCheck/DynamicLogic/Quantify.hs --- a/src/Test/QuickCheck/DynamicLogic/Quantify.hs +++ b/src/Test/QuickCheck/DynamicLogic/Quantify.hs @@ -32,10 +32,22 @@ import Test.QuickCheck.DynamicLogic.CanGenerate import Test.QuickCheck.StateModel --- | A `Quantification` over a type @a@ is a generator that can be used with --- `Plutus.Contract.Test.ContractModel.forAllQ` to generate random values in --- DL scenarios. In addition to a QuickCheck generator a `Quantification` contains a shrinking --- strategy that ensures that shrunk values stay in the range of the generator. +-- | A `Quantification` over a type @a@ is a generator that can be used to generate random values in +-- DL scenarios. +-- +-- A `Quantification` is similar to a `Test.QuickCheck.Arbitrary`, it groups together: +-- +-- * A standard QuickCheck _generator_ in the `Gen` monad, which can be "empty", +-- * A _shrinking_ strategy for generated values in the case of a +-- failures ensuring they stay within the domain, +-- * A _predicate_ allowing finer grained control on generation +-- and shrinking process, e.g in the case the range of the generator +-- depends on trace context. +-- +-- NOTE: Leaving the possibility of generating `Nothing` is useful to simplify the generation +-- process for `elements` or `frequency` which may normally crash when the list to select +-- elements from is empty. This makes writing `DL` formulas cleaner, removing the need to +-- handle non-existence cases explicitly. data Quantification a = Quantification { genQ :: Maybe (Gen a) , isaQ :: a -> Bool @@ -51,10 +63,11 @@ shrinkQ :: Quantification a -> a -> [a] shrinkQ q a = filter (isaQ q) (shrQ q a) --- | Wrap a `Gen a` generator in a `Quantification a`. --- Uses given shrinker. -withGenQ :: Gen a -> (a -> [a]) -> Quantification a -withGenQ gen = Quantification (Just gen) (const True) +-- | Construct a `Quantification a` from its constituents. +-- Note the predicate provided is used to restrict both the range of values +-- generated and the list of possible shrinked values. +withGenQ :: Gen a -> (a -> Bool) -> (a -> [a]) -> Quantification a +withGenQ gen isA = Quantification (Just $ gen `suchThat` isA) isA -- | Pack up an `Arbitrary` instance as a `Quantification`. Treats all values as being in range. arbitraryQ :: Arbitrary a => Quantification a @@ -228,6 +241,8 @@ from (x : xs) = (x, xs) from [] = error "quantify: impossible" +-- | Turns a `Quantification` into a `Property` to enable QuickChecking its +-- validity. validQuantification :: Show a => Quantification a -> Property validQuantification q = forAllShrink (fromJust $ genQ q) (shrinkQ q) $ isaQ q diff --git a/src/Test/QuickCheck/StateModel.hs b/src/Test/QuickCheck/StateModel.hs --- a/src/Test/QuickCheck/StateModel.hs +++ b/src/Test/QuickCheck/StateModel.hs @@ -36,7 +36,6 @@ computePrecondition, computeArbitraryAction, computeShrinkAction, - failureResult, ) where import Control.Monad @@ -47,14 +46,14 @@ import Data.Data import Data.Kind import Data.List +import Data.Monoid (Endo (..)) import Data.Set qualified as Set +import Data.Void import GHC.Generics -import GHC.Stack import Test.QuickCheck as QC import Test.QuickCheck.DynamicLogic.SmartShrinking import Test.QuickCheck.Monadic import Test.QuickCheck.StateModel.Variables -import Data.Monoid (Endo (..)) -- | The typeclass users implement to define a model against which to validate some implementation. -- @@ -97,7 +96,7 @@ -- @ -- data Action RegState a where -- Spawn :: Action RegState ThreadId - -- Register :: String -> Var ThreadId -> Action RegState (Either ErrorCall ()) + -- Register :: String -> Var ThreadId -> Action RegState () -- KillThread :: Var ThreadId -> Action RegState () -- @ -- @@ -105,6 +104,13 @@ -- anything. data Action state a + -- | The type of errors that actions can throw. If this is defined as anything + -- other than `Void` `perform` is required to return `Either (Error state) a` + -- instead of `a`. + type Error state + + type Error state = Void + -- | Display name for `Action`. -- This is useful to provide sensible statistics about the distribution of `Action`s run -- when checking a property. @@ -154,6 +160,22 @@ deriving instance (forall a. Show (Action state a)) => Show (Any (Action state)) +-- | The result required of `perform` depending on the `Error` type +-- of a state model. If there are no errors, `Error state = Void`, and +-- so we don't need to specify if the action failed or not. +type family PerformResult e a where + PerformResult Void a = a + PerformResult e a = Either e a + +class IsPerformResult e a where + performResultToEither :: PerformResult e a -> Either e a + +instance {-# OVERLAPPING #-} IsPerformResult Void a where + performResultToEither = Right + +instance {-# OVERLAPPABLE #-} (PerformResult e a ~ Either e a) => IsPerformResult e a where + performResultToEither = id + -- TODO: maybe it makes sense to write -- out a long list of these instances type family Realized (m :: Type -> Type) a :: Type @@ -166,6 +188,9 @@ newtype PostconditionM m a = PostconditionM {runPost :: WriterT (Endo Property, Endo Property) m a} deriving (Functor, Applicative, Monad) +instance MonadTrans PostconditionM where + lift = PostconditionM . lift + -- | Apply the property transformation to the property after evaluating -- the postcondition. Useful for collecting statistics while avoiding -- duplication between `monitoring` and `postcondition`. @@ -176,7 +201,7 @@ counterexamplePost :: Monad m => String -> PostconditionM m () counterexamplePost c = PostconditionM $ tell (mempty, Endo $ counterexample c) -class Monad m => RunModel state m where +class (forall a. Show (Action state a), Monad m) => RunModel state m where -- | Perform an `Action` in some `state` in the `Monad` `m`. This -- is the function that's used to exercise the actual stateful -- implementation, usually through various side-effects as permitted @@ -187,40 +212,47 @@ -- -- The `Lookup` parameter provides an /environment/ to lookup `Var -- a` instances from previous steps. - perform :: forall a. Typeable a => state -> Action state a -> LookUp m -> m (Realized m a) + perform :: Typeable a => state -> Action state a -> LookUp m -> m (PerformResult (Error state) (Realized m a)) -- | Postcondition on the `a` value produced at some step. -- The result is `assert`ed and will make the property fail should it be `False`. This is useful -- to check the implementation produces expected values. - postcondition :: forall a. (state, state) -> Action state a -> LookUp m -> Realized m a -> PostconditionM m Bool + postcondition :: (state, state) -> Action state a -> LookUp m -> Realized m a -> PostconditionM m Bool postcondition _ _ _ _ = pure True -- | Postcondition on the result of running a _negative_ `Action`. -- The result is `assert`ed and will make the property fail should it be `False`. This is useful -- to check the implementation produces e.g. the expected errors or to check that the SUT hasn't -- been updated during the execution of the negative action. - postconditionOnFailure :: forall a. (state, state) -> Action state a -> LookUp m -> Realized m a -> PostconditionM m Bool + postconditionOnFailure :: (state, state) -> Action state a -> LookUp m -> Either (Error state) (Realized m a) -> PostconditionM m Bool postconditionOnFailure _ _ _ _ = pure True -- | Allows the user to attach additional information to the `Property` at each step of the process. -- This function is given the full transition that's been executed, including the start and ending -- `state`, the `Action`, the current environment to `Lookup` and the value produced by `perform` -- while executing this step. - monitoring :: forall a. (state, state) -> Action state a -> LookUp m -> Realized m a -> Property -> Property + monitoring :: (state, state) -> Action state a -> LookUp m -> Either (Error state) (Realized m a) -> Property -> Property monitoring _ _ _ _ prop = prop --- | Indicate that the result of an action (in `perform`) --- should not be inspected by the postcondition or appear --- in a positive test. Useful when we want to give a type --- for an `Action` like `SomeAct :: Action SomeState SomeType` --- instead of `SomeAct :: Action SomeState (Either SomeError SomeType)` --- but still need to return something in `perform` in the failure case. -failureResult :: HasCallStack => a -failureResult = error "A result of a failing action has been erronesouly inspected" + -- | Allows the user to attach additional information to the `Property` if a positive action fails. + monitoringFailure :: state -> Action state a -> LookUp m -> Error state -> Property -> Property + monitoringFailure _ _ _ _ prop = prop -computePostcondition :: forall m state a. RunModel state m => (state, state) -> ActionWithPolarity state a -> LookUp m -> Realized m a -> PostconditionM m Bool +computePostcondition + :: forall m state a + . RunModel state m + => (state, state) + -> ActionWithPolarity state a + -> LookUp m + -> Either (Error state) (Realized m a) + -> PostconditionM m Bool computePostcondition ss (ActionWithPolarity a p) l r - | p == PosPolarity = postcondition ss a l r + | p == PosPolarity = case r of + Right ra -> postcondition ss a l ra + -- NOTE: this is actually redundant as this handled + -- at the call site for this function, but this is + -- good hygiene? + Left _ -> pure False | otherwise = postconditionOnFailure ss a l r type LookUp m = forall a. Typeable a => Var a -> Realized m a @@ -249,7 +281,7 @@ lookUpVar :: Typeable a => Env m -> Var a -> Realized m a lookUpVar env v = case lookUpVarMaybe env v of - Nothing -> error $ "Variable " ++ show v ++ " is not bound!" + Nothing -> error $ "Variable " ++ show v ++ " is not bound at type " ++ show (typeRep v) ++ "!" Just a -> a data WithUsedVars a = WithUsedVars VarContext a @@ -474,8 +506,12 @@ loop s ((var := act) : as) = loop (computeNextState @state s act var) as runActions - :: forall state m - . (StateModel state, RunModel state m) + :: forall state m e + . ( StateModel state + , RunModel state m + , e ~ Error state + , forall a. IsPerformResult e a + ) => Actions state -> PropertyM m (Annotated state, Env m) runActions (Actions_ rejected (Smart _ actions)) = loop initialAnnotatedState [] actions @@ -488,24 +524,37 @@ return (_s, reverse env) loop s env ((v := act) : as) = do pre $ computePrecondition s act - ret <- run $ perform (underlyingState s) (polarAction act) (lookUpVar env) + ret <- run $ performResultToEither <$> perform (underlyingState s) (polarAction act) (lookUpVar env) let name = show (polarity act) ++ actionName (polarAction act) monitor $ tabulate "Actions" [name] - let var = unsafeCoerceVar v - s' = computeNextState s act var - env' = (var :== ret) : env monitor $ tabulate "Action polarity" [show $ polarity act] - monitor $ monitoring @state @m (underlyingState s, underlyingState s') (polarAction act) (lookUpVar env') ret - (b, (Endo mon, Endo onFail)) <- - run - . runWriterT - . runPost - $ computePostcondition @m - (underlyingState s, underlyingState s') - act - (lookUpVar env) - ret - monitor mon - unless b $ monitor onFail - assert b - loop s' env' as + if + | polarity act == PosPolarity + , Left err <- ret -> do + monitor $ + monitoringFailure @state @m + (underlyingState s) + (polarAction act) + (lookUpVar env) + err + stop False + | otherwise -> do + let var = unsafeCoerceVar v + s' = computeNextState s act var + env' + | Right val <- ret = (var :== val) : env + | otherwise = env + monitor $ monitoring @state @m (underlyingState s, underlyingState s') (polarAction act) (lookUpVar env') ret + (b, (Endo mon, Endo onFail)) <- + run + . runWriterT + . runPost + $ computePostcondition @m + (underlyingState s, underlyingState s') + act + (lookUpVar env) + ret + monitor mon + unless b $ monitor onFail + assert b + loop s' env' as diff --git a/src/Test/QuickCheck/StateModel/Variables.hs b/src/Test/QuickCheck/StateModel/Variables.hs --- a/src/Test/QuickCheck/StateModel/Variables.hs +++ b/src/Test/QuickCheck/StateModel/Variables.hs @@ -1,4 +1,5 @@ {-# LANGUAGE AllowAmbiguousTypes #-} +{-# LANGUAGE QuantifiedConstraints #-} {-# LANGUAGE UndecidableInstances #-} module Test.QuickCheck.StateModel.Variables ( @@ -14,6 +15,7 @@ extendContext, isWellTyped, allVariables, + isEmptyCtx, unsafeCoerceVar, unsafeNextVarIndex, ) where @@ -58,6 +60,9 @@ instance HasVariables a => HasVariables (Set a) where getAllVariables = getAllVariables . Set.toList +instance (forall a. HasVariables (f a)) => HasVariables (Any f) where + getAllVariables (Some a) = getAllVariables a + newtype HasNoVariables a = HasNoVariables a deriving via a instance Show a => Show (HasNoVariables a) @@ -101,8 +106,11 @@ -- The use of typeRep here is on purpose to avoid printing `Var` unnecessarily. showBinding (Some v) = show v ++ " :: " ++ show (typeRep v) +isEmptyCtx :: VarContext -> Bool +isEmptyCtx (VarCtx ctx) = null ctx + isWellTyped :: Typeable a => Var a -> VarContext -> Bool -isWellTyped v (VarCtx ctx) = Some v `Set.member` ctx +isWellTyped v (VarCtx ctx) = not (null ctx) && Some v `Set.member` ctx -- TODO: check the invariant that no variable index is used -- twice at different types. This is generally not an issue diff --git a/test/Spec.hs b/test/Spec.hs --- a/test/Spec.hs +++ b/test/Spec.hs @@ -2,7 +2,9 @@ module Main (main) where +import Spec.DynamicLogic.CounterModel qualified import Spec.DynamicLogic.RegistryModel qualified +import Test.QuickCheck.DynamicLogic.QuantifySpec qualified import Test.Tasty main :: IO () @@ -13,4 +15,6 @@ testGroup "dynamic logic" [ Spec.DynamicLogic.RegistryModel.tests + , Spec.DynamicLogic.CounterModel.tests + , Test.QuickCheck.DynamicLogic.QuantifySpec.tests ] diff --git a/test/Spec/DynamicLogic/CounterModel.hs b/test/Spec/DynamicLogic/CounterModel.hs new file mode 100644 --- /dev/null +++ b/test/Spec/DynamicLogic/CounterModel.hs @@ -0,0 +1,57 @@ +module Spec.DynamicLogic.CounterModel where + +import Control.Monad.Reader +import Data.IORef +import Test.QuickCheck +import Test.QuickCheck.Extras +import Test.QuickCheck.Monadic +import Test.QuickCheck.StateModel +import Test.Tasty hiding (after) +import Test.Tasty.QuickCheck + +data Counter = Counter Int + deriving (Show, Generic) + +deriving instance Show (Action Counter a) +deriving instance Eq (Action Counter a) +instance HasVariables (Action Counter a) where + getAllVariables _ = mempty + +instance StateModel Counter where + data Action Counter a where + Inc :: Action Counter () + Reset :: Action Counter Int + + initialState = Counter 0 + + arbitraryAction _ _ = frequency [(5, pure $ Some Inc), (1, pure $ Some Reset)] + + nextState (Counter n) Inc _ = Counter (n + 1) + nextState _ Reset _ = Counter 0 + +instance RunModel Counter (ReaderT (IORef Int) IO) where + perform _ Inc _ = do + ref <- ask + lift $ modifyIORef ref succ + perform _ Reset _ = do + ref <- ask + lift $ do + n <- readIORef ref + writeIORef ref 0 + pure n + + postcondition (Counter n, _) Reset _ res = pure $ n == res + postcondition _ _ _ _ = pure True + +prop_counter :: Actions Counter -> Property +prop_counter as = monadicIO $ do + ref <- lift $ newIORef (0 :: Int) + runPropertyReaderT (runActions as) ref + assert True + +tests :: TestTree +tests = + testGroup + "counter tests" + [ testProperty "prop_conter" $ prop_counter + ] diff --git a/test/Spec/DynamicLogic/RegistryModel.hs b/test/Spec/DynamicLogic/RegistryModel.hs --- a/test/Spec/DynamicLogic/RegistryModel.hs +++ b/test/Spec/DynamicLogic/RegistryModel.hs @@ -40,10 +40,12 @@ data Action RegState a where Spawn :: Action RegState ThreadId WhereIs :: String -> Action RegState (Maybe ThreadId) - Register :: String -> Var ThreadId -> Action RegState (Either SomeException ()) - Unregister :: String -> Action RegState (Either SomeException ()) + Register :: String -> Var ThreadId -> Action RegState () + Unregister :: String -> Action RegState () KillThread :: Var ThreadId -> Action RegState () + type Error RegState = SomeException + precondition s (Register name tid) = name `Map.notMember` regs s && tid `notElem` Map.elems (regs s) @@ -109,7 +111,8 @@ instance RunModel RegState RegM where perform _ Spawn _ = do - lift $ forkIO (threadDelay 10000000) + tid <- lift $ forkIO (threadDelay 10000000) + pure $ Right tid perform _ (Register name tid) env = do reg <- ask lift $ try $ register reg name (env tid) @@ -118,24 +121,22 @@ lift $ try $ unregister reg name perform _ (WhereIs name) _ = do reg <- ask - lift $ whereis reg name + res <- lift $ whereis reg name + pure $ Right res perform _ (KillThread tid) env = do lift $ killThread (env tid) lift $ threadDelay 100 + pure $ Right () postcondition (s, _) (WhereIs name) env mtid = do pure $ (env <$> Map.lookup name (regs s)) == mtid - postcondition _ Register{} _ res = do - pure $ isRight res postcondition _ _ _ _ = pure True postconditionOnFailure (s, _) act@Register{} _ res = do monitorPost $ tabulate "Reason for -Register" - [ why s act - | Left{} <- [res] - ] + [why s act] pure $ isLeft res postconditionOnFailure _s _ _ _ = pure True diff --git a/test/Test/QuickCheck/DynamicLogic/QuantifySpec.hs b/test/Test/QuickCheck/DynamicLogic/QuantifySpec.hs new file mode 100644 --- /dev/null +++ b/test/Test/QuickCheck/DynamicLogic/QuantifySpec.hs @@ -0,0 +1,16 @@ +module Test.QuickCheck.DynamicLogic.QuantifySpec where + +import Test.QuickCheck (Arbitrary (..), Gen, Property) +import Test.QuickCheck.DynamicLogic.Quantify (validQuantification, withGenQ) +import Test.Tasty (TestTree, testGroup) +import Test.Tasty.QuickCheck (testProperty) + +propWithGenQRestrictsValues :: Property +propWithGenQRestrictsValues = + validQuantification $ withGenQ (arbitrary :: Gen Int) ((< 10) . abs) (shrink @Int) + +tests :: TestTree +tests = + testGroup + "Quantification" + [testProperty "withGenQ restricts possible generated values" propWithGenQRestrictsValues]