gcc/ada/libgnat/s-aridou.adb

   1 ------------------------------------------------------------------------------
   2 --                                                                          --
   3 --                         GNAT RUN-TIME COMPONENTS                         --
   4 --                                                                          --
   5 --                  S Y S T E M . A R I T H _ D O U B L E                   --
   6 --                                                                          --
   7 --                                 B o d y                                  --
   8 --                                                                          --
   9 --          Copyright (C) 1992-2023, Free Software Foundation, Inc.         --
  10 --                                                                          --
  11 -- GNAT is free software;  you can  redistribute it  and/or modify it under --
  12 -- terms of the  GNU General Public License as published  by the Free Soft- --
  13 -- ware  Foundation;  either version 3,  or (at your option) any later ver- --
  14 -- sion.  GNAT is distributed in the hope that it will be useful, but WITH- --
  15 -- OUT ANY WARRANTY;  without even the  implied warranty of MERCHANTABILITY --
  16 -- or FITNESS FOR A PARTICULAR PURPOSE.                                     --
  17 --                                                                          --
  18 -- As a special exception under Section 7 of GPL version 3, you are granted --
  19 -- additional permissions described in the GCC Runtime Library Exception,   --
  20 -- version 3.1, as published by the Free Software Foundation.               --
  21 --                                                                          --
  22 -- You should have received a copy of the GNU General Public License and    --
  23 -- a copy of the GCC Runtime Library Exception along with this program;     --
  24 -- see the files COPYING3 and COPYING.RUNTIME respectively.  If not, see    --
  25 -- <http://www.gnu.org/licenses/>.                                          --
  26 --                                                                          --
  27 -- GNAT was originally developed  by the GNAT team at  New York University. --
  28 -- Extensive contributions were provided by Ada Core Technologies Inc.      --
  29 --                                                                          --
  30 ------------------------------------------------------------------------------
  31
  32 with Ada.Unchecked_Conversion;
  33 with System.SPARK.Cut_Operations; use System.SPARK.Cut_Operations;
  34
  35 package body System.Arith_Double
  36   with SPARK_Mode
  37 is
  38    --  Contracts, ghost code, loop invariants and assertions in this unit are
  39    --  meant for analysis only, not for run-time checking, as it would be too
  40    --  costly otherwise. This is enforced by setting the assertion policy to
  41    --  Ignore.
  42
  43    pragma Assertion_Policy (Pre            => Ignore,
  44                             Post           => Ignore,
  45                             Contract_Cases => Ignore,
  46                             Ghost          => Ignore,
  47                             Loop_Invariant => Ignore,
  48                             Assert         => Ignore);
  49
  50    pragma Suppress (Overflow_Check);
  51    pragma Suppress (Range_Check);
  52
  53    function To_Uns is new Ada.Unchecked_Conversion (Double_Int, Double_Uns);
  54    function To_Int is new Ada.Unchecked_Conversion (Double_Uns, Double_Int);
  55
  56    Double_Size : constant Natural := Double_Int'Size;
  57    Single_Size : constant Natural := Double_Int'Size / 2;
  58
  59    --  Log of Single_Size in base 2, so that Single_Size = 2 ** Log_Single_Size
  60    Log_Single_Size : constant Natural :=
  61      (case Single_Size is
  62         when 32  => 5,
  63         when 64  => 6,
  64         when 128 => 7,
  65         when others => raise Program_Error)
  66    with Ghost;
  67
  68    --  Power-of-two constants
  69
  70    pragma Warnings
  71      (Off, "non-preelaborable call not allowed in preelaborated unit",
  72       Reason => "Ghost code is not compiled");
  73    pragma Warnings
  74      (Off, "non-static constant in preelaborated unit",
  75       Reason => "Ghost code is not compiled");
  76    Big_0 : constant Big_Integer :=
  77      Big (Double_Uns'(0))
  78    with Ghost;
  79    Big_2xxSingle : constant Big_Integer :=
  80      Big (Double_Int'(2 ** Single_Size))
  81    with Ghost;
  82    Big_2xxDouble_Minus_1 : constant Big_Integer :=
  83      Big (Double_Uns'(2 ** (Double_Size - 1)))
  84    with Ghost;
  85    Big_2xxDouble : constant Big_Integer :=
  86      Big (Double_Uns'(2 ** Double_Size - 1)) + 1
  87    with Ghost;
  88    pragma Warnings
  89      (On, "non-preelaborable call not allowed in preelaborated unit");
  90    pragma Warnings (On, "non-static constant in preelaborated unit");
  91
  92    -----------------------
  93    -- Local Subprograms --
  94    -----------------------
  95
  96    function "+" (A, B : Single_Uns) return Double_Uns is
  97      (Double_Uns (A) + Double_Uns (B));
  98    function "+" (A : Double_Uns; B : Single_Uns) return Double_Uns is
  99      (A + Double_Uns (B));
 100    --  Length doubling additions
 101
 102    function "*" (A, B : Single_Uns) return Double_Uns is
 103      (Double_Uns (A) * Double_Uns (B));
 104    --  Length doubling multiplication
 105
 106    function "/" (A : Double_Uns; B : Single_Uns) return Double_Uns is
 107      (A / Double_Uns (B))
 108    with
 109      Pre => B /= 0;
 110    --  Length doubling division
 111
 112    function "&" (Hi, Lo : Single_Uns) return Double_Uns is
 113      (Shift_Left (Double_Uns (Hi), Single_Size) or Double_Uns (Lo));
 114    --  Concatenate hi, lo values to form double result
 115
 116    function "abs" (X : Double_Int) return Double_Uns is
 117      (if X = Double_Int'First
 118       then Double_Uns'(2 ** (Double_Size - 1))
 119       else Double_Uns (Double_Int'(abs X)));
 120    --  Convert absolute value of X to unsigned. Note that we can't just use
 121    --  the expression of the Else since it overflows for X = Double_Int'First.
 122
 123    function "rem" (A : Double_Uns; B : Single_Uns) return Double_Uns is
 124      (A rem Double_Uns (B))
 125    with
 126      Pre => B /= 0;
 127    --  Length doubling remainder
 128
 129    function Big_2xx (N : Natural) return Big_Positive is
 130      (Big (Double_Uns'(2 ** N)))
 131    with
 132      Ghost,
 133      Pre  => N < Double_Size,
 134      Post => Big_2xx'Result > 0;
 135    --  2**N as a big integer
 136
 137    function Big3 (X1, X2, X3 : Single_Uns) return Big_Natural is
 138      (Big_2xxSingle * Big_2xxSingle * Big (Double_Uns (X1))
 139                     + Big_2xxSingle * Big (Double_Uns (X2))
 140                                     + Big (Double_Uns (X3)))
 141    with Ghost;
 142    --  X1&X2&X3 as a big integer
 143
 144    function Big3 (X1, X2, X3 : Big_Integer) return Big_Integer is
 145      (Big_2xxSingle * Big_2xxSingle * X1
 146                     + Big_2xxSingle * X2
 147                                     + X3)
 148    with Ghost;
 149    --  Version of Big3 on big integers
 150
 151    function Le3 (X1, X2, X3, Y1, Y2, Y3 : Single_Uns) return Boolean
 152    with
 153      Post => Le3'Result = (Big3 (X1, X2, X3) <= Big3 (Y1, Y2, Y3));
 154    --  Determines if (3 * Single_Size)-bit value X1&X2&X3 <= Y1&Y2&Y3
 155
 156    function Lo (A : Double_Uns) return Single_Uns is
 157      (Single_Uns (A and (2 ** Single_Size - 1)));
 158    --  Low order half of double value
 159
 160    function Hi (A : Double_Uns) return Single_Uns is
 161      (Single_Uns (Shift_Right (A, Single_Size)));
 162    --  High order half of double value
 163
 164    procedure Sub3 (X1, X2, X3 : in out Single_Uns; Y1, Y2, Y3 : Single_Uns)
 165    with
 166      Pre  => Big3 (X1, X2, X3) >= Big3 (Y1, Y2, Y3),
 167      Post => Big3 (X1, X2, X3) = Big3 (X1, X2, X3)'Old - Big3 (Y1, Y2, Y3);
 168    --  Computes X1&X2&X3 := X1&X2&X3 - Y1&Y1&Y3 mod 2 ** (3 * Single_Size)
 169
 170    function To_Neg_Int (A : Double_Uns) return Double_Int
 171    with
 172      Annotate => (GNATprove, Always_Return),
 173      Pre      => In_Double_Int_Range (-Big (A)),
 174      Post     => Big (To_Neg_Int'Result) = -Big (A);
 175    --  Convert to negative integer equivalent. If the input is in the range
 176    --  0 .. 2 ** (Double_Size - 1), then the corresponding nonpositive signed
 177    --  integer (obtained by negating the given value) is returned, otherwise
 178    --  constraint error is raised.
 179
 180    function To_Pos_Int (A : Double_Uns) return Double_Int
 181    with
 182      Annotate => (GNATprove, Always_Return),
 183      Pre      => In_Double_Int_Range (Big (A)),
 184      Post     => Big (To_Pos_Int'Result) = Big (A);
 185    --  Convert to positive integer equivalent. If the input is in the range
 186    --  0 .. 2 ** (Double_Size - 1) - 1, then the corresponding non-negative
 187    --  signed integer is returned, otherwise constraint error is raised.
 188
 189    procedure Raise_Error;
 190    pragma No_Return (Raise_Error);
 191    --  Raise constraint error with appropriate message
 192
 193    ------------------
 194    -- Local Lemmas --
 195    ------------------
 196
 197    procedure Inline_Le3 (X1, X2, X3, Y1, Y2, Y3 : Single_Uns)
 198    with
 199      Ghost,
 200      Pre  => Le3 (X1, X2, X3, Y1, Y2, Y3),
 201      Post => Big3 (X1, X2, X3) <= Big3 (Y1, Y2, Y3);
 202
 203    procedure Lemma_Abs_Commutation (X : Double_Int)
 204    with
 205      Ghost,
 206      Post => abs (Big (X)) = Big (Double_Uns'(abs X));
 207
 208    procedure Lemma_Abs_Div_Commutation (X, Y : Big_Integer)
 209    with
 210      Ghost,
 211      Pre  => Y /= 0,
 212      Post => abs (X / Y) = abs X / abs Y;
 213
 214    procedure Lemma_Abs_Mult_Commutation (X, Y : Big_Integer)
 215    with
 216      Ghost,
 217      Post => abs (X * Y) = abs X * abs Y;
 218
 219    procedure Lemma_Abs_Range (X : Big_Integer)
 220    with
 221      Ghost,
 222      Pre  => In_Double_Int_Range (X),
 223      Post => abs (X) <= Big_2xxDouble_Minus_1
 224        and then In_Double_Int_Range (-abs (X));
 225
 226    procedure Lemma_Abs_Rem_Commutation (X, Y : Big_Integer)
 227    with
 228      Ghost,
 229      Pre  => Y /= 0,
 230      Post => abs (X rem Y) = (abs X) rem (abs Y);
 231
 232    procedure Lemma_Add_Commutation (X : Double_Uns; Y : Single_Uns)
 233    with
 234      Ghost,
 235      Pre  => X <= 2 ** Double_Size - 2 ** Single_Size,
 236      Post => Big (X) + Big (Double_Uns (Y)) = Big (X + Double_Uns (Y));
 237
 238    procedure Lemma_Add_One (X : Double_Uns)
 239    with
 240      Ghost,
 241      Pre  => X /= Double_Uns'Last,
 242      Post => Big (X + Double_Uns'(1)) = Big (X) + 1;
 243
 244    procedure Lemma_Big_Of_Double_Uns (X : Double_Uns)
 245    with
 246      Ghost,
 247      Post => Big (X) < Big_2xxDouble;
 248
 249    procedure Lemma_Big_Of_Double_Uns_Of_Single_Uns (X : Single_Uns)
 250    with
 251      Ghost,
 252      Post => Big (Double_Uns (X)) >= 0
 253        and then Big (Double_Uns (X)) < Big_2xxSingle;
 254
 255    procedure Lemma_Bounded_Powers_Of_2_Increasing (M, N : Natural)
 256    with
 257      Ghost,
 258      Pre  => M < N and then N < Double_Size,
 259      Post => Double_Uns'(2)**M < Double_Uns'(2)**N;
 260
 261    procedure Lemma_Concat_Definition (X, Y : Single_Uns)
 262    with
 263      Ghost,
 264      Post => Big (X & Y) = Big_2xxSingle * Big (Double_Uns (X))
 265                                          + Big (Double_Uns (Y));
 266
 267    procedure Lemma_Deep_Mult_Commutation
 268      (Factor : Big_Integer;
 269       X, Y   : Single_Uns)
 270    with
 271      Ghost,
 272      Post =>
 273        Factor * Big (Double_Uns (X)) * Big (Double_Uns (Y)) =
 274          Factor * Big (Double_Uns (X) * Double_Uns (Y));
 275
 276    procedure Lemma_Div_Commutation (X, Y : Double_Uns)
 277    with
 278      Ghost,
 279      Pre  => Y /= 0,
 280      Post => Big (X) / Big (Y) = Big (X / Y);
 281
 282    procedure Lemma_Div_Definition
 283      (A : Double_Uns;
 284       B : Single_Uns;
 285       Q : Double_Uns;
 286       R : Double_Uns)
 287    with
 288      Ghost,
 289      Pre  => B /= 0 and then Q = A / B and then R = A rem B,
 290      Post => Big (A) = Big (Double_Uns (B)) * Big (Q) + Big (R);
 291
 292    procedure Lemma_Div_Ge (X, Y, Z : Big_Integer)
 293    with
 294      Ghost,
 295      Pre  => Z > 0 and then X >= Y * Z,
 296      Post => X / Z >= Y;
 297
 298    procedure Lemma_Div_Lt (X, Y, Z : Big_Natural)
 299    with
 300      Ghost,
 301      Pre  => Z > 0 and then X < Y * Z,
 302      Post => X / Z < Y;
 303
 304    procedure Lemma_Div_Eq (A, B, S, R : Big_Integer)
 305    with
 306      Ghost,
 307      Pre  => A * S = B * S + R and then S /= 0,
 308      Post => A = B + R / S;
 309
 310    procedure Lemma_Double_Big_2xxSingle
 311    with
 312      Ghost,
 313      Post => Big_2xxSingle * Big_2xxSingle = Big_2xxDouble;
 314
 315    procedure Lemma_Double_Shift (X : Double_Uns; S, S1 : Double_Uns)
 316    with
 317      Ghost,
 318      Pre  => S <= Double_Uns (Double_Size)
 319        and then S1 <= Double_Uns (Double_Size),
 320      Post => Shift_Left (Shift_Left (X, Natural (S)), Natural (S1)) =
 321              Shift_Left (X, Natural (S + S1));
 322
 323    procedure Lemma_Double_Shift (X : Single_Uns; S, S1 : Natural)
 324    with
 325      Ghost,
 326      Pre  => S <= Single_Size - S1,
 327      Post => Shift_Left (Shift_Left (X, S), S1) = Shift_Left (X, S + S1);
 328
 329    procedure Lemma_Double_Shift (X : Double_Uns; S, S1 : Natural)
 330    with
 331      Ghost,
 332      Pre  => S <= Double_Size - S1,
 333      Post => Shift_Left (Shift_Left (X, S), S1) = Shift_Left (X, S + S1);
 334
 335    procedure Lemma_Double_Shift_Left (X : Double_Uns; S, S1 : Double_Uns)
 336    with
 337      Ghost,
 338      Pre  => S <= Double_Uns (Double_Size)
 339        and then S1 <= Double_Uns (Double_Size),
 340      Post => Shift_Left (Shift_Left (X, Natural (S)), Natural (S1)) =
 341              Shift_Left (X, Natural (S + S1));
 342
 343    procedure Lemma_Double_Shift_Left (X : Double_Uns; S, S1 : Natural)
 344    with
 345      Ghost,
 346      Pre  => S <= Double_Size - S1,
 347      Post => Shift_Left (Shift_Left (X, S), S1) = Shift_Left (X, S + S1);
 348
 349    procedure Lemma_Double_Shift_Right (X : Double_Uns; S, S1 : Double_Uns)
 350    with
 351      Ghost,
 352      Pre  => S <= Double_Uns (Double_Size)
 353        and then S1 <= Double_Uns (Double_Size),
 354      Post => Shift_Right (Shift_Right (X, Natural (S)), Natural (S1)) =
 355              Shift_Right (X, Natural (S + S1));
 356
 357    procedure Lemma_Double_Shift_Right (X : Double_Uns; S, S1 : Natural)
 358    with
 359      Ghost,
 360      Pre  => S <= Double_Size - S1,
 361      Post => Shift_Right (Shift_Right (X, S), S1) = Shift_Right (X, S + S1);
 362
 363    procedure Lemma_Ge_Commutation (A, B : Double_Uns)
 364    with
 365      Ghost,
 366      Pre  => A >= B,
 367      Post => Big (A) >= Big (B);
 368
 369    procedure Lemma_Ge_Mult (A, B, C, D : Big_Integer)
 370    with
 371      Ghost,
 372      Pre  => A >= B and then B * C >= D and then C > 0,
 373      Post => A * C >= D;
 374
 375    procedure Lemma_Gt_Commutation (A, B : Double_Uns)
 376    with
 377      Ghost,
 378      Pre  => A > B,
 379      Post => Big (A) > Big (B);
 380
 381    procedure Lemma_Gt_Mult (A, B, C, D : Big_Integer)
 382    with
 383      Ghost,
 384      Pre  => A >= B and then B * C > D and then C > 0,
 385      Post => A * C > D;
 386
 387    procedure Lemma_Hi_Lo (Xu : Double_Uns; Xhi, Xlo : Single_Uns)
 388    with
 389      Ghost,
 390      Pre  => Xhi = Hi (Xu) and Xlo = Lo (Xu),
 391      Post => Big (Xu) =
 392        Big_2xxSingle * Big (Double_Uns (Xhi)) + Big (Double_Uns (Xlo));
 393
 394    procedure Lemma_Hi_Lo_3 (Xu : Double_Uns; Xhi, Xlo : Single_Uns)
 395    with
 396      Ghost,
 397      Pre  => Xhi = Hi (Xu) and then Xlo = Lo (Xu),
 398      Post => Big (Xu) = Big3 (0, Xhi, Xlo);
 399
 400    procedure Lemma_Lo_Is_Ident (X : Double_Uns)
 401    with
 402      Ghost,
 403      Pre  => Big (X) < Big_2xxSingle,
 404      Post => Double_Uns (Lo (X)) = X;
 405
 406    procedure Lemma_Lt_Commutation (A, B : Double_Uns)
 407    with
 408      Ghost,
 409      Pre  => A < B,
 410      Post => Big (A) < Big (B);
 411
 412    procedure Lemma_Lt_Mult (A, B, C, D : Big_Integer)
 413    with
 414      Ghost,
 415      Pre  => A < B and then B * C <= D and then C > 0,
 416      Post => A * C < D;
 417
 418    procedure Lemma_Mult_Commutation (X, Y : Single_Uns)
 419    with
 420      Ghost,
 421      Post =>
 422        Big (Double_Uns (X)) * Big (Double_Uns (Y)) =
 423          Big (Double_Uns (X) * Double_Uns (Y));
 424
 425    procedure Lemma_Mult_Commutation (X, Y : Double_Int)
 426    with
 427      Ghost,
 428      Pre  => In_Double_Int_Range (Big (X) * Big (Y)),
 429      Post => Big (X) * Big (Y) = Big (X * Y);
 430
 431    procedure Lemma_Mult_Commutation (X, Y, Z : Double_Uns)
 432    with
 433      Ghost,
 434      Pre  => Big (X) * Big (Y) < Big_2xxDouble and then Z = X * Y,
 435      Post => Big (X) * Big (Y) = Big (Z);
 436
 437    procedure Lemma_Mult_Decomposition
 438      (Mult               : Big_Integer;
 439       Xu, Yu             : Double_Uns;
 440       Xhi, Xlo, Yhi, Ylo : Single_Uns)
 441    with
 442      Ghost,
 443      Pre  => Mult = Big (Xu) * Big (Yu)
 444        and then Xhi = Hi (Xu)
 445        and then Xlo = Lo (Xu)
 446        and then Yhi = Hi (Yu)
 447        and then Ylo = Lo (Yu),
 448      Post => Mult =
 449        Big_2xxSingle * Big_2xxSingle * (Big (Double_Uns'(Xhi * Yhi)))
 450                      + Big_2xxSingle * (Big (Double_Uns'(Xhi * Ylo)))
 451                      + Big_2xxSingle * (Big (Double_Uns'(Xlo * Yhi)))
 452                                      + (Big (Double_Uns'(Xlo * Ylo)));
 453
 454    procedure Lemma_Mult_Distribution (X, Y, Z : Big_Integer)
 455    with
 456      Ghost,
 457      Post => X * (Y + Z) = X * Y + X * Z;
 458
 459    procedure Lemma_Mult_Div (A, B : Big_Integer)
 460    with
 461      Ghost,
 462      Pre  => B /= 0,
 463      Post => A * B / B = A;
 464
 465    procedure Lemma_Mult_Non_Negative (X, Y : Big_Integer)
 466    with
 467      Ghost,
 468      Pre  => (X >= 0 and then Y >= 0)
 469        or else (X <= 0 and then Y <= 0),
 470      Post => X * Y >= 0;
 471
 472    procedure Lemma_Mult_Non_Positive (X, Y : Big_Integer)
 473    with
 474      Ghost,
 475      Pre  => (X <= Big_0 and then Y >= Big_0)
 476        or else (X >= Big_0 and then Y <= Big_0),
 477      Post => X * Y <= Big_0;
 478
 479    procedure Lemma_Mult_Positive (X, Y : Big_Integer)
 480    with
 481      Ghost,
 482      Pre  => (X > Big_0 and then Y > Big_0)
 483        or else (X < Big_0 and then Y < Big_0),
 484      Post => X * Y > Big_0;
 485
 486    procedure Lemma_Neg_Div (X, Y : Big_Integer)
 487    with
 488      Ghost,
 489      Pre  => Y /= 0,
 490      Post => X / Y = (-X) / (-Y);
 491
 492    procedure Lemma_Neg_Rem (X, Y : Big_Integer)
 493    with
 494      Ghost,
 495      Pre  => Y /= 0,
 496      Post => X rem Y = X rem (-Y);
 497
 498    procedure Lemma_Not_In_Range_Big2xx64
 499    with
 500      Post => not In_Double_Int_Range (Big_2xxDouble)
 501        and then not In_Double_Int_Range (-Big_2xxDouble);
 502
 503    procedure Lemma_Powers (A : Big_Natural; B, C : Natural)
 504    with
 505      Ghost,
 506      Pre  => B <= Natural'Last - C,
 507      Post => A**B * A**C = A**(B + C);
 508
 509    procedure Lemma_Powers_Of_2 (M, N : Natural)
 510    with
 511      Ghost,
 512      Pre  => M < Double_Size
 513        and then N < Double_Size
 514        and then M + N <= Double_Size,
 515      Post =>
 516        Big_2xx (M) * Big_2xx (N) =
 517          (if M + N = Double_Size then Big_2xxDouble else Big_2xx (M + N));
 518
 519    procedure Lemma_Powers_Of_2_Commutation (M : Natural)
 520    with
 521      Ghost,
 522      Subprogram_Variant => (Decreases => M),
 523      Pre  => M <= Double_Size,
 524      Post => Big (Double_Uns'(2))**M =
 525               (if M < Double_Size then Big_2xx (M) else Big_2xxDouble);
 526
 527    procedure Lemma_Powers_Of_2_Increasing (M, N : Natural)
 528    with
 529      Ghost,
 530      Subprogram_Variant => (Increases => M),
 531      Pre  => M < N,
 532      Post => Big (Double_Uns'(2))**M < Big (Double_Uns'(2))**N;
 533
 534    procedure Lemma_Rem_Abs (X, Y : Big_Integer)
 535    with
 536      Ghost,
 537      Pre  => Y /= 0,
 538      Post => X rem Y = X rem (abs Y);
 539    pragma Unreferenced (Lemma_Rem_Abs);
 540
 541    procedure Lemma_Rem_Commutation (X, Y : Double_Uns)
 542    with
 543      Ghost,
 544      Pre  => Y /= 0,
 545      Post => Big (X) rem Big (Y) = Big (X rem Y);
 546
 547    procedure Lemma_Rem_Is_Ident (X, Y : Big_Integer)
 548    with
 549      Ghost,
 550      Pre  => abs X < abs Y,
 551      Post => X rem Y = X;
 552    pragma Unreferenced (Lemma_Rem_Is_Ident);
 553
 554    procedure Lemma_Rem_Sign (X, Y : Big_Integer)
 555    with
 556      Ghost,
 557      Pre  => Y /= 0,
 558      Post => Same_Sign (X rem Y, X);
 559    pragma Unreferenced (Lemma_Rem_Sign);
 560
 561    procedure Lemma_Rev_Div_Definition (A, B, Q, R : Big_Natural)
 562    with
 563      Ghost,
 564      Pre  => A = B * Q + R and then R < B,
 565      Post => Q = A / B and then R = A rem B;
 566
 567    procedure Lemma_Shift_Left (X : Double_Uns; Shift : Natural)
 568    with
 569      Ghost,
 570      Pre  => Shift < Double_Size
 571        and then Big (X) * Big_2xx (Shift) < Big_2xxDouble,
 572      Post => Big (Shift_Left (X, Shift)) = Big (X) * Big_2xx (Shift);
 573
 574    procedure Lemma_Shift_Right (X : Double_Uns; Shift : Natural)
 575    with
 576      Ghost,
 577      Pre  => Shift < Double_Size,
 578      Post => Big (Shift_Right (X, Shift)) = Big (X) / Big_2xx (Shift);
 579
 580    procedure Lemma_Shift_Without_Drop
 581      (X, Y  : Double_Uns;
 582       Mask  : Single_Uns;
 583       Shift : Natural)
 584    with
 585      Ghost,
 586      Pre  => (Hi (X) and Mask) = 0  --  X has the first Shift bits off
 587        and then Shift <= Single_Size
 588        and then Mask = Shift_Left (Single_Uns'Last, Single_Size - Shift)
 589        and then Y = Shift_Left (X, Shift),
 590      Post => Big (Y) = Big_2xx (Shift) * Big (X);
 591
 592    procedure Lemma_Simplify (X, Y : Big_Integer)
 593    with
 594      Ghost,
 595      Pre  => Y /= 0,
 596      Post => X * Y / Y = X;
 597
 598    procedure Lemma_Substitution (A, B, C, C1, D : Big_Integer)
 599    with
 600      Ghost,
 601      Pre  => C = C1 and then A = B * C + D,
 602      Post => A = B * C1 + D;
 603
 604    procedure Lemma_Subtract_Commutation (X, Y : Double_Uns)
 605    with
 606      Ghost,
 607      Pre  => X >= Y,
 608      Post => Big (X) - Big (Y) = Big (X - Y);
 609
 610    procedure Lemma_Subtract_Double_Uns (X, Y : Double_Int)
 611    with
 612      Ghost,
 613      Pre  => X >= 0 and then X <= Y,
 614      Post => Double_Uns (Y - X) = Double_Uns (Y) - Double_Uns (X);
 615
 616    procedure Lemma_Word_Commutation (X : Single_Uns)
 617    with
 618      Ghost,
 619      Post => Big_2xxSingle * Big (Double_Uns (X))
 620        = Big (2**Single_Size * Double_Uns (X));
 621
 622    -----------------------------
 623    -- Local lemma null bodies --
 624    -----------------------------
 625
 626    procedure Inline_Le3 (X1, X2, X3, Y1, Y2, Y3 : Single_Uns) is null;
 627    procedure Lemma_Abs_Commutation (X : Double_Int) is null;
 628    procedure Lemma_Abs_Mult_Commutation (X, Y : Big_Integer) is null;
 629    procedure Lemma_Abs_Range (X : Big_Integer) is null;
 630    procedure Lemma_Add_Commutation (X : Double_Uns; Y : Single_Uns) is null;
 631    procedure Lemma_Add_One (X : Double_Uns) is null;
 632    procedure Lemma_Big_Of_Double_Uns (X : Double_Uns) is null;
 633    procedure Lemma_Big_Of_Double_Uns_Of_Single_Uns (X : Single_Uns) is null;
 634    procedure Lemma_Bounded_Powers_Of_2_Increasing (M, N : Natural) is null;
 635    procedure Lemma_Deep_Mult_Commutation
 636      (Factor : Big_Integer;
 637       X, Y   : Single_Uns)
 638    is null;
 639    procedure Lemma_Div_Commutation (X, Y : Double_Uns) is null;
 640    procedure Lemma_Div_Definition
 641      (A : Double_Uns;
 642       B : Single_Uns;
 643       Q : Double_Uns;
 644       R : Double_Uns)
 645    is null;
 646    procedure Lemma_Div_Ge (X, Y, Z : Big_Integer) is null;
 647    procedure Lemma_Div_Lt (X, Y, Z : Big_Natural) is null;
 648    procedure Lemma_Double_Big_2xxSingle is null;
 649    procedure Lemma_Double_Shift (X : Double_Uns; S, S1 : Double_Uns) is null;
 650    procedure Lemma_Double_Shift (X : Single_Uns; S, S1 : Natural) is null;
 651    procedure Lemma_Double_Shift_Left (X : Double_Uns; S, S1 : Double_Uns)
 652    is null;
 653    procedure Lemma_Double_Shift_Right (X : Double_Uns; S, S1 : Double_Uns)
 654    is null;
 655    procedure Lemma_Ge_Commutation (A, B : Double_Uns) is null;
 656    procedure Lemma_Ge_Mult (A, B, C, D : Big_Integer) is null;
 657    procedure Lemma_Gt_Commutation (A, B : Double_Uns) is null;
 658    procedure Lemma_Gt_Mult (A, B, C, D : Big_Integer) is null;
 659    procedure Lemma_Lo_Is_Ident (X : Double_Uns) is null;
 660    procedure Lemma_Lt_Commutation (A, B : Double_Uns) is null;
 661    procedure Lemma_Lt_Mult (A, B, C, D : Big_Integer) is null;
 662    procedure Lemma_Mult_Commutation (X, Y : Single_Uns) is null;
 663    procedure Lemma_Mult_Commutation (X, Y : Double_Int) is null;
 664    procedure Lemma_Mult_Commutation (X, Y, Z : Double_Uns) is null;
 665    procedure Lemma_Mult_Distribution (X, Y, Z : Big_Integer) is null;
 666    procedure Lemma_Mult_Non_Negative (X, Y : Big_Integer) is null;
 667    procedure Lemma_Mult_Non_Positive (X, Y : Big_Integer) is null;
 668    procedure Lemma_Mult_Positive (X, Y : Big_Integer) is null;
 669    procedure Lemma_Neg_Rem (X, Y : Big_Integer) is null;
 670    procedure Lemma_Not_In_Range_Big2xx64 is null;
 671    procedure Lemma_Powers (A : Big_Natural; B, C : Natural) is null;
 672    procedure Lemma_Rem_Commutation (X, Y : Double_Uns) is null;
 673    procedure Lemma_Rem_Is_Ident (X, Y : Big_Integer) is null;
 674    procedure Lemma_Rem_Sign (X, Y : Big_Integer) is null;
 675    procedure Lemma_Rev_Div_Definition (A, B, Q, R : Big_Natural) is null;
 676    procedure Lemma_Simplify (X, Y : Big_Integer) is null;
 677    procedure Lemma_Substitution (A, B, C, C1, D : Big_Integer) is null;
 678    procedure Lemma_Subtract_Commutation (X, Y : Double_Uns) is null;
 679    procedure Lemma_Subtract_Double_Uns (X, Y : Double_Int) is null;
 680    procedure Lemma_Word_Commutation (X : Single_Uns) is null;
 681
 682    --------------------------
 683    -- Add_With_Ovflo_Check --
 684    --------------------------
 685
 686    function Add_With_Ovflo_Check (X, Y : Double_Int) return Double_Int is
 687       R : constant Double_Int := To_Int (To_Uns (X) + To_Uns (Y));
 688
 689       --  Local lemmas
 690
 691       procedure Prove_Negative_X
 692       with
 693         Ghost,
 694         Pre  => X < 0 and then (Y > 0 or else R < 0),
 695         Post => R = X + Y;
 696
 697       procedure Prove_Non_Negative_X
 698       with
 699         Ghost,
 700         Pre  => X >= 0 and then (Y < 0 or else R >= 0),
 701         Post => R = X + Y;
 702
 703       procedure Prove_Overflow_Case
 704       with
 705         Ghost,
 706         Pre  =>
 707           (if X >= 0 then Y >= 0 and then R < 0
 708                      else Y <= 0 and then R >= 0),
 709         Post => not In_Double_Int_Range (Big (X) + Big (Y));
 710
 711       ----------------------
 712       -- Prove_Negative_X --
 713       ----------------------
 714
 715       procedure Prove_Negative_X is
 716       begin
 717          if X = Double_Int'First then
 718             if Y > 0 then
 719                null;
 720             else
 721                pragma Assert
 722                  (To_Uns (X) + To_Uns (Y) =
 723                     2 ** (Double_Size - 1) - Double_Uns (-Y));
 724                pragma Assert  --  as R < 0
 725                  (To_Uns (X) + To_Uns (Y) >= 2 ** (Double_Size - 1));
 726                pragma Assert (Y = 0);
 727             end if;
 728
 729          elsif Y = Double_Int'First then
 730             pragma Assert
 731               (To_Uns (X) + To_Uns (Y) =
 732                  2 ** (Double_Size - 1) - Double_Uns (-X));
 733             pragma Assert (False);
 734
 735          elsif Y <= 0 then
 736             pragma Assert
 737               (To_Uns (X) + To_Uns (Y) = -Double_Uns (-X) - Double_Uns (-Y));
 738
 739          else  --  Y > 0, 0 > X > Double_Int'First
 740             declare
 741                Ru : constant Double_Uns := To_Uns (X) + To_Uns (Y);
 742             begin
 743                pragma Assert (Ru = -Double_Uns (-X) + Double_Uns (Y));
 744                if Ru < 2 ** (Double_Size - 1) then  --  R >= 0
 745                   Lemma_Subtract_Double_Uns (-X, Y);
 746                   pragma Assert (Ru = Double_Uns (X + Y));
 747
 748                elsif Ru = 2 ** (Double_Size - 1) then
 749                   pragma Assert (Double_Uns (Y) < 2 ** (Double_Size - 1));
 750                   pragma Assert (Double_Uns (-X) < 2 ** (Double_Size - 1));
 751                   pragma Assert (False);
 752
 753                else
 754                   pragma Assert
 755                     (R = -Double_Int (-(-Double_Uns (-X) + Double_Uns (Y))));
 756                   pragma Assert
 757                     (R = -Double_Int (-Double_Uns (Y) + Double_Uns (-X)));
 758                end if;
 759             end;
 760          end if;
 761       end Prove_Negative_X;
 762
 763       --------------------------
 764       -- Prove_Non_Negative_X --
 765       --------------------------
 766
 767       procedure Prove_Non_Negative_X is
 768       begin
 769          if Y >= 0 or else Y = Double_Int'First then
 770             null;
 771          else
 772             pragma Assert
 773               (To_Uns (X) + To_Uns (Y) = Double_Uns (X) - Double_Uns (-Y));
 774          end if;
 775       end Prove_Non_Negative_X;
 776
 777       -------------------------
 778       -- Prove_Overflow_Case --
 779       -------------------------
 780
 781       procedure Prove_Overflow_Case is
 782       begin
 783          if X < 0 and then X /= Double_Int'First and then Y /= Double_Int'First
 784          then
 785             pragma Assert
 786               (To_Uns (X) + To_Uns (Y) = -Double_Uns (-X) - Double_Uns (-Y));
 787          end if;
 788       end Prove_Overflow_Case;
 789
 790    --  Start of processing for Add_With_Ovflo_Check
 791
 792    begin
 793       if X >= 0 then
 794          if Y < 0 or else R >= 0 then
 795             Prove_Non_Negative_X;
 796             return R;
 797          end if;
 798
 799       else -- X < 0
 800          if Y > 0 or else R < 0 then
 801             Prove_Negative_X;
 802             return R;
 803          end if;
 804       end if;
 805
 806       Prove_Overflow_Case;
 807       Raise_Error;
 808    end Add_With_Ovflo_Check;
 809
 810    -------------------
 811    -- Double_Divide --
 812    -------------------
 813
 814    procedure Double_Divide
 815      (X, Y, Z : Double_Int;
 816       Q, R    : out Double_Int;
 817       Round   : Boolean)
 818    is
 819       Xu  : constant Double_Uns := abs X;
 820       Yu  : constant Double_Uns := abs Y;
 821
 822       Yhi : constant Single_Uns := Hi (Yu);
 823       Ylo : constant Single_Uns := Lo (Yu);
 824
 825       Zu  : constant Double_Uns := abs Z;
 826       Zhi : constant Single_Uns := Hi (Zu);
 827       Zlo : constant Single_Uns := Lo (Zu);
 828
 829       T1, T2     : Double_Uns;
 830       Du, Qu, Ru : Double_Uns;
 831       Den_Pos    : constant Boolean := (Y < 0) = (Z < 0);
 832
 833       --  Local ghost variables
 834
 835       Mult  : constant Big_Integer := abs (Big (Y) * Big (Z)) with Ghost;
 836       Quot  : Big_Integer with Ghost;
 837       Big_R : Big_Integer with Ghost;
 838       Big_Q : Big_Integer with Ghost;
 839
 840       --  Local lemmas
 841
 842       procedure Prove_Overflow_Case
 843       with
 844         Ghost,
 845         Pre  => X = Double_Int'First and then Big (Y) * Big (Z) = -1,
 846         Post => not In_Double_Int_Range (Big (X) / (Big (Y) * Big (Z)))
 847           and then not In_Double_Int_Range
 848             (Round_Quotient (Big (X), Big (Y) * Big (Z),
 849                              Big (X) / (Big (Y) * Big (Z)),
 850                              Big (X) rem (Big (Y) * Big (Z))));
 851       --  Proves the special case where -2**(Double_Size - 1) is divided by -1,
 852       --  generating an overflow.
 853
 854       procedure Prove_Quotient_Zero
 855       with
 856         Ghost,
 857         Pre  => Mult >= Big_2xxDouble
 858           and then
 859             not (Mult = Big_2xxDouble
 860                    and then X = Double_Int'First
 861                    and then Round)
 862           and then Q = 0
 863           and then R = X,
 864         Post => Big (R) = Big (X) rem (Big (Y) * Big (Z))
 865           and then
 866             (if Round then
 867                Big (Q) = Round_Quotient (Big (X), Big (Y) * Big (Z),
 868                                          Big (X) / (Big (Y) * Big (Z)),
 869                                          Big (R))
 870              else Big (Q) = Big (X) / (Big (Y) * Big (Z)));
 871       --  Proves the general case where divisor doesn't fit in Double_Uns and
 872       --  quotient is 0.
 873
 874       procedure Prove_Round_To_One
 875       with
 876         Ghost,
 877         Pre  => Mult = Big_2xxDouble
 878           and then X = Double_Int'First
 879           and then Q = (if Den_Pos then -1 else 1)
 880           and then R = X
 881           and then Round,
 882         Post => Big (R) = Big (X) rem (Big (Y) * Big (Z))
 883           and then Big (Q) = Round_Quotient (Big (X), Big (Y) * Big (Z),
 884                                              Big (X) / (Big (Y) * Big (Z)),
 885                                              Big (R));
 886       --  Proves the special case where the divisor doesn't fit in Double_Uns
 887       --  but quotient is still 1 or -1 due to rounding
 888       --  (abs (Y*Z) = 2**Double_Size and X = -2**(Double_Size - 1) and Round).
 889
 890       procedure Prove_Rounding_Case
 891       with
 892         Ghost,
 893         Pre  => Mult /= 0
 894           and then Quot = Big (X) / (Big (Y) * Big (Z))
 895           and then Big_R = Big (X) rem (Big (Y) * Big (Z))
 896           and then Big_Q =
 897             Round_Quotient (Big (X), Big (Y) * Big (Z), Quot, Big_R)
 898           and then Big (Ru) = abs Big_R
 899           and then Big (Du) = Mult
 900           and then Big (Qu) =
 901             (if Ru > (Du - Double_Uns'(1)) / Double_Uns'(2)
 902              then abs Quot + 1
 903              else abs Quot),
 904         Post => abs Big_Q = Big (Qu);
 905       --  Proves correctness of the rounding of the unsigned quotient
 906
 907       procedure Prove_Sign_Quotient
 908       with
 909         Ghost,
 910         Pre  => Mult /= 0
 911           and then Quot = Big (X) / (Big (Y) * Big (Z))
 912           and then Big_R = Big (X) rem (Big (Y) * Big (Z))
 913           and then Big_Q =
 914             (if Round then
 915                Round_Quotient (Big (X), Big (Y) * Big (Z), Quot, Big_R)
 916              else Quot),
 917         Post =>
 918           (if X >= 0 then
 919              (if Den_Pos then Big_Q >= 0 else Big_Q <= 0)
 920            else
 921              (if Den_Pos then Big_Q <= 0 else Big_Q >= 0));
 922       --  Proves the correct sign of the signed quotient Big_Q
 923
 924       procedure Prove_Signs
 925       with
 926         Ghost,
 927         Pre  => Mult /= 0
 928           and then Quot = Big (X) / (Big (Y) * Big (Z))
 929           and then Big_R = Big (X) rem (Big (Y) * Big (Z))
 930           and then Big_Q =
 931             (if Round then
 932                Round_Quotient (Big (X), Big (Y) * Big (Z), Quot, Big_R)
 933              else Quot)
 934           and then Big (Ru) = abs Big_R
 935           and then Big (Qu) = abs Big_Q
 936           and then R = (if X >= 0 then To_Int (Ru) else To_Int (-Ru))
 937           and then
 938             Q = (if (X >= 0) = Den_Pos then To_Int (Qu) else To_Int (-Qu))
 939           and then not (X = Double_Int'First and then Big (Y) * Big (Z) = -1),
 940         Post => Big (R) = Big (X) rem (Big (Y) * Big (Z))
 941           and then
 942             (if Round then
 943                Big (Q) = Round_Quotient (Big (X), Big (Y) * Big (Z),
 944                                          Big (X) / (Big (Y) * Big (Z)),
 945                                          Big (R))
 946              else Big (Q) = Big (X) / (Big (Y) * Big (Z)));
 947       --  Proves final signs match the intended result after the unsigned
 948       --  division is done.
 949
 950       -----------------------------
 951       -- Local lemma null bodies --
 952       -----------------------------
 953
 954       procedure Prove_Overflow_Case is null;
 955       procedure Prove_Quotient_Zero is null;
 956       procedure Prove_Round_To_One is null;
 957       procedure Prove_Sign_Quotient is null;
 958
 959       -------------------------
 960       -- Prove_Rounding_Case --
 961       -------------------------
 962
 963       procedure Prove_Rounding_Case is
 964       begin
 965          if Same_Sign (Big (X), Big (Y) * Big (Z)) then
 966             null;
 967          end if;
 968       end Prove_Rounding_Case;
 969
 970       -----------------
 971       -- Prove_Signs --
 972       -----------------
 973
 974       procedure Prove_Signs is
 975       begin
 976          if (X >= 0) = Den_Pos then
 977             pragma Assert (Quot >= 0);
 978             pragma Assert (Big_Q >= 0);
 979             pragma Assert (Q >= 0);
 980             pragma Assert (Big (Q) = Big_Q);
 981          else
 982             pragma Assert ((X >= 0) /= (Big (Y) * Big (Z) >= 0));
 983             pragma Assert (Quot <= 0);
 984             pragma Assert (Big_Q <= 0);
 985             pragma Assert (if X >= 0 then R >= 0);
 986             pragma Assert (if X < 0 then R <= 0);
 987             pragma Assert (Big (R) = Big_R);
 988          end if;
 989       end Prove_Signs;
 990
 991    --  Start of processing for Double_Divide
 992
 993    begin
 994       if Yu = 0 or else Zu = 0 then
 995          Raise_Error;
 996       end if;
 997
 998       pragma Assert (Mult /= 0);
 999       pragma Assert (Den_Pos = (Big (Y) * Big (Z) > 0));
1000       Quot := Big (X) / (Big (Y) * Big (Z));
1001       Big_R := Big (X) rem (Big (Y) * Big (Z));
1002       if Round then
1003          Big_Q := Round_Quotient (Big (X), Big (Y) * Big (Z), Quot, Big_R);
1004       else
1005          Big_Q := Quot;
1006       end if;
1007       Lemma_Abs_Mult_Commutation (Big (Y), Big (Z));
1008       Lemma_Mult_Decomposition (Mult, Yu, Zu, Yhi, Ylo, Zhi, Zlo);
1009
1010       --  Compute Y * Z. Note that if the result overflows Double_Uns, then
1011       --  the rounded result is zero, except for the very special case where
1012       --  X = -2 ** (Double_Size - 1) and abs (Y * Z) = 2 ** Double_Size, when
1013       --  Round is True.
1014
1015       if Yhi /= 0 then
1016          if Zhi /= 0 then
1017             R := X;
1018
1019             --  Handle the special case when Round is True
1020
1021             if Yhi = 1
1022               and then Zhi = 1
1023               and then Ylo = 0
1024               and then Zlo = 0
1025               and then X = Double_Int'First
1026               and then Round
1027             then
1028                Q := (if Den_Pos then -1 else 1);
1029
1030                Prove_Round_To_One;
1031
1032             else
1033                Q := 0;
1034
1035                pragma Assert (Double_Uns'(Yhi * Zhi) >= Double_Uns (Yhi));
1036                pragma Assert (Double_Uns'(Yhi * Zhi) >= Double_Uns (Zhi));
1037                pragma Assert (Big (Double_Uns'(Yhi * Zhi)) >= 1);
1038                if Yhi > 1 or else Zhi > 1 then
1039                   pragma Assert (Big (Double_Uns'(Yhi * Zhi)) > 1);
1040                   pragma Assert (if X = Double_Int'First and then Round then
1041                                     Mult > Big_2xxDouble);
1042                elsif Zlo > 0 then
1043                   pragma Assert (Big (Double_Uns'(Yhi * Zlo)) > 0);
1044                   pragma Assert (if X = Double_Int'First and then Round then
1045                                     Mult > Big_2xxDouble);
1046                elsif Ylo > 0 then
1047                   pragma Assert (Double_Uns'(Ylo * Zhi) > 0);
1048                   pragma Assert (Big (Double_Uns'(Ylo * Zhi)) > 0);
1049                   pragma Assert (if X = Double_Int'First and then Round then
1050                                     Mult > Big_2xxDouble);
1051                else
1052                   pragma Assert (not (X = Double_Int'First and then Round));
1053                end if;
1054                Prove_Quotient_Zero;
1055             end if;
1056
1057             return;
1058          else
1059             T2 := Yhi * Zlo;
1060             pragma Assert (Big (T2) = Big (Double_Uns'(Yhi * Zlo)));
1061             pragma Assert (Big_0 = Big (Double_Uns'(Ylo * Zhi)));
1062          end if;
1063
1064       else
1065          T2 := Ylo * Zhi;
1066          pragma Assert (Big (T2) = Big (Double_Uns'(Ylo * Zhi)));
1067          pragma Assert (Big_0 = Big (Double_Uns'(Yhi * Zlo)));
1068       end if;
1069
1070       T1 := Ylo * Zlo;
1071
1072       pragma Assert (Big (T2) = Big (Double_Uns'(Yhi * Zlo))
1073                               + Big (Double_Uns'(Ylo * Zhi)));
1074       Lemma_Mult_Distribution (Big_2xxSingle,
1075                                Big (Double_Uns'(Yhi * Zlo)),
1076                                Big (Double_Uns'(Ylo * Zhi)));
1077       pragma Assert (Mult = Big_2xxSingle * Big (T2) + Big (T1));
1078       Lemma_Hi_Lo (T1, Hi (T1), Lo (T1));
1079       pragma Assert
1080         (Mult = Big_2xxSingle * Big (T2)
1081               + Big_2xxSingle * Big (Double_Uns (Hi (T1)))
1082                               + Big (Double_Uns (Lo (T1))));
1083       Lemma_Mult_Distribution (Big_2xxSingle,
1084                                Big (T2),
1085                                Big (Double_Uns (Hi (T1))));
1086       Lemma_Add_Commutation (T2, Hi (T1));
1087
1088       T2 := T2 + Hi (T1);
1089
1090       pragma Assert
1091         (Mult = Big_2xxSingle * Big (T2) + Big (Double_Uns (Lo (T1))));
1092       Lemma_Hi_Lo (T2, Hi (T2), Lo (T2));
1093       Lemma_Mult_Distribution (Big_2xxSingle,
1094                                Big (Double_Uns (Hi (T2))),
1095                                Big (Double_Uns (Lo (T2))));
1096       Lemma_Double_Big_2xxSingle;
1097       pragma Assert
1098         (Mult = Big_2xxDouble * Big (Double_Uns (Hi (T2)))
1099               + Big_2xxSingle * Big (Double_Uns (Lo (T2)))
1100                               + Big (Double_Uns (Lo (T1))));
1101
1102       if Hi (T2) /= 0 then
1103          R := X;
1104
1105          --  Handle the special case when Round is True
1106
1107          if Hi (T2) = 1
1108            and then Lo (T2) = 0
1109            and then Lo (T1) = 0
1110            and then X = Double_Int'First
1111            and then Round
1112          then
1113             Q := (if Den_Pos then -1 else 1);
1114
1115             Prove_Round_To_One;
1116
1117          else
1118             Q := 0;
1119
1120             pragma Assert (Big (Double_Uns (Hi (T2))) >= 1);
1121             pragma Assert (Big (Double_Uns (Lo (T2))) >= 0);
1122             pragma Assert (Big (Double_Uns (Lo (T1))) >= 0);
1123             pragma Assert (Big_2xxSingle * Big (Double_Uns (Lo (T2)))
1124                                          + Big (Double_Uns (Lo (T1))) >= 0);
1125             pragma Assert (Mult >= Big_2xxDouble * Big (Double_Uns (Hi (T2))));
1126             pragma Assert (Mult >= Big_2xxDouble);
1127             if Hi (T2) > 1 then
1128                pragma Assert (Big (Double_Uns (Hi (T2))) > 1);
1129                pragma Assert (if X = Double_Int'First and then Round then
1130                                  Mult > Big_2xxDouble);
1131             elsif Lo (T2) > 0 then
1132                pragma Assert (Big (Double_Uns (Lo (T2))) > 0);
1133                pragma Assert (Big_2xxSingle > 0);
1134                pragma Assert (Big_2xxSingle * Big (Double_Uns (Lo (T2))) > 0);
1135                pragma Assert (Big_2xxSingle * Big (Double_Uns (Lo (T2)))
1136                                             + Big (Double_Uns (Lo (T1))) > 0);
1137                pragma Assert (if X = Double_Int'First and then Round then
1138                                  Mult > Big_2xxDouble);
1139             elsif Lo (T1) > 0 then
1140                pragma Assert (Double_Uns (Lo (T1)) > 0);
1141                Lemma_Gt_Commutation (Double_Uns (Lo (T1)), 0);
1142                pragma Assert (Big (Double_Uns (Lo (T1))) > 0);
1143                pragma Assert (if X = Double_Int'First and then Round then
1144                                  Mult > Big_2xxDouble);
1145             else
1146                pragma Assert (not (X = Double_Int'First and then Round));
1147             end if;
1148             Prove_Quotient_Zero;
1149          end if;
1150
1151          return;
1152       end if;
1153
1154       Du := Lo (T2) & Lo (T1);
1155
1156       Lemma_Hi_Lo (Du, Lo (T2), Lo (T1));
1157       pragma Assert (Mult = Big (Du));
1158       pragma Assert (Du /= 0);
1159       --  Multiplication of 2-limb arguments Yu and Zu leads to 4-limb result
1160       --  (where each limb is a single value). Cases where 4 limbs are needed
1161       --  require Yhi /= 0 and Zhi /= 0 and lead to early exit. Remaining cases
1162       --  where 3 limbs are needed correspond to Hi(T2) /= 0 and lead to early
1163       --  exit. Thus, at this point, the result fits in 2 limbs which are
1164       --  exactly Lo (T2) and Lo (T1), which corresponds to the value of Du.
1165       --  As the case where one of Yu or Zu is null also led to early exit,
1166       --  we have Du /= 0 here.
1167
1168       --  Check overflow case of largest negative number divided by -1
1169
1170       if X = Double_Int'First and then Du = 1 and then not Den_Pos then
1171          Prove_Overflow_Case;
1172          Raise_Error;
1173       end if;
1174
1175       --  Perform the actual division
1176
1177       pragma Assert (Du /= 0);
1178       --  Multiplication of 2-limb arguments Yu and Zu leads to 4-limb result
1179       --  (where each limb is a single value). Cases where 4 limbs are needed
1180       --  require Yhi/=0 and Zhi/=0 and lead to early exit. Remaining cases
1181       --  where 3 limbs are needed correspond to Hi(T2)/=0 and lead to early
1182       --  exit. Thus, at this point, the result fits in 2 limbs which are
1183       --  exactly Lo(T2) and Lo(T1), which corresponds to the value of Du.
1184       --  As the case where one of Yu or Zu is null also led to early exit,
1185       --  we have Du/=0 here.
1186
1187       Qu := Xu / Du;
1188       Ru := Xu rem Du;
1189
1190       Lemma_Div_Commutation (Xu, Du);
1191       Lemma_Abs_Div_Commutation (Big (X), Big (Y) * Big (Z));
1192       Lemma_Abs_Commutation (X);
1193       pragma Assert (abs Quot = Big (Qu));
1194       Lemma_Rem_Commutation (Xu, Du);
1195       Lemma_Abs_Rem_Commutation (Big (X), Big (Y) * Big (Z));
1196       pragma Assert (abs Big_R = Big (Ru));
1197
1198       --  Deal with rounding case
1199
1200       if Round then
1201          if Ru > (Du - Double_Uns'(1)) / Double_Uns'(2) then
1202             Lemma_Add_Commutation (Qu, 1);
1203
1204             Qu := Qu + Double_Uns'(1);
1205          end if;
1206
1207          Prove_Rounding_Case;
1208       end if;
1209
1210       pragma Assert (abs Big_Q = Big (Qu));
1211       Prove_Sign_Quotient;
1212
1213       --  Set final signs (RM 4.5.5(27-30))
1214
1215       --  Case of dividend (X) sign positive
1216
1217       if X >= 0 then
1218          R := To_Int (Ru);
1219          Q := (if Den_Pos then To_Int (Qu) else To_Int (-Qu));
1220
1221       --  We perform the unary minus operation on the unsigned value
1222       --  before conversion to signed, to avoid a possible overflow
1223       --  for value -2 ** (Double_Size - 1), both for computing R and Q.
1224
1225       --  Case of dividend (X) sign negative
1226
1227       else
1228          R := To_Int (-Ru);
1229          Q := (if Den_Pos then To_Int (-Qu) else To_Int (Qu));
1230       end if;
1231
1232       Prove_Signs;
1233    end Double_Divide;
1234
1235    ---------
1236    -- Le3 --
1237    ---------
1238
1239    function Le3 (X1, X2, X3, Y1, Y2, Y3 : Single_Uns) return Boolean is
1240    begin
1241       if X1 < Y1 then
1242          return True;
1243       elsif X1 > Y1 then
1244          return False;
1245       elsif X2 < Y2 then
1246          return True;
1247       elsif X2 > Y2 then
1248          return False;
1249       else
1250          return X3 <= Y3;
1251       end if;
1252    end Le3;
1253
1254    -------------------------------
1255    -- Lemma_Abs_Div_Commutation --
1256    -------------------------------
1257
1258    procedure Lemma_Abs_Div_Commutation (X, Y : Big_Integer) is
1259    begin
1260       if Y < 0 then
1261          if X < 0 then
1262             pragma Assert (abs (X / Y) = abs (X / (-Y)));
1263          else
1264             Lemma_Neg_Div (X, Y);
1265             pragma Assert (abs (X / Y) = abs ((-X) / (-Y)));
1266          end if;
1267       end if;
1268    end Lemma_Abs_Div_Commutation;
1269
1270    -------------------------------
1271    -- Lemma_Abs_Rem_Commutation --
1272    -------------------------------
1273
1274    procedure Lemma_Abs_Rem_Commutation (X, Y : Big_Integer) is
1275    begin
1276       if Y < 0 then
1277          Lemma_Neg_Rem (X, Y);
1278          if X < 0 then
1279             pragma Assert (X rem Y = -((-X) rem (-Y)));
1280             pragma Assert (abs (X rem Y) = (abs X) rem (abs Y));
1281          else
1282             pragma Assert (abs (X rem Y) = (abs X) rem (abs Y));
1283          end if;
1284       end if;
1285    end Lemma_Abs_Rem_Commutation;
1286
1287    -----------------------------
1288    -- Lemma_Concat_Definition --
1289    -----------------------------
1290
1291    procedure Lemma_Concat_Definition (X, Y : Single_Uns) is
1292       Hi : constant Double_Uns := Shift_Left (Double_Uns (X), Single_Size);
1293       Lo : constant Double_Uns := Double_Uns (Y);
1294    begin
1295       pragma Assert (Hi = Double_Uns'(2 ** Single_Size) * Double_Uns (X));
1296       pragma Assert ((Hi or Lo) = Hi + Lo);
1297    end Lemma_Concat_Definition;
1298
1299    ------------------
1300    -- Lemma_Div_Eq --
1301    ------------------
1302
1303    procedure Lemma_Div_Eq (A, B, S, R : Big_Integer) is
1304    begin
1305       pragma Assert ((A - B) * S = R);
1306       pragma Assert ((A - B) * S / S = R / S);
1307       Lemma_Mult_Div (A - B, S);
1308       pragma Assert (A - B = R / S);
1309    end Lemma_Div_Eq;
1310
1311    ------------------------
1312    -- Lemma_Double_Shift --
1313    ------------------------
1314
1315    procedure Lemma_Double_Shift (X : Double_Uns; S, S1 : Natural) is
1316    begin
1317       Lemma_Double_Shift (X, Double_Uns (S), Double_Uns (S1));
1318       pragma Assert (Shift_Left (Shift_Left (X, S), S1)
1319         = Shift_Left (Shift_Left (X, S), Natural (Double_Uns (S1))));
1320       pragma Assert (Shift_Left (X, S + S1)
1321         = Shift_Left (X, Natural (Double_Uns (S + S1))));
1322    end Lemma_Double_Shift;
1323
1324    -----------------------------
1325    -- Lemma_Double_Shift_Left --
1326    -----------------------------
1327
1328    procedure Lemma_Double_Shift_Left (X : Double_Uns; S, S1 : Natural) is
1329    begin
1330       Lemma_Double_Shift_Left (X, Double_Uns (S), Double_Uns (S1));
1331       pragma Assert (Shift_Left (Shift_Left (X, S), S1)
1332         = Shift_Left (Shift_Left (X, S), Natural (Double_Uns (S1))));
1333       pragma Assert (Shift_Left (X, S + S1)
1334         = Shift_Left (X, Natural (Double_Uns (S + S1))));
1335    end Lemma_Double_Shift_Left;
1336
1337    ------------------------------
1338    -- Lemma_Double_Shift_Right --
1339    ------------------------------
1340
1341    procedure Lemma_Double_Shift_Right (X : Double_Uns; S, S1 : Natural) is
1342    begin
1343       Lemma_Double_Shift_Right (X, Double_Uns (S), Double_Uns (S1));
1344       pragma Assert (Shift_Right (Shift_Right (X, S), S1)
1345         = Shift_Right (Shift_Right (X, S), Natural (Double_Uns (S1))));
1346       pragma Assert (Shift_Right (X, S + S1)
1347         = Shift_Right (X, Natural (Double_Uns (S + S1))));
1348    end Lemma_Double_Shift_Right;
1349
1350    -----------------
1351    -- Lemma_Hi_Lo --
1352    -----------------
1353
1354    procedure Lemma_Hi_Lo (Xu : Double_Uns; Xhi, Xlo : Single_Uns) is
1355    begin
1356       pragma Assert (Double_Uns (Xhi) = Xu / Double_Uns'(2 ** Single_Size));
1357       pragma Assert (Double_Uns (Xlo) = Xu mod 2 ** Single_Size);
1358    end Lemma_Hi_Lo;
1359
1360    -------------------
1361    -- Lemma_Hi_Lo_3 --
1362    -------------------
1363
1364    procedure Lemma_Hi_Lo_3 (Xu : Double_Uns; Xhi, Xlo : Single_Uns) is
1365    begin
1366       Lemma_Hi_Lo (Xu, Xhi, Xlo);
1367    end Lemma_Hi_Lo_3;
1368
1369    ------------------------------
1370    -- Lemma_Mult_Decomposition --
1371    ------------------------------
1372
1373    procedure Lemma_Mult_Decomposition
1374      (Mult               : Big_Integer;
1375       Xu, Yu             : Double_Uns;
1376       Xhi, Xlo, Yhi, Ylo : Single_Uns)
1377    is
1378    begin
1379       Lemma_Hi_Lo (Xu, Xhi, Xlo);
1380       Lemma_Hi_Lo (Yu, Yhi, Ylo);
1381
1382       pragma Assert
1383         (Mult =
1384            (Big_2xxSingle * Big (Double_Uns (Xhi)) + Big (Double_Uns (Xlo))) *
1385            (Big_2xxSingle * Big (Double_Uns (Yhi)) + Big (Double_Uns (Ylo))));
1386       pragma Assert (Mult =
1387         Big_2xxSingle
1388           * Big_2xxSingle * Big (Double_Uns (Xhi)) * Big (Double_Uns (Yhi))
1389           + Big_2xxSingle * Big (Double_Uns (Xhi)) * Big (Double_Uns (Ylo))
1390           + Big_2xxSingle * Big (Double_Uns (Xlo)) * Big (Double_Uns (Yhi))
1391                           + Big (Double_Uns (Xlo)) * Big (Double_Uns (Ylo)));
1392       Lemma_Deep_Mult_Commutation (Big_2xxSingle * Big_2xxSingle, Xhi, Yhi);
1393       Lemma_Deep_Mult_Commutation (Big_2xxSingle, Xhi, Ylo);
1394       Lemma_Deep_Mult_Commutation (Big_2xxSingle, Xlo, Yhi);
1395       Lemma_Mult_Commutation (Xlo, Ylo);
1396       pragma Assert (Mult =
1397         Big_2xxSingle * Big_2xxSingle * Big (Double_Uns'(Xhi * Yhi))
1398                       + Big_2xxSingle * Big (Double_Uns'(Xhi * Ylo))
1399                       + Big_2xxSingle * Big (Double_Uns'(Xlo * Yhi))
1400                                       + Big (Double_Uns'(Xlo * Ylo)));
1401    end Lemma_Mult_Decomposition;
1402
1403    --------------------
1404    -- Lemma_Mult_Div --
1405    --------------------
1406
1407    procedure Lemma_Mult_Div (A, B : Big_Integer) is
1408    begin
1409       if B > 0 then
1410          pragma Assert (A * B / B = A);
1411       else
1412          pragma Assert (A * (-B) / (-B) = A);
1413       end if;
1414    end Lemma_Mult_Div;
1415
1416    -------------------
1417    -- Lemma_Neg_Div --
1418    -------------------
1419
1420    procedure Lemma_Neg_Div (X, Y : Big_Integer) is
1421    begin
1422       pragma Assert ((-X) / (-Y) = -(X / (-Y)));
1423       pragma Assert (X / (-Y) = -(X / Y));
1424    end Lemma_Neg_Div;
1425
1426    -----------------------
1427    -- Lemma_Powers_Of_2 --
1428    -----------------------
1429
1430    procedure Lemma_Powers_Of_2 (M, N : Natural) is
1431    begin
1432       if M + N < Double_Size then
1433          pragma Assert (Double_Uns'(2**M) * Double_Uns'(2**N)
1434                         = Double_Uns'(2**(M + N)));
1435       end if;
1436
1437       Lemma_Powers_Of_2_Commutation (M);
1438       Lemma_Powers_Of_2_Commutation (N);
1439       Lemma_Powers_Of_2_Commutation (M + N);
1440       Lemma_Powers (Big (Double_Uns'(2)), M, N);
1441
1442       if M + N < Double_Size then
1443          pragma Assert (Big (Double_Uns'(2))**M * Big (Double_Uns'(2))**N
1444                         = Big (Double_Uns'(2))**(M + N));
1445          Lemma_Powers_Of_2_Increasing (M + N, Double_Size);
1446          Lemma_Mult_Commutation (2 ** M, 2 ** N, 2 ** (M + N));
1447       else
1448          pragma Assert (Big (Double_Uns'(2))**M * Big (Double_Uns'(2))**N
1449                         = Big (Double_Uns'(2))**(M + N));
1450       end if;
1451    end Lemma_Powers_Of_2;
1452
1453    -----------------------------------
1454    -- Lemma_Powers_Of_2_Commutation --
1455    -----------------------------------
1456
1457    procedure Lemma_Powers_Of_2_Commutation (M : Natural) is
1458    begin
1459       if M > 0 then
1460          Lemma_Powers_Of_2_Commutation (M - 1);
1461          pragma Assert (Big (Double_Uns'(2))**(M - 1) = Big_2xx (M - 1));
1462          pragma Assert (Big (Double_Uns'(2))**M = Big_2xx (M - 1) * 2);
1463          if M < Double_Size then
1464             Lemma_Powers_Of_2_Increasing (M - 1, Double_Size - 1);
1465             Lemma_Bounded_Powers_Of_2_Increasing (M - 1, Double_Size - 1);
1466             pragma Assert (Double_Uns'(2 ** (M - 1)) * 2 = Double_Uns'(2**M));
1467             Lemma_Mult_Commutation
1468               (Double_Uns'(2 ** (M - 1)), 2, Double_Uns'(2**M));
1469             pragma Assert (Big (Double_Uns'(2))**M = Big_2xx (M));
1470          end if;
1471       end if;
1472    end Lemma_Powers_Of_2_Commutation;
1473
1474    ----------------------------------
1475    -- Lemma_Powers_Of_2_Increasing --
1476    ----------------------------------
1477
1478    procedure Lemma_Powers_Of_2_Increasing (M, N : Natural) is
1479    begin
1480       if M + 1 < N then
1481          Lemma_Powers_Of_2_Increasing (M + 1, N);
1482       end if;
1483    end Lemma_Powers_Of_2_Increasing;
1484
1485    -------------------
1486    -- Lemma_Rem_Abs --
1487    -------------------
1488
1489    procedure Lemma_Rem_Abs (X, Y : Big_Integer) is
1490    begin
1491       Lemma_Neg_Rem (X, Y);
1492    end Lemma_Rem_Abs;
1493
1494    ----------------------
1495    -- Lemma_Shift_Left --
1496    ----------------------
1497
1498    procedure Lemma_Shift_Left (X : Double_Uns; Shift : Natural) is
1499
1500       procedure Lemma_Mult_Pow2 (X : Double_Uns; I : Natural)
1501       with
1502         Ghost,
1503         Pre  => I < Double_Size - 1,
1504         Post => X * Double_Uns'(2) ** I * Double_Uns'(2)
1505           = X * Double_Uns'(2) ** (I + 1);
1506
1507       procedure Lemma_Mult_Pow2 (X : Double_Uns; I : Natural) is
1508          Mul1 : constant Double_Uns := Double_Uns'(2) ** I;
1509          Mul2 : constant Double_Uns := Double_Uns'(2);
1510          Left : constant Double_Uns := X * Mul1 * Mul2;
1511       begin
1512          pragma Assert (Left = X * (Mul1 * Mul2));
1513          pragma Assert (Mul1 * Mul2 = Double_Uns'(2) ** (I + 1));
1514       end Lemma_Mult_Pow2;
1515
1516       XX : Double_Uns := X;
1517
1518    begin
1519       for J in 1 .. Shift loop
1520          declare
1521             Cur_XX : constant Double_Uns := XX;
1522          begin
1523             XX := Shift_Left (XX, 1);
1524             pragma Assert (XX = Cur_XX * Double_Uns'(2));
1525             Lemma_Mult_Pow2 (X, J - 1);
1526          end;
1527          Lemma_Double_Shift_Left (X, J - 1, 1);
1528          pragma Loop_Invariant (XX = Shift_Left (X, J));
1529          pragma Loop_Invariant (XX = X * Double_Uns'(2) ** J);
1530       end loop;
1531    end Lemma_Shift_Left;
1532
1533    -----------------------
1534    -- Lemma_Shift_Right --
1535    -----------------------
1536
1537    procedure Lemma_Shift_Right (X : Double_Uns; Shift : Natural) is
1538
1539       procedure Lemma_Div_Pow2 (X : Double_Uns; I : Natural)
1540       with
1541         Ghost,
1542         Pre  => I < Double_Size - 1,
1543         Post => X / Double_Uns'(2) ** I / Double_Uns'(2)
1544           = X / Double_Uns'(2) ** (I + 1);
1545
1546       procedure Lemma_Div_Pow2 (X : Double_Uns; I : Natural) is
1547          Div1 : constant Double_Uns := Double_Uns'(2) ** I;
1548          Div2 : constant Double_Uns := Double_Uns'(2);
1549          Left : constant Double_Uns := X / Div1 / Div2;
1550       begin
1551          pragma Assert (Left = X / (Div1 * Div2));
1552          pragma Assert (Div1 * Div2 = Double_Uns'(2) ** (I + 1));
1553       end Lemma_Div_Pow2;
1554
1555       XX : Double_Uns := X;
1556
1557    begin
1558       for J in 1 .. Shift loop
1559          declare
1560             Cur_XX : constant Double_Uns := XX;
1561          begin
1562             XX := Shift_Right (XX, 1);
1563             pragma Assert (XX = Cur_XX / Double_Uns'(2));
1564             Lemma_Div_Pow2 (X, J - 1);
1565          end;
1566          Lemma_Double_Shift_Right (X, J - 1, 1);
1567          pragma Loop_Invariant (XX = Shift_Right (X, J));
1568          pragma Loop_Invariant (XX = X / Double_Uns'(2) ** J);
1569       end loop;
1570    end Lemma_Shift_Right;
1571
1572    ------------------------------
1573    -- Lemma_Shift_Without_Drop --
1574    ------------------------------
1575
1576    procedure Lemma_Shift_Without_Drop
1577      (X, Y  : Double_Uns;
1578       Mask  : Single_Uns;
1579       Shift : Natural)
1580    is
1581       pragma Unreferenced (Mask);
1582
1583       procedure Lemma_Bound
1584       with
1585         Pre  => Shift <= Single_Size
1586           and then X <= 2**Single_Size
1587             * Double_Uns'(2**(Single_Size - Shift) - 1)
1588             + Single_Uns'(2**Single_Size - 1),
1589         Post => X <= 2**(Double_Size - Shift) - 1;
1590
1591       procedure Lemma_Exp_Pos (N : Integer)
1592       with
1593         Pre  => N in 0 .. Double_Size - 1,
1594         Post => Double_Uns'(2**N) > 0;
1595
1596       -----------------------------
1597       -- Local lemma null bodies --
1598       -----------------------------
1599
1600       procedure Lemma_Bound is null;
1601       procedure Lemma_Exp_Pos (N : Integer) is null;
1602
1603    --  Start of processing for Lemma_Shift_Without_Drop
1604
1605    begin
1606       if Shift = 0 then
1607          pragma Assert (Big (Y) = Big_2xx (Shift) * Big (X));
1608          return;
1609       end if;
1610
1611       Lemma_Bound;
1612       Lemma_Exp_Pos (Double_Size - Shift);
1613       pragma Assert (X < 2**(Double_Size - Shift));
1614       pragma Assert (Big (X) < Big_2xx (Double_Size - Shift));
1615       pragma Assert (Y = 2**Shift * X);
1616       Lemma_Lt_Mult (Big (X), Big_2xx (Double_Size - Shift), Big_2xx (Shift),
1617                      Big_2xx (Shift) * Big_2xx (Double_Size - Shift));
1618       pragma Assert (Big_2xx (Shift) * Big (X)
1619                      < Big_2xx (Shift) * Big_2xx (Double_Size - Shift));
1620       Lemma_Powers_Of_2 (Shift, Double_Size - Shift);
1621       Lemma_Mult_Commutation (2**Shift, X, Y);
1622       pragma Assert (Big (Y) = Big_2xx (Shift) * Big (X));
1623    end Lemma_Shift_Without_Drop;
1624
1625    -------------------------------
1626    -- Multiply_With_Ovflo_Check --
1627    -------------------------------
1628
1629    function Multiply_With_Ovflo_Check (X, Y : Double_Int) return Double_Int is
1630       Xu  : constant Double_Uns := abs X;
1631       Xhi : constant Single_Uns := Hi (Xu);
1632       Xlo : constant Single_Uns := Lo (Xu);
1633
1634       Yu  : constant Double_Uns := abs Y;
1635       Yhi : constant Single_Uns := Hi (Yu);
1636       Ylo : constant Single_Uns := Lo (Yu);
1637
1638       T1, T2 : Double_Uns;
1639
1640       --  Local ghost variables
1641
1642       Mult : constant Big_Integer := abs (Big (X) * Big (Y)) with Ghost;
1643
1644       --  Local lemmas
1645
1646       procedure Prove_Both_Too_Large
1647       with
1648         Ghost,
1649         Pre  => Xhi /= 0
1650           and then Yhi /= 0
1651           and then Mult =
1652             Big_2xxSingle * Big_2xxSingle * (Big (Double_Uns'(Xhi * Yhi)))
1653                       + Big_2xxSingle * (Big (Double_Uns'(Xhi * Ylo)))
1654                       + Big_2xxSingle * (Big (Double_Uns'(Xlo * Yhi)))
1655                                   + (Big (Double_Uns'(Xlo * Ylo))),
1656         Post => not In_Double_Int_Range (Big (X) * Big (Y));
1657
1658       procedure Prove_Final_Decomposition
1659       with
1660         Ghost,
1661         Pre  => In_Double_Int_Range (Big (X) * Big (Y))
1662           and then Mult = Big_2xxSingle * Big (T2) + Big (Double_Uns (Lo (T1)))
1663           and then Hi (T2) = 0,
1664         Post => Mult = Big (Lo (T2) & Lo (T1));
1665
1666       procedure Prove_Neg_Int
1667       with
1668         Ghost,
1669         Pre  => In_Double_Int_Range (Big (X) * Big (Y))
1670           and then Mult = Big (T2)
1671           and then ((X >= 0 and then Y < 0) or else (X < 0 and then Y >= 0)),
1672         Post => To_Neg_Int (T2) = X * Y;
1673
1674       procedure Prove_Pos_Int
1675       with
1676         Ghost,
1677         Pre  => In_Double_Int_Range (Big (X) * Big (Y))
1678           and then Mult = Big (T2)
1679           and then ((X >= 0 and then Y >= 0) or else (X < 0 and then Y < 0)),
1680         Post => In_Double_Int_Range (Big (T2))
1681           and then To_Pos_Int (T2) = X * Y;
1682
1683       procedure Prove_Result_Too_Large
1684       with
1685         Ghost,
1686         Pre  => Mult = Big_2xxSingle * Big (T2) + Big (Double_Uns (Lo (T1)))
1687           and then Hi (T2) /= 0,
1688         Post => not In_Double_Int_Range (Big (X) * Big (Y));
1689
1690       procedure Prove_Too_Large
1691       with
1692         Ghost,
1693         Pre  => abs (Big (X) * Big (Y)) >= Big_2xxDouble,
1694         Post => not In_Double_Int_Range (Big (X) * Big (Y));
1695
1696       --------------------------
1697       -- Prove_Both_Too_Large --
1698       --------------------------
1699
1700       procedure Prove_Both_Too_Large is
1701       begin
1702          pragma Assert (Mult >=
1703            Big_2xxSingle * Big_2xxSingle * Big (Double_Uns'(Xhi * Yhi)));
1704          pragma Assert (Double_Uns (Xhi) * Double_Uns (Yhi) >= 1);
1705          pragma Assert (Mult >= Big_2xxSingle * Big_2xxSingle);
1706          Prove_Too_Large;
1707       end Prove_Both_Too_Large;
1708
1709       -------------------------------
1710       -- Prove_Final_Decomposition --
1711       -------------------------------
1712
1713       procedure Prove_Final_Decomposition is
1714       begin
1715          Lemma_Hi_Lo (T2, Hi (T2), Lo (T2));
1716          pragma Assert (Mult = Big_2xxSingle * Big (Double_Uns (Lo (T2)))
1717                                              + Big (Double_Uns (Lo (T1))));
1718          pragma Assert (Mult <= Big_2xxDouble_Minus_1);
1719          Lemma_Mult_Commutation (X, Y);
1720          pragma Assert (Mult = abs (Big (X * Y)));
1721          Lemma_Word_Commutation (Lo (T2));
1722          pragma Assert (Mult = Big (Double_Uns'(2 ** Single_Size)
1723                           * Double_Uns (Lo (T2)))
1724                           + Big (Double_Uns (Lo (T1))));
1725          Lemma_Add_Commutation (Double_Uns'(2 ** Single_Size)
1726                                   * Double_Uns (Lo (T2)),
1727                                 Lo (T1));
1728          pragma Assert (Mult = Big (Double_Uns'(2 ** Single_Size)
1729                           * Double_Uns (Lo (T2)) + Lo (T1)));
1730          pragma Assert (Lo (T2) & Lo (T1) = Double_Uns'(2 ** Single_Size)
1731                           * Double_Uns (Lo (T2)) + Lo (T1));
1732       end Prove_Final_Decomposition;
1733
1734       -------------------
1735       -- Prove_Neg_Int --
1736       -------------------
1737
1738       procedure Prove_Neg_Int is
1739       begin
1740          pragma Assert (X * Y <= 0);
1741          pragma Assert (Mult = -Big (X * Y));
1742       end Prove_Neg_Int;
1743
1744       -------------------
1745       -- Prove_Pos_Int --
1746       -------------------
1747
1748       procedure Prove_Pos_Int is
1749       begin
1750          pragma Assert (X * Y >= 0);
1751          pragma Assert (Mult = Big (X * Y));
1752       end Prove_Pos_Int;
1753
1754       ----------------------------
1755       -- Prove_Result_Too_Large --
1756       ----------------------------
1757
1758       procedure Prove_Result_Too_Large is
1759       begin
1760          pragma Assert (Mult >= Big_2xxSingle * Big (T2));
1761          Lemma_Hi_Lo (T2, Hi (T2), Lo (T2));
1762          pragma Assert (Mult >=
1763            Big_2xxSingle * Big_2xxSingle * Big (Double_Uns (Hi (T2))));
1764          pragma Assert (Double_Uns (Hi (T2)) >= 1);
1765          pragma Assert (Mult >= Big_2xxSingle * Big_2xxSingle);
1766          Prove_Too_Large;
1767       end Prove_Result_Too_Large;
1768
1769       ---------------------
1770       -- Prove_Too_Large --
1771       ---------------------
1772
1773       procedure Prove_Too_Large is null;
1774
1775    --  Start of processing for Multiply_With_Ovflo_Check
1776
1777    begin
1778       Lemma_Mult_Decomposition (Mult, Xu, Yu, Xhi, Xlo, Yhi, Ylo);
1779
1780       if Xhi /= 0 then
1781          if Yhi /= 0 then
1782             Prove_Both_Too_Large;
1783             Raise_Error;
1784          else
1785             T2 := Xhi * Ylo;
1786             pragma Assert (Big (T2) = Big (Double_Uns'(Xhi * Ylo))
1787                                     + Big (Double_Uns'(Xlo * Yhi)));
1788          end if;
1789
1790       elsif Yhi /= 0 then
1791          T2 := Xlo * Yhi;
1792          pragma Assert (Big (T2) = Big (Double_Uns'(Xhi * Ylo))
1793                                  + Big (Double_Uns'(Xlo * Yhi)));
1794
1795       else -- Yhi = Xhi = 0
1796          T2 := 0;
1797       end if;
1798
1799       --  Here we have T2 set to the contribution to the upper half of the
1800       --  result from the upper halves of the input values.
1801
1802       T1 := Xlo * Ylo;
1803
1804       pragma Assert (Big (T2) = Big (Double_Uns'(Xhi * Ylo))
1805                               + Big (Double_Uns'(Xlo * Yhi)));
1806       Lemma_Mult_Distribution (Big_2xxSingle, Big (Double_Uns'(Xhi * Ylo)),
1807                                               Big (Double_Uns'(Xlo * Yhi)));
1808       pragma Assert (Mult = Big_2xxSingle * Big (T2) + Big (T1));
1809       Lemma_Add_Commutation (T2, Hi (T1));
1810       pragma Assert
1811         (Big (T2 + Hi (T1)) = Big (T2) + Big (Double_Uns (Hi (T1))));
1812
1813       T2 := T2 + Hi (T1);
1814
1815       Lemma_Hi_Lo (T1, Hi (T1), Lo (T1));
1816       pragma Assert
1817         (Mult = Big_2xxSingle * Big (T2) + Big (Double_Uns (Lo (T1))));
1818
1819       if Hi (T2) /= 0 then
1820          Prove_Result_Too_Large;
1821          Raise_Error;
1822       end if;
1823
1824       Prove_Final_Decomposition;
1825
1826       T2 := Lo (T2) & Lo (T1);
1827
1828       pragma Assert (Mult = Big (T2));
1829
1830       if X >= 0 then
1831          if Y >= 0 then
1832             Prove_Pos_Int;
1833             return To_Pos_Int (T2);
1834             pragma Annotate (CodePeer, Intentional, "precondition",
1835                              "Intentional Unsigned->Signed conversion");
1836          else
1837             Prove_Neg_Int;
1838             Lemma_Abs_Range (Big (X) * Big (Y));
1839             return To_Neg_Int (T2);
1840          end if;
1841       else -- X < 0
1842          if Y < 0 then
1843             Prove_Pos_Int;
1844             return To_Pos_Int (T2);
1845             pragma Annotate (CodePeer, Intentional, "precondition",
1846                              "Intentional Unsigned->Signed conversion");
1847          else
1848             Prove_Neg_Int;
1849             Lemma_Abs_Range (Big (X) * Big (Y));
1850             return To_Neg_Int (T2);
1851          end if;
1852       end if;
1853
1854    end Multiply_With_Ovflo_Check;
1855
1856    -----------------
1857    -- Raise_Error --
1858    -----------------
1859
1860    procedure Raise_Error is
1861    begin
1862       raise Constraint_Error with "Double arithmetic overflow";
1863       pragma Annotate
1864         (GNATprove, Intentional, "exception might be raised",
1865          "Procedure Raise_Error is called to signal input errors");
1866    end Raise_Error;
1867
1868    -------------------
1869    -- Scaled_Divide --
1870    -------------------
1871
1872    procedure Scaled_Divide
1873      (X, Y, Z : Double_Int;
1874       Q, R    : out Double_Int;
1875       Round   : Boolean)
1876    is
1877       Xu  : constant Double_Uns := abs X;
1878       Xhi : constant Single_Uns := Hi (Xu);
1879       Xlo : constant Single_Uns := Lo (Xu);
1880
1881       Yu  : constant Double_Uns := abs Y;
1882       Yhi : constant Single_Uns := Hi (Yu);
1883       Ylo : constant Single_Uns := Lo (Yu);
1884
1885       Zu  : Double_Uns := abs Z;
1886       Zhi : Single_Uns := Hi (Zu);
1887       Zlo : Single_Uns := Lo (Zu);
1888
1889       D : array (1 .. 4) of Single_Uns with Relaxed_Initialization;
1890       --  The dividend, four digits (D(1) is high order)
1891
1892       Qd : array (1 .. 2) of Single_Uns with Relaxed_Initialization;
1893       --  The quotient digits, two digits (Qd(1) is high order)
1894
1895       S1, S2, S3 : Single_Uns;
1896       --  Value to subtract, three digits (S1 is high order)
1897
1898       Qu : Double_Uns;
1899       Ru : Double_Uns;
1900       --  Unsigned quotient and remainder
1901
1902       Mask : Single_Uns;
1903       --  Mask of bits used to compute the scaling factor below
1904
1905       Scale : Natural;
1906       --  Scaling factor used for multiple-precision divide. Dividend and
1907       --  Divisor are multiplied by 2 ** Scale, and the final remainder is
1908       --  divided by the scaling factor. The reason for this scaling is to
1909       --  allow more accurate estimation of quotient digits.
1910
1911       Shift : Natural;
1912       --  Shift factor used to compute the scaling factor above
1913
1914       T1, T2, T3 : Double_Uns;
1915       --  Temporary values
1916
1917       --  Local ghost variables
1918
1919       Mult  : constant Big_Natural := abs (Big (X) * Big (Y)) with Ghost;
1920       Quot  : Big_Integer with Ghost;
1921       Big_R : Big_Integer with Ghost;
1922       Big_Q : Big_Integer with Ghost;
1923       Inter : Natural with Ghost;
1924
1925       --  Local ghost functions
1926
1927       function Is_Mult_Decomposition
1928         (D1, D2, D3, D4 : Big_Integer)
1929          return Boolean
1930       is
1931         (Mult = Big_2xxSingle * Big_2xxSingle * Big_2xxSingle * D1
1932                               + Big_2xxSingle * Big_2xxSingle * D2
1933                                               + Big_2xxSingle * D3
1934                                                               + D4)
1935       with Ghost;
1936
1937       function Is_Scaled_Mult_Decomposition
1938         (D1, D2, D3, D4 : Big_Integer)
1939          return Boolean
1940       is
1941         (Mult * Big_2xx (Scale)
1942            = Big_2xxSingle * Big_2xxSingle * Big_2xxSingle * D1
1943                            + Big_2xxSingle * Big_2xxSingle * D2
1944                                            + Big_2xxSingle * D3
1945                                                            + D4)
1946       with
1947         Ghost,
1948         Pre  => Scale < Double_Size;
1949
1950       --  Local lemmas
1951
1952       procedure Prove_Dividend_Scaling
1953       with
1954         Ghost,
1955         Pre  => D'Initialized
1956           and then Scale <= Single_Size
1957           and then Is_Mult_Decomposition (Big (Double_Uns (D (1))),
1958                                           Big (Double_Uns (D (2))),
1959                                           Big (Double_Uns (D (3))),
1960                                           Big (Double_Uns (D (4))))
1961           and then Big (D (1) & D (2)) * Big_2xx (Scale) < Big_2xxDouble
1962           and then T1 = Shift_Left (D (1) & D (2), Scale)
1963           and then T2 = Shift_Left (Double_Uns (D (3)), Scale)
1964           and then T3 = Shift_Left (Double_Uns (D (4)), Scale),
1965         Post => Is_Scaled_Mult_Decomposition
1966           (Big (Double_Uns (Hi (T1))),
1967            Big (Double_Uns (Lo (T1) or Hi (T2))),
1968            Big (Double_Uns (Lo (T2) or Hi (T3))),
1969            Big (Double_Uns (Lo (T3))));
1970       --  Proves the scaling of the 4-digit dividend actually multiplies it by
1971       --  2**Scale.
1972
1973       procedure Prove_Multiplication (Q : Single_Uns)
1974       with
1975         Ghost,
1976         Pre  => T1 = Q * Lo (Zu)
1977           and then T2 = Q * Hi (Zu)
1978           and then S3 = Lo (T1)
1979           and then T3 = Hi (T1) + Lo (T2)
1980           and then S2 = Lo (T3)
1981           and then S1 = Hi (T3) + Hi (T2),
1982         Post => Big3 (S1, S2, S3) = Big (Double_Uns (Q)) * Big (Zu);
1983       --  Proves correctness of the multiplication of divisor by quotient to
1984       --  compute amount to subtract.
1985
1986       procedure Prove_Mult_Decomposition_Split3
1987         (D1, D2, D3, D3_Hi, D3_Lo, D4 : Big_Integer)
1988       with
1989         Ghost,
1990         Pre  => Is_Mult_Decomposition (D1, D2, D3, D4)
1991           and then D3 = Big_2xxSingle * D3_Hi + D3_Lo,
1992         Post => Is_Mult_Decomposition (D1, D2 + D3_Hi, D3_Lo, D4);
1993       --  Proves decomposition of Mult after splitting third component
1994
1995       procedure Prove_Negative_Dividend
1996       with
1997         Ghost,
1998         Pre  => Z /= 0
1999           and then Big (Qu) = abs Big_Q
2000           and then In_Double_Int_Range (Big_Q)
2001           and then Big (Ru) = abs Big_R
2002           and then ((X >= 0 and Y < 0) or (X < 0 and Y >= 0))
2003           and then Big_Q =
2004             (if Round then Round_Quotient (Big (X) * Big (Y), Big (Z),
2005                                            Big (X) * Big (Y) / Big (Z),
2006                                            Big (X) * Big (Y) rem Big (Z))
2007              else Big (X) * Big (Y) / Big (Z))
2008           and then Big_R = Big (X) * Big (Y) rem Big (Z),
2009          Post =>
2010            (if Z > 0 then Big_Q <= Big_0
2011               and then In_Double_Int_Range (-Big (Qu))
2012             else Big_Q >= Big_0
2013               and then In_Double_Int_Range (Big (Qu)))
2014            and then In_Double_Int_Range (-Big (Ru));
2015       --  Proves the sign of rounded quotient when dividend is non-positive
2016
2017       procedure Prove_Overflow
2018       with
2019         Ghost,
2020         Pre  => Z /= 0
2021           and then Mult >= Big_2xxDouble * Big (Double_Uns'(abs Z)),
2022         Post => not In_Double_Int_Range (Big (X) * Big (Y) / Big (Z))
2023           and then not In_Double_Int_Range
2024             (Round_Quotient (Big (X) * Big (Y), Big (Z),
2025                              Big (X) * Big (Y) / Big (Z),
2026                              Big (X) * Big (Y) rem Big (Z)));
2027       --  Proves overflow case when the quotient has at least 3 digits
2028
2029       procedure Prove_Positive_Dividend
2030       with
2031         Ghost,
2032         Pre  => Z /= 0
2033           and then Big (Qu) = abs Big_Q
2034           and then In_Double_Int_Range (Big_Q)
2035           and then Big (Ru) = abs Big_R
2036           and then ((X >= 0 and Y >= 0) or (X < 0 and Y < 0))
2037           and then Big_Q =
2038             (if Round then Round_Quotient (Big (X) * Big (Y), Big (Z),
2039                                            Big (X) * Big (Y) / Big (Z),
2040                                            Big (X) * Big (Y) rem Big (Z))
2041              else Big (X) * Big (Y) / Big (Z))
2042           and then Big_R = Big (X) * Big (Y) rem Big (Z),
2043         Post =>
2044            (if Z > 0 then Big_Q >= Big_0
2045               and then In_Double_Int_Range (Big (Qu))
2046             else Big_Q <= Big_0
2047               and then In_Double_Int_Range (-Big (Qu)))
2048            and then In_Double_Int_Range (Big (Ru));
2049       --  Proves the sign of rounded quotient when dividend is non-negative
2050
2051       procedure Prove_Qd_Calculation_Part_1 (J : Integer)
2052       with
2053         Ghost,
2054         Pre  => J in 1 .. 2
2055           and then D'Initialized
2056           and then D (J) < Zhi
2057           and then Hi (Zu) = Zhi
2058           and then Qd (J)'Initialized
2059           and then Qd (J) = Lo ((D (J) & D (J + 1)) / Zhi),
2060         Post => Big (Double_Uns (Qd (J))) >=
2061           Big3 (D (J), D (J + 1), D (J + 2)) / Big (Zu);
2062       --  When dividing 3 digits by 2 digits, proves the initial calculation
2063       --  of the quotient given by dividing the first 2 digits of the dividend
2064       --  by the first digit of the divisor is not an underestimate (so
2065       --  readjusting down works).
2066
2067       procedure Prove_Q_Too_Big
2068       with
2069         Ghost,
2070         Pre  => In_Double_Int_Range (Big_Q)
2071           and then abs Big_Q = Big_2xxDouble,
2072         Post => False;
2073       --  Proves the inconsistency when Q is equal to Big_2xx64
2074
2075       procedure Prove_Rescaling
2076       with
2077         Ghost,
2078         Pre  => Scale <= Single_Size
2079           and then Z /= 0
2080           and then Mult * Big_2xx (Scale) = Big (Zu) * Big (Qu) + Big (Ru)
2081           and then Big (Ru) < Big (Zu)
2082           and then Big (Zu) = Big (Double_Uns'(abs Z)) * Big_2xx (Scale)
2083           and then Quot = Big (X) * Big (Y) / Big (Z)
2084           and then Big_R = Big (X) * Big (Y) rem Big (Z),
2085         Post => abs Quot = Big (Qu)
2086           and then abs Big_R = Big (Shift_Right (Ru, Scale));
2087       --  Proves scaling back only the remainder is the right thing to do after
2088       --  computing the scaled division.
2089
2090       procedure Prove_Rounding_Case
2091       with
2092         Ghost,
2093         Pre  => Z /= 0
2094           and then Quot = Big (X) * Big (Y) / Big (Z)
2095           and then Big_R = Big (X) * Big (Y) rem Big (Z)
2096           and then Big_Q =
2097             Round_Quotient (Big (X) * Big (Y), Big (Z), Quot, Big_R)
2098           and then Big (Ru) = abs Big_R
2099           and then Big (Zu) = Big (Double_Uns'(abs Z)),
2100         Post => abs Big_Q =
2101           (if Ru > (Zu - Double_Uns'(1)) / Double_Uns'(2)
2102            then abs Quot + 1
2103            else abs Quot);
2104       --  Proves correctness of the rounding of the unsigned quotient
2105
2106       procedure Prove_Scaled_Mult_Decomposition_Regroup24
2107         (D1, D2, D3, D4 : Big_Integer)
2108       with
2109         Ghost,
2110         Pre  => Scale < Double_Size
2111           and then Is_Scaled_Mult_Decomposition (D1, D2, D3, D4),
2112         Post => Is_Scaled_Mult_Decomposition
2113           (0, Big_2xxSingle * D1 + D2, 0, Big_2xxSingle * D3 + D4);
2114       --  Proves scaled decomposition of Mult after regrouping on second and
2115       --  fourth component.
2116
2117       procedure Prove_Scaled_Mult_Decomposition_Regroup3
2118         (D1, D2, D3, D4 : Big_Integer)
2119       with
2120         Ghost,
2121         Pre  => Scale < Double_Size
2122           and then Is_Scaled_Mult_Decomposition (D1, D2, D3, D4),
2123         Post => Is_Scaled_Mult_Decomposition (0, 0, Big3 (D1, D2, D3), D4);
2124       --  Proves scaled decomposition of Mult after regrouping on third
2125       --  component.
2126
2127       procedure Prove_Sign_R
2128       with
2129         Ghost,
2130         Pre  => Z /= 0 and then Big_R = Big (X) * Big (Y) rem Big (Z),
2131         Post => In_Double_Int_Range (Big_R);
2132
2133       procedure Prove_Signs
2134       with
2135         Ghost,
2136         Pre  => Z /= 0
2137           and then Quot = Big (X) * Big (Y) / Big (Z)
2138           and then Big_R = Big (X) * Big (Y) rem Big (Z)
2139           and then Big_Q =
2140             (if Round then
2141                Round_Quotient (Big (X) * Big (Y), Big (Z), Quot, Big_R)
2142              else Quot)
2143           and then Big (Ru) = abs Big_R
2144           and then Big (Qu) = abs Big_Q
2145           and then In_Double_Int_Range (Big_Q)
2146           and then In_Double_Int_Range (Big_R)
2147           and then R =
2148             (if (X >= 0) = (Y >= 0) then To_Pos_Int (Ru) else To_Neg_Int (Ru))
2149           and then Q =
2150             (if ((X >= 0) = (Y >= 0)) = (Z >= 0) then To_Pos_Int (Qu)
2151              else To_Neg_Int (Qu)),  --  need to ensure To_Pos_Int precondition
2152         Post => Big (R) = Big_R and then Big (Q) = Big_Q;
2153       --  Proves final signs match the intended result after the unsigned
2154       --  division is done.
2155
2156       procedure Prove_Z_Low
2157       with
2158         Ghost,
2159         Pre  => Z /= 0
2160           and then D'Initialized
2161           and then Hi (abs Z) = 0
2162           and then Lo (abs Z) = Zlo
2163           and then Mult =
2164             Big_2xxSingle * Big_2xxSingle * Big (Double_Uns (D (2)))
2165                           + Big_2xxSingle * Big (Double_Uns (D (3)))
2166                                           + Big (Double_Uns (D (4)))
2167           and then D (2) < Zlo
2168           and then Quot = (Big (X) * Big (Y)) / Big (Z)
2169           and then Big_R = (Big (X) * Big (Y)) rem Big (Z)
2170           and then T1 = D (2) & D (3)
2171           and then T2 = Lo (T1 rem Zlo) & D (4)
2172           and then Qu = Lo (T1 / Zlo) & Lo (T2 / Zlo)
2173           and then Ru = T2 rem Zlo,
2174         Post => Big (Qu) = abs Quot
2175           and then Big (Ru) = abs Big_R;
2176       --  Proves the case where the divisor is only one digit
2177
2178       ----------------------------
2179       -- Prove_Dividend_Scaling --
2180       ----------------------------
2181
2182       procedure Prove_Dividend_Scaling is
2183          Big_D12 : constant Big_Integer :=
2184            Big_2xx (Scale) * Big (D (1) & D (2));
2185          Big_T1  : constant Big_Integer := Big (T1);
2186          Big_D3  : constant Big_Integer :=
2187            Big_2xx (Scale) * Big (Double_Uns (D (3)));
2188          Big_T2  : constant Big_Integer := Big (T2);
2189          Big_D4  : constant Big_Integer :=
2190            Big_2xx (Scale) * Big (Double_Uns (D (4)));
2191          Big_T3  : constant Big_Integer := Big (T3);
2192
2193       begin
2194          Lemma_Shift_Left (D (1) & D (2), Scale);
2195          Lemma_Ge_Mult (Big_2xxSingle, Big_2xx (Scale), Big_2xxSingle,
2196                         Big_2xxSingle * Big_2xx (Scale));
2197          Lemma_Lt_Mult (Big (Double_Uns (D (3))), Big_2xxSingle,
2198                         Big_2xx (Scale), Big_2xxDouble);
2199          Lemma_Shift_Left (Double_Uns (D (3)), Scale);
2200          Lemma_Lt_Mult (Big (Double_Uns (D (4))), Big_2xxSingle,
2201                         Big_2xx (Scale), Big_2xxDouble);
2202          Lemma_Shift_Left (Double_Uns (D (4)), Scale);
2203          Lemma_Hi_Lo (D (1) & D (2), D (1), D (2));
2204          pragma Assert (Mult * Big_2xx (Scale) =
2205            Big_2xxSingle * Big_2xxSingle * Big_D12
2206                          + Big_2xxSingle * Big_D3
2207                                          + Big_D4);
2208          pragma Assert (Big_2xx (Scale) > 0);
2209          declare
2210             Two_xx_Scale : constant Double_Uns := Double_Uns'(2 ** Scale);
2211             D12          : constant Double_Uns := D (1) & D (2);
2212          begin
2213             pragma Assert (Big_2xx (Scale) * Big (D12) < Big_2xxDouble);
2214             pragma Assert (Big (Two_xx_Scale) * Big (D12) < Big_2xxDouble);
2215             Lemma_Mult_Commutation (Two_xx_Scale, D12, T1);
2216          end;
2217          pragma Assert (Big_D12 = Big_T1);
2218          pragma Assert (Big_2xxSingle * Big_2xxSingle * Big_D12
2219                         = Big_2xxSingle * Big_2xxSingle * Big_T1);
2220          Lemma_Mult_Commutation (2 ** Scale, Double_Uns (D (3)), T2);
2221          pragma Assert (Big_D3 = Big_T2);
2222          pragma Assert (Big_2xxSingle * Big_D3 = Big_2xxSingle * Big_T2);
2223          Lemma_Mult_Commutation (2 ** Scale, Double_Uns (D (4)), T3);
2224          pragma Assert (Big_D4 = Big_T3);
2225          pragma Assert
2226            (By (Is_Scaled_Mult_Decomposition (0, Big_T1, Big_T2, Big_T3),
2227             By (Big_2xxSingle * Big_2xxSingle * Big_D12 =
2228                 Big_2xxSingle * Big_2xxSingle * Big_T1,
2229                 Big_D12 = Big_T1)
2230               and then
2231             By (Big_2xxSingle * Big_D3  = Big_2xxSingle * Big_T2,
2232                 Big_D3 = Big_T2)
2233               and then
2234             Big_D4 = Big_T3));
2235          Lemma_Hi_Lo (T1, Hi (T1), Lo (T1));
2236          Lemma_Hi_Lo (T2, Hi (T2), Lo (T2));
2237          Lemma_Hi_Lo (T3, Hi (T3), Lo (T3));
2238          Lemma_Mult_Distribution (Big_2xxSingle * Big_2xxSingle,
2239                                   Big_2xxSingle * Big (Double_Uns (Hi (T1))),
2240                                   Big (Double_Uns (Lo (T1))));
2241          Lemma_Mult_Distribution (Big_2xxSingle,
2242                                   Big_2xxSingle * Big (Double_Uns (Hi (T2))),
2243                                   Big (Double_Uns (Lo (T2))));
2244          Lemma_Mult_Distribution (Big_2xxSingle * Big_2xxSingle,
2245                                   Big (Double_Uns (Lo (T1))),
2246                                   Big (Double_Uns (Hi (T2))));
2247          Lemma_Mult_Distribution (Big_2xxSingle,
2248                                   Big (Double_Uns (Lo (T2))),
2249                                   Big (Double_Uns (Hi (T3))));
2250          pragma Assert
2251            (By (Is_Scaled_Mult_Decomposition
2252               (Big (Double_Uns (Hi (T1))),
2253                Big (Double_Uns (Lo (T1))) + Big (Double_Uns (Hi (T2))),
2254                Big (Double_Uns (Lo (T2))) + Big (Double_Uns (Hi (T3))),
2255                Big (Double_Uns (Lo (T3)))),
2256             --  Start from stating equality between the expanded values of
2257             --  the right-hand side in the known and desired assertions over
2258             --  Is_Scaled_Mult_Decomposition.
2259             By (Big_2xxSingle * Big_2xxSingle * Big_2xxSingle *
2260               Big (Double_Uns (Hi (T1)))
2261             + Big_2xxSingle * Big_2xxSingle *
2262               (Big (Double_Uns (Lo (T1))) + Big (Double_Uns (Hi (T2))))
2263             + Big_2xxSingle *
2264               (Big (Double_Uns (Lo (T2))) + Big (Double_Uns (Hi (T3))))
2265             + Big (Double_Uns (Lo (T3))) =
2266               Big_2xxSingle * Big_2xxSingle * Big_2xxSingle * 0
2267             + Big_2xxSingle * Big_2xxSingle * Big_T1
2268             + Big_2xxSingle * Big_T2
2269             + Big_T3,
2270               --  Now list all known equalities that contribute
2271               Big_2xxSingle * Big_2xxSingle * Big_2xxSingle *
2272               Big (Double_Uns (Hi (T1)))
2273             + Big_2xxSingle * Big_2xxSingle *
2274               (Big (Double_Uns (Lo (T1))) + Big (Double_Uns (Hi (T2))))
2275             + Big_2xxSingle *
2276               (Big (Double_Uns (Lo (T2))) + Big (Double_Uns (Hi (T3))))
2277             + Big (Double_Uns (Lo (T3))) =
2278               Big_2xxSingle * Big_2xxSingle * Big_2xxSingle *
2279                 Big (Double_Uns (Hi (T1)))
2280             + Big_2xxSingle * Big_2xxSingle * Big (Double_Uns (Lo (T1)))
2281             + Big_2xxSingle * Big_2xxSingle * Big (Double_Uns (Hi (T2)))
2282             + Big_2xxSingle * Big (Double_Uns (Lo (T2)))
2283             + Big_2xxSingle * Big (Double_Uns (Hi (T3)))
2284             + Big (Double_Uns (Lo (T3)))
2285               and then
2286             By (Big_2xxSingle * Big_2xxSingle * Big (T1)
2287             = Big_2xxSingle * Big_2xxSingle * Big_2xxSingle
2288             * Big (Double_Uns (Hi (T1)))
2289             + Big_2xxSingle * Big_2xxSingle * Big (Double_Uns (Lo (T1))),
2290             Big_2xxSingle * Big_2xxSingle * Big (T1)
2291             = Big_2xxSingle * Big_2xxSingle
2292             * (Big_2xxSingle * Big (Double_Uns (Hi (T1)))
2293                + Big (Double_Uns (Lo (T1)))))
2294               and then
2295             By (Big_2xxSingle * Big (T2)
2296             = Big_2xxSingle * Big_2xxSingle * Big (Double_Uns (Hi (T2)))
2297             + Big_2xxSingle * Big (Double_Uns (Lo (T2))),
2298             Big_2xxSingle * Big (T2)
2299             = Big_2xxSingle * (Big_2xxSingle * Big (Double_Uns (Hi (T2)))
2300               + Big (Double_Uns (Lo (T2)))))
2301               and then
2302             Big (T3) = Big_2xxSingle * Big (Double_Uns (Hi (T3)))
2303             + Big (Double_Uns (Lo (T3))))));
2304          Lemma_Mult_Distribution (Big_2xxSingle * Big_2xxSingle,
2305                                   Big (Double_Uns (Lo (T1))),
2306                                   Big (Double_Uns (Hi (T2))));
2307          pragma Assert (Double_Uns (Lo (T1) or Hi (T2)) =
2308                           Double_Uns (Lo (T1)) + Double_Uns (Hi (T2)));
2309          pragma Assert (Double_Uns (Lo (T2) or Hi (T3)) =
2310                           Double_Uns (Lo (T2)) + Double_Uns (Hi (T3)));
2311          Lemma_Add_Commutation (Double_Uns (Lo (T1)), Hi (T2));
2312          Lemma_Add_Commutation (Double_Uns (Lo (T2)), Hi (T3));
2313          pragma Assert
2314            (By (Is_Scaled_Mult_Decomposition
2315               (Big (Double_Uns (Hi (T1))),
2316                Big (Double_Uns (Lo (T1) or Hi (T2))),
2317                Big (Double_Uns (Lo (T2) or Hi (T3))),
2318                Big (Double_Uns (Lo (T3)))),
2319             By (Big_2xxSingle * Big_2xxSingle
2320               * Big (Double_Uns (Lo (T1) or Hi (T2))) =
2321                 Big_2xxSingle * Big_2xxSingle * Big (Double_Uns (Lo (T1)))
2322               + Big_2xxSingle * Big_2xxSingle * Big (Double_Uns (Hi (T2))),
2323               Big_2xxSingle * Big_2xxSingle
2324               * Big (Double_Uns (Lo (T1)) + Double_Uns (Hi (T2))) =
2325                 Big_2xxSingle * Big_2xxSingle
2326               * (Big (Double_Uns (Lo (T1))) + Big (Double_Uns (Hi (T2)))))
2327               and then
2328             Big_2xxSingle * Big (Double_Uns (Lo (T2) or Hi (T3))) =
2329             Big_2xxSingle * Big (Double_Uns (Lo (T2)))
2330             + Big_2xxSingle * Big (Double_Uns (Hi (T3)))));
2331       end Prove_Dividend_Scaling;
2332
2333       --------------------------
2334       -- Prove_Multiplication --
2335       --------------------------
2336
2337       procedure Prove_Multiplication (Q : Single_Uns) is
2338       begin
2339          Lemma_Hi_Lo (Zu, Hi (Zu), Lo (Zu));
2340          Lemma_Hi_Lo (T1, Hi (T1), S3);
2341          Lemma_Hi_Lo (T2, Hi (T2), Lo (T2));
2342          Lemma_Hi_Lo (T3, Hi (T3), S2);
2343          Lemma_Mult_Commutation (Double_Uns (Q), Double_Uns (Lo (Zu)), T1);
2344          Lemma_Mult_Commutation (Double_Uns (Q), Double_Uns (Hi (Zu)), T2);
2345          pragma Assert (Big (Double_Uns (Q)) * Big (Zu) =
2346                           Big_2xxSingle * Big (T2) + Big (T1));
2347          pragma Assert (Big (Double_Uns (Q)) * Big (Zu) =
2348            Big_2xxSingle * Big_2xxSingle * Big (Double_Uns (Hi (T2)))
2349          + Big_2xxSingle * Big_2xxSingle * Big (Double_Uns (Hi (T3)))
2350                          + Big_2xxSingle * Big (Double_Uns (S2))
2351                                          + Big (Double_Uns (S3)));
2352          pragma Assert (Double_Uns (Hi (T3)) + Hi (T2) = Double_Uns (S1));
2353          Lemma_Add_Commutation (Double_Uns (Hi (T3)), Hi (T2));
2354          pragma Assert
2355            (Big (Double_Uns (Hi (T3))) + Big (Double_Uns (Hi (T2))) =
2356               Big (Double_Uns (S1)));
2357          Lemma_Mult_Distribution (Big_2xxSingle * Big_2xxSingle,
2358                                   Big (Double_Uns (Hi (T3))),
2359                                   Big (Double_Uns (Hi (T2))));
2360          pragma Assert
2361            (Big_2xxSingle * Big_2xxSingle * Big (Double_Uns (Hi (T2)))
2362             + Big_2xxSingle * Big_2xxSingle * Big (Double_Uns (Hi (T3)))
2363             = Big_2xxSingle * Big_2xxSingle * Big (Double_Uns (S1)));
2364          pragma Assert (Big (Double_Uns (Q)) * Big (Zu) =
2365            Big_2xxSingle * Big_2xxSingle * Big (Double_Uns (S1))
2366                          + Big_2xxSingle * Big (Double_Uns (S2))
2367                                          + Big (Double_Uns (S3)));
2368          pragma Assert
2369            (By (Big (Double_Uns (Q)) * Big (Zu) = Big3 (S1, S2, S3),
2370               Big3 (S1, S2, S3) =
2371                 Big_2xxSingle * Big_2xxSingle * Big (Double_Uns (S1))
2372                               + Big_2xxSingle * Big (Double_Uns (S2))
2373                                               + Big (Double_Uns (S3))));
2374       end Prove_Multiplication;
2375
2376       -------------------------------------
2377       -- Prove_Mult_Decomposition_Split3 --
2378       -------------------------------------
2379
2380       procedure Prove_Mult_Decomposition_Split3
2381         (D1, D2, D3, D3_Hi, D3_Lo, D4 : Big_Integer)
2382       is null;
2383
2384       -----------------------------
2385       -- Prove_Negative_Dividend --
2386       -----------------------------
2387
2388       procedure Prove_Negative_Dividend is
2389       begin
2390          Lemma_Mult_Non_Positive (Big (X), Big (Y));
2391       end Prove_Negative_Dividend;
2392
2393       --------------------
2394       -- Prove_Overflow --
2395       --------------------
2396
2397       procedure Prove_Overflow is
2398       begin
2399          Lemma_Div_Ge (Mult, Big_2xxDouble, Big (Double_Uns'(abs Z)));
2400          Lemma_Abs_Commutation (Z);
2401          Lemma_Abs_Div_Commutation (Big (X) * Big (Y), Big (Z));
2402       end Prove_Overflow;
2403
2404       -----------------------------
2405       -- Prove_Positive_Dividend --
2406       -----------------------------
2407
2408       procedure Prove_Positive_Dividend is
2409       begin
2410          Lemma_Mult_Non_Negative (Big (X), Big (Y));
2411       end Prove_Positive_Dividend;
2412
2413       ---------------------------------
2414       -- Prove_Qd_Calculation_Part_1 --
2415       ---------------------------------
2416
2417       procedure Prove_Qd_Calculation_Part_1 (J : Integer) is
2418       begin
2419          Lemma_Hi_Lo (D (J) & D (J + 1), D (J), D (J + 1));
2420          Lemma_Lt_Commutation (Double_Uns (D (J)), Double_Uns (Zhi));
2421          Lemma_Gt_Mult (Big (Double_Uns (Zhi)),
2422                         Big (Double_Uns (D (J))) + 1,
2423                         Big_2xxSingle, Big (D (J) & D (J + 1)));
2424          Lemma_Div_Lt
2425            (Big (D (J) & D (J + 1)), Big_2xxSingle, Big (Double_Uns (Zhi)));
2426          Lemma_Div_Commutation (D (J) & D (J + 1), Double_Uns (Zhi));
2427          Lemma_Lo_Is_Ident ((D (J) & D (J + 1)) / Zhi);
2428          Lemma_Div_Definition (D (J) & D (J + 1), Zhi, Double_Uns (Qd (J)),
2429                                (D (J) & D (J + 1)) rem Zhi);
2430          Lemma_Lt_Commutation
2431            ((D (J) & D (J + 1)) rem Zhi, Double_Uns (Zhi));
2432          Lemma_Gt_Mult
2433            ((Big (Double_Uns (Qd (J))) + 1) * Big (Double_Uns (Zhi)),
2434             Big (D (J) & D (J + 1)) + 1, Big_2xxSingle,
2435             Big3 (D (J), D (J + 1), D (J + 2)));
2436          Lemma_Hi_Lo (Zu, Zhi, Lo (Zu));
2437          Lemma_Gt_Mult (Big (Zu), Big_2xxSingle * Big (Double_Uns (Zhi)),
2438                         Big (Double_Uns (Qd (J))) + 1,
2439                         Big3 (D (J), D (J + 1), D (J + 2)));
2440          Lemma_Div_Lt (Big3 (D (J), D (J + 1), D (J + 2)),
2441                        Big (Double_Uns (Qd (J))) + 1, Big (Zu));
2442       end Prove_Qd_Calculation_Part_1;
2443
2444       ---------------------
2445       -- Prove_Q_Too_Big --
2446       ---------------------
2447
2448       procedure Prove_Q_Too_Big is
2449       begin
2450          pragma Assert (Big_Q = Big_2xxDouble or Big_Q = -Big_2xxDouble);
2451          Lemma_Not_In_Range_Big2xx64;
2452       end Prove_Q_Too_Big;
2453
2454       ---------------------
2455       -- Prove_Rescaling --
2456       ---------------------
2457
2458       procedure Prove_Rescaling is
2459       begin
2460          Lemma_Div_Lt (Big (Ru), Big (Double_Uns'(abs Z)), Big_2xx (Scale));
2461          Lemma_Div_Eq (Mult, Big (Double_Uns'(abs Z)) * Big (Qu),
2462                        Big_2xx (Scale), Big (Ru));
2463          Lemma_Rev_Div_Definition (Mult, Big (Double_Uns'(abs Z)),
2464                                    Big (Qu), Big (Ru) / Big_2xx (Scale));
2465          Lemma_Abs_Div_Commutation (Big (X) * Big (Y), Big (Z));
2466          Lemma_Abs_Rem_Commutation (Big (X) * Big (Y), Big (Z));
2467          Lemma_Abs_Commutation (Z);
2468          Lemma_Shift_Right (Ru, Scale);
2469       end Prove_Rescaling;
2470
2471       -------------------------
2472       -- Prove_Rounding_Case --
2473       -------------------------
2474
2475       procedure Prove_Rounding_Case is
2476       begin
2477          if Same_Sign (Big (X) * Big (Y), Big (Z)) then
2478             null;
2479          end if;
2480       end Prove_Rounding_Case;
2481
2482       -----------------------------------------------
2483       -- Prove_Scaled_Mult_Decomposition_Regroup24 --
2484       -----------------------------------------------
2485
2486       procedure Prove_Scaled_Mult_Decomposition_Regroup24
2487         (D1, D2, D3, D4 : Big_Integer)
2488       is null;
2489
2490       ----------------------------------------------
2491       -- Prove_Scaled_Mult_Decomposition_Regroup3 --
2492       ----------------------------------------------
2493
2494       procedure Prove_Scaled_Mult_Decomposition_Regroup3
2495         (D1, D2, D3, D4 : Big_Integer)
2496       is null;
2497
2498       ------------------
2499       -- Prove_Sign_R --
2500       ------------------
2501
2502       procedure Prove_Sign_R is
2503       begin
2504          pragma Assert (In_Double_Int_Range (Big (Z)));
2505       end Prove_Sign_R;
2506
2507       -----------------
2508       -- Prove_Signs --
2509       -----------------
2510
2511       procedure Prove_Signs is null;
2512
2513       -----------------
2514       -- Prove_Z_Low --
2515       -----------------
2516
2517       procedure Prove_Z_Low is
2518       begin
2519          Lemma_Hi_Lo (T1, D (2), D (3));
2520          Lemma_Add_Commutation (Double_Uns (D (2)), 1);
2521          pragma Assert
2522            (Big (Double_Uns (D (2))) + 1 <= Big (Double_Uns (Zlo)));
2523          Lemma_Div_Definition (T1, Zlo, T1 / Zlo, T1 rem Zlo);
2524          pragma Assert (Double_Uns (Lo (T1 rem Zlo)) = T1 rem Zlo);
2525          Lemma_Hi_Lo (T2, Lo (T1 rem Zlo), D (4));
2526          pragma Assert (T1 rem Zlo < Double_Uns (Zlo));
2527          pragma Assert (T1 rem Zlo + Double_Uns'(1) <= Double_Uns (Zlo));
2528          Lemma_Ge_Commutation (Double_Uns (Zlo), T1 rem Zlo + Double_Uns'(1));
2529          Lemma_Add_Commutation (T1 rem Zlo, 1);
2530          pragma Assert (Big (T1 rem Zlo) + 1 <= Big (Double_Uns (Zlo)));
2531          Lemma_Div_Definition (T2, Zlo, T2 / Zlo, Ru);
2532          pragma Assert
2533            (Mult = Big (Double_Uns (Zlo)) *
2534               (Big_2xxSingle * Big (T1 / Zlo) + Big (T2 / Zlo)) + Big (Ru));
2535          pragma Assert (Big_2xxSingle * Big (Double_Uns (D (2)))
2536                                       + Big (Double_Uns (D (3)))
2537                         < Big_2xxSingle * (Big (Double_Uns (D (2))) + 1));
2538          Lemma_Div_Lt (Big (T1), Big_2xxSingle, Big (Double_Uns (Zlo)));
2539          Lemma_Div_Commutation (T1, Double_Uns (Zlo));
2540          Lemma_Lo_Is_Ident (T1 / Zlo);
2541          pragma Assert
2542            (Big (T2) <= Big_2xxSingle * (Big (Double_Uns (Zlo)) - 1)
2543                                       + Big (Double_Uns (D (4))));
2544          Lemma_Div_Lt (Big (T2), Big_2xxSingle, Big (Double_Uns (Zlo)));
2545          Lemma_Div_Commutation (T2, Double_Uns (Zlo));
2546          Lemma_Lo_Is_Ident (T2 / Zlo);
2547          Lemma_Hi_Lo (Qu, Lo (T1 / Zlo), Lo (T2 / Zlo));
2548          Lemma_Substitution (Mult, Big (Double_Uns (Zlo)),
2549                              Big_2xxSingle * Big (T1 / Zlo) + Big (T2 / Zlo),
2550                              Big (Qu), Big (Ru));
2551          Lemma_Lt_Commutation (Ru, Double_Uns (Zlo));
2552          Lemma_Rev_Div_Definition
2553            (Mult, Big (Double_Uns (Zlo)), Big (Qu), Big (Ru));
2554          pragma Assert (Double_Uns (Zlo) = abs Z);
2555          Lemma_Abs_Commutation (Z);
2556          Lemma_Abs_Div_Commutation (Big (X) * Big (Y), Big (Z));
2557          Lemma_Abs_Rem_Commutation (Big (X) * Big (Y), Big (Z));
2558       end Prove_Z_Low;
2559
2560    --  Start of processing for Scaled_Divide
2561
2562    begin
2563       if Z = 0 then
2564          Raise_Error;
2565       end if;
2566
2567       Quot := Big (X) * Big (Y) / Big (Z);
2568       Big_R := Big (X) * Big (Y) rem Big (Z);
2569       if Round then
2570          Big_Q := Round_Quotient (Big (X) * Big (Y), Big (Z), Quot, Big_R);
2571       else
2572          Big_Q := Quot;
2573       end if;
2574
2575       --  First do the multiplication, giving the four digit dividend
2576
2577       Lemma_Abs_Mult_Commutation (Big (X), Big (Y));
2578       Lemma_Abs_Commutation (X);
2579       Lemma_Abs_Commutation (Y);
2580       Lemma_Mult_Decomposition (Mult, Xu, Yu, Xhi, Xlo, Yhi, Ylo);
2581       pragma Assert
2582         (Is_Mult_Decomposition
2583            (D1 => 0,
2584             D2 => Big (Double_Uns'(Xhi * Yhi)),
2585             D3 => Big (Double_Uns'(Xhi * Ylo)) + Big (Double_Uns'(Xlo * Yhi)),
2586             D4 => Big (Double_Uns'(Xlo * Ylo))));
2587
2588       T1 := Xlo * Ylo;
2589       D (4) := Lo (T1);
2590       D (3) := Hi (T1);
2591
2592       Lemma_Hi_Lo (T1, D (3), D (4));
2593       pragma Assert
2594         (Is_Mult_Decomposition
2595            (D1 => 0,
2596             D2 => Big (Double_Uns'(Xhi * Yhi)),
2597             D3 => Big (Double_Uns'(Xhi * Ylo)) + Big (Double_Uns'(Xlo * Yhi))
2598               + Big (Double_Uns (D (3))),
2599             D4 => Big (Double_Uns (D (4)))));
2600
2601       if Yhi /= 0 then
2602          T1 := Xlo * Yhi;
2603
2604          Lemma_Hi_Lo (T1, Hi (T1), Lo (T1));
2605          pragma Assert
2606            (Is_Mult_Decomposition
2607               (D1 => 0,
2608                D2 => Big (Double_Uns'(Xhi * Yhi)) + Big (Double_Uns (Hi (T1))),
2609                D3 => Big (Double_Uns'(Xhi * Ylo)) + Big (Double_Uns (Lo (T1)))
2610                  + Big (Double_Uns (D (3))),
2611                D4 => Big (Double_Uns (D (4)))));
2612
2613          T2 := D (3) + Lo (T1);
2614
2615          Lemma_Add_Commutation (Double_Uns (Lo (T1)), D (3));
2616          pragma Assert
2617            (Is_Mult_Decomposition
2618               (D1 => 0,
2619                D2 => Big (Double_Uns'(Xhi * Yhi)) + Big (Double_Uns (Hi (T1))),
2620                D3 => Big (Double_Uns'(Xhi * Ylo)) + Big (T2),
2621                D4 => Big (Double_Uns (D (4)))));
2622          Lemma_Mult_Distribution (Big_2xxSingle,
2623                                   Big (Double_Uns (D (3))),
2624                                   Big (Double_Uns (Lo (T1))));
2625          Lemma_Hi_Lo (T2, Hi (T2), Lo (T2));
2626          pragma Assert
2627            (Is_Mult_Decomposition
2628               (D1 => 0,
2629                D2 => Big (Double_Uns'(Xhi * Yhi)) + Big (Double_Uns (Hi (T1)))
2630                  + Big (Double_Uns (Hi (T2))),
2631                D3 => Big (Double_Uns'(Xhi * Ylo)) + Big (Double_Uns (Lo (T2))),
2632                D4 => Big (Double_Uns (D (4)))));
2633
2634          D (3) := Lo (T2);
2635          D (2) := Hi (T1) + Hi (T2);
2636
2637          pragma Assert (Double_Uns (Hi (T1)) + Hi (T2) = Double_Uns (D (2)));
2638          Lemma_Add_Commutation (Double_Uns (Hi (T1)), Hi (T2));
2639          pragma Assert
2640            (Big (Double_Uns (Hi (T1))) + Big (Double_Uns (Hi (T2))) =
2641               Big (Double_Uns (D (2))));
2642          pragma Assert
2643            (Is_Mult_Decomposition
2644               (D1 => 0,
2645                D2 => Big (Double_Uns'(Xhi * Yhi)) + Big (Double_Uns (D (2))),
2646                D3 => Big (Double_Uns'(Xhi * Ylo)) + Big (Double_Uns (D (3))),
2647                D4 => Big (Double_Uns (D (4)))));
2648
2649          if Xhi /= 0 then
2650             T1 := Xhi * Ylo;
2651
2652             Lemma_Hi_Lo (T1, Hi (T1), Lo (T1));
2653             pragma Assert
2654               (By (Is_Mult_Decomposition
2655                  (D1 => 0,
2656                   D2 => Big (Double_Uns'(Xhi * Yhi)) + Big (Double_Uns (D (2)))
2657                     + Big (Double_Uns (Hi (T1))),
2658                   D3 => Big (Double_Uns (Lo (T1))) + Big (Double_Uns (D (3))),
2659                   D4 => Big (Double_Uns (D (4)))),
2660                (By (Big_2xxSingle * Big (T1) =
2661                     Big_2xxSingle * Big_2xxSingle * Big (Double_Uns (Hi (T1)))
2662                     + Big_2xxSingle * Big (Double_Uns (Lo (T1))),
2663                     Big_2xxSingle * Big (T1) =
2664                     Big_2xxSingle * (Big_2xxSingle * Big (Double_Uns (Hi (T1)))
2665                     + Big (Double_Uns (Lo (T1))))))));
2666
2667             T2 := D (3) + Lo (T1);
2668
2669             Lemma_Add_Commutation (Double_Uns (D (3)), Lo (T1));
2670             Lemma_Hi_Lo (T2, Hi (T2), Lo (T2));
2671             Prove_Mult_Decomposition_Split3
2672               (D1    => 0,
2673                D2    => Big (Double_Uns'(Xhi * Yhi)) + Big (Double_Uns (D (2)))
2674                  + Big (Double_Uns (Hi (T1))),
2675                D3    => Big (T2),
2676                D3_Hi => Big (Double_Uns (Hi (T2))),
2677                D3_Lo => Big (Double_Uns (Lo (T2))),
2678                D4    => Big (Double_Uns (D (4))));
2679
2680             D (3) := Lo (T2);
2681             T3 := D (2) + Hi (T1);
2682
2683             Lemma_Add_Commutation (Double_Uns (D (2)), Hi (T1));
2684             pragma Assert
2685               (Is_Mult_Decomposition
2686                  (D1 => 0,
2687                   D2 => Big (Double_Uns'(Xhi * Yhi)) + Big (T3)
2688                     + Big (Double_Uns (Hi (T2))),
2689                   D3 => Big (Double_Uns (D (3))),
2690                   D4 => Big (Double_Uns (D (4)))));
2691             Lemma_Add_Commutation (T3, Hi (T2));
2692
2693             T3 := T3 + Hi (T2);
2694             T2 := Double_Uns'(Xhi * Yhi);
2695
2696             pragma Assert
2697               (Is_Mult_Decomposition
2698                  (D1 => 0,
2699                   D2 => Big (T2) + Big (T3),
2700                   D3 => Big (Double_Uns (D (3))),
2701                   D4 => Big (Double_Uns (D (4)))));
2702             Lemma_Hi_Lo (T2, Hi (T2), Lo (T2));
2703             pragma Assert
2704               (By (Is_Mult_Decomposition
2705                  (D1 => Big (Double_Uns (Hi (T2))),
2706                   D2 => Big (Double_Uns (Lo (T2))) + Big (T3),
2707                   D3 => Big (Double_Uns (D (3))),
2708                   D4 => Big (Double_Uns (D (4)))),
2709                By (Big_2xxSingle * Big_2xxSingle * Big (T2) =
2710                    Big_2xxSingle * Big_2xxSingle * Big_2xxSingle
2711                  * Big (Double_Uns (Hi (T2)))
2712                  + Big_2xxSingle * Big_2xxSingle * Big (Double_Uns (Lo (T2))),
2713                Big_2xxSingle * Big_2xxSingle *
2714                  (Big_2xxSingle * Big (Double_Uns (Hi (T2)))
2715                                 + Big (Double_Uns (Lo (T2))))
2716                  = Big_2xxSingle * Big_2xxSingle * Big_2xxSingle
2717                      * Big (Double_Uns (Hi (T2)))
2718                    + Big_2xxSingle * Big_2xxSingle
2719                      * Big (Double_Uns (Lo (T2))))));
2720
2721             T1 := T3 + Lo (T2);
2722             D (2) := Lo (T1);
2723
2724             Lemma_Add_Commutation (T3, Lo (T2));
2725             pragma Assert
2726               (Is_Mult_Decomposition
2727                  (D1 => Big (Double_Uns (Hi (T2))),
2728                   D2 => Big (T1),
2729                   D3 => Big (Double_Uns (D (3))),
2730                   D4 => Big (Double_Uns (D (4)))));
2731             Lemma_Hi_Lo (T1, Hi (T1), Lo (T1));
2732             pragma Assert
2733               (By (Is_Mult_Decomposition
2734                 (D1 => Big (Double_Uns (Hi (T2))) + Big (Double_Uns (Hi (T1))),
2735                  D2 => Big (Double_Uns (D (2))),
2736                  D3 => Big (Double_Uns (D (3))),
2737                  D4 => Big (Double_Uns (D (4)))),
2738                By (Big_2xxSingle * Big_2xxSingle * Big (Double_Uns (Lo (T1))) =
2739                    Big_2xxSingle * Big_2xxSingle * Big (Double_Uns (D (2))),
2740                    D (2) = Lo (T1))
2741                  and then
2742                By (Big_2xxSingle * Big_2xxSingle * Big (T1) =
2743                    Big_2xxSingle * Big_2xxSingle * Big_2xxSingle
2744                  * Big (Double_Uns (Hi (T1)))
2745                  + Big_2xxSingle * Big_2xxSingle * Big (Double_Uns (Lo (T1))),
2746                Big_2xxSingle * Big_2xxSingle *
2747                  (Big_2xxSingle * Big (Double_Uns (Hi (T1)))
2748                                 + Big (Double_Uns (Lo (T1))))
2749                  = Big_2xxSingle * Big_2xxSingle * Big_2xxSingle
2750                      * Big (Double_Uns (Hi (T1)))
2751                    + Big_2xxSingle * Big_2xxSingle
2752                      * Big (Double_Uns (Lo (T1))))));
2753
2754             D (1) := Hi (T2) + Hi (T1);
2755
2756             pragma Assert
2757               (Double_Uns (Hi (T2)) + Hi (T1) = Double_Uns (D (1)));
2758             Lemma_Add_Commutation (Double_Uns (Hi (T2)), Hi (T1));
2759             pragma Assert
2760               (Big (Double_Uns (Hi (T2))) + Big (Double_Uns (Hi (T1))) =
2761                    Big (Double_Uns (D (1))));
2762
2763             pragma Assert
2764               (By (Is_Mult_Decomposition
2765                  (D1 => Big (Double_Uns (D (1))),
2766                   D2 => Big (Double_Uns (D (2))),
2767                   D3 => Big (Double_Uns (D (3))),
2768                   D4 => Big (Double_Uns (D (4)))),
2769                Big_2xxSingle * Big_2xxSingle * Big_2xxSingle *
2770                  Big (Double_Uns (D (1)))
2771                = Big_2xxSingle * Big_2xxSingle * Big_2xxSingle *
2772                  (Big (Double_Uns (Hi (T2)) + Double_Uns (Hi (T1))))));
2773          else
2774             D (1) := 0;
2775
2776             pragma Assert
2777               (By (Is_Mult_Decomposition
2778                  (D1 => Big (Double_Uns (D (1))),
2779                   D2 => Big (Double_Uns (D (2))),
2780                   D3 => Big (Double_Uns (D (3))),
2781                   D4 => Big (Double_Uns (D (4)))),
2782                Big (Double_Uns'(Xhi * Yhi)) = 0
2783                  and then Big (Double_Uns'(Xhi * Ylo)) = 0
2784                  and then Big (Double_Uns (D (1))) = 0));
2785          end if;
2786
2787          pragma Assert
2788            (Is_Mult_Decomposition (D1 => Big (Double_Uns (D (1))),
2789                                    D2 => Big (Double_Uns (D (2))),
2790                                    D3 => Big (Double_Uns (D (3))),
2791                                    D4 => Big (Double_Uns (D (4)))));
2792       else
2793          pragma Assert
2794            (By (Is_Mult_Decomposition
2795               (D1 => 0,
2796                D2 => 0,
2797                D3 => Big (Double_Uns'(Xhi * Ylo)) + Big (Double_Uns (D (3))),
2798                D4 => Big (Double_Uns (D (4)))),
2799             Big (Double_Uns'(Xhi * Yhi)) = 0
2800               and then Big (Double_Uns'(Xlo * Yhi)) = 0));
2801
2802          if Xhi /= 0 then
2803             T1 := Xhi * Ylo;
2804
2805             Lemma_Hi_Lo (T1, Hi (T1), Lo (T1));
2806             pragma Assert
2807               (By (Is_Mult_Decomposition
2808                  (D1 => 0,
2809                   D2 => Big (Double_Uns (Hi (T1))),
2810                   D3 => Big (Double_Uns (Lo (T1))) + Big (Double_Uns (D (3))),
2811                   D4 => Big (Double_Uns (D (4)))),
2812                Big_2xxSingle * Big (Double_Uns'(Xhi * Ylo)) =
2813                  Big_2xxSingle * Big_2xxSingle * Big (Double_Uns (Hi (T1)))
2814                    + Big_2xxSingle * Big (Double_Uns (Lo (T1)))));
2815
2816             T2 := D (3) + Lo (T1);
2817
2818             Lemma_Add_Commutation (Double_Uns (Lo (T1)), D (3));
2819             pragma Assert
2820               (By (Is_Mult_Decomposition
2821                  (D1 => 0,
2822                   D2 => Big (Double_Uns (Hi (T1))),
2823                   D3 => Big (T2),
2824                   D4 => Big (Double_Uns (D (4)))),
2825                Big_2xxSingle * Big (T2) =
2826                  Big_2xxSingle *
2827                    (Big (Double_Uns (Lo (T1))) + Big (Double_Uns (D (3))))));
2828             Lemma_Mult_Distribution (Big_2xxSingle,
2829                                      Big (Double_Uns (D (3))),
2830                                      Big (Double_Uns (Lo (T1))));
2831             Lemma_Hi_Lo (T2, Hi (T2), Lo (T2));
2832
2833             D (3) := Lo (T2);
2834             D (2) := Hi (T1) + Hi (T2);
2835
2836             pragma Assert
2837               (Double_Uns (Hi (T1)) + Hi (T2) = Double_Uns (D (2)));
2838             Lemma_Add_Commutation (Double_Uns (Hi (T1)), Hi (T2));
2839             pragma Assert
2840               (Big (Double_Uns (Hi (T1))) + Big (Double_Uns (Hi (T2))) =
2841                  Big (Double_Uns (D (2))));
2842             pragma Assert
2843               (Is_Mult_Decomposition
2844                  (D1 => 0,
2845                   D2 => Big (Double_Uns (D (2))),
2846                   D3 => Big (Double_Uns (D (3))),
2847                   D4 => Big (Double_Uns (D (4)))));
2848          else
2849             D (2) := 0;
2850
2851             pragma Assert
2852               (By (Is_Mult_Decomposition
2853                  (D1 => 0,
2854                   D2 => Big (Double_Uns (D (2))),
2855                   D3 => Big (Double_Uns (D (3))),
2856                   D4 => Big (Double_Uns (D (4)))),
2857                Big (Double_Uns'(Xhi * Ylo)) = 0
2858                  and then Big (Double_Uns (D (2))) = 0));
2859          end if;
2860
2861          D (1) := 0;
2862       end if;
2863
2864       pragma Assert (Is_Mult_Decomposition (D1 => Big (Double_Uns (D (1))),
2865                                             D2 => Big (Double_Uns (D (2))),
2866                                             D3 => Big (Double_Uns (D (3))),
2867                                             D4 => Big (Double_Uns (D (4)))));
2868
2869       --  Now it is time for the dreaded multiple precision division. First an
2870       --  easy case, check for the simple case of a one digit divisor.
2871
2872       if Zhi = 0 then
2873          if D (1) /= 0 or else D (2) >= Zlo then
2874             if D (1) > 0 then
2875                pragma Assert
2876                  (Mult >= Big_2xxSingle * Big_2xxSingle * Big_2xxSingle
2877                           * Big (Double_Uns (D (1))));
2878                Lemma_Double_Big_2xxSingle;
2879                Lemma_Mult_Positive (Big_2xxDouble, Big_2xxSingle);
2880                Lemma_Ge_Mult (Big (Double_Uns (D (1))),
2881                               1,
2882                               Big_2xxDouble * Big_2xxSingle,
2883                               Big_2xxDouble * Big_2xxSingle);
2884                Lemma_Mult_Positive (Big_2xxSingle, Big (Double_Uns (D (1))));
2885                Lemma_Ge_Mult (Big_2xxSingle * Big_2xxSingle, Big_2xxDouble,
2886                               Big_2xxSingle * Big (Double_Uns (D (1))),
2887                               Big_2xxDouble * Big_2xxSingle);
2888                pragma Assert (Mult >= Big_2xxDouble * Big_2xxSingle);
2889                Lemma_Ge_Commutation (2 ** Single_Size, Zu);
2890                Lemma_Ge_Mult (Big_2xxSingle, Big (Zu), Big_2xxDouble,
2891                               Big_2xxDouble * Big (Zu));
2892                pragma Assert (Mult >= Big_2xxDouble * Big (Zu));
2893             else
2894                Lemma_Ge_Commutation (Double_Uns (D (2)), Zu);
2895                pragma Assert (Mult >= Big_2xxDouble * Big (Zu));
2896             end if;
2897
2898             Prove_Overflow;
2899             Raise_Error;
2900
2901          --  Here we are dividing at most three digits by one digit
2902
2903          else
2904             T1 := D (2) & D (3);
2905             T2 := Lo (T1 rem Zlo) & D (4);
2906
2907             Qu := Lo (T1 / Zlo) & Lo (T2 / Zlo);
2908             Ru := T2 rem Zlo;
2909
2910             Prove_Z_Low;
2911          end if;
2912
2913       --  If divisor is double digit and dividend is too large, raise error
2914
2915       elsif (D (1) & D (2)) >= Zu then
2916          Lemma_Hi_Lo (D (1) & D (2), D (1), D (2));
2917          Lemma_Ge_Commutation (D (1) & D (2), Zu);
2918          Prove_Overflow;
2919          Raise_Error;
2920
2921       --  This is the complex case where we definitely have a double digit
2922       --  divisor and a dividend of at least three digits. We use the classical
2923       --  multiple-precision division algorithm (see section (4.3.1) of Knuth's
2924       --  "The Art of Computer Programming", Vol. 2 for a description
2925       --  (algorithm D).
2926
2927       else
2928          --  First normalize the divisor so that it has the leading bit on.
2929          --  We do this by finding the appropriate left shift amount.
2930
2931          Lemma_Lt_Commutation (D (1) & D (2), Zu);
2932          pragma Assert (Mult < Big_2xxDouble * Big (Zu));
2933
2934          Shift := Single_Size;
2935          Mask  := Single_Uns'Last;
2936          Scale := 0;
2937
2938          Inter := 0;
2939          pragma Assert (Big_2xx (Scale) = 1);
2940
2941          while Shift > 1 loop
2942             pragma Loop_Invariant (Scale <= Single_Size - Shift);
2943             pragma Loop_Invariant ((Hi (Zu) and Mask) /= 0);
2944             pragma Loop_Invariant
2945               (Mask = Shift_Left (Single_Uns'Last, Single_Size - Shift));
2946             pragma Loop_Invariant (Zu = Shift_Left (abs Z, Scale));
2947             pragma Loop_Invariant (Big (Zu) =
2948               Big (Double_Uns'(abs Z)) * Big_2xx (Scale));
2949             pragma Loop_Invariant (Inter in 0 .. Log_Single_Size - 1);
2950             pragma Loop_Invariant (Shift = 2 ** (Log_Single_Size - Inter));
2951             pragma Loop_Invariant (Shift mod 2 = 0);
2952
2953             declare
2954                --  Local ghost variables
2955
2956                Shift_Prev : constant Natural := Shift with Ghost;
2957                Mask_Prev  : constant Single_Uns := Mask with Ghost;
2958                Zu_Prev    : constant Double_Uns := Zu with Ghost;
2959
2960                --  Local lemmas
2961
2962                procedure Prove_Power
2963                with
2964                  Ghost,
2965                  Pre  => Inter in 0 .. Log_Single_Size - 1
2966                    and then Shift = 2 ** (Log_Single_Size - Inter),
2967                  Post => Shift / 2 = 2 ** (Log_Single_Size - (Inter + 1))
2968                    and then (Shift = 2 or (Shift / 2) mod 2 = 0);
2969
2970                procedure Prove_Prev_And_Mask (Prev, Mask : Single_Uns)
2971                with
2972                  Ghost,
2973                  Pre  => Prev /= 0
2974                    and then (Prev and Mask) = 0,
2975                  Post => (Prev and not Mask) /= 0;
2976
2977                procedure Prove_Shift_Progress
2978                with
2979                  Ghost,
2980                  Pre  => Shift <= Single_Size / 2
2981                    and then Shift_Prev = 2 * Shift
2982                    and then Mask_Prev =
2983                      Shift_Left (Single_Uns'Last, Single_Size - Shift_Prev)
2984                    and then Mask =
2985                      Shift_Left (Single_Uns'Last,
2986                                  Single_Size - Shift_Prev + Shift),
2987                  Post => Mask_Prev =
2988                      Shift_Left (Single_Uns'Last, Single_Size - 2 * Shift)
2989                    and then Mask =
2990                      Shift_Left (Single_Uns'Last, Single_Size - Shift);
2991
2992                procedure Prove_Shifting
2993                with
2994                  Ghost,
2995                  Pre  => Shift <= Single_Size / 2
2996                    and then Zu = Shift_Left (Zu_Prev, Shift)
2997                    and then Mask_Prev =
2998                      Shift_Left (Single_Uns'Last, Single_Size - 2 * Shift)
2999                    and then Mask =
3000                      Shift_Left (Single_Uns'Last, Single_Size - Shift)
3001                    and then (Hi (Zu_Prev) and Mask_Prev and not Mask) /= 0,
3002                  Post => (Hi (Zu) and Mask) /= 0;
3003
3004                -----------------------------
3005                -- Local lemma null bodies --
3006                -----------------------------
3007
3008                procedure Prove_Prev_And_Mask (Prev, Mask : Single_Uns) is null;
3009                procedure Prove_Power is null;
3010                procedure Prove_Shifting is null;
3011                procedure Prove_Shift_Progress is null;
3012
3013             begin
3014                pragma Assert (Mask = Shift_Left (Single_Uns'Last,
3015                               Single_Size - Shift_Prev));
3016                Prove_Power;
3017
3018                Shift := Shift / 2;
3019
3020                Inter := Inter + 1;
3021                pragma Assert (Shift_Prev = 2 * Shift);
3022
3023                Mask := Shift_Left (Mask, Shift);
3024
3025                Lemma_Double_Shift
3026                  (Single_Uns'Last, Single_Size - Shift_Prev, Shift);
3027                Prove_Shift_Progress;
3028
3029                if (Hi (Zu) and Mask) = 0 then
3030                   Zu := Shift_Left (Zu, Shift);
3031
3032                   pragma Assert ((Hi (Zu_Prev) and Mask_Prev) /= 0);
3033                   pragma Assert
3034                     (By ((Hi (Zu_Prev) and Mask_Prev and Mask) = 0,
3035                      (Hi (Zu_Prev) and Mask) = 0
3036                      and then
3037                      (Hi (Zu_Prev) and Mask_Prev and Mask)
3038                      = (Hi (Zu_Prev) and Mask and Mask_Prev)
3039                     ));
3040                   Prove_Prev_And_Mask (Hi (Zu_Prev) and Mask_Prev, Mask);
3041                   Prove_Shifting;
3042                   pragma Assert (Big (Zu_Prev) =
3043                     Big (Double_Uns'(abs Z)) * Big_2xx (Scale));
3044                   Lemma_Shift_Without_Drop (Zu_Prev, Zu, Mask, Shift);
3045                   Lemma_Substitution
3046                     (Big (Zu), Big_2xx (Shift),
3047                      Big (Zu_Prev), Big (Double_Uns'(abs Z)) * Big_2xx (Scale),
3048                      0);
3049                   Lemma_Powers_Of_2 (Shift, Scale);
3050                   Lemma_Substitution
3051                     (Big (Zu), Big (Double_Uns'(abs Z)),
3052                      Big_2xx (Shift) * Big_2xx (Scale),
3053                      Big_2xx (Shift + Scale), 0);
3054                   Lemma_Double_Shift (abs Z, Scale, Shift);
3055
3056                   Scale := Scale + Shift;
3057
3058                   pragma Assert (Zu = Shift_Left (abs Z, Scale));
3059                   pragma Assert
3060                     (Big (Zu) = Big (Double_Uns'(abs Z)) * Big_2xx (Scale));
3061                end if;
3062
3063                pragma Assert
3064                  (Big (Zu) = Big (Double_Uns'(abs Z)) * Big_2xx (Scale));
3065             end;
3066          end loop;
3067
3068          Zhi := Hi (Zu);
3069          Zlo := Lo (Zu);
3070
3071          pragma Assert (Shift = 1);
3072          pragma Assert (Mask = Shift_Left (Single_Uns'Last, Single_Size - 1));
3073          pragma Assert ((Zhi and Mask) /= 0);
3074          pragma Assert (Zhi >= 2 ** (Single_Size - 1));
3075          pragma Assert (Big (Zu) = Big (Double_Uns'(abs Z)) * Big_2xx (Scale));
3076          --  We have Hi (Zu) /= 0 before normalization. The sequence of
3077          --  Shift_Left operations results in the leading bit of Zu being 1 by
3078          --  moving the leftmost 1-bit in Zu to leading position, thus
3079          --  Zhi = Hi (Zu) >= 2 ** (Single_Size - 1) here.
3080
3081          --  Note that when we scale up the dividend, it still fits in four
3082          --  digits, since we already tested for overflow, and scaling does
3083          --  not change the invariant that (D (1) & D (2)) < Zu.
3084
3085          Lemma_Lt_Commutation (D (1) & D (2), abs Z);
3086          Lemma_Big_Of_Double_Uns (Zu);
3087          Lemma_Lt_Mult (Big (D (1) & D (2)),
3088                         Big (Double_Uns'(abs Z)), Big_2xx (Scale),
3089                         Big_2xxDouble);
3090
3091          T1 := Shift_Left (D (1) & D (2), Scale);
3092          T2 := Shift_Left (Double_Uns (D (3)), Scale);
3093          T3 := Shift_Left (Double_Uns (D (4)), Scale);
3094
3095          Prove_Dividend_Scaling;
3096
3097          D (1) := Hi (T1);
3098          D (2) := Lo (T1) or Hi (T2);
3099          D (3) := Lo (T2) or Hi (T3);
3100          D (4) := Lo (T3);
3101
3102          pragma Assert (Big (Double_Uns (Hi (T1))) = Big (Double_Uns (D (1))));
3103          pragma Assert
3104            (Big_2xxSingle * Big_2xxSingle * Big_2xxSingle
3105             * Big (Double_Uns (Hi (T1)))
3106             = Big_2xxSingle * Big_2xxSingle * Big_2xxSingle
3107             * Big (Double_Uns (D (1))));
3108          Lemma_Substitution (Big_2xxDouble * Big (Zu), Big_2xxDouble, Big (Zu),
3109                              Big (Double_Uns'(abs Z)) * Big_2xx (Scale), 0);
3110          Lemma_Lt_Mult (Mult, Big_2xxDouble * Big (Double_Uns'(abs Z)),
3111                         Big_2xx (Scale), Big_2xxDouble * Big (Zu));
3112          pragma Assert (Mult >= Big_0);
3113          pragma Assert (Big_2xx (Scale) >= Big_0);
3114          Lemma_Mult_Non_Negative (Mult, Big_2xx (Scale));
3115          Lemma_Div_Lt (Mult * Big_2xx (Scale), Big (Zu), Big_2xxDouble);
3116          Lemma_Concat_Definition (D (1), D (2));
3117          Lemma_Double_Big_2xxSingle;
3118          Prove_Scaled_Mult_Decomposition_Regroup24
3119            (Big (Double_Uns (D (1))),
3120             Big (Double_Uns (D (2))),
3121             Big (Double_Uns (D (3))),
3122             Big (Double_Uns (D (4))));
3123          Lemma_Substitution
3124            (Mult * Big_2xx (Scale), Big_2xxSingle * Big_2xxSingle,
3125               Big_2xxSingle * Big (Double_Uns (D (1)))
3126                             + Big (Double_Uns (D (2))),
3127               Big (D (1) & D (2)),
3128               Big_2xxSingle * Big (Double_Uns (D (3)))
3129                             + Big (Double_Uns (D (4))));
3130          pragma Assert (Big (D (1) & D (2)) < Big (Zu));
3131
3132          --  Loop to compute quotient digits, runs twice for Qd (1) and Qd (2)
3133
3134          declare
3135             --  Local lemmas
3136
3137             procedure Prove_First_Iteration (X1, X2, X3, X4 : Single_Uns)
3138             with
3139               Ghost,
3140               Pre  => X1 = 0,
3141               Post =>
3142                 Big_2xxSingle * Big3 (X1, X2, X3) + Big (Double_Uns (X4))
3143                   = Big3 (X2, X3, X4);
3144
3145             ---------------------------
3146             -- Prove_First_Iteration --
3147             ---------------------------
3148
3149             procedure Prove_First_Iteration (X1, X2, X3, X4 : Single_Uns) is
3150             null;
3151
3152             --  Local ghost variables
3153
3154             Qd1  : Single_Uns := 0 with Ghost;
3155             D234 : Big_Integer := 0 with Ghost;
3156             D123 : constant Big_Integer := Big3 (D (1), D (2), D (3))
3157               with Ghost;
3158             D4   : constant Big_Integer := Big (Double_Uns (D (4)))
3159               with Ghost;
3160
3161          begin
3162             Prove_Scaled_Mult_Decomposition_Regroup3
3163               (Big (Double_Uns (D (1))),
3164                Big (Double_Uns (D (2))),
3165                Big (Double_Uns (D (3))),
3166                Big (Double_Uns (D (4))));
3167             pragma Assert (Mult * Big_2xx (Scale) = Big_2xxSingle * D123 + D4);
3168
3169             for J in 1 .. 2 loop
3170                Lemma_Hi_Lo (D (J) & D (J + 1), D (J), D (J + 1));
3171                pragma Assert (Big (D (J) & D (J + 1)) < Big (Zu));
3172
3173                --  Compute next quotient digit. We have to divide three digits
3174                --  by two digits. We estimate the quotient by dividing the
3175                --  leading two digits by the leading digit. Given the scaling
3176                --  we did above which ensured the first bit of the divisor is
3177                --  set, this gives an estimate of the quotient that is at most
3178                --  two too high.
3179
3180                if D (J) > Zhi then
3181                   Lemma_Lt_Commutation (Zu, D (J) & D (J + 1));
3182                   pragma Assert (False);
3183
3184                elsif D (J) = Zhi then
3185                   Qd (J) := Single_Uns'Last;
3186
3187                   Lemma_Concat_Definition (D (J), D (J + 1));
3188                   Lemma_Big_Of_Double_Uns_Of_Single_Uns (D (J + 2));
3189                   pragma Assert (Big_2xxSingle > Big (Double_Uns (D (J + 2))));
3190                   pragma Assert (Big3 (D (J), D (J + 1), 0) + Big_2xxSingle
3191                                  > Big3 (D (J), D (J + 1), D (J + 2)));
3192                   pragma Assert (Big (Double_Uns'(0)) = 0);
3193                   pragma Assert (Big (D (J) & D (J + 1)) * Big_2xxSingle =
3194                     Big_2xxSingle * (Big_2xxSingle * Big (Double_Uns (D (J)))
3195                                               + Big (Double_Uns (D (J + 1)))));
3196                   pragma Assert (Big (D (J) & D (J + 1)) * Big_2xxSingle =
3197                     Big_2xxSingle * Big_2xxSingle * Big (Double_Uns (D (J)))
3198                                + Big_2xxSingle * Big (Double_Uns (D (J + 1))));
3199                   pragma Assert (Big (D (J) & D (J + 1)) * Big_2xxSingle
3200                                  = Big3 (D (J), D (J + 1), 0));
3201                   pragma Assert ((Big (D (J) & D (J + 1)) + 1) * Big_2xxSingle
3202                                  = Big3 (D (J), D (J + 1), 0) + Big_2xxSingle);
3203                   Lemma_Gt_Mult (Big (Zu), Big (D (J) & D (J + 1)) + 1,
3204                                  Big_2xxSingle,
3205                                  Big3 (D (J), D (J + 1), D (J + 2)));
3206                   Lemma_Div_Lt
3207                     (Big3 (D (J), D (J + 1), D (J + 2)),
3208                      Big_2xxSingle, Big (Zu));
3209                   pragma Assert (Big (Double_Uns (Qd (J))) >=
3210                     Big3 (D (J), D (J + 1), D (J + 2)) / Big (Zu));
3211
3212                else
3213                   Qd (J) := Lo ((D (J) & D (J + 1)) / Zhi);
3214
3215                   Prove_Qd_Calculation_Part_1 (J);
3216                end if;
3217
3218                pragma Assert (for all K in 1 .. J => Qd (K)'Initialized);
3219                Lemma_Gt_Mult
3220                  (Big (Double_Uns (Qd (J))),
3221                   Big3 (D (J), D (J + 1), D (J + 2)) / Big (Zu),
3222                   Big (Zu), Big3 (D (J), D (J + 1), D (J + 2)) - Big (Zu));
3223
3224                --  Compute amount to subtract
3225
3226                T1 := Qd (J) * Zlo;
3227                T2 := Qd (J) * Zhi;
3228                S3 := Lo (T1);
3229                T3 := Hi (T1) + Lo (T2);
3230                S2 := Lo (T3);
3231                S1 := Hi (T3) + Hi (T2);
3232
3233                Prove_Multiplication (Qd (J));
3234
3235                --  Adjust quotient digit if it was too high
3236
3237                --  We use the version of the algorithm in the 2nd Edition
3238                --  of "The Art of Computer Programming". This had a bug not
3239                --  discovered till 1995, see Vol 2 errata:
3240                --     http://www-cs-faculty.stanford.edu/~uno/err2-2e.ps.gz.
3241                --  Under rare circumstances the expression in the test could
3242                --  overflow. This version was further corrected in 2005, see
3243                --  Vol 2 errata:
3244                --     http://www-cs-faculty.stanford.edu/~uno/all2-pre.ps.gz.
3245                --  This implementation is not impacted by these bugs, due
3246                --  to the use of a word-size comparison done in function Le3
3247                --  instead of a comparison on two-word integer quantities in
3248                --  the original algorithm.
3249
3250                Lemma_Hi_Lo_3 (Zu, Zhi, Zlo);
3251
3252                while not Le3 (S1, S2, S3, D (J), D (J + 1), D (J + 2)) loop
3253                   pragma Loop_Invariant
3254                     (for all K in 1 .. J => Qd (K)'Initialized);
3255                   pragma Loop_Invariant (if J = 2 then Qd (1) = Qd1);
3256                   pragma Loop_Invariant
3257                     (Big3 (S1, S2, S3) = Big (Double_Uns (Qd (J))) * Big (Zu));
3258                   pragma Loop_Invariant
3259                     (Big3 (S1, S2, S3) > Big3 (D (J), D (J + 1), D (J + 2)));
3260                   pragma Assert (Big3 (S1, S2, S3) > 0);
3261                   if Qd (J) = 0 then
3262                      pragma Assert (Big3 (S1, S2, S3) = 0);
3263                      pragma Assert (False);
3264                   end if;
3265                   Lemma_Ge_Commutation (Double_Uns (Qd (J)), 1);
3266                   Lemma_Ge_Mult
3267                     (Big (Double_Uns (Qd (J))), 1, Big (Zu), Big (Zu));
3268
3269                   Sub3 (S1, S2, S3, 0, Zhi, Zlo);
3270
3271                   pragma Assert
3272                     (Big3 (S1, S2, S3) >
3273                        Big3 (D (J), D (J + 1), D (J + 2)) - Big (Zu));
3274                   Lemma_Subtract_Commutation (Double_Uns (Qd (J)), 1);
3275                   pragma Assert (Double_Uns (Qd (J)) - Double_Uns'(1)
3276                                  = Double_Uns (Qd (J) - 1));
3277                   pragma Assert (Big (Double_Uns'(1)) = 1);
3278                   Lemma_Substitution (Big3 (S1, S2, S3), Big (Zu),
3279                                       Big (Double_Uns (Qd (J))) - 1,
3280                                       Big (Double_Uns (Qd (J) - 1)), 0);
3281
3282                   declare
3283                      Prev : constant Single_Uns := Qd (J) - 1 with Ghost;
3284                   begin
3285                      Qd (J) := Qd (J) - 1;
3286
3287                      pragma Assert (Qd (J) = Prev);
3288                   end;
3289
3290                   pragma Assert
3291                     (Big3 (S1, S2, S3) = Big (Double_Uns (Qd (J))) * Big (Zu));
3292                end loop;
3293
3294                --  Now subtract S1&S2&S3 from D1&D2&D3 ready for next step
3295
3296                pragma Assert (for all K in 1 .. J => Qd (K)'Initialized);
3297                pragma Assert
3298                  (Big3 (S1, S2, S3) = Big (Double_Uns (Qd (J))) * Big (Zu));
3299                pragma Assert (Big3 (S1, S2, S3) >
3300                                 Big3 (D (J), D (J + 1), D (J + 2)) - Big (Zu));
3301                Inline_Le3 (S1, S2, S3, D (J), D (J + 1), D (J + 2));
3302
3303                Sub3 (D (J), D (J + 1), D (J + 2), S1, S2, S3);
3304
3305                pragma Assert (Big3 (D (J), D (J + 1), D (J + 2)) < Big (Zu));
3306                if D (J) > 0 then
3307                   Lemma_Double_Big_2xxSingle;
3308                   pragma Assert (Big3 (D (J), D (J + 1), D (J + 2)) =
3309                     Big_2xxSingle
3310                       * Big_2xxSingle * Big (Double_Uns (D (J)))
3311                       + Big_2xxSingle * Big (Double_Uns (D (J + 1)))
3312                                       + Big (Double_Uns (D (J + 2))));
3313                   pragma Assert (Big_2xxSingle >= 0);
3314                   Lemma_Big_Of_Double_Uns_Of_Single_Uns (D (J + 1));
3315                   pragma Assert (Big (Double_Uns (D (J + 1))) >= 0);
3316                   Lemma_Mult_Non_Negative
3317                     (Big_2xxSingle, Big (Double_Uns (D (J + 1))));
3318                   pragma Assert
3319                     (By (Big3 (D (J), D (J + 1), D (J + 2)) >=
3320                        Big_2xxSingle * Big_2xxSingle
3321                        * Big (Double_Uns (D (J))),
3322                      By (Big3 (D (J), D (J + 1), D (J + 2))
3323                      - Big_2xxSingle * Big_2xxSingle
3324                        * Big (Double_Uns (D (J)))
3325                      = Big_2xxSingle * Big (Double_Uns (D (J + 1)))
3326                                      + Big (Double_Uns (D (J + 2))),
3327                      Big3 (D (J), D (J + 1), D (J + 2)) =
3328                        Big_2xxSingle
3329                        * Big_2xxSingle * Big (Double_Uns (D (J)))
3330                        + Big_2xxSingle * Big (Double_Uns (D (J + 1)))
3331                                        + Big (Double_Uns (D (J + 2))))
3332                        and then
3333                      By (Big_2xxSingle * Big (Double_Uns (D (J + 1)))
3334                                        + Big (Double_Uns (D (J + 2))) >= 0,
3335                      Big_2xxSingle * Big (Double_Uns (D (J + 1))) >= 0
3336                        and then
3337                      Big (Double_Uns (D (J + 2))) >= 0
3338                     )));
3339                   Lemma_Ge_Commutation (Double_Uns (D (J)), Double_Uns'(1));
3340                   Lemma_Ge_Mult (Big (Double_Uns (D (J))),
3341                                  Big (Double_Uns'(1)),
3342                                  Big_2xxDouble,
3343                                  Big (Double_Uns'(1)) * Big_2xxDouble);
3344                   pragma Assert
3345                     (Big_2xxDouble * Big (Double_Uns'(1)) = Big_2xxDouble);
3346                   pragma Assert
3347                     (Big3 (D (J), D (J + 1), D (J + 2)) >= Big_2xxDouble);
3348                   pragma Assert (False);
3349                end if;
3350
3351                if J = 1 then
3352                   Qd1 := Qd (1);
3353                   D234 := Big3 (D (2), D (3), D (4));
3354                   pragma Assert (D4 = Big (Double_Uns (D (4))));
3355                   Lemma_Substitution
3356                     (Mult * Big_2xx (Scale), Big_2xxSingle, D123,
3357                      Big3 (D (1), D (2), D (3)) + Big3 (S1, S2, S3),
3358                      Big (Double_Uns (D (4))));
3359                   Prove_First_Iteration (D (1), D (2), D (3), D (4));
3360                   Lemma_Substitution (Mult * Big_2xx (Scale), Big_2xxSingle,
3361                                       Big3 (S1, S2, S3),
3362                                       Big (Double_Uns (Qd1)) * Big (Zu),
3363                                       D234);
3364                else
3365                   pragma Assert (Qd1 = Qd (1));
3366                   pragma Assert
3367                     (By (Mult * Big_2xx (Scale) =
3368                        Big_2xxSingle * Big (Double_Uns (Qd1)) * Big (Zu)
3369                      + Big3 (S1, S2, S3)
3370                      + Big3 (D (2), D (3), D (4)),
3371                      Big3 (D (2), D (3), D (4)) = D234 - Big3 (S1, S2, S3)));
3372                   pragma Assert
3373                     (By (Mult * Big_2xx (Scale) =
3374                        Big_2xxSingle * Big (Double_Uns (Qd (1))) * Big (Zu)
3375                                      + Big (Double_Uns (Qd (2))) * Big (Zu)
3376                      + Big_2xxSingle * Big (Double_Uns (D (3)))
3377                                      + Big (Double_Uns (D (4))),
3378                      Big_2xxSingle * Big (Double_Uns (Qd (1))) * Big (Zu)
3379                        = Big_2xxSingle * Big (Double_Uns (Qd1)) * Big (Zu)
3380                        and then
3381                      Big3 (S1, S2, S3) = Big (Double_Uns (Qd (2))) * Big (Zu)
3382                        and then
3383                      By (Big3 (D (2), D (3), D (4))
3384                          = Big_2xxSingle * Big (Double_Uns (D (3)))
3385                                          + Big (Double_Uns (D (4))),
3386                         Big3 (D (2), D (3), D (4))
3387                          = Big_2xxSingle * Big_2xxSingle *
3388                            Big (Double_Uns (D (2)))
3389                            + Big_2xxSingle * Big (Double_Uns (D (3)))
3390                                            + Big (Double_Uns (D (4)))
3391                           and then
3392                        Big_2xxSingle * Big_2xxSingle * Big (Double_Uns (D (2)))
3393                         = 0)
3394                     ));
3395                end if;
3396             end loop;
3397          end;
3398
3399          --  The two quotient digits are now set, and the remainder of the
3400          --  scaled division is in D3&D4. To get the remainder for the
3401          --  original unscaled division, we rescale this dividend.
3402
3403          --  We rescale the divisor as well, to make the proper comparison
3404          --  for rounding below.
3405
3406          pragma Assert (for all K in 1 .. 2 => Qd (K)'Initialized);
3407          Qu := Qd (1) & Qd (2);
3408          Ru := D (3) & D (4);
3409
3410          pragma Assert
3411            (Mult * Big_2xx (Scale) =
3412               Big_2xxSingle * Big (Double_Uns (Qd (1))) * Big (Zu)
3413                             + Big (Double_Uns (Qd (2))) * Big (Zu)
3414             + Big_2xxSingle * Big (Double_Uns (D (3)))
3415                             + Big (Double_Uns (D (4))));
3416          Lemma_Hi_Lo (Qu, Qd (1), Qd (2));
3417          Lemma_Hi_Lo (Ru, D (3), D (4));
3418          Lemma_Substitution
3419            (Mult * Big_2xx (Scale), Big (Zu),
3420             Big_2xxSingle * Big (Double_Uns (Qd (1)))
3421               + Big (Double_Uns (Qd (2))),
3422             Big (Qu), Big (Ru));
3423          Prove_Rescaling;
3424
3425          Ru := Shift_Right (Ru, Scale);
3426
3427          Lemma_Shift_Right (Zu, Scale);
3428
3429          Zu := Shift_Right (Zu, Scale);
3430
3431          Lemma_Simplify (Big (Double_Uns'(abs Z)), Big_2xx (Scale));
3432       end if;
3433
3434       pragma Assert (Big (Ru) = abs Big_R);
3435       pragma Assert (Big (Qu) = abs Quot);
3436       pragma Assert (Big (Zu) = Big (Double_Uns'(abs Z)));
3437
3438       --  Deal with rounding case
3439
3440       if Round then
3441          Prove_Rounding_Case;
3442
3443          if Ru > (Zu - Double_Uns'(1)) / Double_Uns'(2) then
3444             pragma Assert (abs Big_Q = Big (Qu) + 1);
3445
3446             --  Protect against wrapping around when rounding, by signaling
3447             --  an overflow when the quotient is too large.
3448
3449             if Qu = Double_Uns'Last then
3450                Prove_Q_Too_Big;
3451                Raise_Error;
3452             end if;
3453
3454             Lemma_Add_One (Qu);
3455
3456             Qu := Qu + Double_Uns'(1);
3457          end if;
3458       end if;
3459
3460       pragma Assert (Big (Qu) = abs Big_Q);
3461
3462       --  Set final signs (RM 4.5.5(27-30))
3463
3464       --  Case of dividend (X * Y) sign positive
3465
3466       if (X >= 0 and then Y >= 0) or else (X < 0 and then Y < 0) then
3467          Prove_Positive_Dividend;
3468
3469          R := To_Pos_Int (Ru);
3470          Q := (if Z > 0 then To_Pos_Int (Qu) else To_Neg_Int (Qu));
3471
3472       --  Case of dividend (X * Y) sign negative
3473
3474       else
3475          Prove_Negative_Dividend;
3476
3477          R := To_Neg_Int (Ru);
3478          Q := (if Z > 0 then To_Neg_Int (Qu) else To_Pos_Int (Qu));
3479       end if;
3480
3481       Prove_Sign_R;
3482       Prove_Signs;
3483    end Scaled_Divide;
3484
3485    ----------
3486    -- Sub3 --
3487    ----------
3488
3489    procedure Sub3 (X1, X2, X3 : in out Single_Uns; Y1, Y2, Y3 : Single_Uns) is
3490
3491       --  Local ghost variables
3492
3493       XX1 : constant Single_Uns := X1 with Ghost;
3494       XX2 : constant Single_Uns := X2 with Ghost;
3495       XX3 : constant Single_Uns := X3 with Ghost;
3496
3497       --  Local lemmas
3498
3499       procedure Lemma_Add3_No_Carry (X1, X2, X3, Y1, Y2, Y3 : Single_Uns)
3500       with
3501         Ghost,
3502         Pre  => X1 <= Single_Uns'Last - Y1
3503           and then X2 <= Single_Uns'Last - Y2
3504           and then X3 <= Single_Uns'Last - Y3,
3505         Post => Big3 (X1 + Y1, X2 + Y2, X3 + Y3)
3506               = Big3 (X1, X2, X3) + Big3 (Y1, Y2, Y3);
3507
3508       procedure Lemma_Ge_Expand (X1, X2, X3, Y1, Y2, Y3 : Single_Uns)
3509       with
3510         Ghost,
3511         Pre  => Big3 (X1, X2, X3) >= Big3 (Y1, Y2, Y3),
3512         Post => X1 > Y1
3513           or else (X1 = Y1 and then X2 > Y2)
3514           or else (X1 = Y1 and then X2 = Y2 and then X3 >= Y3);
3515
3516       procedure Lemma_Sub3_No_Carry (X1, X2, X3, Y1, Y2, Y3 : Single_Uns)
3517       with
3518         Ghost,
3519         Pre  => X1 >= Y1 and then X2 >= Y2 and then X3 >= Y3,
3520         Post => Big3 (X1 - Y1, X2 - Y2, X3 - Y3)
3521               = Big3 (X1, X2, X3) - Big3 (Y1, Y2, Y3);
3522
3523       procedure Lemma_Sub3_With_Carry2 (X1, X2, X3, Y2 : Single_Uns)
3524       with
3525         Ghost,
3526         Pre  => X2 < Y2,
3527         Post => Big3 (X1, X2 - Y2, X3)
3528           = Big3 (X1, X2, X3) + Big3 (Single_Uns'(1), 0, 0) - Big3 (0, Y2, 0);
3529
3530       procedure Lemma_Sub3_With_Carry3 (X1, X2, X3, Y3 : Single_Uns)
3531       with
3532         Ghost,
3533         Pre  => X3 < Y3,
3534         Post => Big3 (X1, X2, X3 - Y3)
3535           = Big3 (X1, X2, X3) + Big3 (Single_Uns'(0), 1, 0) - Big3 (0, 0, Y3);
3536
3537       -------------------------
3538       -- Lemma_Add3_No_Carry --
3539       -------------------------
3540
3541       procedure Lemma_Add3_No_Carry (X1, X2, X3, Y1, Y2, Y3 : Single_Uns) is
3542       begin
3543          Lemma_Add_Commutation (Double_Uns (X1), Y1);
3544          Lemma_Add_Commutation (Double_Uns (X2), Y2);
3545          Lemma_Add_Commutation (Double_Uns (X3), Y3);
3546          pragma Assert (Double_Uns (Single_Uns'(X1 + Y1))
3547                         = Double_Uns (X1) + Double_Uns (Y1));
3548          pragma Assert (Double_Uns (Single_Uns'(X2 + Y2))
3549                         = Double_Uns (X2) + Double_Uns (Y2));
3550          pragma Assert (Double_Uns (Single_Uns'(X3 + Y3))
3551                         = Double_Uns (X3) + Double_Uns (Y3));
3552       end Lemma_Add3_No_Carry;
3553
3554       ---------------------
3555       -- Lemma_Ge_Expand --
3556       ---------------------
3557
3558       procedure Lemma_Ge_Expand (X1, X2, X3, Y1, Y2, Y3 : Single_Uns) is null;
3559
3560       -------------------------
3561       -- Lemma_Sub3_No_Carry --
3562       -------------------------
3563
3564       procedure Lemma_Sub3_No_Carry (X1, X2, X3, Y1, Y2, Y3 : Single_Uns) is
3565       begin
3566          Lemma_Subtract_Commutation (Double_Uns (X1), Double_Uns (Y1));
3567          Lemma_Subtract_Commutation (Double_Uns (X2), Double_Uns (Y2));
3568          Lemma_Subtract_Commutation (Double_Uns (X3), Double_Uns (Y3));
3569       end Lemma_Sub3_No_Carry;
3570
3571       ----------------------------
3572       -- Lemma_Sub3_With_Carry2 --
3573       ----------------------------
3574
3575       procedure Lemma_Sub3_With_Carry2 (X1, X2, X3, Y2 : Single_Uns) is
3576          pragma Unreferenced (X1, X3);
3577       begin
3578          Lemma_Add_Commutation
3579            (Double_Uns'(2 ** Single_Size) - Double_Uns (Y2), X2);
3580          Lemma_Subtract_Commutation
3581            (Double_Uns'(2 ** Single_Size), Double_Uns (Y2));
3582       end Lemma_Sub3_With_Carry2;
3583
3584       ----------------------------
3585       -- Lemma_Sub3_With_Carry3 --
3586       ----------------------------
3587
3588       procedure Lemma_Sub3_With_Carry3 (X1, X2, X3, Y3 : Single_Uns) is
3589          pragma Unreferenced (X1, X2);
3590       begin
3591          Lemma_Add_Commutation
3592            (Double_Uns'(2 ** Single_Size) - Double_Uns (Y3), X3);
3593          Lemma_Subtract_Commutation
3594            (Double_Uns'(2 ** Single_Size), Double_Uns (Y3));
3595       end Lemma_Sub3_With_Carry3;
3596
3597    --  Start of processing for Sub3
3598
3599    begin
3600       Lemma_Ge_Expand (X1, X2, X3, Y1, Y2, Y3);
3601
3602       if Y3 > X3 then
3603          if X2 = 0 then
3604             pragma Assert (X1 >= 1);
3605             Lemma_Sub3_No_Carry (X1, X2, X3, 1, 0, 0);
3606
3607             X1 := X1 - 1;
3608
3609             pragma Assert
3610               (Big3 (X1, X2, X3) =
3611                  Big3 (XX1, XX2, XX3) - Big3 (Single_Uns'(1), 0, 0));
3612             pragma Assert
3613               (Big3 (X1, X2, X3) = Big3 (XX1, XX2, XX3)
3614                - Big3 (Single_Uns'(0), Single_Uns'Last, 0)
3615                - Big3 (Single_Uns'(0), 1, 0));
3616             Lemma_Add3_No_Carry (X1, X2, X3, 0, Single_Uns'Last, 0);
3617          else
3618             Lemma_Sub3_No_Carry (X1, X2, X3, 0, 1, 0);
3619          end if;
3620
3621          X2 := X2 - 1;
3622
3623          pragma Assert
3624            (Big3 (X1, X2, X3) =
3625               Big3 (XX1, XX2, XX3) - Big3 (Single_Uns'(0), 1, 0));
3626          Lemma_Sub3_With_Carry3 (X1, X2, X3, Y3);
3627       else
3628          Lemma_Sub3_No_Carry (X1, X2, X3, 0, 0, Y3);
3629       end if;
3630
3631       X3 := X3 - Y3;
3632
3633       pragma Assert
3634         (Big3 (X1, X2, X3) = Big3 (XX1, XX2, XX3) - Big3 (0, 0, Y3));
3635
3636       if Y2 > X2 then
3637          pragma Assert (X1 >= 1);
3638          Lemma_Sub3_No_Carry (X1, X2, X3, 1, 0, 0);
3639
3640          X1 := X1 - 1;
3641
3642          pragma Assert
3643            (Big3 (X1, X2, X3) = Big3 (XX1, XX2, XX3)
3644             - Big3 (0, 0, Y3) - Big3 (Single_Uns'(1), 0, 0));
3645          Lemma_Sub3_With_Carry2 (X1, X2, X3, Y2);
3646       else
3647          Lemma_Sub3_No_Carry (X1, X2, X3, 0, Y2, 0);
3648       end if;
3649
3650       X2 := X2 - Y2;
3651
3652       pragma Assert
3653         (Big3 (X1, X2, X3) = Big3 (XX1, XX2, XX3) - Big3 (0, Y2, Y3));
3654       pragma Assert (X1 >= Y1);
3655       Lemma_Sub3_No_Carry (X1, Y2, X3, Y1, 0, 0);
3656
3657       X1 := X1 - Y1;
3658
3659       pragma Assert
3660         (Big3 (X1, X2, X3) = Big3 (XX1, XX2, XX3)
3661          - Big3 (0, Y2, Y3) - Big3 (Y1, 0, 0));
3662       Lemma_Add3_No_Carry (0, Y2, Y3, Y1, 0, 0);
3663       pragma Assert
3664         (Big3 (X1, X2, X3) = Big3 (XX1, XX2, XX3) - Big3 (Y1, Y2, Y3));
3665    end Sub3;
3666
3667    -------------------------------
3668    -- Subtract_With_Ovflo_Check --
3669    -------------------------------
3670
3671    function Subtract_With_Ovflo_Check (X, Y : Double_Int) return Double_Int is
3672       R : constant Double_Int := To_Int (To_Uns (X) - To_Uns (Y));
3673
3674       --  Local lemmas
3675
3676       procedure Prove_Negative_X
3677       with
3678         Ghost,
3679         Pre  => X < 0 and then (Y <= 0 or else R < 0),
3680         Post => R = X - Y;
3681
3682       procedure Prove_Non_Negative_X
3683       with
3684         Ghost,
3685         Pre  => X >= 0 and then (Y > 0 or else R >= 0),
3686         Post => R = X - Y;
3687
3688       procedure Prove_Overflow_Case
3689       with
3690         Ghost,
3691         Pre  =>
3692           (if X >= 0 then Y <= 0 and then R < 0
3693                      else Y > 0 and then R >= 0),
3694         Post => not In_Double_Int_Range (Big (X) - Big (Y));
3695
3696       ----------------------
3697       -- Prove_Negative_X --
3698       ----------------------
3699
3700       procedure Prove_Negative_X is
3701       begin
3702          if X = Double_Int'First then
3703             if Y = Double_Int'First or else Y > 0 then
3704                null;
3705             else
3706                pragma Assert
3707                  (To_Uns (X) - To_Uns (Y) =
3708                     2 ** (Double_Size - 1) + Double_Uns (-Y));
3709             end if;
3710
3711          elsif Y >= 0 or else Y = Double_Int'First then
3712             null;
3713
3714          else
3715             pragma Assert
3716               (To_Uns (X) - To_Uns (Y) = -Double_Uns (-X) + Double_Uns (-Y));
3717          end if;
3718       end Prove_Negative_X;
3719
3720       --------------------------
3721       -- Prove_Non_Negative_X --
3722       --------------------------
3723
3724       procedure Prove_Non_Negative_X is
3725       begin
3726          if Y > 0 then
3727             declare
3728                Ru : constant Double_Uns := To_Uns (X) - To_Uns (Y);
3729             begin
3730                pragma Assert (Ru = Double_Uns (X) - Double_Uns (Y));
3731                if Ru < 2 ** (Double_Size - 1) then  --  R >= 0
3732                   pragma Assert (To_Uns (Y) <= To_Uns (X));
3733                   Lemma_Subtract_Double_Uns (X => Y, Y => X);
3734                   pragma Assert (Ru = Double_Uns (X - Y));
3735
3736                elsif Ru = 2 ** (Double_Size - 1) then
3737                   pragma Assert (Double_Uns (Y) < 2 ** (Double_Size - 1));
3738                   pragma Assert (False);
3739
3740                else
3741                   pragma Assert
3742                     (R = -Double_Int (-(Double_Uns (X) - Double_Uns (Y))));
3743                   pragma Assert
3744                     (R = -Double_Int (-Double_Uns (X) + Double_Uns (Y)));
3745                   pragma Assert
3746                     (R = -Double_Int (Double_Uns (Y) - Double_Uns (X)));
3747                end if;
3748             end;
3749
3750          elsif Y = Double_Int'First then
3751             pragma Assert
3752               (To_Uns (X) - To_Uns (Y) =
3753                  Double_Uns (X) - 2 ** (Double_Size - 1));
3754             pragma Assert (False);
3755
3756          else
3757             pragma Assert
3758               (To_Uns (X) - To_Uns (Y) = Double_Uns (X) + Double_Uns (-Y));
3759          end if;
3760       end Prove_Non_Negative_X;
3761
3762       -------------------------
3763       -- Prove_Overflow_Case --
3764       -------------------------
3765
3766       procedure Prove_Overflow_Case is
3767       begin
3768          if X >= 0 and then Y /= Double_Int'First then
3769             pragma Assert
3770               (To_Uns (X) - To_Uns (Y) = Double_Uns (X) + Double_Uns (-Y));
3771
3772          elsif X < 0 and then X /= Double_Int'First then
3773             pragma Assert
3774               (To_Uns (X) - To_Uns (Y) = -Double_Uns (-X) - Double_Uns (Y));
3775          end if;
3776       end Prove_Overflow_Case;
3777
3778    --  Start of processing for Subtract_With_Ovflo_Check
3779
3780    begin
3781       if X >= 0 then
3782          if Y > 0 or else R >= 0 then
3783             Prove_Non_Negative_X;
3784             return R;
3785          end if;
3786
3787       else -- X < 0
3788          if Y <= 0 or else R < 0 then
3789             Prove_Negative_X;
3790             return R;
3791          end if;
3792       end if;
3793
3794       Prove_Overflow_Case;
3795       Raise_Error;
3796    end Subtract_With_Ovflo_Check;
3797
3798    ----------------
3799    -- To_Neg_Int --
3800    ----------------
3801
3802    function To_Neg_Int (A : Double_Uns) return Double_Int is
3803       R : constant Double_Int :=
3804         (if A = 2 ** (Double_Size - 1) then Double_Int'First else -To_Int (A));
3805       --  Note that we can't just use the expression of the Else, because it
3806       --  overflows for A = 2 ** (Double_Size - 1).
3807    begin
3808       if R <= 0 then
3809          return R;
3810       else
3811          Raise_Error;
3812       end if;
3813    end To_Neg_Int;
3814
3815    ----------------
3816    -- To_Pos_Int --
3817    ----------------
3818
3819    function To_Pos_Int (A : Double_Uns) return Double_Int is
3820       R : constant Double_Int := To_Int (A);
3821    begin
3822       if R >= 0 then
3823          return R;
3824       else
3825          Raise_Error;
3826       end if;
3827    end To_Pos_Int;
3828
3829 end System.Arith_Double;