Lost in translation (with SPARK user rules)

["Yannick Duchêne (Hibou57)" <yannick_duchene@yahoo.fr>]

Lost in translation... do you know the movie ?

No, I'm joking, this is not about this 2002 movie, that's about SPARK, and  
exactly, about translating some expressions in the rules language.

Previously, I have successfully added these rules, in an *.RLU file:

    inequals(122):  X/Y<1     may_be_deduced_from [ X>=0, Y>0, Y>X ].
    inequals(123):  X/Y<1     may_be_deduced_from [ X<=0, Y<0, Y<X ].
    inequals(124):  X/Y>(-1)  may_be_deduced_from [ X>=0, Y<0, (-Y)>X ].
    inequals(125):  X/Y>(-1)  may_be_deduced_from [ X<=0, Y>0, Y>(-X) ].


I wanted to do the same, for another kind of rule, about bitwise. The rule  
I wanted to add is something like:
(X and 2 ** N) = 0 may be deduced from ((X / (2 ** N)) and 1) = 0
and the opposite

I tried with this:

    bitwise(112): bit__and(X div (2**N), 1)=0 may_be_deduced_from [  
(bit__and(X, 2**N)=0), X>=0, N>=0 ].
    bitwise(113): bit__and(X, 2**N)=0 may_be_deduced_from [ (bit__and(X div  
(2**N), 1)=0), X>=0, N>=0 ].

But this fails, although the simplifier does not returns me any syntax  
error messages about this *.RLU file. This fails, because it cannot prove  
something like this:

    --# check ((Instance and 2) = 0) -> (((Instance / 2) and 1) = 0);

The latter should be directly deduced from the two previous rules if these  
were OK. So I suppose something is wrong with these rules, and the  
expression in “[...]” is not interpreted the way it seems to be to me.

One entertaining thing: I've noticed “and 1” is always replaced by “mod 2”  
in the simplifier's *.SIV output files. As an example, the latter Check  
clause is replaced by:

    C1:    bit__and(instance, 2) = 0 -> instance div 2 mod 2 = 0 .