Non-minimal list counter examples

[jmid]

In some (relatively rare) circumstances the QCheck.Shrink.list_spine shrinker can produce non-minimal counterexamples.
Notice the last 4-element counterexample in the following:

# #require "qcheck-core";;
# #require "qcheck-core.runner";;
# open QCheck;;
# let t =
  Test.make
    (small_list small_nat)
    (fun xs -> not (List.mem 0 xs && List.mem 1 xs && List.mem 2 xs));;

# QCheck.Test.check_exn ~rand:(Random.State.make [|16;17;16|]) t;;
Exception:
test `anon_test_1` failed on ≥ 1 cases: [1; 0; 2] (after 13 shrink steps)
                                          
# QCheck.Test.check_exn ~rand:(Random.State.make [|16;17;17|]) t;;
Exception:
test `anon_test_1` failed on ≥ 1 cases: [1; 0; 2] (after 2 shrink steps)
                                          
# QCheck.Test.check_exn ~rand:(Random.State.make [|16;17;18|]) t;;
Exception:
test `anon_test_1` failed on ≥ 1 cases: [2; 1; 0; 0] (after 4 shrink steps)

This is a consequence of the computationally fast list shrinker from #242.
In slogan form the issue can be phrased as: "speed or exhaustiveness - pick one".

In a few more words:

• A naive shrinker will try to remove each element in turn, producing O(n) shrinking candidates
  • Even that strategy is not exhaustive, as some reductions requires simultaneously removing more than one element (occurrences of add k; remove k that cancel out each other is one such example)
  • It will be prohibitively slow on longer lists though
  • We previously had a slower, but more exhaustive shrinker (see List shrinker performance #64 for more details)
• The current list shrinker is faster and thus scales to larger lists
  • To do so, we should only produce O(log n) shrinker candidates on a single shrinker invocation
  • This prohibits trying all removal candidates
  • The current shrinker is motivated and explained in more detail in Shrinker improvements #235

I'm not sure what would be the best fix to the issue without breaking the computational complexity.

In https://github.com/jmid/multicoretests where we hit this, I'm experimenting with simply stopping the recursion a bit earlier and emitting hand-chosen shrinker candidates for the new base cases.

    let rec shrink_list_spine l yield =
      let rec split l len acc = match len,l with
        | _,[]
        | 0,_ -> List.rev acc, l
        | _,x::xs -> split xs (len-1) (x::acc) in
      match l with
      | [] -> ()
      | [_] -> yield []
      | [x;y] -> yield []; yield [x]; yield [y]
      | [x;y;z] -> yield [x]; yield [x;y]; yield [x;z]; yield [y;z]
      | [x;y;z;w] -> yield [x;y;z]; yield [x;y;w]; yield [x;z;w]; yield [y;z;w]
      | _::_ ->
        let len = List.length l in
        let xs,ys = split l ((1 + len) / 2) [] in
        yield xs;
        shrink_list_spine xs (fun xs' -> yield (xs'@ys))

This has the advantage of not emitting any more candidates and the disadvantage of pushing the problem of incompleteness to larger lists (recall slogan above).

The following snippet can be used to produce an ASCII-plot of shrinker candidate counts:

# let rec loop n acc = match n with
  | 0 -> ()
  | _ ->
    Printf.printf "%3i: %!" (List.length acc);
    Shrink.list_spine acc (fun xs -> Printf.printf "#%!");
    Printf.printf "\n%!";
    loop (n-1) (n::acc)

The shape is identical - and nicely logarithmic for both Shrink.list_spine and shrink_list_spine above:

# loop 30 [];;
  0: 
  1: #
  2: ###
  3: ####
  4: ####
  5: #####
  6: #####
  7: #####
  8: #####
  9: ######
 10: ######
 11: ######
 12: ######
 13: ######
 14: ######
 15: ######
 16: ######
 17: #######
 18: #######
 19: #######
 20: #######
 21: #######
 22: #######
 23: #######
 24: #######
 25: #######
 26: #######
 27: #######
 28: #######
 29: #######

[c-cube]

At a glance: can we shrink large lists with the fast current algo, and shrink small (len < 16) lists with the more exhaustive algo? Just like sorting uses merge sort for large arrays and insertion sort for small ones?

[jmid]

That's a good suggestion 👍
To avoid breaking the complexity of the current (recursive) algo, we should then have a top-level Shrink.list that just calculates the length and decides between Shrink.list_fast and Shrink.list_more_exhaustive.

(I realize that there's redundant List.length computation going on in the current algo - and so more speed to be gained - but I digress... 😅 )