mirror/gcc
1
0
Fork 0
mirror of https://github.com/gcc-mirror/gcc.git synced 2024-11-21 13:40:47 +00:00
Code Issues Actions Packages Projects Releases Wiki Activity

ada: Adapt proofs of light runtime to current version of SPARK

Browse Source 
gcc/ada/ChangeLog:

	* libgnat/a-strmap.adb: Add assert to regain proofs.
	* libgnat/a-strsup.adb: Likewise.
	* libgnat/s-aridou.adb: Add assertions to regain proofs.
	* libgnat/s-arit32.adb: Use Exceptional_Cases to specify Raise.
	* libgnat/s-arit64.adb: Use Round_Quatient from Impl instead of
	redefining it.
	* libgnat/s-arit64.ads: Likewise.
	* libgnat/s-expmod.adb: Regain proof of lemma.
	* libgnat/s-exponn.adb: Likewise.
	* libgnat/s-expont.adb: Likewise.
	* libgnat/s-imgboo.adb: Add local lemma to regain proof.
	* libgnat/s-valuti.ads: Add Always_Terminates on Bad_Value.
This commit is contained in:
Claire Dross 2024-10-18 11:45:29 +02:00 committed by Marc Poulhiès
parent 3e4146b693
commit f62972f5ca
11 changed files with 228 additions and 93 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

3
gcc/ada/libgnat/a-strmap.adb
View File

@ -148,7 +148,7 @@ is
pragma Loop_Invariant (if Map = Identity then J = 0);
pragma Loop_Invariant (J <= Character'Pos (C) + 1);
pragma Loop_Invariant (Result (1 .. J)'Initialized);
pragma Loop_Invariant (for all K in 1 .. J => Result (K)'Initialized);
pragma Loop_Invariant (for all K in 1 .. J => Result (K) <= C);
pragma Loop_Invariant
(SPARK_Proof_Sorted_Character_Sequence (Result (1 .. J)));
@ -404,6 +404,7 @@ is
pragma Loop_Invariant
(for all K in 1 .. J => Result (K) = Map (Domain (K)));
end loop;
pragma Assert (Is_Domain (Map, Domain (1 .. J)));
-- Show the equality of Domain and To_Domain(Map)

2
gcc/ada/libgnat/a-strsup.adb
View File

@ -1627,6 +1627,8 @@ package body Ada.Strings.Superbounded with SPARK_Mode is
Result.Data (K) =
Item (Item'Last - (Max_Length - K) mod Ilen));
end loop;
pragma Assert
(Result.Data (1 .. Max_Length)'Initialized);
when Strings.Error =>
raise Ada.Strings.Length_Error;

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

@ -54,6 +54,10 @@ is
pragma Suppress (Overflow_Check);
pragma Suppress (Range_Check);
pragma Warnings
(Off, "statement has no effect",
Reason => "Ghost code on dead paths is used for verification only");
function To_Uns is new Ada.Unchecked_Conversion (Double_Int, Double_Uns);
function To_Int is new Ada.Unchecked_Conversion (Double_Uns, Double_Int);
@ -123,7 +127,9 @@ is
function "abs" (X : Double_Int) return Double_Uns is
(if X = Double_Int'First
then Double_Uns'(2 ** (Double_Size - 1))
else Double_Uns (Double_Int'(abs X)));
else Double_Uns (Double_Int'(abs X)))
with Post => abs (Big (X)) = Big ("abs"'Result),
Annotate => (GNATprove, Hide_Info, "Expression_Function_Body");
-- Convert absolute value of X to unsigned. Note that we can't just use
-- the expression of the Else since it overflows for X = Double_Int'First.
@ -146,8 +152,7 @@ is
+ Big_2xxSingle * Big (Double_Uns (X2))
+ Big (Double_Uns (X3)))
with
Ghost,
Annotate => (GNATprove, Inline_For_Proof);
Ghost;
-- X1&X2&X3 as a big integer
function Le3 (X1, X2, X3, Y1, Y2, Y3 : Single_Uns) return Boolean
@ -186,7 +191,8 @@ is
-- 0 .. 2 ** (Double_Size - 1) - 1, then the corresponding non-negative
-- signed integer is returned, otherwise constraint error is raised.
procedure Raise_Error;
procedure Raise_Error with
Exceptional_Cases => (Constraint_Error => True);
pragma No_Return (Raise_Error);
-- Raise constraint error with appropriate message
@ -1897,9 +1903,6 @@ is
procedure Raise_Error is
begin
raise Constraint_Error with "Double arithmetic overflow";
pragma Annotate
(GNATprove, Intentional, "exception might be raised",
"Procedure Raise_Error is called to signal input errors");
end Raise_Error;
-------------------
@ -2025,6 +2028,15 @@ is
-- Proves correctness of the multiplication of divisor by quotient to
-- compute amount to subtract.
procedure Prove_Mult_Decomposition_Split2
(D1, D2, D2_Hi, D2_Lo, D3, D4 : Big_Integer)
with
Ghost,
Pre => Is_Mult_Decomposition (D1, D2, D3, D4)
and then D2 = Big_2xxSingle * D2_Hi + D2_Lo,
Post => Is_Mult_Decomposition (D1 + D2_Hi, D2_Lo, D3, D4);
-- Proves decomposition of Mult after splitting second component
procedure Prove_Mult_Decomposition_Split3
(D1, D2, D3, D3_Hi, D3_Lo, D4 : Big_Integer)
with
@ -2327,9 +2339,11 @@ is
Big_2xxSingle * Big_2xxSingle * Big (Double_Uns (Hi (T2)))
+ Big_2xxSingle * Big (T3)
+ Big (Double_Uns (S3)),
Big_2xxSingle * Big (Double_Uns (Lo (T2)))
+ Big_2xxSingle * Big (Double_Uns (Hi (T1)))
= Big_2xxSingle * Big (T3)));
By (Big_2xxSingle * Big (Double_Uns (Lo (T2)))
+ Big_2xxSingle * Big (Double_Uns (Hi (T1)))
= Big_2xxSingle * Big (T3),
Double_Uns (Lo (T2))
+ Double_Uns (Hi (T1)) = T3)));
pragma Assert (Double_Uns (Hi (T3)) + Hi (T2) = Double_Uns (S1));
Lemma_Add_Commutation (Double_Uns (Hi (T3)), Hi (T2));
pragma Assert
@ -2340,6 +2354,14 @@ is
Big (Double_Uns (Hi (T2))));
end Prove_Multiplication;
-------------------------------------
-- Prove_Mult_Decomposition_Split2 --
-------------------------------------
procedure Prove_Mult_Decomposition_Split2
(D1, D2, D2_Hi, D2_Lo, D3, D4 : Big_Integer)
is null;
-------------------------------------
-- Prove_Mult_Decomposition_Split3 --
-------------------------------------
@ -2492,7 +2514,10 @@ is
pragma Assert
(Big (Double_Uns (D (2))) + 1 <= Big (Double_Uns (Zlo)));
Lemma_Div_Definition (T1, Zlo, T1 / Zlo, T1 rem Zlo);
pragma Assert (Double_Uns (Lo (T1 rem Zlo)) = T1 rem Zlo);
pragma Assert
(By (Lo (T1 rem Zlo) = Hi (T2),
By (Double_Uns (Lo (T1 rem Zlo)) = T1 rem Zlo,
T1 rem Zlo <= Double_Uns (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));
@ -2501,24 +2526,26 @@ is
pragma Assert (Big (T1 rem Zlo) + 1 <= Big (Double_Uns (Zlo)));
Lemma_Div_Definition (T2, Zlo, T2 / Zlo, Ru);
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));
(By (Big_2xxSingle * Big (Double_Uns (D (2)))
+ Big (Double_Uns (D (3)))
< Big_2xxSingle * (Big (Double_Uns (D (2))) + 1),
Mult = 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);
pragma Assert
(Big (T2) <= Big_2xxSingle * (Big (Double_Uns (Zlo)) - 1)
+ Big (Double_Uns (D (4))));
Lemma_Hi_Lo (Qu, Lo (T1 / Zlo), Lo (T2 / 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_2xxSingle * Big (T1 / Zlo) + Big (T2 / Zlo),
Big (Qu), Big (Ru));
pragma Assert
(By (Ru < Double_Uns (Zlo), Ru = T2 rem Zlo));
Lemma_Lt_Commutation (Ru, Double_Uns (Zlo));
Lemma_Rev_Div_Definition
(Mult, Big (Double_Uns (Zlo)), Big (Qu), Big (Ru));
@ -2606,34 +2633,51 @@ is
T2 := Double_Uns'(Xhi * Yhi);
Lemma_Hi_Lo (T2, Hi (T2), Lo (T2));
pragma Assert
(Is_Mult_Decomposition
(D1 => Big (Double_Uns (Hi (T2))),
D2 => Big (T3) + Big (Double_Uns (Lo (T2))),
D3 => Big (Double_Uns (D (3))),
D4 => Big (Double_Uns (D (4)))));
T1 := T3 + Lo (T2);
D (2) := Lo (T1);
Lemma_Add_Commutation (T3, Lo (T2));
Lemma_Hi_Lo (T1, Hi (T1), Lo (T1));
Prove_Mult_Decomposition_Split2
(D1 => Big (Double_Uns (Hi (T2))),
D2 => Big (T1),
D2_Lo => Big (Double_Uns (Lo (T1))),
D2_Hi => Big (Double_Uns (Hi (T1))),
D3 => Big (Double_Uns (D (3))),
D4 => Big (Double_Uns (D (4))));
D (1) := Hi (T2) + Hi (T1);
pragma Assert
(Double_Uns (Hi (T2)) + Hi (T1) = Double_Uns (D (1)));
Lemma_Add_Commutation (Double_Uns (Hi (T2)), Hi (T1));
pragma Assert
(Big (Double_Uns (Hi (T2))) + Big (Double_Uns (Hi (T1))) =
Big (Double_Uns (D (1))));
pragma Assert
(Is_Mult_Decomposition (D1 => Big (Double_Uns (D (1))),
D2 => Big (Double_Uns (D (2))),
D3 => Big (Double_Uns (D (3))),
D4 => Big (Double_Uns (D (4)))));
pragma Assert_And_Cut
(D'Initialized
and Is_Mult_Decomposition (D1 => Big (Double_Uns (D (1))),
D2 => Big (Double_Uns (D (2))),
D3 => Big (Double_Uns (D (3))),
D4 => Big (Double_Uns (D (4)))));
else
pragma Assert
(Is_Mult_Decomposition
(D1 => 0,
D2 => Big (Double_Uns (D (2))),
D3 => Big (Double_Uns (D (3)))
+ Big (Double_Uns (Xhi)) * Big (Yu),
D4 => Big (Double_Uns (D (4)))));
D (1) := 0;
pragma Assert
(Is_Mult_Decomposition (D1 => Big (Double_Uns (D (1))),
D2 => Big (Double_Uns (D (2))),
D3 => Big (Double_Uns (D (3))),
D4 => Big (Double_Uns (D (4)))));
pragma Assert_And_Cut
(D'Initialized
and Is_Mult_Decomposition (D1 => Big (Double_Uns (D (1))),
D2 => Big (Double_Uns (D (2))),
D3 => Big (Double_Uns (D (3))),
D4 => Big (Double_Uns (D (4)))));
end if;
else
@ -2686,6 +2730,13 @@ is
end if;
D (1) := 0;
pragma Assert_And_Cut
(D'Initialized
and Is_Mult_Decomposition (D1 => Big (Double_Uns (D (1))),
D2 => Big (Double_Uns (D (2))),
D3 => Big (Double_Uns (D (3))),
D4 => Big (Double_Uns (D (4)))));
end if;
pragma Assert_And_Cut
@ -2914,12 +2965,17 @@ is
(Big (Zu) = Big (Double_Uns'(abs Z)) * Big_2xx (Scale));
end;
end loop;
pragma Assert_And_Cut
(Scale <= Single_Size - 1
and then (Hi (Zu) and Mask) /= 0
and then Mask = Shift_Left (Single_Uns'Last, Single_Size - 1)
and then Zu = Shift_Left (abs Z, Scale)
and then Big (Zu) = Big (Double_Uns'(abs Z)) * Big_2xx (Scale)
and then Mult < Big_2xxDouble * Big (Double_Uns'(abs Z)));
Zhi := Hi (Zu);
Zlo := Lo (Zu);
pragma Assert (Shift = 1);
pragma Assert (Mask = Shift_Left (Single_Uns'Last, Single_Size - 1));
pragma Assert ((Zhi and Mask) /= 0);
pragma Assert (Zhi >= 2 ** (Single_Size - 1));
pragma Assert (Big (Zu) = Big (Double_Uns'(abs Z)) * Big_2xx (Scale));
@ -2949,14 +3005,11 @@ is
D (3) := Lo (T2) or Hi (T3);
D (4) := Lo (T3);
pragma Assert (Big (Double_Uns (Hi (T1))) = Big (Double_Uns (D (1))));
pragma Assert
(Big_2xxSingle * Big_2xxSingle * Big_2xxSingle
* Big (Double_Uns (Hi (T1)))
= Big_2xxSingle * Big_2xxSingle * Big_2xxSingle
* Big (Double_Uns (D (1))));
pragma Assert (D (1) = Hi (T1) and D (2) = (Lo (T1) or Hi (T2))
and D (3) = (Lo (T2) or Hi (T3)) and D (4) = Lo (T3));
Lemma_Substitution (Big_2xxDouble * Big (Zu), Big_2xxDouble, Big (Zu),
Big (Double_Uns'(abs Z)) * Big_2xx (Scale), 0);
pragma Assert (Mult < Big_2xxDouble * Big (Double_Uns'(abs Z)));
Lemma_Lt_Mult (Mult, Big_2xxDouble * Big (Double_Uns'(abs Z)),
Big_2xx (Scale), Big_2xxDouble * Big (Zu));
pragma Assert (Mult >= Big_0);
@ -3040,8 +3093,12 @@ is
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)));
pragma Assert
(By (Big3 (D (J), D (J + 1), 0) + Big_2xxSingle
> Big3 (D (J), D (J + 1), D (J + 2)),
Big3 (D (J), D (J + 1), 0) =
Big_2xxSingle * Big_2xxSingle * Big (Double_Uns (D (J)))
+ Big_2xxSingle * Big (Double_Uns (D (J + 1)))));
pragma Assert (Big (Double_Uns'(0)) = 0);
pragma Assert (Big (D (J) & D (J + 1)) * Big_2xxSingle =
Big_2xxSingle * (Big_2xxSingle * Big (Double_Uns (D (J)))
@ -3107,7 +3164,8 @@ is
while not Le3 (S1, S2, S3, D (J), D (J + 1), D (J + 2)) loop
pragma Loop_Invariant
(for all K in 1 .. J => Qd (K)'Initialized);
(Qd (1)'Initialized
and (if J = 2 then Qd (2)'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));
@ -3131,39 +3189,57 @@ is
pragma Assert (Double_Uns (Qd (J)) - Double_Uns'(1)
= Double_Uns (Qd (J) - 1));
pragma Assert (Big (Double_Uns'(1)) = 1);
Lemma_Substitution (Big3 (S1, S2, S3), Big (Zu),
Big (Double_Uns (Qd (J))) - 1,
Big (Double_Uns (Qd (J) - 1)), 0);
declare
Prev : constant Single_Uns := Qd (J) - 1 with Ghost;
Prev : constant Single_Uns := Qd (J) with Ghost;
begin
Qd (J) := Qd (J) - 1;
pragma Assert (Qd (J) = Prev);
pragma Assert (Qd (J)'Initialized);
if J = 2 then
pragma Assert (Qd (J - 1)'Initialized);
end if;
pragma Assert (for all K in 1 .. J => Qd (K)'Initialized);
Lemma_Substitution (Big3 (S1, S2, S3), Big (Zu),
Big (Double_Uns (Prev)) - 1,
Big (Double_Uns (Qd (J))), 0);
end;
pragma Assert
(Big3 (S1, S2, S3) = Big (Double_Uns (Qd (J))) * Big (Zu));
end loop;
pragma Assert_And_Cut
(Qd (1)'Initialized
and then (if J = 2 then Qd (2)'Initialized and Qd (1) = Qd1)
and then D'Initialized
and then (if J = 2 then D234'Initialized)
and then Big3 (D (J), D (J + 1), D (J + 2)) =
(if J = 1 then D123 else D234)
and then (if J = 1 then D4 = Big (Double_Uns (D (4))))
and then Big3 (S1, S2, S3) =
Big (Double_Uns (Qd (J))) * Big (Zu)
and then Le3 (S1, S2, S3, D (J), D (J + 1), D (J + 2))
and then Big3 (D (J), D (J + 1), D (J + 2)) -
Big3 (S1, S2, S3) < Big (Zu));
-- 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) >
Big3 (D (J), D (J + 1), D (J + 2)) - Big (Zu));
Inline_Le3 (S1, S2, S3, D (J), D (J + 1), D (J + 2));
Sub3 (D (J), D (J + 1), D (J + 2), S1, S2, S3);
declare
D4_G : constant Single_Uns := D (4) with Ghost;
begin
Sub3 (D (J), D (J + 1), D (J + 2), S1, S2, S3);
pragma Assert (if J = 1 then D (4) = D4_G);
pragma Assert
(By
(D'Initialized,
D (1)'Initialized and D (2)'Initialized
and D (3)'Initialized and D (4)'Initialized));
pragma Assert
(Big3 (D (J), D (J + 1), D (J + 2)) =
(if J = 1 then D123 else D234)
- Big3 (S1, S2, S3));
end;
pragma Assert
(Big3 (D (J), D (J + 1), D (J + 2)) < Big (Zu));
pragma Assert (Big3 (D (J), D (J + 1), D (J + 2)) < Big (Zu));
if D (J) > 0 then
Lemma_Double_Big_2xxSingle;
pragma Assert (Big3 (D (J), D (J + 1), D (J + 2)) =
@ -3222,6 +3298,17 @@ is
end if;
end loop;
pragma Assert_And_Cut
(Qd (1)'Initialized and then Qd (2)'Initialized
and then D'Initialized
and then Big_2xxSingle * Big (Double_Uns (D (3)))
+ Big (Double_Uns (D (4))) < Big (Zu)
and then 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))));
end;
-- The two quotient digits are now set, and the remainder of the
@ -3231,16 +3318,9 @@ 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);
pragma Assert
(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))));
Lemma_Hi_Lo (Qu, Qd (1), Qd (2));
Lemma_Hi_Lo (Ru, D (3), D (4));
Lemma_Substitution

4
gcc/ada/libgnat/s-arit32.adb
View File

@ -119,7 +119,9 @@ is
-- 0 .. 2**31 - 1, then the corresponding nonnegative signed integer is
-- returned, otherwise constraint error is raised.
procedure Raise_Error;
procedure Raise_Error with
Always_Terminates,
Exceptional_Cases => (Constraint_Error => True);
pragma No_Return (Raise_Error);
-- Raise constraint error with appropriate message

4
gcc/ada/libgnat/s-arit64.adb
View File

@ -28,6 +28,7 @@
-- Extensive contributions were provided by Ada Core Technologies Inc. --
-- --
------------------------------------------------------------------------------
pragma Assertion_Policy (Ghost => Ignore);
with System.Arith_Double;
@ -51,6 +52,9 @@ is
function Multiply_With_Ovflo_Check64 (X, Y : Int64) return Int64
renames Impl.Multiply_With_Ovflo_Check;
function Round_Quotient (X, Y, Q, R : Big_Integer) return Big_Integer
renames Impl.Round_Quotient;
procedure Scaled_Divide64
(X, Y, Z : Int64;
Q, R : out Int64;

16
gcc/ada/libgnat/s-arit64.ads
View File

@ -125,15 +125,15 @@ is
or else (X < Big (Int64'(0))) = (Y < Big (Int64'(0))))
with Ghost;
function Round_Quotient (X, Y, Q, R : Big_Integer) return Big_Integer is
(if abs R > (abs Y - Big (Int64'(1))) / Big (Int64'(2)) then
(if Same_Sign (X, Y) then Q + Big (Int64'(1))
else Q - Big (Int64'(1)))
else
Q)
with
function Round_Quotient (X, Y, Q, R : Big_Integer) return Big_Integer with
Ghost,
Pre => Y /= 0 and then Q = X / Y and then R = X rem Y;
Pre => Y /= 0 and then Q = X / Y and then R = X rem Y,
Post => Round_Quotient'Result =
(if abs R > (abs Y - Big (Int64'(1))) / Big (Int64'(2)) then
(if Same_Sign (X, Y) then Q + Big (Int64'(1))
else Q - Big (Int64'(1)))
else
Q);
procedure Scaled_Divide64
(X, Y, Z : Int64;

21
gcc/ada/libgnat/s-expmod.adb
View File

@ -149,14 +149,24 @@ is
----------------------
procedure Lemma_Exp_Expand (A : Big_Integer; Exp : Natural) is
procedure Lemma_Exp_Distribution (Exp_1, Exp_2 : Natural) with
Pre => Natural'Last - Exp_2 >= Exp_1,
Post => A ** (Exp_1 + Exp_2) = A ** (Exp_1) * A ** (Exp_2);
----------------------------
-- Lemma_Exp_Distribution --
----------------------------
procedure Lemma_Exp_Distribution (Exp_1, Exp_2 : Natural) is null;
begin
if Exp rem 2 = 0 then
pragma Assert (Exp = Exp / 2 + Exp / 2);
else
pragma Assert (Exp = Exp / 2 + Exp / 2 + 1);
pragma Assert (A ** Exp = A ** (Exp / 2) * A ** (Exp / 2 + 1));
pragma Assert (A ** (Exp / 2 + 1) = A ** (Exp / 2) * A);
pragma Assert (A ** Exp = A ** (Exp / 2) * A ** (Exp / 2) * A);
Lemma_Exp_Distribution (Exp / 2, Exp / 2 + 1);
Lemma_Exp_Distribution (Exp / 2, 1);
end if;
end Lemma_Exp_Expand;
@ -253,7 +263,10 @@ is
Post => Big (Mult (X, Y)) = (Big (X) * Big (Y)) mod M
and then Big (Mult (X, Y)) < M;
procedure Lemma_Mult (X, Y : Unsigned) is null;
procedure Lemma_Mult (X, Y : Unsigned) is
begin
pragma Assert (Big (Mult (X, Y)) = (Big (X) * Big (Y)) mod M);
end Lemma_Mult;
Rest : Big_Integer with Ghost;
-- Ghost variable to hold Factor**Exp between Exp and Factor updates

16
gcc/ada/libgnat/s-exponn.adb
View File

@ -185,14 +185,24 @@ is
----------------------
procedure Lemma_Exp_Expand (A : Big_Integer; Exp : Natural) is
procedure Lemma_Exp_Distribution (Exp_1, Exp_2 : Natural) with
Pre => A /= 0 and then Natural'Last - Exp_2 >= Exp_1,
Post => A ** (Exp_1 + Exp_2) = A ** (Exp_1) * A ** (Exp_2);
----------------------------
-- Lemma_Exp_Distribution --
----------------------------
procedure Lemma_Exp_Distribution (Exp_1, Exp_2 : Natural) is null;
begin
if Exp rem 2 = 0 then
pragma Assert (Exp = Exp / 2 + Exp / 2);
else
pragma Assert (Exp = Exp / 2 + Exp / 2 + 1);
pragma Assert (A ** Exp = A ** (Exp / 2) * A ** (Exp / 2 + 1));
pragma Assert (A ** (Exp / 2 + 1) = A ** (Exp / 2) * A);
pragma Assert (A ** Exp = A ** (Exp / 2) * A ** (Exp / 2) * A);
Lemma_Exp_Distribution (Exp / 2, Exp / 2 + 1);
Lemma_Exp_Distribution (Exp / 2, 1);
end if;
end Lemma_Exp_Expand;

16
gcc/ada/libgnat/s-expont.adb
View File

@ -185,14 +185,24 @@ is
----------------------
procedure Lemma_Exp_Expand (A : Big_Integer; Exp : Natural) is
procedure Lemma_Exp_Distribution (Exp_1, Exp_2 : Natural) with
Pre => A /= 0 and then Natural'Last - Exp_2 >= Exp_1,
Post => A ** (Exp_1 + Exp_2) = A ** (Exp_1) * A ** (Exp_2);
----------------------------
-- Lemma_Exp_Distribution --
----------------------------
procedure Lemma_Exp_Distribution (Exp_1, Exp_2 : Natural) is null;
begin
if Exp rem 2 = 0 then
pragma Assert (Exp = Exp / 2 + Exp / 2);
else
pragma Assert (Exp = Exp / 2 + Exp / 2 + 1);
pragma Assert (A ** Exp = A ** (Exp / 2) * A ** (Exp / 2 + 1));
pragma Assert (A ** (Exp / 2 + 1) = A ** (Exp / 2) * A);
pragma Assert (A ** Exp = A ** (Exp / 2) * A ** (Exp / 2) * A);
Lemma_Exp_Distribution (Exp / 2, Exp / 2 + 1);
Lemma_Exp_Distribution (Exp / 2, 1);
end if;
end Lemma_Exp_Expand;

20
gcc/ada/libgnat/s-imgboo.adb
View File

@ -41,6 +41,20 @@ package body System.Img_Bool
with SPARK_Mode
is
-- Local lemmas
procedure Lemma_Is_First_Non_Space_Ghost (S : String; R : Positive) with
Ghost,
Pre => R in S'Range and then S (R) /= ' '
and then System.Val_Spec.Only_Space_Ghost (S, S'First, R - 1),
Post => System.Val_Spec.First_Non_Space_Ghost (S, S'First, S'Last) = R;
------------------------------------
-- Lemma_Is_First_Non_Space_Ghost --
------------------------------------
procedure Lemma_Is_First_Non_Space_Ghost (S : String; R : Positive) is null;
-------------------
-- Image_Boolean --
-------------------
@ -55,13 +69,11 @@ is
if V then
S (1 .. 4) := "TRUE";
P := 4;
pragma Assert
(System.Val_Spec.First_Non_Space_Ghost (S, S'First, S'Last) = 1);
Lemma_Is_First_Non_Space_Ghost (S, 1);
else
S (1 .. 5) := "FALSE";
P := 5;
pragma Assert
(System.Val_Spec.First_Non_Space_Ghost (S, S'First, S'Last) = 1);
Lemma_Is_First_Non_Space_Ghost (S, 1);
end if;
end Image_Boolean;

1
gcc/ada/libgnat/s-valuti.ads
View File

@ -54,6 +54,7 @@ is
procedure Bad_Value (S : String)
with
Always_Terminates,
Depends => (null => S),
Exceptional_Cases => (others => Standard.False);
pragma No_Return (Bad_Value);