Which part of the documentation is this related to?

This package seems great, and I'm excited to give it a try. But there are several words that seem to relate to simple concepts, but are never really explained, making it unclear what exactly I can expect from this package. Specifically, the words "shrinking", "fuzzing", and "invariant" come to mind.

The biggest one is "shrinking", which is used right from the start:

shrinking of examples, which can smartly shrink initial failures to smaller example while preserving the invariants the original input was generated under

In other places throughout the docs, you glance at defining it. For example:

[once a failure is found], reducing it to something we humans can more easily use to pinpoint the uncovered bug, through a process called "shrinking".

and

Supposition.jl will [...] [try to shrink the input to the minimal example] that reproduces the same error.

But I have no idea what metric I use to define a "minimal" example, or what my simple human mind could fail to comprehend. My first thought was that Supposition would somehow try to eliminate optional arguments or keywords. I suppose I've found an explanation here, but something similar in this package's docs would be helpful. But I'll note that this very sensible definition is in tension with what I guess from the quotes above.

At one point, the docs also seem to equate shrinking with fuzzing. Again, I consult that other package's docs and find an explanation that doesn't seem consistent with what's being used here.

The word "invariant" also comes up almost immediately. When I do find some uses that give me context, it seems like an invariant is just a property. Is there some distinction that makes those different?

How could this be communicated better?

It seems to me that the "Main Page" should have a nice paragraph right near the top that introduces a few of these terms, as a way of introducing the topic, and motivating why people should want to use this approach generally (as well as this package specifically).

Supposition.@check function commutative(a=intgen, b=intgen)
     add(a,b) == add(b,a)
end

Normally b=intgen would make intgen the default argument to the function, but here it's a generator for arguments to the function. What if I actually want to pass a generator as an argument? What does Supposition.@check function commutative(a=3, b=4) do -- does it error, requiring a Just(3) or what?

It seems ambiguous and potentially confusing. Perhaps it is worth considering alternative syntax, or maybe it'll grow on me.

These must be done before registration:

• Overall API review
  • #12 and similar considerations
  • #13
• Fully customizable configuration
  • #9
  • #17
• Organize the repo
  • Create an issue template
  • Create a PR template
  • Find a place for user discussion.
    • No short-form chat, more forum like. Potential: Github Discussion, Discourse?
    • This is done now, with Github Discussions: https://github.com/Seelengrab/Supposition.jl/discussions. I'm torn about being centralized on one platform, but it's the easiest thing to do since it doesn't require people to sign up for anything else. If users can report issues/open PRs, they can also participate in the discussion.

Currently, Data.Vectors generates an extremely skewed sampling of all allowed lengths:

(data generated through map(length, (example(Data.Vectors(Data.Integers{UInt8}())) for _ in 1:10_000)))

which means that properties that require long vectors to fail won't ever fail with these defaults:

julia> using Supposition

julia> vecgen = Data.Vectors(Data.Integers{UInt8}());

julia> vecgen.max_size |> Int
10000

julia> vecgen.min_size |> Int
0

julia> @check db=Supposition.NoRecordDB() function findMin(v=vecgen)
           length(v) < 100
       end;
Test Summary: | Pass  Total  
findMin       |    1      1  

The default maximum length is 10_000, and generating such long vectors is now extremely rare. The underlying reason for that is because the underlying generation just does an exponential backoff on the length:

There are two potential paths to fixing this:

1. Tell each TestCase which "generation" of testcase it is, make that information accessible & incorporate it into produce.
   • This would mean implementing a form of iterative deepening, where later generations of TestCases are more and more likely to generate Vectors closer to the maximum length. The thinking here is that during generation, if a small example already exists we'd like to find it first, and only then try a longer & more complex one. This wouldn't change the naive plot above (shorter examples are better anyway), but should be visible in a histogram-per-generation style plot, resulting in an overall more bell-curve-like shape over the entire generation process.
2. Implement #3, remove the exponential backoff completely and implement a custom shrinker for Vectors that takes the high-level structure of "the start has the length, everything after that are the elements" into account when shrinking.

For the short term (and because it doesn't require additional new & large features), option 1) will probably suffice, but a long term solution is likely going to be better with 2). 2) also has the advantage of requiring less memory overall, because we no longer have to encode the individual markers of where elements are into the choice sequence itself, but can rather have that information be stored as metadata only.

This issue is used to trigger TagBot; feel free to unsubscribe.

If you haven't already, you should update your TagBot.yml to include issue comment triggers.
Please see this post on Discourse for instructions and more details.

If you'd like for me to do this for you, comment TagBot fix on this issue.
I'll open a PR within a few hours, please be patient!

Currently, only a handful of data types are implemented directly in Supposition.jl. This feature intends to use the reflection capabilities provided by the compiler to generate (almost) any arbitrary T from its type.

This needs to:

• Account for throwing constructors
• Recurse for any required arguments
• Inspect which methods are actually constructor functions
  • Filter out the default constructor that just calls convert on every argument, since that would lead to quite a lot of avoidable errors
  • Currently, my thinking is that this can be done by inspecting code_typed, rejecting methods that infer as Union{} (these will throw) and only considering those that have an Expr(:new) in themselves. The reasoning for this is that any outer constructors that may want to establish invariants through checks like x < 5 || throw(ArgumentError()) are trivially circumventable by just calling the inner constructor directly (either with arguments that happen to dispatch to the inner one, or through invoke).
• Allow overriding through user defined dispatches
  • We have multiple dispatch, so allow users to hook into this at their own risk.

Shrinking-wise, this should just fall back to lexicographic shrinking, but this too should again be customizable. It may be the case that a user is fine with having the full space of possible values emerge from this Possibility, but only cares about shrinking them in a specific way.

What happened?

julia> Supposition.@check function checkassociativeinstance(a::Data.Floats(),b::Data.Floats(),c::Data.Floats())
       (a + b) + c == a + (b + c)
       end
ERROR: LoadError: ArgumentError: An argument doesn't have a generator set!
in expression starting at REPL[13]:1

How could this be communicated better?

It says "An argument doesn't have a generator set!" but

• I don't know what a generator set is
• Why is it yelling at me (with a !)

Julia Version

julia> versioninfo()
Julia Version 1.10.0
Commit 3120989f39b (2023-12-25 18:01 UTC)
Build Info:
  Official https://julialang.org/ release
Platform Info:
  OS: Linux (x86_64-linux-gnu)
  CPU: 24 × AMD Ryzen 9 3900XT 12-Core Processor
  WORD_SIZE: 64
  LIBM: libopenlibm
  LLVM: libLLVM-15.0.7 (ORCJIT, znver2)
  Threads: 17 on 24 virtual cores
Environment:
  JULIA_NUM_THREADS = 12

Package Environment

(@main) pkg> st Supposition
Status `~/.julia/environments/main/Project.toml`
  [5a0628fe] Supposition v0.3.1

Currently, this is done through a global variable:

This should simply be moved into CheckConfig. At the same time, this can be safely increased to something like 100_000.

gen_f = @composed function f(x=Data.Floats{Float64}())
  x
end

Here we give two different names f and gen_f. What is the benefit of separating them out like this? Why not just use f?

Currently, each @check invocation needs its own set of configuration options passed, even when a lot of tests should use the same settings. This can be seen in our own testsuite:

where every invocation of @check has verbose=verb passed.

This feature would:

• Provide a way to pass a CheckConfig directly to @check
  • Invocations like @check verbose=true config=my_config ... would prioritize explicitly passed-in options, but otherwise default to whatever my_config specifies.
• Provide a way to change the defaults for an entire block of code, without having to pass a CheckConfig to every @check individually
  • This can be done with a ScopedValue; since we already rely on them for CURRENT_TESTCASE, this won't have an impact on compat.

The place to modify for adding the config keyword to the macro is here:

which is also where loading from an existing global default would occur.

Currently, the printing of all of these subtypes is very excessive. Implementing the 3-arg Base.show(::IO, ::MIME"text/plain", obj) on a per-Possibility-basis is needed for this to be better, and can be done incrementally.

Possibility without a dedicated show method, at the time of writing:

• Composed
• Data.AsciiCharacters
• Data.Bind
• Data.Booleans
• Data.Characters
• Data.Dicts
• Data.Floats
• Data.Integers
• Data.Just
• Data.Map
• Data.OneOf
• Data.Pairs
• Data.Recursive
• Data.SampledFrom
• Data.Satisfying
• Data.Text
• Data.Vectors
• Data.WeightedNumbers
• Data.WeightedSample

It should be either documented or not mentioned.

help?> Data.Recursive
  Recursive(base::Possibility, extend; max_layers::Int=5) <: Possibility{T}


  A Possibility for generating recursive data structures. base is the basecase of the recursion. extend is a function
  returning a new Possibility when given a Possibility, called to recursively expand a tree starting from base.

  max_layers designates the maximum number of times extend will be used to wrap base in new layers. This must be at least 1,
  so that at least the base case can always be generated.

  Examples
  ========

  julia> base = Data.Integers{UInt8}()
  
  julia> wrap(pos) = Data.Vectors(pos; min_size=2, max_size=3)
  
  julia> rec = Data.recursive(wrap, base; max_layers=3);

help?> Data.recursive
  No documentation found.

  Supposition.Data.recursive is a Function.

What happened?

julia> Supposition.@check checkassociativeinstance(a,b,c) = (a + b) + c == a + (b + c)
ERROR: LoadError: ArgumentError: Given expression is not a function call or definition!
in expression starting at REPL[2]:1

How could this be communicated better?

It says it's not a function definition but it is one, so it shouldn't say that it isn't.

Julia Version

julia> versioninfo()
Julia Version 1.10.0
Commit 3120989f39b (2023-12-25 18:01 UTC)
Build Info:
  Official https://julialang.org/ release
Platform Info:
  OS: Linux (x86_64-linux-gnu)
  CPU: 24 × AMD Ryzen 9 3900XT 12-Core Processor
  WORD_SIZE: 64
  LIBM: libopenlibm
  LLVM: libLLVM-15.0.7 (ORCJIT, znver2)
  Threads: 17 on 24 virtual cores
Environment:
  JULIA_NUM_THREADS = 12

Package Environment

(@main) pkg> st Supposition
Status `~/.julia/environments/main/Project.toml`
  [5a0628fe] Supposition v0.3.1

My pet peeve about hypothesis.py is that it uses the plural booleans() to generate a single boolean. I think it is easier to understand that a single draw from a generator generates one instance of the thing. For example

function f(ints)
  sum(ints)
end

f takes a thing called ints which is supposed to be passed a sequence of integers. But Data.Integers() will pass it a single integer. I think this is confusing and it would be easier to understand if the way to generate one integer were Integer() and, if needed, a shortcut to generate multiple integers were Integers().

A counterargument is that it's more natural for map and filter to work on things that are named pural.

There are supposed to be more spaces after Test Summary:.

using Test
julia> @testset "trigonometric identities" begin
           θ = 2/3*π
           @test sin(-θ) ≈ -sin(θ)
           @test cos(-θ) ≈ cos(θ)
           @test sin(2θ) ≈ 2*sin(θ)*cos(θ)
           @test cos(2θ) ≈ cos(θ)^2 - sin(θ)^2
       end;
Test Summary:            | Pass  Total  Time
trigonometric identities |    4      4  0.1s

julia> Supposition.@check function increasing_function_is_increasing(f=increasing_functions, xs=Data.Vectors(Data.Floats{Float64}(nans=false)))
           xs = sort(xs)
           ys = map(f, xs)
           issorted(ys)
       end
Test Summary: | Pass  Total  Time
increasing_function_is_increasing |    1      1  0.3s

https://docs.julialang.org/en/v1/manual/style-guide/#bang-convention gives the convention

Append ! to names of functions that modify their arguments

Since assume!(::Bool) doesn't modify its arguments I suspect it should be assume(::Bool).

What happened?

Running @check in a project that has a test directory but not a SuppositionDB directory leads to a SystemError:

[sukera@tower Supposition.jl]$ ls
CONTRIBUTING.md  docs  LICENSE  Manifest.toml  Project.toml  README.md  src  test
[sukera@tower Supposition.jl]$ ls test/
Project.toml  runtests.jl
[sukera@tower Supposition.jl]$ julia -q --project=.
julia> using Supposition

julia> @check function doubleError(i=Data.Integers{UInt}())
           i > 10 && error("10")
           error("<")
       end;
┌ Warning: Encountered an error, but it was different from the previously seen one - Ignoring!
│   Error = <
│   Location = doubleError(i::UInt64) at REPL[2]:3
└ @ Supposition ~/Documents/projects/Supposition.jl/src/teststate.jl:111
┌ Error: Property errored!
│   Description = "doubleError"
│   Example = (i = 0x000000000000000b,)
│   exception =
│    10
│    Stacktrace:
│     [1] error(s::String)
│       @ Base ./error.jl:35
│     [2] doubleError(i::UInt64)
│       @ Main ./REPL[2]:2
└ @ Supposition ~/Documents/projects/Supposition.jl/src/testset.jl:275
ERROR: SystemError: opening file "/home/sukera/Documents/projects/Supposition.jl/test/SuppositionDB/doubleError(UInt64)_doubleError": No such file or directory
Stacktrace:
  [1] systemerror(p::String, errno::Int32; extrainfo::Nothing)
    @ Base ./error.jl:176
  [2] systemerror
    @ ./error.jl:175 [inlined]
  [3] open(fname::String; lock::Bool, read::Nothing, write::Nothing, create::Nothing, truncate::Bool, append::Nothing)
    @ Base ./iostream.jl:295
  [4] open
    @ ./iostream.jl:277 [inlined]
  [5] open(fname::String, mode::String; lock::Bool)
    @ Base ./iostream.jl:358
  [6] open(fname::String, mode::String)
    @ Base ./iostream.jl:357
  [7] open(::Serialization.var"#1#2"{Supposition.Attempt}, ::String, ::Vararg{String}; kwargs::@Kwargs{})
    @ Base ./io.jl:406
  [8] open
    @ ./io.jl:405 [inlined]
  [9] serialize
    @ ~/julia/usr/share/julia/stdlib/v1.12/Serialization/src/Serialization.jl:818 [inlined]
 [10] record!
    @ ~/Documents/projects/Supposition.jl/src/history.jl:32 [inlined]
 [11] finish(sr::Supposition.SuppositionReport)
    @ Supposition ~/Documents/projects/Supposition.jl/src/testset.jl:249
 [12] top-level scope
    @ ~/Documents/projects/Supposition.jl/src/api.jl:279
 [13] macro expansion
    @ ~/julia/usr/share/julia/stdlib/v1.12/Test/src/Test.jl:180 [inlined]

What did you expect to happen?

When the test is finished, the found failure should be recorded in the given DB, if any has been given.

Julia Version

julia> versioninfo()
Julia Version 1.12.0-DEV.186
Commit 11c54a62be (2024-03-14 14:30 UTC)
Platform Info:
  OS: Linux (x86_64-pc-linux-gnu)
  CPU: 24 × AMD Ryzen 9 7900X 12-Core Processor
  WORD_SIZE: 64
  LLVM: libLLVM-16.0.6 (ORCJIT, znver4)
Threads: 23 default, 1 interactive, 11 GC (on 24 virtual cores)
Environment:
  JULIA_PKG_USE_CLI_GIT = true

Package Environment

This is with version `v0.2.0`, commit `fc14aec`.

help?> (Supposition.Data)
  No docstring or readme file found for module Supposition.Data.

  Module does not export any names.

It would be helpful to show what's available to generate.

It may be beneficial to track more than one good attempt, which can be attempted to be improved independently from other good-ish attempts. See e.g. IJON: Exploring Deep State Spaces via Fuzzing, which implements a form of coverage based fuzzing through multiple (user annotated) targets, allowing their fuzzer to beat Level 3-4 of the first Super Mario Bros.:

(theirs is the one at the bottom, while the one at the top struggles with the large state space).

This feature would:

• Extend the number of tracked targets from 1 to (just throwing out a number here) 256
  • These would be exposed as a second argument specifying the slot to store the score in; the default would be slot 1.
• Make target optimization smarter by choosing amongst the tracked targets which would be a good case for further expansion, again trying to maximize its score
• Rework how was_better is calculated, since tracking more than one target means the calculation whether any given example actually was better becomes more complicated.
  • Perhaps this can be done by allowing a custom overall scoring function, given the calculated scores?
  • If none is given, this could default to prioritizing the first slot over the second etc. Receiving a custom function for deciding whether the example was better than the last allows users to decide that they want to ignore e.g. slot 33 in almost all cases, except when slot 40 is >500, for example.
  • Allowing a custom function should not be required to consider this feature implemented, and can be done at a later time. This should simplify a first implementation quite a bit, since we can postpone thoughts on how to expose this information to a user.

Currently, all shrinking is done naively & directly on the choice sequence (see here). This is neither customizable, nor anywhere close to optimal (and not at all how Hypothesis proper does it).

The plan for this is the following:

• Implement region tracking on a per-Possibility basis, preferrably automatically tracking which Possibility we're currently in
• Implement region shrinking, giving information about what the region represents
• Expose an interface for hooking into shrinking on a per-Possibility basis

My current idea is to follow what Hypothesis does about half way, informing how the regions are tracked. A custom shrinker would be given access to the part of the choice sequence it's responsible for, having it return a newly modified choice sequence as a replacement. It may be necessary to rework the interface surrounding Possibility a bit to do so - e.g. proptest returns a ValueTree when producing elements, similar to what PropCheck/Hedgehog do (except smarter when it comes to laziness of shrunk values).

Currently, Overrun is simply caught and marked as a regular rejection, but it would be better to report to the user that an Overrun occurred. This way, a user is informed that their exploration exhausts the maximum number of choices per TestCase and that they should consider either increasing the memory limit through the configuration, or limit their maximum sizes so the choices taken in their particular implementation don't hit the overrun limits anymore.

Which part of the documentation is this related to?

https://seelengrab.github.io/Supposition.jl/dev/interfaces.html
https://seelengrab.github.io/Supposition.jl/dev/api.html

How could this be communicated better?

I don't like a design where there's an "API" that's not supported. If you want to document internals, that's great, but imho it belongs on a devdocs/internals page, not on the same page with the public Data stuff.

Currently it's something like

• Public macros and functions
• Public Data generators and internals

I suggest

• Public macros and functions
• Public Data generators
• Devdocs/Internals

This is currently not supported since the data model is not rich enough to provide good shrinks (without rejecting too many test cases), but would be very nice to have. This would mostly copy what Hypothesis is doing here, which might require #3 so that the generated values continue to shrink well.

The workaround for now is to use assume! in user code involving Data.Floats to reject any unwanted samples.

Currently, the way to do stateful fuzzing is very ad-hoc and relies on good problem modeling skills to generate good sequences of operations.

This feature should:

• Manage the state required for the fuzzing automatically (e.g. by grouping them all into a mutable struct which is modified by the various operations one can do)
• Allow the specification of transition rules from one state to the next, allowing (almost) arbitrary modifications to the declared state.
• Allow specifying preconditions on a per-rule basis, so that these are checked before any given transition is attempted.
• Allow specifying additional invariants/postconditions on the state that must be upheld after every (or perhaps even just some?) operation.
• Provide good printing of the ensuing result, clearly showing the sequence of actions taken to find the minimal counterexample.
• Ideally, this would also have a configuration option to allow operations to run in parallel, which would allow users to fuzz their datastructures for race conditions (if they violate an invariant in parallel fuzzing mode, they have a race condition).
  • This is quite a bit more tricky than it may seem at first, since shrinking may rely on very precise scheduling decisions of the Julia scheduler. An initial implementation can either omit this point entirely or just abort completely and report the found stream of (task, action_taken, time) in some form.

Printing the results of a SuppositionReport is currently pretty ugly and relies on Logging:

It would be great to implement fancier printing here using StyledStrings.jl once it becomes available/registered.

The printing should:

• On a Pass
  • Show which property passed
  • Show the best score any example achieved, if available
  • If broken=true, ensure that this is communicated as a failure (which it's also reported as to the parent AbstractTestSet)
• On a Fail
  • Clearly communicate when a property didn't hold
  • Clearly show the minimal found inputs that made the property fail
• On a Error
  • Show the entire error that occurred
  • Show the stacktrace from the point of the property, up to the point where the error was thrown
  • Show the minimal example that lead to the error
  • Show how many different errors (if any) were encountered)
    • This will require a bit of additional tracking data, so can be done later too

After getting annoyed by all the fiddly details when testing with normal floats, I wanted to to try testing a claim using BigFloat. But Data.Floats{BigFloat}() doesn't work.

julia> Data.Floats{BigFloat}()
ERROR: TypeError: in Floats, in T, expected T<:Union{Float16, Float32, Float64}, got Type{BigFloat}

Currently, @composed requires passing an Expr(:function:

foo = @composed function bar(a=..., b=...)
   ... use a & b ...
end

This can be very cumbersome & unwieldy, since users have to always think of new names for things they're only seldom going to invoke manually.

This would be better served by allowing syntax like

foo = @composed (a=..., b=...) -> (.. use a & b ...)

In addition, it would also be good to allow using existing functions as well:

foo = @composed build_foo(f=..., g=...)

This needs to be done here:

in a similar manner to how the internals of @check have been split. While we're at it, it would be good to also support anonymous function syntax for @check. Of course, using anonymous function syntax comes with the caveat that it's more difficult to call the property manually. One other potential issue with this is that currently, the macro relies heavily on there being some name attached to the callable that we can use to refer to the function, which doesn't exist at parse time for anonymous functions.