From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: Received: by sourceware.org (Postfix, from userid 1914) id 183023858427; Wed, 5 Jan 2022 11:33:32 +0000 (GMT) DKIM-Filter: OpenDKIM Filter v2.11.0 sourceware.org 183023858427 MIME-Version: 1.0 Content-Transfer-Encoding: 7bit Content-Type: text/plain; charset="utf-8" From: Pierre-Marie de Rodat To: gcc-cvs@gcc.gnu.org Subject: [gcc r12-6226] [Ada] Rename parameter-dependent constants in generic unit X-Act-Checkin: gcc X-Git-Author: Yannick Moy X-Git-Refname: refs/heads/master X-Git-Oldrev: 50d8b1066a46cc134c1accc270c9be1b1cae8bc2 X-Git-Newrev: 1a056c2788630270b37066a1ac76d1e64ac6e194 Message-Id: <20220105113332.183023858427@sourceware.org> Date: Wed, 5 Jan 2022 11:33:32 +0000 (GMT) X-BeenThere: gcc-cvs@gcc.gnu.org X-Mailman-Version: 2.1.29 Precedence: list List-Id: Gcc-cvs mailing list List-Unsubscribe: , List-Archive: List-Help: List-Subscribe: , X-List-Received-Date: Wed, 05 Jan 2022 11:33:32 -0000 https://gcc.gnu.org/g:1a056c2788630270b37066a1ac76d1e64ac6e194 commit r12-6226-g1a056c2788630270b37066a1ac76d1e64ac6e194 Author: Yannick Moy Date: Mon Nov 29 17:52:56 2021 +0100 [Ada] Rename parameter-dependent constants in generic unit gcc/ada/ * libgnat/s-aridou.adb: Apply replacement. Diff: --- gcc/ada/libgnat/s-aridou.adb | 365 +++++++++++++++++++++++-------------------- 1 file changed, 194 insertions(+), 171 deletions(-) diff --git a/gcc/ada/libgnat/s-aridou.adb b/gcc/ada/libgnat/s-aridou.adb index 57d427b147e..c93636a309f 100644 --- a/gcc/ada/libgnat/s-aridou.adb +++ b/gcc/ada/libgnat/s-aridou.adb @@ -64,10 +64,7 @@ is when others => raise Program_Error) with Ghost; - -- Power-of-two constants. Use the names Big_2xx32, Big_2xx63 and Big_2xx64 - -- even if Single_Size might not be 32 and Double_Size might not be 64, as - -- this facilitates code and proof understanding, compared to more generic - -- names. + -- Power-of-two constants pragma Warnings (Off, "non-preelaborable call not allowed in preelaborated unit", @@ -78,13 +75,13 @@ is Big_0 : constant Big_Integer := Big (Double_Uns'(0)) with Ghost; - Big_2xx32 : constant Big_Integer := + Big_2xxSingle : constant Big_Integer := Big (Double_Int'(2 ** Single_Size)) with Ghost; - Big_2xx63 : constant Big_Integer := + Big_2xxDouble_Minus_1 : constant Big_Integer := Big (Double_Uns'(2 ** (Double_Size - 1))) with Ghost; - Big_2xx64 : constant Big_Integer := + Big_2xxDouble : constant Big_Integer := Big (Double_Uns'(2 ** Double_Size - 1)) + 1 with Ghost; pragma Warnings @@ -137,8 +134,9 @@ is -- 2**N as a big integer function Big3 (X1, X2, X3 : Single_Uns) return Big_Integer is - (Big_2xx32 * Big_2xx32 * Big (Double_Uns (X1)) - + Big_2xx32 * Big (Double_Uns (X2)) + Big (Double_Uns (X3))) + (Big_2xxSingle * Big_2xxSingle * Big (Double_Uns (X1)) + + Big_2xxSingle * Big (Double_Uns (X2)) + + Big (Double_Uns (X3))) with Ghost; -- X1&X2&X3 as a big integer @@ -353,8 +351,8 @@ is with Ghost, Pre => Xhi = Hi (Xu) and Xlo = Lo (Xu), - Post => - Big (Xu) = Big_2xx32 * Big (Double_Uns (Xhi)) + Big (Double_Uns (Xlo)); + Post => Big (Xu) = + Big_2xxSingle * Big (Double_Uns (Xhi)) + Big (Double_Uns (Xlo)); procedure Lemma_Hi_Lo_3 (Xu : Double_Uns; Xhi, Xlo : Single_Uns) with @@ -365,7 +363,7 @@ is procedure Lemma_Lo_Is_Ident (X : Double_Uns) with Ghost, - Pre => Big (X) < Big_2xx32, + Pre => Big (X) < Big_2xxSingle, Post => Double_Uns (Lo (X)) = X; procedure Lemma_Lt_Commutation (A, B : Double_Uns) @@ -396,7 +394,7 @@ is procedure Lemma_Mult_Commutation (X, Y, Z : Double_Uns) with Ghost, - Pre => Big (X) * Big (Y) < Big_2xx64 and then Z = X * Y, + Pre => Big (X) * Big (Y) < Big_2xxDouble and then Z = X * Y, Post => Big (X) * Big (Y) = Big (Z); procedure Lemma_Mult_Decomposition @@ -411,9 +409,9 @@ is and then Yhi = Hi (Yu) and then Ylo = Lo (Yu), Post => Mult = - Big_2xx32 * Big_2xx32 * (Big (Double_Uns'(Xhi * Yhi))) - + Big_2xx32 * (Big (Double_Uns'(Xhi * Ylo))) - + Big_2xx32 * (Big (Double_Uns'(Xlo * Yhi))) + Big_2xxSingle * Big_2xxSingle * (Big (Double_Uns'(Xhi * Yhi))) + + Big_2xxSingle * (Big (Double_Uns'(Xhi * Ylo))) + + Big_2xxSingle * (Big (Double_Uns'(Xlo * Yhi))) + (Big (Double_Uns'(Xlo * Ylo))); procedure Lemma_Mult_Distribution (X, Y, Z : Big_Integer) @@ -435,8 +433,8 @@ is procedure Lemma_Not_In_Range_Big2xx64 with - Post => not In_Double_Int_Range (Big_2xx64) - and then not In_Double_Int_Range (-Big_2xx64); + Post => not In_Double_Int_Range (Big_2xxDouble) + and then not In_Double_Int_Range (-Big_2xxDouble); procedure Lemma_Powers_Of_2 (M, N : Natural) with @@ -446,7 +444,7 @@ is and then M + N <= Double_Size, Post => Big_2xx (M) * Big_2xx (N) = - (if M + N = Double_Size then Big_2xx64 else Big_2xx (M + N)); + (if M + N = Double_Size then Big_2xxDouble else Big_2xx (M + N)); procedure Lemma_Powers_Of_2_Commutation (M : Natural) with @@ -454,7 +452,7 @@ is Subprogram_Variant => (Decreases => M), Pre => M <= Double_Size, Post => Big (Double_Uns'(2))**M = - (if M < Double_Size then Big_2xx (M) else Big_2xx64); + (if M < Double_Size then Big_2xx (M) else Big_2xxDouble); procedure Lemma_Powers_Of_2_Increasing (M, N : Natural) with @@ -541,7 +539,7 @@ is procedure Lemma_Word_Commutation (X : Single_Uns) with Ghost, - Post => Big_2xx32 * Big (Double_Uns (X)) + Post => Big_2xxSingle * Big (Double_Uns (X)) = Big (2**Single_Size * Double_Uns (X)); ----------------------------- @@ -772,9 +770,11 @@ is procedure Prove_Quotient_Zero with Ghost, - Pre => Mult >= Big_2xx64 + Pre => Mult >= Big_2xxDouble and then - not (Mult = Big_2xx64 and then X = Double_Int'First and then Round) + not (Mult = Big_2xxDouble + and then X = Double_Int'First + and then Round) and then Q = 0 and then R = X, Post => Big (R) = Big (X) rem (Big (Y) * Big (Z)) @@ -790,7 +790,7 @@ is procedure Prove_Round_To_One with Ghost, - Pre => Mult = Big_2xx64 + Pre => Mult = Big_2xxDouble and then X = Double_Int'First and then Q = (if Den_Pos then -1 else 1) and then R = X @@ -944,28 +944,32 @@ is pragma Assert (Big (T2) = Big (Double_Uns'(Yhi * Zlo)) + Big (Double_Uns'(Ylo * Zhi))); - Lemma_Mult_Distribution (Big_2xx32, Big (Double_Uns'(Yhi * Zlo)), - Big (Double_Uns'(Ylo * Zhi))); - pragma Assert (Mult = Big_2xx32 * Big (T2) + Big (T1)); + Lemma_Mult_Distribution (Big_2xxSingle, + Big (Double_Uns'(Yhi * Zlo)), + Big (Double_Uns'(Ylo * Zhi))); + pragma Assert (Mult = Big_2xxSingle * Big (T2) + Big (T1)); Lemma_Hi_Lo (T1, Hi (T1), Lo (T1)); pragma Assert - (Mult = Big_2xx32 * Big (T2) - + Big_2xx32 * Big (Double_Uns (Hi (T1))) - + Big (Double_Uns (Lo (T1)))); - Lemma_Mult_Distribution (Big_2xx32, Big (T2), - Big (Double_Uns (Hi (T1)))); + (Mult = Big_2xxSingle * Big (T2) + + Big_2xxSingle * Big (Double_Uns (Hi (T1))) + + Big (Double_Uns (Lo (T1)))); + Lemma_Mult_Distribution (Big_2xxSingle, + Big (T2), + Big (Double_Uns (Hi (T1)))); Lemma_Add_Commutation (T2, Hi (T1)); T2 := T2 + Hi (T1); - pragma Assert (Mult = Big_2xx32 * Big (T2) + Big (Double_Uns (Lo (T1)))); + pragma Assert + (Mult = Big_2xxSingle * Big (T2) + Big (Double_Uns (Lo (T1)))); Lemma_Hi_Lo (T2, Hi (T2), Lo (T2)); - Lemma_Mult_Distribution (Big_2xx32, Big (Double_Uns (Hi (T2))), - Big (Double_Uns (Lo (T2)))); + Lemma_Mult_Distribution (Big_2xxSingle, + Big (Double_Uns (Hi (T2))), + Big (Double_Uns (Lo (T2)))); pragma Assert - (Mult = Big_2xx64 * Big (Double_Uns (Hi (T2))) - + Big_2xx32 * Big (Double_Uns (Lo (T2))) - + Big (Double_Uns (Lo (T1)))); + (Mult = Big_2xxDouble * Big (Double_Uns (Hi (T2))) + + Big_2xxSingle * Big (Double_Uns (Lo (T2))) + + Big (Double_Uns (Lo (T1)))); if Hi (T2) /= 0 then R := X; @@ -988,7 +992,7 @@ 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 (Mult >= Big_2xx64); + pragma Assert (Mult >= Big_2xxDouble); if Hi (T2) > 1 then pragma Assert (Big (Double_Uns (Hi (T2))) > 1); elsif Lo (T2) > 0 then @@ -1195,22 +1199,24 @@ is Lemma_Hi_Lo (Yu, Yhi, Ylo); pragma Assert - (Mult = (Big_2xx32 * Big (Double_Uns (Xhi)) + Big (Double_Uns (Xlo))) * - (Big_2xx32 * Big (Double_Uns (Yhi)) + Big (Double_Uns (Ylo)))); + (Mult = + (Big_2xxSingle * Big (Double_Uns (Xhi)) + Big (Double_Uns (Xlo))) * + (Big_2xxSingle * Big (Double_Uns (Yhi)) + Big (Double_Uns (Ylo)))); pragma Assert (Mult = - Big_2xx32 * Big_2xx32 * Big (Double_Uns (Xhi)) * Big (Double_Uns (Yhi)) - + Big_2xx32 * Big (Double_Uns (Xhi)) * Big (Double_Uns (Ylo)) - + Big_2xx32 * Big (Double_Uns (Xlo)) * Big (Double_Uns (Yhi)) - + Big (Double_Uns (Xlo)) * Big (Double_Uns (Ylo))); - Lemma_Deep_Mult_Commutation (Big_2xx32 * Big_2xx32, Xhi, Yhi); - Lemma_Deep_Mult_Commutation (Big_2xx32, Xhi, Ylo); - Lemma_Deep_Mult_Commutation (Big_2xx32, Xlo, Yhi); + Big_2xxSingle + * Big_2xxSingle * Big (Double_Uns (Xhi)) * Big (Double_Uns (Yhi)) + + Big_2xxSingle * Big (Double_Uns (Xhi)) * Big (Double_Uns (Ylo)) + + Big_2xxSingle * Big (Double_Uns (Xlo)) * Big (Double_Uns (Yhi)) + + Big (Double_Uns (Xlo)) * Big (Double_Uns (Ylo))); + Lemma_Deep_Mult_Commutation (Big_2xxSingle * Big_2xxSingle, Xhi, Yhi); + Lemma_Deep_Mult_Commutation (Big_2xxSingle, Xhi, Ylo); + Lemma_Deep_Mult_Commutation (Big_2xxSingle, Xlo, Yhi); Lemma_Mult_Commutation (Xlo, Ylo); pragma Assert (Mult = - Big_2xx32 * Big_2xx32 * Big (Double_Uns'(Xhi * Yhi)) - + Big_2xx32 * Big (Double_Uns'(Xhi * Ylo)) - + Big_2xx32 * Big (Double_Uns'(Xlo * Yhi)) - + Big (Double_Uns'(Xlo * Ylo))); + Big_2xxSingle * Big_2xxSingle * Big (Double_Uns'(Xhi * Yhi)) + + Big_2xxSingle * Big (Double_Uns'(Xhi * Ylo)) + + Big_2xxSingle * Big (Double_Uns'(Xlo * Yhi)) + + Big (Double_Uns'(Xlo * Ylo))); end Lemma_Mult_Decomposition; ------------------- @@ -1383,9 +1389,9 @@ is Pre => Xhi /= 0 and then Yhi /= 0 and then Mult = - Big_2xx32 * Big_2xx32 * (Big (Double_Uns'(Xhi * Yhi))) - + Big_2xx32 * (Big (Double_Uns'(Xhi * Ylo))) - + Big_2xx32 * (Big (Double_Uns'(Xlo * Yhi))) + Big_2xxSingle * Big_2xxSingle * (Big (Double_Uns'(Xhi * Yhi))) + + Big_2xxSingle * (Big (Double_Uns'(Xhi * Ylo))) + + Big_2xxSingle * (Big (Double_Uns'(Xlo * Yhi))) + (Big (Double_Uns'(Xlo * Ylo))), Post => not In_Double_Int_Range (Big (X) * Big (Y)); @@ -1393,7 +1399,7 @@ is with Ghost, Pre => In_Double_Int_Range (Big (X) * Big (Y)) - and then Mult = Big_2xx32 * Big (T2) + Big (Double_Uns (Lo (T1))) + and then Mult = Big_2xxSingle * Big (T2) + Big (Double_Uns (Lo (T1))) and then Hi (T2) = 0, Post => Mult = Big (Lo (T2) & Lo (T1)); @@ -1416,14 +1422,14 @@ is procedure Prove_Result_Too_Large with Ghost, - Pre => Mult = Big_2xx32 * Big (T2) + Big (Double_Uns (Lo (T1))) + Pre => Mult = Big_2xxSingle * Big (T2) + Big (Double_Uns (Lo (T1))) and then Hi (T2) /= 0, Post => not In_Double_Int_Range (Big (X) * Big (Y)); procedure Prove_Too_Large with Ghost, - Pre => abs (Big (X) * Big (Y)) >= Big_2xx64, + Pre => abs (Big (X) * Big (Y)) >= Big_2xxDouble, Post => not In_Double_Int_Range (Big (X) * Big (Y)); -------------------------- @@ -1432,10 +1438,10 @@ is procedure Prove_Both_Too_Large is begin - pragma Assert - (Mult >= Big_2xx32 * Big_2xx32 * Big (Double_Uns'(Xhi * Yhi))); + pragma Assert (Mult >= + Big_2xxSingle * Big_2xxSingle * Big (Double_Uns'(Xhi * Yhi))); pragma Assert (Double_Uns (Xhi) * Double_Uns (Yhi) >= 1); - pragma Assert (Mult >= Big_2xx32 * Big_2xx32); + pragma Assert (Mult >= Big_2xxSingle * Big_2xxSingle); Prove_Too_Large; end Prove_Both_Too_Large; @@ -1446,9 +1452,9 @@ is procedure Prove_Final_Decomposition is begin Lemma_Hi_Lo (T2, Hi (T2), Lo (T2)); - pragma Assert (Mult = Big_2xx32 * Big (Double_Uns (Lo (T2))) - + Big (Double_Uns (Lo (T1)))); - pragma Assert (Mult <= Big_2xx63); + pragma Assert (Mult = Big_2xxSingle * Big (Double_Uns (Lo (T2))) + + Big (Double_Uns (Lo (T1)))); + pragma Assert (Mult <= Big_2xxDouble_Minus_1); Lemma_Mult_Commutation (X, Y); pragma Assert (Mult = abs (Big (X * Y))); Lemma_Word_Commutation (Lo (T2)); @@ -1490,12 +1496,12 @@ is procedure Prove_Result_Too_Large is begin - pragma Assert (Mult >= Big_2xx32 * Big (T2)); + pragma Assert (Mult >= Big_2xxSingle * Big (T2)); Lemma_Hi_Lo (T2, Hi (T2), Lo (T2)); - pragma Assert - (Mult >= Big_2xx32 * Big_2xx32 * Big (Double_Uns (Hi (T2)))); + pragma Assert (Mult >= + Big_2xxSingle * Big_2xxSingle * Big (Double_Uns (Hi (T2)))); pragma Assert (Double_Uns (Hi (T2)) >= 1); - pragma Assert (Mult >= Big_2xx32 * Big_2xx32); + pragma Assert (Mult >= Big_2xxSingle * Big_2xxSingle); Prove_Too_Large; end Prove_Result_Too_Large; @@ -1532,9 +1538,9 @@ is pragma Assert (Big (T2) = Big (Double_Uns'(Xhi * Ylo)) + Big (Double_Uns'(Xlo * Yhi))); - Lemma_Mult_Distribution (Big_2xx32, Big (Double_Uns'(Xhi * Ylo)), + Lemma_Mult_Distribution (Big_2xxSingle, Big (Double_Uns'(Xhi * Ylo)), Big (Double_Uns'(Xlo * Yhi))); - pragma Assert (Mult = Big_2xx32 * Big (T2) + Big (T1)); + pragma Assert (Mult = Big_2xxSingle * Big (T2) + Big (T1)); Lemma_Add_Commutation (T2, Hi (T1)); pragma Assert (Big (T2 + Hi (T1)) = Big (T2) + Big (Double_Uns (Hi (T1)))); @@ -1542,7 +1548,8 @@ is T2 := T2 + Hi (T1); Lemma_Hi_Lo (T1, Hi (T1), Lo (T1)); - pragma Assert (Mult = Big_2xx32 * Big (T2) + Big (Double_Uns (Lo (T1)))); + pragma Assert + (Mult = Big_2xxSingle * Big (T2) + Big (Double_Uns (Lo (T1)))); if Hi (T2) /= 0 then Prove_Result_Too_Large; @@ -1656,19 +1663,21 @@ is Pre => D'Initialized and then Scale <= Single_Size and then Mult = - Big_2xx32 * Big_2xx32 * Big_2xx32 * Big (Double_Uns (D (1))) - + Big_2xx32 * Big_2xx32 * Big (Double_Uns (D (2))) - + Big_2xx32 * Big (Double_Uns (D (3))) + 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 Big (D (1) & D (2)) * Big_2xx (Scale) < Big_2xx64 + and then Big (D (1) & D (2)) * Big_2xx (Scale) < Big_2xxDouble and then T1 = Shift_Left (D (1) & D (2), Scale) and then T2 = Shift_Left (Double_Uns (D (3)), Scale) and then T3 = Shift_Left (Double_Uns (D (4)), Scale), Post => Mult * Big_2xx (Scale) = - Big_2xx32 * Big_2xx32 * Big_2xx32 * Big (Double_Uns (Hi (T1))) - + Big_2xx32 * Big_2xx32 * Big (Double_Uns (Lo (T1) or + Big_2xxSingle + * Big_2xxSingle * Big_2xxSingle * Big (Double_Uns (Hi (T1))) + + Big_2xxSingle * Big_2xxSingle * Big (Double_Uns (Lo (T1) or Hi (T2))) - + Big_2xx32 * Big (Double_Uns (Lo (T2) or + + Big_2xxSingle * Big (Double_Uns (Lo (T2) or Hi (T3))) + Big (Double_Uns (Lo (T3))); -- Proves the scaling of the 4-digit dividend actually multiplies it by @@ -1712,7 +1721,8 @@ is procedure Prove_Overflow with Ghost, - Pre => Z /= 0 and then Mult >= Big_2xx64 * Big (Double_Uns'(abs Z)), + Pre => Z /= 0 + and then Mult >= Big_2xxDouble * Big (Double_Uns'(abs Z)), Post => not In_Double_Int_Range (Big (X) * Big (Y) / Big (Z)) and then not In_Double_Int_Range (Round_Quotient (Big (X) * Big (Y), Big (Z), @@ -1762,7 +1772,7 @@ is with Ghost, Pre => In_Double_Int_Range (Big_Q) - and then abs Big_Q = Big_2xx64, + and then abs Big_Q = Big_2xxDouble, Post => False; -- Proves the inconsistency when Q is equal to Big_2xx64 @@ -1833,9 +1843,10 @@ is and then D'Initialized and then Hi (abs Z) = 0 and then Lo (abs Z) = Zlo - and then Mult = Big_2xx32 * Big_2xx32 * Big (Double_Uns (D (2))) - + Big_2xx32 * Big (Double_Uns (D (3))) - + Big (Double_Uns (D (4))) + and then Mult = + Big_2xxSingle * Big_2xxSingle * Big (Double_Uns (D (2))) + + Big_2xxSingle * Big (Double_Uns (D (3))) + + Big (Double_Uns (D (4))) and then D (2) < Zlo and then Quot = (Big (X) * Big (Y)) / Big (Z) and then Big_R = (Big (X) * Big (Y)) rem Big (Z) @@ -1855,14 +1866,15 @@ is begin Lemma_Hi_Lo (D (1) & D (2), D (1), D (2)); pragma Assert (Mult * Big_2xx (Scale) = - Big_2xx32 * Big_2xx32 * Big_2xx (Scale) * Big (D (1) & D (2)) - + Big_2xx32 * Big_2xx (Scale) * Big (Double_Uns (D (3))) - + Big_2xx (Scale) * Big (Double_Uns (D (4)))); + Big_2xxSingle + * Big_2xxSingle * Big_2xx (Scale) * Big (D (1) & D (2)) + + Big_2xxSingle * Big_2xx (Scale) * Big (Double_Uns (D (3))) + + Big_2xx (Scale) * Big (Double_Uns (D (4)))); pragma Assert (Big_2xx (Scale) > 0); - Lemma_Lt_Mult (Big (Double_Uns (D (3))), Big_2xx32, - Big_2xx (Scale), Big_2xx64); - Lemma_Lt_Mult (Big (Double_Uns (D (4))), Big_2xx32, - Big_2xx (Scale), Big_2xx64); + Lemma_Lt_Mult (Big (Double_Uns (D (3))), Big_2xxSingle, + Big_2xx (Scale), Big_2xxDouble); + Lemma_Lt_Mult (Big (Double_Uns (D (4))), Big_2xxSingle, + Big_2xx (Scale), Big_2xxDouble); Lemma_Mult_Commutation (2 ** Scale, D (1) & D (2), T1); declare Big_D12 : constant Big_Integer := @@ -1870,8 +1882,8 @@ is Big_T1 : constant Big_Integer := Big (T1); begin pragma Assert (Big_D12 = Big_T1); - pragma Assert (Big_2xx32 * Big_2xx32 * Big_D12 - = Big_2xx32 * Big_2xx32 * Big_T1); + pragma Assert (Big_2xxSingle * Big_2xxSingle * Big_D12 + = Big_2xxSingle * Big_2xxSingle * Big_T1); end; Lemma_Mult_Commutation (2 ** Scale, Double_Uns (D (3)), T2); declare @@ -1880,7 +1892,7 @@ is Big_T2 : constant Big_Integer := Big (T2); begin pragma Assert (Big_D3 = Big_T2); - pragma Assert (Big_2xx32 * Big_D3 = Big_2xx32 * Big_T2); + pragma Assert (Big_2xxSingle * Big_D3 = Big_2xxSingle * Big_T2); end; Lemma_Mult_Commutation (2 ** Scale, Double_Uns (D (4)), T3); declare @@ -1891,7 +1903,9 @@ is pragma Assert (Big_D4 = Big_T3); end; pragma Assert (Mult * Big_2xx (Scale) = - Big_2xx32 * Big_2xx32 * Big (T1) + Big_2xx32 * Big (T2) + Big (T3)); + Big_2xxSingle * Big_2xxSingle * Big (T1) + + Big_2xxSingle * Big (T2) + + Big (T3)); Lemma_Hi_Lo (T1, Hi (T1), Lo (T1)); Lemma_Hi_Lo (T2, Hi (T2), Lo (T2)); Lemma_Hi_Lo (T3, Hi (T3), Lo (T3)); @@ -1912,10 +1926,10 @@ is Lemma_Hi_Lo (T2, Hi (T2), Lo (T2)); Lemma_Hi_Lo (T3, Hi (T3), S2); pragma Assert (Big (Double_Uns (Q)) * Big (Zu) = - Big_2xx32 * Big_2xx32 * Big (Double_Uns (Hi (T2))) - + Big_2xx32 * Big_2xx32 * Big (Double_Uns (Hi (T3))) - + Big_2xx32 * Big (Double_Uns (S2)) - + Big (Double_Uns (S3))); + Big_2xxSingle * Big_2xxSingle * Big (Double_Uns (Hi (T2))) + + Big_2xxSingle * Big_2xxSingle * Big (Double_Uns (Hi (T3))) + + Big_2xxSingle * Big (Double_Uns (S2)) + + Big (Double_Uns (S3))); pragma Assert (Double_Uns (Hi (T3)) + Hi (T2) = Double_Uns (S1)); Lemma_Add_Commutation (Double_Uns (Hi (T3)), Hi (T2)); pragma Assert @@ -1938,7 +1952,7 @@ is procedure Prove_Overflow is begin - Lemma_Div_Ge (Mult, Big_2xx64, Big (Double_Uns'(abs Z))); + Lemma_Div_Ge (Mult, Big_2xxDouble, Big (Double_Uns'(abs Z))); Lemma_Abs_Commutation (Z); Lemma_Abs_Div_Commutation (Big (X) * Big (Y), Big (Z)); end Prove_Overflow; @@ -1962,9 +1976,9 @@ is Lemma_Lt_Commutation (Double_Uns (D (J)), Double_Uns (Zhi)); Lemma_Gt_Mult (Big (Double_Uns (Zhi)), Big (Double_Uns (D (J))) + 1, - Big_2xx32, Big (D (J) & D (J + 1))); + Big_2xxSingle, Big (D (J) & D (J + 1))); Lemma_Div_Lt - (Big (D (J) & D (J + 1)), Big_2xx32, Big (Double_Uns (Zhi))); + (Big (D (J) & D (J + 1)), Big_2xxSingle, Big (Double_Uns (Zhi))); Lemma_Div_Commutation (D (J) & D (J + 1), Double_Uns (Zhi)); Lemma_Lo_Is_Ident ((D (J) & D (J + 1)) / Zhi); Lemma_Div_Definition (D (J) & D (J + 1), Zhi, Double_Uns (Qd (J)), @@ -1973,10 +1987,10 @@ is ((D (J) & D (J + 1)) rem Zhi, Double_Uns (Zhi)); Lemma_Gt_Mult ((Big (Double_Uns (Qd (J))) + 1) * Big (Double_Uns (Zhi)), - Big (D (J) & D (J + 1)) + 1, Big_2xx32, + Big (D (J) & D (J + 1)) + 1, Big_2xxSingle, Big3 (D (J), D (J + 1), D (J + 2))); Lemma_Hi_Lo (Zu, Zhi, Lo (Zu)); - Lemma_Gt_Mult (Big (Zu), Big_2xx32 * Big (Double_Uns (Zhi)), + Lemma_Gt_Mult (Big (Zu), Big_2xxSingle * Big (Double_Uns (Zhi)), Big (Double_Uns (Qd (J))) + 1, Big3 (D (J), D (J + 1), D (J + 2))); Lemma_Div_Lt (Big3 (D (J), D (J + 1), D (J + 2)), @@ -1989,7 +2003,7 @@ is procedure Prove_Q_Too_Big is begin - pragma Assert (Big_Q = Big_2xx64 or Big_Q = -Big_2xx64); + pragma Assert (Big_Q = Big_2xxDouble or Big_Q = -Big_2xxDouble); Lemma_Not_In_Range_Big2xx64; end Prove_Q_Too_Big; @@ -2055,16 +2069,16 @@ is Lemma_Div_Definition (T2, Zlo, T2 / Zlo, Ru); pragma Assert (Mult = Big (Double_Uns (Zlo)) * - (Big_2xx32 * Big (T1 / Zlo) + Big (T2 / Zlo)) + Big (Ru)); - Lemma_Div_Lt (Big (T1), Big_2xx32, Big (Double_Uns (Zlo))); + (Big_2xxSingle * Big (T1 / Zlo) + Big (T2 / Zlo)) + Big (Ru)); + Lemma_Div_Lt (Big (T1), Big_2xxSingle, Big (Double_Uns (Zlo))); Lemma_Div_Commutation (T1, Double_Uns (Zlo)); Lemma_Lo_Is_Ident (T1 / Zlo); - Lemma_Div_Lt (Big (T2), Big_2xx32, Big (Double_Uns (Zlo))); + Lemma_Div_Lt (Big (T2), Big_2xxSingle, Big (Double_Uns (Zlo))); Lemma_Div_Commutation (T2, Double_Uns (Zlo)); Lemma_Lo_Is_Ident (T2 / Zlo); Lemma_Hi_Lo (Qu, Lo (T1 / Zlo), Lo (T2 / Zlo)); Lemma_Substitution (Mult, Big (Double_Uns (Zlo)), - Big_2xx32 * Big (T1 / Zlo) + Big (T2 / Zlo), + Big_2xxSingle * Big (T1 / Zlo) + Big (T2 / Zlo), Big (Qu), Big (Ru)); Lemma_Lt_Commutation (Ru, Double_Uns (Zlo)); Lemma_Rev_Div_Definition @@ -2110,7 +2124,7 @@ is T2 := D (3) + Lo (T1); - Lemma_Mult_Distribution (Big_2xx32, + Lemma_Mult_Distribution (Big_2xxSingle, Big (Double_Uns (D (3))), Big (Double_Uns (Lo (T1)))); Lemma_Hi_Lo (T2, Hi (T2), Lo (T2)); @@ -2159,9 +2173,10 @@ is Big (Double_Uns (D (1)))); pragma Assert (Mult = - Big_2xx32 * Big_2xx32 * Big_2xx32 * Big (Double_Uns (D (1))) - + Big_2xx32 * Big_2xx32 * Big (Double_Uns (D (2))) - + Big_2xx32 * Big (Double_Uns (D (3))) + 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)))); else @@ -2169,9 +2184,10 @@ is end if; pragma Assert (Mult = - Big_2xx32 * Big_2xx32 * Big_2xx32 * Big (Double_Uns (D (1))) - + Big_2xx32 * Big_2xx32 * Big (Double_Uns (D (2))) - + Big_2xx32 * Big (Double_Uns (D (3))) + 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)))); else @@ -2182,7 +2198,7 @@ is T2 := D (3) + Lo (T1); - Lemma_Mult_Distribution (Big_2xx32, + Lemma_Mult_Distribution (Big_2xxSingle, Big (Double_Uns (D (3))), Big (Double_Uns (Lo (T1)))); Lemma_Hi_Lo (T2, Hi (T2), Lo (T2)); @@ -2196,27 +2212,28 @@ is pragma Assert (Big (Double_Uns (Hi (T1))) + Big (Double_Uns (Hi (T2))) = Big (Double_Uns (D (2)))); - pragma Assert - (Mult = Big_2xx32 * Big_2xx32 * Big (Double_Uns (D (2))) - + Big_2xx32 * Big (Double_Uns (D (3))) + pragma Assert (Mult = + Big_2xxSingle * Big_2xxSingle * Big (Double_Uns (D (2))) + + Big_2xxSingle * Big (Double_Uns (D (3))) + Big (Double_Uns (D (4)))); else D (2) := 0; - pragma Assert - (Mult = Big_2xx32 * Big_2xx32 * Big (Double_Uns (D (2))) - + Big_2xx32 * Big (Double_Uns (D (3))) + pragma Assert (Mult = + Big_2xxSingle * Big_2xxSingle * Big (Double_Uns (D (2))) + + Big_2xxSingle * Big (Double_Uns (D (3))) + Big (Double_Uns (D (4)))); end if; D (1) := 0; end if; - pragma Assert - (Mult = Big_2xx32 * Big_2xx32 * Big_2xx32 * Big (Double_Uns (D (1))) - + Big_2xx32 * Big_2xx32 * Big (Double_Uns (D (2))) - + Big_2xx32 * Big (Double_Uns (D (3))) - + Big (Double_Uns (D (4)))); + pragma Assert (Mult = + 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)))); -- Now it is time for the dreaded multiple precision division. First an -- easy case, check for the simple case of a one digit divisor. @@ -2225,14 +2242,14 @@ is if D (1) /= 0 or else D (2) >= Zlo then if D (1) > 0 then pragma Assert - (Mult >= Big_2xx32 * Big_2xx32 * Big_2xx32 + (Mult >= Big_2xxSingle * Big_2xxSingle * Big_2xxSingle * Big (Double_Uns (D (1)))); - pragma Assert (Mult >= Big_2xx64 * Big_2xx32); + pragma Assert (Mult >= Big_2xxDouble * Big_2xxSingle); Lemma_Ge_Commutation (2 ** Single_Size, Zu); - pragma Assert (Mult >= Big_2xx64 * Big (Zu)); + pragma Assert (Mult >= Big_2xxDouble * Big (Zu)); else Lemma_Ge_Commutation (Double_Uns (D (2)), Zu); - pragma Assert (Mult >= Big_2xx64 * Big (Zu)); + pragma Assert (Mult >= Big_2xxDouble * Big (Zu)); end if; Prove_Overflow; @@ -2387,7 +2404,7 @@ is Lemma_Lt_Commutation (D (1) & D (2), abs Z); Lemma_Lt_Mult (Big (D (1) & D (2)), Big (Double_Uns'(abs Z)), Big_2xx (Scale), - Big_2xx64); + Big_2xxDouble); T1 := Shift_Left (D (1) & D (2), Scale); T2 := Shift_Left (Double_Uns (D (3)), Scale); @@ -2401,21 +2418,23 @@ is D (4) := Lo (T3); pragma Assert (Mult * Big_2xx (Scale) = - Big_2xx32 * Big_2xx32 * Big_2xx32 * Big (Double_Uns (D (1))) - + Big_2xx32 * Big_2xx32 * Big (Double_Uns (D (2))) - + Big_2xx32 * Big (Double_Uns (D (3))) + 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)))); - Lemma_Substitution (Big_2xx64 * Big (Zu), Big_2xx64, Big (Zu), + Lemma_Substitution (Big_2xxDouble * Big (Zu), Big_2xxDouble, Big (Zu), Big (Double_Uns'(abs Z)) * Big_2xx (Scale), 0); - Lemma_Lt_Mult (Mult, Big_2xx64 * Big (Double_Uns'(abs Z)), - Big_2xx (Scale), Big_2xx64 * Big (Zu)); - Lemma_Div_Lt (Mult * Big_2xx (Scale), Big (Zu), Big_2xx64); - Lemma_Substitution (Mult * Big_2xx (Scale), Big_2xx32, - Big_2xx32 * Big_2xx32 * Big (Double_Uns (D (1))) - + Big_2xx32 * Big (Double_Uns (D (2))) - + Big (Double_Uns (D (3))), - Big3 (D (1), D (2), D (3)), - Big (Double_Uns (D (4)))); + Lemma_Lt_Mult (Mult, Big_2xxDouble * Big (Double_Uns'(abs Z)), + Big_2xx (Scale), Big_2xxDouble * Big (Zu)); + Lemma_Div_Lt (Mult * Big_2xx (Scale), Big (Zu), Big_2xxDouble); + 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)))); -- Loop to compute quotient digits, runs twice for Qd (1) and Qd (2) @@ -2427,7 +2446,7 @@ is Ghost, Pre => X1 = 0, Post => - Big_2xx32 * Big3 (X1, X2, X3) + Big (Double_Uns (X4)) + Big_2xxSingle * Big3 (X1, X2, X3) + Big (Double_Uns (X4)) = Big3 (X2, X3, X4); --------------------------- @@ -2463,10 +2482,11 @@ is Qd (J) := Single_Uns'Last; Lemma_Gt_Mult (Big (Zu), Big (D (J) & D (J + 1)) + 1, - Big_2xx32, + Big_2xxSingle, Big3 (D (J), D (J + 1), D (J + 2))); Lemma_Div_Lt - (Big3 (D (J), D (J + 1), D (J + 2)), Big_2xx32, Big (Zu)); + (Big3 (D (J), D (J + 1), D (J + 2)), + Big_2xxSingle, Big (Zu)); else Qd (J) := Lo ((D (J) & D (J + 1)) / Zhi); @@ -2548,50 +2568,52 @@ is pragma Assert (Big3 (D (J), D (J + 1), D (J + 2)) < Big (Zu)); if D (J) > 0 then - pragma Assert (Big_2xx32 * Big_2xx32 = Big_2xx64); + pragma Assert + (Big_2xxSingle * Big_2xxSingle = Big_2xxDouble); pragma Assert (Big3 (D (J), D (J + 1), D (J + 2)) = - Big_2xx32 * Big_2xx32 - * Big (Double_Uns (D (J))) - + Big_2xx32 * Big (Double_Uns (D (J + 1))) - + Big (Double_Uns (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)))); pragma Assert (Big3 (D (J), D (J + 1), D (J + 2)) = - Big_2xx64 * Big (Double_Uns (D (J))) - + Big_2xx32 * Big (Double_Uns (D (J + 1))) - + Big (Double_Uns (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 (Big3 (D (J), D (J + 1), D (J + 2)) >= - Big_2xx64 * Big (Double_Uns (D (J)))); + Big_2xxDouble * Big (Double_Uns (D (J)))); Lemma_Ge_Commutation (Double_Uns (D (J)), Double_Uns'(1)); pragma Assert - (Big3 (D (J), D (J + 1), D (J + 2)) >= Big_2xx64); + (Big3 (D (J), D (J + 1), D (J + 2)) >= Big_2xxDouble); pragma Assert (False); end if; if J = 1 then Qd1 := Qd (1); Lemma_Substitution - (Mult * Big_2xx (Scale), Big_2xx32, D123, + (Mult * Big_2xx (Scale), Big_2xxSingle, D123, Big3 (D (1), D (2), D (3)) + Big3 (S1, S2, S3), Big (Double_Uns (D (4)))); Prove_First_Iteration (D (1), D (2), D (3), D (4)); - Lemma_Substitution (Mult * Big_2xx (Scale), Big_2xx32, + 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))); else pragma Assert (Qd1 = Qd (1)); pragma Assert - (Big_2xx32 * Big_2xx32 * Big (Double_Uns (D (2))) = 0); + (Big_2xxSingle * Big_2xxSingle * Big (Double_Uns (D (2))) + = 0); pragma Assert (Mult * Big_2xx (Scale) = - Big_2xx32 * Big (Double_Uns (Qd (1))) * Big (Zu) + Big_2xxSingle * Big (Double_Uns (Qd (1))) * Big (Zu) + Big3 (S1, S2, S3) + Big3 (D (2), D (3), D (4))); pragma Assert (Mult * Big_2xx (Scale) = - Big_2xx32 * Big (Double_Uns (Qd (1))) * Big (Zu) - + Big (Double_Uns (Qd (2))) * Big (Zu) - + Big_2xx32 * Big (Double_Uns (D (3))) - + Big (Double_Uns (D (4)))); + 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)))); end if; end loop; end; @@ -2608,15 +2630,16 @@ is pragma Assert (Mult * Big_2xx (Scale) = - Big_2xx32 * Big (Double_Uns (Qd (1))) * Big (Zu) - + Big (Double_Uns (Qd (2))) * Big (Zu) - + Big_2xx32 * Big (Double_Uns (D (3))) - + Big (Double_Uns (D (4)))); + 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)))); Lemma_Hi_Lo (Qu, Qd (1), Qd (2)); Lemma_Hi_Lo (Ru, D (3), D (4)); Lemma_Substitution (Mult * Big_2xx (Scale), Big (Zu), - Big_2xx32 * Big (Double_Uns (Qd (1))) + Big (Double_Uns (Qd (2))), + Big_2xxSingle * Big (Double_Uns (Qd (1))) + + Big (Double_Uns (Qd (2))), Big (Qu), Big (Ru)); Prove_Rescaling;