From 4709037646e9b0aa66815f86ebf98a97eb663186 Mon Sep 17 00:00:00 2001 From: Yannick Moy Date: Thu, 7 Jul 2022 09:38:42 +0000 Subject: [PATCH] [Ada] Fix proof of runtime unit System.Arith_64 After changes in provers and Why3, changes are needed to recover automatic proof of System.Arith_64. This is the first part of it. 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. --- gcc/ada/libgnat/s-aridou.adb | 96 ++++++++++++++++++++++++++++++++++++++++++-- 1 file changed, 92 insertions(+), 4 deletions(-) diff --git a/gcc/ada/libgnat/s-aridou.adb b/gcc/ada/libgnat/s-aridou.adb index 880a899..b40e4c3 100644 --- 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); -- 2.7.4