[gcc r12-6288] [Ada] Proof of runtime units for binary modular exponentiation

[gcc r12-6288] [Ada] Proof of runtime units for binary modular exponentiation

[Pierre-Marie de Rodat]

https://gcc.gnu.org/g:ed722edd2f4accad60744b95426dba3fc9ca084c

commit r12-6288-ged722edd2f4accad60744b95426dba3fc9ca084c
Author: Yannick Moy <moy@adacore.com>
Date:   Thu Dec 2 10:55:04 2021 +0100

    [Ada] Proof of runtime units for binary modular exponentiation
    
    gcc/ada/
    
            * libgnat/s-explllu.ads: Mark in SPARK.
            * libgnat/s-expllu.ads: Mark in SPARK.
            * libgnat/s-exponu.adb: Add loop invariants and needed
            assertions.
            * libgnat/s-exponu.ads: Add functional contract.
            * libgnat/s-expuns.ads: Mark in SPARK.

Diff:
---
 gcc/ada/libgnat/s-explllu.ads | 15 ++++++++++++++-
 gcc/ada/libgnat/s-expllu.ads  | 15 ++++++++++++++-
 gcc/ada/libgnat/s-exponu.adb  | 23 ++++++++++++++++++++++-
 gcc/ada/libgnat/s-exponu.ads  | 16 +++++++++++++++-
 gcc/ada/libgnat/s-expuns.ads  | 15 ++++++++++++++-
 5 files changed, 79 insertions(+), 5 deletions(-)

diff --git a/gcc/ada/libgnat/s-explllu.ads b/gcc/ada/libgnat/s-explllu.ads
index 5a54ada1a4e..eb883a43f57 100644
--- a/gcc/ada/libgnat/s-explllu.ads
+++ b/gcc/ada/libgnat/s-explllu.ads
@@ -34,10 +34,23 @@
 --  The result is always full width, the caller must do a masking operation if
 --  the modulus is less than 2 ** Long_Long_Long_Unsigned'Size.
 
+--  Preconditions in this unit are meant for analysis only, not for run-time
+--  checking, so that the expected exceptions are raised. This is enforced
+--  by setting the corresponding assertion policy to Ignore. Postconditions
+--  and contract cases should not be executed at runtime as well, in order
+--  not to slow down the execution of these functions.
+
+pragma Assertion_Policy (Pre            => Ignore,
+                         Post           => Ignore,
+                         Contract_Cases => Ignore,
+                         Ghost          => Ignore);
+
 with System.Exponu;
 with System.Unsigned_Types;
 
-package System.Exp_LLLU is
+package System.Exp_LLLU
+  with SPARK_Mode
+is
 
    subtype Long_Long_Long_Unsigned is Unsigned_Types.Long_Long_Long_Unsigned;
 
diff --git a/gcc/ada/libgnat/s-expllu.ads b/gcc/ada/libgnat/s-expllu.ads
index 9f7b404aeb4..e028f670f94 100644
--- a/gcc/ada/libgnat/s-expllu.ads
+++ b/gcc/ada/libgnat/s-expllu.ads
@@ -34,10 +34,23 @@
 --  The result is always full width, the caller must do a masking operation if
 --  the modulus is less than 2 ** Long_Long_Unsigned'Size.
 
+--  Preconditions in this unit are meant for analysis only, not for run-time
+--  checking, so that the expected exceptions are raised. This is enforced
+--  by setting the corresponding assertion policy to Ignore. Postconditions
+--  and contract cases should not be executed at runtime as well, in order
+--  not to slow down the execution of these functions.
+
+pragma Assertion_Policy (Pre            => Ignore,
+                         Post           => Ignore,
+                         Contract_Cases => Ignore,
+                         Ghost          => Ignore);
+
 with System.Exponu;
 with System.Unsigned_Types;
 
-package System.Exp_LLU is
+package System.Exp_LLU
+  with SPARK_Mode
+is
 
    subtype Long_Long_Unsigned is Unsigned_Types.Long_Long_Unsigned;
 
diff --git a/gcc/ada/libgnat/s-exponu.adb b/gcc/ada/libgnat/s-exponu.adb
index 95256386960..06ed5099c25 100644
--- a/gcc/ada/libgnat/s-exponu.adb
+++ b/gcc/ada/libgnat/s-exponu.adb
@@ -29,7 +29,19 @@
 --                                                                          --
 ------------------------------------------------------------------------------
 
-function System.Exponu (Left : Int; Right : Natural) return Int is
+function System.Exponu (Left : Int; Right : Natural) return Int
+  with SPARK_Mode
+is
+   --  Preconditions, postconditions, ghost code, loop invariants and
+   --  assertions in this unit are meant for analysis only, not for run-time
+   --  checking, as it would be too costly otherwise. This is enforced by
+   --  setting the assertion policy to Ignore.
+
+   pragma Assertion_Policy (Pre            => Ignore,
+                            Post           => Ignore,
+                            Ghost          => Ignore,
+                            Loop_Invariant => Ignore,
+                            Assert         => Ignore);
 
    --  Note that negative exponents get a constraint error because the
    --  subtype of the Right argument (the exponent) is Natural.
@@ -49,7 +61,16 @@ begin
 
    if Exp /= 0 then
       loop
+         pragma Loop_Invariant (Exp > 0);
+         pragma Loop_Invariant (Result * Factor ** Exp = Left ** Right);
+         pragma Loop_Variant (Decreases => Exp);
+
          if Exp rem 2 /= 0 then
+            pragma Assert
+              (Result * (Factor * Factor ** (Exp - 1)) = Left ** Right);
+            pragma Assert
+              ((Result * Factor) * Factor ** (Exp - 1) = Left ** Right);
+
             Result := Result * Factor;
          end if;
 
diff --git a/gcc/ada/libgnat/s-exponu.ads b/gcc/ada/libgnat/s-exponu.ads
index 7faa1229efd..b18a3a4119c 100644
--- a/gcc/ada/libgnat/s-exponu.ads
+++ b/gcc/ada/libgnat/s-exponu.ads
@@ -31,8 +31,22 @@
 
 --  Modular integer exponentiation
 
+--  Preconditions in this unit are meant for analysis only, not for run-time
+--  checking, so that the expected exceptions are raised. This is enforced
+--  by setting the corresponding assertion policy to Ignore. Postconditions
+--  and contract cases should not be executed at runtime as well, in order
+--  not to slow down the execution of these functions.
+
+pragma Assertion_Policy (Pre            => Ignore,
+                         Post           => Ignore,
+                         Contract_Cases => Ignore,
+                         Ghost          => Ignore);
+
 generic
 
    type Int is mod <>;
 
-function System.Exponu (Left : Int; Right : Natural) return Int;
+function System.Exponu (Left : Int; Right : Natural) return Int
+with
+  SPARK_Mode,
+  Post => System.Exponu'Result = Left ** Right;
diff --git a/gcc/ada/libgnat/s-expuns.ads b/gcc/ada/libgnat/s-expuns.ads
index b49e7c0ca05..751f3fa275a 100644
--- a/gcc/ada/libgnat/s-expuns.ads
+++ b/gcc/ada/libgnat/s-expuns.ads
@@ -34,10 +34,23 @@
 --  The result is always full width, the caller must do a masking operation if
 --  the modulus is less than 2 ** Unsigned'Size.
 
+--  Preconditions in this unit are meant for analysis only, not for run-time
+--  checking, so that the expected exceptions are raised. This is enforced
+--  by setting the corresponding assertion policy to Ignore. Postconditions
+--  and contract cases should not be executed at runtime as well, in order
+--  not to slow down the execution of these functions.
+
+pragma Assertion_Policy (Pre            => Ignore,
+                         Post           => Ignore,
+                         Contract_Cases => Ignore,
+                         Ghost          => Ignore);
+
 with System.Exponu;
 with System.Unsigned_Types;
 
-package System.Exp_Uns is
+package System.Exp_Uns
+  with SPARK_Mode
+is
 
    subtype Unsigned is Unsigned_Types.Unsigned;