Shrink with confidence: product types, QuickCheck and Plutarch

Introduction

QuickCheck is a tool that sees wide use at MLabs, and Plutarch is no exception to this. In our experience, QuickCheck can be a powerful helper to finding, diagnosing and ultimately fixing bugs. This stems from a powerful combination of both finding issues that we could never have thought of, as well as the ability to automatically minimize reproducing cases, a concept known as shrinking.

As part of our ongoing work to fully release Plutarch 2.0, we have to tackle the major task of adding support for all the V4 ledger types. Plutarch 1.0 contains our starting point: a key part of what ensures the correctness of this starting point is a large number of property tests to ensure that our definitions align precisely with those of plutarch-ledger-api. In particular, we have to ensure that the Data encodings are exactly the same between both of these. To allow us to write such tests, we have a large number of orphan Arbitrary instances in Plutarch 1.0. These instances, and the tests that are based on them, were invaluable to us during previous upgrades, including the most recent release of Plutarch 1.0 to add support for the V4 types and their new representations.

While Plutarch 1.0 gives us a good starting point, the differences between 1.0 and 2.0 are significant enough that we had to re-evaluate all of the instances we would be using. During this time, we discovered a subtle problem with shrinkers over product types that, while not breaking any shrinker invariants, would produce far worse shrinks than necessary, rendering them much less useful. While solving this problem is not difficult, the solutions available to us were far from satisfactory, forcing us to either give up precise control over invariants or requiring large amounts of rather tedious boilerplate. Given the complexity of the data types used by the ledger, both of these solutions were a bad fit for Plutarch.

Realizing that we would not only have to fix these problems for Plutarch 2.0's future release, but also fix them in the still-maintained Plutarch 1.0 codebase, we decided that the correct approach would be to solve this problem in a way that both gives us the manual control we need, while also being as easy to write for product types as arbitrary methods would be. To this end, we created quickcheck-helpers, which we already use in both Plutarch 1.0 and Plutarch 2.0 for all Arbitrary instances for ledger types. This library in no way depends on Plutarch, Plutus or Nix, being a pure Haskell library that only requires QuickCheck. Thanks to this, we have also released it on Hackage, so that the entire Haskell community might benefit from it.

In this post, we describe the problem that we found, the naive solutions to it that exist (and why we consider them unsatisfactory), and then describe the solution implemented in quickcheck-helpers. We then discuss the specific capabilities we chose to provide in quickcheck-helpers, as well as what we couldn't, or chose not to, provide. Lastly, we cover how quickcheck-helpers specifically fits into the use case for Plutarch 1.0 (and 2.0) specifically. This problem surprised us, and we wanted to share what we discovered, and our solution, to help other Haskellers not make the same mistake we did.

The problem with shrinkers on product types

Consider the following data type:

data Pair a = Pair a a
    deriving stock (Show, Eq)

If we want an Arbitrary instance for Pair, we can define the arbitrary method quickly and easily:

instance Arbitrary a => Arbitrary (Pair a) where
    arbitrary = Pair <$> arbitrary <*> arbitrary

We can do this because the Applicative syntax using <*> and <$> mirrors the data constructor call for Pair. This is clear, concise, and poses no issues.

We could thus be led to believe that we could do something similar for shrink:

instance Arbitrary a => Arbitrary (Pair a) where
    -- Perfectly fine
    arbitrary = Pair <$> arbitrary <*> arbitrary
    -- Not fine at all
    shrink (Pair x y) = Pair <$> shrink x <*> shrink y

So why is defining shrink using the same syntax such an issue? Consider x = Pair 0 6, y = Pair 6 0 and z = Pair 0 0. We expect that x and y should still shrink, but z should not. However, if we see what happens when we use shrink in GHCi, we get an unpleasant surprise:

ghci> shrink (Pair 0 6 :: Pair Int)
[]
ghci> shrink (Pair 6 0 :: Pair Int)
[]
ghci> shrink (Pair 0 0 :: Pair Int)
[]

This shows the root of the problem. To be clear, the cause here is not the Applicative-style definition. Even if we rewrite using do-notation (or anything else), the same problem persists:

instance Arbitrary a => Arbitrary (Pair a) where
    arbitrary = Pair <$> arbitrary <*> arbitrary
    -- Makes no difference
    shrink (Pair x y) = do
        x' <- shrink x
        y' <- shrink y
        pure . Pair x' $ y'

Needless to say, this is quite a surprising behaviour. While it doesn't violate any of the invariants a shrinker must obey, it will mean that shrinking stops much sooner than it should. Thus, especially on larger product types, we could end up with bigger 'minimal' cases than we need to, which complicates the debugging process that QuickCheck is meant to assist.

Why does this happen?

To see the reason behind this behaviour, let us look specifically at what happens when we shrink x = Pair 0 6:

shrink (Pair 0 6 :: Pair Int)
>>> definition 
do
    x' <- shrink 0
    y' <- shrink 6
    pure . Pair x' $ y'
>>> by definition, then ApplicativeDo
Pair <$> [] <*> [0, 3, 5]
>>> by <*> for lists
[]

This stems from []'s Applicative and Monad instances modelling non-determinism. Pair in this context acts as a 'combiner' of nondeterministic subcomputations, which we can see if we example the instance of Applicative for lists:

-- Not the actual implementation, but provided for clarity
instance Applicative [] where
    pure x = [x]
    fs <*> xs = case fs of 
        [] -> []
        (f : fs') -> fmap f xs <> (fs' <*> xs)

From this, we can see that if we have [] on either side of <*>, we end up with [] as the result:

[] <*> xs
>>> by definition of <*>
case [] of 
    [] -> []
    (f : fs') -> fmap f xs <> (fs' <*> xs)
>>> by pattern match
[]

(f : fs) <*> []
>>> by definition of <*>
case [] of 
    [] -> []
    (f : fs') -> fmap f xs <> (fs' <*> xs)
>>> by pattern match
fmap f [] <> (fs' <*> [])
>>> by definition of fmap
[] <> (fs' <*> [])
>>> fs' is now one item shorter, but the result doesn't change
>>> eventually we hit the case that fs' = [] and stop

In general, this is the only possible correct behaviour which maintains the laws of Applicative. Given no functions to apply, or no arguments to apply them to, the only validly-typed list we can produce is the empty one! However, in the specific context of shrinking product types, this produces the odd outcome that we fail to shrink if any field fails to shrink, whereas we actually want that to happen only when they all do.

How to solve this?

Avoiding this problem requires us to manually shrink each field in isolation:

instance Arbitrary a => Arbitrary (Pair a) where
    -- unchanged
    arbitrary = Pair <$> arbitrary <*> arbitrary
    -- fixed
    shrink (Pair x y) = 
        -- shrink y only
        (Pair <$> pure x <*> shrink y) <|>
        -- shrink x only
        (Pair <$> shrink x <*> pure y)

This now works as we expect:

ghci> shrink (Pair 0 6 :: Pair Int)
[Pair 0 0,Pair 0 3,Pair 0 5]
ghci> shrink (Pair 6 0 :: Pair Int)
[Pair 0 0,Pair 3 0,Pair 5 0]
ghci> shrink (Pair 0 0 :: Pair Int)
[]

However, this kind of solution is long, tedious and easy to mess up. If a given product type has n fields, the shrink method implementation for that product type must have n entries separated by <|>, with each entry consisting of n calls to pure or shrink. This is a quadratic amount of code relative the number of fields, and writing this by hand, especially for large records, is not viable in general.

"But why not use Generic?"

Those readers more familiar with QuickCheck might well ask this question at this point. Indeed, we can use functionality from QuickCheck itself to potentially 'fix' the issue we just described, while also not requiring a lot of boilerplate.

First, we need to give our type an instance of Generic:

data Pair a = Pair a a
    deriving stock (Generic)

We can then use genericShrink from QuickCheck to define a shrinker in a single line:

instance Arbitrary a => Arbitrary (Pair a) where
    arbitrary = Pair <$> arbitrary <*> arbitrary
    shrink = genericShrink

This indeed behaves as we would expect it to:

ghci> shrink (Pair 0 6 :: Pair Int)
[Pair 0 0,Pair 0 3,Pair 0 5]
ghci> shrink (Pair 6 0 :: Pair Int)
[Pair 0 0,Pair 3 0,Pair 5 0]
ghci> shrink (Pair 0 0 :: Pair Int)
[]

However, there are numerous problems with this solution:

• Determining what exactly Generic-based code does is difficult unless you spend a lot of time looking at the mechanisms or reading Core.
• Generic-based code is inefficient both at compile time and at runtime, especially if the instances requires are over types with many fields.
• genericShrink is completely unaware of any non-structural invariants, or any relationships between fields not expressed by their types.

The last of these requires some elaboration. Consider a type which combines a list with a cache of its length:

data CountedList a = CountedList Int [a]
    deriving stock (Eq, Show, Generic)

Any functionality we provide over CountedList must ensure the following invariants always hold:

• The Int field cannot be negative; and
• The Int field must correspond exactly to the length of the [a] field.

Both of these invariants are non-structural: nothing about the definition of CountedList, or the types Int and [], enforces them. This extends to Arbitrary as well: we must ensure that not only does arbitrary not produce terms which violate these invariants, but also that shrink doesn't produce shrunk terms that violate them either.

However, here, genericShrink works against us pretty badly. If we were to write the Arbitrary instance like this:

instance Arbitrary a => Arbitrary (CountedList a) where
    arbitrary = do
        len <- getNonNegative arbitrary
        CountedList len <$> vectorOf len arbitrary
    shrink = genericShrink

we can easily end up with completely nonsensical shrunk terms:

ghci> shrink (CountedList 2 [1, 3] :: CountedList Int)
[CountedList 0 [1,3],CountedList 1 [1,3],CountedList 2 [],CountedList 2 [3],CountedList 2 [1],CountedList 2 [0,3],CountedList 2 [1,0],CountedList 2 [1,2]]

This completely destroys any benefit of shrinking: we end up with a tonne of 'false positive' shrinks which potentially could cause test failures, despite the conditions that they represent being literally impossible. Thus, in cases like CountedList, we are forced to write our shrinkers by hand, even if only a small portion of our fields have invariants of this kind.

Our solution

Ideally, we would like a solution that gives us both of the following for product type shrinkers:

• Manual control over shrinking where needed, such as for non-structural invariants; and
• Brevity, ideally to the same level as arbitrary instances for the same product type.

To this end, we designed quickcheck-helpers. More specifically, we designed a wrapper type Shrink, as well as some operations for it, which allow shrink to be defined using the same Applicative-style approach, but which allow product types to shrink the way we expect.

So how does it work? The key insight is that a shrinker producing [] in isolation can tell us nothing in particular: that shrinker might be part of a much bigger shrink, or possibly just be on its own. In the specific case of shrinking a product type, we do this by composing shrinkers, but that particular composition is not aware that we are dealing with a product type. Thus, we have to provide a way to direct specifically shrinking of product types: then, we will have enough information to know which, and how many, shrinkers have to fail before we fail shrinking the entire product type.

To see how we do this, let's first examine the definition of Shrink:

data Shrink a = 
    NonShrinking a |
    Shrinking (NonEmpty a)

We can imagine Shrink a as being the equivalent of Either a (NonEmpty a): Left x in this case means 'we failed to shrink x, but we remember it in case we need it again', whereas Right ys in this case means 'we shrunk, and ys are the shrunk terms that resulted'. Another way to look at this is that we have extended [] with the additional information of what we tried to shrink in case of failure.

To see how this works in practice, we need to look at the other main part of quickcheck-helpers' functionality:

neShrink :: Arbitrary a => a -> Shrink a
neShrink x = case shrink x of 
    [] -> NonShrinking x
    (y : ys) -> Shrinking (y :| ys)

We can see the use for the NonShrinking 'arm' of Shrink here: it allows us to 'remember' the term that we failed to shrink, in case we end up needing it later. In the context of shrinking product types, this is exactly the information that we need.

For Shrink to be of much use, it has to be composable, in the same way [] can be. We can straightforwardly define a Functor instance:

instance Functor Shrink where
    fmap f = \case
        NonShrinking x -> NonShrinking $ f a
        Shrinking xs -> Shrinking $ fmap f xs

Applicative however is more interesting:

instance Applicative Shrink where
    fs <*> xs = case fs of 
        NonShrinking f -> case xs of 
            NonShrinking x -> NonShrinking (f x)
            Shrinking xs' -> Shrinking (fmap f xs')
        Shrinking fs' -> case xs of 
            NonShrinking x -> Shrinking (fmap ($ x) fs')
            Shrinking xs' -> Shrinking (fs' <*> xs')
    pure = NonShrinking

To see why this is the implementation of <*> we want, let's consider what happens when we attempt `Pair <$ data-preserve-html-node="true"> neShrink (0 :: Int) <* data-preserve-html-node="true"> neShrink (6 :: Int):

-- initial
Pair <$> neShrink 0 <*> neShrink 6
-- definition of neShrink for 0
Pair <$> NonShrinking 0 <*> neShrink 6
-- definition of <$>
NonShrinking (Pair 0) <*> neShrink 6
-- definition of neShrink for 6
NonShrinking (Pair 0) <*> Shrinking (5 :| [3, 0])
-- definition of <*>
Shrinking (fmap (Pair 0)) (5 :| [3, 0])
-- definition of fmap
Shrinking (Pair 0 5 :| [Pair 0 3, Pair 0 0])

We can see that even though the left-hand-side of <*> is not shrinkable, the right-hand-side still is. As we can 'remember' the term we failed to shrink, provided we have at least one NonShrinking in our composition using <*>, we can still determine what the shrink would look like.

From here, we can derive pure simply by following the relevant laws. While the implementation described above follows these laws, this doesn't really explain why our choice of pure is correct. To see why this is the case, let's consider the difference between how Shrink and [] treat a singleton result.

A singleton list [x] can be seen as two different things in the context of non-determinism:

• [x] is a computation that was not meant to be non-deterministic in the first place (that is, it came from pure); and
• [x] is a non-deterministic computation that happens to produce exactly one result.

While making these two things equivalent is not a problem for non-determinism more generally, for shrinking, these are very different situations: the first cannot have come from shrinking (and thus, should not be subject to it), while the second must have come from shrinking. Shrink distinguishes these two cases: NonShrinking x represents the first case, while Shrinking (x :| []) represents the second. By that logic, pure should indeed be NonShrinking.

With Applicative available, we have enough tools to define a Shrink suitable to our task. The last part we need is a way of 'running' a Shrink to produce the expected result of a shrinker:

toShrink :: Shrink a -> [a]
toShrink = \case
    NonShrinking _ -> []
    Shrinking (x :| xs) -> x : xs

Putting this all together, we get the following definition of Arbitrary:

instance Arbitrary a => Arbitrary (Pair a) where
    -- Same as before
    arbitrary = Pair <$> arbitrary <*> arbitrary
    -- Uses the new operations in `Shrink`
    shrink (Pair x y) = toShrink (Pair <$> neShrink x <*> neShrink y)

This works the way that we expect:

ghci> shrink (Pair 0 6 :: Pair Int)
[Pair 0 0,Pair 0 3,Pair 0 5]
ghci> shrink (Pair 6 0 :: Pair Int)
[Pair 0 0,Pair 3 0,Pair 5 0]
ghci> shrink (Pair 0 0 :: Pair Int)
[]

While this does solve our problem as we posed it, it's worth asking whether Shrink can be made more capable. In particular, it would be great to have Alternative and Monad instances, as this would allow us to completely replace all use of [] for shrinkers. However, both of these are not possible to define for Shrink while staying true to the laws that these type classes expect their instances to follow. The root cause of this is the same as the reasoning we gave above for pure: distinguishing terms that were produced by shrinking from terms that were not.

Alternative is the easier case to explain. What should we do if we are given NonShrinkable x <|> Shrinkable (y :| ys)? The first option that seems sensible is something like Shrinkable (x :| (y : ys)), but this immediately poses a problem: we have now 'forgotten' that x did not come from shrinking! This would immediately cause problems, potentially even creating infinite shrinking loops by accidentally including a shrinking target in the list of its own shrinks. To see the problem, consider the following situation under the definition of <|> presented above:

(Pair <$> pure (0 :: Int) <*> neShrink (1 :: Int)) <|> 
(Pair <$> neShrink (0 :: Int) <*> pure (1 :: Int))
-- definition of neShrink for 0, 1
(Pair <$> pure (0 :: Int) <*> Shrinking (0 :| [])) <|>
(Pair <$> NonShrinking 0 <*> pure (1 :: Int))
-- definition of pure
(Pair <$> NonShrinking 0 <*> Shrinking (0 :| [])) <|>
(Pair <$> NonShrinking 0 <*> NonShrinking 1)
-- Definition of <$>
(NonShrinking (Pair 0) <*> Shrinking (0 :| [])) <|>
(NonShrinking (Pair 0) <*> NonShrinking 1)
-- Definition of <*>
Shrinking (Pair 0 0 :| []) <|> NonShrinking (Pair 0 1)
-- Implied definition of <|>
Shrinking (Pair 0 0 :| [Pair 0 1])

This is catastrophic - by mirroring something that would give correct answers in [], we end up with a shrinker that includes the target in the list of shrinks, thereby looping forever.

An alternative option would be to 'throw away' any NonShrinking results when combining with <|>. Then, we would have NonShrinkable x <> Shrinkable ys = Shrinkable ys. This avoids the problem we showed above, but presents a new problem: what should we do when faced with Shrinkable x <|> Shrinkable y? We can choose to either produce Shrinkable x in this case (that is, the first non-shrinkable we see) or Shrinkable y (that is, the last non-shrinkable we see). Both of these choices avoid the problem from before:

(Pair <$> pure (0 :: Int) <*> neShrink (1 :: Int)) <|> 
(Pair <$> neShrink (0 :: Int) <*> pure (1 :: Int))
-- definition of neShrink for 0, 1
(Pair <$> pure (0 :: Int) <*> Shrinking (0 :| [])) <|>
(Pair <$> NonShrinking 0 <*> pure (1 :: Int))
-- definition of pure
(Pair <$> NonShrinking 0 <*> Shrinking (0 :| [])) <|>
(Pair <$> NonShrinking 0 <*> NonShrinking 1)
-- Definition of <$>
(NonShrinking (Pair 0) <*> Shrinking (0 :| [])) <|>
(NonShrinking (Pair 0) <*> NonShrinking 1)
-- Definition of <*>
Shrinking (Pair 0 0 :| []) <|> NonShrinking (Pair 0 1)
-- New definition of <|> (doesn't matter whether we choose first or last)
Shrinking (Pair 0 0 :| [])

This choice also happens to satisfy the associativity law for <|>. However, we now have the problem of empty: how do we produce Shrink a for any a whatsoever? Lists solve this problem using [], but Shrink doesn't have such an option on purpose, specifically to prevent the issue of shrinks 'stopping early' that we discussed initially. While we could potentially add another data constructor to Shrink for this purpose, it would ultimately just bring back the very problem we were trying to avoid. Thus, we can see that an Alternative instance for Shrink is not possible while maintaining both our goals and the relevant laws.

The Monad situation runs into a similar problem, but in a more complex way. Consider the situation where we have Shrinking (x :| xs) >>= f. The f in this case has type a -> Shrink b, and could produce a mixture of Shrinking and NonShrinking results depending on what x and xs are here. "No problem!", you say, "Let's just take our second solution for <|> and generalize it.". By this solution, given the above, we would apply f to x and xs, then 'throw out' any NonShrinking results we end up with. However, this immediately runs into a problem: what if we get no Shrinking results from applying f? We would need something like empty in this case, which we already saw that we cannot have without bringing back the very problem we sought to avoid. However, even if we found that cost acceptable, there is yet another problem. According to the laws of Monad, we must have x >>= pure = x for any x. Given that pure = NonShrinking, if we had Shrinking (x :| xs) >>= pure, we would end up with empty, which is different to Shrinking (x :| xs). Thus, even if we were willing to accept empty, Shrink would still fail to be a Monad.

Thus, Shrink is not a full replacement for [] in defining shrinkers. Instead, it represents a sub-language specifically for defining how to shrink product types. We can use Shrink to replace [] for some types (such as Pair given above). However, in some cases, we have to use Shrink by 'embedding' it into a [] computation. Consider, for example, the instance for These:

-- data These a b = This a | That b | These a b

instance (Arbitrary a, Arbitrary b) => Arbitrary (These a b) where
    arbitrary = oneof [
        This <$> arbitrary, 
        That <$> arbitrary, 
        These <$> arbitrary <*> arbitrary
        ]
    shrink = \case
        This x -> This <$> shrink x
        That y -> That <$> shrink y
        These x y -> toShrink (These <$> neShrink x <*> neShrink y)

For the one-field constructors of These, we can define the shrinker as usual. For the two-field These constructor, we instead use Shrink to ensure that we get the behaviour we want.

Our real-life use case

So why did MLabs need to solve this problem? Fundamentally, this stems from an important requirement for both Plutarch 1.0 and Plutarch 2.0: we must ensure that the Plutarch-side definitions corresponding to ledger types are correct given the canonical definitions and implementations in plutus-ledger-api. Specifically, we must ensure that the Data representation of each of these types is consistent across plutus-ledger-api and Plutarch.

To ensure that we can test this, we use property-based testing, together with a large number of orphan instances for all the plutus-ledger-api types, in Plutarch 1.0. To ensure the same capabilities remain in Plutarch 2.0, we have ported the instances for the V4 ledger types. These instances require working over extremely large product types: for example, TopTxInfoSimplified contains 18 fields (somewhat ironically given its name). Furthermore, we often have non-structural invariants to maintain: TopTxInfoSimplified has two list fields that must remain-non-empty, for example. As part of this effort, we found that our shrinkers for such types were incorrectly defined using Applicative syntax for lists.

Due to the non-structural invariants on many types, we cannot avoid the use of manually-written shrinkers. Fixing this issue in both Plutarch 1.0 and Plutarch 2.0 would take a huge amount of effort, and likely create bugs that would be difficult to detect, and make our tests weaker by remaining. To that end, we decided that a solution like quickcheck-helpers could be used by both Plutarch 1.0 and Plutarch 2.0 to solve this problem once and for all. Indeed, at the time of writing, the instances needed for Plutarch 2.0 using quickcheck-helpers have already been merged, and the 1.0 instances are part of an active PR.

Conclusion

QuickCheck, when used correctly, is a powerful testing tool. Not only can it uncover classes of bugs you could never have thought of, it can automatically minimize reproducing cases to help with debugging and regression prevention. Plutarch's extensive use of QuickCheck has demonstrated its power in many situations, but none more so than ensuring that Plutarch's definitions of the Plutus ledger types stay in-sync with the definitions and representations in plutus-ledger-api.

At the same time, QuickCheck is only as good as the tests you write, which in turn, are only as good as the Arbitrary instances used to generate cases for them. Shrinkers in particular are a known point of difficulty with QuickCheck, especially when the results must maintain complex invariants. The subtlety of the problem we describe is easy to miss, and potentially severely limits the usefulness of shrinkers over product types. The solutions either require giving up all non-structural control over shrinker definitions, or quadratic amounts of tedium and great care.

As major users of QuickCheck, we believe in the importance of good shrinkers, and feel that the problem we described is one that should be solved once and for all. To that end, we created quickcheck-helpers, and are using it to ensure that Plutarch 1.0 remains well-tested, and that Plutarch 2.0 will continue that practice. This will make Plutarch 2.0's release better and stronger, but will also benefit the Haskell community by providing a helper for QuickCheck in any project.