From patchwork Fri Sep 2 07:53:21 2022 Content-Type: text/plain; charset="utf-8" MIME-Version: 1.0 Content-Transfer-Encoding: 7bit X-Patchwork-Submitter: =?utf-8?q?Marc_Poulhi=C3=A8s?= X-Patchwork-Id: 920 Return-Path: Delivered-To: ouuuleilei@gmail.com Received: by 2002:adf:ecc5:0:0:0:0:0 with SMTP id s5csp611483wro; Fri, 2 Sep 2022 00:57:57 -0700 (PDT) X-Google-Smtp-Source: AA6agR4rjICAWZhtyYy5izN9raPf+v4rFyQ5la8B1R9c97y9TkMZnTyYBqb9wtaAGiK12j6sHoWS X-Received: by 2002:a05:6402:1f8c:b0:43e:8fab:76c with SMTP id c12-20020a0564021f8c00b0043e8fab076cmr31544525edc.126.1662105477142; Fri, 02 Sep 2022 00:57:57 -0700 (PDT) ARC-Seal: i=1; a=rsa-sha256; t=1662105477; cv=none; d=google.com; s=arc-20160816; b=JOMYGDjFIX+IgnxzwwsKWwMEivhKADjeV+HhqBIIpTUlh8rESYTciThKIxP9It7+K3 BgCuIz/BL/7CaI8NT5fx6WZfPcPNoAECMH0aDfplodeI32UkPcyGGFbNywQaIlLSWJfV sct6lzs+ROslMB4Jl9VzfQLchUEzFDbp3nROlUiUx0NOMYYr8ba2tFgD6fwpdpM32ZXw GYSaQFKM2QzvZ2cw123XOxJ8hD70WFfpbtiw8cbXFBza6xkNUuelnTXgTkTKf2GIcgRU kgOF4/IKYpiLh+2UzKo5zlZw0qqCVA2eqFUuDl7PqRuRjk2gs8eR8IlrAKQl1FSZKR/T IZRg== ARC-Message-Signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=arc-20160816; h=sender:errors-to:cc:reply-to:from:list-subscribe:list-help :list-post:list-archive:list-unsubscribe:list-id:precedence :content-disposition:mime-version:message-id:subject:to:date :dmarc-filter:delivered-to:dkim-signature:dkim-filter; bh=fnosUpXwFDiIZa4bmaG9N2OUbzwlzNgmcPEO4Ezgv6I=; b=Q074MTVR4WyIptRDE4XQa0MD1V21NUfSRYKJM1zLm+R1zCkF19LJMUMtpOyNq8YB/L Nr+uQ+AM8DK+knGDFKLFxui7rjSah/E7bqzDQ2CI6vcSTtjfQxl8AQzBT5+lIX87y2mW /XV0d3n6V+jsTLSIcZJluFK+FYZVYDp5Jv7Psv5Avj/n5nrmXz3enu5YLFaknvAww014 bhJYVwQ8TcqbIMo4+HqWW8PR/ABVuLq7nat00s/ftooGX3QphKSCfjdLxYD6s/LLqTRE To5FzOa06ndGjgVKNA4Y++ezl1RWBQW5M4y0aqQmd2j9/wrJek7k3GmrFgsaF2FZyDjn 8xWA== ARC-Authentication-Results: i=1; mx.google.com; dkim=pass header.i=@gcc.gnu.org header.s=default header.b=mdVCVpnP; spf=pass (google.com: domain of gcc-patches-bounces+ouuuleilei=gmail.com@gcc.gnu.org designates 2620:52:3:1:0:246e:9693:128c as permitted sender) smtp.mailfrom="gcc-patches-bounces+ouuuleilei=gmail.com@gcc.gnu.org"; dmarc=pass (p=NONE sp=NONE dis=NONE) header.from=gnu.org Received: from sourceware.org (server2.sourceware.org. [2620:52:3:1:0:246e:9693:128c]) by mx.google.com with ESMTPS id sh38-20020a1709076ea600b007414dda0c62si1356290ejc.817.2022.09.02.00.57.56 for (version=TLS1_3 cipher=TLS_AES_256_GCM_SHA384 bits=256/256); Fri, 02 Sep 2022 00:57:57 -0700 (PDT) Received-SPF: pass (google.com: domain of gcc-patches-bounces+ouuuleilei=gmail.com@gcc.gnu.org designates 2620:52:3:1:0:246e:9693:128c as permitted sender) client-ip=2620:52:3:1:0:246e:9693:128c; Authentication-Results: mx.google.com; dkim=pass header.i=@gcc.gnu.org header.s=default header.b=mdVCVpnP; spf=pass (google.com: domain of gcc-patches-bounces+ouuuleilei=gmail.com@gcc.gnu.org designates 2620:52:3:1:0:246e:9693:128c as permitted sender) smtp.mailfrom="gcc-patches-bounces+ouuuleilei=gmail.com@gcc.gnu.org"; dmarc=pass (p=NONE sp=NONE dis=NONE) header.from=gnu.org Received: from server2.sourceware.org (localhost [IPv6:::1]) by sourceware.org (Postfix) with ESMTP id 740843857C6F for ; Fri, 2 Sep 2022 07:56:11 +0000 (GMT) DKIM-Filter: OpenDKIM Filter v2.11.0 sourceware.org 740843857C6F DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gcc.gnu.org; s=default; t=1662105371; bh=fnosUpXwFDiIZa4bmaG9N2OUbzwlzNgmcPEO4Ezgv6I=; h=Date:To:Subject:List-Id:List-Unsubscribe:List-Archive:List-Post: List-Help:List-Subscribe:From:Reply-To:Cc:From; b=mdVCVpnPkircpUHVTbDHgkd2B1z0+oGu1G2XM3+jPIViiuODEjNvzF7EP7ELE4+rX W1RnvNhktKgTXp44LsfvXivY9jsV71b7ZMl2bkySSyHLLc62G2hon4Pry0aqDhvIQm X6MfjDoos2OgPb8MFhfvKWnWTB+3mlLQLawDQO+w= X-Original-To: gcc-patches@gcc.gnu.org Delivered-To: gcc-patches@gcc.gnu.org Received: from mail-wm1-x334.google.com (mail-wm1-x334.google.com [IPv6:2a00:1450:4864:20::334]) by sourceware.org (Postfix) with ESMTPS id CFC703858C55 for ; Fri, 2 Sep 2022 07:53:23 +0000 (GMT) DMARC-Filter: OpenDMARC Filter v1.4.1 sourceware.org CFC703858C55 Received: by mail-wm1-x334.google.com with SMTP id ay39-20020a05600c1e2700b003a5503a80cfso918936wmb.2 for ; Fri, 02 Sep 2022 00:53:23 -0700 (PDT) X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20210112; h=content-disposition:mime-version:message-id:subject:cc:to:from:date :x-gm-message-state:from:to:cc:subject:date; bh=fnosUpXwFDiIZa4bmaG9N2OUbzwlzNgmcPEO4Ezgv6I=; b=KReadNGH/iA/g7zQquAJf+xyahjY0TCvcE+pp6Vun7Wyhl5tyuBH+BlYSPGN0nyXwd mXsnpXosCdFM8qSEBW3S6dhz138x1EHxIepLgO+oernnVoeCVVs5uSrmD5lq2g+bb0PG BBF7fHP4+zBJ28XDDNMwMO4maS3DNfIr/W0siStxhWWNLVfA/gJtkmS1z+86WtK7qq3x ozyZpHQt/NvbIkiWdr65YsYTXY+eT6mArNu2UV2UUGUFhqIOD+phwgA+8Fyth7wkIAls /jrvoOSOTKBKNAuA4malqyGc4r06Rr7napd1A/YiRUhYU6UUyVqB2hFIqN5tYdaOLF+r v1gA== X-Gm-Message-State: ACgBeo2HdM2Y3wTEZZ2K+gshGQ6BZMVrnRO7l6/moS3HUtxTkn7Yn+Ol rajZAtANO5ki3Ih6HqXMHvhsNkjTCYHsdg== X-Received: by 2002:a05:600c:26d2:b0:3a6:280c:24a with SMTP id 18-20020a05600c26d200b003a6280c024amr1842677wmv.130.1662105202696; Fri, 02 Sep 2022 00:53:22 -0700 (PDT) Received: from poulhies-Precision-5550 (static-176-191-105-132.ftth.abo.bbox.fr. [176.191.105.132]) by smtp.gmail.com with ESMTPSA id j39-20020a05600c1c2700b003a62400724bsm1504164wms.0.2022.09.02.00.53.21 (version=TLS1_3 cipher=TLS_AES_256_GCM_SHA384 bits=256/256); Fri, 02 Sep 2022 00:53:21 -0700 (PDT) Date: Fri, 2 Sep 2022 09:53:21 +0200 To: gcc-patches@gcc.gnu.org Subject: [Ada] Recover proof of Scaled_Divide in System.Arith_64 Message-ID: <20220902075321.GA1121015@poulhies-Precision-5550> MIME-Version: 1.0 Content-Disposition: inline X-Spam-Status: No, score=-10.6 required=5.0 tests=BAYES_00, DKIM_SIGNED, DKIM_VALID, DKIM_VALID_AU, DKIM_VALID_EF, GIT_PATCH_0, KAM_ASCII_DIVIDERS, KAM_NUMSUBJECT, RCVD_IN_DNSWL_NONE, SPF_HELO_NONE, SPF_PASS, TXREP, T_SCC_BODY_TEXT_LINE autolearn=ham autolearn_force=no version=3.4.6 X-Spam-Checker-Version: SpamAssassin 3.4.6 (2021-04-09) on server2.sourceware.org X-BeenThere: gcc-patches@gcc.gnu.org X-Mailman-Version: 2.1.29 Precedence: list List-Id: Gcc-patches mailing list List-Unsubscribe: , List-Archive: List-Post: List-Help: List-Subscribe: , X-Patchwork-Original-From: =?utf-8?q?Marc_Poulhi=C3=A8s_via_Gcc-patches?= From: =?utf-8?q?Marc_Poulhi=C3=A8s?= Reply-To: Marc =?iso-8859-1?q?Poulhi=E8s?= Cc: Yannick Moy Errors-To: gcc-patches-bounces+ouuuleilei=gmail.com@gcc.gnu.org Sender: "Gcc-patches" X-getmail-retrieved-from-mailbox: =?utf-8?q?INBOX?= X-GMAIL-THRID: =?utf-8?q?1742843913268563515?= X-GMAIL-MSGID: =?utf-8?q?1742843913268563515?= Proof of Scaled_Divide was impacted by changes in provers and Why3. Recover it partially, leaving some unproved basic inferences to be further investigated. Tested on x86_64-pc-linux-gnu, committed on trunk gcc/ada/ * libgnat/s-aridou.adb: Add or rework ghost code. * libgnat/s-aridou.ads: Add Big_Positive subtype. diff --git a/gcc/ada/libgnat/s-aridou.adb b/gcc/ada/libgnat/s-aridou.adb --- a/gcc/ada/libgnat/s-aridou.adb +++ b/gcc/ada/libgnat/s-aridou.adb @@ -126,7 +126,7 @@ is Pre => B /= 0; -- Length doubling remainder - function Big_2xx (N : Natural) return Big_Integer is + function Big_2xx (N : Natural) return Big_Positive is (Big (Double_Uns'(2 ** N))) with Ghost, @@ -141,6 +141,13 @@ is with Ghost; -- X1&X2&X3 as a big integer + function Big3 (X1, X2, X3 : Big_Integer) return Big_Integer is + (Big_2xxSingle * Big_2xxSingle * X1 + + Big_2xxSingle * X2 + + X3) + with Ghost; + -- Version of Big3 on big integers + function Le3 (X1, X2, X3, Y1, Y2, Y3 : Single_Uns) return Boolean with Post => Le3'Result = (Big3 (X1, X2, X3) <= Big3 (Y1, Y2, Y3)); @@ -234,6 +241,17 @@ is Pre => X /= Double_Uns'Last, Post => Big (X + Double_Uns'(1)) = Big (X) + 1; + procedure Lemma_Big_Of_Double_Uns (X : Double_Uns) + with + Ghost, + Post => Big (X) < Big_2xxDouble; + + procedure Lemma_Big_Of_Double_Uns_Of_Single_Uns (X : Single_Uns) + with + Ghost, + Post => Big (Double_Uns (X)) >= 0 + and then Big (Double_Uns (X)) < Big_2xxSingle; + procedure Lemma_Bounded_Powers_Of_2_Increasing (M, N : Natural) with Ghost, @@ -447,9 +465,9 @@ is procedure Lemma_Mult_Non_Negative (X, Y : Big_Integer) with Ghost, - Pre => (X >= Big_0 and then Y >= Big_0) - or else (X <= Big_0 and then Y <= Big_0), - Post => X * Y >= Big_0; + Pre => (X >= 0 and then Y >= 0) + or else (X <= 0 and then Y <= 0), + Post => X * Y >= 0; procedure Lemma_Mult_Non_Positive (X, Y : Big_Integer) with @@ -458,6 +476,13 @@ is or else (X >= Big_0 and then Y <= Big_0), Post => X * Y <= Big_0; + procedure Lemma_Mult_Positive (X, Y : Big_Integer) + with + Ghost, + Pre => (X > Big_0 and then Y > Big_0) + or else (X < Big_0 and then Y < Big_0), + Post => X * Y > Big_0; + procedure Lemma_Neg_Div (X, Y : Big_Integer) with Ghost, @@ -604,6 +629,8 @@ is procedure Lemma_Abs_Range (X : Big_Integer) is null; procedure Lemma_Add_Commutation (X : Double_Uns; Y : Single_Uns) is null; procedure Lemma_Add_One (X : Double_Uns) is null; + procedure Lemma_Big_Of_Double_Uns (X : Double_Uns) is null; + procedure Lemma_Big_Of_Double_Uns_Of_Single_Uns (X : Single_Uns) is null; procedure Lemma_Bounded_Powers_Of_2_Increasing (M, N : Natural) is null; procedure Lemma_Deep_Mult_Commutation (Factor : Big_Integer; @@ -638,6 +665,7 @@ is procedure Lemma_Mult_Distribution (X, Y, Z : Big_Integer) is null; procedure Lemma_Mult_Non_Negative (X, Y : Big_Integer) is null; procedure Lemma_Mult_Non_Positive (X, Y : Big_Integer) is null; + procedure Lemma_Mult_Positive (X, Y : Big_Integer) is null; procedure Lemma_Neg_Rem (X, Y : Big_Integer) is null; procedure Lemma_Not_In_Range_Big2xx64 is null; procedure Lemma_Powers (A : Big_Natural; B, C : Natural) is null; @@ -1888,7 +1916,7 @@ is -- Local ghost variables - Mult : constant Big_Integer := abs (Big (X) * Big (Y)) with Ghost; + Mult : constant Big_Natural := abs (Big (X) * Big (Y)) with Ghost; Quot : Big_Integer with Ghost; Big_R : Big_Integer with Ghost; Big_Q : Big_Integer with Ghost; @@ -1955,6 +1983,15 @@ is -- Proves correctness of the multiplication of divisor by quotient to -- compute amount to subtract. + procedure Prove_Mult_Decomposition_Split3 + (D1, D2, D3, D3_Hi, D3_Lo, D4 : Big_Integer) + with + Ghost, + Pre => Is_Mult_Decomposition (D1, D2, D3, D4) + and then D3 = Big_2xxSingle * D3_Hi + D3_Lo, + Post => Is_Mult_Decomposition (D1, D2 + D3_Hi, D3_Lo, D4); + -- Proves decomposition of Mult after splitting third component + procedure Prove_Negative_Dividend with Ghost, @@ -2066,6 +2103,27 @@ is else abs Quot); -- Proves correctness of the rounding of the unsigned quotient + procedure Prove_Scaled_Mult_Decomposition_Regroup24 + (D1, D2, D3, D4 : Big_Integer) + with + Ghost, + Pre => Scale < Double_Size + and then Is_Scaled_Mult_Decomposition (D1, D2, D3, D4), + Post => Is_Scaled_Mult_Decomposition + (0, Big_2xxSingle * D1 + D2, 0, Big_2xxSingle * D3 + D4); + -- Proves scaled decomposition of Mult after regrouping on second and + -- fourth component. + + procedure Prove_Scaled_Mult_Decomposition_Regroup3 + (D1, D2, D3, D4 : Big_Integer) + with + Ghost, + Pre => Scale < Double_Size + and then Is_Scaled_Mult_Decomposition (D1, D2, D3, D4), + Post => Is_Scaled_Mult_Decomposition (0, 0, Big3 (D1, D2, D3), D4); + -- Proves scaled decomposition of Mult after regrouping on third + -- component. + procedure Prove_Sign_R with Ghost, @@ -2315,6 +2373,14 @@ is + Big (Double_Uns (S3)))); end Prove_Multiplication; + ------------------------------------- + -- Prove_Mult_Decomposition_Split3 -- + ------------------------------------- + + procedure Prove_Mult_Decomposition_Split3 + (D1, D2, D3, D3_Hi, D3_Lo, D4 : Big_Integer) + is null; + ----------------------------- -- Prove_Negative_Dividend -- ----------------------------- @@ -2413,6 +2479,22 @@ is end if; end Prove_Rounding_Case; + ----------------------------------------------- + -- Prove_Scaled_Mult_Decomposition_Regroup24 -- + ----------------------------------------------- + + procedure Prove_Scaled_Mult_Decomposition_Regroup24 + (D1, D2, D3, D4 : Big_Integer) + is null; + + ---------------------------------------------- + -- Prove_Scaled_Mult_Decomposition_Regroup3 -- + ---------------------------------------------- + + procedure Prove_Scaled_Mult_Decomposition_Regroup3 + (D1, D2, D3, D4 : Big_Integer) + is null; + ------------------ -- Prove_Sign_R -- ------------------ @@ -2585,29 +2667,15 @@ is T2 := D (3) + Lo (T1); Lemma_Add_Commutation (Double_Uns (D (3)), Lo (T1)); - pragma Assert - (Is_Mult_Decomposition - (D1 => 0, - D2 => Big (Double_Uns'(Xhi * Yhi)) + Big (Double_Uns (D (2))) - + Big (Double_Uns (Hi (T1))), - D3 => Big (T2), - D4 => Big (Double_Uns (D (4))))); Lemma_Hi_Lo (T2, Hi (T2), Lo (T2)); - pragma Assert - (By (Is_Mult_Decomposition - (D1 => 0, - D2 => Big (Double_Uns'(Xhi * Yhi)) + Big (Double_Uns (D (2))) - + Big (Double_Uns (Hi (T1))) + Big (Double_Uns (Hi (T2))), - D3 => Big (Double_Uns (Lo (T2))), - D4 => Big (Double_Uns (D (4)))), - By (Big_2xxSingle * Big (T2) = - Big_2xxSingle * Big_2xxSingle * Big (Double_Uns (Hi (T2))) - + Big_2xxSingle * Big (Double_Uns (Lo (T2))), - Big_2xxSingle * - (Big_2xxSingle * Big (Double_Uns (Hi (T2))) - + Big (Double_Uns (Lo (T2)))) - = Big_2xxSingle * Big_2xxSingle * Big (Double_Uns (Hi (T2))) - + Big_2xxSingle * Big (Double_Uns (Lo (T2)))))); + Prove_Mult_Decomposition_Split3 + (D1 => 0, + D2 => Big (Double_Uns'(Xhi * Yhi)) + Big (Double_Uns (D (2))) + + Big (Double_Uns (Hi (T1))), + D3 => Big (T2), + D3_Hi => Big (Double_Uns (Hi (T2))), + D3_Lo => Big (Double_Uns (Lo (T2))), + D4 => Big (Double_Uns (D (4)))); D (3) := Lo (T2); T3 := D (2) + Hi (T1); @@ -2807,8 +2875,20 @@ is pragma Assert (Mult >= Big_2xxSingle * Big_2xxSingle * Big_2xxSingle * Big (Double_Uns (D (1)))); + Lemma_Double_Big_2xxSingle; + Lemma_Mult_Positive (Big_2xxDouble, Big_2xxSingle); + Lemma_Ge_Mult (Big (Double_Uns (D (1))), + 1, + Big_2xxDouble * Big_2xxSingle, + Big_2xxDouble * Big_2xxSingle); + Lemma_Mult_Positive (Big_2xxSingle, Big (Double_Uns (D (1)))); + Lemma_Ge_Mult (Big_2xxSingle * Big_2xxSingle, Big_2xxDouble, + Big_2xxSingle * Big (Double_Uns (D (1))), + Big_2xxDouble * Big_2xxSingle); pragma Assert (Mult >= Big_2xxDouble * Big_2xxSingle); Lemma_Ge_Commutation (2 ** Single_Size, Zu); + Lemma_Ge_Mult (Big_2xxSingle, Big (Zu), Big_2xxDouble, + Big_2xxDouble * Big (Zu)); pragma Assert (Mult >= Big_2xxDouble * Big (Zu)); else Lemma_Ge_Commutation (Double_Uns (D (2)), Zu); @@ -2887,6 +2967,13 @@ is Post => Shift / 2 = 2 ** (Log_Single_Size - (Inter + 1)) and then (Shift = 2 or (Shift / 2) mod 2 = 0); + procedure Prove_Prev_And_Mask (Prev, Mask : Single_Uns) + with + Ghost, + Pre => Prev /= 0 + and then (Prev and Mask) = 0, + Post => (Prev and not Mask) /= 0; + procedure Prove_Shift_Progress with Ghost, @@ -2918,6 +3005,7 @@ is -- Local lemma null bodies -- ----------------------------- + procedure Prove_Prev_And_Mask (Prev, Mask : Single_Uns) is null; procedure Prove_Power is null; procedure Prove_Shifting is null; procedure Prove_Shift_Progress is null; @@ -2941,6 +3029,15 @@ is if (Hi (Zu) and Mask) = 0 then Zu := Shift_Left (Zu, Shift); + pragma Assert ((Hi (Zu_Prev) and Mask_Prev) /= 0); + pragma Assert + (By ((Hi (Zu_Prev) and Mask_Prev and Mask) = 0, + (Hi (Zu_Prev) and Mask) = 0 + and then + (Hi (Zu_Prev) and Mask_Prev and Mask) + = (Hi (Zu_Prev) and Mask and Mask_Prev) + )); + Prove_Prev_And_Mask (Hi (Zu_Prev) and Mask_Prev, Mask); Prove_Shifting; pragma Assert (Big (Zu_Prev) = Big (Double_Uns'(abs Z)) * Big_2xx (Scale)); @@ -2986,6 +3083,7 @@ is -- not change the invariant that (D (1) & D (2)) < Zu. Lemma_Lt_Commutation (D (1) & D (2), abs Z); + Lemma_Big_Of_Double_Uns (Zu); Lemma_Lt_Mult (Big (D (1) & D (2)), Big (Double_Uns'(abs Z)), Big_2xx (Scale), Big_2xxDouble); @@ -3007,82 +3105,21 @@ is * Big (Double_Uns (Hi (T1))) = Big_2xxSingle * Big_2xxSingle * Big_2xxSingle * Big (Double_Uns (D (1)))); - - pragma Assert - (Is_Scaled_Mult_Decomposition - (Big (Double_Uns (D (1))), - Big (Double_Uns (D (2))), - Big (Double_Uns (D (3))), - Big (Double_Uns (D (4))))); - pragma Assert - (By (Is_Scaled_Mult_Decomposition - (0, - 0, - Big_2xxSingle * Big_2xxSingle * Big (Double_Uns (D (1))) - + Big_2xxSingle * Big (Double_Uns (D (2))) - + Big (Double_Uns (D (3))), - Big (Double_Uns (D (4)))), - Big_2xxSingle * - (Big_2xxSingle * Big_2xxSingle * Big (Double_Uns (D (1))) - + Big_2xxSingle * Big (Double_Uns (D (2))) - + Big (Double_Uns (D (3)))) - + Big (Double_Uns (D (4))) = - Big_2xxSingle * - Big_2xxSingle * Big_2xxSingle * Big (Double_Uns (D (1))) - + Big_2xxSingle * Big_2xxSingle * Big (Double_Uns (D (2))) - + Big_2xxSingle * Big (Double_Uns (D (3))) - + Big (Double_Uns (D (4))) - and then - (By (Mult * Big_2xx (Scale) = - Big_2xxSingle * - Big_2xxSingle * Big_2xxSingle * Big (Double_Uns (D (1))) - + Big_2xxSingle * Big_2xxSingle * Big (Double_Uns (D (2))) - + Big_2xxSingle * Big (Double_Uns (D (3))) - + Big (Double_Uns (D (4))), - Is_Scaled_Mult_Decomposition - (Big (Double_Uns (D (1))), - Big (Double_Uns (D (2))), - Big (Double_Uns (D (3))), - Big (Double_Uns (D (4)))))))); - Lemma_Substitution - (Mult * Big_2xx (Scale), Big_2xxSingle, - Big_2xxSingle * Big_2xxSingle * Big (Double_Uns (D (1))) - + Big_2xxSingle * Big (Double_Uns (D (2))) - + Big (Double_Uns (D (3))), - Big3 (D (1), D (2), D (3)), - Big (Double_Uns (D (4)))); Lemma_Substitution (Big_2xxDouble * Big (Zu), Big_2xxDouble, Big (Zu), Big (Double_Uns'(abs Z)) * Big_2xx (Scale), 0); Lemma_Lt_Mult (Mult, Big_2xxDouble * Big (Double_Uns'(abs Z)), Big_2xx (Scale), Big_2xxDouble * Big (Zu)); + pragma Assert (Mult >= Big_0); + pragma Assert (Big_2xx (Scale) >= Big_0); + Lemma_Mult_Non_Negative (Mult, Big_2xx (Scale)); Lemma_Div_Lt (Mult * Big_2xx (Scale), Big (Zu), Big_2xxDouble); Lemma_Concat_Definition (D (1), D (2)); Lemma_Double_Big_2xxSingle; - pragma Assert - (Big_2xxSingle * - (Big_2xxSingle * Big_2xxSingle * Big (Double_Uns (D (1))) - + Big_2xxSingle * Big (Double_Uns (D (2))) - + Big (Double_Uns (D (3)))) - + Big (Double_Uns (D (4))) - = Big_2xxSingle * Big_2xxSingle * - (Big_2xxSingle * Big (Double_Uns (D (1))) - + Big (Double_Uns (D (2)))) - + Big_2xxSingle * Big (Double_Uns (D (3))) - + Big (Double_Uns (D (4)))); - pragma Assert - (By (Is_Scaled_Mult_Decomposition - (0, - Big_2xxSingle * Big (Double_Uns (D (1))) - + Big (Double_Uns (D (2))), - 0, - Big_2xxSingle * Big (Double_Uns (D (3))) - + Big (Double_Uns (D (4)))), - Big_2xxSingle * Big_2xxSingle * - (Big_2xxSingle * Big (Double_Uns (D (1))) - + Big (Double_Uns (D (2)))) = - Big_2xxSingle * - Big_2xxSingle * Big_2xxSingle * Big (Double_Uns (D (1))) - + Big_2xxSingle * Big_2xxSingle * Big (Double_Uns (D (2))))); + Prove_Scaled_Mult_Decomposition_Regroup24 + (Big (Double_Uns (D (1))), + Big (Double_Uns (D (2))), + Big (Double_Uns (D (3))), + Big (Double_Uns (D (4)))); Lemma_Substitution (Mult * Big_2xx (Scale), Big_2xxSingle * Big_2xxSingle, Big_2xxSingle * Big (Double_Uns (D (1))) @@ -3115,10 +3152,20 @@ is -- Local ghost variables Qd1 : Single_Uns := 0 with Ghost; + D234 : Big_Integer := 0 with Ghost; D123 : constant Big_Integer := Big3 (D (1), D (2), D (3)) with Ghost; + D4 : constant Big_Integer := Big (Double_Uns (D (4))) + with Ghost; begin + Prove_Scaled_Mult_Decomposition_Regroup3 + (Big (Double_Uns (D (1))), + Big (Double_Uns (D (2))), + Big (Double_Uns (D (3))), + Big (Double_Uns (D (4)))); + pragma Assert (Mult * Big_2xx (Scale) = Big_2xxSingle * D123 + D4); + for J in 1 .. 2 loop Lemma_Hi_Lo (D (J) & D (J + 1), D (J), D (J + 1)); pragma Assert (Big (D (J) & D (J + 1)) < Big (Zu)); @@ -3138,6 +3185,7 @@ is Qd (J) := Single_Uns'Last; Lemma_Concat_Definition (D (J), D (J + 1)); + Lemma_Big_Of_Double_Uns_Of_Single_Uns (D (J + 2)); pragma Assert (Big_2xxSingle > Big (Double_Uns (D (J + 2)))); pragma Assert (Big3 (D (J), D (J + 1), 0) + Big_2xxSingle > Big3 (D (J), D (J + 1), D (J + 2))); @@ -3158,6 +3206,8 @@ is Lemma_Div_Lt (Big3 (D (J), D (J + 1), D (J + 2)), Big_2xxSingle, Big (Zu)); + pragma Assert (Big (Double_Uns (Qd (J))) >= + Big3 (D (J), D (J + 1), D (J + 2)) / Big (Zu)); else Qd (J) := Lo ((D (J) & D (J + 1)) / Zhi); @@ -3165,6 +3215,7 @@ is Prove_Qd_Calculation_Part_1 (J); end if; + pragma Assert (for all K in 1 .. J => Qd (K)'Initialized); Lemma_Gt_Mult (Big (Double_Uns (Qd (J))), Big3 (D (J), D (J + 1), D (J + 2)) / Big (Zu), @@ -3199,7 +3250,9 @@ is Lemma_Hi_Lo_3 (Zu, Zhi, Zlo); while not Le3 (S1, S2, S3, D (J), D (J + 1), D (J + 2)) loop - pragma Loop_Invariant (Qd (J)'Initialized); + pragma Loop_Invariant + (for all K in 1 .. J => Qd (K)'Initialized); + pragma Loop_Invariant (if J = 2 then Qd (1) = Qd1); pragma Loop_Invariant (Big3 (S1, S2, S3) = Big (Double_Uns (Qd (J))) * Big (Zu)); pragma Loop_Invariant @@ -3240,6 +3293,7 @@ is -- Now subtract S1&S2&S3 from D1&D2&D3 ready for next step + pragma Assert (for all K in 1 .. J => Qd (K)'Initialized); pragma Assert (Big3 (S1, S2, S3) = Big (Double_Uns (Qd (J))) * Big (Zu)); pragma Assert (Big3 (S1, S2, S3) > @@ -3256,19 +3310,32 @@ is * Big_2xxSingle * Big (Double_Uns (D (J))) + Big_2xxSingle * Big (Double_Uns (D (J + 1))) + Big (Double_Uns (D (J + 2)))); - pragma Assert (Big3 (D (J), D (J + 1), D (J + 2)) = - Big_2xxDouble * Big (Double_Uns (D (J))) - + Big_2xxSingle * Big (Double_Uns (D (J + 1))) - + Big (Double_Uns (D (J + 2)))); pragma Assert (Big_2xxSingle >= 0); + Lemma_Big_Of_Double_Uns_Of_Single_Uns (D (J + 1)); pragma Assert (Big (Double_Uns (D (J + 1))) >= 0); + Lemma_Mult_Non_Negative + (Big_2xxSingle, Big (Double_Uns (D (J + 1)))); pragma Assert - (Big_2xxSingle * Big (Double_Uns (D (J + 1))) >= 0); - pragma Assert - (Big_2xxSingle * Big (Double_Uns (D (J + 1))) - + Big (Double_Uns (D (J + 2))) >= 0); - pragma Assert (Big3 (D (J), D (J + 1), D (J + 2)) >= - Big_2xxDouble * Big (Double_Uns (D (J)))); + (By (Big3 (D (J), D (J + 1), D (J + 2)) >= + Big_2xxSingle * Big_2xxSingle + * Big (Double_Uns (D (J))), + By (Big3 (D (J), D (J + 1), D (J + 2)) + - Big_2xxSingle * Big_2xxSingle + * Big (Double_Uns (D (J))) + = Big_2xxSingle * Big (Double_Uns (D (J + 1))) + + Big (Double_Uns (D (J + 2))), + Big3 (D (J), D (J + 1), D (J + 2)) = + Big_2xxSingle + * Big_2xxSingle * Big (Double_Uns (D (J))) + + Big_2xxSingle * Big (Double_Uns (D (J + 1))) + + Big (Double_Uns (D (J + 2)))) + and then + By (Big_2xxSingle * Big (Double_Uns (D (J + 1))) + + Big (Double_Uns (D (J + 2))) >= 0, + Big_2xxSingle * Big (Double_Uns (D (J + 1))) >= 0 + and then + Big (Double_Uns (D (J + 2))) >= 0 + ))); Lemma_Ge_Commutation (Double_Uns (D (J)), Double_Uns'(1)); Lemma_Ge_Mult (Big (Double_Uns (D (J))), Big (Double_Uns'(1)), @@ -3283,6 +3350,8 @@ is if J = 1 then Qd1 := Qd (1); + D234 := Big3 (D (2), D (3), D (4)); + pragma Assert (D4 = Big (Double_Uns (D (4)))); Lemma_Substitution (Mult * Big_2xx (Scale), Big_2xxSingle, D123, Big3 (D (1), D (2), D (3)) + Big3 (S1, S2, S3), @@ -3291,23 +3360,38 @@ is Lemma_Substitution (Mult * Big_2xx (Scale), Big_2xxSingle, Big3 (S1, S2, S3), Big (Double_Uns (Qd1)) * Big (Zu), - Big3 (D (2), D (3), D (4))); + D234); else pragma Assert (Qd1 = Qd (1)); pragma Assert - (Big_2xxSingle * Big_2xxSingle * Big (Double_Uns (D (2))) - = 0); - pragma Assert - (Mult * Big_2xx (Scale) = - Big_2xxSingle * Big (Double_Uns (Qd (1))) * Big (Zu) + (By (Mult * Big_2xx (Scale) = + Big_2xxSingle * Big (Double_Uns (Qd1)) * Big (Zu) + Big3 (S1, S2, S3) - + Big3 (D (2), D (3), D (4))); + + Big3 (D (2), D (3), D (4)), + Big3 (D (2), D (3), D (4)) = D234 - Big3 (S1, S2, S3))); pragma Assert - (Mult * Big_2xx (Scale) = + (By (Mult * Big_2xx (Scale) = Big_2xxSingle * Big (Double_Uns (Qd (1))) * Big (Zu) + Big (Double_Uns (Qd (2))) * Big (Zu) + Big_2xxSingle * Big (Double_Uns (D (3))) - + Big (Double_Uns (D (4)))); + + Big (Double_Uns (D (4))), + Big_2xxSingle * Big (Double_Uns (Qd (1))) * Big (Zu) + = Big_2xxSingle * Big (Double_Uns (Qd1)) * Big (Zu) + and then + Big3 (S1, S2, S3) = Big (Double_Uns (Qd (2))) * Big (Zu) + and then + By (Big3 (D (2), D (3), D (4)) + = Big_2xxSingle * Big (Double_Uns (D (3))) + + Big (Double_Uns (D (4))), + Big3 (D (2), D (3), D (4)) + = Big_2xxSingle * Big_2xxSingle * + Big (Double_Uns (D (2))) + + Big_2xxSingle * Big (Double_Uns (D (3))) + + Big (Double_Uns (D (4))) + and then + Big_2xxSingle * Big_2xxSingle * Big (Double_Uns (D (2))) + = 0) + )); end if; end loop; end; @@ -3319,6 +3403,7 @@ is -- We rescale the divisor as well, to make the proper comparison -- for rounding below. + pragma Assert (for all K in 1 .. 2 => Qd (K)'Initialized); Qu := Qd (1) & Qd (2); Ru := D (3) & D (4); @@ -3440,14 +3525,14 @@ is Ghost, Pre => X2 < Y2, Post => Big3 (X1, X2 - Y2, X3) - = Big3 (X1, X2, X3) + Big3 (1, 0, 0) - Big3 (0, Y2, 0); + = Big3 (X1, X2, X3) + Big3 (Single_Uns'(1), 0, 0) - Big3 (0, Y2, 0); procedure Lemma_Sub3_With_Carry3 (X1, X2, X3, Y3 : Single_Uns) with Ghost, Pre => X3 < Y3, Post => Big3 (X1, X2, X3 - Y3) - = Big3 (X1, X2, X3) + Big3 (0, 1, 0) - Big3 (0, 0, Y3); + = Big3 (X1, X2, X3) + Big3 (Single_Uns'(0), 1, 0) - Big3 (0, 0, Y3); ------------------------- -- Lemma_Add3_No_Carry -- @@ -3522,10 +3607,12 @@ is X1 := X1 - 1; pragma Assert - (Big3 (X1, X2, X3) = Big3 (XX1, XX2, XX3) - Big3 (1, 0, 0)); + (Big3 (X1, X2, X3) = + Big3 (XX1, XX2, XX3) - Big3 (Single_Uns'(1), 0, 0)); pragma Assert (Big3 (X1, X2, X3) = Big3 (XX1, XX2, XX3) - - Big3 (0, Single_Uns'Last, 0) - Big3 (0, 1, 0)); + - Big3 (Single_Uns'(0), Single_Uns'Last, 0) + - Big3 (Single_Uns'(0), 1, 0)); Lemma_Add3_No_Carry (X1, X2, X3, 0, Single_Uns'Last, 0); else Lemma_Sub3_No_Carry (X1, X2, X3, 0, 1, 0); @@ -3534,7 +3621,8 @@ is X2 := X2 - 1; pragma Assert - (Big3 (X1, X2, X3) = Big3 (XX1, XX2, XX3) - Big3 (0, 1, 0)); + (Big3 (X1, X2, X3) = + Big3 (XX1, XX2, XX3) - Big3 (Single_Uns'(0), 1, 0)); Lemma_Sub3_With_Carry3 (X1, X2, X3, Y3); else Lemma_Sub3_No_Carry (X1, X2, X3, 0, 0, Y3); @@ -3553,7 +3641,7 @@ is pragma Assert (Big3 (X1, X2, X3) = Big3 (XX1, XX2, XX3) - - Big3 (0, 0, Y3) - Big3 (1, 0, 0)); + - Big3 (0, 0, Y3) - Big3 (Single_Uns'(1), 0, 0)); Lemma_Sub3_With_Carry2 (X1, X2, X3, Y2); else Lemma_Sub3_No_Carry (X1, X2, X3, 0, Y2, 0); diff --git a/gcc/ada/libgnat/s-aridou.ads b/gcc/ada/libgnat/s-aridou.ads --- a/gcc/ada/libgnat/s-aridou.ads +++ b/gcc/ada/libgnat/s-aridou.ads @@ -69,6 +69,7 @@ is package BI_Ghost renames Ada.Numerics.Big_Numbers.Big_Integers_Ghost; subtype Big_Integer is BI_Ghost.Big_Integer with Ghost; subtype Big_Natural is BI_Ghost.Big_Natural with Ghost; + subtype Big_Positive is BI_Ghost.Big_Positive with Ghost; use type BI_Ghost.Big_Integer; package Signed_Conversion is