Checking if an Integer is an Exact Binary Power

[Solomon E via Digitalmars-d]

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