public inbox for gcc-cvs@sourceware.org
help / color / mirror / Atom feed
* [gcc r13-832] [Ada] Update proofs of double arithmetic unit after prover changes
@ 2022-05-30 8:30 Pierre-Marie de Rodat
0 siblings, 0 replies; only message in thread
From: Pierre-Marie de Rodat @ 2022-05-30 8:30 UTC (permalink / raw)
To: gcc-cvs
https://gcc.gnu.org/g:40e01041b3593c72f3d52013953fbfbe0011abb8
commit r13-832-g40e01041b3593c72f3d52013953fbfbe0011abb8
Author: Yannick Moy <moy@adacore.com>
Date: Tue Apr 19 15:46:05 2022 +0000
[Ada] Update proofs of double arithmetic unit after prover changes
Changes in GNATprove (translation to Why3 and provers) result in proofs
being much less automatic, and requiring ghost code to detail
intermediate steps. In some cases, it is better to use the new By
mechanism to prove assertions in steps, as this avoids polluting the
proof context for other proofs. For that reason, add units s-spark.ads
and s-spcuop.ads/b to the runtime sources.
gcc/ada/
* Makefile.rtl: Add new units.
* libgnat/s-aridou.adb (Scaled_Divide): Add ghost code for provers.
* libgnat/s-spcuop.adb: New unit for ghost cut operations.
* libgnat/s-spcuop.ads: New unit for ghost cut operations.
* libgnat/s-spark.ads: New unit.
Diff:
---
gcc/ada/Makefile.rtl | 2 +
gcc/ada/libgnat/s-aridou.adb | 530 +++++++++++++++++++++++++++++++++++--------
gcc/ada/libgnat/s-spark.ads | 36 +++
gcc/ada/libgnat/s-spcuop.adb | 42 ++++
gcc/ada/libgnat/s-spcuop.ads | 59 +++++
5 files changed, 578 insertions(+), 91 deletions(-)
diff --git a/gcc/ada/Makefile.rtl b/gcc/ada/Makefile.rtl
index ed3d33408d8..8812d15a218 100644
--- a/gcc/ada/Makefile.rtl
+++ b/gcc/ada/Makefile.rtl
@@ -749,6 +749,8 @@ GNATRTL_NONTASKING_OBJS= \
s-shasto$(objext) \
s-soflin$(objext) \
s-soliin$(objext) \
+ s-spark$(objext) \
+ s-spcuop$(objext) \
s-spsufi$(objext) \
s-stache$(objext) \
s-stalib$(objext) \
diff --git a/gcc/ada/libgnat/s-aridou.adb b/gcc/ada/libgnat/s-aridou.adb
index d2149681dbe..259c0ac0da2 100644
--- a/gcc/ada/libgnat/s-aridou.adb
+++ b/gcc/ada/libgnat/s-aridou.adb
@@ -30,6 +30,7 @@
------------------------------------------------------------------------------
with Ada.Unchecked_Conversion;
+with System.SPARK.Cut_Operations; use System.SPARK.Cut_Operations;
package body System.Arith_Double
with SPARK_Mode
@@ -1822,6 +1823,31 @@ is
Big_Q : Big_Integer with Ghost;
Inter : Natural with Ghost;
+ -- Local ghost functions
+
+ function Is_Mult_Decomposition
+ (D1, D2, D3, D4 : Big_Integer)
+ return Boolean
+ is
+ (Mult = Big_2xxSingle * Big_2xxSingle * Big_2xxSingle * D1
+ + Big_2xxSingle * Big_2xxSingle * D2
+ + Big_2xxSingle * D3
+ + D4)
+ with Ghost;
+
+ function Is_Scaled_Mult_Decomposition
+ (D1, D2, D3, D4 : Big_Integer)
+ return Boolean
+ is
+ (Mult * Big_2xx (Scale)
+ = Big_2xxSingle * Big_2xxSingle * Big_2xxSingle * D1
+ + Big_2xxSingle * Big_2xxSingle * D2
+ + Big_2xxSingle * D3
+ + D4)
+ with
+ Ghost,
+ Pre => Scale < Double_Size;
+
-- Local lemmas
procedure Prove_Dividend_Scaling
@@ -1829,24 +1855,19 @@ is
Ghost,
Pre => D'Initialized
and then Scale <= Single_Size
- and then Mult =
- 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 Is_Mult_Decomposition (Big (Double_Uns (D (1))),
+ Big (Double_Uns (D (2))),
+ Big (Double_Uns (D (3))),
+ Big (Double_Uns (D (4))))
and then Big (D (1) & D (2)) * Big_2xx (Scale) < Big_2xxDouble
and then T1 = Shift_Left (D (1) & D (2), Scale)
and then T2 = Shift_Left (Double_Uns (D (3)), Scale)
and then T3 = Shift_Left (Double_Uns (D (4)), Scale),
- Post => Mult * Big_2xx (Scale) =
- Big_2xxSingle
- * Big_2xxSingle * Big_2xxSingle * Big (Double_Uns (Hi (T1)))
- + Big_2xxSingle * Big_2xxSingle * Big (Double_Uns (Lo (T1) or
- Hi (T2)))
- + Big_2xxSingle * Big (Double_Uns (Lo (T2) or
- Hi (T3)))
- + Big (Double_Uns (Lo (T3)));
+ Post => Is_Scaled_Mult_Decomposition
+ (Big (Double_Uns (Hi (T1))),
+ Big (Double_Uns (Lo (T1) or Hi (T2))),
+ Big (Double_Uns (Lo (T2) or Hi (T3))),
+ Big (Double_Uns (Lo (T3))));
-- Proves the scaling of the 4-digit dividend actually multiplies it by
-- 2**Scale.
@@ -2030,21 +2051,32 @@ is
----------------------------
procedure Prove_Dividend_Scaling is
+ Big_D12 : constant Big_Integer :=
+ Big_2xx (Scale) * Big (D (1) & D (2));
+ Big_T1 : constant Big_Integer := Big (T1);
+ Big_D3 : constant Big_Integer :=
+ Big_2xx (Scale) * Big (Double_Uns (D (3)));
+ Big_T2 : constant Big_Integer := Big (T2);
+ Big_D4 : constant Big_Integer :=
+ Big_2xx (Scale) * Big (Double_Uns (D (4)));
+ Big_T3 : constant Big_Integer := Big (T3);
+
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_Lt_Mult (Big (Double_Uns (D (3))), Big_2xxSingle,
+ Big_2xx (Scale), Big_2xxDouble);
Lemma_Shift_Left (Double_Uns (D (3)), Scale);
+ Lemma_Lt_Mult (Big (Double_Uns (D (4))), Big_2xxSingle,
+ Big_2xx (Scale), Big_2xxDouble);
Lemma_Shift_Left (Double_Uns (D (4)), Scale);
Lemma_Hi_Lo (D (1) & D (2), D (1), D (2));
pragma Assert (Mult * Big_2xx (Scale) =
- Big_2xxSingle
- * Big_2xxSingle * Big_2xx (Scale) * Big (D (1) & D (2))
- + Big_2xxSingle * Big_2xx (Scale) * Big (Double_Uns (D (3)))
- + Big_2xx (Scale) * Big (Double_Uns (D (4))));
+ Big_2xxSingle * Big_2xxSingle * Big_D12
+ + Big_2xxSingle * Big_D3
+ + Big_D4);
pragma Assert (Big_2xx (Scale) > 0);
- Lemma_Lt_Mult (Big (Double_Uns (D (3))), Big_2xxSingle,
- Big_2xx (Scale), Big_2xxDouble);
- Lemma_Lt_Mult (Big (Double_Uns (D (4))), Big_2xxSingle,
- Big_2xx (Scale), Big_2xxDouble);
declare
Two_xx_Scale : constant Double_Uns := Double_Uns'(2 ** Scale);
D12 : constant Double_Uns := D (1) & D (2);
@@ -2053,43 +2085,120 @@ is
pragma Assert (Big (Two_xx_Scale) * Big (D12) < Big_2xxDouble);
Lemma_Mult_Commutation (Two_xx_Scale, D12, T1);
end;
- declare
- Big_D12 : constant Big_Integer :=
- Big_2xx (Scale) * Big (D (1) & D (2));
- Big_T1 : constant Big_Integer := Big (T1);
- begin
- pragma Assert (Big_D12 = Big_T1);
- pragma Assert (Big_2xxSingle * Big_2xxSingle * Big_D12
- = Big_2xxSingle * Big_2xxSingle * Big_T1);
- end;
+ pragma Assert (Big_D12 = Big_T1);
+ pragma Assert (Big_2xxSingle * Big_2xxSingle * Big_D12
+ = Big_2xxSingle * Big_2xxSingle * Big_T1);
Lemma_Mult_Commutation (2 ** Scale, Double_Uns (D (3)), T2);
- declare
- Big_D3 : constant Big_Integer :=
- Big_2xx (Scale) * Big (Double_Uns (D (3)));
- Big_T2 : constant Big_Integer := Big (T2);
- begin
- pragma Assert (Big_D3 = Big_T2);
- pragma Assert (Big_2xxSingle * Big_D3 = Big_2xxSingle * Big_T2);
- end;
+ pragma Assert (Big_D3 = Big_T2);
+ pragma Assert (Big_2xxSingle * Big_D3 = Big_2xxSingle * Big_T2);
Lemma_Mult_Commutation (2 ** Scale, Double_Uns (D (4)), T3);
- declare
- Big_D4 : constant Big_Integer :=
- Big_2xx (Scale) * Big (Double_Uns (D (4)));
- Big_T3 : constant Big_Integer := Big (T3);
- begin
- pragma Assert (Big_D4 = Big_T3);
- end;
- pragma Assert (Mult * Big_2xx (Scale) =
- Big_2xxSingle * Big_2xxSingle * Big (T1)
- + Big_2xxSingle * Big (T2)
- + Big (T3));
+ pragma Assert (Big_D4 = Big_T3);
+ pragma Assert
+ (By (Is_Scaled_Mult_Decomposition (0, Big_T1, Big_T2, Big_T3),
+ By (Big_2xxSingle * Big_2xxSingle * Big_D12 =
+ Big_2xxSingle * Big_2xxSingle * Big_T1,
+ Big_D12 = Big_T1)
+ and then
+ By (Big_2xxSingle * Big_D3 = Big_2xxSingle * Big_T2,
+ Big_D3 = Big_T2)
+ and then
+ Big_D4 = Big_T3));
Lemma_Hi_Lo (T1, Hi (T1), Lo (T1));
Lemma_Hi_Lo (T2, Hi (T2), Lo (T2));
Lemma_Hi_Lo (T3, Hi (T3), Lo (T3));
+ Lemma_Mult_Distribution (Big_2xxSingle * Big_2xxSingle,
+ Big_2xxSingle * Big (Double_Uns (Hi (T1))),
+ Big (Double_Uns (Lo (T1))));
+ Lemma_Mult_Distribution (Big_2xxSingle,
+ Big_2xxSingle * Big (Double_Uns (Hi (T2))),
+ Big (Double_Uns (Lo (T2))));
+ Lemma_Mult_Distribution (Big_2xxSingle * Big_2xxSingle,
+ Big (Double_Uns (Lo (T1))),
+ Big (Double_Uns (Hi (T2))));
+ Lemma_Mult_Distribution (Big_2xxSingle,
+ Big (Double_Uns (Lo (T2))),
+ Big (Double_Uns (Hi (T3))));
+ pragma Assert
+ (By (Is_Scaled_Mult_Decomposition
+ (Big (Double_Uns (Hi (T1))),
+ Big (Double_Uns (Lo (T1))) + Big (Double_Uns (Hi (T2))),
+ Big (Double_Uns (Lo (T2))) + Big (Double_Uns (Hi (T3))),
+ Big (Double_Uns (Lo (T3)))),
+ -- Start from stating equality between the expanded values of
+ -- the right-hand side in the known and desired assertions over
+ -- Is_Scaled_Mult_Decomposition.
+ By (Big_2xxSingle * Big_2xxSingle * Big_2xxSingle *
+ Big (Double_Uns (Hi (T1)))
+ + Big_2xxSingle * Big_2xxSingle *
+ (Big (Double_Uns (Lo (T1))) + Big (Double_Uns (Hi (T2))))
+ + Big_2xxSingle *
+ (Big (Double_Uns (Lo (T2))) + Big (Double_Uns (Hi (T3))))
+ + Big (Double_Uns (Lo (T3))) =
+ Big_2xxSingle * Big_2xxSingle * Big_2xxSingle * 0
+ + Big_2xxSingle * Big_2xxSingle * Big_T1
+ + Big_2xxSingle * Big_T2
+ + Big_T3,
+ -- Now list all known equalities that contribute
+ Big_2xxSingle * Big_2xxSingle * Big_2xxSingle *
+ Big (Double_Uns (Hi (T1)))
+ + Big_2xxSingle * Big_2xxSingle *
+ (Big (Double_Uns (Lo (T1))) + Big (Double_Uns (Hi (T2))))
+ + Big_2xxSingle *
+ (Big (Double_Uns (Lo (T2))) + Big (Double_Uns (Hi (T3))))
+ + Big (Double_Uns (Lo (T3))) =
+ Big_2xxSingle * Big_2xxSingle * Big_2xxSingle *
+ Big (Double_Uns (Hi (T1)))
+ + Big_2xxSingle * Big_2xxSingle * Big (Double_Uns (Lo (T1)))
+ + Big_2xxSingle * Big_2xxSingle * Big (Double_Uns (Hi (T2)))
+ + Big_2xxSingle * Big (Double_Uns (Lo (T2)))
+ + Big_2xxSingle * Big (Double_Uns (Hi (T3)))
+ + Big (Double_Uns (Lo (T3)))
+ and then
+ By (Big_2xxSingle * Big_2xxSingle * Big (T1)
+ = Big_2xxSingle * Big_2xxSingle * Big_2xxSingle
+ * Big (Double_Uns (Hi (T1)))
+ + Big_2xxSingle * Big_2xxSingle * Big (Double_Uns (Lo (T1))),
+ Big_2xxSingle * Big_2xxSingle * Big (T1)
+ = Big_2xxSingle * Big_2xxSingle
+ * (Big_2xxSingle * Big (Double_Uns (Hi (T1)))
+ + Big (Double_Uns (Lo (T1)))))
+ and then
+ By (Big_2xxSingle * Big (T2)
+ = Big_2xxSingle * Big_2xxSingle * Big (Double_Uns (Hi (T2)))
+ + Big_2xxSingle * Big (Double_Uns (Lo (T2))),
+ Big_2xxSingle * Big (T2)
+ = Big_2xxSingle * (Big_2xxSingle * Big (Double_Uns (Hi (T2)))
+ + Big (Double_Uns (Lo (T2)))))
+ and then
+ Big (T3) = Big_2xxSingle * Big (Double_Uns (Hi (T3)))
+ + Big (Double_Uns (Lo (T3))))));
+ Lemma_Mult_Distribution (Big_2xxSingle * Big_2xxSingle,
+ Big (Double_Uns (Lo (T1))),
+ Big (Double_Uns (Hi (T2))));
pragma Assert (Double_Uns (Lo (T1) or Hi (T2)) =
Double_Uns (Lo (T1)) + Double_Uns (Hi (T2)));
pragma Assert (Double_Uns (Lo (T2) or Hi (T3)) =
Double_Uns (Lo (T2)) + Double_Uns (Hi (T3)));
+ Lemma_Add_Commutation (Double_Uns (Lo (T1)), Hi (T2));
+ Lemma_Add_Commutation (Double_Uns (Lo (T2)), Hi (T3));
+ pragma Assert
+ (By (Is_Scaled_Mult_Decomposition
+ (Big (Double_Uns (Hi (T1))),
+ Big (Double_Uns (Lo (T1) or Hi (T2))),
+ Big (Double_Uns (Lo (T2) or Hi (T3))),
+ Big (Double_Uns (Lo (T3)))),
+ By (Big_2xxSingle * Big_2xxSingle
+ * Big (Double_Uns (Lo (T1) or Hi (T2))) =
+ Big_2xxSingle * Big_2xxSingle * Big (Double_Uns (Lo (T1)))
+ + Big_2xxSingle * Big_2xxSingle * Big (Double_Uns (Hi (T2))),
+ Big_2xxSingle * Big_2xxSingle
+ * Big (Double_Uns (Lo (T1)) + Double_Uns (Hi (T2))) =
+ Big_2xxSingle * Big_2xxSingle
+ * (Big (Double_Uns (Lo (T1))) + Big (Double_Uns (Hi (T2)))))
+ and then
+ Big_2xxSingle * Big (Double_Uns (Lo (T2) or Hi (T3))) =
+ Big_2xxSingle * Big (Double_Uns (Lo (T2)))
+ + Big_2xxSingle * Big (Double_Uns (Hi (T3)))));
end Prove_Dividend_Scaling;
--------------------------
@@ -2299,24 +2408,58 @@ is
Lemma_Abs_Commutation (X);
Lemma_Abs_Commutation (Y);
Lemma_Mult_Decomposition (Mult, Xu, Yu, Xhi, Xlo, Yhi, Ylo);
+ pragma Assert
+ (Is_Mult_Decomposition
+ (D1 => 0,
+ D2 => Big (Double_Uns'(Xhi * Yhi)),
+ D3 => Big (Double_Uns'(Xhi * Ylo)) + Big (Double_Uns'(Xlo * Yhi)),
+ D4 => Big (Double_Uns'(Xlo * Ylo))));
T1 := Xlo * Ylo;
D (4) := Lo (T1);
D (3) := Hi (T1);
Lemma_Hi_Lo (T1, D (3), D (4));
+ pragma Assert
+ (Is_Mult_Decomposition
+ (D1 => 0,
+ D2 => Big (Double_Uns'(Xhi * Yhi)),
+ D3 => Big (Double_Uns'(Xhi * Ylo)) + Big (Double_Uns'(Xlo * Yhi))
+ + Big (Double_Uns (D (3))),
+ D4 => Big (Double_Uns (D (4)))));
if Yhi /= 0 then
T1 := Xlo * Yhi;
Lemma_Hi_Lo (T1, Hi (T1), Lo (T1));
+ pragma Assert
+ (Is_Mult_Decomposition
+ (D1 => 0,
+ D2 => Big (Double_Uns'(Xhi * Yhi)) + Big (Double_Uns (Hi (T1))),
+ D3 => Big (Double_Uns'(Xhi * Ylo)) + Big (Double_Uns (Lo (T1)))
+ + Big (Double_Uns (D (3))),
+ D4 => Big (Double_Uns (D (4)))));
T2 := D (3) + Lo (T1);
+ Lemma_Add_Commutation (Double_Uns (Lo (T1)), D (3));
+ pragma Assert
+ (Is_Mult_Decomposition
+ (D1 => 0,
+ D2 => Big (Double_Uns'(Xhi * Yhi)) + Big (Double_Uns (Hi (T1))),
+ D3 => Big (Double_Uns'(Xhi * Ylo)) + Big (T2),
+ D4 => Big (Double_Uns (D (4)))));
Lemma_Mult_Distribution (Big_2xxSingle,
Big (Double_Uns (D (3))),
Big (Double_Uns (Lo (T1))));
Lemma_Hi_Lo (T2, Hi (T2), Lo (T2));
+ pragma Assert
+ (Is_Mult_Decomposition
+ (D1 => 0,
+ D2 => Big (Double_Uns'(Xhi * Yhi)) + Big (Double_Uns (Hi (T1)))
+ + Big (Double_Uns (Hi (T2))),
+ D3 => Big (Double_Uns'(Xhi * Ylo)) + Big (Double_Uns (Lo (T2))),
+ D4 => Big (Double_Uns (D (4)))));
D (3) := Lo (T2);
D (2) := Hi (T1) + Hi (T2);
@@ -2326,31 +2469,131 @@ is
pragma Assert
(Big (Double_Uns (Hi (T1))) + Big (Double_Uns (Hi (T2))) =
Big (Double_Uns (D (2))));
+ pragma Assert
+ (Is_Mult_Decomposition
+ (D1 => 0,
+ D2 => Big (Double_Uns'(Xhi * Yhi)) + Big (Double_Uns (D (2))),
+ D3 => Big (Double_Uns'(Xhi * Ylo)) + Big (Double_Uns (D (3))),
+ D4 => Big (Double_Uns (D (4)))));
if Xhi /= 0 then
T1 := Xhi * Ylo;
Lemma_Hi_Lo (T1, Hi (T1), Lo (T1));
+ pragma Assert
+ (By (Is_Mult_Decomposition
+ (D1 => 0,
+ D2 => Big (Double_Uns'(Xhi * Yhi)) + Big (Double_Uns (D (2)))
+ + Big (Double_Uns (Hi (T1))),
+ D3 => Big (Double_Uns (Lo (T1))) + Big (Double_Uns (D (3))),
+ D4 => Big (Double_Uns (D (4)))),
+ (By (Big_2xxSingle * Big (T1) =
+ Big_2xxSingle * Big_2xxSingle * Big (Double_Uns (Hi (T1)))
+ + Big_2xxSingle * Big (Double_Uns (Lo (T1))),
+ Big_2xxSingle * Big (T1) =
+ Big_2xxSingle * (Big_2xxSingle * Big (Double_Uns (Hi (T1)))
+ + Big (Double_Uns (Lo (T1))))))));
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))))));
D (3) := Lo (T2);
T3 := D (2) + Hi (T1);
+ Lemma_Add_Commutation (Double_Uns (D (2)), Hi (T1));
+ pragma Assert
+ (Is_Mult_Decomposition
+ (D1 => 0,
+ D2 => Big (Double_Uns'(Xhi * Yhi)) + Big (T3)
+ + Big (Double_Uns (Hi (T2))),
+ D3 => Big (Double_Uns (D (3))),
+ D4 => Big (Double_Uns (D (4)))));
Lemma_Add_Commutation (T3, Hi (T2));
T3 := T3 + Hi (T2);
T2 := Double_Uns'(Xhi * Yhi);
+ pragma Assert
+ (Is_Mult_Decomposition
+ (D1 => 0,
+ D2 => Big (T2) + Big (T3),
+ D3 => Big (Double_Uns (D (3))),
+ D4 => Big (Double_Uns (D (4)))));
Lemma_Hi_Lo (T2, Hi (T2), Lo (T2));
- Lemma_Add_Commutation (T3, Lo (T2));
+ pragma Assert
+ (By (Is_Mult_Decomposition
+ (D1 => Big (Double_Uns (Hi (T2))),
+ D2 => Big (Double_Uns (Lo (T2))) + Big (T3),
+ D3 => Big (Double_Uns (D (3))),
+ D4 => Big (Double_Uns (D (4)))),
+ By (Big_2xxSingle * Big_2xxSingle * Big (T2) =
+ Big_2xxSingle * Big_2xxSingle * Big_2xxSingle
+ * Big (Double_Uns (Hi (T2)))
+ + Big_2xxSingle * Big_2xxSingle * Big (Double_Uns (Lo (T2))),
+ Big_2xxSingle * Big_2xxSingle *
+ (Big_2xxSingle * Big (Double_Uns (Hi (T2)))
+ + Big (Double_Uns (Lo (T2))))
+ = Big_2xxSingle * Big_2xxSingle * Big_2xxSingle
+ * Big (Double_Uns (Hi (T2)))
+ + Big_2xxSingle * Big_2xxSingle
+ * Big (Double_Uns (Lo (T2))))));
T1 := T3 + Lo (T2);
D (2) := Lo (T1);
- Lemma_Hi_Lo (T1, Hi (T1), D (2));
+ Lemma_Add_Commutation (T3, Lo (T2));
+ pragma Assert
+ (Is_Mult_Decomposition
+ (D1 => Big (Double_Uns (Hi (T2))),
+ D2 => Big (T1),
+ D3 => Big (Double_Uns (D (3))),
+ D4 => Big (Double_Uns (D (4)))));
+ Lemma_Hi_Lo (T1, Hi (T1), Lo (T1));
+ pragma Assert
+ (By (Is_Mult_Decomposition
+ (D1 => Big (Double_Uns (Hi (T2))) + Big (Double_Uns (Hi (T1))),
+ D2 => Big (Double_Uns (D (2))),
+ D3 => Big (Double_Uns (D (3))),
+ D4 => Big (Double_Uns (D (4)))),
+ By (Big_2xxSingle * Big_2xxSingle * Big (Double_Uns (Lo (T1))) =
+ Big_2xxSingle * Big_2xxSingle * Big (Double_Uns (D (2))),
+ D (2) = Lo (T1))
+ and then
+ By (Big_2xxSingle * Big_2xxSingle * Big (T1) =
+ Big_2xxSingle * Big_2xxSingle * Big_2xxSingle
+ * Big (Double_Uns (Hi (T1)))
+ + Big_2xxSingle * Big_2xxSingle * Big (Double_Uns (Lo (T1))),
+ Big_2xxSingle * Big_2xxSingle *
+ (Big_2xxSingle * Big (Double_Uns (Hi (T1)))
+ + Big (Double_Uns (Lo (T1))))
+ = Big_2xxSingle * Big_2xxSingle * Big_2xxSingle
+ * Big (Double_Uns (Hi (T1)))
+ + Big_2xxSingle * Big_2xxSingle
+ * Big (Double_Uns (Lo (T1))))));
D (1) := Hi (T2) + Hi (T1);
@@ -2361,32 +2604,71 @@ is
(Big (Double_Uns (Hi (T2))) + Big (Double_Uns (Hi (T1))) =
Big (Double_Uns (D (1))));
- pragma Assert (Mult =
- 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))));
-
+ pragma Assert
+ (By (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)))),
+ Big_2xxSingle * Big_2xxSingle * Big_2xxSingle *
+ Big (Double_Uns (D (1)))
+ = Big_2xxSingle * Big_2xxSingle * Big_2xxSingle *
+ (Big (Double_Uns (Hi (T2)) + Double_Uns (Hi (T1))))));
else
D (1) := 0;
- end if;
- pragma Assert (Mult =
- 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))));
+ pragma Assert
+ (By (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)))),
+ Big (Double_Uns'(Xhi * Yhi)) = 0
+ and then Big (Double_Uns'(Xhi * Ylo)) = 0
+ and then Big (Double_Uns (D (1))) = 0));
+ end if;
+ 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)))));
else
+ pragma Assert
+ (By (Is_Mult_Decomposition
+ (D1 => 0,
+ D2 => 0,
+ D3 => Big (Double_Uns'(Xhi * Ylo)) + Big (Double_Uns (D (3))),
+ D4 => Big (Double_Uns (D (4)))),
+ Big (Double_Uns'(Xhi * Yhi)) = 0
+ and then Big (Double_Uns'(Xlo * Yhi)) = 0));
+
if Xhi /= 0 then
T1 := Xhi * Ylo;
Lemma_Hi_Lo (T1, Hi (T1), Lo (T1));
+ pragma Assert
+ (By (Is_Mult_Decomposition
+ (D1 => 0,
+ D2 => Big (Double_Uns (Hi (T1))),
+ D3 => Big (Double_Uns (Lo (T1))) + Big (Double_Uns (D (3))),
+ D4 => Big (Double_Uns (D (4)))),
+ Big_2xxSingle * Big (Double_Uns'(Xhi * Ylo)) =
+ Big_2xxSingle * Big_2xxSingle * Big (Double_Uns (Hi (T1)))
+ + Big_2xxSingle * Big (Double_Uns (Lo (T1)))));
T2 := D (3) + Lo (T1);
+ Lemma_Add_Commutation (Double_Uns (Lo (T1)), D (3));
+ pragma Assert
+ (By (Is_Mult_Decomposition
+ (D1 => 0,
+ D2 => Big (Double_Uns (Hi (T1))),
+ D3 => Big (T2),
+ D4 => Big (Double_Uns (D (4)))),
+ Big_2xxSingle * Big (T2) =
+ Big_2xxSingle *
+ (Big (Double_Uns (Lo (T1))) + Big (Double_Uns (D (3))))));
Lemma_Mult_Distribution (Big_2xxSingle,
Big (Double_Uns (D (3))),
Big (Double_Uns (Lo (T1))));
@@ -2401,28 +2683,32 @@ is
pragma Assert
(Big (Double_Uns (Hi (T1))) + Big (Double_Uns (Hi (T2))) =
Big (Double_Uns (D (2))));
- pragma Assert (Mult =
- Big_2xxSingle * Big_2xxSingle * Big (Double_Uns (D (2)))
- + Big_2xxSingle * Big (Double_Uns (D (3)))
- + Big (Double_Uns (D (4))));
+ pragma Assert
+ (Is_Mult_Decomposition
+ (D1 => 0,
+ D2 => Big (Double_Uns (D (2))),
+ D3 => Big (Double_Uns (D (3))),
+ D4 => Big (Double_Uns (D (4)))));
else
D (2) := 0;
- pragma Assert (Mult =
- Big_2xxSingle * Big_2xxSingle * Big (Double_Uns (D (2)))
- + Big_2xxSingle * Big (Double_Uns (D (3)))
- + Big (Double_Uns (D (4))));
+ pragma Assert
+ (By (Is_Mult_Decomposition
+ (D1 => 0,
+ D2 => Big (Double_Uns (D (2))),
+ D3 => Big (Double_Uns (D (3))),
+ D4 => Big (Double_Uns (D (4)))),
+ Big (Double_Uns'(Xhi * Ylo)) = 0
+ and then Big (Double_Uns (D (2))) = 0));
end if;
D (1) := 0;
end if;
- pragma Assert (Mult =
- 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))));
+ 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)))));
-- Now it is time for the dreaded multiple precision division. First an
-- easy case, check for the simple case of a one digit divisor.
@@ -2627,17 +2913,49 @@ is
D (3) := Lo (T2) or Hi (T3);
D (4) := Lo (T3);
- pragma Assert (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))));
- 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));
- Lemma_Div_Lt (Mult * Big_2xx (Scale), Big (Zu), Big_2xxDouble);
+ 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
+ (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)))
@@ -2645,8 +2963,38 @@ is
+ 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));
+ 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)))));
Lemma_Substitution
(Mult * Big_2xx (Scale), Big_2xxSingle * Big_2xxSingle,
Big_2xxSingle * Big (Double_Uns (D (1)))
diff --git a/gcc/ada/libgnat/s-spark.ads b/gcc/ada/libgnat/s-spark.ads
new file mode 100644
index 00000000000..25a18a417ed
--- /dev/null
+++ b/gcc/ada/libgnat/s-spark.ads
@@ -0,0 +1,36 @@
+------------------------------------------------------------------------------
+-- --
+-- GNAT COMPILER COMPONENTS --
+-- --
+-- S Y S T E M . S P A R K --
+-- --
+-- S p e c --
+-- --
+-- Copyright (C) 2022, Free Software Foundation, Inc. --
+-- --
+-- GNAT is free software; you can redistribute it and/or modify it under --
+-- terms of the GNU General Public License as published by the Free Soft- --
+-- ware Foundation; either version 3, or (at your option) any later ver- --
+-- sion. GNAT is distributed in the hope that it will be useful, but WITH- --
+-- OUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY --
+-- or FITNESS FOR A PARTICULAR PURPOSE. --
+-- --
+-- As a special exception under Section 7 of GPL version 3, you are granted --
+-- additional permissions described in the GCC Runtime Library Exception, --
+-- version 3.1, as published by the Free Software Foundation. --
+-- --
+-- You should have received a copy of the GNU General Public License and --
+-- a copy of the GCC Runtime Library Exception along with this program; --
+-- see the files COPYING3 and COPYING.RUNTIME respectively. If not, see --
+-- <http://www.gnu.org/licenses/>. --
+-- --
+-- GNAT was originally developed by the GNAT team at New York University. --
+-- Extensive contributions were provided by Ada Core Technologies Inc. --
+-- --
+------------------------------------------------------------------------------
+
+package System.SPARK with
+ SPARK_Mode,
+ Pure
+is
+end System.SPARK;
diff --git a/gcc/ada/libgnat/s-spcuop.adb b/gcc/ada/libgnat/s-spcuop.adb
new file mode 100644
index 00000000000..d91f89750cd
--- /dev/null
+++ b/gcc/ada/libgnat/s-spcuop.adb
@@ -0,0 +1,42 @@
+------------------------------------------------------------------------------
+-- --
+-- GNAT COMPILER COMPONENTS --
+-- --
+-- S Y S T E M . S P A R K . C U T _ O P E R A T I O N S --
+-- --
+-- B o d y --
+-- --
+-- Copyright (C) 2022, Free Software Foundation, Inc. --
+-- --
+-- GNAT is free software; you can redistribute it and/or modify it under --
+-- terms of the GNU General Public License as published by the Free Soft- --
+-- ware Foundation; either version 3, or (at your option) any later ver- --
+-- sion. GNAT is distributed in the hope that it will be useful, but WITH- --
+-- OUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY --
+-- or FITNESS FOR A PARTICULAR PURPOSE. --
+-- --
+-- As a special exception under Section 7 of GPL version 3, you are granted --
+-- additional permissions described in the GCC Runtime Library Exception, --
+-- version 3.1, as published by the Free Software Foundation. --
+-- --
+-- You should have received a copy of the GNU General Public License and --
+-- a copy of the GCC Runtime Library Exception along with this program; --
+-- see the files COPYING3 and COPYING.RUNTIME respectively. If not, see --
+-- <http://www.gnu.org/licenses/>. --
+-- --
+-- GNAT was originally developed by the GNAT team at New York University. --
+-- Extensive contributions were provided by Ada Core Technologies Inc. --
+-- --
+------------------------------------------------------------------------------
+
+package body System.SPARK.Cut_Operations with
+ SPARK_Mode => Off
+is
+
+ function By (Consequence, Premise : Boolean) return Boolean is
+ (Premise and then Consequence);
+
+ function So (Premise, Consequence : Boolean) return Boolean is
+ (Premise and then Consequence);
+
+end System.SPARK.Cut_Operations;
diff --git a/gcc/ada/libgnat/s-spcuop.ads b/gcc/ada/libgnat/s-spcuop.ads
new file mode 100644
index 00000000000..39a61c96af1
--- /dev/null
+++ b/gcc/ada/libgnat/s-spcuop.ads
@@ -0,0 +1,59 @@
+------------------------------------------------------------------------------
+-- --
+-- GNAT COMPILER COMPONENTS --
+-- --
+-- S Y S T E M . S P A R K . C U T _ O P E R A T I O N S --
+-- --
+-- S p e c --
+-- --
+-- Copyright (C) 2022, Free Software Foundation, Inc. --
+-- --
+-- GNAT is free software; you can redistribute it and/or modify it under --
+-- terms of the GNU General Public License as published by the Free Soft- --
+-- ware Foundation; either version 3, or (at your option) any later ver- --
+-- sion. GNAT is distributed in the hope that it will be useful, but WITH- --
+-- OUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY --
+-- or FITNESS FOR A PARTICULAR PURPOSE. --
+-- --
+-- As a special exception under Section 7 of GPL version 3, you are granted --
+-- additional permissions described in the GCC Runtime Library Exception, --
+-- version 3.1, as published by the Free Software Foundation. --
+-- --
+-- You should have received a copy of the GNU General Public License and --
+-- a copy of the GCC Runtime Library Exception along with this program; --
+-- see the files COPYING3 and COPYING.RUNTIME respectively. If not, see --
+-- <http://www.gnu.org/licenses/>. --
+-- --
+-- GNAT was originally developed by the GNAT team at New York University. --
+-- Extensive contributions were provided by Ada Core Technologies Inc. --
+-- --
+------------------------------------------------------------------------------
+
+-- By and So are connectors used to manually help the proof of assertions by
+-- introducing intermediate steps. They can only be used inside pragmas
+-- Assert or Assert_And_Cut. They are handled in the following way:
+--
+-- * If A and B are two boolean expressions, proving By (A, B) requires
+-- proving B, the premise, and then A assuming B, the side-condition. When
+-- By (A, B) is assumed on the other hand, we only assume A. B is used
+-- for the proof, but is not visible afterward.
+--
+-- * If A and B are two boolean expressions, proving So (A, B) requires
+-- proving A, the premise, and then B assuming A, the side-condition. When
+-- So (A, B) is assumed both A and B are assumed to be true.
+
+package System.SPARK.Cut_Operations with
+ SPARK_Mode,
+ Pure,
+ Annotate => (GNATprove, Terminating)
+is
+
+ function By (Consequence, Premise : Boolean) return Boolean with
+ Ghost,
+ Global => null;
+
+ function So (Premise, Consequence : Boolean) return Boolean with
+ Ghost,
+ Global => null;
+
+end System.SPARK.Cut_Operations;
^ permalink raw reply [flat|nested] only message in thread
only message in thread, other threads:[~2022-05-30 8:30 UTC | newest]
Thread overview: (only message) (download: mbox.gz / follow: Atom feed)
-- links below jump to the message on this page --
2022-05-30 8:30 [gcc r13-832] [Ada] Update proofs of double arithmetic unit after prover changes Pierre-Marie de Rodat
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).