From 8b6fb7010294e9de970b4aa90de9acdc6f63d751 Mon Sep 17 00:00:00 2001
From: Rik <rik.de.kort@hey.com>
Date: Wed, 13 Mar 2024 19:06:38 +0100
Subject: [PATCH 01/11] Tester for clarity in removal shrinking

---
 minithesis.py | 95 +++++++++++++++++++++++++++------------------------
 1 file changed, 51 insertions(+), 44 deletions(-)

diff --git a/minithesis.py b/minithesis.py
index c508661..8d57541 100644
--- a/minithesis.py
+++ b/minithesis.py
@@ -674,50 +674,7 @@ def consider(choices: array[int]) -> bool:
             # issues, but the end result should still be fine.
 
             # First try deleting each choice we made in chunks.
-            # We try longer chunks because this allows us to
-            # delete whole composite elements: e.g. deleting an
-            # element from a generated list requires us to delete
-            # both the choice of whether to include it and also
-            # the element itself, which may involve more than one
-            # choice. Some things will take more than 8 choices
-            # in the sequence. That's too bad, we may not be
-            # able to delete those. In Hypothesis proper we
-            # record the boundaries corresponding to ``any``
-            # calls so that we can try deleting those, but
-            # that's pretty high overhead and also a bunch of
-            # slightly annoying code that it's not worth porting.
-            #
-            # We could instead do a quadratic amount of work
-            # to try all boundaries, but in general we don't
-            # want to do that because even a shrunk test case
-            # can involve a relatively large number of choices.
-            k = 8
-            while k > 0:
-                i = len(self.result) - k - 1
-                while i >= 0:
-                    if i >= len(self.result):
-                        # Can happen if we successfully lowered
-                        # the value at i - 1
-                        i -= 1
-                        continue
-                    attempt = self.result[:i] + self.result[i + k :]
-                    assert len(attempt) < len(self.result)
-                    if not consider(attempt):
-                        # This fixes a common problem that occurs
-                        # when you have dependencies on some
-                        # length parameter. e.g. draw a number
-                        # between 0 and 10 and then draw that
-                        # many elements. This can't delete
-                        # everything that occurs that way, but
-                        # it can delete some things and often
-                        # will get us unstuck when nothing else
-                        # does.
-                        if i > 0 and attempt[i - 1] > 0:
-                            attempt[i - 1] -= 1
-                            if consider(attempt):
-                                i += 1
-                        i -= 1
-                k //= 2
+            self.shrink_remove(consider)
 
             def replace(values: Mapping[int, int]) -> bool:
                 """Attempts to replace some indices in the current
@@ -809,6 +766,56 @@ def replace(values: Mapping[int, int]) -> bool:
                                 ),
                             )
 
+    def shrink_remove(self, consider):
+        # Try removing chunks, starting from the end.
+        # We try longer chunks because this allows us to
+        # delete whole composite elements: e.g. deleting an
+        # element from a generated list requires us to delete
+        # both the choice of whether to include it and also
+        # the element itself, which may involve more than one
+        # choice. Some things will take more than 8 choices
+        # in the sequence. That's too bad, we may not be
+        # able to delete those. In Hypothesis proper we
+        # record the boundaries corresponding to ``any``
+        # calls so that we can try deleting those, but
+        # that's pretty high overhead and also a bunch of
+        # slightly annoying code that it's not worth porting.
+        #
+        # We could instead do a quadratic amount of work
+        # to try all boundaries, but in general we don't
+        # want to do that because even a shrunk test case
+        # can involve a relatively large number of choices.
+        for n_to_remove in range(8, 0, -1):
+            removal_index = len(self.result) - n_to_remove - 1
+            while removal_index >= 0:
+                if removal_index >= len(self.result):
+                    # Can happen if we successfully lowered
+                    # the value at removal_index - 1
+                    removal_index -= 1
+                    continue
+                attempt = self.result[:removal_index] + self.result[removal_index + n_to_remove:]
+                assert len(attempt) < len(self.result)
+                if not consider(attempt):
+                    # If we have dependencies on some length
+                    # parameter, e.g. draw a number between
+                    # 0 and 10 and then draw that many
+                    # elements, shrinking often gets stuck
+                    # because the decision to add many
+                    # elements was made early in the chain.
+                    # We check if the element just
+                    # prior to our removal could be a length
+                    # and try decreasing it.
+                    # This can't delete everything that occurs
+                    # as described, but it can delete some
+                    # things and often will get us unstuck
+                    # when nothing else does.
+                    if removal_index > 0 and attempt[removal_index - 1] > 0:
+                        attempt[removal_index - 1] -= 1
+                        # If successful, retry the removal pass
+                        if consider(attempt):
+                            continue
+                    removal_index -= 1
+
 
 def bin_search_down(lo: int, hi: int, f: Callable[[int], bool]) -> int:
     """Returns n in [lo, hi] such that f(n) is True,

From 8d86bf3858055211d851f4e25ff7194a04022229 Mon Sep 17 00:00:00 2001
From: Rik <rik.de.kort@hey.com>
Date: Wed, 13 Mar 2024 19:37:45 +0100
Subject: [PATCH 02/11] Try extract a shrinking pass in a functional style

---
 minithesis.py | 108 ++++++++++++++++++++++++++++++--------------------
 1 file changed, 64 insertions(+), 44 deletions(-)

diff --git a/minithesis.py b/minithesis.py
index 8d57541..9237c44 100644
--- a/minithesis.py
+++ b/minithesis.py
@@ -676,53 +676,17 @@ def consider(choices: array[int]) -> bool:
             # First try deleting each choice we made in chunks.
             self.shrink_remove(consider)
 
-            def replace(values: Mapping[int, int]) -> bool:
-                """Attempts to replace some indices in the current
-                result with new values. Useful for some purely lexicographic
-                reductions that we are about to perform."""
-                assert self.result is not None
-                attempt = array("Q", self.result)
-                for i, v in values.items():
-                    # The size of self.result can change during shrinking.
-                    # If that happens, stop attempting to make use of these
-                    # replacements because some other shrink pass is better
-                    # to run now.
-                    if i >= len(attempt):
-                        return False
-                    attempt[i] = v
-                return consider(attempt)
-
             # Now we try replacing blocks of choices with zeroes.
-            # Note that unlike the above we skip k = 1 because we
-            # handle that in the next step. Often (but not always)
-            # a block of all zeroes is the shortlex smallest value
-            # that a region can be.
-            k = 8
-
-            while k > 1:
-                i = len(self.result) - k
-                while i >= 0:
-                    if replace({j: 0 for j in range(i, i + k)}):
-                        # If we've succeeded then all of [i, i + k]
-                        # is zero so we adjust i so that the next region
-                        # does not overlap with this at all.
-                        i -= k
-                    else:
-                        # Otherwise we might still be able to zero some
-                        # of these values but not the last one, so we
-                        # just go back one.
-                        i -= 1
-                k //= 2
+            self.result = shrink_zeroes(self.result, consider)
 
             # Now try replacing each choice with a smaller value
             # by doing a binary search. This will replace n with 0 or n - 1
             # if possible, but will also more efficiently replace it with
             # a smaller number than doing multiple subtractions would.
-            i = len(self.result) - 1
-            while i >= 0:
-                # Attempt to replace
-                bin_search_down(0, self.result[i], lambda v: replace({i: v}))
-                i -= 1
+            for i in reversed(range(len(self.result))):
+                bin_search_down(
+                    0, self.result[i], lambda v: replace(self.result, {i: v}, consider)
+                )
 
             # NB from here on this is just showing off cool shrinker tricks and
             # you probably don't need to worry about it and can skip these bits
@@ -753,7 +717,11 @@ def replace(values: Mapping[int, int]) -> bool:
                     if j < len(self.result):  # pragma: no cover
                         # Try swapping out of order pairs
                         if self.result[i] > self.result[j]:
-                            replace({j: self.result[i], i: self.result[j]})
+                            replace(
+                                self.result,
+                                {j: self.result[i], i: self.result[j]},
+                                consider,
+                            )
                         # j could be out of range if the previous swap succeeded.
                         if j < len(self.result) and self.result[i] > 0:
                             previous_i = self.result[i]
@@ -762,7 +730,9 @@ def replace(values: Mapping[int, int]) -> bool:
                                 0,
                                 previous_i,
                                 lambda v: replace(
-                                    {i: v, j: previous_j + (previous_i - v)}
+                                    self.result,
+                                    {i: v, j: previous_j + (previous_i - v)},
+                                    consider,
                                 ),
                             )
 
@@ -793,7 +763,10 @@ def shrink_remove(self, consider):
                     # the value at removal_index - 1
                     removal_index -= 1
                     continue
-                attempt = self.result[:removal_index] + self.result[removal_index + n_to_remove:]
+                attempt = (
+                    self.result[:removal_index]
+                    + self.result[removal_index + n_to_remove :]
+                )
                 assert len(attempt) < len(self.result)
                 if not consider(attempt):
                     # If we have dependencies on some length
@@ -817,6 +790,53 @@ def shrink_remove(self, consider):
                     removal_index -= 1
 
 
+def replace(
+    current: array[int],
+    values: Mapping[int, int],
+    is_interesting: Callable[[array[int]], bool],
+) -> bool:
+    """Attempts to replace some indices in the current
+    result with new values. Useful for some purely lexicographic
+    reductions that we are about to perform."""
+    assert current is not None
+    attempt = array("Q", current)
+    for i, v in values.items():
+        # The size of self.result can change during shrinking.
+        # If that happens, stop attempting to make use of these
+        # replacements because some other shrink pass is better
+        # to run now.
+        if i >= len(attempt):
+            return False
+        attempt[i] = v
+    return is_interesting(attempt)
+
+
+def shrink_zeroes(
+    attempt: array[int], is_interesting: Callable[[array[int]], bool]
+) -> array[int]:
+    # Try replacing blocks with zeroes
+    # Note that unlike the above we skip k = 1 because we
+    # handle that in the next step. Often (but not always)
+    # a block of all zeroes is the shortlex smallest value
+    # that a region can be.
+    size = 8
+    while size > 1:
+        i = len(attempt) - size
+        while i >= 0:
+            if replace(attempt, {j: 0 for j in range(i, i + size)}, is_interesting):
+                # If we've succeeded then all of [i, i + size]
+                # is zero so we adjust i so that the next region
+                # does not overlap with this at all.
+                i -= size
+            else:
+                # Otherwise we might still be able to zero some
+                # of these values but not the last one, so we
+                # just go back one.
+                i -= 1
+        size //= 2
+    return attempt
+
+
 def bin_search_down(lo: int, hi: int, f: Callable[[int], bool]) -> int:
     """Returns n in [lo, hi] such that f(n) is True,
     where it is assumed and will not be checked that

From 751dbe5efebc30a983651078848b84d7f666dcec Mon Sep 17 00:00:00 2001
From: Rik <rik.de.kort@hey.com>
Date: Wed, 13 Mar 2024 19:57:48 +0100
Subject: [PATCH 03/11] Revert "Try extract a shrinking pass in a functional
 style"

This reverts commit 8d86bf3858055211d851f4e25ff7194a04022229.
---
 minithesis.py | 108 ++++++++++++++++++++------------------------------
 1 file changed, 44 insertions(+), 64 deletions(-)

diff --git a/minithesis.py b/minithesis.py
index 9237c44..8d57541 100644
--- a/minithesis.py
+++ b/minithesis.py
@@ -676,17 +676,53 @@ def consider(choices: array[int]) -> bool:
             # First try deleting each choice we made in chunks.
             self.shrink_remove(consider)
 
+            def replace(values: Mapping[int, int]) -> bool:
+                """Attempts to replace some indices in the current
+                result with new values. Useful for some purely lexicographic
+                reductions that we are about to perform."""
+                assert self.result is not None
+                attempt = array("Q", self.result)
+                for i, v in values.items():
+                    # The size of self.result can change during shrinking.
+                    # If that happens, stop attempting to make use of these
+                    # replacements because some other shrink pass is better
+                    # to run now.
+                    if i >= len(attempt):
+                        return False
+                    attempt[i] = v
+                return consider(attempt)
+
             # Now we try replacing blocks of choices with zeroes.
-            self.result = shrink_zeroes(self.result, consider)
+            # Note that unlike the above we skip k = 1 because we
+            # handle that in the next step. Often (but not always)
+            # a block of all zeroes is the shortlex smallest value
+            # that a region can be.
+            k = 8
+
+            while k > 1:
+                i = len(self.result) - k
+                while i >= 0:
+                    if replace({j: 0 for j in range(i, i + k)}):
+                        # If we've succeeded then all of [i, i + k]
+                        # is zero so we adjust i so that the next region
+                        # does not overlap with this at all.
+                        i -= k
+                    else:
+                        # Otherwise we might still be able to zero some
+                        # of these values but not the last one, so we
+                        # just go back one.
+                        i -= 1
+                k //= 2
 
             # Now try replacing each choice with a smaller value
             # by doing a binary search. This will replace n with 0 or n - 1
             # if possible, but will also more efficiently replace it with
             # a smaller number than doing multiple subtractions would.
-            for i in reversed(range(len(self.result))):
-                bin_search_down(
-                    0, self.result[i], lambda v: replace(self.result, {i: v}, consider)
-                )
+            i = len(self.result) - 1
+            while i >= 0:
+                # Attempt to replace
+                bin_search_down(0, self.result[i], lambda v: replace({i: v}))
+                i -= 1
 
             # NB from here on this is just showing off cool shrinker tricks and
             # you probably don't need to worry about it and can skip these bits
@@ -717,11 +753,7 @@ def consider(choices: array[int]) -> bool:
                     if j < len(self.result):  # pragma: no cover
                         # Try swapping out of order pairs
                         if self.result[i] > self.result[j]:
-                            replace(
-                                self.result,
-                                {j: self.result[i], i: self.result[j]},
-                                consider,
-                            )
+                            replace({j: self.result[i], i: self.result[j]})
                         # j could be out of range if the previous swap succeeded.
                         if j < len(self.result) and self.result[i] > 0:
                             previous_i = self.result[i]
@@ -730,9 +762,7 @@ def consider(choices: array[int]) -> bool:
                                 0,
                                 previous_i,
                                 lambda v: replace(
-                                    self.result,
-                                    {i: v, j: previous_j + (previous_i - v)},
-                                    consider,
+                                    {i: v, j: previous_j + (previous_i - v)}
                                 ),
                             )
 
@@ -763,10 +793,7 @@ def shrink_remove(self, consider):
                     # the value at removal_index - 1
                     removal_index -= 1
                     continue
-                attempt = (
-                    self.result[:removal_index]
-                    + self.result[removal_index + n_to_remove :]
-                )
+                attempt = self.result[:removal_index] + self.result[removal_index + n_to_remove:]
                 assert len(attempt) < len(self.result)
                 if not consider(attempt):
                     # If we have dependencies on some length
@@ -790,53 +817,6 @@ def shrink_remove(self, consider):
                     removal_index -= 1
 
 
-def replace(
-    current: array[int],
-    values: Mapping[int, int],
-    is_interesting: Callable[[array[int]], bool],
-) -> bool:
-    """Attempts to replace some indices in the current
-    result with new values. Useful for some purely lexicographic
-    reductions that we are about to perform."""
-    assert current is not None
-    attempt = array("Q", current)
-    for i, v in values.items():
-        # The size of self.result can change during shrinking.
-        # If that happens, stop attempting to make use of these
-        # replacements because some other shrink pass is better
-        # to run now.
-        if i >= len(attempt):
-            return False
-        attempt[i] = v
-    return is_interesting(attempt)
-
-
-def shrink_zeroes(
-    attempt: array[int], is_interesting: Callable[[array[int]], bool]
-) -> array[int]:
-    # Try replacing blocks with zeroes
-    # Note that unlike the above we skip k = 1 because we
-    # handle that in the next step. Often (but not always)
-    # a block of all zeroes is the shortlex smallest value
-    # that a region can be.
-    size = 8
-    while size > 1:
-        i = len(attempt) - size
-        while i >= 0:
-            if replace(attempt, {j: 0 for j in range(i, i + size)}, is_interesting):
-                # If we've succeeded then all of [i, i + size]
-                # is zero so we adjust i so that the next region
-                # does not overlap with this at all.
-                i -= size
-            else:
-                # Otherwise we might still be able to zero some
-                # of these values but not the last one, so we
-                # just go back one.
-                i -= 1
-        size //= 2
-    return attempt
-
-
 def bin_search_down(lo: int, hi: int, f: Callable[[int], bool]) -> int:
     """Returns n in [lo, hi] such that f(n) is True,
     where it is assumed and will not be checked that

From 46cf95e937a10d973392401e56cbcd36287396ff Mon Sep 17 00:00:00 2001
From: Rik <rik.de.kort@hey.com>
Date: Wed, 13 Mar 2024 20:42:13 +0100
Subject: [PATCH 04/11] Retry extract a shrinking pass in a functional style

---
 minithesis.py | 96 ++++++++++++++++++++++++++++++++-------------------
 1 file changed, 60 insertions(+), 36 deletions(-)

diff --git a/minithesis.py b/minithesis.py
index 8d57541..8ab3d1a 100644
--- a/minithesis.py
+++ b/minithesis.py
@@ -82,6 +82,8 @@
 S = TypeVar("S", covariant=True)
 U = TypeVar("U")  # Invariant
 
+InterestTest = Callable[[array], bool]  # Really array[int] -> bool
+
 
 class Database(Protocol):
     def __setitem__(self, key: str, value: bytes) -> None:
@@ -676,43 +678,12 @@ def consider(choices: array[int]) -> bool:
             # First try deleting each choice we made in chunks.
             self.shrink_remove(consider)
 
-            def replace(values: Mapping[int, int]) -> bool:
-                """Attempts to replace some indices in the current
-                result with new values. Useful for some purely lexicographic
-                reductions that we are about to perform."""
-                assert self.result is not None
-                attempt = array("Q", self.result)
-                for i, v in values.items():
-                    # The size of self.result can change during shrinking.
-                    # If that happens, stop attempting to make use of these
-                    # replacements because some other shrink pass is better
-                    # to run now.
-                    if i >= len(attempt):
-                        return False
-                    attempt[i] = v
-                return consider(attempt)
-
             # Now we try replacing blocks of choices with zeroes.
             # Note that unlike the above we skip k = 1 because we
             # handle that in the next step. Often (but not always)
             # a block of all zeroes is the shortlex smallest value
             # that a region can be.
-            k = 8
-
-            while k > 1:
-                i = len(self.result) - k
-                while i >= 0:
-                    if replace({j: 0 for j in range(i, i + k)}):
-                        # If we've succeeded then all of [i, i + k]
-                        # is zero so we adjust i so that the next region
-                        # does not overlap with this at all.
-                        i -= k
-                    else:
-                        # Otherwise we might still be able to zero some
-                        # of these values but not the last one, so we
-                        # just go back one.
-                        i -= 1
-                k //= 2
+            self.result = shrink_zeroes(self.result, consider)
 
             # Now try replacing each choice with a smaller value
             # by doing a binary search. This will replace n with 0 or n - 1
@@ -721,7 +692,13 @@ def replace(values: Mapping[int, int]) -> bool:
             i = len(self.result) - 1
             while i >= 0:
                 # Attempt to replace
-                bin_search_down(0, self.result[i], lambda v: replace({i: v}))
+                bin_search_down(
+                    0,
+                    self.result[i],
+                    lambda v: is_interesting_with_replacement(
+                        self.result, {i: v}, consider
+                    ),
+                )
                 i -= 1
 
             # NB from here on this is just showing off cool shrinker tricks and
@@ -753,7 +730,11 @@ def replace(values: Mapping[int, int]) -> bool:
                     if j < len(self.result):  # pragma: no cover
                         # Try swapping out of order pairs
                         if self.result[i] > self.result[j]:
-                            replace({j: self.result[i], i: self.result[j]})
+                            is_interesting_with_replacement(
+                                self.result,
+                                {j: self.result[i], i: self.result[j]},
+                                consider,
+                            )
                         # j could be out of range if the previous swap succeeded.
                         if j < len(self.result) and self.result[i] > 0:
                             previous_i = self.result[i]
@@ -761,8 +742,10 @@ def replace(values: Mapping[int, int]) -> bool:
                             bin_search_down(
                                 0,
                                 previous_i,
-                                lambda v: replace(
-                                    {i: v, j: previous_j + (previous_i - v)}
+                                lambda v: is_interesting_with_replacement(
+                                    self.result,
+                                    {i: v, j: previous_j + (previous_i - v)},
+                                    consider,
                                 ),
                             )
 
@@ -817,6 +800,47 @@ def shrink_remove(self, consider):
                     removal_index -= 1
 
 
+def shrink_zeroes(current: array[int], test: InterestTest) -> array[int]:
+    sizes_to_try = [8, 4, 2, 1]
+    for size in sizes_to_try:
+        i = len(current) - size
+        while i >= 0:
+            # Zero out section starting at i
+            attempt = current[:i] + array("Q", (0 for _ in range(size))) + current[i + size:]
+
+            if test(attempt):
+                current = attempt
+                # If we've succeeded then all of [i, i + size]
+                # is zero so we adjust i so that the next region
+                # does not overlap with this at all.
+                i -= size
+            else:
+                # Otherwise we might still be able to zero some
+                # of these values but not the last one, so we
+                # just go back one.
+                i -= 1
+    return current
+
+
+def is_interesting_with_replacement(
+    current: array[int], values: Mapping[int, int], test: InterestTest
+) -> bool:
+    """Attempts to replace some indices in the current
+    result with new values. Useful for some purely lexicographic
+    reductions that we are about to perform."""
+    assert current is not None
+
+    # If replacement map is out-of-range, abort.
+    # Some other shrinking pass is probably better.
+    if any(i >= len(current) for i in values.keys()):
+        return False
+
+    attempt = array("Q", current)
+    for i, v in values.items():
+        attempt[i] = v
+    return test(attempt)
+
+
 def bin_search_down(lo: int, hi: int, f: Callable[[int], bool]) -> int:
     """Returns n in [lo, hi] such that f(n) is True,
     where it is assumed and will not be checked that

From 94626a8619718c9fcab22f2f51de142b0951f59f Mon Sep 17 00:00:00 2001
From: Rik <rik.de.kort@hey.com>
Date: Wed, 13 Mar 2024 20:49:01 +0100
Subject: [PATCH 05/11] Move explanatory comment down, skip size=1 in
 shrink_zeroes

---
 minithesis.py | 23 +++++++++++++++--------
 1 file changed, 15 insertions(+), 8 deletions(-)

diff --git a/minithesis.py b/minithesis.py
index 8ab3d1a..b73c270 100644
--- a/minithesis.py
+++ b/minithesis.py
@@ -679,10 +679,6 @@ def consider(choices: array[int]) -> bool:
             self.shrink_remove(consider)
 
             # Now we try replacing blocks of choices with zeroes.
-            # Note that unlike the above we skip k = 1 because we
-            # handle that in the next step. Often (but not always)
-            # a block of all zeroes is the shortlex smallest value
-            # that a region can be.
             self.result = shrink_zeroes(self.result, consider)
 
             # Now try replacing each choice with a smaller value
@@ -776,7 +772,10 @@ def shrink_remove(self, consider):
                     # the value at removal_index - 1
                     removal_index -= 1
                     continue
-                attempt = self.result[:removal_index] + self.result[removal_index + n_to_remove:]
+                attempt = (
+                    self.result[:removal_index]
+                    + self.result[removal_index + n_to_remove :]
+                )
                 assert len(attempt) < len(self.result)
                 if not consider(attempt):
                     # If we have dependencies on some length
@@ -801,12 +800,20 @@ def shrink_remove(self, consider):
 
 
 def shrink_zeroes(current: array[int], test: InterestTest) -> array[int]:
-    sizes_to_try = [8, 4, 2, 1]
-    for size in sizes_to_try:
+    # Try zero-ing out sections.
+    # Note that we skip a block of size 1 because that will
+    # be taken care of by a pass that tries lower values.
+    # Often (but not always), a block of all zeroes is the
+    # shortlex smallest value that a region can be.
+    for size in [8, 4, 2]:
         i = len(current) - size
         while i >= 0:
             # Zero out section starting at i
-            attempt = current[:i] + array("Q", (0 for _ in range(size))) + current[i + size:]
+            attempt = (
+                current[:i]
+                + array("Q", (0 for _ in range(size)))
+                + current[i + size :]
+            )
 
             if test(attempt):
                 current = attempt

From c234d989381e58027a477bac00294423510cedb2 Mon Sep 17 00:00:00 2001
From: Rik <rik.de.kort@hey.com>
Date: Wed, 13 Mar 2024 20:58:48 +0100
Subject: [PATCH 06/11] Extract shrink-lowering pass

---
 minithesis.py | 34 +++++++++++++++++-----------------
 1 file changed, 17 insertions(+), 17 deletions(-)

diff --git a/minithesis.py b/minithesis.py
index b73c270..cb98703 100644
--- a/minithesis.py
+++ b/minithesis.py
@@ -682,20 +682,8 @@ def consider(choices: array[int]) -> bool:
             self.result = shrink_zeroes(self.result, consider)
 
             # Now try replacing each choice with a smaller value
-            # by doing a binary search. This will replace n with 0 or n - 1
-            # if possible, but will also more efficiently replace it with
-            # a smaller number than doing multiple subtractions would.
-            i = len(self.result) - 1
-            while i >= 0:
-                # Attempt to replace
-                bin_search_down(
-                    0,
-                    self.result[i],
-                    lambda v: is_interesting_with_replacement(
-                        self.result, {i: v}, consider
-                    ),
-                )
-                i -= 1
+            self.result = shrink_lower(self.result, consider)
+
 
             # NB from here on this is just showing off cool shrinker tricks and
             # you probably don't need to worry about it and can skip these bits
@@ -810,9 +798,7 @@ def shrink_zeroes(current: array[int], test: InterestTest) -> array[int]:
         while i >= 0:
             # Zero out section starting at i
             attempt = (
-                current[:i]
-                + array("Q", (0 for _ in range(size)))
-                + current[i + size :]
+                current[:i] + array("Q", (0 for _ in range(size))) + current[i + size :]
             )
 
             if test(attempt):
@@ -829,6 +815,20 @@ def shrink_zeroes(current: array[int], test: InterestTest) -> array[int]:
     return current
 
 
+def shrink_lower(current: array[int], is_interesting: InterestTest) -> array[int]:
+    # Try replacing each choice with a smaller value
+    # by doing a binary search. This will replace n with 0 or n - 1
+    # if possible, but will also more efficiently replace it with
+    # a smaller number than doing multiple subtractions would.
+    for i in reversed(range(len(current))):
+        current[i] = bin_search_down(
+            0,
+            current[i],
+            lambda v: is_interesting_with_replacement(current, {i: v}, is_interesting),
+        )
+    return current
+
+
 def is_interesting_with_replacement(
     current: array[int], values: Mapping[int, int], test: InterestTest
 ) -> bool:

From 5affd0259371234a10468cd88ee86553dfa795c9 Mon Sep 17 00:00:00 2001
From: Rik <rik.de.kort@hey.com>
Date: Wed, 13 Mar 2024 21:20:05 +0100
Subject: [PATCH 07/11] Extract shrink_sort pass

---
 minithesis.py | 26 ++++++++++++++++----------
 1 file changed, 16 insertions(+), 10 deletions(-)

diff --git a/minithesis.py b/minithesis.py
index cb98703..d5c47e3 100644
--- a/minithesis.py
+++ b/minithesis.py
@@ -684,7 +684,6 @@ def consider(choices: array[int]) -> bool:
             # Now try replacing each choice with a smaller value
             self.result = shrink_lower(self.result, consider)
 
-
             # NB from here on this is just showing off cool shrinker tricks and
             # you probably don't need to worry about it and can skip these bits
             # unless they're easy and you want bragging rights for how much
@@ -692,15 +691,7 @@ def consider(choices: array[int]) -> bool:
 
             # Try sorting out of order ranges of choices, as ``sort(x) <= x``,
             # so this is always a lexicographic reduction.
-            k = 8
-            while k > 1:
-                for i in range(len(self.result) - k - 1, -1, -1):
-                    consider(
-                        self.result[:i]
-                        + array("Q", sorted(self.result[i : i + k]))
-                        + self.result[i + k :]
-                    )
-                k //= 2
+            self.result = shrink_sort(self.result, consider)
 
             # Try adjusting nearby pairs of integers by redistributing value
             # between them. This is useful for tests that depend on the
@@ -829,6 +820,21 @@ def shrink_lower(current: array[int], is_interesting: InterestTest) -> array[int
     return current
 
 
+def shrink_sort(current: array[int], is_interesting: InterestTest) -> array[int]:
+    # Try sorting out of order ranges of choices, as ``sort(x) <= x``,
+    # so this is always a lexicographic reduction.
+    for size in [8, 4, 2]:
+        for i in reversed(range(len(current) - size)):
+            attempt = (
+                current[:i]
+                + array("Q", sorted(current[i : i + size]))
+                + current[i + size :]
+            )
+            if is_interesting(attempt):
+                current = attempt
+    return current
+
+
 def is_interesting_with_replacement(
     current: array[int], values: Mapping[int, int], test: InterestTest
 ) -> bool:

From 9a9422129461e2557b6e508186684abf912bbd26 Mon Sep 17 00:00:00 2001
From: Rik <rik.de.kort@hey.com>
Date: Fri, 15 Mar 2024 14:56:01 +0100
Subject: [PATCH 08/11] Successfully extract shrink_redistribute pass

---
 minithesis.py | 82 +++++++++++++++++++++++++++++----------------------
 1 file changed, 47 insertions(+), 35 deletions(-)

diff --git a/minithesis.py b/minithesis.py
index d5c47e3..e297d1e 100644
--- a/minithesis.py
+++ b/minithesis.py
@@ -657,12 +657,13 @@ def consider(choices: array[int]) -> bool:
         while prev != self.result:
             prev = self.result
 
-            # A note on weird loop order: We iterate backwards
-            # through the choice sequence rather than forwards,
-            # because later bits tend to depend on earlier bits
-            # so it's easier to make changes near the end and
-            # deleting bits at the end may allow us to make
-            # changes earlier on that we we'd have missed.
+            # A note on weird loop order in shrinking passes:
+            # We iterate backwards through the choice sequence
+            # rather than forwards, because later bits tend to
+            # depend on earlier bits so it's easier to make
+            # changes near the end and deleting bits at the end
+            # may allow us to make changes earlier on that we'd
+            # have missed.
             #
             # Note that we do not restart the loop at the end
             # when we find a successful shrink. This is because
@@ -694,35 +695,8 @@ def consider(choices: array[int]) -> bool:
             self.result = shrink_sort(self.result, consider)
 
             # Try adjusting nearby pairs of integers by redistributing value
-            # between them. This is useful for tests that depend on the
-            # sum of some generated values.
-            for k in [2, 1]:
-                for i in range(len(self.result) - 1 - k, -1, -1):
-                    j = i + k
-                    # This check is necessary because the previous changes
-                    # might have shrunk the size of result, but also it's tedious
-                    # to write tests for this so I didn't.
-                    if j < len(self.result):  # pragma: no cover
-                        # Try swapping out of order pairs
-                        if self.result[i] > self.result[j]:
-                            is_interesting_with_replacement(
-                                self.result,
-                                {j: self.result[i], i: self.result[j]},
-                                consider,
-                            )
-                        # j could be out of range if the previous swap succeeded.
-                        if j < len(self.result) and self.result[i] > 0:
-                            previous_i = self.result[i]
-                            previous_j = self.result[j]
-                            bin_search_down(
-                                0,
-                                previous_i,
-                                lambda v: is_interesting_with_replacement(
-                                    self.result,
-                                    {i: v, j: previous_j + (previous_i - v)},
-                                    consider,
-                                ),
-                            )
+            # between them.
+            self.result = shrink_redistribute(self.result, consider)
 
     def shrink_remove(self, consider):
         # Try removing chunks, starting from the end.
@@ -835,6 +809,44 @@ def shrink_sort(current: array[int], is_interesting: InterestTest) -> array[int]
     return current
 
 
+def shrink_redistribute(
+    current: array[int], is_interesting: InterestTest
+) -> array[int]:
+    # Try adjusting nearby pairs of integers by redistributing value
+    # between them. This is useful for tests that depend on the
+    # sum of some generated values.
+    for gap in [2, 1]:
+        for i in reversed(range(len(current) - gap)):
+            j = i + gap
+            # This check is necessary because the previous changes
+            # might have shrunk the size of result, but also it's tedious
+            # to write tests for this so I didn't.
+            if j < len(current):  # pragma: no cover
+                # Try swapping out of order pairs
+                if current[i] > current[j]:
+                    attempt = array("Q", current)
+                    attempt[i], attempt[j] = attempt[j], attempt[i]
+                    if is_interesting(attempt):
+                        current = attempt
+                # j could be out of range if the previous swap succeeded.
+                if j < len(current) and current[i] > 0:
+                    previous_i = current[i]
+                    previous_j = current[j]
+                    attempt = array("Q", current)
+                    attempt[i] = bin_search_down(
+                        0,
+                        previous_i,
+                        lambda v: is_interesting_with_replacement(
+                            attempt,
+                            {i: v, j: previous_j + (previous_i - v)},
+                            is_interesting,
+                        ),
+                    )
+                    attempt[j] = previous_j + (previous_i - attempt[i])
+                    current = attempt
+    return current
+
+
 def is_interesting_with_replacement(
     current: array[int], values: Mapping[int, int], test: InterestTest
 ) -> bool:

From 4513aa34319ca871dfa282a6e25209f23047d0ac Mon Sep 17 00:00:00 2001
From: Rik <rik.de.kort@hey.com>
Date: Fri, 15 Mar 2024 15:29:46 +0100
Subject: [PATCH 09/11] Fix bug where removal shrinking got stuck

---
 minithesis.py | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/minithesis.py b/minithesis.py
index e297d1e..c2602b6 100644
--- a/minithesis.py
+++ b/minithesis.py
@@ -118,7 +118,7 @@ def _(test_case):
     that fails.
 
     The test will be run immediately, unlike in Hypothesis where
-    @given wraps a function to expose it to the the test runner.
+    @given wraps a function to expose it to the test runner.
     If you don't want it to be run immediately wrap it inside a
     test function yourself.
 
@@ -749,7 +749,7 @@ def shrink_remove(self, consider):
                         # If successful, retry the removal pass
                         if consider(attempt):
                             continue
-                    removal_index -= 1
+                removal_index -= 1
 
 
 def shrink_zeroes(current: array[int], test: InterestTest) -> array[int]:

From 9acc786c6bda3ef684927243fd987c2286b9d078 Mon Sep 17 00:00:00 2001
From: Rik <rik.de.kort@hey.com>
Date: Fri, 15 Mar 2024 15:37:01 +0100
Subject: [PATCH 10/11] Remove shrink_remove from class

---
 minithesis.py | 117 +++++++++++++++++++++++++-------------------------
 1 file changed, 59 insertions(+), 58 deletions(-)

diff --git a/minithesis.py b/minithesis.py
index c2602b6..ea6e946 100644
--- a/minithesis.py
+++ b/minithesis.py
@@ -86,14 +86,11 @@
 
 
 class Database(Protocol):
-    def __setitem__(self, key: str, value: bytes) -> None:
-        ...
+    def __setitem__(self, key: str, value: bytes) -> None: ...
 
-    def get(self, key: str) -> Optional[bytes]:
-        ...
+    def get(self, key: str) -> Optional[bytes]: ...
 
-    def __delitem__(self, key: str) -> None:
-        ...
+    def __delitem__(self, key: str) -> None: ...
 
 
 def run_test(
@@ -677,7 +674,7 @@ def consider(choices: array[int]) -> bool:
             # issues, but the end result should still be fine.
 
             # First try deleting each choice we made in chunks.
-            self.shrink_remove(consider)
+            self.result = shrink_remove(self.result, consider)
 
             # Now we try replacing blocks of choices with zeroes.
             self.result = shrink_zeroes(self.result, consider)
@@ -698,58 +695,62 @@ def consider(choices: array[int]) -> bool:
             # between them.
             self.result = shrink_redistribute(self.result, consider)
 
-    def shrink_remove(self, consider):
-        # Try removing chunks, starting from the end.
-        # We try longer chunks because this allows us to
-        # delete whole composite elements: e.g. deleting an
-        # element from a generated list requires us to delete
-        # both the choice of whether to include it and also
-        # the element itself, which may involve more than one
-        # choice. Some things will take more than 8 choices
-        # in the sequence. That's too bad, we may not be
-        # able to delete those. In Hypothesis proper we
-        # record the boundaries corresponding to ``any``
-        # calls so that we can try deleting those, but
-        # that's pretty high overhead and also a bunch of
-        # slightly annoying code that it's not worth porting.
-        #
-        # We could instead do a quadratic amount of work
-        # to try all boundaries, but in general we don't
-        # want to do that because even a shrunk test case
-        # can involve a relatively large number of choices.
-        for n_to_remove in range(8, 0, -1):
-            removal_index = len(self.result) - n_to_remove - 1
-            while removal_index >= 0:
-                if removal_index >= len(self.result):
-                    # Can happen if we successfully lowered
-                    # the value at removal_index - 1
-                    removal_index -= 1
-                    continue
-                attempt = (
-                    self.result[:removal_index]
-                    + self.result[removal_index + n_to_remove :]
-                )
-                assert len(attempt) < len(self.result)
-                if not consider(attempt):
-                    # If we have dependencies on some length
-                    # parameter, e.g. draw a number between
-                    # 0 and 10 and then draw that many
-                    # elements, shrinking often gets stuck
-                    # because the decision to add many
-                    # elements was made early in the chain.
-                    # We check if the element just
-                    # prior to our removal could be a length
-                    # and try decreasing it.
-                    # This can't delete everything that occurs
-                    # as described, but it can delete some
-                    # things and often will get us unstuck
-                    # when nothing else does.
-                    if removal_index > 0 and attempt[removal_index - 1] > 0:
-                        attempt[removal_index - 1] -= 1
-                        # If successful, retry the removal pass
-                        if consider(attempt):
-                            continue
+
+def shrink_remove(current: array[int], is_interesting: InterestTest) -> array[int]:
+    # Try removing chunks, starting from the end.
+    # We try longer chunks because this allows us to
+    # delete whole composite elements: e.g. deleting an
+    # element from a generated list requires us to delete
+    # both the choice of whether to include it and also
+    # the element itself, which may involve more than one
+    # choice. Some things will take more than 8 choices
+    # in the sequence. That's too bad, we may not be
+    # able to delete those. In Hypothesis proper we
+    # record the boundaries corresponding to ``any``
+    # calls so that we can try deleting those, but
+    # that's pretty high overhead and also a bunch of
+    # slightly annoying code that it's not worth porting.
+    #
+    # We could instead do a quadratic amount of work
+    # to try all boundaries, but in general we don't
+    # want to do that because even a shrunk test case
+    # can involve a relatively large number of choices.
+    for n_to_remove in range(8, 0, -1):
+        removal_index = len(current) - n_to_remove - 1
+        while removal_index >= 0:
+            if removal_index >= len(current):
+                # Can happen if we successfully lowered
+                # the value at removal_index - 1
                 removal_index -= 1
+                continue
+            attempt = current[:removal_index] + current[removal_index + n_to_remove :]
+            assert len(attempt) < len(current)
+            if is_interesting(attempt):
+                current = attempt
+                removal_index -= 1
+                continue
+            else:
+                # If we have dependencies on some length
+                # parameter, e.g. draw a number between
+                # 0 and 10 and then draw that many
+                # elements, shrinking often gets stuck
+                # because the decision to add many
+                # elements was made early in the chain.
+                # We check if the element just
+                # prior to our removal could be a length
+                # and try decreasing it.
+                # This can't delete everything that occurs
+                # as described, but it can delete some
+                # things and often will get us unstuck
+                # when nothing else does.
+                if removal_index > 0 and attempt[removal_index - 1] > 0:
+                    attempt[removal_index - 1] -= 1
+                    # If successful, retry the removal pass
+                    if is_interesting(attempt):
+                        current = attempt
+                        continue
+                removal_index -= 1
+    return current
 
 
 def shrink_zeroes(current: array[int], test: InterestTest) -> array[int]:

From c10ba8215a19b7ba717f31d707678bbd516d5a19 Mon Sep 17 00:00:00 2001
From: Rik <rik.de.kort@hey.com>
Date: Mon, 18 Mar 2024 17:08:17 +0100
Subject: [PATCH 11/11] Minor formatting fix

---
 minithesis.py | 9 ++++++---
 1 file changed, 6 insertions(+), 3 deletions(-)

diff --git a/minithesis.py b/minithesis.py
index ea6e946..22d02ab 100644
--- a/minithesis.py
+++ b/minithesis.py
@@ -86,11 +86,14 @@
 
 
 class Database(Protocol):
-    def __setitem__(self, key: str, value: bytes) -> None: ...
+    def __setitem__(self, key: str, value: bytes) -> None:
+        ...
 
-    def get(self, key: str) -> Optional[bytes]: ...
+    def get(self, key: str) -> Optional[bytes]:
+        ...
 
-    def __delitem__(self, key: str) -> None: ...
+    def __delitem__(self, key: str) -> None:
+        ...
 
 
 def run_test(