From patchwork Wed Jul 13 10:02:52 2022 Content-Type: text/plain; charset="utf-8" MIME-Version: 1.0 Content-Transfer-Encoding: 7bit X-Patchwork-Submitter: Pierre-Marie de Rodat X-Patchwork-Id: 1655928 Return-Path: X-Original-To: incoming@patchwork.ozlabs.org Delivered-To: patchwork-incoming@bilbo.ozlabs.org Authentication-Results: bilbo.ozlabs.org; dkim=pass (1024-bit key; unprotected) header.d=gcc.gnu.org header.i=@gcc.gnu.org header.a=rsa-sha256 header.s=default header.b=QFzKY9Xk; dkim-atps=neutral Authentication-Results: ozlabs.org; spf=pass (sender SPF authorized) smtp.mailfrom=gcc.gnu.org (client-ip=8.43.85.97; helo=sourceware.org; envelope-from=gcc-patches-bounces+incoming=patchwork.ozlabs.org@gcc.gnu.org; receiver=) Received: from sourceware.org (server2.sourceware.org [8.43.85.97]) (using TLSv1.3 with cipher TLS_AES_256_GCM_SHA384 (256/256 bits) key-exchange X25519 server-signature RSA-PSS (2048 bits) server-digest SHA256) (No client certificate requested) by bilbo.ozlabs.org (Postfix) with ESMTPS id 4LjY921Ghlz9s1l for ; Wed, 13 Jul 2022 20:03:18 +1000 (AEST) Received: from server2.sourceware.org (localhost [IPv6:::1]) by sourceware.org (Postfix) with ESMTP id EE37538768AF for ; Wed, 13 Jul 2022 10:03:15 +0000 (GMT) DKIM-Filter: OpenDKIM Filter v2.11.0 sourceware.org EE37538768AF DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gcc.gnu.org; s=default; t=1657706596; bh=26D2LVJGdd5lDQ3vjM7KrvO2rKd8dOrXrKbYnh8OeJc=; h=Date:To:Subject:List-Id:List-Unsubscribe:List-Archive:List-Post: List-Help:List-Subscribe:From:Reply-To:Cc:From; b=QFzKY9XkQptguSBoJYukyAVHOGS5Td08u21H7bnHj85CsIKUcyoUNTyzXYJVYDzh+ b9v2JRGsiJaQWbUgYUPBSr/IE3MGiJ58Ylz80rtVF0AbN+xIffbck29fVm/JI5FUEO 7er2xHwj8UZz6P0GFKIV8swkG35U4J/TfDPMA7+U= X-Original-To: gcc-patches@gcc.gnu.org Delivered-To: gcc-patches@gcc.gnu.org Received: from mail-ed1-x535.google.com (mail-ed1-x535.google.com [IPv6:2a00:1450:4864:20::535]) by sourceware.org (Postfix) with ESMTPS id 6C97038515D6 for ; Wed, 13 Jul 2022 10:02:54 +0000 (GMT) DMARC-Filter: OpenDMARC Filter v1.4.1 sourceware.org 6C97038515D6 Received: by mail-ed1-x535.google.com with SMTP id m16so13393581edb.11 for ; Wed, 13 Jul 2022 03:02:54 -0700 (PDT) X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20210112; h=x-gm-message-state:date:from:to:cc:subject:message-id:mime-version :content-disposition; bh=26D2LVJGdd5lDQ3vjM7KrvO2rKd8dOrXrKbYnh8OeJc=; b=hvyzHGO59saWUi8ixUwy6MXK8+SVAPR0KdMOanBGhW+0KOlsoVh62XirnRCt5OCJxj JcxnsNVLXQgIa8G5csl/uQdQmSibnjwnF7uDRvCcyRt0q8QOLZ+JDdrQh0BuPtfALMWU oqN47kJQ5IWHLYpFXoSp9B8QFRTzgEaRAAblRFUrTTh4DzpiKF9xbx7xXdE5UZ2RxBFW xBt9HYSEkmgfvhhcA5FTUbUeqxqp0ytNMfffo4Eo8q9YGcJv3j6SS7xurpDOljoe888j H1b/WmjKDXcix/AfeK5AXzuEWr7PJ/ru19ytXaALP1NaAjSkEoQw0Lw45p46mQ5EsFgC kIJQ== X-Gm-Message-State: AJIora9aanfdTEUvWbJB4HdKBO2Xj5fPRPFUmHGbIyAGcBQxP2B2SxTd 3lHh9gNKO3f379nXSye7mlembzWQJQCnJg== X-Google-Smtp-Source: AGRyM1sRALTCgTSAblDdHkSv6RMba331nFHsrNqdIhMc54Hi4EiVWQ+86JAdGT537jPlNfY5F50xmw== X-Received: by 2002:a05:6402:3201:b0:43a:b203:219c with SMTP id g1-20020a056402320100b0043ab203219cmr3631377eda.371.1657706573205; Wed, 13 Jul 2022 03:02:53 -0700 (PDT) Received: from adacore.com ([45.147.211.82]) by smtp.gmail.com with ESMTPSA id d10-20020aa7d5ca000000b0043586bee560sm7566580eds.68.2022.07.13.03.02.52 (version=TLS1_3 cipher=TLS_AES_256_GCM_SHA384 bits=256/256); Wed, 13 Jul 2022 03:02:52 -0700 (PDT) Date: Wed, 13 Jul 2022 10:02:52 +0000 To: gcc-patches@gcc.gnu.org Subject: [Ada] Fix proof of runtime unit System.Arith_64 Message-ID: <20220713100252.GA994608@adacore.com> MIME-Version: 1.0 Content-Disposition: inline X-Spam-Status: No, score=-12.5 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: Pierre-Marie de Rodat via Gcc-patches From: Pierre-Marie de Rodat Reply-To: Pierre-Marie de Rodat Cc: Yannick Moy Errors-To: gcc-patches-bounces+incoming=patchwork.ozlabs.org@gcc.gnu.org Sender: "Gcc-patches" After changes in provers and Why3, changes are needed to recover automatic proof of System.Arith_64. This is the first part of it. Tested on x86_64-pc-linux-gnu, committed on trunk gcc/ada/ * libgnat/s-aridou.adb (Lemma_Mult_Div, Lemma_Powers): New lemmas. (Prove_Sign_Quotient): New local lemma. (Prove_Signs): Expand definition of Big_R and Big_Q in the postcondition. Add intermediate assertions. (Double_Divide): Call new lemma. (Lemma_Div_Eq): Provide body for proving lemma. (Lemma_Powers_Of_2, Lemma_Shift_Without_Drop, Prove_Dividend_Scaling, Prove_Multiplication, Prove_Z_Low): Call lemmas, add intermediate assertions. 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 @@ -438,6 +438,12 @@ is Ghost, Post => X * (Y + Z) = X * Y + X * Z; + procedure Lemma_Mult_Div (A, B : Big_Integer) + with + Ghost, + Pre => B /= 0, + Post => A * B / B = A; + procedure Lemma_Mult_Non_Negative (X, Y : Big_Integer) with Ghost, @@ -469,6 +475,12 @@ is Post => not In_Double_Int_Range (Big_2xxDouble) and then not In_Double_Int_Range (-Big_2xxDouble); + procedure Lemma_Powers (A : Big_Natural; B, C : Natural) + with + Ghost, + Pre => B <= Natural'Last - C, + Post => A**B * A**C = A**(B + C); + procedure Lemma_Powers_Of_2 (M, N : Natural) with Ghost, @@ -606,7 +618,6 @@ is is null; procedure Lemma_Div_Ge (X, Y, Z : Big_Integer) is null; procedure Lemma_Div_Lt (X, Y, Z : Big_Natural) is null; - procedure Lemma_Div_Eq (A, B, S, R : Big_Integer) is null; procedure Lemma_Double_Big_2xxSingle is null; procedure Lemma_Double_Shift (X : Double_Uns; S, S1 : Double_Uns) is null; procedure Lemma_Double_Shift (X : Single_Uns; S, S1 : Natural) is null; @@ -629,6 +640,7 @@ is procedure Lemma_Mult_Non_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; procedure Lemma_Rem_Commutation (X, Y : Double_Uns) is null; procedure Lemma_Rem_Is_Ident (X, Y : Big_Integer) is null; procedure Lemma_Rem_Sign (X, Y : Big_Integer) is null; @@ -864,6 +876,23 @@ is Post => abs Big_Q = Big (Qu); -- Proves correctness of the rounding of the unsigned quotient + procedure Prove_Sign_Quotient + with + Ghost, + Pre => Mult /= 0 + and then Quot = Big (X) / (Big (Y) * Big (Z)) + and then Big_R = Big (X) rem (Big (Y) * Big (Z)) + and then Big_Q = + (if Round then + Round_Quotient (Big (X), Big (Y) * Big (Z), Quot, Big_R) + else Quot), + Post => + (if X >= 0 then + (if Den_Pos then Big_Q >= 0 else Big_Q <= 0) + else + (if Den_Pos then Big_Q <= 0 else Big_Q >= 0)); + -- Proves the correct sign of the signed quotient Big_Q + procedure Prove_Signs with Ghost, @@ -880,7 +909,13 @@ is and then Q = (if (X >= 0) = Den_Pos then To_Int (Qu) else To_Int (-Qu)) and then not (X = Double_Int'First and then Big (Y) * Big (Z) = -1), - Post => Big (R) = Big_R and then Big (Q) = Big_Q; + Post => Big (R) = Big (X) rem (Big (Y) * Big (Z)) + and then + (if Round then + Big (Q) = Round_Quotient (Big (X), Big (Y) * Big (Z), + Big (X) / (Big (Y) * Big (Z)), + Big (R)) + else Big (Q) = Big (X) / (Big (Y) * Big (Z))); -- Proves final signs match the intended result after the unsigned -- division is done. @@ -891,6 +926,7 @@ is procedure Prove_Overflow_Case is null; procedure Prove_Quotient_Zero is null; procedure Prove_Round_To_One is null; + procedure Prove_Sign_Quotient is null; ------------------------- -- Prove_Rounding_Case -- @@ -1056,6 +1092,8 @@ is pragma Assert (Big (Double_Uns (Hi (T2))) >= 1); pragma Assert (Big (Double_Uns (Lo (T2))) >= 0); pragma Assert (Big (Double_Uns (Lo (T1))) >= 0); + pragma Assert (Big_2xxSingle * Big (Double_Uns (Lo (T2))) + + Big (Double_Uns (Lo (T1))) >= 0); pragma Assert (Mult >= Big_2xxDouble * Big (Double_Uns (Hi (T2)))); pragma Assert (Mult >= Big_2xxDouble); if Hi (T2) > 1 then @@ -1064,6 +1102,10 @@ is Mult > Big_2xxDouble); elsif Lo (T2) > 0 then pragma Assert (Big (Double_Uns (Lo (T2))) > 0); + pragma Assert (Big_2xxSingle > 0); + pragma Assert (Big_2xxSingle * Big (Double_Uns (Lo (T2))) > 0); + pragma Assert (Big_2xxSingle * Big (Double_Uns (Lo (T2))) + + Big (Double_Uns (Lo (T1))) > 0); pragma Assert (if X = Double_Int'First and then Round then Mult > Big_2xxDouble); elsif Lo (T1) > 0 then @@ -1138,6 +1180,7 @@ is end if; pragma Assert (abs Big_Q = Big (Qu)); + Prove_Sign_Quotient; -- Set final signs (RM 4.5.5(27-30)) @@ -1225,6 +1268,18 @@ is pragma Assert ((Hi or Lo) = Hi + Lo); end Lemma_Concat_Definition; + ------------------ + -- Lemma_Div_Eq -- + ------------------ + + procedure Lemma_Div_Eq (A, B, S, R : Big_Integer) is + begin + pragma Assert ((A - B) * S = R); + pragma Assert ((A - B) * S / S = R / S); + Lemma_Mult_Div (A - B, S); + pragma Assert (A - B = R / S); + end Lemma_Div_Eq; + ------------------------ -- Lemma_Double_Shift -- ------------------------ @@ -1317,6 +1372,19 @@ is + Big (Double_Uns'(Xlo * Ylo))); end Lemma_Mult_Decomposition; + -------------------- + -- Lemma_Mult_Div -- + -------------------- + + procedure Lemma_Mult_Div (A, B : Big_Integer) is + begin + if B > 0 then + pragma Assert (A * B / B = A); + else + pragma Assert (A * (-B) / (-B) = A); + end if; + end Lemma_Mult_Div; + ------------------- -- Lemma_Neg_Div -- ------------------- @@ -1341,6 +1409,7 @@ is Lemma_Powers_Of_2_Commutation (M); Lemma_Powers_Of_2_Commutation (N); Lemma_Powers_Of_2_Commutation (M + N); + Lemma_Powers (Big (Double_Uns'(2)), M, N); if M + N < Double_Size then pragma Assert (Big (Double_Uns'(2))**M * Big (Double_Uns'(2))**N @@ -1516,6 +1585,8 @@ is pragma Assert (X < 2**(Double_Size - Shift)); pragma Assert (Big (X) < Big_2xx (Double_Size - Shift)); pragma Assert (Y = 2**Shift * X); + Lemma_Lt_Mult (Big (X), Big_2xx (Double_Size - Shift), Big_2xx (Shift), + Big_2xx (Shift) * Big_2xx (Double_Size - Shift)); pragma Assert (Big_2xx (Shift) * Big (X) < Big_2xx (Shift) * Big_2xx (Double_Size - Shift)); Lemma_Powers_Of_2 (Shift, Double_Size - Shift); @@ -2063,8 +2134,8 @@ is begin Lemma_Shift_Left (D (1) & D (2), Scale); - pragma Assert (By (Big_2xxSingle * Big_2xx (Scale) <= Big_2xxDouble, - Big_2xx (Scale) <= Big_2xxSingle)); + Lemma_Ge_Mult (Big_2xxSingle, Big_2xx (Scale), Big_2xxSingle, + Big_2xxSingle * Big_2xx (Scale)); Lemma_Lt_Mult (Big (Double_Uns (D (3))), Big_2xxSingle, Big_2xx (Scale), Big_2xxDouble); Lemma_Shift_Left (Double_Uns (D (3)), Scale); @@ -2225,10 +2296,23 @@ is pragma Assert (Big (Double_Uns (Hi (T3))) + Big (Double_Uns (Hi (T2))) = Big (Double_Uns (S1))); + Lemma_Mult_Distribution (Big_2xxSingle * Big_2xxSingle, + Big (Double_Uns (Hi (T3))), + Big (Double_Uns (Hi (T2)))); pragma Assert (Big_2xxSingle * Big_2xxSingle * Big (Double_Uns (Hi (T2))) + Big_2xxSingle * Big_2xxSingle * Big (Double_Uns (Hi (T3))) = Big_2xxSingle * Big_2xxSingle * Big (Double_Uns (S1))); + pragma Assert (Big (Double_Uns (Q)) * Big (Zu) = + Big_2xxSingle * Big_2xxSingle * Big (Double_Uns (S1)) + + Big_2xxSingle * Big (Double_Uns (S2)) + + Big (Double_Uns (S3))); + pragma Assert + (By (Big (Double_Uns (Q)) * Big (Zu) = Big3 (S1, S2, S3), + Big3 (S1, S2, S3) = + Big_2xxSingle * Big_2xxSingle * Big (Double_Uns (S1)) + + Big_2xxSingle * Big (Double_Uns (S2)) + + Big (Double_Uns (S3)))); end Prove_Multiplication; ----------------------------- @@ -2357,6 +2441,7 @@ is Lemma_Div_Definition (T1, Zlo, T1 / Zlo, T1 rem Zlo); pragma Assert (Double_Uns (Lo (T1 rem Zlo)) = T1 rem Zlo); Lemma_Hi_Lo (T2, Lo (T1 rem Zlo), D (4)); + pragma Assert (T1 rem Zlo < Double_Uns (Zlo)); pragma Assert (T1 rem Zlo + Double_Uns'(1) <= Double_Uns (Zlo)); Lemma_Ge_Commutation (Double_Uns (Zlo), T1 rem Zlo + Double_Uns'(1)); Lemma_Add_Commutation (T1 rem Zlo, 1); @@ -2365,6 +2450,9 @@ is pragma Assert (Mult = Big (Double_Uns (Zlo)) * (Big_2xxSingle * Big (T1 / Zlo) + Big (T2 / Zlo)) + Big (Ru)); + pragma Assert (Big_2xxSingle * Big (Double_Uns (D (2))) + + Big (Double_Uns (D (3))) + < Big_2xxSingle * (Big (Double_Uns (D (2))) + 1)); Lemma_Div_Lt (Big (T1), Big_2xxSingle, Big (Double_Uns (Zlo))); Lemma_Div_Commutation (T1, Double_Uns (Zlo)); Lemma_Lo_Is_Ident (T1 / Zlo);