[Ada] Fix proof of runtime unit System.Value* and System.Image*

Refactor specification of the Value* and Image* units and fix proofs.

gcc/ada/

	* libgnat/a-nbnbig.ads: Add Always_Return annotation.
	* libgnat/s-vaispe.ads: New ghost unit for the specification of
	System.Value_I. Restore proofs.
	* libgnat/s-vauspe.ads: New ghost unit for the specification of
	System.Value_U. Restore proofs.
	* libgnat/s-valuei.adb: The specification only subprograms are
	moved to System.Value_I_Spec. Restore proofs.
	* libgnat/s-valueu.adb: The specification only subprograms are
	moved to System.Value_U_Spec. Restore proofs.
	* libgnat/s-valuti.ads
	(Uns_Params): Generic unit used to bundle together the
	specification functions of System.Value_U_Spec.
	(Int_Params): Generic unit used to bundle together the
	specification functions of System.Value_I_Spec.
	* libgnat/s-imagef.adb: It is now possible to instantiate the
	appropriate specification units instead of creating imported ghost
	subprograms.
	* libgnat/s-imagei.adb: Update to refactoring of specifications
	and fix proofs.
	* libgnat/s-imageu.adb: Likewise.
	* libgnat/s-imgint.ads: Ghost parameters are grouped together in a
	package now.
	* libgnat/s-imglli.ads: Likewise.
	* libgnat/s-imgllu.ads: Likewise.
	* libgnat/s-imgllli.ads: Likewise.
	* libgnat/s-imglllu.ads: Likewise.
	* libgnat/s-imguns.ads: Likewise.
	* libgnat/s-vallli.ads: Likewise.
	* libgnat/s-valllli.ads: Likewise.
	* libgnat/s-imagei.ads: Likewise.
	* libgnat/s-imageu.ads: Likewise.
	* libgnat/s-vaispe.adb: Likewise.
	* libgnat/s-valint.ads: Likewise.
	* libgnat/s-valuei.ads: Likewise.
	* libgnat/s-valueu.ads: Likewise.
	* libgnat/s-vauspe.adb: Likewise.

24 files changed, 1853 insertions, 1547 deletions

diff --git a/gcc/ada/libgnat/a-nbnbig.ads b/gcc/ada/libgnat/a-nbnbig.ads
index f574e78..3979f14 100644
--- a/gcc/ada/libgnat/a-nbnbig.ads
+++ b/gcc/ada/libgnat/a-nbnbig.ads
@@ -32,6 +32,8 @@ package Ada.Numerics.Big_Numbers.Big_Integers_Ghost with
    Ghost,
    Pure
 is
+   pragma Annotate (GNATprove, Always_Return, Big_Integers_Ghost);
+
    type Big_Integer is private
      with Integer_Literal => From_Universal_Image;
 
diff --git a/gcc/ada/libgnat/s-imagef.adb b/gcc/ada/libgnat/s-imagef.adb
index fd8e848..bfe8540 100644
--- a/gcc/ada/libgnat/s-imagef.adb
+++ b/gcc/ada/libgnat/s-imagef.adb
@@ -31,7 +31,8 @@
 
 with System.Image_I;
 with System.Img_Util; use System.Img_Util;
-with System.Val_Util;
+with System.Value_I_Spec;
+with System.Value_U_Spec;
 
 package body System.Image_F is
 
@@ -69,70 +70,16 @@ package body System.Image_F is
    --  if the small is larger than 1, and smaller than 2**(Int'Size - 1) / 10
    --  if the small is smaller than 1.
 
-   --  Define ghost subprograms without implementation (marked as Import) to
-   --  create a suitable package Int_Params for type Int, as instantiations
-   --  of System.Image_F use for this type one of the derived integer types
-   --  defined in Interfaces, instead of the standard signed integer types
-   --  which are used to define System.Img_*.Int_Params.
-
-   type Uns_Option (Overflow : Boolean := False) is record
-      case Overflow is
-         when True =>
-            null;
-         when False =>
-            Value : Uns := 0;
-      end case;
-   end record;
-
    Unsigned_Width_Ghost : constant Natural := Int'Width;
 
-   function Wrap_Option (Value : Uns) return Uns_Option
-     with Ghost, Import;
-   function Only_Decimal_Ghost
-     (Str      : String;
-      From, To : Integer)
-      return Boolean
-     with Ghost, Import;
-   function Hexa_To_Unsigned_Ghost (X : Character) return Uns
-     with Ghost, Import;
-   function Scan_Based_Number_Ghost
-     (Str      : String;
-      From, To : Integer;
-      Base     : Uns := 10;
-      Acc      : Uns := 0)
-      return Uns_Option
-     with Ghost, Import;
-   function Is_Integer_Ghost (Str : String) return Boolean
-     with Ghost, Import;
-   procedure Prove_Iter_Scan_Based_Number_Ghost
-     (Str1, Str2 : String;
-      From, To : Integer;
-      Base     : Uns := 10;
-      Acc      : Uns := 0)
-     with Ghost, Import;
-   procedure Prove_Scan_Only_Decimal_Ghost (Str : String; Val : Int)
-     with Ghost, Import;
-   function Abs_Uns_Of_Int (Val : Int) return Uns
-     with Ghost, Import;
-   function Value_Integer (Str : String) return Int
-     with Ghost, Import;
-
-   package Int_Params is new Val_Util.Int_Params
-     (Int                                => Int,
-      Uns                                => Uns,
-      Uns_Option                         => Uns_Option,
-      Unsigned_Width_Ghost               => Unsigned_Width_Ghost,
-      Wrap_Option                        => Wrap_Option,
-      Only_Decimal_Ghost                 => Only_Decimal_Ghost,
-      Hexa_To_Unsigned_Ghost             => Hexa_To_Unsigned_Ghost,
-      Scan_Based_Number_Ghost            => Scan_Based_Number_Ghost,
-      Is_Integer_Ghost                   => Is_Integer_Ghost,
-      Prove_Iter_Scan_Based_Number_Ghost => Prove_Iter_Scan_Based_Number_Ghost,
-      Prove_Scan_Only_Decimal_Ghost      => Prove_Scan_Only_Decimal_Ghost,
-      Abs_Uns_Of_Int                     => Abs_Uns_Of_Int,
-      Value_Integer                      => Value_Integer);
-
-   package Image_I is new System.Image_I (Int_Params);
+   package Uns_Spec is new System.Value_U_Spec (Uns);
+   package Int_Spec is new System.Value_I_Spec (Int, Uns, Uns_Spec.Uns_Params);
+
+   package Image_I is new System.Image_I
+     (Int                  => Int,
+      Uns                  => Uns,
+      Unsigned_Width_Ghost => Unsigned_Width_Ghost,
+      Int_Params           => Int_Spec.Int_Params);
 
    procedure Set_Image_Integer
      (V : Int;
diff --git a/gcc/ada/libgnat/s-imagei.adb b/gcc/ada/libgnat/s-imagei.adb
index ff853d3..8997e3c 100644
--- a/gcc/ada/libgnat/s-imagei.adb
+++ b/gcc/ada/libgnat/s-imagei.adb
@@ -46,42 +46,6 @@ package body System.Image_I is
                             Post               => Ignore,
                             Subprogram_Variant => Ignore);
 
-   --  As a use_clause for Int_Params cannot be used for instances of this
-   --  generic in System specs, rename all constants and subprograms.
-
-   Unsigned_Width_Ghost : constant Natural := Int_Params.Unsigned_Width_Ghost;
-
-   function Wrap_Option (Value : Uns) return Uns_Option
-     renames Int_Params.Wrap_Option;
-   function Only_Decimal_Ghost
-     (Str      : String;
-      From, To : Integer)
-      return Boolean
-      renames Int_Params.Only_Decimal_Ghost;
-   function Hexa_To_Unsigned_Ghost (X : Character) return Uns
-     renames Int_Params.Hexa_To_Unsigned_Ghost;
-   function Scan_Based_Number_Ghost
-     (Str      : String;
-      From, To : Integer;
-      Base     : Uns := 10;
-      Acc      : Uns := 0)
-      return Uns_Option
-      renames Int_Params.Scan_Based_Number_Ghost;
-   function Is_Integer_Ghost (Str : String) return Boolean
-     renames Int_Params.Is_Integer_Ghost;
-   procedure Prove_Iter_Scan_Based_Number_Ghost
-     (Str1, Str2 : String;
-      From, To : Integer;
-      Base     : Uns := 10;
-      Acc      : Uns := 0)
-      renames Int_Params.Prove_Iter_Scan_Based_Number_Ghost;
-   procedure Prove_Scan_Only_Decimal_Ghost (Str : String; Val : Int)
-     renames Int_Params.Prove_Scan_Only_Decimal_Ghost;
-   function Abs_Uns_Of_Int (Val : Int) return Uns
-     renames Int_Params.Abs_Uns_Of_Int;
-   function Value_Integer (Str : String) return Int
-     renames Int_Params.Value_Integer;
-
    subtype Non_Positive is Int range Int'First .. 0;
 
    function Uns_Of_Non_Positive (T : Non_Positive) return Uns is
@@ -99,9 +63,9 @@ package body System.Image_I is
        and then P <= S'Last - Unsigned_Width_Ghost + 1,
      Post => S (S'First .. P'Old) = S'Old (S'First .. P'Old)
        and then P in P'Old + 1 .. S'Last
-       and then Only_Decimal_Ghost (S, From => P'Old + 1, To => P)
-       and then Scan_Based_Number_Ghost (S, From => P'Old + 1, To => P)
-         = Wrap_Option (Uns_Of_Non_Positive (T));
+       and then UP.Only_Decimal_Ghost (S, From => P'Old + 1, To => P)
+       and then UP.Scan_Based_Number_Ghost (S, From => P'Old + 1, To => P)
+         = UP.Wrap_Option (Uns_Of_Non_Positive (T));
    --  Set digits of absolute value of T, which is zero or negative. We work
    --  with the negative of the value so that the largest negative number is
    --  not a special case.
@@ -182,11 +146,12 @@ package body System.Image_I is
           and then P in 2 .. S'Last
           and then S (1) in ' ' | '-'
           and then (S (1) = '-') = (V < 0)
-          and then Only_Decimal_Ghost (S, From => 2, To => P)
-          and then Scan_Based_Number_Ghost (S, From => 2, To => P)
-            = Wrap_Option (Abs_Uns_Of_Int (V)),
-        Post => Is_Integer_Ghost (S (1 .. P))
-          and then Value_Integer (S (1 .. P)) = V;
+          and then UP.Only_Decimal_Ghost (S, From => 2, To => P)
+          and then UP.Scan_Based_Number_Ghost (S, From => 2, To => P)
+            = UP.Wrap_Option (IP.Abs_Uns_Of_Int (V)),
+        Post => not System.Val_Util.Only_Space_Ghost (S, 1, P)
+          and then IP.Is_Integer_Ghost (S (1 .. P))
+          and then IP.Is_Value_Integer_Ghost (S (1 .. P), V);
       --  Ghost lemma to prove the value of Value_Integer from the value of
       --  Scan_Based_Number_Ghost and the sign on a decimal string.
 
@@ -198,11 +163,14 @@ package body System.Image_I is
          Str : constant String := S (1 .. P);
       begin
          pragma Assert (Str'First = 1);
-         pragma Assert (Only_Decimal_Ghost (Str, From => 2, To => P));
-         Prove_Iter_Scan_Based_Number_Ghost (S, Str, From => 2, To => P);
-         pragma Assert (Scan_Based_Number_Ghost (Str, From => 2, To => P)
-            = Wrap_Option (Abs_Uns_Of_Int (V)));
-         Prove_Scan_Only_Decimal_Ghost (Str, V);
+         pragma Assert (Str (2) /= ' ');
+         pragma Assert
+           (UP.Only_Decimal_Ghost (Str, From => 2, To => P));
+         UP.Prove_Scan_Based_Number_Ghost_Eq (S, Str, From => 2, To => P);
+         pragma Assert
+           (UP.Scan_Based_Number_Ghost (Str, From => 2, To => P)
+            = UP.Wrap_Option (IP.Abs_Uns_Of_Int (V)));
+         IP.Prove_Scan_Only_Decimal_Ghost (Str, V);
       end Prove_Value_Integer;
 
    --  Start of processing for Image_Integer
@@ -226,6 +194,8 @@ package body System.Image_I is
 
          pragma Assert (P_Prev + Offset = 2);
       end;
+      pragma Assert (if V >= 0 then S (1) = ' ');
+      pragma Assert (S (1) in ' ' | '-');
 
       Prove_Value_Integer;
    end Image_Integer;
@@ -248,42 +218,78 @@ package body System.Image_I is
       S_Init     : constant String := S with Ghost;
       Uns_T      : constant Uns := Uns_Of_Non_Positive (T) with Ghost;
       Uns_Value  : Uns := Uns_Of_Non_Positive (Value) with Ghost;
-      Prev, Cur  : Uns_Option with Ghost;
       Prev_Value : Uns with Ghost;
       Prev_S     : String := S with Ghost;
 
       --  Local ghost lemmas
 
-      procedure Prove_Character_Val (RU : Uns; RI : Int)
+      procedure Prove_Character_Val (RU : Uns; RI : Non_Positive)
       with
         Ghost,
-        Pre  => RU in 0 .. 9
-          and then RI in 0 .. 9,
-        Post => Character'Val (48 + RU) in '0' .. '9'
-          and then Character'Val (48 + RI) in '0' .. '9';
+        Post => RU rem 10 in 0 .. 9
+          and then -(RI rem 10) in 0 .. 9
+          and then Character'Val (48 + RU rem 10) in '0' .. '9'
+          and then Character'Val (48 - RI rem 10) in '0' .. '9';
       --  Ghost lemma to prove the value of a character corresponding to the
       --  next figure.
 
+      procedure Prove_Euclidian (Val, Quot, Rest : Uns)
+      with
+        Ghost,
+        Pre  => Quot = Val / 10
+          and then Rest = Val rem 10,
+        Post => Uns'Last - Rest >= 10 * Quot and then Val = 10 * Quot + Rest;
+      --  Ghost lemma to prove the relation between the quotient/remainder of
+      --  division by 10 and the initial value.
+
       procedure Prove_Hexa_To_Unsigned_Ghost (RU : Uns; RI : Int)
       with
         Ghost,
         Pre  => RU in 0 .. 9
           and then RI in 0 .. 9,
-        Post => Hexa_To_Unsigned_Ghost (Character'Val (48 + RU)) = RU
-          and then Hexa_To_Unsigned_Ghost (Character'Val (48 + RI)) = Uns (RI);
+        Post => UP.Hexa_To_Unsigned_Ghost
+            (Character'Val (48 + RU)) = RU
+          and then UP.Hexa_To_Unsigned_Ghost
+            (Character'Val (48 + RI)) = Uns (RI);
       --  Ghost lemma to prove that Hexa_To_Unsigned_Ghost returns the source
       --  figure when applied to the corresponding character.
 
-      procedure Prove_Unchanged
-      with
-        Ghost,
-        Pre  => P <= S'Last
-          and then S_Init'First = S'First
-          and then S_Init'Last = S'Last
-          and then (for all K in S'First .. P => S (K) = S_Init (K)),
-        Post => S (S'First .. P) = S_Init (S'First .. P);
-      --  Ghost lemma to prove that the part of string S before P has not been
-      --  modified.
+      procedure Prove_Scan_Iter
+        (S, Prev_S      : String;
+         V, Prev_V, Res : Uns;
+         P, Max         : Natural)
+        with
+          Ghost,
+          Pre =>
+            S'First = Prev_S'First and then S'Last = Prev_S'Last
+            and then S'Last < Natural'Last and then
+            Max in S'Range and then P in S'First .. Max and then
+            (for all I in P + 1 .. Max => Prev_S (I) in '0' .. '9')
+            and then (for all I in P + 1 .. Max => Prev_S (I) = S (I))
+            and then S (P) in '0' .. '9'
+            and then V <= Uns'Last / 10
+            and then Uns'Last - UP.Hexa_To_Unsigned_Ghost (S (P))
+              >= 10 * V
+            and then Prev_V =
+              V * 10 + UP.Hexa_To_Unsigned_Ghost (S (P))
+            and then
+              (if P = Max then Prev_V = Res
+               else UP.Scan_Based_Number_Ghost
+                 (Str  => Prev_S,
+                  From => P + 1,
+                  To   => Max,
+                  Base => 10,
+                  Acc  => Prev_V) = UP.Wrap_Option (Res)),
+          Post =>
+            (for all I in P .. Max => S (I) in '0' .. '9')
+            and then UP.Scan_Based_Number_Ghost
+              (Str  => S,
+               From => P,
+               To   => Max,
+               Base => 10,
+               Acc  => V) = UP.Wrap_Option (Res);
+      --  Ghost lemma to prove that Scan_Based_Number_Ghost is preserved
+      --  through an iteration of the loop.
 
       procedure Prove_Uns_Of_Non_Positive_Value
       with
@@ -294,50 +300,44 @@ package body System.Image_I is
       --  Ghost lemma to prove that the relation between Value and its unsigned
       --  version is preserved.
 
-      procedure Prove_Iter_Scan
-        (Str1, Str2 : String;
-         From, To : Integer;
-         Base     : Uns := 10;
-         Acc      : Uns := 0)
-      with
-        Ghost,
-        Pre  => Str1'Last /= Positive'Last
-          and then
-            (From > To or else (From >= Str1'First and then To <= Str1'Last))
-          and then Only_Decimal_Ghost (Str1, From, To)
-          and then Str1'First = Str2'First
-          and then Str1'Last = Str2'Last
-          and then (for all J in From .. To => Str1 (J) = Str2 (J)),
-        Post =>
-          Scan_Based_Number_Ghost (Str1, From, To, Base, Acc)
-            = Scan_Based_Number_Ghost (Str2, From, To, Base, Acc);
-      --  Ghost lemma to prove that the result of Scan_Based_Number_Ghost only
-      --  depends on the value of the argument string in the (From .. To) range
-      --  of indexes. This is a wrapper on Prove_Iter_Scan_Based_Number_Ghost
-      --  so that we can call it here on ghost arguments.
-
       -----------------------------
       -- Local lemma null bodies --
       -----------------------------
 
-      procedure Prove_Character_Val (RU : Uns; RI : Int) is null;
+      procedure Prove_Character_Val (RU : Uns; RI : Non_Positive) is null;
+      procedure Prove_Euclidian (Val, Quot, Rest : Uns) is null;
       procedure Prove_Hexa_To_Unsigned_Ghost (RU : Uns; RI : Int) is null;
-      procedure Prove_Unchanged is null;
       procedure Prove_Uns_Of_Non_Positive_Value is null;
 
       ---------------------
-      -- Prove_Iter_Scan --
+      -- Prove_Scan_Iter --
       ---------------------
 
-      procedure Prove_Iter_Scan
-        (Str1, Str2 : String;
-         From, To : Integer;
-         Base     : Uns := 10;
-         Acc      : Uns := 0)
+      procedure Prove_Scan_Iter
+        (S, Prev_S      : String;
+         V, Prev_V, Res : Uns;
+         P, Max         : Natural)
       is
+         pragma Unreferenced (Res);
       begin
-         Prove_Iter_Scan_Based_Number_Ghost (Str1, Str2, From, To, Base, Acc);
-      end Prove_Iter_Scan;
+         UP.Lemma_Scan_Based_Number_Ghost_Step
+           (Str  => S,
+            From => P,
+            To   => Max,
+            Base => 10,
+            Acc  => V);
+         if P < Max then
+            UP.Prove_Scan_Based_Number_Ghost_Eq
+              (Prev_S, S, P + 1, Max, 10, Prev_V);
+         else
+            UP.Lemma_Scan_Based_Number_Ghost_Base
+              (Str  => S,
+               From => P + 1,
+               To   => Max,
+               Base => 10,
+               Acc  => Prev_V);
+         end if;
+      end Prove_Scan_Iter;
 
    --  Start of processing for Set_Digits
 
@@ -383,13 +383,9 @@ package body System.Image_I is
       for J in reverse  1 .. Nb_Digits loop
          Lemma_Div_Commutation (Uns_Value, 10);
          Lemma_Div_Twice (Big (Uns_T), Big_10 ** (Nb_Digits - J), Big_10);
-         Prove_Character_Val (Uns_Value rem 10, -(Value rem 10));
+         Prove_Character_Val (Uns_Value, Value);
          Prove_Hexa_To_Unsigned_Ghost (Uns_Value rem 10, -(Value rem 10));
          Prove_Uns_Of_Non_Positive_Value;
-         pragma Assert (Uns_Value rem 10 = Uns_Of_Non_Positive (Value rem 10));
-         pragma Assert (Uns_Value rem 10 = Uns (-(Value rem 10)));
-         pragma Assert
-           (Uns_Value = From_Big (Big (Uns_T) / Big_10 ** (Nb_Digits - J)));
 
          Prev_Value := Uns_Value;
          Prev_S := S;
@@ -399,68 +395,44 @@ package body System.Image_I is
          S (P + J) := Character'Val (48 - (Value rem 10));
          Value := Value / 10;
 
-         pragma Assert (S (P + J) in '0' .. '9');
-         pragma Assert (Hexa_To_Unsigned_Ghost (S (P + J)) =
-           From_Big (Big (Uns_T) / Big_10 ** (Nb_Digits - J)) rem 10);
-         pragma Assert
-           (for all K in P + J + 1 .. P + Nb_Digits => S (K) in '0' .. '9');
+         Prove_Euclidian
+           (Val  => Prev_Value,
+            Quot => Uns_Value,
+            Rest => UP.Hexa_To_Unsigned_Ghost (S (P + J)));
 
-         Prev := Scan_Based_Number_Ghost
-           (Str  => S,
-            From => P + J + 1,
-            To   => P + Nb_Digits,
-            Base => 10,
-            Acc  => Prev_Value);
-         Cur := Scan_Based_Number_Ghost
-           (Str  => S,
-            From => P + J,
-            To   => P + Nb_Digits,
-            Base => 10,
-            Acc  => Uns_Value);
-         pragma Assert (Prev_Value = 10 * Uns_Value + (Prev_Value rem 10));
-         pragma Assert
-           (Prev_Value rem 10 = Hexa_To_Unsigned_Ghost (S (P + J)));
-         pragma Assert
-           (Prev_Value = 10 * Uns_Value + Hexa_To_Unsigned_Ghost (S (P + J)));
-
-         if J /= Nb_Digits then
-            Prove_Iter_Scan
-              (Prev_S, S, P + J + 1, P + Nb_Digits, 10, Prev_Value);
-         end if;
-
-         pragma Assert (Prev = Cur);
-         pragma Assert (Prev = Wrap_Option (Uns_T));
+         Prove_Scan_Iter
+           (S, Prev_S, Uns_Value, Prev_Value, Uns_T, P + J, P + Nb_Digits);
 
          pragma Loop_Invariant (Uns_Value = Uns_Of_Non_Positive (Value));
          pragma Loop_Invariant (Uns_Value <= Uns'Last / 10);
          pragma Loop_Invariant
            (for all K in S'First .. P => S (K) = S_Init (K));
-         pragma Loop_Invariant (Only_Decimal_Ghost (S, P + J, P + Nb_Digits));
+         pragma Loop_Invariant
+           (UP.Only_Decimal_Ghost (S, P + J, P + Nb_Digits));
          pragma Loop_Invariant
            (for all K in P + J .. P + Nb_Digits => S (K) in '0' .. '9');
          pragma Loop_Invariant (Pow = Big_10 ** (Nb_Digits - J + 1));
          pragma Loop_Invariant (Big (Uns_Value) = Big (Uns_T) / Pow);
          pragma Loop_Invariant
-           (Scan_Based_Number_Ghost
+           (UP.Scan_Based_Number_Ghost
               (Str  => S,
                From => P + J,
                To   => P + Nb_Digits,
                Base => 10,
                Acc  => Uns_Value)
-              = Wrap_Option (Uns_T));
+              = UP.Wrap_Option (Uns_T));
       end loop;
 
       pragma Assert (Big (Uns_Value) = Big (Uns_T) / Big_10 ** (Nb_Digits));
       pragma Assert (Uns_Value = 0);
-      Prove_Unchanged;
       pragma Assert
-        (Scan_Based_Number_Ghost
+        (UP.Scan_Based_Number_Ghost
            (Str  => S,
             From => P + 1,
             To   => P + Nb_Digits,
             Base => 10,
             Acc  => Uns_Value)
-         = Wrap_Option (Uns_T));
+         = UP.Wrap_Option (Uns_T));
 
       P := P + Nb_Digits;
    end Set_Digits;
diff --git a/gcc/ada/libgnat/s-imagei.ads b/gcc/ada/libgnat/s-imagei.ads
index 10116d1..575c60a 100644
--- a/gcc/ada/libgnat/s-imagei.ads
+++ b/gcc/ada/libgnat/s-imagei.ads
@@ -48,19 +48,19 @@ pragma Assertion_Policy (Pre                => Ignore,
 with System.Val_Util;
 
 generic
+   type Int is range <>;
+   type Uns is mod <>;
 
-   with package Int_Params is new System.Val_Util.Int_Params (<>);
+   Unsigned_Width_Ghost : Natural;
 
-package System.Image_I is
-
-   subtype Int is Int_Params.Int;
-   use type Int_Params.Int;
+   with package Int_Params is new System.Val_Util.Int_Params
+     (Int => Int, Uns => Uns, others => <>)
+   with Ghost;
 
-   subtype Uns is Int_Params.Uns;
-   use type Int_Params.Uns;
-
-   subtype Uns_Option is Int_Params.Uns_Option;
-   use type Int_Params.Uns_Option;
+package System.Image_I is
+   package IP renames Int_Params;
+   package UP renames IP.Uns_Params;
+   use type UP.Uns_Option;
 
    procedure Image_Integer
      (V : Int;
@@ -69,9 +69,9 @@ package System.Image_I is
    with
      Pre  => S'First = 1
        and then S'Last < Integer'Last
-       and then S'Last >= Int_Params.Unsigned_Width_Ghost,
+       and then S'Last >= Unsigned_Width_Ghost,
      Post => P in S'Range
-       and then Int_Params.Value_Integer (S (1 .. P)) = V;
+       and then IP.Is_Value_Integer_Ghost (S (1 .. P), V);
    --  Computes Int'Image (V) and stores the result in S (1 .. P)
    --  setting the resulting value of P. The caller guarantees that S
    --  is long enough to hold the result, and that S'First is 1.
@@ -87,23 +87,23 @@ package System.Image_I is
        and then S'First <= S'Last
        and then
          (if V >= 0 then
-            P <= S'Last - Int_Params.Unsigned_Width_Ghost + 1
+            P <= S'Last - Unsigned_Width_Ghost + 1
           else
-            P <= S'Last - Int_Params.Unsigned_Width_Ghost),
+            P <= S'Last - Unsigned_Width_Ghost),
      Post => S (S'First .. P'Old) = S'Old (S'First .. P'Old)
        and then
          (declare
             Minus  : constant Boolean := S (P'Old + 1) = '-';
             Offset : constant Positive := (if V >= 0 then 1 else 2);
-            Abs_V  : constant Uns := Int_Params.Abs_Uns_Of_Int (V);
+            Abs_V  : constant Uns := IP.Abs_Uns_Of_Int (V);
           begin
             Minus = (V < 0)
               and then P in P'Old + Offset .. S'Last
-              and then Int_Params.Only_Decimal_Ghost
+              and then UP.Only_Decimal_Ghost
                 (S, From => P'Old + Offset, To => P)
-              and then Int_Params.Scan_Based_Number_Ghost
+              and then UP.Scan_Based_Number_Ghost
                 (S, From => P'Old + Offset, To => P)
-                = Int_Params.Wrap_Option (Abs_V));
+                = UP.Wrap_Option (Abs_V));
    --  Stores the image of V in S starting at S (P + 1), P is updated to point
    --  to the last character stored. The value stored is identical to the value
    --  of Int'Image (V) except that no leading space is stored when V is
diff --git a/gcc/ada/libgnat/s-imageu.adb b/gcc/ada/libgnat/s-imageu.adb
index 6932487..0e1c2bb 100644
--- a/gcc/ada/libgnat/s-imageu.adb
+++ b/gcc/ada/libgnat/s-imageu.adb
@@ -147,11 +147,12 @@ package body System.Image_U is
           and then S'Last < Integer'Last
           and then P in 2 .. S'Last
           and then S (1) = ' '
-          and then Only_Decimal_Ghost (S, From => 2, To => P)
-          and then Scan_Based_Number_Ghost (S, From => 2, To => P)
-            = Wrap_Option (V),
-        Post => Is_Unsigned_Ghost (S (1 .. P))
-          and then Value_Unsigned (S (1 .. P)) = V;
+          and then Uns_Params.Only_Decimal_Ghost (S, From => 2, To => P)
+          and then Uns_Params.Scan_Based_Number_Ghost (S, From => 2, To => P)
+            = Uns_Params.Wrap_Option (V),
+        Post => not System.Val_Util.Only_Space_Ghost (S, 1, P)
+          and then Uns_Params.Is_Unsigned_Ghost (S (1 .. P))
+          and then Uns_Params.Is_Value_Unsigned_Ghost (S (1 .. P), V);
       --  Ghost lemma to prove the value of Value_Unsigned from the value of
       --  Scan_Based_Number_Ghost on a decimal string.
 
@@ -163,11 +164,15 @@ package body System.Image_U is
          Str : constant String := S (1 .. P);
       begin
          pragma Assert (Str'First = 1);
-         pragma Assert (Only_Decimal_Ghost (Str, From => 2, To => P));
-         Prove_Iter_Scan_Based_Number_Ghost (S, Str, From => 2, To => P);
-         pragma Assert (Scan_Based_Number_Ghost (Str, From => 2, To => P)
-            = Wrap_Option (V));
-         Prove_Scan_Only_Decimal_Ghost (Str, V);
+         pragma Assert (S (2) /= ' ');
+         pragma Assert
+           (Uns_Params.Only_Decimal_Ghost (Str, From => 2, To => P));
+         Uns_Params.Prove_Scan_Based_Number_Ghost_Eq
+           (S, Str, From => 2, To => P);
+         pragma Assert
+           (Uns_Params.Scan_Based_Number_Ghost (Str, From => 2, To => P)
+            = Uns_Params.Wrap_Option (V));
+         Uns_Params.Prove_Scan_Only_Decimal_Ghost (Str, V);
       end Prove_Value_Unsigned;
 
    --  Start of processing for Image_Unsigned
@@ -196,7 +201,6 @@ package body System.Image_U is
 
       Pow        : Big_Positive := 1 with Ghost;
       S_Init     : constant String := S with Ghost;
-      Prev, Cur  : Uns_Option with Ghost;
       Prev_Value : Uns with Ghost;
       Prev_S     : String := S with Ghost;
 
@@ -205,8 +209,8 @@ package body System.Image_U is
       procedure Prove_Character_Val (R : Uns)
       with
         Ghost,
-        Pre  => R in 0 .. 9,
-        Post => Character'Val (48 + R) in '0' .. '9';
+        Post => R rem 10 in 0 .. 9
+          and then Character'Val (48 + R rem 10) in '0' .. '9';
       --  Ghost lemma to prove the value of a character corresponding to the
       --  next figure.
 
@@ -215,7 +219,7 @@ package body System.Image_U is
         Ghost,
         Pre  => Quot = Val / 10
           and then Rest = Val rem 10,
-        Post => Val = 10 * Quot + Rest;
+        Post => Uns'Last - Rest >= 10 * Quot and then Val = 10 * Quot + Rest;
       --  Ghost lemma to prove the relation between the quotient/remainder of
       --  division by 10 and the initial value.
 
@@ -223,42 +227,46 @@ package body System.Image_U is
       with
         Ghost,
         Pre  => R in 0 .. 9,
-        Post => Hexa_To_Unsigned_Ghost (Character'Val (48 + R)) = R;
+        Post => Uns_Params.Hexa_To_Unsigned_Ghost (Character'Val (48 + R)) = R;
       --  Ghost lemma to prove that Hexa_To_Unsigned_Ghost returns the source
       --  figure when applied to the corresponding character.
 
-      procedure Prove_Unchanged
-      with
-        Ghost,
-        Pre  => P <= S'Last
-          and then S_Init'First = S'First
-          and then S_Init'Last = S'Last
-          and then (for all K in S'First .. P => S (K) = S_Init (K)),
-        Post => S (S'First .. P) = S_Init (S'First .. P);
-      --  Ghost lemma to prove that the part of string S before P has not been
-      --  modified.
-
-      procedure Prove_Iter_Scan
-        (Str1, Str2 : String;
-         From, To : Integer;
-         Base     : Uns := 10;
-         Acc      : Uns := 0)
-      with
-        Ghost,
-        Pre  => Str1'Last /= Positive'Last
-          and then
-            (From > To or else (From >= Str1'First and then To <= Str1'Last))
-          and then Only_Decimal_Ghost (Str1, From, To)
-          and then Str1'First = Str2'First
-          and then Str1'Last = Str2'Last
-          and then (for all J in From .. To => Str1 (J) = Str2 (J)),
-        Post =>
-          Scan_Based_Number_Ghost (Str1, From, To, Base, Acc)
-            = Scan_Based_Number_Ghost (Str2, From, To, Base, Acc);
-      --  Ghost lemma to prove that the result of Scan_Based_Number_Ghost only
-      --  depends on the value of the argument string in the (From .. To) range
-      --  of indexes. This is a wrapper on Prove_Iter_Scan_Based_Number_Ghost
-      --  so that we can call it here on ghost arguments.
+      procedure Prove_Scan_Iter
+        (S, Prev_S      : String;
+         V, Prev_V, Res : Uns;
+         P, Max         : Natural)
+        with
+          Ghost,
+          Pre =>
+            S'First = Prev_S'First and then S'Last = Prev_S'Last
+            and then S'Last < Natural'Last and then
+            Max in S'Range and then P in S'First .. Max and then
+            (for all I in P + 1 .. Max => Prev_S (I) in '0' .. '9')
+            and then (for all I in P + 1 .. Max => Prev_S (I) = S (I))
+            and then S (P) in '0' .. '9'
+            and then V <= Uns'Last / 10
+            and then Uns'Last - Uns_Params.Hexa_To_Unsigned_Ghost (S (P))
+              >= 10 * V
+            and then Prev_V =
+              V * 10 + Uns_Params.Hexa_To_Unsigned_Ghost (S (P))
+            and then
+              (if P = Max then Prev_V = Res
+               else Uns_Params.Scan_Based_Number_Ghost
+                 (Str  => Prev_S,
+                  From => P + 1,
+                  To   => Max,
+                  Base => 10,
+                  Acc  => Prev_V) = Uns_Params.Wrap_Option (Res)),
+          Post =>
+            (for all I in P .. Max => S (I) in '0' .. '9')
+            and then Uns_Params.Scan_Based_Number_Ghost
+              (Str  => S,
+               From => P,
+               To   => Max,
+               Base => 10,
+               Acc  => V) = Uns_Params.Wrap_Option (Res);
+      --  Ghost lemma to prove that Scan_Based_Number_Ghost is preserved
+      --  through an iteration of the loop.
 
       -----------------------------
       -- Local lemma null bodies --
@@ -267,21 +275,36 @@ package body System.Image_U is
       procedure Prove_Character_Val (R : Uns) is null;
       procedure Prove_Euclidian (Val, Quot, Rest : Uns) is null;
       procedure Prove_Hexa_To_Unsigned_Ghost (R : Uns) is null;
-      procedure Prove_Unchanged is null;
 
       ---------------------
-      -- Prove_Iter_Scan --
+      -- Prove_Scan_Iter --
       ---------------------
 
-      procedure Prove_Iter_Scan
-        (Str1, Str2 : String;
-         From, To : Integer;
-         Base     : Uns := 10;
-         Acc      : Uns := 0)
+      procedure Prove_Scan_Iter
+        (S, Prev_S      : String;
+         V, Prev_V, Res : Uns;
+         P, Max         : Natural)
       is
+         pragma Unreferenced (Res);
       begin
-         Prove_Iter_Scan_Based_Number_Ghost (Str1, Str2, From, To, Base, Acc);
-      end Prove_Iter_Scan;
+         Uns_Params.Lemma_Scan_Based_Number_Ghost_Step
+           (Str  => S,
+            From => P,
+            To   => Max,
+            Base => 10,
+            Acc  => V);
+         if P < Max then
+            Uns_Params.Prove_Scan_Based_Number_Ghost_Eq
+              (Prev_S, S, P + 1, Max, 10, Prev_V);
+         else
+            Uns_Params.Lemma_Scan_Based_Number_Ghost_Base
+              (Str  => S,
+               From => P + 1,
+               To   => Max,
+               Base => 10,
+               Acc  => Prev_V);
+         end if;
+      end Prove_Scan_Iter;
 
    --  Start of processing for Set_Image_Unsigned
 
@@ -313,6 +336,7 @@ package body System.Image_U is
          Lemma_Non_Zero (Value);
          pragma Assert (Pow <= Big (Uns'Last));
       end loop;
+      pragma Assert (Big (V) / (Big_10 ** Nb_Digits) = 0);
 
       Value := V;
       Pow := 1;
@@ -323,77 +347,43 @@ package body System.Image_U is
       for J in reverse 1 .. Nb_Digits loop
          Lemma_Div_Commutation (Value, 10);
          Lemma_Div_Twice (Big (V), Big_10 ** (Nb_Digits - J), Big_10);
-         Prove_Character_Val (Value rem 10);
+         Prove_Character_Val (Value);
          Prove_Hexa_To_Unsigned_Ghost (Value rem 10);
 
          Prev_Value := Value;
          Prev_S := S;
          Pow := Pow * 10;
-
          S (P + J) := Character'Val (48 + (Value rem 10));
          Value := Value / 10;
 
-         pragma Assert (S (P + J) in '0' .. '9');
-         pragma Assert (Hexa_To_Unsigned_Ghost (S (P + J)) =
-           From_Big (Big (V) / Big_10 ** (Nb_Digits - J)) rem 10);
-         pragma Assert
-           (for all K in P + J + 1 .. P + Nb_Digits => S (K) in '0' .. '9');
-         pragma Assert
-           (for all K in P + J + 1 .. P + Nb_Digits =>
-              Hexa_To_Unsigned_Ghost (S (K)) =
-                From_Big (Big (V) / Big_10 ** (Nb_Digits - (K - P))) rem 10);
-
-         Prev := Scan_Based_Number_Ghost
-           (Str  => S,
-            From => P + J + 1,
-            To   => P + Nb_Digits,
-            Base => 10,
-            Acc  => Prev_Value);
-         Cur := Scan_Based_Number_Ghost
-           (Str  => S,
-            From => P + J,
-            To   => P + Nb_Digits,
-            Base => 10,
-            Acc  => Value);
-
-         if J /= Nb_Digits then
-            Prove_Euclidian (Val  => Prev_Value,
-                             Quot => Value,
-                             Rest => Hexa_To_Unsigned_Ghost (S (P + J)));
-            pragma Assert
-              (Prev_Value = 10 * Value + Hexa_To_Unsigned_Ghost (S (P + J)));
-            Prove_Iter_Scan
-              (Prev_S, S, P + J + 1, P + Nb_Digits, 10, Prev_Value);
-         end if;
+         Prove_Euclidian
+           (Val  => Prev_Value,
+            Quot => Value,
+            Rest => Uns_Params.Hexa_To_Unsigned_Ghost (S (P + J)));
 
-         pragma Assert (Prev = Cur);
-         pragma Assert (Prev = Wrap_Option (V));
+         Prove_Scan_Iter
+           (S, Prev_S, Value, Prev_Value, V, P + J, P + Nb_Digits);
 
          pragma Loop_Invariant (Value <= Uns'Last / 10);
          pragma Loop_Invariant
            (for all K in S'First .. P => S (K) = S_Init (K));
-         pragma Loop_Invariant (Only_Decimal_Ghost (S, P + J, P + Nb_Digits));
-         pragma Loop_Invariant
-           (for all K in P + J .. P + Nb_Digits => S (K) in '0' .. '9');
          pragma Loop_Invariant
-           (for all K in P + J .. P + Nb_Digits =>
-              Hexa_To_Unsigned_Ghost (S (K)) =
-                From_Big (Big (V) / Big_10 ** (Nb_Digits - (K - P))) rem 10);
+           (Uns_Params.Only_Decimal_Ghost
+              (S, From => P + J, To => P + Nb_Digits));
          pragma Loop_Invariant (Pow = Big_10 ** (Nb_Digits - J + 1));
          pragma Loop_Invariant (Big (Value) = Big (V) / Pow);
          pragma Loop_Invariant
-           (Scan_Based_Number_Ghost
+           (Uns_Params.Scan_Based_Number_Ghost
               (Str  => S,
                From => P + J,
                To   => P + Nb_Digits,
                Base => 10,
                Acc  => Value)
-              = Wrap_Option (V));
+              = Uns_Params.Wrap_Option (V));
       end loop;
+      pragma Assert (Big (Value) = Big (V) / (Big_10 ** Nb_Digits));
       pragma Assert (Value = 0);
 
-      Prove_Unchanged;
-
       P := P + Nb_Digits;
    end Set_Image_Unsigned;
 
diff --git a/gcc/ada/libgnat/s-imageu.ads b/gcc/ada/libgnat/s-imageu.ads
index 789cf65..3d80ea9 100644
--- a/gcc/ada/libgnat/s-imageu.ads
+++ b/gcc/ada/libgnat/s-imageu.ads
@@ -45,45 +45,22 @@ pragma Assertion_Policy (Pre                => Ignore,
                          Ghost              => Ignore,
                          Subprogram_Variant => Ignore);
 
+with System.Val_Util;
+
 generic
 
    type Uns is mod <>;
-   type Uns_Option is private;
 
    --  Additional parameters for ghost subprograms used inside contracts
 
    Unsigned_Width_Ghost : Natural;
 
-   with function Wrap_Option (Value : Uns) return Uns_Option
-      with Ghost;
-   with function Only_Decimal_Ghost
-     (Str      : String;
-      From, To : Integer)
-      return Boolean
-      with Ghost;
-   with function Hexa_To_Unsigned_Ghost (X : Character) return Uns
-      with Ghost;
-   with function Scan_Based_Number_Ghost
-     (Str      : String;
-      From, To : Integer;
-      Base     : Uns := 10;
-      Acc      : Uns := 0) return Uns_Option
-      with Ghost;
-   with function Is_Unsigned_Ghost (Str : String) return Boolean
-      with Ghost;
-   with function Value_Unsigned (Str : String) return Uns;
-   with procedure Prove_Iter_Scan_Based_Number_Ghost
-     (Str1, Str2 : String;
-      From, To : Integer;
-      Base     : Uns := 10;
-      Acc      : Uns := 0)
-      with Ghost;
-   with procedure Prove_Scan_Only_Decimal_Ghost
-     (Str : String;
-      Val : Uns)
-      with Ghost;
+   with package Uns_Params is new System.Val_Util.Uns_Params
+     (Uns => Uns, others => <>)
+   with Ghost;
 
 package System.Image_U is
+   use all type Uns_Params.Uns_Option;
 
    procedure Image_Unsigned
      (V : Uns;
@@ -94,7 +71,7 @@ package System.Image_U is
        and then S'Last < Integer'Last
        and then S'Last >= Unsigned_Width_Ghost,
      Post => P in S'Range
-       and then Value_Unsigned (S (1 .. P)) = V;
+       and then Uns_Params.Is_Value_Unsigned_Ghost (S (1 .. P), V);
    pragma Inline (Image_Unsigned);
    --  Computes Uns'Image (V) and stores the result in S (1 .. P) setting
    --  the resulting value of P. The caller guarantees that S is long enough to
@@ -112,9 +89,10 @@ package System.Image_U is
        and then P <= S'Last - Unsigned_Width_Ghost + 1,
      Post => S (S'First .. P'Old) = S'Old (S'First .. P'Old)
        and then P in P'Old + 1 .. S'Last
-       and then Only_Decimal_Ghost (S, From => P'Old + 1, To => P)
-       and then Scan_Based_Number_Ghost (S, From => P'Old + 1, To => P)
-         = Wrap_Option (V);
+       and then Uns_Params.Only_Decimal_Ghost (S, From => P'Old + 1, To => P)
+       and then Uns_Params.Scan_Based_Number_Ghost
+         (S, From => P'Old + 1, To => P)
+         = Uns_Params.Wrap_Option (V);
    --  Stores the image of V in S starting at S (P + 1), P is updated to point
    --  to the last character stored. The value stored is identical to the value
    --  of Uns'Image (V) except that no leading space is stored. The caller
diff --git a/gcc/ada/libgnat/s-imgint.ads b/gcc/ada/libgnat/s-imgint.ads
index fd5bea3..8672e58 100644
--- a/gcc/ada/libgnat/s-imgint.ads
+++ b/gcc/ada/libgnat/s-imgint.ads
@@ -48,8 +48,6 @@ pragma Assertion_Policy (Pre                => Ignore,
 with System.Image_I;
 with System.Unsigned_Types;
 with System.Val_Int;
-with System.Val_Uns;
-with System.Val_Util;
 with System.Wid_Uns;
 
 package System.Img_Int
@@ -57,27 +55,12 @@ package System.Img_Int
 is
    subtype Unsigned is Unsigned_Types.Unsigned;
 
-   package Int_Params is new Val_Util.Int_Params
-     (Int                                => Integer,
-      Uns                                => Unsigned,
-      Uns_Option                         => Val_Uns.Impl.Uns_Option,
-      Unsigned_Width_Ghost               =>
+   package Impl is new Image_I
+     (Int                  => Integer,
+      Uns                  => Unsigned,
+      Unsigned_Width_Ghost =>
          Wid_Uns.Width_Unsigned (0, Unsigned'Last),
-      Only_Decimal_Ghost                 => Val_Uns.Impl.Only_Decimal_Ghost,
-      Hexa_To_Unsigned_Ghost             =>
-         Val_Uns.Impl.Hexa_To_Unsigned_Ghost,
-      Wrap_Option                        => Val_Uns.Impl.Wrap_Option,
-      Scan_Based_Number_Ghost            =>
-         Val_Uns.Impl.Scan_Based_Number_Ghost,
-      Prove_Iter_Scan_Based_Number_Ghost =>
-         Val_Uns.Impl.Prove_Iter_Scan_Based_Number_Ghost,
-      Is_Integer_Ghost                   => Val_Int.Impl.Is_Integer_Ghost,
-      Prove_Scan_Only_Decimal_Ghost      =>
-         Val_Int.Impl.Prove_Scan_Only_Decimal_Ghost,
-      Abs_Uns_Of_Int                     => Val_Int.Impl.Abs_Uns_Of_Int,
-      Value_Integer                      => Val_Int.Impl.Value_Integer);
-
-   package Impl is new Image_I (Int_Params);
+      Int_Params           => System.Val_Int.Impl.Spec.Int_Params);
 
    procedure Image_Integer
      (V : Integer;
diff --git a/gcc/ada/libgnat/s-imglli.ads b/gcc/ada/libgnat/s-imglli.ads
index 20f108c..99c1951 100644
--- a/gcc/ada/libgnat/s-imglli.ads
+++ b/gcc/ada/libgnat/s-imglli.ads
@@ -48,8 +48,6 @@ pragma Assertion_Policy (Pre                => Ignore,
 with System.Image_I;
 with System.Unsigned_Types;
 with System.Val_LLI;
-with System.Val_LLU;
-with System.Val_Util;
 with System.Wid_LLU;
 
 package System.Img_LLI
@@ -57,27 +55,13 @@ package System.Img_LLI
 is
    subtype Long_Long_Unsigned is Unsigned_Types.Long_Long_Unsigned;
 
-   package Int_Params is new Val_Util.Int_Params
-     (Int                                => Long_Long_Integer,
-      Uns                                => Long_Long_Unsigned,
-      Uns_Option                         => Val_LLU.Impl.Uns_Option,
-      Unsigned_Width_Ghost               =>
-         Wid_LLU.Width_Long_Long_Unsigned (0, Long_Long_Unsigned'Last),
-      Only_Decimal_Ghost                 => Val_LLU.Impl.Only_Decimal_Ghost,
-      Hexa_To_Unsigned_Ghost             =>
-         Val_LLU.Impl.Hexa_To_Unsigned_Ghost,
-      Wrap_Option                        => Val_LLU.Impl.Wrap_Option,
-      Scan_Based_Number_Ghost            =>
-         Val_LLU.Impl.Scan_Based_Number_Ghost,
-      Prove_Iter_Scan_Based_Number_Ghost =>
-         Val_LLU.Impl.Prove_Iter_Scan_Based_Number_Ghost,
-      Is_Integer_Ghost                   => Val_LLI.Impl.Is_Integer_Ghost,
-      Prove_Scan_Only_Decimal_Ghost      =>
-         Val_LLI.Impl.Prove_Scan_Only_Decimal_Ghost,
-      Abs_Uns_Of_Int                     => Val_LLI.Impl.Abs_Uns_Of_Int,
-      Value_Integer                      => Val_LLI.Impl.Value_Integer);
-
-   package Impl is new Image_I (Int_Params);
+   package Impl is new Image_I
+     (Int                  => Long_Long_Integer,
+      Uns                  => Long_Long_Unsigned,
+      Unsigned_Width_Ghost =>
+         Wid_LLU.Width_Long_Long_Unsigned
+           (0, Long_Long_Unsigned'Last),
+      Int_Params           => System.Val_LLI.Impl.Spec.Int_Params);
 
    procedure Image_Long_Long_Integer
      (V : Long_Long_Integer;
diff --git a/gcc/ada/libgnat/s-imgllli.ads b/gcc/ada/libgnat/s-imgllli.ads
index 989c296..931c288 100644
--- a/gcc/ada/libgnat/s-imgllli.ads
+++ b/gcc/ada/libgnat/s-imgllli.ads
@@ -48,8 +48,6 @@ pragma Assertion_Policy (Pre                => Ignore,
 with System.Image_I;
 with System.Unsigned_Types;
 with System.Val_LLLI;
-with System.Val_LLLU;
-with System.Val_Util;
 with System.Wid_LLLU;
 
 package System.Img_LLLI
@@ -57,28 +55,13 @@ package System.Img_LLLI
 is
    subtype Long_Long_Long_Unsigned is Unsigned_Types.Long_Long_Long_Unsigned;
 
-   package Int_Params is new Val_Util.Int_Params
-     (Int                                => Long_Long_Long_Integer,
-      Uns                                => Long_Long_Long_Unsigned,
-      Uns_Option                         => Val_LLLU.Impl.Uns_Option,
-      Unsigned_Width_Ghost               =>
+   package Impl is new Image_I
+     (Int                  => Long_Long_Long_Integer,
+      Uns                  => Long_Long_Long_Unsigned,
+      Unsigned_Width_Ghost =>
          Wid_LLLU.Width_Long_Long_Long_Unsigned
            (0, Long_Long_Long_Unsigned'Last),
-      Only_Decimal_Ghost                 => Val_LLLU.Impl.Only_Decimal_Ghost,
-      Hexa_To_Unsigned_Ghost             =>
-         Val_LLLU.Impl.Hexa_To_Unsigned_Ghost,
-      Wrap_Option                        => Val_LLLU.Impl.Wrap_Option,
-      Scan_Based_Number_Ghost            =>
-         Val_LLLU.Impl.Scan_Based_Number_Ghost,
-      Prove_Iter_Scan_Based_Number_Ghost =>
-         Val_LLLU.Impl.Prove_Iter_Scan_Based_Number_Ghost,
-      Is_Integer_Ghost                   => Val_LLLI.Impl.Is_Integer_Ghost,
-      Prove_Scan_Only_Decimal_Ghost      =>
-         Val_LLLI.Impl.Prove_Scan_Only_Decimal_Ghost,
-      Abs_Uns_Of_Int                     => Val_LLLI.Impl.Abs_Uns_Of_Int,
-      Value_Integer                      => Val_LLLI.Impl.Value_Integer);
-
-   package Impl is new Image_I (Int_Params);
+      Int_Params           => System.Val_LLLI.Impl.Spec.Int_Params);
 
    procedure Image_Long_Long_Long_Integer
      (V : Long_Long_Long_Integer;
diff --git a/gcc/ada/libgnat/s-imglllu.ads b/gcc/ada/libgnat/s-imglllu.ads
index 0116aa8..53b39a8 100644
--- a/gcc/ada/libgnat/s-imglllu.ads
+++ b/gcc/ada/libgnat/s-imglllu.ads
@@ -56,23 +56,11 @@ is
    subtype Long_Long_Long_Unsigned is Unsigned_Types.Long_Long_Long_Unsigned;
 
    package Impl is new Image_U
-     (Uns                                => Long_Long_Long_Unsigned,
-      Uns_Option                         => Val_LLLU.Impl.Uns_Option,
-      Unsigned_Width_Ghost               =>
+     (Uns                  => Long_Long_Long_Unsigned,
+      Unsigned_Width_Ghost =>
          Wid_LLLU.Width_Long_Long_Long_Unsigned
         (0, Long_Long_Long_Unsigned'Last),
-      Only_Decimal_Ghost                 => Val_LLLU.Impl.Only_Decimal_Ghost,
-      Hexa_To_Unsigned_Ghost             =>
-         Val_LLLU.Impl.Hexa_To_Unsigned_Ghost,
-      Wrap_Option                        => Val_LLLU.Impl.Wrap_Option,
-      Scan_Based_Number_Ghost            =>
-         Val_LLLU.Impl.Scan_Based_Number_Ghost,
-      Is_Unsigned_Ghost                  => Val_LLLU.Impl.Is_Unsigned_Ghost,
-      Value_Unsigned                     => Val_LLLU.Impl.Value_Unsigned,
-      Prove_Iter_Scan_Based_Number_Ghost =>
-         Val_LLLU.Impl.Prove_Iter_Scan_Based_Number_Ghost,
-      Prove_Scan_Only_Decimal_Ghost      =>
-         Val_LLLU.Impl.Prove_Scan_Only_Decimal_Ghost);
+      Uns_Params           => System.Val_LLLU.Impl.Spec.Uns_Params);
 
    procedure Image_Long_Long_Long_Unsigned
      (V : Long_Long_Long_Unsigned;
diff --git a/gcc/ada/libgnat/s-imgllu.ads b/gcc/ada/libgnat/s-imgllu.ads
index 67372d7..28339cd 100644
--- a/gcc/ada/libgnat/s-imgllu.ads
+++ b/gcc/ada/libgnat/s-imgllu.ads
@@ -56,22 +56,10 @@ is
    subtype Long_Long_Unsigned is Unsigned_Types.Long_Long_Unsigned;
 
    package Impl is new Image_U
-     (Uns                                => Long_Long_Unsigned,
-      Uns_Option                         => Val_LLU.Impl.Uns_Option,
-      Unsigned_Width_Ghost               =>
+     (Uns                  => Long_Long_Unsigned,
+      Unsigned_Width_Ghost =>
          Wid_LLU.Width_Long_Long_Unsigned (0, Long_Long_Unsigned'Last),
-      Only_Decimal_Ghost                 => Val_LLU.Impl.Only_Decimal_Ghost,
-      Hexa_To_Unsigned_Ghost             =>
-         Val_LLU.Impl.Hexa_To_Unsigned_Ghost,
-      Wrap_Option                        => Val_LLU.Impl.Wrap_Option,
-      Scan_Based_Number_Ghost            =>
-         Val_LLU.Impl.Scan_Based_Number_Ghost,
-      Is_Unsigned_Ghost                  => Val_LLU.Impl.Is_Unsigned_Ghost,
-      Value_Unsigned                     => Val_LLU.Impl.Value_Unsigned,
-      Prove_Iter_Scan_Based_Number_Ghost =>
-         Val_LLU.Impl.Prove_Iter_Scan_Based_Number_Ghost,
-      Prove_Scan_Only_Decimal_Ghost      =>
-         Val_LLU.Impl.Prove_Scan_Only_Decimal_Ghost);
+      Uns_Params           => System.Val_LLU.Impl.Spec.Uns_Params);
 
    procedure Image_Long_Long_Unsigned
      (V : Long_Long_Unsigned;
diff --git a/gcc/ada/libgnat/s-imguns.ads b/gcc/ada/libgnat/s-imguns.ads
index fa903ce..120bd5d 100644
--- a/gcc/ada/libgnat/s-imguns.ads
+++ b/gcc/ada/libgnat/s-imguns.ads
@@ -56,22 +56,10 @@ is
    subtype Unsigned is Unsigned_Types.Unsigned;
 
    package Impl is new Image_U
-     (Uns                                => Unsigned,
-      Uns_Option                         => Val_Uns.Impl.Uns_Option,
-      Unsigned_Width_Ghost               =>
+     (Uns                  => Unsigned,
+      Unsigned_Width_Ghost =>
          Wid_Uns.Width_Unsigned (0, Unsigned'Last),
-      Only_Decimal_Ghost                 => Val_Uns.Impl.Only_Decimal_Ghost,
-      Hexa_To_Unsigned_Ghost             =>
-         Val_Uns.Impl.Hexa_To_Unsigned_Ghost,
-      Wrap_Option                        => Val_Uns.Impl.Wrap_Option,
-      Scan_Based_Number_Ghost            =>
-         Val_Uns.Impl.Scan_Based_Number_Ghost,
-      Is_Unsigned_Ghost                  => Val_Uns.Impl.Is_Unsigned_Ghost,
-      Value_Unsigned                     => Val_Uns.Impl.Value_Unsigned,
-      Prove_Iter_Scan_Based_Number_Ghost =>
-         Val_Uns.Impl.Prove_Iter_Scan_Based_Number_Ghost,
-      Prove_Scan_Only_Decimal_Ghost      =>
-         Val_Uns.Impl.Prove_Scan_Only_Decimal_Ghost);
+      Uns_Params           => System.Val_Uns.Impl.Spec.Uns_Params);
 
    procedure Image_Unsigned
      (V : Unsigned;
diff --git a/gcc/ada/libgnat/s-vaispe.adb b/gcc/ada/libgnat/s-vaispe.adb
new file mode 100644
index 0000000..dca2fd7
--- /dev/null
+++ b/gcc/ada/libgnat/s-vaispe.adb
@@ -0,0 +1,87 @@
+------------------------------------------------------------------------------
+--                                                                          --
+--                         GNAT COMPILER COMPONENTS                         --
+--                                                                          --
+--                   S Y S T E M . V A L U E _ I _ S P E C                  --
+--                                                                          --
+--                                 B o d y                                  --
+--                                                                          --
+--          Copyright (C) 2022-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.      --
+--                                                                          --
+------------------------------------------------------------------------------
+
+pragma Assertion_Policy (Pre                => Ignore,
+                         Post               => Ignore,
+                         Contract_Cases     => Ignore,
+                         Ghost              => Ignore,
+                         Subprogram_Variant => Ignore);
+
+package body System.Value_I_Spec is
+
+   -----------------------------------
+   -- Prove_Scan_Only_Decimal_Ghost --
+   -----------------------------------
+
+   procedure Prove_Scan_Only_Decimal_Ghost (Str : String; Val : Int) is
+      Non_Blank : constant Positive := First_Non_Space_Ghost
+        (Str, Str'First, Str'Last);
+      pragma Assert (Str (Str'First + 1) /= ' ');
+      pragma Assert
+        (if Val < 0 then Non_Blank = Str'First
+         else
+           Str (Str'First) = ' '
+            and then Non_Blank = Str'First + 1);
+      Minus     : constant Boolean := Str (Non_Blank) = '-';
+      Fst_Num   : constant Positive :=
+        (if Minus then Non_Blank + 1 else Non_Blank);
+      pragma Assert (Fst_Num = Str'First + 1);
+      Uval      : constant Uns := Abs_Uns_Of_Int (Val);
+
+      procedure Prove_Conversion_Is_Identity (Val : Int; Uval : Uns)
+      with
+        Pre  => Minus = (Val < 0)
+          and then Uval = Abs_Uns_Of_Int (Val),
+        Post => Uns_Is_Valid_Int (Minus, Uval)
+          and then Is_Int_Of_Uns (Minus, Uval, Val);
+      --  Local proof of the unicity of the signed representation
+
+      procedure Prove_Conversion_Is_Identity (Val : Int; Uval : Uns) is null;
+
+   --  Start of processing for Prove_Scan_Only_Decimal_Ghost
+
+   begin
+      Prove_Conversion_Is_Identity (Val, Uval);
+      pragma Assert
+        (Uns_Params.Is_Raw_Unsigned_Format_Ghost (Str (Fst_Num .. Str'Last)));
+      pragma Assert
+        (Uns_Params.Scan_Split_No_Overflow_Ghost (Str, Fst_Num, Str'Last));
+      Uns_Params.Lemma_Exponent_Unsigned_Ghost_Base (Uval, 0, 10);
+      pragma Assert
+        (Uns_Params.Raw_Unsigned_No_Overflow_Ghost (Str, Fst_Num, Str'Last));
+      pragma Assert (Only_Space_Ghost
+        (Str, Uns_Params.Raw_Unsigned_Last_Ghost
+                        (Str, Fst_Num, Str'Last), Str'Last));
+      pragma Assert (Is_Integer_Ghost (Str));
+      pragma Assert (Is_Value_Integer_Ghost (Str, Val));
+   end Prove_Scan_Only_Decimal_Ghost;
+
+end System.Value_I_Spec;
diff --git a/gcc/ada/libgnat/s-vaispe.ads b/gcc/ada/libgnat/s-vaispe.ads
new file mode 100644
index 0000000..5a5e051
--- /dev/null
+++ b/gcc/ada/libgnat/s-vaispe.ads
@@ -0,0 +1,199 @@
+------------------------------------------------------------------------------
+--                                                                          --
+--                         GNAT COMPILER COMPONENTS                         --
+--                                                                          --
+--                   S Y S T E M . V A L U E _ I _ S P E C                  --
+--                                                                          --
+--                                 S p e c                                  --
+--                                                                          --
+--          Copyright (C) 2022-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.      --
+--                                                                          --
+------------------------------------------------------------------------------
+
+--  This package contains the specification entities using for the formal
+--  verification of the routines for scanning signed integer values.
+
+--  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,
+                         Subprogram_Variant => Ignore);
+
+with System.Val_Util; use System.Val_Util;
+
+generic
+
+   type Int is range <>;
+
+   type Uns is mod <>;
+
+   --  Additional parameters for specification subprograms on modular Unsigned
+   --  integers.
+
+   with package Uns_Params is new System.Val_Util.Uns_Params
+     (Uns => Uns, others => <>)
+   with Ghost;
+
+package System.Value_I_Spec with
+   Ghost,
+   SPARK_Mode,
+   Annotate => (GNATprove, Always_Return)
+is
+   pragma Preelaborate;
+   use all type Uns_Params.Uns_Option;
+
+   function Uns_Is_Valid_Int (Minus : Boolean; Uval : Uns) return Boolean is
+     (if Minus then Uval <= Uns (Int'Last) + 1
+      else Uval <= Uns (Int'Last))
+   with Post => True;
+   --  Return True if Uval (or -Uval when Minus is True) is a valid number of
+   --  type Int.
+
+   function Is_Int_Of_Uns
+     (Minus : Boolean;
+      Uval  : Uns;
+      Val   : Int)
+      return Boolean
+   is
+     (if Minus and then Uval = Uns (Int'Last) + 1 then Val = Int'First
+      elsif Minus then Val = -(Int (Uval))
+      else Val = Int (Uval))
+   with
+     Pre  => Uns_Is_Valid_Int (Minus, Uval),
+     Post => True;
+   --  Return True if Uval (or -Uval when Minus is True) is equal to Val
+
+   function Abs_Uns_Of_Int (Val : Int) return Uns is
+     (if Val = Int'First then Uns (Int'Last) + 1
+      elsif Val < 0 then Uns (-Val)
+      else Uns (Val));
+   --  Return the unsigned absolute value of Val
+
+   function Slide_To_1 (Str : String) return String
+   with
+     Post =>
+       Only_Space_Ghost (Str, Str'First, Str'Last) =
+         (for all J in Str'First .. Str'Last =>
+            Slide_To_1'Result (J - Str'First + 1) = ' ');
+   --  Slides Str so that it starts at 1
+
+   function Slide_If_Necessary (Str : String) return String is
+     (if Str'Last = Positive'Last then Slide_To_1 (Str) else Str);
+   --  If Str'Last = Positive'Last then slides Str so that it starts at 1
+
+   function Is_Integer_Ghost (Str : String) return Boolean is
+     (declare
+        Non_Blank : constant Positive := First_Non_Space_Ghost
+          (Str, Str'First, Str'Last);
+        Fst_Num   : constant Positive :=
+          (if Str (Non_Blank) in '+' | '-' then Non_Blank + 1 else Non_Blank);
+      begin
+        Uns_Params.Is_Raw_Unsigned_Format_Ghost (Str (Fst_Num .. Str'Last))
+          and then Uns_Params.Raw_Unsigned_No_Overflow_Ghost
+             (Str, Fst_Num, Str'Last)
+          and then
+            Uns_Is_Valid_Int
+              (Minus => Str (Non_Blank) = '-',
+               Uval  => Uns_Params.Scan_Raw_Unsigned_Ghost
+                 (Str, Fst_Num, Str'Last))
+          and then Only_Space_Ghost
+            (Str, Uns_Params.Raw_Unsigned_Last_Ghost
+             (Str, Fst_Num, Str'Last), Str'Last))
+   with
+     Pre => not Only_Space_Ghost (Str, Str'First, Str'Last)
+       and then Str'Last /= Positive'Last,
+     Post => True;
+   --  Ghost function that determines if Str has the correct format for a
+   --  signed number, consisting in some blank characters, an optional
+   --  sign, a raw unsigned number which does not overflow and then some
+   --  more blank characters.
+
+   function Is_Value_Integer_Ghost (Str : String; Val : Int) return Boolean is
+     (declare
+        Non_Blank : constant Positive := First_Non_Space_Ghost
+          (Str, Str'First, Str'Last);
+        Fst_Num   : constant Positive :=
+          (if Str (Non_Blank) in '+' | '-' then Non_Blank + 1 else Non_Blank);
+        Uval      : constant Uns :=
+          Uns_Params.Scan_Raw_Unsigned_Ghost (Str, Fst_Num, Str'Last);
+      begin
+        Is_Int_Of_Uns (Minus => Str (Non_Blank) = '-',
+                       Uval  => Uval,
+                       Val   => Val))
+   with
+     Pre => not Only_Space_Ghost (Str, Str'First, Str'Last)
+       and then Str'Last /= Positive'Last
+       and then Is_Integer_Ghost (Str),
+     Post => True;
+   --  Ghost function that returns True if Val is the value corresponding to
+   --  the signed number represented by Str.
+
+   procedure Prove_Scan_Only_Decimal_Ghost (Str : String; Val : Int)
+   with
+     Ghost,
+     Pre  => Str'Last /= Positive'Last
+       and then Str'Length >= 2
+       and then Str (Str'First) in ' ' | '-'
+       and then (Str (Str'First) = '-') = (Val < 0)
+       and then Uns_Params.Only_Decimal_Ghost (Str, Str'First + 1, Str'Last)
+       and then Uns_Params.Scan_Based_Number_Ghost
+         (Str, Str'First + 1, Str'Last)
+         = Uns_Params.Wrap_Option (Abs_Uns_Of_Int (Val)),
+     Post => Is_Integer_Ghost (Slide_If_Necessary (Str))
+       and then Is_Value_Integer_Ghost (Str, Val);
+   --  Ghost lemma used in the proof of 'Image implementation, to prove that
+   --  the result of Value_Integer on a decimal string is the same as the
+   --  signing the result of Scan_Based_Number_Ghost.
+
+   --  Bundle Int type with other types, constants and subprograms used in
+   --  ghost code, so that this package can be instantiated once and used
+   --  multiple times as generic formal for a given Int type.
+
+   package Int_Params is new System.Val_Util.Int_Params
+     (Uns                             => Uns,
+      Int                             => Int,
+      P_Uns_Params                    => Uns_Params,
+      P_Is_Integer_Ghost              => Is_Integer_Ghost,
+      P_Is_Value_Integer_Ghost        => Is_Value_Integer_Ghost,
+      P_Is_Int_Of_Uns                 => Is_Int_Of_Uns,
+      P_Abs_Uns_Of_Int                => Abs_Uns_Of_Int,
+      P_Prove_Scan_Only_Decimal_Ghost => Prove_Scan_Only_Decimal_Ghost);
+
+private
+
+   ----------------
+   -- Slide_To_1 --
+   ----------------
+
+   function Slide_To_1 (Str : String) return String is
+     (declare
+        Res : constant String (1 .. Str'Length) := Str;
+      begin
+        Res);
+
+end System.Value_I_Spec;
diff --git a/gcc/ada/libgnat/s-valint.ads b/gcc/ada/libgnat/s-valint.ads
index 9e47f1b..3872d7c 100644
--- a/gcc/ada/libgnat/s-valint.ads
+++ b/gcc/ada/libgnat/s-valint.ads
@@ -54,23 +54,10 @@ package System.Val_Int with SPARK_Mode is
    subtype Unsigned is Unsigned_Types.Unsigned;
 
    package Impl is new Value_I
-     (Int                          => Integer,
-      Uns                          => Unsigned,
-      Scan_Raw_Unsigned            => Val_Uns.Scan_Raw_Unsigned,
-      Uns_Option                   => Val_Uns.Impl.Uns_Option,
-      Wrap_Option                  => Val_Uns.Impl.Wrap_Option,
-      Is_Raw_Unsigned_Format_Ghost =>
-         Val_Uns.Impl.Is_Raw_Unsigned_Format_Ghost,
-      Raw_Unsigned_Overflows_Ghost =>
-         Val_Uns.Impl.Raw_Unsigned_Overflows_Ghost,
-      Scan_Raw_Unsigned_Ghost      =>
-         Val_Uns.Impl.Scan_Raw_Unsigned_Ghost,
-      Raw_Unsigned_Last_Ghost      =>
-         Val_Uns.Impl.Raw_Unsigned_Last_Ghost,
-      Only_Decimal_Ghost           =>
-         Val_Uns.Impl.Only_Decimal_Ghost,
-      Scan_Based_Number_Ghost      =>
-         Val_Uns.Impl.Scan_Based_Number_Ghost);
+     (Int               => Integer,
+      Uns               => Unsigned,
+      Scan_Raw_Unsigned => Val_Uns.Scan_Raw_Unsigned,
+      Uns_Params        => System.Val_Uns.Impl.Spec.Uns_Params);
 
    procedure Scan_Integer
      (Str : String;
diff --git a/gcc/ada/libgnat/s-vallli.ads b/gcc/ada/libgnat/s-vallli.ads
index 5bccb1a..85bf282 100644
--- a/gcc/ada/libgnat/s-vallli.ads
+++ b/gcc/ada/libgnat/s-vallli.ads
@@ -54,24 +54,10 @@ package System.Val_LLI with SPARK_Mode is
    subtype Long_Long_Unsigned is Unsigned_Types.Long_Long_Unsigned;
 
    package Impl is new Value_I
-     (Int                          => Long_Long_Integer,
-      Uns                          => Long_Long_Unsigned,
-      Scan_Raw_Unsigned            =>
-         Val_LLU.Scan_Raw_Long_Long_Unsigned,
-      Uns_Option                   => Val_LLU.Impl.Uns_Option,
-      Wrap_Option                  => Val_LLU.Impl.Wrap_Option,
-      Is_Raw_Unsigned_Format_Ghost =>
-         Val_LLU.Impl.Is_Raw_Unsigned_Format_Ghost,
-      Raw_Unsigned_Overflows_Ghost =>
-         Val_LLU.Impl.Raw_Unsigned_Overflows_Ghost,
-      Scan_Raw_Unsigned_Ghost      =>
-         Val_LLU.Impl.Scan_Raw_Unsigned_Ghost,
-      Raw_Unsigned_Last_Ghost      =>
-         Val_LLU.Impl.Raw_Unsigned_Last_Ghost,
-      Only_Decimal_Ghost           =>
-         Val_LLU.Impl.Only_Decimal_Ghost,
-      Scan_Based_Number_Ghost      =>
-         Val_LLU.Impl.Scan_Based_Number_Ghost);
+     (Int               => Long_Long_Integer,
+      Uns               => Long_Long_Unsigned,
+      Scan_Raw_Unsigned => Val_LLU.Scan_Raw_Long_Long_Unsigned,
+      Uns_Params        => System.Val_LLU.Impl.Spec.Uns_Params);
 
    procedure Scan_Long_Long_Integer
      (Str  : String;
diff --git a/gcc/ada/libgnat/s-valllli.ads b/gcc/ada/libgnat/s-valllli.ads
index 586c737..e53fb0b 100644
--- a/gcc/ada/libgnat/s-valllli.ads
+++ b/gcc/ada/libgnat/s-valllli.ads
@@ -54,24 +54,10 @@ package System.Val_LLLI with SPARK_Mode is
    subtype Long_Long_Long_Unsigned is Unsigned_Types.Long_Long_Long_Unsigned;
 
    package Impl is new Value_I
-     (Int                          => Long_Long_Long_Integer,
-      Uns                          => Long_Long_Long_Unsigned,
-      Scan_Raw_Unsigned            =>
-         Val_LLLU.Scan_Raw_Long_Long_Long_Unsigned,
-      Uns_Option                   => Val_LLLU.Impl.Uns_Option,
-      Wrap_Option                  => Val_LLLU.Impl.Wrap_Option,
-      Is_Raw_Unsigned_Format_Ghost =>
-         Val_LLLU.Impl.Is_Raw_Unsigned_Format_Ghost,
-      Raw_Unsigned_Overflows_Ghost =>
-         Val_LLLU.Impl.Raw_Unsigned_Overflows_Ghost,
-      Scan_Raw_Unsigned_Ghost      =>
-         Val_LLLU.Impl.Scan_Raw_Unsigned_Ghost,
-      Raw_Unsigned_Last_Ghost      =>
-         Val_LLLU.Impl.Raw_Unsigned_Last_Ghost,
-      Only_Decimal_Ghost           =>
-         Val_LLLU.Impl.Only_Decimal_Ghost,
-      Scan_Based_Number_Ghost      =>
-         Val_LLLU.Impl.Scan_Based_Number_Ghost);
+     (Int               => Long_Long_Long_Integer,
+      Uns               => Long_Long_Long_Unsigned,
+      Scan_Raw_Unsigned => Val_LLLU.Scan_Raw_Long_Long_Long_Unsigned,
+      Uns_Params        => System.Val_LLLU.Impl.Spec.Uns_Params);
 
    procedure Scan_Long_Long_Long_Integer
      (Str  : String;
diff --git a/gcc/ada/libgnat/s-valuei.adb b/gcc/ada/libgnat/s-valuei.adb
index b453ffc..51764b2 100644
--- a/gcc/ada/libgnat/s-valuei.adb
+++ b/gcc/ada/libgnat/s-valuei.adb
@@ -41,59 +41,6 @@ package body System.Value_I is
                             Assert_And_Cut     => Ignore,
                             Subprogram_Variant => Ignore);
 
-   -----------------------------------
-   -- Prove_Scan_Only_Decimal_Ghost --
-   -----------------------------------
-
-   procedure Prove_Scan_Only_Decimal_Ghost (Str : String; Val : Int) is
-      Non_Blank : constant Positive := First_Non_Space_Ghost
-        (Str, Str'First, Str'Last);
-      pragma Assert
-        (if Val < 0 then Non_Blank = Str'First
-         else
-            Only_Space_Ghost (Str, Str'First, Str'First)
-            and then Non_Blank = Str'First + 1);
-      Minus : constant Boolean := Str (Non_Blank) = '-';
-      Fst_Num   : constant Positive :=
-        (if Minus then Non_Blank + 1 else Non_Blank);
-      pragma Assert (Fst_Num = Str'First + 1);
-      Uval      : constant Uns :=
-        Scan_Raw_Unsigned_Ghost (Str, Fst_Num, Str'Last);
-
-      procedure Unique_Int_Of_Uns (Val1, Val2 : Int)
-      with
-        Pre  => Uns_Is_Valid_Int (Minus, Uval)
-          and then Is_Int_Of_Uns (Minus, Uval, Val1)
-          and then Is_Int_Of_Uns (Minus, Uval, Val2),
-        Post => Val1 = Val2;
-      --  Local proof of the unicity of the signed representation
-
-      procedure Unique_Int_Of_Uns (Val1, Val2 : Int) is null;
-
-   --  Start of processing for Prove_Scan_Only_Decimal_Ghost
-
-   begin
-      pragma Assert (Minus = (Val < 0));
-      pragma Assert (Uval = Abs_Uns_Of_Int (Val));
-      pragma Assert (if Minus then Uval <= Uns (Int'Last) + 1
-                     else Uval <= Uns (Int'Last));
-      pragma Assert (Uns_Is_Valid_Int (Minus, Uval));
-      pragma Assert
-        (if Minus and then Uval = Uns (Int'Last) + 1 then Val = Int'First
-         elsif Minus then Val = -(Int (Uval))
-         else Val = Int (Uval));
-      pragma Assert (Is_Int_Of_Uns (Minus, Uval, Val));
-      pragma Assert
-        (Is_Raw_Unsigned_Format_Ghost (Str (Fst_Num .. Str'Last)));
-      pragma Assert
-        (not Raw_Unsigned_Overflows_Ghost (Str, Fst_Num, Str'Last));
-      pragma Assert (Only_Space_Ghost
-        (Str, Raw_Unsigned_Last_Ghost (Str, Fst_Num, Str'Last), Str'Last));
-      pragma Assert (Is_Integer_Ghost (Str));
-      pragma Assert (Is_Value_Integer_Ghost (Str, Val));
-      Unique_Int_Of_Uns (Val, Value_Integer (Str));
-   end Prove_Scan_Only_Decimal_Ghost;
-
    ------------------
    -- Scan_Integer --
    ------------------
@@ -104,6 +51,25 @@ package body System.Value_I is
       Max : Integer;
       Res : out Int)
    is
+      procedure Prove_Is_Int_Of_Uns
+        (Minus : Boolean;
+         Uval  : Uns;
+         Val   : Int)
+      with Ghost,
+        Pre => Spec.Uns_Is_Valid_Int (Minus, Uval)
+          and then
+            (if Minus and then Uval = Uns (Int'Last) + 1 then Val = Int'First
+             elsif Minus then Val = -(Int (Uval))
+             else Val = Int (Uval)),
+        Post => Spec.Is_Int_Of_Uns (Minus, Uval, Val);
+      --  Unfold the definition of Is_Int_Of_Uns
+
+      procedure Prove_Is_Int_Of_Uns
+        (Minus : Boolean;
+         Uval  : Uns;
+         Val   : Int)
+      is null;
+
       Uval : Uns;
       --  Unsigned result
 
@@ -131,7 +97,8 @@ package body System.Value_I is
       end if;
 
       Scan_Raw_Unsigned (Str, Ptr, Max, Uval);
-      pragma Assert (Uval = Scan_Raw_Unsigned_Ghost (Str, Fst_Num, Max));
+      pragma Assert
+        (Uval = Uns_Params.Scan_Raw_Unsigned_Ghost (Str, Fst_Num, Max));
 
       --  Deal with overflow cases, and also with largest negative number
 
@@ -152,6 +119,11 @@ package body System.Value_I is
       else
          Res := Int (Uval);
       end if;
+
+      Prove_Is_Int_Of_Uns
+        (Minus => Str (Non_Blank) = '-',
+         Uval  => Uval,
+         Val   => Res);
    end Scan_Integer;
 
    -------------------
@@ -167,7 +139,15 @@ package body System.Value_I is
       if Str'Last = Positive'Last then
          declare
             subtype NT is String (1 .. Str'Length);
+            procedure Prove_Is_Integer_Ghost with
+              Ghost,
+              Pre  => Str'Length < Natural'Last
+              and then not Only_Space_Ghost (Str, Str'First, Str'Last)
+              and then Spec.Is_Integer_Ghost (Spec.Slide_To_1 (Str)),
+              Post => Spec.Is_Integer_Ghost (NT (Str));
+            procedure Prove_Is_Integer_Ghost is null;
          begin
+            Prove_Is_Integer_Ghost;
             return Value_Integer (NT (Str));
          end;
 
@@ -187,8 +167,6 @@ package body System.Value_I is
                else Non_Blank)
             with Ghost;
          begin
-            pragma Assert
-              (Is_Raw_Unsigned_Format_Ghost (Str (Fst_Num .. Str'Last)));
 
             declare
                P_Acc : constant not null access Integer := P'Access;
@@ -197,12 +175,13 @@ package body System.Value_I is
             end;
 
             pragma Assert
-              (P = Raw_Unsigned_Last_Ghost (Str, Fst_Num, Str'Last));
+              (P = Uns_Params.Raw_Unsigned_Last_Ghost
+                 (Str, Fst_Num, Str'Last));
 
             Scan_Trailing_Blanks (Str, P);
 
             pragma Assert
-              (Is_Value_Integer_Ghost (Slide_If_Necessary (Str), V));
+              (Spec.Is_Value_Integer_Ghost (Spec.Slide_If_Necessary (Str), V));
             return V;
          end;
       end if;
diff --git a/gcc/ada/libgnat/s-valuei.ads b/gcc/ada/libgnat/s-valuei.ads
index 5e42773..3f78db6 100644
--- a/gcc/ada/libgnat/s-valuei.ads
+++ b/gcc/ada/libgnat/s-valuei.ads
@@ -39,6 +39,7 @@ pragma Assertion_Policy (Pre                => Ignore,
                          Subprogram_Variant => Ignore);
 
 with System.Val_Util; use System.Val_Util;
+with System.Value_I_Spec;
 
 generic
 
@@ -54,71 +55,15 @@ generic
 
    --  Additional parameters for ghost subprograms used inside contracts
 
-   type Uns_Option is private;
-   with function Wrap_Option (Value : Uns) return Uns_Option
-      with Ghost;
-   with function Is_Raw_Unsigned_Format_Ghost (Str : String) return Boolean
-      with Ghost;
-   with function Raw_Unsigned_Overflows_Ghost
-     (Str      : String;
-      From, To : Integer)
-      return Boolean
-      with Ghost;
-   with function Scan_Raw_Unsigned_Ghost
-     (Str      : String;
-      From, To : Integer)
-      return Uns
-      with Ghost;
-   with function Raw_Unsigned_Last_Ghost
-     (Str      : String;
-      From, To : Integer)
-      return Positive
-      with Ghost;
-   with function Only_Decimal_Ghost
-     (Str      : String;
-      From, To : Integer)
-      return Boolean
-      with Ghost;
-   with function Scan_Based_Number_Ghost
-     (Str      : String;
-      From, To : Integer;
-      Base     : Uns := 10;
-      Acc      : Uns := 0)
-      return Uns_Option
-      with Ghost;
+   with package Uns_Params is new System.Val_Util.Uns_Params
+     (Uns => Uns, others => <>)
+   with Ghost;
 
 package System.Value_I is
    pragma Preelaborate;
+   use all type Uns_Params.Uns_Option;
 
-   function Uns_Is_Valid_Int (Minus : Boolean; Uval : Uns) return Boolean is
-     (if Minus then Uval <= Uns (Int'Last) + 1
-      else Uval <= Uns (Int'Last))
-   with Ghost,
-     Post => True;
-   --  Return True if Uval (or -Uval when Minus is True) is a valid number of
-   --  type Int.
-
-   function Is_Int_Of_Uns
-     (Minus : Boolean;
-      Uval  : Uns;
-      Val   : Int)
-      return Boolean
-   is
-     (if Minus and then Uval = Uns (Int'Last) + 1 then Val = Int'First
-      elsif Minus then Val = -(Int (Uval))
-      else Val = Int (Uval))
-   with
-     Ghost,
-     Pre  => Uns_Is_Valid_Int (Minus, Uval),
-     Post => True;
-   --  Return True if Uval (or -Uval when Minus is True) is equal to Val
-
-   function Abs_Uns_Of_Int (Val : Int) return Uns is
-     (if Val = Int'First then Uns (Int'Last) + 1
-      elsif Val < 0 then Uns (-Val)
-      else Uns (Val))
-   with Ghost;
-   --  Return the unsigned absolute value of Val
+   package Spec is new System.Value_I_Spec (Int, Uns, Uns_Params);
 
    procedure Scan_Integer
      (Str : String;
@@ -139,11 +84,13 @@ package System.Value_I is
               (if Str (Non_Blank) in '+' | '-' then Non_Blank + 1
                else Non_Blank);
           begin
-            Is_Raw_Unsigned_Format_Ghost (Str (Fst_Num .. Max))
-              and then not Raw_Unsigned_Overflows_Ghost (Str, Fst_Num, Max)
-              and then Uns_Is_Valid_Int
+            Uns_Params.Is_Raw_Unsigned_Format_Ghost (Str (Fst_Num .. Max))
+              and then Uns_Params.Raw_Unsigned_No_Overflow_Ghost
+                (Str, Fst_Num, Max)
+              and then Spec.Uns_Is_Valid_Int
                 (Minus => Str (Non_Blank) = '-',
-                 Uval  => Scan_Raw_Unsigned_Ghost (Str, Fst_Num, Max))),
+                 Uval  => Uns_Params.Scan_Raw_Unsigned_Ghost
+                   (Str, Fst_Num, Max))),
     Post =>
       (declare
          Non_Blank : constant Positive := First_Non_Space_Ghost
@@ -152,12 +99,13 @@ package System.Value_I is
            (if Str (Non_Blank) in '+' | '-' then Non_Blank + 1
             else Non_Blank);
          Uval      : constant Uns :=
-            Scan_Raw_Unsigned_Ghost (Str, Fst_Num, Max);
+            Uns_Params.Scan_Raw_Unsigned_Ghost (Str, Fst_Num, Max);
        begin
-         Is_Int_Of_Uns (Minus => Str (Non_Blank) = '-',
-                        Uval  => Uval,
-                        Val   => Res)
-           and then Ptr.all = Raw_Unsigned_Last_Ghost (Str, Fst_Num, Max));
+           Spec.Is_Int_Of_Uns (Minus => Str (Non_Blank) = '-',
+                               Uval  => Uval,
+                               Val   => Res)
+           and then Ptr.all = Uns_Params.Raw_Unsigned_Last_Ghost
+             (Str, Fst_Num, Max));
    --  This procedure scans the string starting at Str (Ptr.all) for a valid
    --  integer according to the syntax described in (RM 3.5(43)). The substring
    --  scanned extends no further than Str (Max). There are three cases for the
@@ -183,111 +131,17 @@ package System.Value_I is
    --  special case of an all-blank string, and Ptr is unchanged, and hence
    --  is greater than Max as required in this case.
 
-   function Slide_To_1 (Str : String) return String
-   with
-     Ghost,
-     Post =>
-       Only_Space_Ghost (Str, Str'First, Str'Last) =
-         (for all J in Str'First .. Str'Last =>
-            Slide_To_1'Result (J - Str'First + 1) = ' ');
-   --  Slides Str so that it starts at 1
-
-   function Slide_If_Necessary (Str : String) return String is
-     (if Str'Last = Positive'Last then Slide_To_1 (Str) else Str)
-   with
-     Ghost,
-     Post =>
-       Only_Space_Ghost (Str, Str'First, Str'Last) =
-       Only_Space_Ghost (Slide_If_Necessary'Result,
-                         Slide_If_Necessary'Result'First,
-                         Slide_If_Necessary'Result'Last);
-   --  If Str'Last = Positive'Last then slides Str so that it starts at 1
-
-   function Is_Integer_Ghost (Str : String) return Boolean is
-     (declare
-        Non_Blank : constant Positive := First_Non_Space_Ghost
-          (Str, Str'First, Str'Last);
-        Fst_Num   : constant Positive :=
-          (if Str (Non_Blank) in '+' | '-' then Non_Blank + 1 else Non_Blank);
-      begin
-        Is_Raw_Unsigned_Format_Ghost (Str (Fst_Num .. Str'Last))
-          and then not Raw_Unsigned_Overflows_Ghost (Str, Fst_Num, Str'Last)
-          and then
-            Uns_Is_Valid_Int
-              (Minus => Str (Non_Blank) = '-',
-               Uval  => Scan_Raw_Unsigned_Ghost (Str, Fst_Num, Str'Last))
-          and then Only_Space_Ghost
-            (Str, Raw_Unsigned_Last_Ghost (Str, Fst_Num, Str'Last), Str'Last))
-   with
-     Ghost,
-     Pre => not Only_Space_Ghost (Str, Str'First, Str'Last)
-       and then Str'Last /= Positive'Last,
-     Post => True;
-   --  Ghost function that determines if Str has the correct format for a
-   --  signed number, consisting in some blank characters, an optional
-   --  sign, a raw unsigned number which does not overflow and then some
-   --  more blank characters.
-
-   function Is_Value_Integer_Ghost (Str : String; Val : Int) return Boolean is
-     (declare
-        Non_Blank : constant Positive := First_Non_Space_Ghost
-          (Str, Str'First, Str'Last);
-        Fst_Num   : constant Positive :=
-          (if Str (Non_Blank) in '+' | '-' then Non_Blank + 1 else Non_Blank);
-        Uval      : constant Uns :=
-          Scan_Raw_Unsigned_Ghost (Str, Fst_Num, Str'Last);
-      begin
-        Is_Int_Of_Uns (Minus => Str (Non_Blank) = '-',
-                       Uval  => Uval,
-                       Val   => Val))
-   with
-     Ghost,
-     Pre => not Only_Space_Ghost (Str, Str'First, Str'Last)
-       and then Str'Last /= Positive'Last
-       and then Is_Integer_Ghost (Str),
-     Post => True;
-   --  Ghost function that returns True if Val is the value corresponding to
-   --  the signed number represented by Str.
-
    function Value_Integer (Str : String) return Int
    with
      Pre => not Only_Space_Ghost (Str, Str'First, Str'Last)
        and then Str'Length /= Positive'Last
-       and then Is_Integer_Ghost (Slide_If_Necessary (Str)),
-     Post => Is_Value_Integer_Ghost
-       (Slide_If_Necessary (Str), Value_Integer'Result),
+       and then Spec.Is_Integer_Ghost (Spec.Slide_If_Necessary (Str)),
+     Post => Spec.Is_Value_Integer_Ghost
+       (Spec.Slide_If_Necessary (Str), Value_Integer'Result),
      Subprogram_Variant => (Decreases => Str'First);
    --  Used in computing X'Value (Str) where X is a signed integer type whose
    --  base range does not exceed the base range of Integer. Str is the string
    --  argument of the attribute. Constraint_Error is raised if the string is
    --  malformed, or if the value is out of range.
 
-   procedure Prove_Scan_Only_Decimal_Ghost (Str : String; Val : Int)
-   with
-     Ghost,
-     Pre  => Str'Last /= Positive'Last
-       and then Str'Length >= 2
-       and then Str (Str'First) in ' ' | '-'
-       and then (Str (Str'First) = '-') = (Val < 0)
-       and then Only_Decimal_Ghost (Str, Str'First + 1, Str'Last)
-       and then Scan_Based_Number_Ghost (Str, Str'First + 1, Str'Last)
-         = Wrap_Option (Abs_Uns_Of_Int (Val)),
-     Post => Is_Integer_Ghost (Slide_If_Necessary (Str))
-       and then Value_Integer (Str) = Val;
-   --  Ghost lemma used in the proof of 'Image implementation, to prove that
-   --  the result of Value_Integer on a decimal string is the same as the
-   --  signing the result of Scan_Based_Number_Ghost.
-
-private
-
-   ----------------
-   -- Slide_To_1 --
-   ----------------
-
-   function Slide_To_1 (Str : String) return String is
-     (declare
-        Res : constant String (1 .. Str'Length) := Str;
-      begin
-        Res);
-
 end System.Value_I;
diff --git a/gcc/ada/libgnat/s-valueu.adb b/gcc/ada/libgnat/s-valueu.adb
index f5a6881..8f19086 100644
--- a/gcc/ada/libgnat/s-valueu.adb
+++ b/gcc/ada/libgnat/s-valueu.adb
@@ -41,9 +41,12 @@ package body System.Value_U is
                             Assert_And_Cut     => Ignore,
                             Subprogram_Variant => Ignore);
 
+   use type Spec.Uns_Option;
+   use type Spec.Split_Value_Ghost;
+
    --  Local lemmas
 
-   procedure Lemma_Digit_Is_Before_Last
+   procedure Lemma_Digit_Not_Last
      (Str  : String;
       P    : Integer;
       From : Integer;
@@ -54,257 +57,47 @@ package body System.Value_U is
        and then To in From .. Str'Last
        and then Str (From) in '0' .. '9' | 'a' .. 'f' | 'A' .. 'F'
        and then P in From .. To
-       and then Str (P) in '0' .. '9' | 'a' .. 'f' | 'A' .. 'F',
-     Post => P /= Last_Hexa_Ghost (Str (From .. To)) + 1;
-   --  If the character at position P is a digit, P cannot be the position of
-   --  of the first non-digit in Str.
+       and then P <= Spec.Last_Hexa_Ghost (Str (From .. To)) + 1
+       and then Spec.Is_Based_Format_Ghost (Str (From .. To)),
+     Post =>
+       (if Str (P) in '0' .. '9' | 'a' .. 'f' | 'A' .. 'F'
+        then P <= Spec.Last_Hexa_Ghost (Str (From .. To)));
 
-   procedure Lemma_End_Of_Scan
+   procedure Lemma_Underscore_Not_Last
      (Str  : String;
+      P    : Integer;
       From : Integer;
-      To   : Integer;
-      Base : Uns;
-      Acc  : Uns)
-   with Ghost,
-     Pre  => Str'Last /= Positive'Last and then From > To,
-     Post => Scan_Based_Number_Ghost (Str, From, To, Base, Acc) =
-       (False, Acc);
-   --  Unfold the definition of Scan_Based_Number_Ghost on an empty string
-
-   procedure Lemma_Scan_Digit
-     (Str          : String;
-      P            : Integer;
-      Lst          : Integer;
-      Digit        : Uns;
-      Base         : Uns;
-      Old_Acc      : Uns;
-      Acc          : Uns;
-      Scan_Val     : Uns_Option;
-      Old_Overflow : Boolean;
-      Overflow     : Boolean)
-   with Ghost,
-     Pre  => Str'Last /= Positive'Last
-       and then Lst in Str'Range
-       and then P in Str'First .. Lst
-       and then Str (P) in '0' .. '9' | 'a' .. 'f' | 'A' .. 'F'
-       and then Digit = Hexa_To_Unsigned_Ghost (Str (P))
-       and then Only_Hexa_Ghost (Str, P, Lst)
-       and then Base in 2 .. 16
-       and then (if Digit < Base and then Old_Acc <= Uns'Last / Base
-                 then Acc = Base * Old_Acc + Digit)
-       and then (if Digit >= Base
-                   or else Old_Acc > Uns'Last / Base
-                   or else (Old_Acc > (Uns'Last - Base + 1) / Base
-                            and then Acc < Uns'Last / Base)
-                 then Overflow
-                 else Overflow = Old_Overflow)
-       and then
-         (if not Old_Overflow then
-           Scan_Val = Scan_Based_Number_Ghost
-              (Str, P, Lst, Base, Old_Acc)),
-     Post =>
-        (if not Overflow then
-           Scan_Val = Scan_Based_Number_Ghost
-             (Str, P + 1, Lst, Base, Acc))
-       and then
-        (if Overflow then Old_Overflow or else Scan_Val.Overflow);
-   --  Unfold the definition of Scan_Based_Number_Ghost when the string starts
-   --  with a digit.
-
-   procedure Lemma_Scan_Underscore
-     (Str      : String;
-      P        : Integer;
-      From     : Integer;
-      To       : Integer;
-      Lst      : Integer;
-      Base     : Uns;
-      Acc      : Uns;
-      Scan_Val : Uns_Option;
-      Overflow : Boolean;
-      Ext      : Boolean)
+      To   : Integer)
    with Ghost,
      Pre  => Str'Last /= Positive'Last
        and then From in Str'Range
        and then To in From .. Str'Last
-       and then Lst <= To
-       and then P in From .. Lst + 1
-       and then P <= To
-       and then
-         (if Ext then
-            Is_Based_Format_Ghost (Str (From .. To))
-            and then Lst = Last_Hexa_Ghost (Str (From .. To))
-          else Is_Natural_Format_Ghost (Str (From .. To))
-            and then Lst = Last_Number_Ghost (Str (From .. To)))
+       and then Str (From) in '0' .. '9' | 'a' .. 'f' | 'A' .. 'F'
+       and then P in From .. To
        and then Str (P) = '_'
-       and then
-         (if not Overflow then
-           Scan_Val = Scan_Based_Number_Ghost (Str, P, Lst, Base, Acc)),
-     Post => P + 1 <= Lst
-       and then
-         (if Ext then Str (P + 1) in '0' .. '9' | 'a' .. 'f' | 'A' .. 'F'
-          else Str (P + 1) in '0' .. '9')
-       and then
-         (if not Overflow then
-           Scan_Val = Scan_Based_Number_Ghost (Str, P + 1, Lst, Base, Acc));
-   --  Unfold the definition of Scan_Based_Number_Ghost when the string starts
-   --  with an underscore.
+       and then P <= Spec.Last_Hexa_Ghost (Str (From .. To)) + 1
+       and then Spec.Is_Based_Format_Ghost (Str (From .. To)),
+     Post => P + 1 <= Spec.Last_Hexa_Ghost (Str (From .. To))
+       and then Str (P + 1) in '0' .. '9' | 'a' .. 'f' | 'A' .. 'F';
 
    -----------------------------
    -- Local lemma null bodies --
    -----------------------------
 
-   procedure Lemma_Digit_Is_Before_Last
+   procedure Lemma_Digit_Not_Last
      (Str  : String;
       P    : Integer;
       From : Integer;
       To   : Integer)
    is null;
 
-   procedure Lemma_End_Of_Scan
-     (Str          : String;
-      From         : Integer;
-      To           : Integer;
-      Base         : Uns;
-      Acc          : Uns)
-   is null;
-
-   procedure Lemma_Scan_Underscore
-     (Str      : String;
-      P        : Integer;
-      From     : Integer;
-      To       : Integer;
-      Lst      : Integer;
-      Base     : Uns;
-      Acc      : Uns;
-      Scan_Val : Uns_Option;
-      Overflow : Boolean;
-      Ext      : Boolean)
+   procedure Lemma_Underscore_Not_Last
+     (Str  : String;
+      P    : Integer;
+      From : Integer;
+      To   : Integer)
    is null;
 
-   ---------------------
-   -- Last_Hexa_Ghost --
-   ---------------------
-
-   function Last_Hexa_Ghost (Str : String) return Positive is
-   begin
-      for J in Str'Range loop
-         if Str (J) not in '0' .. '9' | 'a' .. 'f' | 'A' .. 'F' | '_' then
-            return J - 1;
-         end if;
-
-         pragma Loop_Invariant
-           (for all K in Str'First .. J =>
-              Str (K) in '0' .. '9' | 'a' .. 'f' | 'A' .. 'F' | '_');
-      end loop;
-
-      return Str'Last;
-   end Last_Hexa_Ghost;
-
-   ----------------------
-   -- Lemma_Scan_Digit --
-   ----------------------
-
-   procedure Lemma_Scan_Digit
-     (Str          : String;
-      P            : Integer;
-      Lst          : Integer;
-      Digit        : Uns;
-      Base         : Uns;
-      Old_Acc      : Uns;
-      Acc          : Uns;
-      Scan_Val     : Uns_Option;
-      Old_Overflow : Boolean;
-      Overflow     : Boolean)
-   is
-      pragma Unreferenced (Str, P, Lst, Scan_Val, Overflow, Old_Overflow);
-   begin
-      if Digit >= Base then
-         null;
-
-      elsif Old_Acc <= (Uns'Last - Base + 1) / Base then
-         pragma Assert (not Scan_Overflows_Ghost (Digit, Base, Old_Acc));
-
-      elsif Old_Acc > Uns'Last / Base then
-         null;
-
-      else
-         pragma Assert
-           ((Acc < Uns'Last / Base) =
-              Scan_Overflows_Ghost (Digit, Base, Old_Acc));
-      end if;
-   end Lemma_Scan_Digit;
-
-   ----------------------------------------
-   -- Prove_Iter_Scan_Based_Number_Ghost --
-   ----------------------------------------
-
-   procedure Prove_Iter_Scan_Based_Number_Ghost
-     (Str1, Str2 : String;
-      From, To : Integer;
-      Base     : Uns := 10;
-      Acc      : Uns := 0)
-   is
-   begin
-      if From > To then
-         null;
-      elsif Str1 (From) = '_' then
-         Prove_Iter_Scan_Based_Number_Ghost
-           (Str1, Str2, From + 1, To, Base, Acc);
-      elsif Scan_Overflows_Ghost
-        (Hexa_To_Unsigned_Ghost (Str1 (From)), Base, Acc)
-      then
-         null;
-      else
-         Prove_Iter_Scan_Based_Number_Ghost
-           (Str1, Str2, From + 1, To, Base,
-            Base * Acc + Hexa_To_Unsigned_Ghost (Str1 (From)));
-      end if;
-   end Prove_Iter_Scan_Based_Number_Ghost;
-
-   -----------------------------------
-   -- Prove_Scan_Only_Decimal_Ghost --
-   -----------------------------------
-
-   procedure Prove_Scan_Only_Decimal_Ghost
-     (Str : String;
-      Val : Uns)
-   is
-      Non_Blank : constant Positive := First_Non_Space_Ghost
-        (Str, Str'First, Str'Last);
-      pragma Assert (Non_Blank = Str'First + 1);
-      Fst_Num   : constant Positive :=
-        (if Str (Non_Blank) = '+' then Non_Blank + 1 else Non_Blank);
-      pragma Assert (Fst_Num = Str'First + 1);
-      Last_Num_Init   : constant Integer :=
-        Last_Number_Ghost (Str (Str'First + 1 .. Str'Last));
-      pragma Assert (Last_Num_Init = Str'Last);
-      Starts_As_Based : constant Boolean :=
-        Last_Num_Init < Str'Last - 1
-        and then Str (Last_Num_Init + 1) in '#' | ':'
-        and then Str (Last_Num_Init + 2) in
-          '0' .. '9' | 'a' .. 'f' | 'A' .. 'F';
-      pragma Assert (Starts_As_Based = False);
-      Last_Num_Based  : constant Integer :=
-        (if Starts_As_Based
-         then Last_Hexa_Ghost (Str (Last_Num_Init + 2 .. Str'Last))
-         else Last_Num_Init);
-      pragma Assert (Last_Num_Based = Str'Last);
-   begin
-      pragma Assert
-        (Is_Opt_Exponent_Format_Ghost (Str (Str'Last + 1 .. Str'Last)));
-      pragma Assert
-        (Is_Natural_Format_Ghost (Str (Str'First + 1 .. Str'Last)));
-      pragma Assert
-        (Is_Raw_Unsigned_Format_Ghost (Str (Str'First + 1 .. Str'Last)));
-      pragma Assert
-        (not Raw_Unsigned_Overflows_Ghost (Str, Str'First + 1, Str'Last));
-      pragma Assert (Val = Exponent_Unsigned_Ghost (Val, 0, 10).Value);
-      pragma Assert
-        (Val = Scan_Raw_Unsigned_Ghost (Str, Str'First + 1, Str'Last));
-      pragma Assert (Is_Unsigned_Ghost (Str));
-      pragma Assert (Is_Value_Unsigned_Ghost (Str, Val));
-   end Prove_Scan_Only_Decimal_Ghost;
-
    -----------------------
    -- Scan_Raw_Unsigned --
    -----------------------
@@ -341,8 +134,8 @@ package body System.Value_U is
       Last_Num_Init : constant Integer :=
         Last_Number_Ghost (Str (Ptr.all .. Max))
       with Ghost;
-      Init_Val      : constant Uns_Option :=
-        Scan_Based_Number_Ghost (Str, Ptr.all, Last_Num_Init)
+      Init_Val      : constant Spec.Uns_Option :=
+        Spec.Scan_Based_Number_Ghost (Str, Ptr.all, Last_Num_Init)
       with Ghost;
       Starts_As_Based : constant Boolean :=
         Last_Num_Init < Max - 1
@@ -352,7 +145,7 @@ package body System.Value_U is
       with Ghost;
       Last_Num_Based  : constant Integer :=
         (if Starts_As_Based
-         then Last_Hexa_Ghost (Str (Last_Num_Init + 2 .. Max))
+         then Spec.Last_Hexa_Ghost (Str (Last_Num_Init + 2 .. Max))
          else Last_Num_Init)
       with Ghost;
       Is_Based        : constant Boolean :=
@@ -360,9 +153,9 @@ package body System.Value_U is
         and then Last_Num_Based < Max
         and then Str (Last_Num_Based + 1) = Str (Last_Num_Init + 1)
       with Ghost;
-      Based_Val       : constant Uns_Option :=
+      Based_Val       : constant Spec.Uns_Option :=
         (if Starts_As_Based and then not Init_Val.Overflow
-         then Scan_Based_Number_Ghost
+         then Spec.Scan_Based_Number_Ghost
            (Str, Last_Num_Init + 2, Last_Num_Based, Init_Val.Value)
          else Init_Val)
       with Ghost;
@@ -379,6 +172,7 @@ package body System.Value_U is
       end if;
 
       P := Ptr.all;
+      Spec.Lemma_Scan_Based_Number_Ghost_Step (Str, P, Last_Num_Init);
       Uval := Character'Pos (Str (P)) - Character'Pos ('0');
       P := P + 1;
 
@@ -392,9 +186,6 @@ package body System.Value_U is
          Umax10 : constant Uns := Uns'Last / 10;
          --  Numbers bigger than Umax10 overflow if multiplied by 10
 
-         Old_Uval     : Uns with Ghost;
-         Old_Overflow : Boolean with Ghost;
-
       begin
          --  Loop through decimal digits
          loop
@@ -403,7 +194,7 @@ package body System.Value_U is
               (if Overflow then Init_Val.Overflow);
             pragma Loop_Invariant
               (if not Overflow
-               then Init_Val = Scan_Based_Number_Ghost
+               then Init_Val = Spec.Scan_Based_Number_Ghost
                  (Str, P, Last_Num_Init, Acc => Uval));
 
             exit when P > Max;
@@ -414,9 +205,8 @@ package body System.Value_U is
 
             if Digit > 9 then
                if Str (P) = '_' then
-                  Lemma_Scan_Underscore
-                    (Str, P, Ptr_Old, Max, Last_Num_Init, 10, Uval,
-                     Init_Val, Overflow, False);
+                  Spec.Lemma_Scan_Based_Number_Ghost_Underscore
+                    (Str, P, Last_Num_Init, Acc => Uval);
                   Scan_Underscore (Str, P, Ptr, Max, False);
                else
                   exit;
@@ -425,11 +215,19 @@ package body System.Value_U is
             --  Accumulate result, checking for overflow
 
             else
-               Old_Uval := Uval;
-               Old_Overflow := Overflow;
+               Spec.Lemma_Scan_Based_Number_Ghost_Step
+                 (Str, P, Last_Num_Init, Acc => Uval);
+               Spec.Lemma_Scan_Based_Number_Ghost_Overflow
+                 (Str, P, Last_Num_Init, Acc => Uval);
 
                if Uval <= Umax then
+                  pragma Assert
+                    (Spec.Hexa_To_Unsigned_Ghost (Str (P)) = Digit);
                   Uval := 10 * Uval + Digit;
+                  pragma Assert
+                    (if not Overflow
+                     then Init_Val = Spec.Scan_Based_Number_Ghost
+                       (Str, P + 1, Last_Num_Init, Acc => Uval));
 
                elsif Uval > Umax10 then
                   Overflow := True;
@@ -440,17 +238,17 @@ package body System.Value_U is
                   if Uval < Umax10 then
                      Overflow := True;
                   end if;
+                  pragma Assert
+                    (if not Overflow
+                     then Init_Val = Spec.Scan_Based_Number_Ghost
+                       (Str, P + 1, Last_Num_Init, Acc => Uval));
                end if;
 
-               Lemma_Scan_Digit
-                 (Str, P, Last_Num_Init, Digit, 10, Old_Uval, Uval, Init_Val,
-                  Old_Overflow, Overflow);
-
                P := P + 1;
             end if;
          end loop;
-         pragma Assert (P = Last_Num_Init + 1);
-         pragma Assert (Init_Val.Overflow = Overflow);
+         Spec.Lemma_Scan_Based_Number_Ghost_Base
+            (Str, P, Last_Num_Init, Acc => Uval);
       end;
 
       pragma Assert_And_Cut
@@ -488,18 +286,14 @@ package body System.Value_U is
             UmaxB : constant Uns := Uns'Last / Base;
             --  Numbers bigger than UmaxB overflow if multiplied by base
 
-            Old_Uval     : Uns with Ghost;
-            Old_Overflow : Boolean with Ghost;
-
          begin
             pragma Assert
               (if Str (P) in '0' .. '9' | 'A' .. 'F' | 'a' .. 'f'
-               then Is_Based_Format_Ghost (Str (P .. Max)));
+               then Spec.Is_Based_Format_Ghost (Str (P .. Max)));
 
             --  Loop to scan out based integer value
 
             loop
-
                --  We require a digit at this stage
 
                if Str (P) in '0' .. '9' then
@@ -519,6 +313,8 @@ package body System.Value_U is
                --  already stored in Ptr.all.
 
                else
+                  Spec.Lemma_Scan_Based_Number_Ghost_Base
+                    (Str, P, Last_Num_Based, Base, Uval);
                   Uval := Base;
                   Base := 10;
                   pragma Assert (Ptr.all = Last_Num_Init + 1);
@@ -529,25 +325,25 @@ package body System.Value_U is
                   exit;
                end if;
 
-               Lemma_Digit_Is_Before_Last (Str, P, Last_Num_Init + 2, Max);
-
                pragma Loop_Invariant (P in P'Loop_Entry .. Last_Num_Based);
                pragma Loop_Invariant
                  (Str (P) in '0' .. '9' | 'a' .. 'f' | 'A' .. 'F'
-                  and then Digit = Hexa_To_Unsigned_Ghost (Str (P)));
+                  and then Digit = Spec.Hexa_To_Unsigned_Ghost (Str (P)));
                pragma Loop_Invariant
                  (if Overflow'Loop_Entry then Overflow);
                pragma Loop_Invariant
                  (if Overflow then
-                    Overflow'Loop_Entry or else Based_Val.Overflow);
+                    (Overflow'Loop_Entry or else Based_Val.Overflow));
                pragma Loop_Invariant
                  (if not Overflow
-                  then Based_Val = Scan_Based_Number_Ghost
+                  then Based_Val = Spec.Scan_Based_Number_Ghost
                     (Str, P, Last_Num_Based, Base, Uval));
                pragma Loop_Invariant (Ptr.all = Last_Num_Init + 1);
 
-               Old_Uval := Uval;
-               Old_Overflow := Overflow;
+               Spec.Lemma_Scan_Based_Number_Ghost_Step
+                 (Str, P, Last_Num_Based, Base, Uval);
+               Spec.Lemma_Scan_Based_Number_Ghost_Overflow
+                 (Str, P, Last_Num_Based, Base, Uval);
 
                --  If digit is too large, just signal overflow and continue.
                --  The idea here is to keep scanning as long as the input is
@@ -560,6 +356,10 @@ package body System.Value_U is
 
                elsif Uval <= Umax then
                   Uval := Base * Uval + Digit;
+                  pragma Assert
+                    (if not Overflow
+                     then Based_Val = Spec.Scan_Based_Number_Ghost
+                       (Str, P + 1, Last_Num_Based, Base, Uval));
 
                elsif Uval > UmaxB then
                   Overflow := True;
@@ -570,6 +370,10 @@ package body System.Value_U is
                   if Uval < UmaxB then
                      Overflow := True;
                   end if;
+                  pragma Assert
+                    (if not Overflow
+                     then Based_Val = Spec.Scan_Based_Number_Ghost
+                       (Str, P + 1, Last_Num_Based, Base, Uval));
                end if;
 
                --  If at end of string with no base char, not a based number
@@ -579,10 +383,6 @@ package body System.Value_U is
 
                P := P + 1;
 
-               Lemma_Scan_Digit
-                 (Str, P - 1, Last_Num_Based, Digit, Base, Old_Uval, Uval,
-                  Based_Val, Old_Overflow, Overflow);
-
                if P > Max then
                   Ptr.all := P;
                   Bad_Value (Str);
@@ -592,48 +392,54 @@ package body System.Value_U is
 
                if Str (P) = Base_Char then
                   Ptr.all := P + 1;
+                  pragma Assert (P = Last_Num_Based + 1);
                   pragma Assert (Ptr.all = Last_Num_Based + 2);
+                  pragma Assert (Starts_As_Based);
+                  pragma Assert (Last_Num_Based < Max);
+                  pragma Assert (Str (Last_Num_Based + 1) = Base_Char);
+                  pragma Assert (Base_Char = Str (Last_Num_Init + 1));
                   pragma Assert (Is_Based);
-                  pragma Assert
-                    (if not Overflow then
-                       Based_Val = Scan_Based_Number_Ghost
-                         (Str, P, Last_Num_Based, Base, Uval));
-                  Lemma_End_Of_Scan (Str, P, Last_Num_Based, Base, Uval);
-                  pragma Assert (if not Overflow then Uval = Based_Val.Value);
+                  Spec.Lemma_Scan_Based_Number_Ghost_Base
+                    (Str, P, Last_Num_Based, Base, Uval);
                   exit;
 
                --  Deal with underscore
 
                elsif Str (P) = '_' then
-                  Lemma_Scan_Underscore
-                    (Str, P, Last_Num_Init + 2, Max, Last_Num_Based, Base,
-                     Uval, Based_Val, Overflow, True);
+                  Lemma_Underscore_Not_Last (Str, P, Last_Num_Init + 2, Max);
+                  Spec.Lemma_Scan_Based_Number_Ghost_Underscore
+                    (Str, P, Last_Num_Based, Base, Uval);
                   Scan_Underscore (Str, P, Ptr, Max, True);
                   pragma Assert
                     (if not Overflow
-                     then Based_Val = Scan_Based_Number_Ghost
+                     then Based_Val = Spec.Scan_Based_Number_Ghost
                        (Str, P, Last_Num_Based, Base, Uval));
+                  pragma Assert (Str (P) /= '_');
+                  pragma Assert (Str (P) /= Base_Char);
                end if;
+
+               Lemma_Digit_Not_Last (Str, P, Last_Num_Init + 2, Max);
+               pragma Assert (Str (P) /= '_');
+               pragma Assert (Str (P) /= Base_Char);
             end loop;
          end;
          pragma Assert
            (if Starts_As_Based then P = Last_Num_Based + 1
             else P = Last_Num_Init + 2);
          pragma Assert
+           (Last_Num_Init < Max - 1
+            and then Str (Last_Num_Init + 1) in '#' | ':');
+         pragma Assert
            (Overflow =
               (Init_Val.Overflow
                or else Init_Val.Value not in 2 .. 16
                or else (Starts_As_Based and then Based_Val.Overflow)));
+         pragma Assert
+           (Overflow /= Spec.Scan_Split_No_Overflow_Ghost (Str, Ptr_Old, Max));
       end if;
 
       pragma Assert_And_Cut
-        (Overflow =
-           (Init_Val.Overflow
-            or else
-              (Last_Num_Init < Max - 1
-               and then Str (Last_Num_Init + 1) in '#' | ':'
-               and then Init_Val.Value not in 2 .. 16)
-            or else (Starts_As_Based and then Based_Val.Overflow))
+        (Overflow /= Spec.Scan_Split_No_Overflow_Ghost (Str, Ptr_Old, Max)
          and then
            (if not Overflow then
                 (if Is_Based then Uval = Based_Val.Value
@@ -649,10 +455,12 @@ package body System.Value_U is
 
       Scan_Exponent (Str, Ptr, Max, Expon);
 
-      pragma Assert (Ptr.all = Raw_Unsigned_Last_Ghost (Str, Ptr_Old, Max));
       pragma Assert
-        (if Starts_As_Exponent_Format_Ghost (Str (First_Exp .. Max))
-         then Expon = Scan_Exponent_Ghost (Str (First_Exp .. Max)));
+        (Ptr.all = Spec.Raw_Unsigned_Last_Ghost (Str, Ptr_Old, Max));
+      pragma Assert
+        (if not Overflow
+         then Spec.Scan_Split_Value_Ghost (Str, Ptr_Old, Max) =
+           (Uval, Base, Expon));
 
       if Expon /= 0 and then Uval /= 0 then
 
@@ -664,8 +472,8 @@ package body System.Value_U is
             UmaxB : constant Uns := Uns'Last / Base;
             --  Numbers bigger than UmaxB overflow if multiplied by base
 
-            Res_Val : constant Uns_Option :=
-              Exponent_Unsigned_Ghost (Uval, Expon, Base)
+            Res_Val : constant Spec.Uns_Option :=
+              Spec.Exponent_Unsigned_Ghost (Uval, Expon, Base)
             with Ghost;
          begin
             for J in 1 .. Expon loop
@@ -674,48 +482,45 @@ package body System.Value_U is
                pragma Loop_Invariant
                  (if Overflow
                   then Overflow'Loop_Entry or else Res_Val.Overflow);
+               pragma Loop_Invariant (Uval /= 0);
                pragma Loop_Invariant
                  (if not Overflow
-                  then Res_Val = Exponent_Unsigned_Ghost
+                  then Res_Val = Spec.Exponent_Unsigned_Ghost
                     (Uval, Expon - J + 1, Base));
 
                pragma Assert
-                 ((Uval > UmaxB) = Scan_Overflows_Ghost (0, Base, Uval));
+                 ((Uval > UmaxB) = Spec.Scan_Overflows_Ghost (0, Base, Uval));
 
                if Uval > UmaxB then
+                  Spec.Lemma_Exponent_Unsigned_Ghost_Overflow
+                     (Uval, Expon - J + 1, Base);
                   Overflow := True;
                   exit;
                end if;
 
+               Spec.Lemma_Exponent_Unsigned_Ghost_Step
+                  (Uval, Expon - J + 1, Base);
+
                Uval := Uval * Base;
             end loop;
+            Spec.Lemma_Exponent_Unsigned_Ghost_Base (Uval, 0, Base);
+
             pragma Assert
-              (Overflow = (Init_Val.Overflow
-               or else
-                 (Last_Num_Init < Max - 1
-                  and then Str (Last_Num_Init + 1) in '#' | ':'
-                  and then Init_Val.Value not in 2 .. 16)
-               or else (Starts_As_Based and then Based_Val.Overflow)
-               or else Res_Val.Overflow));
-            pragma Assert
-              (Overflow = Raw_Unsigned_Overflows_Ghost (Str, Ptr_Old, Max));
-            pragma Assert
-              (Exponent_Unsigned_Ghost (Uval, 0, Base) = (False, Uval));
-            pragma Assert
-              (if not Overflow then Uval = Res_Val.Value);
-            pragma Assert
-              (if not Overflow then
-                  Uval = Scan_Raw_Unsigned_Ghost (Str, Ptr_Old, Max));
+              (Overflow /=
+                 Spec.Raw_Unsigned_No_Overflow_Ghost (Str, Ptr_Old, Max));
+            pragma Assert (if not Overflow then Res_Val = (False, Uval));
          end;
       end if;
+      Spec.Lemma_Exponent_Unsigned_Ghost_Base (Uval, Expon, Base);
       pragma Assert
         (if Expon = 0 or else Uval = 0 then
-            Exponent_Unsigned_Ghost (Uval, Expon, Base) = (False, Uval));
+            Spec.Exponent_Unsigned_Ghost (Uval, Expon, Base) = (False, Uval));
       pragma Assert
-        (Overflow = Raw_Unsigned_Overflows_Ghost (Str, Ptr_Old, Max));
+        (Overflow /=
+           Spec.Raw_Unsigned_No_Overflow_Ghost (Str, Ptr_Old, Max));
       pragma Assert
         (if not Overflow then
-            Uval = Scan_Raw_Unsigned_Ghost (Str, Ptr_Old, Max));
+            Uval = Spec.Scan_Raw_Unsigned_Ghost (Str, Ptr_Old, Max));
 
       --  Return result, dealing with overflow
 
@@ -774,7 +579,15 @@ package body System.Value_U is
       if Str'Last = Positive'Last then
          declare
             subtype NT is String (1 .. Str'Length);
+            procedure Prove_Is_Unsigned_Ghost with
+              Ghost,
+              Pre  => Str'Length < Natural'Last
+              and then not Only_Space_Ghost (Str, Str'First, Str'Last)
+              and then Spec.Is_Unsigned_Ghost (Spec.Slide_To_1 (Str)),
+              Post => Spec.Is_Unsigned_Ghost (NT (Str));
+            procedure Prove_Is_Unsigned_Ghost is null;
          begin
+            Prove_Is_Unsigned_Ghost;
             return Value_Unsigned (NT (Str));
          end;
 
@@ -784,7 +597,6 @@ package body System.Value_U is
          declare
             V : Uns;
             P : aliased Integer := Str'First;
-
             Non_Blank : constant Positive := First_Non_Space_Ghost
               (Str, Str'First, Str'Last)
             with Ghost;
@@ -792,9 +604,6 @@ package body System.Value_U is
               (if Str (Non_Blank) = '+' then Non_Blank + 1 else Non_Blank)
             with Ghost;
          begin
-            pragma Assert
-              (Is_Raw_Unsigned_Format_Ghost (Str (Fst_Num .. Str'Last)));
-
             declare
                P_Acc : constant not null access Integer := P'Access;
             begin
@@ -802,14 +611,15 @@ package body System.Value_U is
             end;
 
             pragma Assert
-              (P = Raw_Unsigned_Last_Ghost (Str, Fst_Num, Str'Last));
+              (P = Spec.Raw_Unsigned_Last_Ghost (Str, Fst_Num, Str'Last));
             pragma Assert
-              (V = Scan_Raw_Unsigned_Ghost (Str, Fst_Num, Str'Last));
+              (V = Spec.Scan_Raw_Unsigned_Ghost (Str, Fst_Num, Str'Last));
 
             Scan_Trailing_Blanks (Str, P);
 
             pragma Assert
-              (Is_Value_Unsigned_Ghost (Slide_If_Necessary (Str), V));
+              (Spec.Is_Value_Unsigned_Ghost
+                 (Spec.Slide_If_Necessary (Str), V));
             return V;
          end;
       end if;
diff --git a/gcc/ada/libgnat/s-valueu.ads b/gcc/ada/libgnat/s-valueu.ads
index 1508b6e..466b96a 100644
--- a/gcc/ada/libgnat/s-valueu.ads
+++ b/gcc/ada/libgnat/s-valueu.ads
@@ -44,6 +44,7 @@ pragma Assertion_Policy (Pre                => Ignore,
                          Ghost              => Ignore,
                          Subprogram_Variant => Ignore);
 
+with System.Value_U_Spec;
 with System.Val_Util; use System.Val_Util;
 
 generic
@@ -53,317 +54,7 @@ generic
 package System.Value_U is
    pragma Preelaborate;
 
-   type Uns_Option (Overflow : Boolean := False) is record
-      case Overflow is
-         when True =>
-            null;
-         when False =>
-            Value : Uns := 0;
-      end case;
-   end record;
-
-   function Wrap_Option (Value : Uns) return Uns_Option is
-     (Overflow => False, Value => Value)
-   with
-     Ghost;
-
-   function Only_Decimal_Ghost
-     (Str      : String;
-      From, To : Integer)
-      return Boolean
-   is
-      (for all J in From .. To => Str (J) in '0' .. '9')
-   with
-     Ghost,
-     Pre => From > To or else (From >= Str'First and then To <= Str'Last);
-   --  Ghost function that returns True if S has only decimal characters
-   --  from index From to index To.
-
-   function Only_Hexa_Ghost (Str : String; From, To : Integer) return Boolean
-   is
-      (for all J in From .. To =>
-          Str (J) in '0' .. '9' | 'a' .. 'f' | 'A' .. 'F' | '_')
-   with
-     Ghost,
-     Pre => From > To or else (From >= Str'First and then To <= Str'Last);
-   --  Ghost function that returns True if S has only hexadecimal characters
-   --  from index From to index To.
-
-   function Last_Hexa_Ghost (Str : String) return Positive
-   with
-     Ghost,
-     Pre  => Str /= ""
-       and then Str (Str'First) in '0' .. '9' | 'a' .. 'f' | 'A' .. 'F',
-     Post => Last_Hexa_Ghost'Result in Str'Range
-       and then (if Last_Hexa_Ghost'Result < Str'Last then
-                   Str (Last_Hexa_Ghost'Result + 1) not in
-                     '0' .. '9' | 'a' .. 'f' | 'A' .. 'F' | '_')
-       and then Only_Hexa_Ghost (Str, Str'First, Last_Hexa_Ghost'Result);
-   --  Ghost function that returns the index of the last character in S that
-   --  is either an hexadecimal digit or an underscore, which necessarily
-   --  exists given the precondition on Str.
-
-   function Is_Based_Format_Ghost (Str : String) return Boolean
-   is
-     (Str /= ""
-        and then Str (Str'First) in '0' .. '9' | 'a' .. 'f' | 'A' .. 'F'
-        and then
-        (declare
-           L : constant Positive := Last_Hexa_Ghost (Str);
-         begin
-           Str (L) /= '_'
-             and then (for all J in Str'First .. L =>
-                         (if Str (J) = '_' then Str (J + 1) /= '_'))))
-   with
-     Ghost;
-   --  Ghost function that determines if Str has the correct format for a
-   --  based number, consisting in a sequence of hexadecimal digits possibly
-   --  separated by single underscores. It may be followed by other characters.
-
-   function Hexa_To_Unsigned_Ghost (X : Character) return Uns is
-     (case X is
-         when '0' .. '9' => Character'Pos (X) - Character'Pos ('0'),
-         when 'a' .. 'f' => Character'Pos (X) - Character'Pos ('a') + 10,
-         when 'A' .. 'F' => Character'Pos (X) - Character'Pos ('A') + 10,
-         when others     => raise Program_Error)
-   with
-     Ghost,
-     Pre => X in '0' .. '9' | 'a' .. 'f' | 'A' .. 'F';
-   --  Ghost function that computes the value corresponding to an hexadecimal
-   --  digit.
-
-   function Scan_Overflows_Ghost
-     (Digit : Uns;
-      Base  : Uns;
-      Acc   : Uns) return Boolean
-   is
-     (Digit >= Base
-      or else Acc > Uns'Last / Base
-      or else Uns'Last - Digit < Base * Acc)
-   with Ghost;
-   --  Ghost function which returns True if Digit + Base * Acc overflows or
-   --  Digit is greater than Base, as this is used by the algorithm for the
-   --  test of overflow.
-
-   function Scan_Based_Number_Ghost
-     (Str      : String;
-      From, To : Integer;
-      Base     : Uns := 10;
-      Acc      : Uns := 0) return Uns_Option
-   with
-     Ghost,
-     Subprogram_Variant => (Increases => From),
-     Pre  => Str'Last /= Positive'Last
-         and then
-           (From > To or else (From >= Str'First and then To <= Str'Last))
-         and then Only_Hexa_Ghost (Str, From, To);
-   --  Ghost function that recursively computes the based number in Str,
-   --  assuming Acc has been scanned already and scanning continues at index
-   --  From.
-
-   function Exponent_Unsigned_Ghost
-     (Value : Uns;
-      Exp   : Natural;
-      Base  : Uns := 10) return Uns_Option
-   with
-     Ghost,
-     Subprogram_Variant => (Decreases => Exp);
-   --  Ghost function that recursively computes Value * Base ** Exp
-
-   function Is_Raw_Unsigned_Format_Ghost (Str : String) return Boolean is
-     (Is_Natural_Format_Ghost (Str)
-      and then
-        (declare
-           Last_Num_Init   : constant Integer := Last_Number_Ghost (Str);
-           Starts_As_Based : constant Boolean :=
-             Last_Num_Init < Str'Last - 1
-             and then Str (Last_Num_Init + 1) in '#' | ':'
-             and then Str (Last_Num_Init + 2) in
-               '0' .. '9' | 'a' .. 'f' | 'A' .. 'F';
-           Last_Num_Based  : constant Integer :=
-             (if Starts_As_Based
-              then Last_Hexa_Ghost (Str (Last_Num_Init + 2 .. Str'Last))
-              else Last_Num_Init);
-           Is_Based        : constant Boolean :=
-             Starts_As_Based
-             and then Last_Num_Based < Str'Last
-             and then Str (Last_Num_Based + 1) = Str (Last_Num_Init + 1);
-           First_Exp       : constant Integer :=
-             (if Is_Based then Last_Num_Based + 2 else Last_Num_Init + 1);
-         begin
-           (if Starts_As_Based then
-              Is_Based_Format_Ghost (Str (Last_Num_Init + 2 .. Str'Last))
-              and then Last_Num_Based < Str'Last)
-            and then Is_Opt_Exponent_Format_Ghost
-              (Str (First_Exp .. Str'Last))))
-   with
-     Ghost,
-     Pre  => Str'Last /= Positive'Last,
-     Post => True;
-   --  Ghost function that determines if Str has the correct format for an
-   --  unsigned number without a sign character.
-   --  It is a natural number in base 10, optionally followed by a based
-   --  number surrounded by delimiters # or :, optionally followed by an
-   --  exponent part.
-
-   function Raw_Unsigned_Overflows_Ghost
-     (Str      : String;
-      From, To : Integer)
-      return Boolean
-   is
-     (declare
-        Last_Num_Init   : constant Integer :=
-          Last_Number_Ghost (Str (From .. To));
-        Init_Val        : constant Uns_Option :=
-          Scan_Based_Number_Ghost (Str, From, Last_Num_Init);
-        Starts_As_Based : constant Boolean :=
-          Last_Num_Init < To - 1
-          and then Str (Last_Num_Init + 1) in '#' | ':'
-          and then Str (Last_Num_Init + 2) in
-          '0' .. '9' | 'a' .. 'f' | 'A' .. 'F';
-        Last_Num_Based  : constant Integer :=
-          (if Starts_As_Based
-           then Last_Hexa_Ghost (Str (Last_Num_Init + 2 .. To))
-           else Last_Num_Init);
-        Is_Based        : constant Boolean :=
-          Starts_As_Based
-          and then Last_Num_Based < To
-          and then Str (Last_Num_Based + 1) = Str (Last_Num_Init + 1);
-        Based_Val       : constant Uns_Option :=
-          (if Starts_As_Based and then not Init_Val.Overflow
-           then Scan_Based_Number_Ghost
-             (Str, Last_Num_Init + 2, Last_Num_Based, Init_Val.Value)
-           else Init_Val);
-        First_Exp       : constant Integer :=
-          (if Is_Based then Last_Num_Based + 2 else Last_Num_Init + 1);
-        Expon           : constant Natural :=
-          (if Starts_As_Exponent_Format_Ghost (Str (First_Exp .. To))
-           then Scan_Exponent_Ghost (Str (First_Exp .. To))
-           else 0);
-      begin
-        Init_Val.Overflow
-        or else
-          (Last_Num_Init < To - 1
-           and then Str (Last_Num_Init + 1) in '#' | ':'
-           and then Init_Val.Value not in 2 .. 16)
-        or else
-          (Starts_As_Based
-           and then Based_Val.Overflow)
-        or else
-          (Starts_As_Exponent_Format_Ghost (Str (First_Exp .. To))
-           and then
-             (declare
-                Base  : constant Uns :=
-                  (if Is_Based then Init_Val.Value else 10);
-                Value : constant Uns :=
-                  (if Is_Based then Based_Val.Value else Init_Val.Value);
-              begin
-                Exponent_Unsigned_Ghost
-                  (Value, Expon, Base).Overflow)))
-   with
-     Ghost,
-     Pre  => Str'Last /= Positive'Last
-       and then From in Str'Range
-       and then To in From .. Str'Last
-       and then Str (From) in '0' .. '9',
-     Post => True;
-   --  Ghost function that determines if the computation of the unsigned number
-   --  represented by Str will overflow. The computation overflows if either:
-   --    * The computation of the decimal part overflows,
-   --    * The decimal part is followed by a valid delimiter for a based
-   --      part, and the number corresponding to the base is not a valid base,
-   --    * The computation of the based part overflows, or
-   --    * There is an exponent and the computation of the exponentiation
-   --      overflows.
-
-   function Scan_Raw_Unsigned_Ghost
-     (Str      : String;
-      From, To : Integer)
-      return Uns
-   is
-     (declare
-        Last_Num_Init   : constant Integer :=
-          Last_Number_Ghost (Str (From .. To));
-        Init_Val        : constant Uns_Option :=
-          Scan_Based_Number_Ghost (Str, From, Last_Num_Init);
-        Starts_As_Based : constant Boolean :=
-          Last_Num_Init < To - 1
-          and then Str (Last_Num_Init + 1) in '#' | ':'
-          and then Str (Last_Num_Init + 2) in
-          '0' .. '9' | 'a' .. 'f' | 'A' .. 'F';
-        Last_Num_Based  : constant Integer :=
-          (if Starts_As_Based
-           then Last_Hexa_Ghost (Str (Last_Num_Init + 2 .. To))
-           else Last_Num_Init);
-        Is_Based        : constant Boolean :=
-          Starts_As_Based
-          and then Last_Num_Based < To
-          and then Str (Last_Num_Based + 1) = Str (Last_Num_Init + 1);
-        Based_Val       : constant Uns_Option :=
-          (if Starts_As_Based and then not Init_Val.Overflow
-           then Scan_Based_Number_Ghost
-             (Str, Last_Num_Init + 2, Last_Num_Based, Init_Val.Value)
-           else Init_Val);
-        First_Exp       : constant Integer :=
-          (if Is_Based then Last_Num_Based + 2 else Last_Num_Init + 1);
-        Expon           : constant Natural :=
-          (if Starts_As_Exponent_Format_Ghost (Str (First_Exp .. To))
-           then Scan_Exponent_Ghost (Str (First_Exp .. To))
-           else 0);
-        Base            : constant Uns :=
-          (if Is_Based then Init_Val.Value else 10);
-        Value           : constant Uns :=
-          (if Is_Based then Based_Val.Value else Init_Val.Value);
-      begin
-        Exponent_Unsigned_Ghost (Value, Expon, Base).Value)
-   with
-     Ghost,
-     Pre  => Str'Last /= Positive'Last
-       and then From in Str'Range
-       and then To in From .. Str'Last
-       and then Str (From) in '0' .. '9'
-       and then not Raw_Unsigned_Overflows_Ghost (Str, From, To),
-     Post => True;
-   --  Ghost function that scans an unsigned number without a sign character
-
-   function Raw_Unsigned_Last_Ghost
-     (Str      : String;
-      From, To : Integer)
-      return Positive
-   is
-     (declare
-        Last_Num_Init   : constant Integer :=
-          Last_Number_Ghost (Str (From .. To));
-        Starts_As_Based : constant Boolean :=
-          Last_Num_Init < To - 1
-          and then Str (Last_Num_Init + 1) in '#' | ':'
-          and then Str (Last_Num_Init + 2) in
-          '0' .. '9' | 'a' .. 'f' | 'A' .. 'F';
-        Last_Num_Based  : constant Integer :=
-          (if Starts_As_Based
-           then Last_Hexa_Ghost (Str (Last_Num_Init + 2 .. To))
-           else Last_Num_Init);
-        Is_Based        : constant Boolean :=
-          Starts_As_Based
-          and then Last_Num_Based < To
-          and then Str (Last_Num_Based + 1) = Str (Last_Num_Init + 1);
-        First_Exp       : constant Integer :=
-          (if Is_Based then Last_Num_Based + 2 else Last_Num_Init + 1);
-      begin
-        (if not Starts_As_Exponent_Format_Ghost (Str (First_Exp .. To))
-         then First_Exp
-         elsif Str (First_Exp + 1) in '-' | '+' then
-           Last_Number_Ghost (Str (First_Exp + 2 .. To)) + 1
-         else Last_Number_Ghost (Str (First_Exp + 1 .. To)) + 1))
-   with
-     Ghost,
-     Pre  => Str'Last /= Positive'Last
-       and then From in Str'Range
-       and then To in From .. Str'Last
-       and then Str (From) in '0' .. '9',
-     Post => Raw_Unsigned_Last_Ghost'Result in From .. To + 1;
-   --  Ghost function that returns the position of the cursor once an unsigned
-   --  number has been seen.
+   package Spec is new System.Value_U_Spec (Uns);
 
    procedure Scan_Raw_Unsigned
      (Str : String;
@@ -373,10 +64,10 @@ package System.Value_U is
    with Pre => Str'Last /= Positive'Last
      and then Ptr.all in Str'Range
      and then Max in Ptr.all .. Str'Last
-     and then Is_Raw_Unsigned_Format_Ghost (Str (Ptr.all .. Max)),
-     Post => not Raw_Unsigned_Overflows_Ghost (Str, Ptr.all'Old, Max)
-     and Res = Scan_Raw_Unsigned_Ghost (Str, Ptr.all'Old, Max)
-     and Ptr.all = Raw_Unsigned_Last_Ghost (Str, Ptr.all'Old, Max);
+     and then Spec.Is_Raw_Unsigned_Format_Ghost (Str (Ptr.all .. Max)),
+     Post => Spec.Raw_Unsigned_No_Overflow_Ghost (Str, Ptr.all'Old, Max)
+     and Res = Spec.Scan_Raw_Unsigned_Ghost (Str, Ptr.all'Old, Max)
+     and Ptr.all = Spec.Raw_Unsigned_Last_Ghost (Str, Ptr.all'Old, Max);
 
    --  This function scans the string starting at Str (Ptr.all) for a valid
    --  integer according to the syntax described in (RM 3.5(43)). The substring
@@ -464,7 +155,7 @@ package System.Value_U is
           Fst_Num   : constant Positive :=
             (if Str (Non_Blank) = '+' then Non_Blank + 1 else Non_Blank);
         begin
-          Is_Raw_Unsigned_Format_Ghost (Str (Fst_Num .. Max))),
+          Spec.Is_Raw_Unsigned_Format_Ghost (Str (Fst_Num .. Max))),
      Post =>
        (declare
           Non_Blank : constant Positive :=
@@ -472,9 +163,9 @@ package System.Value_U is
           Fst_Num   : constant Positive :=
             (if Str (Non_Blank) = '+' then Non_Blank + 1 else Non_Blank);
         begin
-          not Raw_Unsigned_Overflows_Ghost (Str, Fst_Num, Max)
-          and then Res = Scan_Raw_Unsigned_Ghost (Str, Fst_Num, Max)
-          and then Ptr.all = Raw_Unsigned_Last_Ghost (Str, Fst_Num, Max));
+          Spec.Raw_Unsigned_No_Overflow_Ghost (Str, Fst_Num, Max)
+          and then Res = Spec.Scan_Raw_Unsigned_Ghost (Str, Fst_Num, Max)
+          and then Ptr.all = Spec.Raw_Unsigned_Last_Ghost (Str, Fst_Num, Max));
 
    --  Same as Scan_Raw_Unsigned, except scans optional leading
    --  blanks, and an optional leading plus sign.
@@ -482,157 +173,18 @@ package System.Value_U is
    --  Note: if a minus sign is present, Constraint_Error will be raised.
    --  Note: trailing blanks are not scanned.
 
-   function Slide_To_1 (Str : String) return String
-   with Ghost,
-       Post =>
-         Only_Space_Ghost (Str, Str'First, Str'Last) =
-         (for all J in Str'First .. Str'Last =>
-            Slide_To_1'Result (J - Str'First + 1) = ' ');
-   --  Slides Str so that it starts at 1
-
-   function Slide_If_Necessary (Str : String) return String is
-     (if Str'Last = Positive'Last then Slide_To_1 (Str) else Str)
-   with Ghost,
-       Post =>
-         Only_Space_Ghost (Str, Str'First, Str'Last) =
-         Only_Space_Ghost (Slide_If_Necessary'Result,
-                           Slide_If_Necessary'Result'First,
-                           Slide_If_Necessary'Result'Last);
-   --  If Str'Last = Positive'Last then slides Str so that it starts at 1
-
-   function Is_Unsigned_Ghost (Str : String) return Boolean is
-     (declare
-        Non_Blank : constant Positive := First_Non_Space_Ghost
-          (Str, Str'First, Str'Last);
-        Fst_Num   : constant Positive :=
-          (if Str (Non_Blank) = '+' then Non_Blank + 1 else Non_Blank);
-      begin
-        Is_Raw_Unsigned_Format_Ghost (Str (Fst_Num .. Str'Last))
-          and then not Raw_Unsigned_Overflows_Ghost (Str, Fst_Num, Str'Last)
-          and then Only_Space_Ghost
-             (Str, Raw_Unsigned_Last_Ghost (Str, Fst_Num, Str'Last), Str'Last))
-   with Ghost,
-       Pre => not Only_Space_Ghost (Str, Str'First, Str'Last)
-       and then Str'Last /= Positive'Last,
-       Post => True;
-   --  Ghost function that determines if Str has the correct format for an
-   --  unsigned number, consisting in some blank characters, an optional
-   --  + sign, a raw unsigned number which does not overflow and then some
-   --  more blank characters.
-
-   function Is_Value_Unsigned_Ghost (Str : String; Val : Uns) return Boolean is
-     (declare
-        Non_Blank : constant Positive := First_Non_Space_Ghost
-          (Str, Str'First, Str'Last);
-        Fst_Num   : constant Positive :=
-          (if Str (Non_Blank) = '+' then Non_Blank + 1 else Non_Blank);
-      begin
-        Val = Scan_Raw_Unsigned_Ghost (Str, Fst_Num, Str'Last))
-   with Ghost,
-       Pre => not Only_Space_Ghost (Str, Str'First, Str'Last)
-       and then Str'Last /= Positive'Last
-       and then Is_Unsigned_Ghost (Str),
-       Post => True;
-   --  Ghost function that returns True if Val is the value corresponding to
-   --  the unsigned number represented by Str.
-
    function Value_Unsigned
      (Str : String) return Uns
-   with Pre => not Only_Space_Ghost (Str, Str'First, Str'Last)
-     and then Str'Length /= Positive'Last
-     and then Is_Unsigned_Ghost (Slide_If_Necessary (Str)),
+   with Pre => Str'Length /= Positive'Last
+     and then not Only_Space_Ghost (Str, Str'First, Str'Last)
+     and then Spec.Is_Unsigned_Ghost (Spec.Slide_If_Necessary (Str)),
      Post =>
-         Is_Value_Unsigned_Ghost
-           (Slide_If_Necessary (Str), Value_Unsigned'Result),
+         Spec.Is_Value_Unsigned_Ghost
+           (Spec.Slide_If_Necessary (Str), Value_Unsigned'Result),
      Subprogram_Variant => (Decreases => Str'First);
    --  Used in computing X'Value (Str) where X is a modular integer type whose
    --  modulus does not exceed the range of System.Unsigned_Types.Unsigned. Str
    --  is the string argument of the attribute. Constraint_Error is raised if
    --  the string is malformed, or if the value is out of range.
 
-   procedure Prove_Iter_Scan_Based_Number_Ghost
-     (Str1, Str2 : String;
-      From, To : Integer;
-      Base     : Uns := 10;
-      Acc      : Uns := 0)
-   with
-     Ghost,
-     Subprogram_Variant => (Increases => From),
-     Pre  => Str1'Last /= Positive'Last
-       and then Str2'Last /= Positive'Last
-       and then
-         (From > To or else (From >= Str1'First and then To <= Str1'Last))
-       and then
-         (From > To or else (From >= Str2'First and then To <= Str2'Last))
-       and then Only_Hexa_Ghost (Str1, From, To)
-       and then (for all J in From .. To => Str1 (J) = Str2 (J)),
-     Post =>
-       Scan_Based_Number_Ghost (Str1, From, To, Base, Acc)
-         = Scan_Based_Number_Ghost (Str2, From, To, Base, Acc);
-   --  Ghost lemma used in the proof of 'Image implementation, to prove the
-   --  preservation of Scan_Based_Number_Ghost across an update in the string
-   --  in lower indexes.
-
-   procedure Prove_Scan_Only_Decimal_Ghost
-     (Str : String;
-      Val : Uns)
-   with
-     Ghost,
-     Pre  => Str'Last /= Positive'Last
-       and then Str'Length >= 2
-       and then Str (Str'First) = ' '
-       and then Only_Decimal_Ghost (Str, Str'First + 1, Str'Last)
-       and then Scan_Based_Number_Ghost (Str, Str'First + 1, Str'Last)
-         = Wrap_Option (Val),
-     Post => Is_Unsigned_Ghost (Slide_If_Necessary (Str))
-       and then Value_Unsigned (Str) = Val;
-   --  Ghost lemma used in the proof of 'Image implementation, to prove that
-   --  the result of Value_Unsigned on a decimal string is the same as the
-   --  result of Scan_Based_Number_Ghost.
-
-private
-
-   -----------------------------
-   -- Exponent_Unsigned_Ghost --
-   -----------------------------
-
-   function Exponent_Unsigned_Ghost
-     (Value : Uns;
-      Exp   : Natural;
-      Base  : Uns := 10) return Uns_Option
-   is
-      (if Exp = 0 or Value = 0 then (Overflow => False, Value => Value)
-       elsif Scan_Overflows_Ghost (0, Base, Value) then (Overflow => True)
-       else Exponent_Unsigned_Ghost (Value * Base, Exp - 1, Base));
-
-   -----------------------------
-   -- Scan_Based_Number_Ghost --
-   -----------------------------
-
-   function Scan_Based_Number_Ghost
-     (Str      : String;
-      From, To : Integer;
-      Base     : Uns := 10;
-      Acc      : Uns := 0) return Uns_Option
-   is
-      (if From > To then (Overflow => False, Value => Acc)
-       elsif Str (From) = '_'
-       then Scan_Based_Number_Ghost (Str, From + 1, To, Base, Acc)
-       elsif Scan_Overflows_Ghost
-         (Hexa_To_Unsigned_Ghost (Str (From)), Base, Acc)
-       then (Overflow => True)
-       else Scan_Based_Number_Ghost
-         (Str, From + 1, To, Base,
-          Base * Acc + Hexa_To_Unsigned_Ghost (Str (From))));
-
-   ----------------
-   -- Slide_To_1 --
-   ----------------
-
-   function Slide_To_1 (Str : String) return String is
-      (declare
-         Res : constant String (1 .. Str'Length) := Str;
-       begin
-         Res);
-
 end System.Value_U;
diff --git a/gcc/ada/libgnat/s-valuti.ads b/gcc/ada/libgnat/s-valuti.ads
index 2b89b12..7c2da17 100644
--- a/gcc/ada/libgnat/s-valuti.ads
+++ b/gcc/ada/libgnat/s-valuti.ads
@@ -374,48 +374,274 @@ is
    --  no check for this case, the caller must ensure this condition is met.
    pragma Warnings (GNATprove, On, """Ptr"" is not modified");
 
-   --  Bundle Int type with other types, constants and subprograms used in
+   --  Bundle Uns type with other types, constants and subprograms used in
    --  ghost code, so that this package can be instantiated once and used
-   --  multiple times as generic formal for a given Int type.
+   --  multiple times as generic formal for a given Uns type.
    generic
-      type Int is range <>;
       type Uns is mod <>;
-      type Uns_Option is private;
+      type P_Uns_Option is private with Ghost;
+      with function P_Wrap_Option (Value : Uns) return P_Uns_Option
+        with Ghost;
+      with function P_Hexa_To_Unsigned_Ghost (X : Character) return Uns
+        with Ghost;
+      with function P_Scan_Overflows_Ghost
+        (Digit : Uns;
+         Base  : Uns;
+         Acc   : Uns) return Boolean
+        with Ghost;
+      with function P_Is_Raw_Unsigned_Format_Ghost
+        (Str : String) return Boolean
+        with Ghost;
+      with function P_Scan_Split_No_Overflow_Ghost
+        (Str      : String;
+         From, To : Integer)
+      return Boolean
+        with Ghost;
+      with function P_Raw_Unsigned_No_Overflow_Ghost
+        (Str      : String;
+         From, To : Integer)
+      return Boolean
+        with Ghost;
 
-      Unsigned_Width_Ghost : Natural;
+      with function P_Exponent_Unsigned_Ghost
+        (Value : Uns;
+         Exp   : Natural;
+         Base  : Uns := 10) return P_Uns_Option
+        with Ghost;
+      with procedure P_Lemma_Exponent_Unsigned_Ghost_Base
+        (Value : Uns;
+         Exp   : Natural;
+         Base  : Uns := 10)
+        with Ghost;
+      with procedure P_Lemma_Exponent_Unsigned_Ghost_Overflow
+        (Value : Uns;
+         Exp   : Natural;
+         Base  : Uns := 10)
+        with Ghost;
+      with procedure P_Lemma_Exponent_Unsigned_Ghost_Step
+        (Value : Uns;
+         Exp   : Natural;
+         Base  : Uns := 10)
+        with Ghost;
 
-      with function Wrap_Option (Value : Uns) return Uns_Option
-         with Ghost;
-      with function Only_Decimal_Ghost
+      with function P_Scan_Raw_Unsigned_Ghost
         (Str      : String;
          From, To : Integer)
-         return Boolean
-         with Ghost;
-      with function Hexa_To_Unsigned_Ghost (X : Character) return Uns
-         with Ghost;
-      with function Scan_Based_Number_Ghost
+      return Uns
+        with Ghost;
+      with procedure P_Lemma_Scan_Based_Number_Ghost_Base
         (Str      : String;
          From, To : Integer;
          Base     : Uns := 10;
          Acc      : Uns := 0)
-         return Uns_Option
-         with Ghost;
-      with function Is_Integer_Ghost (Str : String) return Boolean
-         with Ghost;
-      with procedure Prove_Iter_Scan_Based_Number_Ghost
+        with Ghost;
+      with procedure P_Lemma_Scan_Based_Number_Ghost_Underscore
+        (Str      : String;
+         From, To : Integer;
+         Base     : Uns := 10;
+         Acc      : Uns := 0)
+        with Ghost;
+      with procedure P_Lemma_Scan_Based_Number_Ghost_Overflow
+        (Str      : String;
+         From, To : Integer;
+         Base     : Uns := 10;
+         Acc      : Uns := 0)
+        with Ghost;
+      with procedure P_Lemma_Scan_Based_Number_Ghost_Step
+        (Str      : String;
+         From, To : Integer;
+         Base     : Uns := 10;
+         Acc      : Uns := 0)
+        with Ghost;
+
+      with function P_Raw_Unsigned_Last_Ghost
+        (Str      : String;
+         From, To : Integer)
+      return Positive
+        with Ghost;
+      with function P_Only_Decimal_Ghost
+        (Str      : String;
+         From, To : Integer)
+      return Boolean
+        with Ghost;
+      with function P_Scan_Based_Number_Ghost
+        (Str      : String;
+         From, To : Integer;
+         Base     : Uns := 10;
+         Acc      : Uns := 0)
+      return P_Uns_Option
+        with Ghost;
+      with function P_Is_Unsigned_Ghost (Str : String) return Boolean
+        with Ghost;
+      with function P_Is_Value_Unsigned_Ghost
+        (Str : String;
+         Val : Uns) return Boolean
+        with Ghost;
+
+      with procedure P_Prove_Scan_Only_Decimal_Ghost
+        (Str : String;
+         Val : Uns)
+        with Ghost;
+      with procedure P_Prove_Scan_Based_Number_Ghost_Eq
         (Str1, Str2 : String;
+         From, To   : Integer;
+         Base       : Uns := 10;
+         Acc        : Uns := 0)
+        with Ghost;
+
+   package Uns_Params is
+      subtype Uns_Option is P_Uns_Option with Ghost;
+      function Wrap_Option (Value : Uns) return Uns_Option renames
+        P_Wrap_Option;
+      function Hexa_To_Unsigned_Ghost
+        (X : Character) return Uns
+         renames P_Hexa_To_Unsigned_Ghost;
+      function Scan_Overflows_Ghost
+        (Digit : Uns;
+         Base  : Uns;
+         Acc   : Uns) return Boolean
+         renames P_Scan_Overflows_Ghost;
+      function Is_Raw_Unsigned_Format_Ghost
+        (Str : String) return Boolean
+         renames P_Is_Raw_Unsigned_Format_Ghost;
+      function Scan_Split_No_Overflow_Ghost
+        (Str      : String;
+         From, To : Integer) return Boolean
+         renames P_Scan_Split_No_Overflow_Ghost;
+      function Raw_Unsigned_No_Overflow_Ghost
+        (Str      : String;
+         From, To : Integer) return Boolean
+         renames P_Raw_Unsigned_No_Overflow_Ghost;
+
+      function Exponent_Unsigned_Ghost
+        (Value : Uns;
+         Exp   : Natural;
+         Base  : Uns := 10) return Uns_Option
+         renames P_Exponent_Unsigned_Ghost;
+      procedure Lemma_Exponent_Unsigned_Ghost_Base
+        (Value : Uns;
+         Exp   : Natural;
+         Base  : Uns := 10)
+         renames P_Lemma_Exponent_Unsigned_Ghost_Base;
+      procedure Lemma_Exponent_Unsigned_Ghost_Overflow
+        (Value : Uns;
+         Exp   : Natural;
+         Base  : Uns := 10)
+         renames P_Lemma_Exponent_Unsigned_Ghost_Overflow;
+      procedure Lemma_Exponent_Unsigned_Ghost_Step
+        (Value : Uns;
+         Exp   : Natural;
+         Base  : Uns := 10)
+         renames P_Lemma_Exponent_Unsigned_Ghost_Step;
+
+      function Scan_Raw_Unsigned_Ghost
+        (Str      : String;
+         From, To : Integer) return Uns
+         renames P_Scan_Raw_Unsigned_Ghost;
+      procedure Lemma_Scan_Based_Number_Ghost_Base
+        (Str      : String;
+         From, To : Integer;
+         Base     : Uns := 10;
+         Acc      : Uns := 0)
+         renames P_Lemma_Scan_Based_Number_Ghost_Base;
+      procedure Lemma_Scan_Based_Number_Ghost_Underscore
+        (Str      : String;
          From, To : Integer;
          Base     : Uns := 10;
          Acc      : Uns := 0)
+         renames P_Lemma_Scan_Based_Number_Ghost_Underscore;
+      procedure Lemma_Scan_Based_Number_Ghost_Overflow
+        (Str      : String;
+         From, To : Integer;
+         Base     : Uns := 10;
+         Acc      : Uns := 0)
+         renames P_Lemma_Scan_Based_Number_Ghost_Overflow;
+      procedure Lemma_Scan_Based_Number_Ghost_Step
+        (Str      : String;
+         From, To : Integer;
+         Base     : Uns := 10;
+         Acc      : Uns := 0)
+         renames P_Lemma_Scan_Based_Number_Ghost_Step;
+
+      function Raw_Unsigned_Last_Ghost
+        (Str      : String;
+         From, To : Integer) return Positive
+         renames P_Raw_Unsigned_Last_Ghost;
+      function Only_Decimal_Ghost
+        (Str      : String;
+         From, To : Integer) return Boolean
+         renames P_Only_Decimal_Ghost;
+      function Scan_Based_Number_Ghost
+        (Str      : String;
+         From, To : Integer;
+         Base     : Uns := 10;
+         Acc      : Uns := 0) return Uns_Option
+         renames P_Scan_Based_Number_Ghost;
+      function Is_Unsigned_Ghost (Str : String) return Boolean
+         renames P_Is_Unsigned_Ghost;
+      function Is_Value_Unsigned_Ghost
+        (Str : String;
+         Val : Uns) return Boolean
+         renames P_Is_Value_Unsigned_Ghost;
+
+      procedure Prove_Scan_Only_Decimal_Ghost
+        (Str : String;
+         Val : Uns)
+         renames P_Prove_Scan_Only_Decimal_Ghost;
+      procedure Prove_Scan_Based_Number_Ghost_Eq
+        (Str1, Str2 : String;
+         From, To   : Integer;
+         Base       : Uns := 10;
+         Acc        : Uns := 0)
+      renames P_Prove_Scan_Based_Number_Ghost_Eq;
+   end Uns_Params;
+
+   --  Bundle Int type with other types, constants and subprograms used in
+   --  ghost code, so that this package can be instantiated once and used
+   --  multiple times as generic formal for a given Int type.
+   generic
+      type Int is range <>;
+      type Uns is mod <>;
+
+      with package P_Uns_Params is new System.Val_Util.Uns_Params
+        (Uns => Uns, others => <>)
+         with Ghost;
+
+      with function P_Abs_Uns_Of_Int (Val : Int) return Uns
+         with Ghost;
+      with function P_Is_Int_Of_Uns
+        (Minus : Boolean;
+         Uval  : Uns;
+         Val   : Int)
+      return Boolean
          with Ghost;
-      with procedure Prove_Scan_Only_Decimal_Ghost (Str : String; Val : Int)
+      with function P_Is_Integer_Ghost (Str : String) return Boolean
          with Ghost;
-      with function Abs_Uns_Of_Int (Val : Int) return Uns
+      with function P_Is_Value_Integer_Ghost
+        (Str : String;
+         Val : Int) return Boolean
          with Ghost;
-      with function Value_Integer (Str : String) return Int
+      with procedure P_Prove_Scan_Only_Decimal_Ghost (Str : String; Val : Int)
          with Ghost;
 
    package Int_Params is
+      package Uns_Params renames P_Uns_Params;
+      function Abs_Uns_Of_Int (Val : Int) return Uns renames
+        P_Abs_Uns_Of_Int;
+      function Is_Int_Of_Uns
+        (Minus : Boolean;
+         Uval  : Uns;
+         Val   : Int)
+      return Boolean
+         renames P_Is_Int_Of_Uns;
+      function Is_Integer_Ghost (Str : String) return Boolean renames
+        P_Is_Integer_Ghost;
+      function Is_Value_Integer_Ghost
+        (Str : String;
+         Val : Int) return Boolean
+         renames P_Is_Value_Integer_Ghost;
+      procedure Prove_Scan_Only_Decimal_Ghost (Str : String; Val : Int) renames
+        P_Prove_Scan_Only_Decimal_Ghost;
    end Int_Params;
 
 private
diff --git a/gcc/ada/libgnat/s-vauspe.adb b/gcc/ada/libgnat/s-vauspe.adb
new file mode 100644
index 0000000..1a870b9
--- /dev/null
+++ b/gcc/ada/libgnat/s-vauspe.adb
@@ -0,0 +1,198 @@
+------------------------------------------------------------------------------
+--                                                                          --
+--                         GNAT COMPILER COMPONENTS                         --
+--                                                                          --
+--                   S Y S T E M . V A L U E _ U _ S P E C                  --
+--                                                                          --
+--                                 B o d y                                  --
+--                                                                          --
+--          Copyright (C) 2022-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.      --
+--                                                                          --
+------------------------------------------------------------------------------
+
+pragma Assertion_Policy (Pre                => Ignore,
+                         Post               => Ignore,
+                         Contract_Cases     => Ignore,
+                         Ghost              => Ignore,
+                         Subprogram_Variant => Ignore);
+
+package body System.Value_U_Spec with SPARK_Mode is
+
+   -----------------------------
+   -- Exponent_Unsigned_Ghost --
+   -----------------------------
+
+   function Exponent_Unsigned_Ghost
+     (Value : Uns;
+      Exp   : Natural;
+      Base  : Uns := 10) return Uns_Option
+   is
+      (if Exp = 0 or Value = 0 then (Overflow => False, Value => Value)
+       elsif Scan_Overflows_Ghost (0, Base, Value) then (Overflow => True)
+       else Exponent_Unsigned_Ghost (Value * Base, Exp - 1, Base));
+
+   ---------------------
+   -- Last_Hexa_Ghost --
+   ---------------------
+
+   function Last_Hexa_Ghost (Str : String) return Positive is
+   begin
+      for J in Str'Range loop
+         if Str (J) not in '0' .. '9' | 'a' .. 'f' | 'A' .. 'F' | '_' then
+            return J - 1;
+         end if;
+
+         pragma Loop_Invariant
+           (for all K in Str'First .. J =>
+              Str (K) in '0' .. '9' | 'a' .. 'f' | 'A' .. 'F' | '_');
+      end loop;
+
+      return Str'Last;
+   end Last_Hexa_Ghost;
+
+   -----------------------------
+   -- Lemmas with null bodies --
+   -----------------------------
+
+   procedure Lemma_Scan_Based_Number_Ghost_Base
+     (Str      : String;
+      From, To : Integer;
+      Base     : Uns := 10;
+      Acc      : Uns := 0)
+   is null;
+
+   procedure Lemma_Scan_Based_Number_Ghost_Underscore
+     (Str      : String;
+      From, To : Integer;
+      Base     : Uns := 10;
+      Acc      : Uns := 0)
+   is null;
+
+   procedure Lemma_Scan_Based_Number_Ghost_Overflow
+     (Str      : String;
+      From, To : Integer;
+      Base     : Uns := 10;
+      Acc      : Uns := 0)
+   is null;
+
+   procedure Lemma_Scan_Based_Number_Ghost_Step
+     (Str      : String;
+      From, To : Integer;
+      Base     : Uns := 10;
+      Acc      : Uns := 0)
+   is null;
+
+   procedure Lemma_Exponent_Unsigned_Ghost_Base
+     (Value : Uns;
+      Exp   : Natural;
+      Base  : Uns := 10)
+   is null;
+
+   procedure Lemma_Exponent_Unsigned_Ghost_Overflow
+     (Value : Uns;
+      Exp   : Natural;
+      Base  : Uns := 10)
+   is null;
+
+   procedure Lemma_Exponent_Unsigned_Ghost_Step
+     (Value : Uns;
+      Exp   : Natural;
+      Base  : Uns := 10)
+   is null;
+
+   --------------------------------------
+   -- Prove_Scan_Based_Number_Ghost_Eq --
+   --------------------------------------
+
+   procedure Prove_Scan_Based_Number_Ghost_Eq
+     (Str1, Str2 : String;
+      From, To : Integer;
+      Base     : Uns := 10;
+      Acc      : Uns := 0)
+   is
+   begin
+      if From > To then
+         null;
+      elsif Str1 (From) = '_' then
+         Prove_Scan_Based_Number_Ghost_Eq
+           (Str1, Str2, From + 1, To, Base, Acc);
+      elsif Scan_Overflows_Ghost
+        (Hexa_To_Unsigned_Ghost (Str1 (From)), Base, Acc)
+      then
+         null;
+      else
+         Prove_Scan_Based_Number_Ghost_Eq
+           (Str1, Str2, From + 1, To, Base,
+            Base * Acc + Hexa_To_Unsigned_Ghost (Str1 (From)));
+      end if;
+   end Prove_Scan_Based_Number_Ghost_Eq;
+
+   -----------------------------------
+   -- Prove_Scan_Only_Decimal_Ghost --
+   -----------------------------------
+
+   procedure Prove_Scan_Only_Decimal_Ghost
+     (Str : String;
+      Val : Uns)
+   is
+      pragma Assert (Str (Str'First + 1) /= ' ');
+      Non_Blank : constant Positive := First_Non_Space_Ghost
+        (Str, Str'First, Str'Last);
+      pragma Assert (Non_Blank = Str'First + 1);
+      Fst_Num   : constant Positive :=
+        (if Str (Non_Blank) = '+' then Non_Blank + 1 else Non_Blank);
+      pragma Assert (Fst_Num = Str'First + 1);
+   begin
+      pragma Assert
+        (Is_Raw_Unsigned_Format_Ghost (Str (Fst_Num .. Str'Last)));
+      pragma Assert
+        (Scan_Split_No_Overflow_Ghost (Str, Str'First + 1, Str'Last));
+      pragma Assert
+        ((Val, 10, 0) = Scan_Split_Value_Ghost (Str, Str'First + 1, Str'Last));
+      pragma Assert
+        (Raw_Unsigned_No_Overflow_Ghost (Str, Fst_Num, Str'Last));
+      pragma Assert (Val = Exponent_Unsigned_Ghost (Val, 0, 10).Value);
+      pragma Assert (Is_Unsigned_Ghost (Str));
+      pragma Assert (Is_Value_Unsigned_Ghost (Str, Val));
+   end Prove_Scan_Only_Decimal_Ghost;
+
+   -----------------------------
+   -- Scan_Based_Number_Ghost --
+   -----------------------------
+
+   function Scan_Based_Number_Ghost
+     (Str      : String;
+      From, To : Integer;
+      Base     : Uns := 10;
+      Acc      : Uns := 0) return Uns_Option
+   is
+      (if From > To then (Overflow => False, Value => Acc)
+       elsif Str (From) = '_'
+       then Scan_Based_Number_Ghost (Str, From + 1, To, Base, Acc)
+       elsif Scan_Overflows_Ghost
+         (Hexa_To_Unsigned_Ghost (Str (From)), Base, Acc)
+       then (Overflow => True)
+       else Scan_Based_Number_Ghost
+         (Str, From + 1, To, Base,
+          Base * Acc + Hexa_To_Unsigned_Ghost (Str (From))));
+
+end System.Value_U_Spec;
diff --git a/gcc/ada/libgnat/s-vauspe.ads b/gcc/ada/libgnat/s-vauspe.ads
new file mode 100644
index 0000000..0d5c19e
--- /dev/null
+++ b/gcc/ada/libgnat/s-vauspe.ads
@@ -0,0 +1,639 @@
+------------------------------------------------------------------------------
+--                                                                          --
+--                         GNAT COMPILER COMPONENTS                         --
+--                                                                          --
+--                   S Y S T E M . V A L U E _ U _ S P E C                  --
+--                                                                          --
+--                                 S p e c                                  --
+--                                                                          --
+--          Copyright (C) 2022-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.      --
+--                                                                          --
+------------------------------------------------------------------------------
+
+--  This package contains the specification entities using for the formal
+--  verification of the routines for scanning modular Unsigned values.
+
+--  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,
+                         Subprogram_Variant => Ignore);
+
+with System.Val_Util; use System.Val_Util;
+
+generic
+
+   type Uns is mod <>;
+
+package System.Value_U_Spec with
+   Ghost,
+   SPARK_Mode,
+   Annotate => (GNATprove, Always_Return)
+is
+   pragma Preelaborate;
+
+   type Uns_Option (Overflow : Boolean := False) is record
+      case Overflow is
+         when True =>
+            null;
+         when False =>
+            Value : Uns := 0;
+      end case;
+   end record;
+
+   function Wrap_Option (Value : Uns) return Uns_Option is
+     (Overflow => False, Value => Value);
+
+   function Only_Decimal_Ghost
+     (Str      : String;
+      From, To : Integer)
+      return Boolean
+   is
+      (for all J in From .. To => Str (J) in '0' .. '9')
+   with
+     Pre => From > To or else (From >= Str'First and then To <= Str'Last);
+   --  Ghost function that returns True if S has only decimal characters
+   --  from index From to index To.
+
+   function Only_Hexa_Ghost (Str : String; From, To : Integer) return Boolean
+   is
+      (for all J in From .. To =>
+          Str (J) in '0' .. '9' | 'a' .. 'f' | 'A' .. 'F' | '_')
+   with
+     Pre => From > To or else (From >= Str'First and then To <= Str'Last);
+   --  Ghost function that returns True if S has only hexadecimal characters
+   --  from index From to index To.
+
+   function Last_Hexa_Ghost (Str : String) return Positive
+   with
+     Pre  => Str /= ""
+       and then Str (Str'First) in '0' .. '9' | 'a' .. 'f' | 'A' .. 'F',
+     Post => Last_Hexa_Ghost'Result in Str'Range
+       and then (if Last_Hexa_Ghost'Result < Str'Last then
+                   Str (Last_Hexa_Ghost'Result + 1) not in
+                     '0' .. '9' | 'a' .. 'f' | 'A' .. 'F' | '_')
+       and then Only_Hexa_Ghost (Str, Str'First, Last_Hexa_Ghost'Result);
+   --  Ghost function that returns the index of the last character in S that
+   --  is either an hexadecimal digit or an underscore, which necessarily
+   --  exists given the precondition on Str.
+
+   function Is_Based_Format_Ghost (Str : String) return Boolean
+   is
+     (Str /= ""
+        and then Str (Str'First) in '0' .. '9' | 'a' .. 'f' | 'A' .. 'F'
+        and then
+        (declare
+           L : constant Positive := Last_Hexa_Ghost (Str);
+         begin
+           Str (L) /= '_'
+             and then (for all J in Str'First .. L =>
+                         (if Str (J) = '_' then Str (J + 1) /= '_'))));
+   --  Ghost function that determines if Str has the correct format for a
+   --  based number, consisting in a sequence of hexadecimal digits possibly
+   --  separated by single underscores. It may be followed by other characters.
+
+   function Hexa_To_Unsigned_Ghost (X : Character) return Uns is
+     (case X is
+         when '0' .. '9' => Character'Pos (X) - Character'Pos ('0'),
+         when 'a' .. 'f' => Character'Pos (X) - Character'Pos ('a') + 10,
+         when 'A' .. 'F' => Character'Pos (X) - Character'Pos ('A') + 10,
+         when others     => raise Program_Error)
+   with
+     Pre => X in '0' .. '9' | 'a' .. 'f' | 'A' .. 'F';
+   --  Ghost function that computes the value corresponding to an hexadecimal
+   --  digit.
+
+   function Scan_Overflows_Ghost
+     (Digit : Uns;
+      Base  : Uns;
+      Acc   : Uns) return Boolean
+   is
+     (Digit >= Base
+      or else Acc > Uns'Last / Base
+      or else Uns'Last - Digit < Base * Acc);
+   --  Ghost function which returns True if Digit + Base * Acc overflows or
+   --  Digit is greater than Base, as this is used by the algorithm for the
+   --  test of overflow.
+
+   function Scan_Based_Number_Ghost
+     (Str      : String;
+      From, To : Integer;
+      Base     : Uns := 10;
+      Acc      : Uns := 0) return Uns_Option
+   with
+     Subprogram_Variant => (Increases => From),
+     Pre  => Str'Last /= Positive'Last
+         and then
+           (From > To or else (From >= Str'First and then To <= Str'Last))
+         and then Only_Hexa_Ghost (Str, From, To);
+   --  Ghost function that recursively computes the based number in Str,
+   --  assuming Acc has been scanned already and scanning continues at index
+   --  From.
+
+   --  Lemmas unfolding the recursive definition of Scan_Based_Number_Ghost
+
+   procedure Lemma_Scan_Based_Number_Ghost_Base
+     (Str      : String;
+      From, To : Integer;
+      Base     : Uns := 10;
+      Acc      : Uns := 0)
+   with
+     Global => null,
+     Pre  => Str'Last /= Positive'Last
+         and then
+           (From > To or else (From >= Str'First and then To <= Str'Last))
+         and then Only_Hexa_Ghost (Str, From, To),
+     Post =>
+      (if From > To
+       then Scan_Based_Number_Ghost (Str, From, To, Base, Acc) =
+         (Overflow => False, Value => Acc));
+   --  Base case: Scan_Based_Number_Ghost returns Acc if From is bigger than To
+
+   procedure Lemma_Scan_Based_Number_Ghost_Underscore
+     (Str      : String;
+      From, To : Integer;
+      Base     : Uns := 10;
+      Acc      : Uns := 0)
+   with
+     Global => null,
+     Pre  => Str'Last /= Positive'Last
+         and then
+           (From > To or else (From >= Str'First and then To <= Str'Last))
+         and then Only_Hexa_Ghost (Str, From, To),
+     Post =>
+      (if From <= To and then Str (From) = '_'
+       then Scan_Based_Number_Ghost (Str, From, To, Base, Acc) =
+           Scan_Based_Number_Ghost (Str, From + 1, To, Base, Acc));
+   --  Underscore case: underscores are ignored while scanning
+
+   procedure Lemma_Scan_Based_Number_Ghost_Overflow
+     (Str      : String;
+      From, To : Integer;
+      Base     : Uns := 10;
+      Acc      : Uns := 0)
+   with
+     Global => null,
+     Pre  => Str'Last /= Positive'Last
+         and then
+           (From > To or else (From >= Str'First and then To <= Str'Last))
+         and then Only_Hexa_Ghost (Str, From, To),
+     Post =>
+      (if From <= To
+         and then Str (From) /= '_'
+         and then Scan_Overflows_Ghost
+           (Hexa_To_Unsigned_Ghost (Str (From)), Base, Acc)
+       then Scan_Based_Number_Ghost (Str, From, To, Base, Acc) =
+           (Overflow => True));
+   --  Overflow case: scanning a digit which causes an overflow
+
+   procedure Lemma_Scan_Based_Number_Ghost_Step
+     (Str      : String;
+      From, To : Integer;
+      Base     : Uns := 10;
+      Acc      : Uns := 0)
+   with
+     Global => null,
+     Pre  => Str'Last /= Positive'Last
+         and then
+           (From > To or else (From >= Str'First and then To <= Str'Last))
+         and then Only_Hexa_Ghost (Str, From, To),
+     Post =>
+      (if From <= To
+         and then Str (From) /= '_'
+         and then not Scan_Overflows_Ghost
+           (Hexa_To_Unsigned_Ghost (Str (From)), Base, Acc)
+       then Scan_Based_Number_Ghost (Str, From, To, Base, Acc) =
+         Scan_Based_Number_Ghost
+           (Str, From + 1, To, Base,
+            Base * Acc + Hexa_To_Unsigned_Ghost (Str (From))));
+   --  Normal case: scanning a digit without overflows
+
+   function Exponent_Unsigned_Ghost
+     (Value : Uns;
+      Exp   : Natural;
+      Base  : Uns := 10) return Uns_Option
+   with
+     Subprogram_Variant => (Decreases => Exp);
+   --  Ghost function that recursively computes Value * Base ** Exp
+
+   --  Lemmas unfolding the recursive definition of Exponent_Unsigned_Ghost
+
+   procedure Lemma_Exponent_Unsigned_Ghost_Base
+     (Value : Uns;
+      Exp   : Natural;
+      Base  : Uns := 10)
+   with
+     Post =>
+       (if Exp = 0 or Value = 0
+        then Exponent_Unsigned_Ghost (Value, Exp, Base) =
+          (Overflow => False, Value => Value));
+   --  Base case: Exponent_Unsigned_Ghost returns 0 if Value or Exp is 0
+
+   procedure Lemma_Exponent_Unsigned_Ghost_Overflow
+     (Value : Uns;
+      Exp   : Natural;
+      Base  : Uns := 10)
+   with
+     Post =>
+       (if Exp /= 0
+          and then Value /= 0
+          and then Scan_Overflows_Ghost (0, Base, Value)
+        then Exponent_Unsigned_Ghost (Value, Exp, Base) = (Overflow => True));
+   --  Overflow case: the next multiplication overflows
+
+   procedure Lemma_Exponent_Unsigned_Ghost_Step
+     (Value : Uns;
+      Exp   : Natural;
+      Base  : Uns := 10)
+   with
+     Post =>
+       (if Exp /= 0
+          and then Value /= 0
+          and then not Scan_Overflows_Ghost (0, Base, Value)
+        then Exponent_Unsigned_Ghost (Value, Exp, Base) =
+            Exponent_Unsigned_Ghost (Value * Base, Exp - 1, Base));
+   --  Normal case: exponentiation without overflows
+
+   function Is_Raw_Unsigned_Format_Ghost (Str : String) return Boolean is
+     (Is_Natural_Format_Ghost (Str)
+      and then
+        (declare
+           Last_Num_Init   : constant Integer := Last_Number_Ghost (Str);
+           Starts_As_Based : constant Boolean :=
+             Last_Num_Init < Str'Last - 1
+             and then Str (Last_Num_Init + 1) in '#' | ':'
+             and then Str (Last_Num_Init + 2) in
+               '0' .. '9' | 'a' .. 'f' | 'A' .. 'F';
+           Last_Num_Based  : constant Integer :=
+             (if Starts_As_Based
+              then Last_Hexa_Ghost (Str (Last_Num_Init + 2 .. Str'Last))
+              else Last_Num_Init);
+           Is_Based        : constant Boolean :=
+             Starts_As_Based
+             and then Last_Num_Based < Str'Last
+             and then Str (Last_Num_Based + 1) = Str (Last_Num_Init + 1);
+           First_Exp       : constant Integer :=
+             (if Is_Based then Last_Num_Based + 2 else Last_Num_Init + 1);
+         begin
+           (if Starts_As_Based then
+              Is_Based_Format_Ghost (Str (Last_Num_Init + 2 .. Str'Last))
+              and then Last_Num_Based < Str'Last)
+            and then Is_Opt_Exponent_Format_Ghost
+              (Str (First_Exp .. Str'Last))))
+   with
+     Pre  => Str'Last /= Positive'Last;
+   --  Ghost function that determines if Str has the correct format for an
+   --  unsigned number without a sign character.
+   --  It is a natural number in base 10, optionally followed by a based
+   --  number surrounded by delimiters # or :, optionally followed by an
+   --  exponent part.
+
+   type Split_Value_Ghost is record
+      Value : Uns;
+      Base  : Uns;
+      Expon : Natural;
+   end record;
+
+   function Scan_Split_No_Overflow_Ghost
+     (Str      : String;
+      From, To : Integer)
+      return Boolean
+   is
+     (declare
+        Last_Num_Init   : constant Integer :=
+          Last_Number_Ghost (Str (From .. To));
+        Init_Val        : constant Uns_Option :=
+          Scan_Based_Number_Ghost (Str, From, Last_Num_Init);
+        Starts_As_Based : constant Boolean :=
+          Last_Num_Init < To - 1
+          and then Str (Last_Num_Init + 1) in '#' | ':'
+          and then Str (Last_Num_Init + 2) in
+          '0' .. '9' | 'a' .. 'f' | 'A' .. 'F';
+        Last_Num_Based  : constant Integer :=
+          (if Starts_As_Based
+           then Last_Hexa_Ghost (Str (Last_Num_Init + 2 .. To))
+           else Last_Num_Init);
+        Based_Val       : constant Uns_Option :=
+          (if Starts_As_Based and then not Init_Val.Overflow
+           then Scan_Based_Number_Ghost
+             (Str, Last_Num_Init + 2, Last_Num_Based, Init_Val.Value)
+           else Init_Val);
+      begin
+        not Init_Val.Overflow
+        and then
+          (Last_Num_Init >= To - 1
+           or else Str (Last_Num_Init + 1) not in '#' | ':'
+           or else Init_Val.Value in 2 .. 16)
+        and then
+          (not Starts_As_Based
+           or else not Based_Val.Overflow))
+   with
+     Pre  => Str'Last /= Positive'Last
+       and then From in Str'Range
+       and then To in From .. Str'Last
+       and then Str (From) in '0' .. '9';
+   --  Ghost function that determines if an overflow might occur while scanning
+   --  the representation of an unsigned number. The computation overflows if
+   --  either:
+   --    * The computation of the decimal part overflows,
+   --    * The decimal part is followed by a valid delimiter for a based
+   --      part, and the number corresponding to the base is not a valid base,
+   --      or
+   --    * The computation of the based part overflows.
+
+   pragma Warnings (Off, "constant * is not referenced");
+   function Scan_Split_Value_Ghost
+     (Str      : String;
+      From, To : Integer)
+      return Split_Value_Ghost
+   is
+     (declare
+        Last_Num_Init   : constant Integer :=
+          Last_Number_Ghost (Str (From .. To));
+        Init_Val        : constant Uns_Option :=
+          Scan_Based_Number_Ghost (Str, From, Last_Num_Init);
+        Starts_As_Based : constant Boolean :=
+          Last_Num_Init < To - 1
+          and then Str (Last_Num_Init + 1) in '#' | ':'
+          and then Str (Last_Num_Init + 2) in
+          '0' .. '9' | 'a' .. 'f' | 'A' .. 'F';
+        Last_Num_Based  : constant Integer :=
+          (if Starts_As_Based
+           then Last_Hexa_Ghost (Str (Last_Num_Init + 2 .. To))
+           else Last_Num_Init);
+        Is_Based        : constant Boolean :=
+          Starts_As_Based
+          and then Last_Num_Based < To
+          and then Str (Last_Num_Based + 1) = Str (Last_Num_Init + 1);
+        Based_Val       : constant Uns_Option :=
+          (if Starts_As_Based and then not Init_Val.Overflow
+           then Scan_Based_Number_Ghost
+             (Str, Last_Num_Init + 2, Last_Num_Based, Init_Val.Value)
+           else Init_Val);
+        First_Exp       : constant Integer :=
+          (if Is_Based then Last_Num_Based + 2 else Last_Num_Init + 1);
+        Expon           : constant Natural :=
+          (if Starts_As_Exponent_Format_Ghost (Str (First_Exp .. To))
+           then Scan_Exponent_Ghost (Str (First_Exp .. To))
+           else 0);
+        Base            : constant Uns :=
+          (if Is_Based then Init_Val.Value else 10);
+        Value           : constant Uns :=
+          (if Is_Based then Based_Val.Value else Init_Val.Value);
+      begin
+        (Value => Value, Base => Base, Expon => Expon))
+   with
+     Pre => Str'Last /= Positive'Last
+       and then From in Str'Range
+       and then To in From .. Str'Last
+       and then Str (From) in '0' .. '9'
+       and then Scan_Split_No_Overflow_Ghost (Str, From, To);
+   --  Ghost function that scans an unsigned number without a sign character
+   --  and return a record containing the values scanned for its value, its
+   --  base, and its exponent.
+   pragma Warnings (On, "constant * is not referenced");
+
+   function Raw_Unsigned_No_Overflow_Ghost
+     (Str      : String;
+      From, To : Integer)
+      return Boolean
+   is
+     (Scan_Split_No_Overflow_Ghost (Str, From, To)
+      and then
+        (declare
+           Val : constant Split_Value_Ghost := Scan_Split_Value_Ghost
+             (Str, From, To);
+         begin
+           not Exponent_Unsigned_Ghost
+             (Val.Value, Val.Expon, Val.Base).Overflow))
+   with
+     Pre => Str'Last /= Positive'Last
+       and then From in Str'Range
+       and then To in From .. Str'Last
+       and then Str (From) in '0' .. '9';
+   --  Ghost function that determines if the computation of the unsigned number
+   --  represented by Str will overflow. The computation overflows if either:
+   --    * The scan of the string overflows, or
+   --    * The computation of the exponentiation overflows.
+
+   function Scan_Raw_Unsigned_Ghost
+     (Str      : String;
+      From, To : Integer)
+      return Uns
+   is
+     (declare
+        Val : constant Split_Value_Ghost := Scan_Split_Value_Ghost
+          (Str, From, To);
+      begin
+        Exponent_Unsigned_Ghost (Val.Value, Val.Expon, Val.Base).Value)
+   with
+     Pre  => Str'Last /= Positive'Last
+       and then From in Str'Range
+       and then To in From .. Str'Last
+       and then Str (From) in '0' .. '9'
+       and then Raw_Unsigned_No_Overflow_Ghost (Str, From, To);
+   --  Ghost function that scans an unsigned number without a sign character
+
+   function Raw_Unsigned_Last_Ghost
+     (Str      : String;
+      From, To : Integer)
+      return Positive
+   is
+     (declare
+        Last_Num_Init   : constant Integer :=
+          Last_Number_Ghost (Str (From .. To));
+        Starts_As_Based : constant Boolean :=
+          Last_Num_Init < To - 1
+          and then Str (Last_Num_Init + 1) in '#' | ':'
+          and then Str (Last_Num_Init + 2) in
+          '0' .. '9' | 'a' .. 'f' | 'A' .. 'F';
+        Last_Num_Based  : constant Integer :=
+          (if Starts_As_Based
+           then Last_Hexa_Ghost (Str (Last_Num_Init + 2 .. To))
+           else Last_Num_Init);
+        Is_Based        : constant Boolean :=
+          Starts_As_Based
+          and then Last_Num_Based < To
+          and then Str (Last_Num_Based + 1) = Str (Last_Num_Init + 1);
+        First_Exp       : constant Integer :=
+          (if Is_Based then Last_Num_Based + 2 else Last_Num_Init + 1);
+      begin
+        (if not Starts_As_Exponent_Format_Ghost (Str (First_Exp .. To))
+         then First_Exp
+         elsif Str (First_Exp + 1) in '-' | '+' then
+           Last_Number_Ghost (Str (First_Exp + 2 .. To)) + 1
+         else Last_Number_Ghost (Str (First_Exp + 1 .. To)) + 1))
+   with
+     Pre  => Str'Last /= Positive'Last
+       and then From in Str'Range
+       and then To in From .. Str'Last
+       and then Str (From) in '0' .. '9';
+   --  Ghost function that returns the position of the cursor once an unsigned
+   --  number has been seen.
+
+   function Slide_To_1 (Str : String) return String
+   with
+     Post =>
+       Only_Space_Ghost (Str, Str'First, Str'Last) =
+       (for all J in Str'First .. Str'Last =>
+          Slide_To_1'Result (J - Str'First + 1) = ' ');
+   --  Slides Str so that it starts at 1
+
+   function Slide_If_Necessary (Str : String) return String is
+     (if Str'Last = Positive'Last then Slide_To_1 (Str) else Str);
+   --  If Str'Last = Positive'Last then slides Str so that it starts at 1
+
+   function Is_Unsigned_Ghost (Str : String) return Boolean is
+     (declare
+        Non_Blank : constant Positive := First_Non_Space_Ghost
+          (Str, Str'First, Str'Last);
+        Fst_Num   : constant Positive :=
+          (if Str (Non_Blank) = '+' then Non_Blank + 1 else Non_Blank);
+      begin
+        Is_Raw_Unsigned_Format_Ghost (Str (Fst_Num .. Str'Last))
+          and then Raw_Unsigned_No_Overflow_Ghost (Str, Fst_Num, Str'Last)
+          and then Only_Space_Ghost
+             (Str, Raw_Unsigned_Last_Ghost (Str, Fst_Num, Str'Last), Str'Last))
+   with
+       Pre => not Only_Space_Ghost (Str, Str'First, Str'Last)
+       and then Str'Last /= Positive'Last;
+   --  Ghost function that determines if Str has the correct format for an
+   --  unsigned number, consisting in some blank characters, an optional
+   --  + sign, a raw unsigned number which does not overflow and then some
+   --  more blank characters.
+
+   function Is_Value_Unsigned_Ghost (Str : String; Val : Uns) return Boolean is
+     (declare
+        Non_Blank : constant Positive := First_Non_Space_Ghost
+          (Str, Str'First, Str'Last);
+        Fst_Num   : constant Positive :=
+          (if Str (Non_Blank) = '+' then Non_Blank + 1 else Non_Blank);
+      begin
+        Val = Scan_Raw_Unsigned_Ghost (Str, Fst_Num, Str'Last))
+   with
+       Pre => not Only_Space_Ghost (Str, Str'First, Str'Last)
+       and then Str'Last /= Positive'Last
+       and then Is_Unsigned_Ghost (Str);
+   --  Ghost function that returns True if Val is the value corresponding to
+   --  the unsigned number represented by Str.
+
+   procedure Prove_Scan_Based_Number_Ghost_Eq
+     (Str1, Str2 : String;
+      From, To : Integer;
+      Base     : Uns := 10;
+      Acc      : Uns := 0)
+   with
+     Subprogram_Variant => (Increases => From),
+     Pre  => Str1'Last /= Positive'Last
+       and then Str2'Last /= Positive'Last
+       and then
+         (From > To or else (From >= Str1'First and then To <= Str1'Last))
+       and then
+         (From > To or else (From >= Str2'First and then To <= Str2'Last))
+       and then Only_Hexa_Ghost (Str1, From, To)
+       and then (for all J in From .. To => Str1 (J) = Str2 (J)),
+     Post =>
+       Scan_Based_Number_Ghost (Str1, From, To, Base, Acc)
+         = Scan_Based_Number_Ghost (Str2, From, To, Base, Acc);
+   --  Scan_Based_Number_Ghost returns the same value on two slices which are
+   --  equal.
+
+   procedure Prove_Scan_Only_Decimal_Ghost
+     (Str : String;
+      Val : Uns)
+   with
+     Pre  => Str'Last /= Positive'Last
+       and then Str'Length >= 2
+       and then Str (Str'First) = ' '
+       and then Only_Decimal_Ghost (Str, Str'First + 1, Str'Last)
+       and then Scan_Based_Number_Ghost (Str, Str'First + 1, Str'Last)
+         = Wrap_Option (Val),
+     Post => Is_Unsigned_Ghost (Slide_If_Necessary (Str))
+       and then
+         Is_Value_Unsigned_Ghost (Slide_If_Necessary (Str), Val);
+   --  Ghost lemma used in the proof of 'Image implementation, to prove that
+   --  the result of Value_Unsigned on a decimal string is the same as the
+   --  result of Scan_Based_Number_Ghost.
+
+   --  Bundle Uns type with other types, constants and subprograms used in
+   --  ghost code, so that this package can be instantiated once and used
+   --  multiple times as generic formal for a given Int type.
+
+   package Uns_Params is new System.Val_Util.Uns_Params
+     (Uns                                        => Uns,
+      P_Uns_Option                               => Uns_Option,
+      P_Wrap_Option                              => Wrap_Option,
+      P_Hexa_To_Unsigned_Ghost                   => Hexa_To_Unsigned_Ghost,
+      P_Scan_Overflows_Ghost                     => Scan_Overflows_Ghost,
+      P_Is_Raw_Unsigned_Format_Ghost             =>
+         Is_Raw_Unsigned_Format_Ghost,
+      P_Scan_Split_No_Overflow_Ghost             =>
+         Scan_Split_No_Overflow_Ghost,
+      P_Raw_Unsigned_No_Overflow_Ghost           =>
+         Raw_Unsigned_No_Overflow_Ghost,
+      P_Exponent_Unsigned_Ghost                  => Exponent_Unsigned_Ghost,
+      P_Lemma_Exponent_Unsigned_Ghost_Base       =>
+         Lemma_Exponent_Unsigned_Ghost_Base,
+      P_Lemma_Exponent_Unsigned_Ghost_Overflow   =>
+         Lemma_Exponent_Unsigned_Ghost_Overflow,
+      P_Lemma_Exponent_Unsigned_Ghost_Step       =>
+         Lemma_Exponent_Unsigned_Ghost_Step,
+      P_Scan_Raw_Unsigned_Ghost                  => Scan_Raw_Unsigned_Ghost,
+      P_Lemma_Scan_Based_Number_Ghost_Base       =>
+         Lemma_Scan_Based_Number_Ghost_Base,
+      P_Lemma_Scan_Based_Number_Ghost_Underscore =>
+         Lemma_Scan_Based_Number_Ghost_Underscore,
+      P_Lemma_Scan_Based_Number_Ghost_Overflow   =>
+         Lemma_Scan_Based_Number_Ghost_Overflow,
+      P_Lemma_Scan_Based_Number_Ghost_Step       =>
+         Lemma_Scan_Based_Number_Ghost_Step,
+      P_Raw_Unsigned_Last_Ghost                  => Raw_Unsigned_Last_Ghost,
+      P_Only_Decimal_Ghost                       => Only_Decimal_Ghost,
+      P_Scan_Based_Number_Ghost                  => Scan_Based_Number_Ghost,
+      P_Is_Unsigned_Ghost                        =>
+         Is_Unsigned_Ghost,
+      P_Is_Value_Unsigned_Ghost                  =>
+         Is_Value_Unsigned_Ghost,
+      P_Prove_Scan_Only_Decimal_Ghost            =>
+         Prove_Scan_Only_Decimal_Ghost,
+      P_Prove_Scan_Based_Number_Ghost_Eq         =>
+         Prove_Scan_Based_Number_Ghost_Eq);
+
+private
+
+   ----------------
+   -- Slide_To_1 --
+   ----------------
+
+   function Slide_To_1 (Str : String) return String is
+      (declare
+         Res : constant String (1 .. Str'Length) := Str;
+       begin
+         Res);
+
+end System.Value_U_Spec;