On Monday, 25 April 2016 at 12:56:27 UTC, Andrei Alexandrescu
wrote:
...
That's smaller and faster, thanks. But how do you show it is
still correct? -- Andrei
First I wrote the following variants of isPow2A. It's more
obvious that they're correct, but they didn't compile to fewer
instructions.
bool isPow2D(T)(T x)
{
return (x > 0) && !(x & (x - 1));
}
(The variant isPow2E avoids a jump instruction:)
bool isPow2E(T)(T x)
{
return (x > 0) & !(x & (x - 1));
}
So at least I had some functions that I knew were doing what I
wanted (handling negative values for sure) to test against.
Then I tried some other things that didn't work, then the bit
shift variant, isPow2F. It seemed to work, I looked at at long
list of results in the terminal and saw what the pattern is, but
right, I shouldn't trust it without a proof.
(x & -x) evaluates to the value of the lowest bit set in x.
Either (x & -x) == x, which is a power of 2, or (x & -x) == x
minus the value of all the bits above the lowest bit set.
(x >>> 1) is equal to half of x or one less than half of x, or a
positive number if x is negative.
For (x & -x) > (x >>> 1) to be true, that would either be because
x is a power of 2, or else x - n > x/2 - 1 (or x - n > x/2, which
is implied by that) where n is the value of the bits above the
lowest bit set, which means n >= 2/3*x. So x - n > x/2 - 1 would
be 1/3*x > x/2 - 1, which would be 0 > 1/6*x - 1. That's
impossible for x > 6. For values of x under 6, the results check
out case by case.
When x is negative in a signed type, the unsigned shift treats x
as if it were an unsigned number. The only particular bit
arrangement that's treated differently when using a signed type
is that -(2^^32) isn't a power of two because it's negative, so
the expression (x & -x) should evaluate to a negative value
before the comparison.
That seems to work for a byte or a short, where (x & -x) comes
out negative when at the min value.
I've written this clumsily because I'm not sure what sort of
symbols to use and don't know how to write mathematical proofs
for algorithms in programming in general, but I thought it was
interesting that writing it down and double checking required
showing how close the algorithm cuts it.
For example, x = 6144, (x & -x) == 2048, (x >>> 1) == 3072.
The cases for 0 to 6, when using signed types for x:
algo B algo F
x 0 B true F false (x & -x) == 0, (x >>> 1) == 0
x 1 B true F true (x & -x) == 1, (x >>> 1) == 0
x 2 B true F true (x & -x) == 2, (x >>> 1) == 1
x 3 B false F false (x & -x) == 1, (x >>> 1) == 1
x 4 B true F true (x & -x) == 4, (x >>> 1) == 2
x 5 B false F false (x & -x) == 1, (x >>> 1) == 2
x 6 B false F false (x & -x) == 2, (x >>> 1) == 3
