[Ada] Proof of runtime units for binary modular exponentiation

[Ada] Proof of runtime units for binary modular exponentiation

[Pierre-Marie de Rodat]

[-- Attachment #1: Type: text/plain, Size: 515 bytes --]

This proves the generic unit System.Exponu instantiated for Unsigned,
Long_Long_Unsigned and Long_Long_Long_Unsigned. The proof is simpler
than the one for signed integers, as there are no possible overflows
here.

Tested on x86_64-pc-linux-gnu, committed on trunk

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.

[-- Attachment #2: patch.diff --]
[-- Type: text/x-diff, Size: 5952 bytes --]

diff --git a/gcc/ada/libgnat/s-explllu.ads b/gcc/ada/libgnat/s-explllu.ads
--- 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
--- 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
--- 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
--- 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
--- 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;