--- layout: fc_discuss_archives title: Message 61 from Frama-C-discuss on November 2013 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] math vs. bits



On 08/11/2013 05:02, John Regehr wrote:

> BTW I cannot get the function below to verify, even though it does not
> have the bitwise or.  Perhaps the division is causing problems?

I took a look the proof obligations generated by Jessie and it is not 
the division that causes a problem (at least not yet). The issue is the 
way modulo arithmetic is encoded. While sufficient to prove your 
function, it is basically unusable. Indeed, modulo is defined in a 
subtractive way rather than by using the modulo operator.

As a consequence, it is impossible to directly deduce anything about (x 
<< 31) due to the combinatorial explosion (about four billion of 
billions of proof steps, if I did not get it wrong). The only sane way 
is to first prove that this subtractive modulo is in fact the 
traditional multiplicative modulo.

So my guess is: it worked for a left rotation by 1, it should have 
worked for a rotation by 2, it might have failed for a rotation by 3, it 
will definitely fail for any larger rotation (e.g. 31 in your case).

> Is there some way I can provide a bit of additional information here so
> these and the n-bit rotate functions verify, or am I stuck with an
> interactive proof assistant?

You are stuck with an interactive proof assistant, I guess. And even 
then it will be uglier than it should be. At this point, I think it is 
not reasonable to verify this kind of programs until a more adequate 
specification of modulo arithmetic is implemented in the tools.

Best regards,

Guillaume