prove lemma unsigned associativity sub

ref #50
Componolit · Jul 19, 2019 · 0ec84cf · 0ec84cf
1 parent 60a8e3a
commit 0ec84cf
Show file tree

Hide file tree

Showing 2 changed files with 48 additions and 4 deletions.
diff --git 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
@@ -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;