* [Ada] Recover proof of Scaled_Divide in System.Arith_64
@ 2022-09-02 7:53 Marc Poulhiès
0 siblings, 0 replies; only message in thread
From: Marc Poulhiès @ 2022-09-02 7:53 UTC (permalink / raw)
To: gcc-patches; +Cc: Yannick Moy
[-- Attachment #1: Type: text/plain, Size: 320 bytes --]
Proof of Scaled_Divide was impacted by changes in provers and Why3.
Recover it partially, leaving some unproved basic inferences to be
further investigated.
Tested on x86_64-pc-linux-gnu, committed on trunk
gcc/ada/
* libgnat/s-aridou.adb: Add or rework ghost code.
* libgnat/s-aridou.ads: Add Big_Positive subtype.
[-- Attachment #2: patch.diff --]
[-- Type: text/x-diff, Size: 27148 bytes --]
diff --git a/gcc/ada/libgnat/s-aridou.adb b/gcc/ada/libgnat/s-aridou.adb
--- a/gcc/ada/libgnat/s-aridou.adb
+++ b/gcc/ada/libgnat/s-aridou.adb
@@ -126,7 +126,7 @@ is
Pre => B /= 0;
-- Length doubling remainder
- function Big_2xx (N : Natural) return Big_Integer is
+ function Big_2xx (N : Natural) return Big_Positive is
(Big (Double_Uns'(2 ** N)))
with
Ghost,
@@ -141,6 +141,13 @@ is
with Ghost;
-- X1&X2&X3 as a big integer
+ function Big3 (X1, X2, X3 : Big_Integer) return Big_Integer is
+ (Big_2xxSingle * Big_2xxSingle * X1
+ + Big_2xxSingle * X2
+ + X3)
+ with Ghost;
+ -- Version of Big3 on big integers
+
function Le3 (X1, X2, X3, Y1, Y2, Y3 : Single_Uns) return Boolean
with
Post => Le3'Result = (Big3 (X1, X2, X3) <= Big3 (Y1, Y2, Y3));
@@ -234,6 +241,17 @@ is
Pre => X /= Double_Uns'Last,
Post => Big (X + Double_Uns'(1)) = Big (X) + 1;
+ procedure Lemma_Big_Of_Double_Uns (X : Double_Uns)
+ with
+ Ghost,
+ Post => Big (X) < Big_2xxDouble;
+
+ procedure Lemma_Big_Of_Double_Uns_Of_Single_Uns (X : Single_Uns)
+ with
+ Ghost,
+ Post => Big (Double_Uns (X)) >= 0
+ and then Big (Double_Uns (X)) < Big_2xxSingle;
+
procedure Lemma_Bounded_Powers_Of_2_Increasing (M, N : Natural)
with
Ghost,
@@ -447,9 +465,9 @@ is
procedure Lemma_Mult_Non_Negative (X, Y : Big_Integer)
with
Ghost,
- Pre => (X >= Big_0 and then Y >= Big_0)
- or else (X <= Big_0 and then Y <= Big_0),
- Post => X * Y >= Big_0;
+ Pre => (X >= 0 and then Y >= 0)
+ or else (X <= 0 and then Y <= 0),
+ Post => X * Y >= 0;
procedure Lemma_Mult_Non_Positive (X, Y : Big_Integer)
with
@@ -458,6 +476,13 @@ is
or else (X >= Big_0 and then Y <= Big_0),
Post => X * Y <= Big_0;
+ procedure Lemma_Mult_Positive (X, Y : Big_Integer)
+ with
+ Ghost,
+ Pre => (X > Big_0 and then Y > Big_0)
+ or else (X < Big_0 and then Y < Big_0),
+ Post => X * Y > Big_0;
+
procedure Lemma_Neg_Div (X, Y : Big_Integer)
with
Ghost,
@@ -604,6 +629,8 @@ is
procedure Lemma_Abs_Range (X : Big_Integer) is null;
procedure Lemma_Add_Commutation (X : Double_Uns; Y : Single_Uns) is null;
procedure Lemma_Add_One (X : Double_Uns) is null;
+ procedure Lemma_Big_Of_Double_Uns (X : Double_Uns) is null;
+ procedure Lemma_Big_Of_Double_Uns_Of_Single_Uns (X : Single_Uns) is null;
procedure Lemma_Bounded_Powers_Of_2_Increasing (M, N : Natural) is null;
procedure Lemma_Deep_Mult_Commutation
(Factor : Big_Integer;
@@ -638,6 +665,7 @@ is
procedure Lemma_Mult_Distribution (X, Y, Z : Big_Integer) is null;
procedure Lemma_Mult_Non_Negative (X, Y : Big_Integer) is null;
procedure Lemma_Mult_Non_Positive (X, Y : Big_Integer) is null;
+ procedure Lemma_Mult_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;
@@ -1888,7 +1916,7 @@ is
-- Local ghost variables
- Mult : constant Big_Integer := abs (Big (X) * Big (Y)) with Ghost;
+ Mult : constant Big_Natural := abs (Big (X) * Big (Y)) with Ghost;
Quot : Big_Integer with Ghost;
Big_R : Big_Integer with Ghost;
Big_Q : Big_Integer with Ghost;
@@ -1955,6 +1983,15 @@ is
-- Proves correctness of the multiplication of divisor by quotient to
-- compute amount to subtract.
+ procedure Prove_Mult_Decomposition_Split3
+ (D1, D2, D3, D3_Hi, D3_Lo, D4 : Big_Integer)
+ with
+ Ghost,
+ Pre => Is_Mult_Decomposition (D1, D2, D3, D4)
+ and then D3 = Big_2xxSingle * D3_Hi + D3_Lo,
+ Post => Is_Mult_Decomposition (D1, D2 + D3_Hi, D3_Lo, D4);
+ -- Proves decomposition of Mult after splitting third component
+
procedure Prove_Negative_Dividend
with
Ghost,
@@ -2066,6 +2103,27 @@ is
else abs Quot);
-- Proves correctness of the rounding of the unsigned quotient
+ procedure Prove_Scaled_Mult_Decomposition_Regroup24
+ (D1, D2, D3, D4 : Big_Integer)
+ with
+ Ghost,
+ Pre => Scale < Double_Size
+ and then Is_Scaled_Mult_Decomposition (D1, D2, D3, D4),
+ Post => Is_Scaled_Mult_Decomposition
+ (0, Big_2xxSingle * D1 + D2, 0, Big_2xxSingle * D3 + D4);
+ -- Proves scaled decomposition of Mult after regrouping on second and
+ -- fourth component.
+
+ procedure Prove_Scaled_Mult_Decomposition_Regroup3
+ (D1, D2, D3, D4 : Big_Integer)
+ with
+ Ghost,
+ Pre => Scale < Double_Size
+ and then Is_Scaled_Mult_Decomposition (D1, D2, D3, D4),
+ Post => Is_Scaled_Mult_Decomposition (0, 0, Big3 (D1, D2, D3), D4);
+ -- Proves scaled decomposition of Mult after regrouping on third
+ -- component.
+
procedure Prove_Sign_R
with
Ghost,
@@ -2315,6 +2373,14 @@ is
+ Big (Double_Uns (S3))));
end Prove_Multiplication;
+ -------------------------------------
+ -- Prove_Mult_Decomposition_Split3 --
+ -------------------------------------
+
+ procedure Prove_Mult_Decomposition_Split3
+ (D1, D2, D3, D3_Hi, D3_Lo, D4 : Big_Integer)
+ is null;
+
-----------------------------
-- Prove_Negative_Dividend --
-----------------------------
@@ -2413,6 +2479,22 @@ is
end if;
end Prove_Rounding_Case;
+ -----------------------------------------------
+ -- Prove_Scaled_Mult_Decomposition_Regroup24 --
+ -----------------------------------------------
+
+ procedure Prove_Scaled_Mult_Decomposition_Regroup24
+ (D1, D2, D3, D4 : Big_Integer)
+ is null;
+
+ ----------------------------------------------
+ -- Prove_Scaled_Mult_Decomposition_Regroup3 --
+ ----------------------------------------------
+
+ procedure Prove_Scaled_Mult_Decomposition_Regroup3
+ (D1, D2, D3, D4 : Big_Integer)
+ is null;
+
------------------
-- Prove_Sign_R --
------------------
@@ -2585,29 +2667,15 @@ is
T2 := D (3) + Lo (T1);
Lemma_Add_Commutation (Double_Uns (D (3)), Lo (T1));
- pragma Assert
- (Is_Mult_Decomposition
- (D1 => 0,
- D2 => Big (Double_Uns'(Xhi * Yhi)) + Big (Double_Uns (D (2)))
- + Big (Double_Uns (Hi (T1))),
- D3 => Big (T2),
- D4 => Big (Double_Uns (D (4)))));
Lemma_Hi_Lo (T2, Hi (T2), Lo (T2));
- pragma Assert
- (By (Is_Mult_Decomposition
- (D1 => 0,
- D2 => Big (Double_Uns'(Xhi * Yhi)) + Big (Double_Uns (D (2)))
- + Big (Double_Uns (Hi (T1))) + Big (Double_Uns (Hi (T2))),
- D3 => Big (Double_Uns (Lo (T2))),
- D4 => Big (Double_Uns (D (4)))),
- By (Big_2xxSingle * Big (T2) =
- Big_2xxSingle * Big_2xxSingle * Big (Double_Uns (Hi (T2)))
- + Big_2xxSingle * Big (Double_Uns (Lo (T2))),
- Big_2xxSingle *
- (Big_2xxSingle * Big (Double_Uns (Hi (T2)))
- + Big (Double_Uns (Lo (T2))))
- = Big_2xxSingle * Big_2xxSingle * Big (Double_Uns (Hi (T2)))
- + Big_2xxSingle * Big (Double_Uns (Lo (T2))))));
+ Prove_Mult_Decomposition_Split3
+ (D1 => 0,
+ D2 => Big (Double_Uns'(Xhi * Yhi)) + Big (Double_Uns (D (2)))
+ + Big (Double_Uns (Hi (T1))),
+ D3 => Big (T2),
+ D3_Hi => Big (Double_Uns (Hi (T2))),
+ D3_Lo => Big (Double_Uns (Lo (T2))),
+ D4 => Big (Double_Uns (D (4))));
D (3) := Lo (T2);
T3 := D (2) + Hi (T1);
@@ -2807,8 +2875,20 @@ is
pragma Assert
(Mult >= Big_2xxSingle * Big_2xxSingle * Big_2xxSingle
* Big (Double_Uns (D (1))));
+ Lemma_Double_Big_2xxSingle;
+ Lemma_Mult_Positive (Big_2xxDouble, Big_2xxSingle);
+ Lemma_Ge_Mult (Big (Double_Uns (D (1))),
+ 1,
+ Big_2xxDouble * Big_2xxSingle,
+ Big_2xxDouble * Big_2xxSingle);
+ Lemma_Mult_Positive (Big_2xxSingle, Big (Double_Uns (D (1))));
+ Lemma_Ge_Mult (Big_2xxSingle * Big_2xxSingle, Big_2xxDouble,
+ Big_2xxSingle * Big (Double_Uns (D (1))),
+ Big_2xxDouble * Big_2xxSingle);
pragma Assert (Mult >= Big_2xxDouble * Big_2xxSingle);
Lemma_Ge_Commutation (2 ** Single_Size, Zu);
+ Lemma_Ge_Mult (Big_2xxSingle, Big (Zu), Big_2xxDouble,
+ Big_2xxDouble * Big (Zu));
pragma Assert (Mult >= Big_2xxDouble * Big (Zu));
else
Lemma_Ge_Commutation (Double_Uns (D (2)), Zu);
@@ -2887,6 +2967,13 @@ is
Post => Shift / 2 = 2 ** (Log_Single_Size - (Inter + 1))
and then (Shift = 2 or (Shift / 2) mod 2 = 0);
+ procedure Prove_Prev_And_Mask (Prev, Mask : Single_Uns)
+ with
+ Ghost,
+ Pre => Prev /= 0
+ and then (Prev and Mask) = 0,
+ Post => (Prev and not Mask) /= 0;
+
procedure Prove_Shift_Progress
with
Ghost,
@@ -2918,6 +3005,7 @@ is
-- Local lemma null bodies --
-----------------------------
+ procedure Prove_Prev_And_Mask (Prev, Mask : Single_Uns) is null;
procedure Prove_Power is null;
procedure Prove_Shifting is null;
procedure Prove_Shift_Progress is null;
@@ -2941,6 +3029,15 @@ is
if (Hi (Zu) and Mask) = 0 then
Zu := Shift_Left (Zu, Shift);
+ pragma Assert ((Hi (Zu_Prev) and Mask_Prev) /= 0);
+ pragma Assert
+ (By ((Hi (Zu_Prev) and Mask_Prev and Mask) = 0,
+ (Hi (Zu_Prev) and Mask) = 0
+ and then
+ (Hi (Zu_Prev) and Mask_Prev and Mask)
+ = (Hi (Zu_Prev) and Mask and Mask_Prev)
+ ));
+ Prove_Prev_And_Mask (Hi (Zu_Prev) and Mask_Prev, Mask);
Prove_Shifting;
pragma Assert (Big (Zu_Prev) =
Big (Double_Uns'(abs Z)) * Big_2xx (Scale));
@@ -2986,6 +3083,7 @@ is
-- not change the invariant that (D (1) & D (2)) < Zu.
Lemma_Lt_Commutation (D (1) & D (2), abs Z);
+ Lemma_Big_Of_Double_Uns (Zu);
Lemma_Lt_Mult (Big (D (1) & D (2)),
Big (Double_Uns'(abs Z)), Big_2xx (Scale),
Big_2xxDouble);
@@ -3007,82 +3105,21 @@ is
* Big (Double_Uns (Hi (T1)))
= Big_2xxSingle * Big_2xxSingle * Big_2xxSingle
* Big (Double_Uns (D (1))));
-
- pragma Assert
- (Is_Scaled_Mult_Decomposition
- (Big (Double_Uns (D (1))),
- Big (Double_Uns (D (2))),
- Big (Double_Uns (D (3))),
- Big (Double_Uns (D (4)))));
- pragma Assert
- (By (Is_Scaled_Mult_Decomposition
- (0,
- 0,
- Big_2xxSingle * Big_2xxSingle * Big (Double_Uns (D (1)))
- + Big_2xxSingle * Big (Double_Uns (D (2)))
- + Big (Double_Uns (D (3))),
- Big (Double_Uns (D (4)))),
- Big_2xxSingle *
- (Big_2xxSingle * Big_2xxSingle * Big (Double_Uns (D (1)))
- + Big_2xxSingle * Big (Double_Uns (D (2)))
- + Big (Double_Uns (D (3))))
- + Big (Double_Uns (D (4))) =
- 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
- (By (Mult * Big_2xx (Scale) =
- 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))),
- Is_Scaled_Mult_Decomposition
- (Big (Double_Uns (D (1))),
- Big (Double_Uns (D (2))),
- Big (Double_Uns (D (3))),
- Big (Double_Uns (D (4))))))));
- 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))));
Lemma_Substitution (Big_2xxDouble * Big (Zu), Big_2xxDouble, Big (Zu),
Big (Double_Uns'(abs Z)) * Big_2xx (Scale), 0);
Lemma_Lt_Mult (Mult, Big_2xxDouble * Big (Double_Uns'(abs Z)),
Big_2xx (Scale), Big_2xxDouble * Big (Zu));
+ pragma Assert (Mult >= Big_0);
+ pragma Assert (Big_2xx (Scale) >= Big_0);
+ Lemma_Mult_Non_Negative (Mult, Big_2xx (Scale));
Lemma_Div_Lt (Mult * Big_2xx (Scale), Big (Zu), Big_2xxDouble);
Lemma_Concat_Definition (D (1), D (2));
Lemma_Double_Big_2xxSingle;
- pragma Assert
- (Big_2xxSingle *
- (Big_2xxSingle * Big_2xxSingle * Big (Double_Uns (D (1)))
- + Big_2xxSingle * Big (Double_Uns (D (2)))
- + Big (Double_Uns (D (3))))
- + Big (Double_Uns (D (4)))
- = Big_2xxSingle * Big_2xxSingle *
- (Big_2xxSingle * Big (Double_Uns (D (1)))
- + Big (Double_Uns (D (2))))
- + Big_2xxSingle * Big (Double_Uns (D (3)))
- + Big (Double_Uns (D (4))));
- pragma Assert
- (By (Is_Scaled_Mult_Decomposition
- (0,
- Big_2xxSingle * Big (Double_Uns (D (1)))
- + Big (Double_Uns (D (2))),
- 0,
- Big_2xxSingle * Big (Double_Uns (D (3)))
- + Big (Double_Uns (D (4)))),
- Big_2xxSingle * Big_2xxSingle *
- (Big_2xxSingle * Big (Double_Uns (D (1)))
- + Big (Double_Uns (D (2)))) =
- Big_2xxSingle *
- Big_2xxSingle * Big_2xxSingle * Big (Double_Uns (D (1)))
- + Big_2xxSingle * Big_2xxSingle * Big (Double_Uns (D (2)))));
+ Prove_Scaled_Mult_Decomposition_Regroup24
+ (Big (Double_Uns (D (1))),
+ Big (Double_Uns (D (2))),
+ Big (Double_Uns (D (3))),
+ Big (Double_Uns (D (4))));
Lemma_Substitution
(Mult * Big_2xx (Scale), Big_2xxSingle * Big_2xxSingle,
Big_2xxSingle * Big (Double_Uns (D (1)))
@@ -3115,10 +3152,20 @@ is
-- Local ghost variables
Qd1 : Single_Uns := 0 with Ghost;
+ D234 : Big_Integer := 0 with Ghost;
D123 : constant Big_Integer := Big3 (D (1), D (2), D (3))
with Ghost;
+ D4 : constant Big_Integer := Big (Double_Uns (D (4)))
+ with Ghost;
begin
+ Prove_Scaled_Mult_Decomposition_Regroup3
+ (Big (Double_Uns (D (1))),
+ Big (Double_Uns (D (2))),
+ Big (Double_Uns (D (3))),
+ Big (Double_Uns (D (4))));
+ pragma Assert (Mult * Big_2xx (Scale) = Big_2xxSingle * D123 + D4);
+
for J in 1 .. 2 loop
Lemma_Hi_Lo (D (J) & D (J + 1), D (J), D (J + 1));
pragma Assert (Big (D (J) & D (J + 1)) < Big (Zu));
@@ -3138,6 +3185,7 @@ is
Qd (J) := Single_Uns'Last;
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)));
@@ -3158,6 +3206,8 @@ 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));
else
Qd (J) := Lo ((D (J) & D (J + 1)) / Zhi);
@@ -3165,6 +3215,7 @@ is
Prove_Qd_Calculation_Part_1 (J);
end if;
+ pragma Assert (for all K in 1 .. J => Qd (K)'Initialized);
Lemma_Gt_Mult
(Big (Double_Uns (Qd (J))),
Big3 (D (J), D (J + 1), D (J + 2)) / Big (Zu),
@@ -3199,7 +3250,9 @@ is
Lemma_Hi_Lo_3 (Zu, Zhi, Zlo);
while not Le3 (S1, S2, S3, D (J), D (J + 1), D (J + 2)) loop
- pragma Loop_Invariant (Qd (J)'Initialized);
+ pragma Loop_Invariant
+ (for all K in 1 .. J => Qd (K)'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));
pragma Loop_Invariant
@@ -3240,6 +3293,7 @@ is
-- 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) >
@@ -3256,19 +3310,32 @@ is
* 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_2xxDouble * Big (Double_Uns (D (J)))
- + Big_2xxSingle * Big (Double_Uns (D (J + 1)))
- + Big (Double_Uns (D (J + 2))));
pragma Assert (Big_2xxSingle >= 0);
+ Lemma_Big_Of_Double_Uns_Of_Single_Uns (D (J + 1));
pragma Assert (Big (Double_Uns (D (J + 1))) >= 0);
+ Lemma_Mult_Non_Negative
+ (Big_2xxSingle, Big (Double_Uns (D (J + 1))));
pragma Assert
- (Big_2xxSingle * Big (Double_Uns (D (J + 1))) >= 0);
- pragma Assert
- (Big_2xxSingle * Big (Double_Uns (D (J + 1)))
- + Big (Double_Uns (D (J + 2))) >= 0);
- pragma Assert (Big3 (D (J), D (J + 1), D (J + 2)) >=
- Big_2xxDouble * Big (Double_Uns (D (J))));
+ (By (Big3 (D (J), D (J + 1), D (J + 2)) >=
+ Big_2xxSingle * Big_2xxSingle
+ * Big (Double_Uns (D (J))),
+ By (Big3 (D (J), D (J + 1), 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))),
+ Big3 (D (J), D (J + 1), 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))))
+ and then
+ By (Big_2xxSingle * Big (Double_Uns (D (J + 1)))
+ + Big (Double_Uns (D (J + 2))) >= 0,
+ Big_2xxSingle * Big (Double_Uns (D (J + 1))) >= 0
+ and then
+ Big (Double_Uns (D (J + 2))) >= 0
+ )));
Lemma_Ge_Commutation (Double_Uns (D (J)), Double_Uns'(1));
Lemma_Ge_Mult (Big (Double_Uns (D (J))),
Big (Double_Uns'(1)),
@@ -3283,6 +3350,8 @@ is
if J = 1 then
Qd1 := Qd (1);
+ D234 := Big3 (D (2), D (3), D (4));
+ pragma Assert (D4 = Big (Double_Uns (D (4))));
Lemma_Substitution
(Mult * Big_2xx (Scale), Big_2xxSingle, D123,
Big3 (D (1), D (2), D (3)) + Big3 (S1, S2, S3),
@@ -3291,23 +3360,38 @@ is
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)));
+ D234);
else
pragma Assert (Qd1 = Qd (1));
pragma Assert
- (Big_2xxSingle * Big_2xxSingle * Big (Double_Uns (D (2)))
- = 0);
- pragma Assert
- (Mult * Big_2xx (Scale) =
- Big_2xxSingle * Big (Double_Uns (Qd (1))) * Big (Zu)
+ (By (Mult * Big_2xx (Scale) =
+ Big_2xxSingle * Big (Double_Uns (Qd1)) * Big (Zu)
+ Big3 (S1, S2, S3)
- + Big3 (D (2), D (3), D (4)));
+ + Big3 (D (2), D (3), D (4)),
+ Big3 (D (2), D (3), D (4)) = D234 - Big3 (S1, S2, S3)));
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))),
+ Big_2xxSingle * Big (Double_Uns (Qd (1))) * Big (Zu)
+ = Big_2xxSingle * Big (Double_Uns (Qd1)) * Big (Zu)
+ and then
+ Big3 (S1, S2, S3) = Big (Double_Uns (Qd (2))) * Big (Zu)
+ and then
+ By (Big3 (D (2), D (3), D (4))
+ = Big_2xxSingle * Big (Double_Uns (D (3)))
+ + Big (Double_Uns (D (4))),
+ Big3 (D (2), D (3), D (4))
+ = Big_2xxSingle * Big_2xxSingle *
+ Big (Double_Uns (D (2)))
+ + Big_2xxSingle * Big (Double_Uns (D (3)))
+ + Big (Double_Uns (D (4)))
+ and then
+ Big_2xxSingle * Big_2xxSingle * Big (Double_Uns (D (2)))
+ = 0)
+ ));
end if;
end loop;
end;
@@ -3319,6 +3403,7 @@ 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);
@@ -3440,14 +3525,14 @@ is
Ghost,
Pre => X2 < Y2,
Post => Big3 (X1, X2 - Y2, X3)
- = Big3 (X1, X2, X3) + Big3 (1, 0, 0) - Big3 (0, Y2, 0);
+ = Big3 (X1, X2, X3) + Big3 (Single_Uns'(1), 0, 0) - Big3 (0, Y2, 0);
procedure Lemma_Sub3_With_Carry3 (X1, X2, X3, Y3 : Single_Uns)
with
Ghost,
Pre => X3 < Y3,
Post => Big3 (X1, X2, X3 - Y3)
- = Big3 (X1, X2, X3) + Big3 (0, 1, 0) - Big3 (0, 0, Y3);
+ = Big3 (X1, X2, X3) + Big3 (Single_Uns'(0), 1, 0) - Big3 (0, 0, Y3);
-------------------------
-- Lemma_Add3_No_Carry --
@@ -3522,10 +3607,12 @@ is
X1 := X1 - 1;
pragma Assert
- (Big3 (X1, X2, X3) = Big3 (XX1, XX2, XX3) - Big3 (1, 0, 0));
+ (Big3 (X1, X2, X3) =
+ Big3 (XX1, XX2, XX3) - Big3 (Single_Uns'(1), 0, 0));
pragma Assert
(Big3 (X1, X2, X3) = Big3 (XX1, XX2, XX3)
- - Big3 (0, Single_Uns'Last, 0) - Big3 (0, 1, 0));
+ - Big3 (Single_Uns'(0), Single_Uns'Last, 0)
+ - Big3 (Single_Uns'(0), 1, 0));
Lemma_Add3_No_Carry (X1, X2, X3, 0, Single_Uns'Last, 0);
else
Lemma_Sub3_No_Carry (X1, X2, X3, 0, 1, 0);
@@ -3534,7 +3621,8 @@ is
X2 := X2 - 1;
pragma Assert
- (Big3 (X1, X2, X3) = Big3 (XX1, XX2, XX3) - Big3 (0, 1, 0));
+ (Big3 (X1, X2, X3) =
+ Big3 (XX1, XX2, XX3) - Big3 (Single_Uns'(0), 1, 0));
Lemma_Sub3_With_Carry3 (X1, X2, X3, Y3);
else
Lemma_Sub3_No_Carry (X1, X2, X3, 0, 0, Y3);
@@ -3553,7 +3641,7 @@ is
pragma Assert
(Big3 (X1, X2, X3) = Big3 (XX1, XX2, XX3)
- - Big3 (0, 0, Y3) - Big3 (1, 0, 0));
+ - Big3 (0, 0, Y3) - Big3 (Single_Uns'(1), 0, 0));
Lemma_Sub3_With_Carry2 (X1, X2, X3, Y2);
else
Lemma_Sub3_No_Carry (X1, X2, X3, 0, Y2, 0);
diff --git a/gcc/ada/libgnat/s-aridou.ads b/gcc/ada/libgnat/s-aridou.ads
--- a/gcc/ada/libgnat/s-aridou.ads
+++ b/gcc/ada/libgnat/s-aridou.ads
@@ -69,6 +69,7 @@ is
package BI_Ghost renames Ada.Numerics.Big_Numbers.Big_Integers_Ghost;
subtype Big_Integer is BI_Ghost.Big_Integer with Ghost;
subtype Big_Natural is BI_Ghost.Big_Natural with Ghost;
+ subtype Big_Positive is BI_Ghost.Big_Positive with Ghost;
use type BI_Ghost.Big_Integer;
package Signed_Conversion is
^ permalink raw reply [flat|nested] only message in thread
only message in thread, other threads:[~2022-09-02 7:53 UTC | newest]
Thread overview: (only message) (download: mbox.gz / follow: Atom feed)
-- links below jump to the message on this page --
2022-09-02 7:53 [Ada] Recover proof of Scaled_Divide in System.Arith_64 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).