[Ada] Proof of System.Arith_32 for double arithmetic on 32bits

Message ID 20211202162910.GA2160025@adacore.com
State Committed
Headers
Series [Ada] Proof of System.Arith_32 for double arithmetic on 32bits |

Commit Message

Pierre-Marie de Rodat Dec. 2, 2021, 4:29 p.m. UTC
  This replicates in a simpler setting the proofs performed for generic
unit System.Arith_Double.

Note that it makes a difference to declare functions Big as expression
functions here instead of renamings, as some checks are not proved with
renamings, so expression functions are used instead.

GNATprove is run with switches --level=3 --prover=all.

Tested on x86_64-pc-linux-gnu, committed on trunk

gcc/ada/

	* libgnat/s-arit32.adb: Add ghost instances and lemmas.
	(Scaled_Divide32): Add ghost code to prove. Minor code
	modification to return early in error when divisor is zero.
	* libgnat/s-arit32.ads: Add ghost instances and utilities.
	(Scaled_Divide32): Add contract.
  

Patch

diff --git a/gcc/ada/libgnat/s-arit32.adb b/gcc/ada/libgnat/s-arit32.adb
--- a/gcc/ada/libgnat/s-arit32.adb
+++ b/gcc/ada/libgnat/s-arit32.adb
@@ -29,9 +29,24 @@ 
 --                                                                          --
 ------------------------------------------------------------------------------
 
+--  Preconditions, postconditions, ghost code, loop invariants and assertions
+--  in this unit are meant for analysis only, not for run-time checking, as it
+--  would be too costly otherwise. This is enforced by setting the assertion
+--  policy to Ignore.
+
+pragma Assertion_Policy (Pre            => Ignore,
+                         Post           => Ignore,
+                         Ghost          => Ignore,
+                         Loop_Invariant => Ignore,
+                         Assert         => Ignore);
+
+with Ada.Numerics.Big_Numbers.Big_Integers_Ghost;
+use Ada.Numerics.Big_Numbers.Big_Integers_Ghost;
 with Ada.Unchecked_Conversion;
 
-package body System.Arith_32 is
+package body System.Arith_32
+  with SPARK_Mode
+is
 
    pragma Suppress (Overflow_Check);
    pragma Suppress (Range_Check);
@@ -43,27 +58,65 @@  package body System.Arith_32 is
 
    function To_Int is new Ada.Unchecked_Conversion (Uns32, Int32);
 
+   package Unsigned_Conversion is new Unsigned_Conversions (Int => Uns32);
+
+   function Big (Arg : Uns32) return Big_Integer is
+     (Unsigned_Conversion.To_Big_Integer (Arg))
+   with Ghost;
+
+   package Unsigned_Conversion_64 is new Unsigned_Conversions (Int => Uns64);
+
+   function Big (Arg : Uns64) return Big_Integer is
+     (Unsigned_Conversion_64.To_Big_Integer (Arg))
+   with Ghost;
+
+   pragma Warnings
+     (Off, "non-preelaborable call not allowed in preelaborated unit",
+      Reason => "Ghost code is not compiled");
+   Big_0 : constant Big_Integer :=
+     Big (Uns32'(0))
+   with Ghost;
+   Big_2xx32 : constant Big_Integer :=
+     Big (Uns32'(2 ** 32 - 1)) + 1
+   with Ghost;
+   Big_2xx64 : constant Big_Integer :=
+     Big (Uns64'(2 ** 64 - 1)) + 1
+   with Ghost;
+   pragma Warnings
+     (On, "non-preelaborable call not allowed in preelaborated unit");
+
    -----------------------
    -- Local Subprograms --
    -----------------------
 
    function "abs" (X : Int32) return Uns32 is
      (if X = Int32'First
-      then 2**31
+      then Uns32'(2**31)
       else Uns32 (Int32'(abs X)));
    --  Convert absolute value of X to unsigned. Note that we can't just use
    --  the expression of the Else since it overflows for X = Int32'First.
 
+   function Lo (A : Uns64) return Uns32 is (Uns32 (A and (2 ** 32 - 1)));
+   --  Low order half of 64-bit value
+
    function Hi (A : Uns64) return Uns32 is (Uns32 (Shift_Right (A, 32)));
    --  High order half of 64-bit value
 
-   function To_Neg_Int (A : Uns32) return Int32;
+   function To_Neg_Int (A : Uns32) return Int32
+   with
+     Annotate => (GNATprove, Terminating),
+     Pre      => In_Int32_Range (-Big (A)),
+     Post     => Big (To_Neg_Int'Result) = -Big (A);
    --  Convert to negative integer equivalent. If the input is in the range
    --  0 .. 2**31, then the corresponding nonpositive signed integer (obtained
    --  by negating the given value) is returned, otherwise constraint error is
    --  raised.
 
-   function To_Pos_Int (A : Uns32) return Int32;
+   function To_Pos_Int (A : Uns32) return Int32
+   with
+     Annotate => (GNATprove, Terminating),
+     Pre      => In_Int32_Range (Big (A)),
+     Post     => Big (To_Pos_Int'Result) = Big (A);
    --  Convert to positive integer equivalent. If the input is in the range
    --  0 .. 2**31 - 1, then the corresponding nonnegative signed integer is
    --  returned, otherwise constraint error is raised.
@@ -72,6 +125,168 @@  package body System.Arith_32 is
    pragma No_Return (Raise_Error);
    --  Raise constraint error with appropriate message
 
+   ------------------
+   -- Local Lemmas --
+   ------------------
+
+   procedure Lemma_Abs_Commutation (X : Int32)
+   with
+     Ghost,
+     Post => abs (Big (X)) = Big (Uns32'(abs X));
+
+   procedure Lemma_Abs_Div_Commutation (X, Y : Big_Integer)
+   with
+     Ghost,
+     Pre  => Y /= 0,
+     Post => abs (X / Y) = abs X / abs Y;
+
+   procedure Lemma_Abs_Mult_Commutation (X, Y : Big_Integer)
+   with
+     Ghost,
+     Post => abs (X * Y) = abs X * abs Y;
+
+   procedure Lemma_Abs_Rem_Commutation (X, Y : Big_Integer)
+   with
+     Ghost,
+     Pre  => Y /= 0,
+     Post => abs (X rem Y) = (abs X) rem (abs Y);
+
+   procedure Lemma_Div_Commutation (X, Y : Uns64)
+   with
+     Ghost,
+     Pre  => Y /= 0,
+     Post => Big (X) / Big (Y) = Big (X / Y);
+
+   procedure Lemma_Div_Ge (X, Y, Z : Big_Integer)
+   with
+     Ghost,
+     Pre  => Z > 0 and then X >= Y * Z,
+     Post => X / Z >= Y;
+
+   procedure Lemma_Ge_Commutation (A, B : Uns32)
+   with
+     Ghost,
+     Pre  => A >= B,
+     Post => Big (A) >= Big (B);
+
+   procedure Lemma_Hi_Lo (Xu : Uns64; Xhi, Xlo : Uns32)
+   with
+     Ghost,
+     Pre  => Xhi = Hi (Xu) and Xlo = Lo (Xu),
+     Post => Big (Xu) = Big_2xx32 * Big (Xhi) + Big (Xlo);
+
+   procedure Lemma_Mult_Commutation (X, Y, Z : Uns64)
+   with
+     Ghost,
+     Pre  => Big (X) * Big (Y) < Big_2xx64 and then Z = X * Y,
+     Post => Big (X) * Big (Y) = Big (Z);
+
+   procedure Lemma_Mult_Non_Negative (X, Y : Big_Integer)
+   with
+     Ghost,
+     Pre  => (X >= Big_0 and then Y >= Big_0)
+       or else (X <= Big_0 and then Y <= Big_0),
+     Post => X * Y >= Big_0;
+
+   procedure Lemma_Mult_Non_Positive (X, Y : Big_Integer)
+   with
+     Ghost,
+     Pre  => (X <= Big_0 and then Y >= Big_0)
+       or else (X >= Big_0 and then Y <= Big_0),
+     Post => X * Y <= Big_0;
+
+   procedure Lemma_Neg_Div (X, Y : Big_Integer)
+   with
+     Ghost,
+     Pre  => Y /= 0,
+     Post => X / Y = (-X) / (-Y);
+
+   procedure Lemma_Neg_Rem (X, Y : Big_Integer)
+   with
+     Ghost,
+     Pre  => Y /= 0,
+     Post => X rem Y = X rem (-Y);
+
+   procedure Lemma_Not_In_Range_Big2xx32
+   with
+     Post => not In_Int32_Range (Big_2xx32)
+       and then not In_Int32_Range (-Big_2xx32);
+
+   procedure Lemma_Rem_Commutation (X, Y : Uns64)
+   with
+     Ghost,
+     Pre  => Y /= 0,
+     Post => Big (X) rem Big (Y) = Big (X rem Y);
+
+   -----------------------------
+   -- Local lemma null bodies --
+   -----------------------------
+
+   procedure Lemma_Abs_Commutation (X : Int32) is null;
+   procedure Lemma_Abs_Mult_Commutation (X, Y : Big_Integer) is null;
+   procedure Lemma_Div_Commutation (X, Y : Uns64) is null;
+   procedure Lemma_Div_Ge (X, Y, Z : Big_Integer) is null;
+   procedure Lemma_Ge_Commutation (A, B : Uns32) is null;
+   procedure Lemma_Mult_Commutation (X, Y, Z : Uns64) is null;
+   procedure Lemma_Mult_Non_Negative (X, Y : Big_Integer) is null;
+   procedure Lemma_Mult_Non_Positive (X, Y : Big_Integer) is null;
+   procedure Lemma_Neg_Rem (X, Y : Big_Integer) is null;
+   procedure Lemma_Not_In_Range_Big2xx32 is null;
+   procedure Lemma_Rem_Commutation (X, Y : Uns64) is null;
+
+   -------------------------------
+   -- Lemma_Abs_Div_Commutation --
+   -------------------------------
+
+   procedure Lemma_Abs_Div_Commutation (X, Y : Big_Integer) is
+   begin
+      if Y < 0 then
+         if X < 0 then
+            pragma Assert (abs (X / Y) = abs (X / (-Y)));
+         else
+            Lemma_Neg_Div (X, Y);
+            pragma Assert (abs (X / Y) = abs ((-X) / (-Y)));
+         end if;
+      end if;
+   end Lemma_Abs_Div_Commutation;
+
+   -------------------------------
+   -- Lemma_Abs_Rem_Commutation --
+   -------------------------------
+
+   procedure Lemma_Abs_Rem_Commutation (X, Y : Big_Integer) is
+   begin
+      if Y < 0 then
+         Lemma_Neg_Rem (X, Y);
+         if X < 0 then
+            pragma Assert (X rem Y = -((-X) rem (-Y)));
+            pragma Assert (abs (X rem Y) = (abs X) rem (abs Y));
+         else
+            pragma Assert (abs (X rem Y) = (abs X) rem (abs Y));
+         end if;
+      end if;
+   end Lemma_Abs_Rem_Commutation;
+
+   -----------------
+   -- Lemma_Hi_Lo --
+   -----------------
+
+   procedure Lemma_Hi_Lo (Xu : Uns64; Xhi, Xlo : Uns32) is
+   begin
+      pragma Assert (Uns64 (Xhi) = Xu / Uns64'(2 ** 32));
+      pragma Assert (Uns64 (Xlo) = Xu mod 2 ** 32);
+   end Lemma_Hi_Lo;
+
+   -------------------
+   -- Lemma_Neg_Div --
+   -------------------
+
+   procedure Lemma_Neg_Div (X, Y : Big_Integer) is
+   begin
+      pragma Assert ((-X) / (-Y) = -(X / (-Y)));
+      pragma Assert (X / (-Y) = -(X / Y));
+   end Lemma_Neg_Div;
+
    -----------------
    -- Raise_Error --
    -----------------
@@ -79,6 +294,9 @@  package body System.Arith_32 is
    procedure Raise_Error is
    begin
       raise Constraint_Error with "32-bit arithmetic overflow";
+      pragma Annotate
+        (GNATprove, Intentional, "exception might be raised",
+         "Procedure Raise_Error is called to signal input errors");
    end Raise_Error;
 
    -------------------
@@ -101,51 +319,252 @@  package body System.Arith_32 is
       Ru : Uns32;
       --  Unsigned quotient and remainder
 
+      --  Local ghost variables
+
+      Mult  : constant Big_Integer := abs (Big (X) * Big (Y)) with Ghost;
+      Quot  : Big_Integer with Ghost;
+      Big_R : Big_Integer with Ghost;
+      Big_Q : Big_Integer with Ghost;
+
+      --  Local lemmas
+
+      procedure Prove_Negative_Dividend
+      with
+        Ghost,
+        Pre  => Z /= 0
+          and then ((X >= 0 and Y < 0) or (X < 0 and Y >= 0))
+          and then Big_Q =
+            (if Round then Round_Quotient (Big (X) * Big (Y), Big (Z),
+                                           Big (X) * Big (Y) / Big (Z),
+                                           Big (X) * Big (Y) rem Big (Z))
+             else Big (X) * Big (Y) / Big (Z)),
+         Post =>
+           (if Z > 0 then Big_Q <= Big_0 else Big_Q >= Big_0);
+      --  Proves the sign of rounded quotient when dividend is non-positive
+
+      procedure Prove_Overflow
+      with
+        Ghost,
+        Pre  => Z /= 0 and then Mult >= Big_2xx32 * Big (Uns32'(abs Z)),
+        Post => not In_Int32_Range (Big (X) * Big (Y) / Big (Z))
+          and then not In_Int32_Range
+            (Round_Quotient (Big (X) * Big (Y), Big (Z),
+                             Big (X) * Big (Y) / Big (Z),
+                             Big (X) * Big (Y) rem Big (Z)));
+      --  Proves overflow case
+
+      procedure Prove_Positive_Dividend
+      with
+        Ghost,
+        Pre  => Z /= 0
+          and then ((X >= 0 and Y >= 0) or (X < 0 and Y < 0))
+          and then Big_Q =
+            (if Round then Round_Quotient (Big (X) * Big (Y), Big (Z),
+                                           Big (X) * Big (Y) / Big (Z),
+                                           Big (X) * Big (Y) rem Big (Z))
+             else Big (X) * Big (Y) / Big (Z)),
+         Post =>
+           (if Z > 0 then Big_Q >= Big_0 else Big_Q <= Big_0);
+      --  Proves the sign of rounded quotient when dividend is non-negative
+
+      procedure Prove_Rounding_Case
+      with
+        Ghost,
+        Pre  => Z /= 0
+          and then Quot = Big (X) * Big (Y) / Big (Z)
+          and then Big_R = Big (X) * Big (Y) rem Big (Z)
+          and then Big_Q =
+            Round_Quotient (Big (X) * Big (Y), Big (Z), Quot, Big_R)
+          and then Big (Ru) = abs Big_R
+          and then Big (Zu) = Big (Uns32'(abs Z)),
+        Post => abs Big_Q =
+          (if Ru > (Zu - Uns32'(1)) / Uns32'(2)
+           then abs Quot + 1
+           else abs Quot);
+      --  Proves correctness of the rounding of the unsigned quotient
+
+      procedure Prove_Sign_R
+      with
+        Ghost,
+        Pre  => Z /= 0 and then Big_R = Big (X) * Big (Y) rem Big (Z),
+        Post => In_Int32_Range (Big_R);
+
+      procedure Prove_Signs
+      with
+        Ghost,
+        Pre  => Z /= 0
+          and then Quot = Big (X) * Big (Y) / Big (Z)
+          and then Big_R = Big (X) * Big (Y) rem Big (Z)
+          and then Big_Q =
+            (if Round then
+               Round_Quotient (Big (X) * Big (Y), Big (Z), Quot, Big_R)
+             else Quot)
+          and then Big (Ru) = abs Big_R
+          and then Big (Qu) = abs Big_Q
+          and then In_Int32_Range (Big_Q)
+          and then In_Int32_Range (Big_R)
+          and then R =
+            (if (X >= 0) = (Y >= 0) then To_Pos_Int (Ru) else To_Neg_Int (Ru))
+          and then Q =
+            (if ((X >= 0) = (Y >= 0)) = (Z >= 0) then To_Pos_Int (Qu)
+             else To_Neg_Int (Qu)),  --  need to ensure To_Pos_Int precondition
+        Post => Big (R) = Big_R and then Big (Q) = Big_Q;
+      --  Proves final signs match the intended result after the unsigned
+      --  division is done.
+
+      -----------------------------
+      -- Prove_Negative_Dividend --
+      -----------------------------
+
+      procedure Prove_Negative_Dividend is
+      begin
+         Lemma_Mult_Non_Positive (Big (X), Big (Y));
+      end Prove_Negative_Dividend;
+
+      --------------------
+      -- Prove_Overflow --
+      --------------------
+
+      procedure Prove_Overflow is
+      begin
+         Lemma_Div_Ge (Mult, Big_2xx32, Big (Uns32'(abs Z)));
+         Lemma_Abs_Commutation (Z);
+         Lemma_Abs_Div_Commutation (Big (X) * Big (Y), Big (Z));
+      end Prove_Overflow;
+
+      -----------------------------
+      -- Prove_Positive_Dividend --
+      -----------------------------
+
+      procedure Prove_Positive_Dividend is
+      begin
+         Lemma_Mult_Non_Negative (Big (X), Big (Y));
+      end Prove_Positive_Dividend;
+
+      -------------------------
+      -- Prove_Rounding_Case --
+      -------------------------
+
+      procedure Prove_Rounding_Case is
+      begin
+         if Same_Sign (Big (X) * Big (Y), Big (Z)) then
+            null;
+         end if;
+      end Prove_Rounding_Case;
+
+      ------------------
+      -- Prove_Sign_R --
+      ------------------
+
+      procedure Prove_Sign_R is
+      begin
+         pragma Assert (In_Int32_Range (Big (Z)));
+      end Prove_Sign_R;
+
+      -----------------
+      -- Prove_Signs --
+      -----------------
+
+      procedure Prove_Signs is null;
+
+   --  Start of processing for Scaled_Divide32
+
    begin
       --  First do the 64-bit multiplication
 
       D := Uns64 (Xu) * Uns64 (Yu);
 
+      pragma Assert (Mult = Big (D));
+      Lemma_Hi_Lo (D, Hi (D), Lo (D));
+      pragma Assert (Mult = Big_2xx32 * Big (Hi (D)) + Big (Lo (D)));
+
+      --  If divisor is zero, raise error
+
+      if Z = 0 then
+         Raise_Error;
+      end if;
+
+      Quot := Big (X) * Big (Y) / Big (Z);
+      Big_R := Big (X) * Big (Y) rem Big (Z);
+      if Round then
+         Big_Q := Round_Quotient (Big (X) * Big (Y), Big (Z), Quot, Big_R);
+      else
+         Big_Q := Quot;
+      end if;
+
       --  If dividend is too large, raise error
 
       if Hi (D) >= Zu then
+         Lemma_Ge_Commutation (Hi (D), Zu);
+         pragma Assert (Mult >= Big_2xx32 * Big (Zu));
+         Prove_Overflow;
          Raise_Error;
+      end if;
 
       --  Then do the 64-bit division
 
-      else
-         Qu := Uns32 (D / Uns64 (Zu));
-         Ru := Uns32 (D rem Uns64 (Zu));
-      end if;
+      Qu := Uns32 (D / Uns64 (Zu));
+      Ru := Uns32 (D rem Uns64 (Zu));
+
+      Lemma_Abs_Div_Commutation (Big (X) * Big (Y), Big (Z));
+      Lemma_Abs_Rem_Commutation (Big (X) * Big (Y), Big (Z));
+      Lemma_Abs_Mult_Commutation (Big (X), Big (Y));
+      Lemma_Abs_Commutation (X);
+      Lemma_Abs_Commutation (Y);
+      Lemma_Abs_Commutation (Z);
+      Lemma_Mult_Commutation (Uns64 (Xu), Uns64 (Yu), D);
+      Lemma_Div_Commutation (D, Uns64 (Zu));
+      Lemma_Rem_Commutation (D, Uns64 (Zu));
+
+      pragma Assert (Big (Ru) = abs Big_R);
+      pragma Assert (Big (Qu) = abs Quot);
+      pragma Assert (Big (Zu) = Big (Uns32'(abs Z)));
 
       --  Deal with rounding case
 
-      if Round and then Ru > (Zu - Uns32'(1)) / Uns32'(2) then
+      if Round then
+         Prove_Rounding_Case;
 
-         --  Protect against wrapping around when rounding, by signaling
-         --  an overflow when the quotient is too large.
+         if Ru > (Zu - Uns32'(1)) / Uns32'(2) then
+            pragma Assert (abs Big_Q = Big (Qu) + 1);
 
-         if Qu = Uns32'Last then
-            Raise_Error;
-         end if;
+            --  Protect against wrapping around when rounding, by signaling
+            --  an overflow when the quotient is too large.
 
-         Qu := Qu + Uns32'(1);
+            if Qu = Uns32'Last then
+               pragma Assert (abs Big_Q = Big_2xx32);
+               Lemma_Not_In_Range_Big2xx32;
+               Raise_Error;
+            end if;
+
+            Qu := Qu + Uns32'(1);
+         end if;
       end if;
 
+      pragma Assert (Big (Qu) = abs Big_Q);
+      pragma Assert (Big (Ru) = abs Big_R);
+
       --  Set final signs (RM 4.5.5(27-30))
 
       --  Case of dividend (X * Y) sign positive
 
       if (X >= 0 and then Y >= 0) or else (X < 0 and then Y < 0) then
+         Prove_Positive_Dividend;
+
          R := To_Pos_Int (Ru);
          Q := (if Z > 0 then To_Pos_Int (Qu) else To_Neg_Int (Qu));
 
       --  Case of dividend (X * Y) sign negative
 
       else
+         Prove_Negative_Dividend;
+
          R := To_Neg_Int (Ru);
          Q := (if Z > 0 then To_Neg_Int (Qu) else To_Pos_Int (Qu));
       end if;
+
+      Prove_Sign_R;
+      Prove_Signs;
    end Scaled_Divide32;
 
    ----------------


diff --git a/gcc/ada/libgnat/s-arit32.ads b/gcc/ada/libgnat/s-arit32.ads
--- a/gcc/ada/libgnat/s-arit32.ads
+++ b/gcc/ada/libgnat/s-arit32.ads
@@ -33,17 +33,79 @@ 
 --  signed integer values in cases where either overflow checking is
 --  required, or intermediate results are longer than 32 bits.
 
+--  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);
+
 with Interfaces;
+with Ada.Numerics.Big_Numbers.Big_Integers_Ghost;
 
-package System.Arith_32 is
-   pragma Pure;
+package System.Arith_32
+  with Pure, SPARK_Mode
+is
+   use type Ada.Numerics.Big_Numbers.Big_Integers_Ghost.Big_Integer;
+   use type Interfaces.Integer_32;
 
    subtype Int32 is Interfaces.Integer_32;
 
+   subtype Big_Integer is
+     Ada.Numerics.Big_Numbers.Big_Integers_Ghost.Big_Integer
+   with Ghost;
+
+   package Signed_Conversion is new
+     Ada.Numerics.Big_Numbers.Big_Integers_Ghost.Signed_Conversions
+     (Int => Int32);
+
+   function Big (Arg : Int32) return Big_Integer is
+     (Signed_Conversion.To_Big_Integer (Arg))
+   with Ghost;
+
+   function In_Int32_Range (Arg : Big_Integer) return Boolean is
+     (Ada.Numerics.Big_Numbers.Big_Integers_Ghost.In_Range
+       (Arg, Big (Int32'First), Big (Int32'Last)))
+   with Ghost;
+
+   function Same_Sign (X, Y : Big_Integer) return Boolean is
+     (X = Big (Int32'(0))
+        or else Y = Big (Int32'(0))
+        or else (X < Big (Int32'(0))) = (Y < Big (Int32'(0))))
+   with Ghost;
+
+   function Round_Quotient (X, Y, Q, R : Big_Integer) return Big_Integer is
+     (if abs R > (abs Y - Big (Int32'(1))) / Big (Int32'(2)) then
+       (if Same_Sign (X, Y) then Q + Big (Int32'(1))
+        else Q - Big (Int32'(1)))
+      else
+        Q)
+   with
+     Ghost,
+     Pre => Y /= 0 and then Q = X / Y and then R = X rem Y;
+
    procedure Scaled_Divide32
      (X, Y, Z : Int32;
       Q, R    : out Int32;
-      Round   : Boolean);
+      Round   : Boolean)
+   with
+     Pre  => Z /= 0
+       and then In_Int32_Range
+         (if Round then Round_Quotient (Big (X) * Big (Y), Big (Z),
+                                        Big (X) * Big (Y) / Big (Z),
+                                        Big (X) * Big (Y) rem Big (Z))
+          else Big (X) * Big (Y) / Big (Z)),
+     Post => Big (R) = Big (X) * Big (Y) rem Big (Z)
+       and then
+         (if Round then
+            Big (Q) = Round_Quotient (Big (X) * Big (Y), Big (Z),
+                                      Big (X) * Big (Y) / Big (Z), Big (R))
+          else
+            Big (Q) = Big (X) * Big (Y) / Big (Z));
    --  Performs the division of (X * Y) / Z, storing the quotient in Q
    --  and the remainder in R. Constraint_Error is raised if Z is zero,
    --  or if the quotient does not fit in 32 bits. Round indicates if