diff --git a/gcc/ada/libgnat/s-exnint.ads b/gcc/ada/libgnat/s-exnint.ads
--- a/gcc/ada/libgnat/s-exnint.ads
+++ b/gcc/ada/libgnat/s-exnint.ads
@@ -31,11 +31,26 @@
 
 --  Integer exponentiation (checks off)
 
+--  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.Exponn;
 
-package System.Exn_Int is
+package System.Exn_Int
+  with SPARK_Mode
+is
+
+   package Exponn_Integer is new Exponn (Integer);
 
-   function Exn_Integer is new Exponn (Integer);
-   pragma Pure_Function (Exn_Integer);
+   function Exn_Integer (Left : Integer; Right : Natural) return Integer
+     renames Exponn_Integer.Expon;
 
 end System.Exn_Int;


diff --git a/gcc/ada/libgnat/s-exnlli.ads b/gcc/ada/libgnat/s-exnlli.ads
--- a/gcc/ada/libgnat/s-exnlli.ads
+++ b/gcc/ada/libgnat/s-exnlli.ads
@@ -31,11 +31,27 @@
 
 --  Long_Long_Integer exponentiation (checks off)
 
+--  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.Exponn;
 
-package System.Exn_LLI is
+package System.Exn_LLI
+  with SPARK_Mode
+is
+
+   package Exponn_Integer is new Exponn (Long_Long_Integer);
 
-   function Exn_Long_Long_Integer is new Exponn (Long_Long_Integer);
-   pragma Pure_Function (Exn_Long_Long_Integer);
+   function Exn_Long_Long_Integer
+     (Left : Long_Long_Integer; Right : Natural) return Long_Long_Integer
+     renames Exponn_Integer.Expon;
 
 end System.Exn_LLI;


diff --git a/gcc/ada/libgnat/s-exnllli.ads b/gcc/ada/libgnat/s-exnllli.ads
--- a/gcc/ada/libgnat/s-exnllli.ads
+++ b/gcc/ada/libgnat/s-exnllli.ads
@@ -31,11 +31,28 @@
 
 --  Long_Long_Long_Integer exponentiation (checks off)
 
+--  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.Exponn;
 
-package System.Exn_LLLI is
+package System.Exn_LLLI
+  with SPARK_Mode
+is
+
+   package Exponn_Integer is new Exponn (Long_Long_Long_Integer);
 
-   function Exn_Long_Long_Long_Integer is new Exponn (Long_Long_Long_Integer);
-   pragma Pure_Function (Exn_Long_Long_Long_Integer);
+   function Exn_Long_Long_Long_Integer
+     (Left : Long_Long_Long_Integer; Right : Natural)
+      return Long_Long_Long_Integer
+     renames Exponn_Integer.Expon;
 
 end System.Exn_LLLI;


diff --git a/gcc/ada/libgnat/s-exponn.adb b/gcc/ada/libgnat/s-exponn.adb
--- a/gcc/ada/libgnat/s-exponn.adb
+++ b/gcc/ada/libgnat/s-exponn.adb
@@ -29,44 +29,198 @@
 --                                                                          --
 ------------------------------------------------------------------------------
 
-function System.Exponn (Left : Int; Right : Natural) return Int is
+package body System.Exponn
+  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 Suppress (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 Suppress (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.Exponn;


diff --git a/gcc/ada/libgnat/s-exponn.ads b/gcc/ada/libgnat/s-exponn.ads
--- a/gcc/ada/libgnat/s-exponn.ads
+++ b/gcc/ada/libgnat/s-exponn.ads
@@ -31,8 +31,41 @@
 
 --  Signed integer exponentiation (checks off)
 
+with Ada.Numerics.Big_Numbers.Big_Integers_Ghost;
+use Ada.Numerics.Big_Numbers.Big_Integers_Ghost;
+
 generic
 
    type Int is range <>;
 
-function System.Exponn (Left : Int; Right : Natural) return Int;
+package System.Exponn
+  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.Exponn;


