packages feed

quickcheck-dynamic 3.3.1 → 3.4.0

raw patch · 10 files changed

+218/−61 lines, 10 files

Files

CHANGELOG.md view
@@ -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
quickcheck-dynamic.cabal view
@@ -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:
src/Test/QuickCheck/DynamicLogic/Internal.hs view
@@ -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
src/Test/QuickCheck/DynamicLogic/Quantify.hs view
@@ -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
src/Test/QuickCheck/StateModel.hs view
@@ -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
src/Test/QuickCheck/StateModel/Variables.hs view
@@ -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
test/Spec.hs view
@@ -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     ]
+ test/Spec/DynamicLogic/CounterModel.hs view
@@ -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+    ]
test/Spec/DynamicLogic/RegistryModel.hs view
@@ -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
+ test/Test/QuickCheck/DynamicLogic/QuantifySpec.hs view
@@ -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]