Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[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