(SPARK Ada) Proving that bitwise and is associative?

(SPARK Ada) Proving that bitwise and is associative?

[benjaminhocking]

I have the following check statements embedded in some SPARK Ada code:
      --# check (value and (mask_32 and Unsigned_32'Mod(LMask_8))) = 0;
      --# check ((value and mask_32) and Unsigned_32'Mod(LMask_8)) = 0;
The SPARK examiner is able to prove the first one (using inference) but not the second one, even though it has already proven the first one, so should be able to prove it by using the first one combined with the fact that bitwise and is associative. Does anyone have any suggestions for how I can help it?

Re: (SPARK Ada) Proving that bitwise and is associative?

[benjaminhocking]

If it helps in the diagnosis, here is the VC:
function_u8_5.
H1:    true .
H2:    value >= unsigned_32__first .
H3:    value <= unsigned_32__last .
H4:    umask_8 mod unsigned_32__modulus >= unsigned_32__first .
H5:    umask_8 mod unsigned_32__modulus <= unsigned_32__last .
H6:    bit__and(umask_8 mod unsigned_32__modulus, lmask_8 mod 
           unsigned_32__modulus) = 0 .
H7:    bit__and(value, umask_8 mod unsigned_32__modulus) < 2 ** 16 mod 
           unsigned_32__modulus .
H8:    bit__and(value, bit__and(umask_8 mod unsigned_32__modulus, 
           lmask_8 mod unsigned_32__modulus)) = 0 .
        ->
C1:    bit__and(bit__and(value, umask_8 mod unsigned_32__modulus), 
           lmask_8 mod unsigned_32__modulus) = 0 .

Note that H8 should imply C1. The simplified VC is less helpful, as it has lost the equivalent of H8:
function_u8_5.
H1:    value >= 0 .
H2:    value <= 4294967295 .
H3:    bit__and(value, 65280) < 65536 .
H4:    unsigned_32__size >= 0 .
H5:    unsigned_16__size >= 0 .
H6:    unsigned_8__size >= 0 .
       ->
C1:    bit__and(value, 65280) mod 256 = 0 .

Re: (SPARK Ada) Proving that bitwise and is associative?

[Phil Thornley]

In article <toCdnaD_COzqZMLOnZ2dnUVZ_i2dnZ2d@giganews.com>, 
benjaminhocking@gmail.com says...
> 
> If it helps in the diagnosis, here is the VC:
> function_u8_5.
> H1:    true .
> H2:    value >= unsigned_32__first .
> H3:    value <= unsigned_32__last .
> H4:    umask_8 mod unsigned_32__modulus >= unsigned_32__first .
> H5:    umask_8 mod unsigned_32__modulus <= unsigned_32__last .
> H6:    bit__and(umask_8 mod unsigned_32__modulus, lmask_8 mod 
>            unsigned_32__modulus) = 0 .
> H7:    bit__and(value, umask_8 mod unsigned_32__modulus) < 2 ** 16 mod 
>            unsigned_32__modulus .
> H8:    bit__and(value, bit__and(umask_8 mod unsigned_32__modulus, 
>            lmask_8 mod unsigned_32__modulus)) = 0 .
>         ->
> C1:    bit__and(bit__and(value, umask_8 mod unsigned_32__modulus), 
>            lmask_8 mod unsigned_32__modulus) = 0 .
> 
> Note that H8 should imply C1. The simplified VC is less helpful, as it has lost the equivalent of H8:
> function_u8_5.
> H1:    value >= 0 .
> H2:    value <= 4294967295 .
> H3:    bit__and(value, 65280) < 65536 .
> H4:    unsigned_32__size >= 0 .
> H5:    unsigned_16__size >= 0 .
> H6:    unsigned_8__size >= 0 .
>        ->
> C1:    bit__and(value, 65280) mod 256 = 0 .

What the Simplifier 'knows' about associativity of bit__and will be 
defined by the proof rules that it has available, but the only 
associativity rule for bit__and listed in the Proof Checker rules manual 
isn't the one you are thinking of here. (See the Checker Rules Manual 
Section 4.3, rule 31). I don't think that the Simplifier has any 
additional proof rules.

[BTW, it looks rather as if is there a side-condition missing from rules 
31-33 for Z. The rules are supposed to only apply to modular types, 
according to the rule file header.]

H8 will be eliminated early on by the Simplifier, using the replacement 
defined by H6, and the rule that
   bit__and(X, 0) may_be_replaced_by 0
reducing H8 to 0 = 0, which will be eliminated.

Rather than trying to find a sequence of check annotations that will 
allow the (very limited) set of rules to provide the proof you want, the 
quickest way to deal with this particular check is probably to give the 
Simplifier a user rule. How general you want to make such a rule is up 
to you, but the one most likely to succeed is probably a very specific 
one such as:
   bit__and(bit__and(X, Y), Z) = 0 may_be_deduced_from
      [ 0 <= X, 0 <= Y, 0 <= Z, bit__and(Y, Z) = 0 ] .

Again, by the time this rule is applied H6 will also have been 
eliminated (user rules are only looked when all the Simplifier 
strategies have been exhausted) so it will only work if H6 can be proved 
again for this VC.

The definition of user proof rules is described in Section 7 of the 
Simplifier manual. All user rules should of course be validated to the 
level appropriate to the integrity of your application.

Cheers,

Phil

Re: (SPARK Ada) Proving that bitwise and is associative?

[Stephen Leake]

benjaminhocking <benjaminhocking@gmail.com> writes:

> I have the following check statements embedded in some SPARK Ada code:
>       --# check (value and (mask_32 and Unsigned_32'Mod(LMask_8))) = 0;
>       --# check ((value and mask_32) and Unsigned_32'Mod(LMask_8)) = 0;
> The SPARK examiner is able to prove the first one (using inference)
> but not the second one, even though it has already proven the first
> one, so should be able to prove it by using the first one combined
> with the fact that bitwise and is associative. Does anyone have any
> suggestions for how I can help it?

I have no experience with SPARK, but would it not be more efficient to
assert somewhere that bitwise "and" is associative, rather than checking
it indirectly here?

-- 
-- Stephe