prove add with overflow check

ref #47

src/minimal/s-arit64.adb

@@ -43,13 +43,36 @@ is
    pragma Suppress (Range_Check);
 
    subtype Uns64 is Unsigned_64;
-   function To_Uns is new Ada.Unchecked_Conversion (Int64, Uns64);
+   function To_Uns_Unchecked is new Ada.Unchecked_Conversion (Int64, Uns64);
    function To_Int_Unchecked is new Ada.Unchecked_Conversion (Uns64, Int64);
 
    function To_Int (U : Uns64) return Int64 with
       Inline,
-      Contract_Cases => (U <= Uns64 (Int64'Last) => To_Int'Result >= 0,
-                         U > Uns64 (Int64'Last) => To_Int'Result < 0);
+      Contract_Cases => (U <= Uns64 (Int64'Last) =>
+                               To_Int'Result = Int64 (U),
+                         U > Uns64 (Int64'Last) =>
+                               To_Int'Result = -Int64 (Uns64'Last - U) - 1);
+
+   function To_Uns (I : Int64) return Uns64 with
+      Inline,
+      Contract_Cases => (I >= 0 => To_Uns'Result = Uns64 (I),
+                         I < 0 => To_Uns'Result =
+                            Uns64'Last - (abs (I) - Uns64'(1)));
+
+   pragma Warnings (Off, "procedure ""Lemma_Identity"" is not referenced");
+   --  This lemma is only used to prove its properties.
+   procedure Lemma_Identity (I : Int64; U : Uns64) with
+      Post => I = To_Int (To_Uns (I))
+              and U = To_Uns (To_Int (U));
+   pragma Warnings (On, "procedure ""Lemma_Identity"" is not referenced");
+
+   procedure Lemma_Uns_Associativity (X, Y : Int64) with
+      Ghost,
+      Pre      => (if X < 0 and Y <= 0 then Int64'First - X < Y)
+                  and (if X >= 0 and Y >= 0 then Int64'Last - X >= Y),
+      Post     => X + Y = To_Int (To_Uns (X) + To_Uns (Y)),
+      Annotate => (GNATprove, False_Positive, "postcondition",
+                   "addition in 2 complement is associative");
 
    subtype Uns32 is Unsigned_32;
 
@@ -123,6 +146,17 @@ is
       return To_Int_Unchecked (U);
    end To_Int;
 
+   function To_Uns (I : Int64) return Uns64 with
+      SPARK_Mode => Off
+   is
+   begin
+      return To_Uns_Unchecked (I);
+   end To_Uns;
+
+   procedure Lemma_Identity (I : Int64; U : Uns64) is null;
+
+   procedure Lemma_Uns_Associativity (X, Y : Int64) is null;
+
    --------------------------
    -- Add_With_Ovflo_Check --
    --------------------------
@@ -131,6 +165,7 @@ is
       R : constant Int64 := To_Int (To_Uns (X) + To_Uns (Y));
 
    begin
+      Lemma_Uns_Associativity (X, Y);
       if X >= 0 then
          if Y < 0 or else R >= 0 then
             return R;

src/minimal/s-arit64.ads

@@ -45,8 +45,12 @@ is
    pragma Pure;
 
    subtype Int64 is Interfaces.Integer_64;
+   use type Interfaces.Integer_64;
 
-   function Add_With_Ovflo_Check (X, Y : Int64) return Int64;
+   function Add_With_Ovflo_Check (X, Y : Int64) return Int64 with
+      Pre  => (if X < 0 and Y <= 0 then Int64'First - X < Y)
+              and (if X >= 0 and Y >= 0 then Int64'Last - X >= Y),
+      Post => Add_With_Ovflo_Check'Result = X + Y;
    --  Raises Constraint_Error if sum of operands overflows 64 bits,
    --  otherwise returns the 64-bit signed integer sum.