1

In a previous question I was asking for help writing a predicate to find if a number is a power of 2. This was a prelude to trying to prove the following C function:

static inline bool
is_power_of_2 (unsigned long v)
{
  return v && ((v & (v - 1)) == 0);
}

(This "trick" comes from here). Using the previous predicate I tried:

/*@
  ensures positive_power_of_2 (v) <==> \result == \true;
 */

but none of the various SMT solvers I'm using (alt-ergo, z3, gappa, cvc4) seem able to prove this.

Rich
  • 926
  • 1
  • 9
  • 17
  • 1
    The reason why SMT solvers can't prove it directly is that you need some kind of reasoning by induction to prove this, and SMT solvers are bad at this kind of task. I brievly tried two ways to prove this property. First using a lemma function, where the idea is to write the naive function and to prove that on each return both sides of the equivalence hold (or not) according to the return value, but it is not that easy to write properties about bits that are well handled by SMT solvers. The second by directly proving it as a lemma using Coq, which is to be feasible, but a bit time consuming. – Ksass'Peuk Oct 15 '20 at 11:33
  • Thanks - very interesting answer. I think if you posted it as an answer I'd "accept" it :-) The purpose of this is trying to research what SMT solvers can and cannot do. – Rich Oct 17 '20 at 09:06

0 Answers0