OpenE2K/gcc
2
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity

[Ada] Fix proof of runtime unit System.Arith_64

Browse Source 
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.
This commit is contained in:
Yannick Moy 2022-07-07 09:38:42 +00:00 committed by Pierre-Marie de Rodat
parent d03a7f8c24
commit 4709037646
1 changed files with 92 additions and 4 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

96
gcc/ada/libgnat/s-aridou.adb
View File

@ -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);