* [COMMITTED] ada: Adapt proof of System.Arith_Double to remove CVC4
@ 2023-07-10 12:43 Marc Poulhiès
0 siblings, 0 replies; only message in thread
From: Marc Poulhiès @ 2023-07-10 12:43 UTC (permalink / raw)
To: gcc-patches; +Cc: Yannick Moy
From: Yannick Moy <moy@adacore.com>
The proof of System.Arith_Double still required the use of
CVC4, now replaced by its successor cvc5. Adapt the proof to be
able to remove CVC4 in the proof of run-time units.
gcc/ada/
* libgnat/s-aridou.adb (Lemma_Div_Mult): New simple lemma.
(Lemma_Powers_Of_2_Commutation): State post in else branch.
(Lemma_Div_Pow2): Introduce local lemma and use it.
(Scaled_Divide): Use cut operations in assertions, lemmas, new
assertions. Introduce local lemma and use it.
Tested on x86_64-pc-linux-gnu, committed on master.
---
gcc/ada/libgnat/s-aridou.adb | 84 ++++++++++++++++++++++++++++++++----
1 file changed, 75 insertions(+), 9 deletions(-)
diff --git a/gcc/ada/libgnat/s-aridou.adb b/gcc/ada/libgnat/s-aridou.adb
index 831590ce387..7ebf8682b32 100644
--- a/gcc/ada/libgnat/s-aridou.adb
+++ b/gcc/ada/libgnat/s-aridou.adb
@@ -301,6 +301,11 @@ is
Pre => A * S = B * S + R and then S /= 0,
Post => A = B + R / S;
+ procedure Lemma_Div_Mult (X : Big_Natural; Y : Big_Positive)
+ with
+ Ghost,
+ Post => X / Y * Y > X - Y;
+
procedure Lemma_Double_Big_2xxSingle
with
Ghost,
@@ -639,6 +644,7 @@ 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_Mult (X : Big_Natural; Y : Big_Positive) 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;
@@ -1449,6 +1455,10 @@ is
(Double_Uns'(2 ** (M - 1)), 2, Double_Uns'(2**M));
pragma Assert (Big (Double_Uns'(2))**M = Big_2xx (M));
end if;
+ else
+ pragma Assert
+ (Big (Double_Uns'(2))**M =
+ (if M < Double_Size then Big_2xx (M) else Big_2xxDouble));
end if;
end Lemma_Powers_Of_2_Commutation;
@@ -1537,6 +1547,19 @@ is
"Q is the quotient of X by Div");
procedure Lemma_Div_Pow2 (X : Double_Uns; I : Natural) is
+
+ -- Local lemmas
+
+ procedure Lemma_Mult_Le (X, Y, Z : Double_Uns)
+ with
+ Ghost,
+ Pre => X <= 1,
+ Post => X * Z <= Z;
+
+ procedure Lemma_Mult_Le (X, Y, Z : Double_Uns) is null;
+
+ -- Local variables
+
Div1 : constant Double_Uns := Double_Uns'(2) ** I;
Div2 : constant Double_Uns := Double_Uns'(2);
Left : constant Double_Uns := X / Div1 / Div2;
@@ -1544,8 +1567,12 @@ is
pragma Assert (R2 <= Div2 - 1);
R1 : constant Double_Uns := X - X / Div1 * Div1;
pragma Assert (R1 < Div1);
+
+ -- Start of processing for Lemma_Div_Pow2
+
begin
pragma Assert (X = Left * (Div1 * Div2) + R2 * Div1 + R1);
+ Lemma_Mult_Le (R2, Div2 - 1, Div1);
pragma Assert (R2 * Div1 + R1 < Div1 * Div2);
Lemma_Quot_Rem (X, Div1 * Div2, Left, R2 * Div1 + R1);
pragma Assert (Left = X / (Div1 * Div2));
@@ -2937,7 +2964,10 @@ is
Big_2xxSingle * Big (Double_Uns (D (3)))
+ Big (Double_Uns (D (4))));
pragma Assert
- (Big (D (1) & D (2)) < Big (Zu));
+ (By (Big (D (1) & D (2)) < Big (Zu),
+ Big_2xxDouble * (Big (Zu) - Big (D (1) & D (2))) >
+ Big_2xxSingle * Big (Double_Uns (D (3)))
+ + Big (Double_Uns (D (4)))));
-- Loop to compute quotient digits, runs twice for Qd (1) and Qd (2)
@@ -2962,7 +2992,7 @@ is
-- Local ghost variables
Qd1 : Single_Uns := 0 with Ghost;
- D234 : Big_Integer with Ghost;
+ D234 : Big_Integer with Ghost, Relaxed_Initialization;
D123 : constant Big_Integer := Big3 (D (1), D (2), D (3))
with Ghost;
D4 : constant Big_Integer := Big (Double_Uns (D (4)))
@@ -3015,8 +3045,10 @@ is
Lemma_Div_Lt
(Big3 (D (J), D (J + 1), D (J + 2)),
Big_2xxSingle, Big (Zu));
- pragma Assert (Big (Double_Uns (Qd (J))) >=
- Big3 (D (J), D (J + 1), D (J + 2)) / Big (Zu));
+ pragma Assert
+ (By (Big (Double_Uns (Qd (J))) >=
+ Big3 (D (J), D (J + 1), D (J + 2)) / Big (Zu),
+ Big (Double_Uns (Qd (J))) = Big_2xxSingle - 1));
else
Qd (J) := Lo ((D (J) & D (J + 1)) / Zhi);
@@ -3025,6 +3057,7 @@ is
end if;
pragma Assert (for all K in 1 .. J => Qd (K)'Initialized);
+ Lemma_Div_Mult (Big3 (D (J), D (J + 1), D (J + 2)), Big (Zu));
Lemma_Gt_Mult
(Big (Double_Uns (Qd (J))),
Big3 (D (J), D (J + 1), D (J + 2)) / Big (Zu),
@@ -3094,6 +3127,11 @@ is
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);
end;
pragma Assert
@@ -3156,11 +3194,18 @@ is
else
pragma Assert (Qd1 = Qd (1));
pragma Assert
- (Mult * Big_2xx (Scale) =
+ (By (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))));
+ + Big (Double_Uns (D (4))),
+ By (Mult * Big_2xx (Scale) =
+ Big_2xxSingle * Big (Double_Uns (Qd (1))) * Big (Zu)
+ + Big3 (D (2), D (3), D (4)) + Big3 (S1, S2, S3),
+ Mult * Big_2xx (Scale) =
+ Big_2xxSingle * Big (Double_Uns (Qd (1))) * Big (Zu)
+ + D234)));
+
end if;
end loop;
end;
@@ -3193,11 +3238,32 @@ is
Ru := Shift_Right (Ru, Scale);
- Lemma_Shift_Right (Zu, Scale);
+ declare
+ -- Local lemma required to help automatic provers
+ procedure Lemma_Div_Congruent
+ (X, Y : Big_Natural;
+ Z : Big_Positive)
+ with
+ Ghost,
+ Pre => X = Y,
+ Post => X / Z = Y / Z;
+
+ procedure Lemma_Div_Congruent
+ (X, Y : Big_Natural;
+ Z : Big_Positive)
+ is null;
- Zu := Shift_Right (Zu, Scale);
+ begin
+ Lemma_Shift_Right (Zu, Scale);
+ Lemma_Div_Congruent (Big (Zu),
+ Big (Double_Uns'(abs Z)) * Big_2xx (Scale),
+ Big_2xx (Scale));
+
+ Zu := Shift_Right (Zu, Scale);
- Lemma_Simplify (Big (Double_Uns'(abs Z)), Big_2xx (Scale));
+ Lemma_Simplify (Big (Double_Uns'(abs Z)), Big_2xx (Scale));
+ pragma Assert (Big (Zu) = Big (Double_Uns'(abs Z)));
+ end;
end if;
pragma Assert (Big (Ru) = abs Big_R);
--
2.40.0
^ permalink raw reply [flat|nested] only message in thread
only message in thread, other threads:[~2023-07-10 12:43 UTC | newest]
Thread overview: (only message) (download: mbox.gz / follow: Atom feed)
-- links below jump to the message on this page --
2023-07-10 12:43 [COMMITTED] ada: Adapt proof of System.Arith_Double to remove CVC4 Marc Poulhiès
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox;
as well as URLs for read-only IMAP folder(s) and NNTP newsgroup(s).