Checking if an Integer is an Exact Binary Power

[Solomon E via Digitalmars-d]

On Monday, 25 April 2016 at 15:27:02 UTC, Xinok wrote:
> On Monday, 25 April 2016 at 12:56:27 UTC, Andrei Alexandrescu 
> wrote:
>> On 4/25/16 6:42 AM, Solomon E wrote:
>>> ...
>>> I generalized function isPow2B to work for negative numbers 
>>> in case of a
>>> signed type, while keeping the assembly the same or better. 
>>> ...
>>>> [...]
>>>
>>> bool isPow2F(T)(T x)
>>> {
>>>      return (x & -x) > (x >>> 1);
>>> }
>>>
>>> ...
>>
>> That's smaller and faster, thanks. But how do you show it is 
>> still correct? -- Andrei
>
> Brute force.
>
> http://dpaste.dzfl.pl/882d7cdc5f74


Brute force? That doesn't prove the algorithm, it only proves the 
implementation.