Smart shrinking for state machine tests

plutus-contract/src/Plutus/Contract/Test/ContractModel.hs

@@ -1,3 +1,15 @@
+-- | This module provides a framework for testing Plutus contracts built on "Test.QuickCheck". The
+--   testing is model based, so to test a contract you define a type modelling the state of the
+--   contract (or set of contracts) and provide an instance of the `ContractModel` class. This
+--   instance specifies what operations (`Action`s) the contract supports, how they interact with
+--   the model state, and how to execute them in the blockchain emulator ("Plutus.Trace.Emulator").
+--   Tests are evaluated by running sequences of actions (random or user-specified) in the emulator
+--   and comparing the state of the blockchain to the model state at the end.
+--
+--   Test cases are written in the `DL` monad, which supports mixing fixed sequences of actions with
+--   random actions, making it easy to write properties like
+--   /it is always possible to get all funds out of the contract/.
+
 {-# LANGUAGE PatternSynonyms #-}
 module Plutus.Contract.Test.ContractModel
     ( -- * Contract models

plutus-contract/src/Plutus/Contract/Test/ContractModel/Internal.hs

@@ -202,8 +202,8 @@ import PlutusTx.Coverage
 import PlutusTx.ErrorCodes
 import Streaming qualified as S
 import Test.QuickCheck.DynamicLogic.Monad qualified as DL
-import Test.QuickCheck.StateModel hiding (Action, Actions, ActionsWithShrinkState, arbitraryAction, initialState,
-                                   monitoring, nextState, perform, precondition, shrinkAction, stateAfter)
+import Test.QuickCheck.StateModel hiding (Action, Actions (..), arbitraryAction, initialState, monitoring, nextState,
+                                   pattern Actions, perform, precondition, shrinkAction, stateAfter)
 import Test.QuickCheck.StateModel qualified as StateModel
 
 import Test.QuickCheck hiding (ShrinkState, checkCoverage, (.&&.), (.||.))
@@ -837,12 +837,12 @@ instance ContractModel state => StateModel (ModelState state) where
 -- Now the failing test can be rerun to check if changes code or model has fixed the problem.
 
 -- | A `Actions` is a list of `Action`s.
-data Actions s = ActionsWithShrinkState ShrinkState [Act s]
+newtype Actions s = Actions_ (Smart [Act s])
 
 {-# COMPLETE Actions #-}
 pattern Actions :: [Act s] -> Actions s
-pattern Actions as <- ActionsWithShrinkState _ as where
-  Actions as = ActionsWithShrinkState initialShrinkState as
+pattern Actions as <- Actions_ (Smart _ as) where
+  Actions as = Actions_ (Smart 0 as)
 
 data Act s = Bind (Var AssetKey) (Action s)
            | NoBind (Var AssetKey) (Action s)
@@ -882,12 +882,12 @@ instance ContractModel s => Arbitrary (Actions s) where
 
 toStateModelActions :: ContractModel state =>
                         Actions state -> StateModel.Actions (ModelState state)
-toStateModelActions (ActionsWithShrinkState ss s) =
-  StateModel.ActionsWithShrinkState ss [ varOf act := ContractAction (isBind act) (actionOf act) | act <- s ]
+toStateModelActions (Actions_ (Smart k s)) =
+  StateModel.Actions_ (Smart k [ varOf act := ContractAction (isBind act) (actionOf act) | act <- s ])
 
 fromStateModelActions :: StateModel.Actions (ModelState s) -> Actions s
-fromStateModelActions (StateModel.ActionsWithShrinkState ss s) =
-  ActionsWithShrinkState ss [if b then Bind (Var i) act else NoBind (Var i) act | Var i := ContractAction b act <- s]
+fromStateModelActions (StateModel.Actions_ (Smart k s)) =
+  Actions_ (Smart k [if b then Bind (Var i) act else NoBind (Var i) act | Var i := ContractAction b act <- s])
 
 -- | An instance of a `DL` scenario generated by `forAllDL`. It is turned into a `Actions` before
 --   being passed to the property argument of `forAllDL`, but in case of a failure the generated

plutus-use-cases/test/Spec/Auction.hs

@@ -199,8 +199,8 @@ instance ContractModel AuctionModel where
 
     arbitraryAction s
         | p /= NotStarted =
-            oneof [ WaitUntil . step <$> choose (1, 10 :: Integer)
-                  , Bid  <$> elements [w2, w3, w4] <*> choose (Ada.getLovelace Ledger.minAdaTxOut, 100_000_000) ]
+            frequency [ (1, WaitUntil . step <$> choose (1, 10 :: Integer))
+                      , (10, Bid  <$> elements [w2, w3, w4] <*> choose (Ada.getLovelace Ledger.minAdaTxOut, 100_000_000)) ]
         | otherwise = pure Init
         where
             p    = s ^. contractState . phase
@@ -247,6 +247,7 @@ instance ContractModel AuctionModel where
                     deposit leader $ Ada.lovelaceValueOf current
                     currentBid .= bid
                     winner     .= w
+                wait 2
 
     perform _ _ _ Init = delay 3
     perform _ _ _ (WaitUntil slot) = void $ Trace.waitUntilSlot slot

quickcheck-dynamic/quickcheck-dynamic.cabal

@@ -36,6 +36,7 @@ library
         Test.QuickCheck.DynamicLogic.CanGenerate
         Test.QuickCheck.DynamicLogic.Monad
         Test.QuickCheck.DynamicLogic.Quantify
+        Test.QuickCheck.DynamicLogic.SmartShrinking
         Test.QuickCheck.StateModel
     build-depends:
         QuickCheck -any,

quickcheck-dynamic/src/Test/QuickCheck/DynamicLogic.hs

@@ -26,6 +26,7 @@ import Test.QuickCheck hiding (generate)
 
 import Test.QuickCheck.DynamicLogic.CanGenerate
 import Test.QuickCheck.DynamicLogic.Quantify
+import Test.QuickCheck.DynamicLogic.SmartShrinking
 import Test.QuickCheck.StateModel
 
 -- | Dynamic logic formulae.
@@ -150,9 +151,7 @@ forAllUniqueScripts n s d k = case generate chooseUniqueNextStep d n s 500 [] of
 
 forAllScripts :: (DynLogicModel s, Testable a) =>
                    DynLogic s -> (Actions s -> a) -> Property
-forAllScripts d k =
-    forAllShrink (sized $ generateDLTest d) (shrinkDLTest d) $
-        withDLScript d k
+forAllScripts d k = forAllMappedScripts id id d k
 
 forAllScripts_ :: (DynLogicModel s, Testable a) =>
                    DynLogic s -> (Actions s -> a) -> Property
@@ -164,8 +163,9 @@ forAllMappedScripts ::
   (DynLogicModel s, Testable a, Show rep) =>
     (rep -> DynLogicTest s) -> (DynLogicTest s -> rep) -> DynLogic s -> (Actions s -> a) -> Property
 forAllMappedScripts to from d k =
-    forAllShrink (sized $ (from<$>) . generateDLTest d) ((from<$>) . shrinkDLTest d . to) $
-        withDLScript d k . to
+    forAllShrink (Smart 0 <$> (sized $ (from<$>) . generateDLTest d))
+                 (shrinkSmart ((from<$>) . shrinkDLTest d . to)) $ \(Smart _ script) ->
+        withDLScript d k (to script)
 
 forAllMappedScripts_ ::
   (DynLogicModel s, Testable a, Show rep) =>

quickcheck-dynamic/src/Test/QuickCheck/DynamicLogic/SmartShrinking.hs

@@ -0,0 +1,15 @@
+module Test.QuickCheck.DynamicLogic.SmartShrinking( shrinkSmart ) where
+
+import Test.QuickCheck
+
+-- This combinator captures the 'smart shrinking' implemented for the
+-- Smart type wrapper in Test.QuickCheck.Modifiers.
+
+shrinkSmart :: (a->[a]) -> Smart a -> [Smart a]
+shrinkSmart shr (Smart i x) = take i' ys `ilv` drop i' ys
+  where
+    ys = [Smart j y | (j,y) <- [0..] `zip` shr x ]
+    i' = 0 `max`  (i-2)
+    []     `ilv` bs     = bs
+    as     `ilv` []     = as
+    (a:as) `ilv` (b:bs) = a : b : (as `ilv` bs)

quickcheck-dynamic/src/Test/QuickCheck/StateModel.hs

@@ -20,8 +20,6 @@ module Test.QuickCheck.StateModel(
   , LookUp, Var(..) -- we export the constructors so that users can construct test cases
   , Actions(..)
   , pattern Actions
-  , ShrinkState
-  , initialShrinkState
   , EnvEntry(..)
   , Env
   , stateAfter
@@ -32,7 +30,8 @@ module Test.QuickCheck.StateModel(
 
 import Data.Typeable
 
-import Test.QuickCheck as QC hiding (ShrinkState)
+import Test.QuickCheck as QC
+import Test.QuickCheck.DynamicLogic.SmartShrinking
 import Test.QuickCheck.Monadic
 
 class (forall a. Show (Action state a),
@@ -106,18 +105,20 @@ instance Eq (Step state) where
   (Var i := act) == (Var j := act') =
     (i==j) && Some act == Some act'
 
-data Actions state = ActionsWithShrinkState ShrinkState [Step state]
-  deriving Eq
+-- Action sequences use Smart shrinking, but this is invisible to
+-- client code because the extra Smart constructor is concealed by a
+-- pattern synonym.
 
-data ShrinkState = ShrinkState { lastShrinkIndex :: Int } deriving Eq
+newtype Actions state = Actions_ (Smart [Step state])
 
-initialShrinkState :: ShrinkState
-initialShrinkState = ShrinkState 0
+pattern Actions :: [Step state] -> Actions state
+pattern Actions as <- Actions_ (Smart _ as) where
+  Actions as = Actions_ (Smart 0 as)
 
 {-# COMPLETE Actions #-}
-pattern Actions :: [Step state] -> Actions state
-pattern Actions as <- ActionsWithShrinkState _ as where
-  Actions as = ActionsWithShrinkState initialShrinkState as
+
+instance Eq (Actions state) where
+  Actions as == Actions as' = as == as'
 
 instance (forall a. Show (Action state a)) => Show (Actions state) where
   showsPrec d (Actions as)
@@ -146,11 +147,9 @@ instance (Typeable state, StateModel state) => Arbitrary (Actions state) where
                               Nothing ->
                                 return [])]
 
-  shrink (ActionsWithShrinkState s as) =
-    rotate (lastShrinkIndex s) $ zipWith mkActions [0..] (map fst <$> shrinkList shrinker (withStates as))
+  shrink (Actions_ as) =
+    map Actions_ (shrinkSmart (map (prune . map fst) . shrinkList shrinker . withStates) as)
     where shrinker ((Var i := act),s) = [((Var i := act'),s) | Some act' <- shrinkAction s act]
-          mkActions i as = ActionsWithShrinkState (ShrinkState i) (prune as)
-          rotate i as = let (hds, tls) = splitAt (max 0 (i-1)) as in tls ++ hds
 
 prune :: StateModel state => [Step state] -> [Step state]
 prune = loop initialState