From 0ec84cf6d17ec1580f619449f212fc108cccee96 Mon Sep 17 00:00:00 2001
From: Johannes Kliemann <kliemann@componolit.com>
Date: Fri, 19 Jul 2019 13:16:52 +0200
Subject: [PATCH] prove lemma unsigned associativity sub ref #50

---
 src/lib/componolit-runtime-conversions.adb | 48 +++++++++++++++++++++-
 src/lib/componolit-runtime-conversions.ads |  4 +-
 2 files changed, 48 insertions(+), 4 deletions(-)

diff --git a/src/lib/componolit-runtime-conversions.adb b/src/lib/componolit-runtime-conversions.adb
index 0e1ed82..0591c55 100644
--- a/src/lib/componolit-runtime-conversions.adb
+++ b/src/lib/componolit-runtime-conversions.adb
@@ -98,6 +98,52 @@ is
       end if;
    end Lemma_Uns_Associativity_Add;
 
-   procedure Lemma_Uns_Associativity_Sub (X, Y : Int64) is null;
+   procedure Lemma_Uns_Associativity_Sub (X, Y : Int64)
+   is
+   begin
+      if X < 0 and Y < 0 then
+         if X = Int64'First and Y = Int64'First then
+            pragma Assert (X - Y = To_Int (To_Uns (X) - To_Uns (Y)));
+         elsif X = Int64'First then
+            pragma Assert (X - Y = X + (-Y));
+            pragma Assert (X - Y = To_Int (To_Uns (X) + To_Uns (-Y)));
+            pragma Assert (-To_Uns (Y) = To_Uns (-Y));
+            pragma Assert (X - Y = To_Int (To_Uns (X) - To_Uns (Y)));
+         elsif Y = Int64'First then
+            pragma Assert (X - Y = To_Int (To_Uns (X) - To_Uns (Y)));
+         else
+            if X >= Y then
+               pragma Assert (X - Y = To_Int (To_Uns (X) - To_Uns (Y)));
+            else --  X < Y
+               pragma Assert (X - Y = X + (-Y));
+               pragma Assert (X - Y = To_Int (To_Uns (X) + (-To_Uns (Y))));
+               pragma Assert (X - Y = To_Int (To_Uns (X) + To_Uns (-Y)));
+               pragma Assert (X - Y = To_Int (To_Uns (X) - To_Uns (Y)));
+            end if;
+         end if;
+      elsif X >= 0 and Y >= 0 then
+         if X >= Y then
+            pragma Assert (X - Y = To_Int (To_Uns (X) - To_Uns (Y)));
+         else --  X < Y
+            pragma Assert (X - Y = -Y - (-X));
+            pragma Assert (X - Y = -Y + X);
+            pragma Assert (X - Y = To_Int (To_Uns (-Y) + To_Uns (X)));
+            pragma Assert (X - Y = To_Int (To_Uns (X) - To_Uns (Y)));
+         end if;
+      elsif X >= 0 and Y < 0 then
+         if Y = Int64'First then
+            pragma Assert (X - Y = To_Int (To_Uns (X) - To_Uns (Y)));
+         else
+            pragma Assert (X - Y = X + (-Y));
+            pragma Assert (X - Y = To_Int (To_Uns (X) + To_Uns (-Y)));
+            pragma Assert (X - Y = To_Int (To_Uns (X) + (-To_Uns (Y))));
+            pragma Assert (X - Y = To_Int (To_Uns (X) - To_Uns (Y)));
+         end if;
+      elsif X < 0 and Y >= 0 then
+         pragma Assert (X - Y = To_Int (To_Uns (X) - To_Uns (Y)));
+      else
+         pragma Assert (X - Y = To_Int (To_Uns (X) - To_Uns (Y)));
+      end if;
+   end Lemma_Uns_Associativity_Sub;
 
 end Componolit.Runtime.Conversions;
diff --git a/src/lib/componolit-runtime-conversions.ads b/src/lib/componolit-runtime-conversions.ads
index 7b8a50b..f900211 100644
--- a/src/lib/componolit-runtime-conversions.ads
+++ b/src/lib/componolit-runtime-conversions.ads
@@ -48,8 +48,6 @@ is
       Pre      => (if X >= 0 and Y <= 0 then Y > Int64'First
                       and then Int64'Last - X >= abs (Y))
                    and (if X < 0 and Y > 0 then Y < Int64'First - X),
-      Post     => X - Y = To_Int (To_Uns (X) - To_Uns (Y)),
-      Annotate => (GNATprove, False_Positive, "postcondition",
-                   "subtraction in 2 complement is associative");
+      Post     => X - Y = To_Int (To_Uns (X) - To_Uns (Y));
 
 end Componolit.Runtime.Conversions;