First attempt at a Supposition.jl-based test

[bvrb]

Started during the Hackathon at JuliaCon Paris under the guidance of @Kolaru, here is my first attempt at adding a test using Supposition.jl (c.p. #733).
To start simple, the goal was to convert an existing test with a hardcoded numerical value to one using randomly generated values from Supposition.jl instead.
For no particular reason, we picked

IntervalArithmetic.jl/test/interval_tests/numeric.jl

Line 175 in 544c000

@test isequal_interval(interval(1//9), interval(1//9, 1//9))

which tests that for a degenerate interval with equal start and endpoints of type Rational, both the one and two argument syntax yield the same interval.

There were a few unforeseen complications, which I tried my best to find a solution for:

1. Generation of Rationals

• As there is no ready-made Rational generator in Supposition.jl, after consulting @Seelengrab I opted to create a simple custom one, where both numerator and denominator are randomly drawn Ints, and the case 0//0 is explicitly thrown out as an invalid test case.
• Interesting edge cases are given by 1//0 and -1//0 (corresponding Inf/-Inf), which will yield an ill-formed interval (see also isempty_interval return false on empty ill intervals #734). However, similar to the discussion in How to automatically find counterexample Seelengrab/Supposition.jl#62 (comment), it is unlikely that a 0 is generated in the denominator for an Int64, so I had to use an Int8 generator instead. As an alternative, one might instead add these cases explicitly to the regular tests.
• There was another problem which took some time to track down, where sometimes an OverflowError would appear, especially when using Int8. The issue can be reproduced by

julia> num = Int8(3) # or any Int8 !=0 which is not a divisor of typemin(Int8)
3

julia> den = typemin(Int8)
-128

julia> num//den
ERROR: OverflowError: 0 - -128 overflowed for type Int8
Stacktrace:
[1] throw_overflowerr_binaryop(op::Symbol, x::Int8, y::Int8)
 @ Base.Checked .\checked.jl:163
[2] checked_sub
 @ .\checked.jl:232 [inlined]
[3] checked_neg
 @ .\checked.jl:95 [inlined]
[4] checked_den
 @ .\rational.jl:22 [inlined]
[5] Rational
 @ .\rational.jl:44 [inlined]
[6] Rational
 @ .\rational.jl:48 [inlined]
[7] //(n::Int8, d::Int8)
 @ Base .\rational.jl:84
[8] top-level scope
 @ REPL[66]:1

So I believe that upon construction of a Rational resulting in an overall negative value, a minus sign in the denominator is transferred to the numerator instead, and the sign of the former is flipped. However, if that value happens to be typemin(Int8), there will be an overflow, since typemax(Int8)==127. To address this, I instead added 1 to the minimum value of the Int generator. Does that seem reasonable?

2. 1//0 and -1//0 & Ill-formed intervals

• The equality test failed whenever the result was an empty, ill-formed interval. As far as I understand the discussion in isempty_interval return false on empty ill intervals #734, this is the way it is supposed to be, as the behavior is similar to a NaN, and any Boolean comparison will yield false.
• For the purpose of the test, I therefore excluded those cases where the decorator is ill.

Also, it might make sense to fix the random seed for reproducibility reasons, but I am not sure if this would go against the spirit of this fuzzing-based approach, which I am not too familiar with.

I apologize for the wall of text for this (at least in theory) rather simple addition, and would appreciate any feedback!

[Seelengrab]

Thanks for the ping! Some notes - in principle fuzzing with just a pair of Int8 is fine of course, but with the default setting of max_examples=10_000 it's a bit wasteful :) There are only 2^8*2^8 = 2^16 distinct input pairs for Int8, which can just as well be covered with a for-loop over all of those inputs. On my machine, a loop printing all of them runs in ~0.5s, so I'd imagine that not printing them & doing some interval math could be faster, even while covering the entire input space (and thus not requiring the entire weight of Supposition.jl!). If your goal is to cover non-edge cases, there is no harm in running @check with e.g. max_examples=1_000 and Int inputs occasionally, should the test prove too costly for regular CI.

Since this is something that comes up from time to time, I'll probably have to think about adding something that triggers these known edge cases for integers earlier 🤔 Another idea might be to add a constructor with minimum/maximum to Data.BitIntegers, which would behave like Data.Floats in that it can produce any bitinteger type from Base from that range (currently, it only has an "all or nothing" constructor). But that's a bit off-topic for this PR, and is something I'll have to take with me 😄

Another thought - is there maybe some transform you can do to create a valid Interval from an illformed one? I'm not familiar with the domain so I'm not sure that this is applicable, it's just generally a good strategy to assume!/reject! as little as possible and try to construct valid inputs for the property only, since this is usually going to be less expensive overall. Avoiding typemin(Int8) by simply adding 1 to the lowerbound is an example for this kind of transform, so are there maybe others for the remaining assume!? Perhaps you could change the property to say that either the intervals are equal, or they must both be illformed (i.e. xor(isequal_interval(x,y), x == ill && y == ill))?

Other than that, this looks like an example of a "Different Paths, Same Destination"-style property test, where you test that two different constructors behave the same for inputs that they should be invariant under - nice!

[OlivierHnt]

Thank @bvrb for opening this PR. This is very interesting, I was not aware of Supposition.jl.
So just glancing at the changes, this is for intervals with Rational bound type? So that every time you run the CI a new value is generated and tried?

Could this be done for floats as well?

[Kolaru]

Thanks very much for the efforts! Except for my two small comments, it looks good to me.

I think it is great to have the general layout of those Suppositions.jl test figure out for the future.

If you'd be willing to add them, I do agree with Olivier that it would be nice to have the same consistency tests for floating point number :)

More advance tests can wait, and we'll need to be somewhat smart to have meaningful ones.

[Kolaru]

These two last lines could be replaced by

x === y

which correctly handles ill formed intervals.

[bvrb]

Thanks! Changed it accordingly.

[Kolaru]

Does this still let the tests run with any integer type, or only Int8?

[Seelengrab]

Data.Integers currently enforces that either you specify the type explicitly like Data.Integers{Int64}, or the types of the two arguments have to match & are what is produced in the end. So as written, this will only produce Int8.

There is a Data.BitIntegers which produces any integer type (except BigInt), but that one doesn't have a lowerbound/upperbound based constructor yet.. The semantics are a bit weird there, because I need to decide what to do if a generated value doesn't fit into the chosen output type...

[bvrb]

Per the discussion above, I now changed this to a regular Int, which is probably the most commonly used type to construct a Rational anyway. This will now however not always trigger the 1//0 and -1//0 edge cases because the input space is much larger, so I instead added a few tests in the construction.jl file, which essentially mirror the already existing tests for Inf/-Inf. Is this ok?

I tried playing around with Data.BitIntegers, but then I also ran into problems when numerator and denominator were of different Signed or Unsigned types when creating the Rational, and this felt more like a separate issue not necessarily to be tackled here.

[bvrb]

Thank you all for the helpful comments and feedback!

@Seelengrab This makes complete sense, and I tried to incorporate most of it. So the way I understand it, the core role of Supposition.jl is to randomly sample a large input space, where edge cases like 0 might or might not be triggered, so these should ideally be tested separately anyway?

I do believe it would be useful to have some sort of cherry picking with regards to the common edge cases, but I imagine it is rather difficult to decide what is "common" and what isn't. Although in the Integers case, including 0 and 1 as the neutral elements wrt. to addition and multiplication probably wouldn't hurt. I have some more questions/thoughts about this, but it's probably better to open a discussion over at Supposition.jl instead as you suggested :)

[bvrb]

@OlivierHnt Thanks! Indeed, Supposition.jl generates random inputs for testing to cover more of the input space, and actually creates several random values at once every time CI is run - as per @Seelengrab's suggestion I have decreased the max_examples parameter as it might be a bit wasteful otherwise.

I think we initially decided to go with a test for Rational type numbers as we didn't want to worry about floating point precision of the randomly generated numbers, but for this particular test this is not really a problem. I have now added another test for the same property that uses randomly generated Float inputs.