[Ada] Proof of runtime units for integer exponentiation (checks on)
authorYannick Moy <moy@adacore.com>
Tue, 30 Nov 2021 14:11:32 +0000 (15:11 +0100)
committerPierre-Marie de Rodat <derodat@adacore.com>
Wed, 5 Jan 2022 11:32:35 +0000 (11:32 +0000)
gcc/ada/

* libgnat/s-expint.ads: Mark in SPARK. Adapt to change to
package.
* libgnat/s-explli.ads: Likewise.
* libgnat/s-expllli.ads: Likewise.
* libgnat/s-expont.adb: Add lemmas and ghost code.
* libgnat/s-expont.ads: Add functional contract.

gcc/ada/libgnat/s-expint.ads
gcc/ada/libgnat/s-explli.ads
gcc/ada/libgnat/s-expllli.ads
gcc/ada/libgnat/s-expont.adb
gcc/ada/libgnat/s-expont.ads

index f41b6fa..b44cae5 100644 (file)
 
 --  Integer exponentiation (checks on)
 
+--  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);
+
 with System.Expont;
 
-package System.Exp_Int is
+package System.Exp_Int
+  with SPARK_Mode
+is
+
+   package Expont_Integer is new Expont (Integer);
 
-   function Exp_Integer is new Expont (Integer);
-   pragma Pure_Function (Exp_Integer);
+   function Exp_Integer (Left : Integer; Right : Natural) return Integer
+     renames Expont_Integer.Expon;
 
 end System.Exp_Int;
index d9c8544..ebf5794 100644 (file)
 
 --  Long_Long_Integer exponentiation (checks on)
 
+--  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);
+
 with System.Expont;
 
-package System.Exp_LLI is
+package System.Exp_LLI
+  with SPARK_Mode
+is
+
+   package Expont_Integer is new Expont (Long_Long_Integer);
 
-   function Exp_Long_Long_Integer is new Expont (Long_Long_Integer);
-   pragma Pure_Function (Exp_Long_Long_Integer);
+   function Exp_Long_Long_Integer
+     (Left : Long_Long_Integer; Right : Natural) return Long_Long_Integer
+     renames Expont_Integer.Expon;
 
 end System.Exp_LLI;
index 1ee278d..3c009bc 100644 (file)
 
 --  Long_Long_Long_Integer exponentiation (checks on)
 
+--  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);
+
 with System.Expont;
 
-package System.Exp_LLLI is
+package System.Exp_LLLI
+  with SPARK_Mode
+is
+
+   package Expont_Integer is new Expont (Long_Long_Long_Integer);
 
-   function Exp_Long_Long_Long_Integer is new Expont (Long_Long_Long_Integer);
-   pragma Pure_Function (Exp_Long_Long_Long_Integer);
+   function Exp_Long_Long_Long_Integer
+     (Left : Long_Long_Long_Integer; Right : Natural)
+      return Long_Long_Long_Integer
+     renames Expont_Integer.Expon;
 
 end System.Exp_LLLI;
index 3c259cf..dc1586b 100644 (file)
 --                                                                          --
 ------------------------------------------------------------------------------
 
-function System.Expont (Left : Int; Right : Natural) return Int is
+package body System.Expont
+  with SPARK_Mode
+is
 
-   --  Note that negative exponents get a constraint error because the
-   --  subtype of the Right argument (the exponent) is Natural.
+   --  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.
 
-   Result : Int     := 1;
-   Factor : Int     := Left;
-   Exp    : Natural := Right;
+   pragma Assertion_Policy (Pre            => Ignore,
+                            Post           => Ignore,
+                            Ghost          => Ignore,
+                            Loop_Invariant => Ignore,
+                            Assert         => Ignore);
 
-begin
-   --  We use the standard logarithmic approach, Exp gets shifted right
-   --  testing successive low order bits and Factor is the value of the
-   --  base raised to the next power of 2.
+   --  Local lemmas
 
-   --  Note: it is not worth special casing base values -1, 0, +1 since
-   --  the expander does this when the base is a literal, and other cases
-   --  will be extremely rare.
+   procedure Lemma_Exp_Expand (A : Big_Integer; Exp : Natural)
+   with
+     Ghost,
+     Pre  => A /= 0,
+     Post =>
+       (if Exp rem 2 = 0 then
+          A ** Exp = A ** (Exp / 2) * A ** (Exp / 2)
+        else
+          A ** Exp = A ** (Exp / 2) * A ** (Exp / 2) * A);
+
+   procedure Lemma_Exp_In_Range (A : Big_Integer; Exp : Positive)
+   with
+     Ghost,
+     Pre  => In_Int_Range (A ** Exp * A ** Exp),
+     Post => In_Int_Range (A * A);
+
+   procedure Lemma_Exp_Not_Zero (A : Big_Integer; Exp : Natural)
+   with
+     Ghost,
+     Pre  => A /= 0,
+     Post => A ** Exp /= 0;
+
+   procedure Lemma_Exp_Positive (A : Big_Integer; Exp : Natural)
+   with
+     Ghost,
+     Pre  => A /= 0
+       and then Exp rem 2 = 0,
+     Post => A ** Exp > 0;
+
+   procedure Lemma_Mult_In_Range (X, Y, Z : Big_Integer)
+   with
+     Ghost,
+     Pre  => Y /= 0
+       and then not (X = -Big (Int'First) and Y = -1)
+       and then X * Y = Z
+       and then In_Int_Range (Z),
+     Post => In_Int_Range (X);
+
+   -----------------------------
+   -- Local lemma null bodies --
+   -----------------------------
+
+   procedure Lemma_Exp_Not_Zero (A : Big_Integer; Exp : Natural) is null;
+   procedure Lemma_Mult_In_Range (X, Y, Z : Big_Integer) is null;
+
+   -----------
+   -- Expon --
+   -----------
+
+   function Expon (Left : Int; Right : Natural) return Int is
+
+      --  Note that negative exponents get a constraint error because the
+      --  subtype of the Right argument (the exponent) is Natural.
+
+      Result : Int     := 1;
+      Factor : Int     := Left;
+      Exp    : Natural := Right;
+
+      Rest : Big_Integer with Ghost;
+      --  Ghost variable to hold Factor**Exp between Exp and Factor updates
+
+   begin
+      --  We use the standard logarithmic approach, Exp gets shifted right
+      --  testing successive low order bits and Factor is the value of the
+      --  base raised to the next power of 2.
+
+      --  Note: for compilation only, it is not worth special casing base
+      --  values -1, 0, +1 since the expander does this when the base is a
+      --  literal, and other cases will be extremely rare. But for proof,
+      --  special casing zero in both positions makes ghost code and lemmas
+      --  simpler, so we do it.
+
+      if Right = 0 then
+         return 1;
+      elsif Left = 0 then
+         return 0;
+      end if;
 
-   if Exp /= 0 then
       loop
+         pragma Loop_Invariant (Exp > 0);
+         pragma Loop_Invariant (Factor /= 0);
+         pragma Loop_Invariant
+           (Big (Result) * Big (Factor) ** Exp = Big (Left) ** Right);
+         pragma Loop_Variant (Decreases => Exp);
+         pragma Annotate
+           (CodePeer, False_Positive,
+            "validity check", "confusion on generated code");
+
          if Exp rem 2 /= 0 then
             declare
                pragma Unsuppress (Overflow_Check);
             begin
+               pragma Assert
+                 (Big (Factor) ** Exp
+                  = Big (Factor) * Big (Factor) ** (Exp - 1));
+               Lemma_Exp_Positive (Big (Factor), Exp - 1);
+               Lemma_Mult_In_Range (Big (Result) * Big (Factor),
+                                    Big (Factor) ** (Exp - 1),
+                                    Big (Left) ** Right);
+
                Result := Result * Factor;
             end;
          end if;
 
+         Lemma_Exp_Expand (Big (Factor), Exp);
+
          Exp := Exp / 2;
          exit when Exp = 0;
 
+         Rest := Big (Factor) ** Exp;
+         pragma Assert
+           (Big (Result) * (Rest * Rest) = Big (Left) ** Right);
+
          declare
             pragma Unsuppress (Overflow_Check);
          begin
+            Lemma_Mult_In_Range (Rest * Rest,
+                                 Big (Result),
+                                 Big (Left) ** Right);
+            Lemma_Exp_In_Range (Big (Factor), Exp);
+
             Factor := Factor * Factor;
          end;
+
+         pragma Assert (Big (Factor) ** Exp = Rest * Rest);
       end loop;
-   end if;
 
-   return Result;
+      pragma Assert (Big (Result) = Big (Left) ** Right);
+
+      return Result;
+   end Expon;
+
+   ----------------------
+   -- Lemma_Exp_Expand --
+   ----------------------
+
+   procedure Lemma_Exp_Expand (A : Big_Integer; Exp : Natural) is
+   begin
+      if Exp rem 2 = 0 then
+         pragma Assert (Exp = Exp / 2 + Exp / 2);
+      else
+         pragma Assert (Exp = Exp / 2 + Exp / 2 + 1);
+         pragma Assert (A ** Exp = A ** (Exp / 2) * A ** (Exp / 2 + 1));
+         pragma Assert (A ** (Exp / 2 + 1) = A ** (Exp / 2) * A);
+         pragma Assert (A ** Exp = A ** (Exp / 2) * A ** (Exp / 2) * A);
+      end if;
+   end Lemma_Exp_Expand;
+
+   ------------------------
+   -- Lemma_Exp_In_Range --
+   ------------------------
+
+   procedure Lemma_Exp_In_Range (A : Big_Integer; Exp : Positive) is
+   begin
+      if A /= 0 and Exp /= 1 then
+         pragma Assert (A ** Exp = A * A ** (Exp - 1));
+         Lemma_Mult_In_Range
+           (A * A, A ** (Exp - 1) * A ** (Exp - 1), A ** Exp * A ** Exp);
+      end if;
+   end Lemma_Exp_In_Range;
+
+   ------------------------
+   -- Lemma_Exp_Positive --
+   ------------------------
+
+   procedure Lemma_Exp_Positive (A : Big_Integer; Exp : Natural) is
+   begin
+      if Exp = 0 then
+         pragma Assert (A ** Exp = 1);
+      else
+         pragma Assert (Exp = 2 * (Exp / 2));
+         pragma Assert (A ** Exp = A ** (Exp / 2) * A ** (Exp / 2));
+         pragma Assert (A ** Exp = (A ** (Exp / 2)) ** 2);
+         Lemma_Exp_Not_Zero (A, Exp / 2);
+      end if;
+   end Lemma_Exp_Positive;
+
 end System.Expont;
index 022cb64..4a62b18 100644 (file)
 
 --  Signed integer exponentiation (checks on)
 
+with Ada.Numerics.Big_Numbers.Big_Integers_Ghost;
+use Ada.Numerics.Big_Numbers.Big_Integers_Ghost;
+
 generic
 
    type Int is range <>;
 
-function System.Expont (Left : Int; Right : Natural) return Int;
+package System.Expont
+  with Pure, SPARK_Mode
+is
+
+   --  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);
+
+   package Signed_Conversion is new Signed_Conversions (Int => Int);
+
+   function Big (Arg : Int) return Big_Integer is
+     (Signed_Conversion.To_Big_Integer (Arg))
+   with Ghost;
+
+   function In_Int_Range (Arg : Big_Integer) return Boolean is
+     (In_Range (Arg, Big (Int'First), Big (Int'Last)))
+   with Ghost;
+
+   function Expon (Left : Int; Right : Natural) return Int
+   with
+     Pre  => In_Int_Range (Big (Left) ** Right),
+     Post => Expon'Result = Left ** Right;
+
+end System.Expont;