jlink
bound5 challenge
I am reading the description of the bound5 challenge and there are various items that require some discussion.
The current description reads:
Given a 5-tuple of lists of 16-bit integers, ...
Let's start with this part. I read -and still do- this part as "Construct/consider 5 random lists of 16-bit integers (i.e., integers in the range -32768..32767) and put them in a tuple." Is my reading correct?
... we want to test the property that if each list sums to less than 256, then the sum of all the values in the lists is less than 5 * 256. ...
The next part in the phrasing talks (to my reading) about a property with a precondition: for all 5-tuples that satisfy the precondition that all of the elements of their five lists sum to less than 256, check that the sum of their values is less than 5 * 256. This seems a very challenging property alright, but challenging for random generation -- not for shrinking! It is highly unlikely that random generation can come up with five random lists of 16-bit integers that their (random) elements sum to less than 256.
So, this challenge basically requires one to write a hacked generator, doesn't it? Also, if one starts with hacked generators, why would these have to be lists in the first place? Wouldn't five random 16-bit integers suffice as elements of the tuple? (The current "solutions" seem to agree with this, as far as I can see.)
... This is false because of overflow. e.g. ([-20000], [-20000], [], [], []) is a counter-example.
This last sentence above is more problematic, IMO. If I understand it correctly, it requires a language that supports addition of 16-bit integers (with the result being also 16 bits) in two's complement, and not all languages have such a type or support that natively. (For example, Erlang has only infinite precision integers.)
Anyway, bottomline:
Besides fixing the phrasing to make it more clear what this problem is about, is this a general enough challenge?
Hypothesis' and jqwik's generated are hacked in that only lists that sum to less than 256 are being generated in the first place.
As for the the 16 bit two's complement part, I think you are right. The language needs such a type or you have to create a type with the same overflow semantics. Whether that is a reasonable thing to do in Erlang I'm not qualified to judge.
IMO, not every library must or should implement each "challenge". If a challenge does not make sense in a given context it shouldn't be tackled.
Hypothesis' and jqwik's generated are hacked in that only lists that sum to less than 256 are being generated in the first place.
Hmm... for Hypothesis, this is only half the truth, isn't it? If I understand this line correctly, the Hypothesis generator only generates lists of size (edit: at most) 1, which IMO completely defeats the intention of this challenge. (Hence my comment in the first post of this issue about having five 16-bit integers instead of lists of integers).
Also, jqwik currently normalizes this example to [[], [], [], [], [-1, -32768]] which, again if I understand the phrasing of the challenge alright, is a counter-example that would never be generated by the hacked generator and thus would never be considered because it fails to satisfy the precondition that the challenge mentions ("if each list sums to less than 256"). Or is my 16-bit two's complement arithmetic in my head wrong?
Anyway, the main point I am trying to make is that we should be extra-clear on what each challenge is about (its intention and expected results) and how it is intended/allowed to be implemented. Otherwise, a big part of the value of the challenge is (IMO) bound to be "lost in translation".
Hmm... for Hypothesis, this is only half the truth, isn't it? If I understand this line correctly, the Hypothesis generator only generates lists of size 1, which IMO completely defeats the intention of this challenge. (Hence my comment in the first post of this issue about having five 16-bit integers instead of lists of integers).
You obviously look with more scrutiny than I do :-/
Also, jqwik currently normalizes this example to
[[], [], [], [], [-1, -32768]]which, again if I understand the phrasing of the challenge alright, is a counter-example that would never be generated by the hacked generator and thus would never be considered because it fails to satisfy the precondition that the challenge mentions ("if each list sums to less than 256"). Or is my 16-bit two's complement arithmetic in my head wrong?
Makes me wonder how that can happen. Will have a look.
Anyway, the main point I am trying to make is that we should be extra-clear on what each challenge is about (its intention and expected results) and how it is intended/allowed to be implemented. Otherwise, a big part of the value of the challenge is (IMO) bound to be "lost in translation".
Yes. The texts are even more ambiguous than I already thought they were.
Here's an emulation of 16bit overflow logic in a language that doesn't have it, inspired by https://www.mathworks.com/matlabcentral/answers/355611-is-there-a-way-to-do-signed-16-bit-integer-math
challengeBound5 : Test
challengeBound5 =
let
bits =
16
max =
2 ^ bits
maxHalf =
max // 2
i16 : Int -> Int
i16 n =
((n + maxHalf) |> modBy max) - maxHalf
i16Add : Int -> Int -> Int
i16Add a b =
i16 (a + b)
i16Sum : List Int -> Int
i16Sum ns =
List.foldl i16Add 0 ns
boundedList : Fuzzer (List Int)
boundedList =
F.listWith
{ minLength = Nothing
, maxLength = Just 1
, customAverageLength = Nothing
}
(F.int -32768 32767)
|> F.filter (\list -> i16Sum list < 256)
tuple5 : Fuzzer ( List Int, List Int, ( List Int, List Int, List Int ) )
tuple5 =
F.tuple3
boundedList
boundedList
(F.tuple3
boundedList
boundedList
boundedList
)
in
testMinithesis "Bound 5"
tuple5
(\( a, b, ( c, d, e ) ) -> i16Sum (List.fastConcat [ a, b, c, d, e ]) < 5 * 256)
(FailsWith ( [ -31488 ], [ -32768 ], ( [], [], [] ) ))
Hmm... for Hypothesis, this is only half the truth, isn't it? If I understand this line correctly, the Hypothesis generator only generates lists of size (edit: at most) 1, which IMO completely defeats the intention of this challenge. (Hence my comment in the first post of this issue about having five 16-bit integers instead of lists of integers).
Huh. I wonder why that's there - I think this is a mistake rather than a deliberate feature of the Hypothesis implementation. I'll fix it.
Also, jqwik currently normalizes this example to
[[], [], [], [], [-1, -32768]]which, again if I understand the phrasing of the challenge alright, is a counter-example that would never be generated by the hacked generator and thus would never be considered because it fails to satisfy the precondition that the challenge mentions ("if each list sums to less than 256"). Or is my 16-bit two's complement arithmetic in my head wrong?
I implemented the sum of shorts wrong in one of the two places :-(
After fixing it the shrunk samples are much less uniform than before:
[[], [], [], [-1], [1, 32767]] (34.00%)
[[], [], [], [-1], [-32768]] (13.00%)
[[], [], [], [1, 32767], [1281, 32767]] (2.00%)
[[], [], [], [-16060], [-16709]] (1.00%)
[[], [], [], [-2767], [-30002]] (1.00%)
[[], [], [], [-12425], [-20344]] (1.00%)
[[], [], [], [-15864], [-16905]] (1.00%)
[[], [], [], [-2], [-32767]] (1.00%)
[[], [], [], [-13117], [-19652]] (1.00%)
[[], [], [], [-15691], [-17078]] (1.00%)
Only 13 from 100 produce the arguably "smallest" sample.