From: Phil Thornley <phil.jpthornley@gmail.com>
Subject: Re: (SPARK Ada) Proving that bitwise and is associative?
Date: Wed, 30 Apr 2014 13:39:01 +0100
Date: 2014-04-30T13:39:01+01:00 [thread overview]
Message-ID: <MPG.2dcaff1cdf41fc509896a9@news.zen.co.uk> (raw)
In-Reply-To: toCdnaD_COzqZMLOnZ2dnUVZ_i2dnZ2d@giganews.com
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
next prev parent reply other threads:[~2014-04-30 12:39 UTC|newest]
Thread overview: 4+ messages / expand[flat|nested] mbox.gz Atom feed top
2014-04-29 15:59 (SPARK Ada) Proving that bitwise and is associative? benjaminhocking
2014-04-29 19:11 ` benjaminhocking
2014-04-30 12:39 ` Phil Thornley [this message]
2014-04-30 7:12 ` Stephen Leake
replies disabled
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox