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=-1.9 required=5.0 tests=BAYES_00,FREEMAIL_FROM
	autolearn=unavailable autolearn_force=no version=3.4.4
X-Received: by 10.182.28.99 with SMTP id a3mr17385073obh.40.1398798712414;
 Tue, 29 Apr 2014 12:11:52 -0700 (PDT)
MIME-Version: 1.0
Path: 
 border2.nntp.dca.giganews.com!ottix-news.ottix.net!news.litech.org!news.glorb.com!l13no12031729iga.0!news-out.google.com!du2ni18994qab.0!nntp.google.com!border1.nntp.dca.giganews.com!nntp.giganews.com!local2.nntp.dca.giganews.com!news.giganews.com.POSTED!not-for-mail
NNTP-Posting-Date: Tue, 29 Apr 2014 14:11:51 -0500
From: benjaminhocking <benjaminhocking@gmail.com>
Subject: Re: (SPARK Ada) Proving that bitwise and is associative?
Newsgroups: comp.lang.ada
X-UserIpAddress: 8.25.3.50
X-InternalId: a2ffaaf1-94fd-4226-af8d-b760914c3733
References: <nd2dnZa1N-bwUcLOnZ2dnUVZ_gOdnZ2d@giganews.com>
Message-ID: <toCdnaD_COzqZMLOnZ2dnUVZ_i2dnZ2d@giganews.com>
Date: Tue, 29 Apr 2014 14:11:51 -0500
X-Usenet-Provider: http://www.giganews.com
X-Trace: 
 sv3-Zm0ebh5C7BgkBQ2GxhE14TVKC/w18lsj2kn5fCW+Oxj/WttMNLCNLChFROj34ebgrag8jzl90ucNfJ3!x2w28heQ34UWJKPol5rHcOLKUuxR6x8V8oXWKBk/pUUYwUGri1I7rJsiLN5AiKITJuU6e3wNWtC3!1A==
X-Complaints-To: abuse@giganews.com
X-DMCA-Notifications: http://www.giganews.com/info/dmca.html
X-Abuse-and-DMCA-Info: Please be sure to forward a copy of ALL headers
X-Abuse-and-DMCA-Info: Otherwise we will be unable to process your complaint
 properly
X-Postfilter: 1.3.40
X-Original-Bytes: 2142
Xref: number.nntp.dca.giganews.com comp.lang.ada:186168
Date: 2014-04-29T14:11:51-05:00
List-Id: <comp.lang.ada>

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 .