From mboxrd@z Thu Jan 1 00:00:00 1970 X-Spam-Checker-Version: SpamAssassin 3.4.4 (2020-01-24) on polar.synack.me X-Spam-Level: X-Spam-Status: No, score=0.1 required=5.0 tests=BAYES_00,FORGED_GMAIL_RCVD, FREEMAIL_FROM,FREEMAIL_REPLY autolearn=no autolearn_force=no version=3.4.4 Path: border1.nntp.dca3.giganews.com!backlog3.nntp.dca3.giganews.com!border1.nntp.dca.giganews.com!nntp.giganews.com!usenet.blueworldhosting.com!feeder01.blueworldhosting.com!feeder.erje.net!eu.feeder.erje.net!newsfeed.freenet.ag!newsfeed0.kamp.net!newsfeed.kamp.net!news.qsc.de!zen.net.uk!hamilton.zen.co.uk!reader01.nrc01.news.zen.net.uk.POSTED!not-for-mail From: Phil Thornley Newsgroups: comp.lang.ada Subject: Re: (SPARK Ada) Proving that bitwise and is associative? Date: Wed, 30 Apr 2014 13:39:01 +0100 Message-ID: References: MIME-Version: 1.0 Content-Type: text/plain; charset="us-ascii" Content-Transfer-Encoding: 7bit User-Agent: MicroPlanet-Gravity/3.0.4 X-Antivirus: avast! (VPS 140429-2, 29/04/2014), Outbound message X-Antivirus-Status: Clean Organization: Zen Internet NNTP-Posting-Host: f11233b1.news.zen.co.uk X-Trace: DXC=WfVL?9P277caogEM\ChbAga0UP_O8AJol=dR0\ckLKG`WeZ<[7LZNRfK=NP@lW4JAcUhLi?]0KG=k510J^32@g5d X-Complaints-To: abuse@zen.co.uk X-Original-Bytes: 4078 Xref: number.nntp.dca.giganews.com comp.lang.ada:186172 Date: 2014-04-30T13:39:01+01:00 List-Id: In article , 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