examples_in_progress/bigInt.mlw

   1
   2
   3 (** {1 A library for arbitrary-precision integer arithmetic} *)
   4
   5 module N
   6
   7   use map.Map
   8   use mach.int.Int31
   9   use mach.array.Array31
  10   use ref.Ref
  11
  12   use int.Int
  13   use int.Power
  14
  15 (** {2 data type for unbound integers and invariants} *)
  16
  17   constant base : int = 10000
  18   (** a power of ten whose square fits on 31 bits *)
  19
  20   type t = { mutable digits: array int31 }
  21   (** an unbounded integer is stored in an array of 31 bits integers,
  22       with all values between 0 included and [base] excluded
  23
  24       index 0 is the lsb. the msb is never 0.
  25   *)
  26   predicate ok_array (a:array int31) =
  27     (to_int a.length >= 1 -> to_int a[to_int a.length - 1] <> 0) /\
  28     forall i:int. 0 <= i < to_int a.length ->
  29       0 <= to_int a[i] < base
  30
  31   predicate ok (x:t) = ok_array x.digits
  32
  33
  34 (** {2 value stored in an array} *)
  35
  36   (* [value_sub x n m] denotes the integer represented by
  37      the digits x[n..m-1] with lsb at index n *)
  38   function value_sub (x:map int int31) (n:int) (m:int) (l:int): int
  39   (* =
  40      if 0 <= n < l /\ n < m then
  41         x.[n] + base * value_sub x (n+1) m l
  42        else 0
  43   *)
  44   axiom value_sub_next:
  45     forall x,n,m,l.
  46       value_sub x n m l =
  47         if 0 <= n < l /\ n < m then
  48           to_int (Map.get x n) + base * value_sub x (n+1) m l
  49         else 0
  50
  51   use map.MapEq
  52
  53   let rec lemma value_sub_frame (x y:map int int31) (n m l:int)
  54     requires { MapEq.map_eq_sub x y n m }
  55     variant  { m - n }
  56     ensures  { value_sub x n m l = value_sub y n m l }
  57   =
  58     if n < m then value_sub_frame x y (n+1) m l else ()
  59
  60   let rec lemma value_sub_tail (x:map int int31) (n m l :int)
  61     requires { 0 <= n <= m < l }
  62     variant  { m - n }
  63     ensures  {
  64       value_sub x n (m+1) l =
  65         value_sub x n m l + to_int (Map.get x m) * power base (m-n) }
  66   = if n < m then value_sub_tail x (n+1) m l else ()
  67
  68   let rec lemma value_sub_tail_end (x:map int int31) (n m l :int)
  69     requires { 0 <= n <= m /\ m >= l }
  70     variant  { m - n }
  71     ensures  { value_sub x n (m+1) l = value_sub x n m l }
  72   = if n < m then value_sub_tail_end x (n+1) m l else ()
  73
  74
  75   let rec lemma value_sub_shorten (x:map int int31) (n m l:int)
  76     requires { 0 <= n <= m <= l }
  77     variant { m - n }
  78     ensures { value_sub x n m l = value_sub x n m m }
  79   = if n < m then value_sub_shorten x (n+1) m l else ()
  80
  81   let rec lemma value_sub_leading_zeros (x:map int int31) (n m' m l:int)
  82     requires { 0 <= n <= m' <= m <= l }
  83     requires { forall i. m' <= i < m -> to_int (Map.get x i) = 0 }
  84     variant { m - m' }
  85     ensures { value_sub x n m l = value_sub x n m' l }
  86   = if m' < m then value_sub_leading_zeros x n (m'+1) m l else ()
  87
  88   function value_array (x:array int31) : int =
  89     value_sub x.elts 0 (to_int x.length) (to_int x.length)
  90
  91   function value (x:t) : int = value_array x.digits
  92
  93
  94 (** {2 general lemmas} *)
  95
  96 (* moved to stdlib
  97   lemma power_monotonic:
  98     forall x y z. 0 <= x <= y -> power z x <= power z y
  99 *)
 100
 101   lemma power_non_neg:
 102      forall x y. x >= 0 /\ y >= 0 -> power x y >= 0
 103
 104   lemma value_zero:
 105     forall x:array int31.
 106       let l = to_int x.length in
 107       l = 0 -> value_array x = 0
 108
 109   lemma value_sub_upper_bound:
 110     forall x:map int int31, n l:int. 0 <= n <= l ->
 111     (forall i:int. 0 <= i < n -> 0 <= to_int (Map.get x i) < base) ->
 112     value_sub x 0 n l < power base n
 113
 114   lemma value_sub_lower_bound:
 115     forall x:map int int31, n l:int. 0 <= n <= l ->
 116     (forall i:int. 0 <= i < n -> 0 <= to_int (Map.get x i) < base) ->
 117     0 <= value_sub x 0 n l
 118
 119   lemma value_sub_lower_bound_tight:
 120     forall x:map int int31, n l:int. 0 < n <= l ->
 121     (forall i:int. 0 <= i < n-1 -> 0 <= to_int (Map.get x i) < base) ->
 122     0 < to_int (Map.get x (n-1)) < base ->
 123     power base (n-1) <= value_sub x 0 n l
 124
 125   lemma value_bounds_array:
 126     forall x:array int31. ok_array x ->
 127       let l = to_int x.length in
 128       l > 0 -> power base (l-1) <= value_array x < power base l
 129
 130 (** {2 conversion from a small integer} *)
 131
 132
 133   let from_small_int (n:int31) : t
 134     requires { 0 <= to_int n < base }
 135     ensures { ok result }
 136     ensures { value result = to_int n }
 137   = let zero = of_int 0 in
 138     let a =
 139       if n = zero then
 140         Array31.make zero zero
 141       else
 142         Array31.make (of_int 1) n
 143     in
 144     { digits = a }
 145
 146 (** {2 Comparisons} *)
 147
 148   exception Break
 149
 150 (* Comparisons *)
 151
 152   let compare_array (x y:array int31) : int31
 153     requires { ok_array x /\ ok_array y }
 154     ensures  { -1 <= to_int result <= 1 }
 155     ensures  { to_int result = -1 -> value_array x < value_array y }
 156     ensures  { to_int result = 0 -> value_array x = value_array y }
 157     ensures  { to_int result = 1 -> value_array x > value_array y }
 158   = let zero = of_int 0 in
 159     let one = of_int 1 in
 160     let minus_one = of_int (-1) in
 161     let l1 = x.length in
 162     let l2 = y.length in
 163     if Int31.(<) l1 l2 then minus_one else
 164       if Int31.(>) l1 l2 then one else
 165     let i = ref l1 in
 166     let res = ref zero in
 167     let ghost acc = ref 0 in
 168     try
 169       while Int31.(>) !i zero do
 170         invariant { to_int !res = 0 }
 171           (* needed to be sure it is zero at normal exit ! *)
 172         invariant { 0 <= to_int !i <= to_int l1 }
 173         invariant {
 174           value_sub x.elts 0 (to_int !i) (to_int l1) = value_array x - !acc
 175         }
 176         invariant {
 177           value_sub y.elts 0 (to_int !i) (to_int l1) = value_array y - !acc
 178         }
 179         variant { to_int !i }
 180         assert { value_array x - !acc =
 181           value_sub x.elts 0 (to_int !i - 1) (to_int l1) +
 182           power base (to_int !i - 1) * (to_int x[to_int !i - 1])
 183           };
 184         assert {  value_array y - !acc =
 185           value_sub y.elts 0 (to_int !i - 1) (to_int l1) +
 186           power base (to_int !i - 1) * (to_int y[to_int !i - 1])
 187           };
 188         i := Int31.(-) !i one;
 189         if Int31.(<) x[!i] y[!i] then
 190           begin
 191           assert { value_sub y.elts 0 (to_int !i) (to_int l1) >= 0 };
 192           assert { value_sub x.elts 0 (to_int !i) (to_int l1) <
 193             power base (to_int !i)
 194           };
 195           assert { value_array y - !acc >=
 196             power base (to_int !i) * (to_int y[to_int !i])
 197           };
 198           assert { to_int y[to_int !i] >= to_int x[to_int !i] + 1 };
 199           assert { power base (to_int !i) * (to_int y[to_int !i]) >=
 200                    power base (to_int !i) * (to_int x[to_int !i] + 1) };
 201           assert { power base (to_int !i) * (to_int y[to_int !i]) >=
 202                    power base (to_int !i) * (to_int x[to_int !i])
 203                    + power base (to_int !i) };
 204             res := minus_one;
 205             raise Break;
 206           end;
 207         if Int31.(>) x[!i] y[!i] then
 208           begin
 209           assert { value_sub x.elts 0 (to_int !i) (to_int l1) >= 0 };
 210           assert { value_sub y.elts 0 (to_int !i) (to_int l1) <
 211             power base (to_int !i)
 212           };
 213           assert { value_array x - !acc >=
 214             power base (to_int !i) * (to_int x[to_int !i])
 215           };
 216           assert { to_int x[to_int !i] >= to_int y[to_int !i] + 1 };
 217           assert { power base (to_int !i) * (to_int x[to_int !i]) >=
 218                    power base (to_int !i) * (to_int y[to_int !i] + 1) };
 219           assert { power base (to_int !i) * (to_int x[to_int !i]) >=
 220                    power base (to_int !i) * (to_int y[to_int !i])
 221                    + power base (to_int !i) };
 222             res := one;
 223             raise Break
 224           end;
 225         acc := !acc + power base (to_int !i) * to_int x[!i];
 226       done;
 227       raise Break
 228     with Break -> !res
 229     end
 230
 231   let eq (x y:t) : bool
 232     requires { ok x /\ ok y }
 233     ensures  { if result then value x = value y else value x <> value y }
 234   = compare_array x.digits y.digits = of_int 0
 235
 236 (** {2 arithmetic operations} *)
 237
 238   exception TooManyDigits
 239
 240   let add_array (x y:array int31) : array int31
 241     requires { ok_array x /\ ok_array y }
 242     requires { to_int x.length <= to_int y.length }
 243     ensures { ok_array result }
 244     ensures { value_array result = value_array x + value_array y }
 245     raises { TooManyDigits -> true }
 246   =
 247     let zero = of_int 0 in
 248     let one = of_int 1 in
 249     let minus_one = of_int (-1) in
 250     let base31 = of_int 10000 in
 251     assert { to_int base31 = base };
 252     let l = x.length in
 253     let h = y.length in
 254     if Int31.(>=) h (of_int 0x3FFFFFFF) then raise TooManyDigits;
 255     let arr = Array31.make (Int31.(+) h one) zero in
 256     let carry = ref zero in
 257     let i = ref zero in
 258     let non_null_idx = ref minus_one in
 259     while Int31.(<) !i l do
 260       invariant { 0 <= to_int !i <= to_int l }
 261       invariant { 0 <= to_int !carry <= 1 }
 262       invariant {
 263         forall j. 0 <= j < to_int !i -> 0 <= to_int arr[j] < base }
 264       invariant { -1 <= to_int !non_null_idx < to_int !i }
 265       invariant {
 266         to_int !non_null_idx >= 0 -> to_int arr[to_int !non_null_idx] <> 0 }
 267       invariant {
 268         forall j. to_int !non_null_idx < j < to_int !i -> to_int arr[j] = 0 }
 269       invariant {
 270         value_sub arr.elts 0 (to_int !i) (to_int h + 1)
 271         + (to_int !carry) * power base (to_int !i) =
 272         value_sub x.elts 0 (to_int !i) (to_int l)
 273         + value_sub y.elts 0 (to_int !i) (to_int h) }
 274       variant { to_int l - to_int !i }
 275       label L in
 276       let sum = Int31.(+) (Int31.(+) x[!i] y[!i]) !carry in
 277       if Int31.(>=) sum base31
 278         then begin arr[!i] <- Int31.(-) sum base31; carry := one end
 279         else begin arr[!i] <- sum; carry := zero end;
 280       if arr[!i] <> zero then non_null_idx := !i;
 281       assert {
 282         MapEq.map_eq_sub arr.elts (arr at L).elts 0 (to_int !i) };
 283       assert { value_sub arr.elts 0 (to_int !i) (to_int h + 1) =
 284          value_sub (arr at L).elts 0 (to_int !i) (to_int h + 1) };
 285       i := Int31.(+) !i one;
 286     done;
 287     while Int31.(<) !i h do
 288       invariant { to_int l <= to_int !i <= to_int h }
 289       invariant { 0 <= to_int !carry <= 1 }
 290       invariant {
 291         forall j. 0 <= j < to_int !i -> 0 <= to_int arr[j] < base }
 292       invariant { -1 <= to_int !non_null_idx < to_int !i }
 293       invariant {
 294         to_int !non_null_idx >= 0 -> to_int arr[to_int !non_null_idx] <> 0 }
 295       invariant {
 296         forall j. to_int !non_null_idx < j < to_int !i -> to_int arr[j] = 0 }
 297       invariant {
 298         value_sub arr.elts 0 (to_int !i) (to_int h + 1)
 299         + (to_int !carry) * power base (to_int !i) =
 300         value_sub x.elts 0 (to_int l) (to_int l)
 301         + value_sub y.elts 0 (to_int !i) (to_int h) }
 302       variant { to_int h - to_int !i }
 303       label L in
 304       let sum = Int31.(+) y[!i] !carry in
 305       if Int31.(>=) sum base31
 306         then begin arr[!i] <- Int31.(-) sum base31; carry := one end
 307         else begin arr[!i] <- sum; carry := zero end;
 308       if arr[!i] <> zero then non_null_idx := !i;
 309       assert {
 310         MapEq.map_eq_sub arr.elts (arr at L).elts 0 (to_int !i) };
 311       assert { value_sub arr.elts 0 (to_int !i) (to_int h + 1) =
 312          value_sub (arr at L).elts 0 (to_int !i) (to_int h + 1) };
 313       i := Int31.(+) !i one;
 314     done;
 315     label L in
 316     arr[!i] <- !carry;
 317     assert {
 318       MapEq.map_eq_sub arr.elts (arr at L).elts 0 (to_int !i) };
 319     assert { value_sub arr.elts 0 (to_int !i) (to_int h + 1) =
 320        value_sub (arr at L).elts 0 (to_int !i) (to_int h + 1) };
 321     assert { value_array arr = value_array x + value_array y };
 322     begin
 323      ensures { -1 <= to_int !non_null_idx <= to_int !i }
 324      ensures { to_int !non_null_idx >= 0 -> to_int arr[to_int !non_null_idx] <> 0 }
 325      ensures {
 326         forall j. to_int !non_null_idx < j <= to_int !i -> to_int arr[j] = 0 }
 327      (if arr[!i] <> zero then non_null_idx := !i)
 328     end;
 329     let len = Int31.(+) !non_null_idx one in
 330     assert { value_sub arr.elts 0 (to_int !i + 1) (to_int h + 1) =
 331       value_sub arr.elts 0 (to_int len) (to_int h + 1) } ;
 332     assert { value_sub arr.elts 0 (to_int !i + 1) (to_int h + 1) =
 333       value_sub arr.elts 0 (to_int len) (to_int len) } ;
 334     let arr' = Array31.make len zero in
 335     Array31.blit arr zero arr' zero len;
 336     assert {
 337       MapEq.map_eq_sub arr.elts arr'.elts 0 (to_int len) };
 338     assert { value_sub arr.elts 0 (to_int len) (to_int len) =
 339       value_sub arr'.elts 0 (to_int len) (to_int len) } ;
 340     assert { to_int arr'.length >= 1 ->
 341                to_int arr'[to_int arr'.length - 1] <> 0 };
 342     assert { forall j. 0 <= j < to_int arr'.length ->
 343                0 <= to_int arr'[j] < base };
 344     arr'
 345
 346   let add (x y:t) : t
 347     requires { ok x /\ ok y }
 348     ensures { ok result }
 349     ensures { value result = value x + value y }
 350     raises { TooManyDigits -> true }
 351   = let l1 = x.digits.length in
 352     let l2 = y.digits.length in
 353     let res =
 354       if Int31.(<=) l1 l2 then
 355         add_array x.digits y.digits
 356       else add_array y.digits x.digits
 357     in
 358     { digits = res }
 359
 360
 361 (* Multiplication: school book algorithm *)
 362 (*
 363   let rec mul_array (x y:array int31) : array int31
 364     requires { ok_array x /\ ok_array y }
 365     ensures { ok_array result }
 366     ensures { value_array result = value_array x * value_array y }
 367     raises { TooManyDigits -> true }
 368   = let zero = of_int 0 in
 369     let one = of_int 1 in
 370     let two = of_int 2 in
 371     let base31 = of_int 10000 in
 372     assert { to_int base31 = base };
 373     let l1 = x.digits.length in
 374     let l2 = y.digits.length in
 375     TODO
 376 *)
 377
 378 (* Multiplication: Karatsuba algorithm
 379
 380   let rec mul_array (x y:array int31) : array int31
 381     requires { ok_array x /\ ok_array y }
 382     ensures { ok_array result }
 383     ensures { value_array result = value_array x * value_array y }
 384     raises { TooManyDigits -> true }
 385   = let zero = of_int 0 in
 386     let one = of_int 1 in
 387     let two = of_int 2 in
 388     let base31 = of_int 10000 in
 389     assert { to_int base31 = base };
 390     let l1 = x.digits.length in
 391     let l2 = y.digits.length in
 392     if Int31.(<=) l1 (of_int 1) && Int31.(<=) l1 (of_int 1) then
 393        (* two small nums *)
 394        let n = x.digits.[0] * y.digits.[0] in
 395        let h = Int31.(/) n base31 in
 396        let l = Int31.(-) n (Int31.(*) h base31) in
 397        if Int31.eq h zero then
 398           if Int31.eq l zero then
 399             let arr = Array31.make zero zero in
 400             { digits = arr }
 401           else
 402             let arr = Array31.make one l in
 403             { digits = arr }
 404        else
 405           let arr = Array31.make two l in
 406           arr.(1) <- h;
 407           { digits = arr }
 408     else
 409       let m = if Int31.(<=) l1 l2 then l2 else l1 in
 410       let m2 = Int31.(/) m two in
 411       let m' = Int31.(-) m m2 in
 412       let low1 = Array31.make m2 zero in
 413       Array31.blit x zero low1 zero m2; (* wrong if l1 < m2 ! *)
 414       let low2 = Array31.make m2 zero in
 415       Array31.blit y zero low2 zero m2; (* wrong if l2 < m2 ! *)
 416       let high1 = Array31.make m' zero in
 417       Array31.blit x m2 high1 zero m'; (* wrong if l1 < m ! *)
 418       let high2 = Array31.make m' zero in
 419       Array31.blit y m2 high2 zero m'; (* wrong if l2 < m ! *)
 420       assert { value_array x = value_array low1 +
 421                  power base m2 * value_array high1 };
 422       assert { value_array y = value_array low2 +
 423                  power base m2 * value_array high2 };
 424       let z0 = mul_array low1 low2 in
 425       let z1 = mul_array (add_array low1 high1) (add_array low2 high2)
 426       let z2 = mul_array high1 high2 in
 427       (*
 428       return (z2*10^(2*m2))+((z1-z2-z0)*10^(m2))+(z0)
 429
 430       -> we need subtraction !
 431       *)
 432
 433   let mul (x y:t) : t
 434     requires { ok x /\ ok y }
 435     ensures { ok result }
 436     ensures { value result = value x * value y }
 437     raises { TooManyDigits -> true }
 438   = let res = mul_array x.digits y.digits in
 439     { digits = res }
 440 *)
 441
 442 end
 443
 444
 445
 446 module Z
 447
 448   use map.Map
 449   use mach.int.Int31
 450   use mach.array.Array31
 451   use ref.Ref
 452
 453   use int.Int
 454   use int.Power
 455   let constant base : int = 32768
 456   let constant max_digit : int = 16384
 457   let constant min_digit : int = -16384
 458
 459   type t = { mutable digits: array int31 }
 460
 461   predicate ok_array (a:array int31) =
 462     forall i:int. 0 <= i < to_int a.length ->
 463       min_digit <= to_int a[i] < max_digit
 464
 465   predicate ok (x:t) = ok_array x.digits
 466
 467   (* [value_sub x n m] denotes the integer represented by
 468      the digits x[n..m-1] with lsb at index n *)
 469   function value_sub (x:map int int31) (n:int) (m:int) (l:int): int
 470   (* =
 471      if 0 <= n < l /\ n < m then
 472         x.[n] + base * value_sub x (n+1) m l
 473        else 0
 474   *)
 475   axiom value_sub_next:
 476     forall x,n,m,l.
 477       value_sub x n m l =
 478         if 0 <= n < l /\ n < m then
 479           to_int (Map.get x n) + base * value_sub x (n+1) m l
 480         else 0
 481
 482   use map.MapEq
 483
 484   let rec lemma value_sub_frame (x y:map int int31) (n m l:int)
 485     requires { MapEq.map_eq_sub x y n m }
 486     variant  { m - n }
 487     ensures  { value_sub x n m l = value_sub y n m l }
 488   =
 489     if n < m then value_sub_frame x y (n+1) m l else ()
 490
 491   let rec lemma value_sub_tail (x:map int int31) (n m l :int)
 492     requires { 0 <= n <= m < l }
 493     variant  { m - n }
 494     ensures  {
 495       value_sub x n (m+1) l =
 496         value_sub x n m l + to_int (Map.get x m) * power base (m-n) }
 497   = if n < m then value_sub_tail x (n+1) m l else ()
 498
 499   let rec lemma value_sub_tail_end (x:map int int31) (n m l :int)
 500     requires { 0 <= n <= m /\ m >= l }
 501     variant  { m - n }
 502     ensures  { value_sub x n (m+1) l = value_sub x n m l }
 503   = if n < m then value_sub_tail_end x (n+1) m l else ()
 504
 505   function value_array (x:array int31) : int =
 506     value_sub x.elts 0 (to_int x.length) (to_int x.length)
 507
 508   function value (x:t) : int = value_array x.digits
 509
 510   let from_small_int (n:int31) : t
 511     requires { min_digit <= to_int n < max_digit }
 512     ensures { ok result }
 513     ensures { value result = to_int n }
 514   =
 515   let a = Array31.make (of_int 1) n in
 516   { digits = a }
 517
 518   exception TooManyDigits
 519
 520   let add_array (x y:array int31) : array int31
 521     requires { ok_array x /\ ok_array y }
 522     requires { to_int x.length <= to_int y.length }
 523     ensures { ok_array result }
 524     ensures { value_array result = value_array x + value_array y }
 525     raises { TooManyDigits -> true }
 526   =
 527     let zero = of_int 0 in
 528     let one = of_int 1 in
 529     let minusone = of_int (-1) in
 530     let base31 = of_int base in
 531     let min_digit31 = of_int min_digit in
 532     let max_digit31 = of_int max_digit in
 533     let l = x.length in
 534     let h = y.length in
 535     if Int31.(>=) h (of_int Int31.max_int31) then raise TooManyDigits;
 536     let arr = Array31.make (Int31.(+) h one) zero in
 537     let carry = ref zero in
 538     let i = ref zero in
 539     while Int31.(<) !i l do
 540       invariant { 0 <= to_int !i <= to_int l }
 541       invariant { -1 <= to_int !carry <= 1 }
 542       invariant {
 543         forall j. 0 <= j < to_int !i -> min_digit <= to_int arr[j] < max_digit }
 544       invariant {
 545         value_sub arr.elts 0 (to_int !i) (to_int h + 1)
 546         + (to_int !carry) * power base (to_int !i) =
 547         value_sub x.elts 0 (to_int !i) (to_int l)
 548         + value_sub y.elts 0 (to_int !i) (to_int h) }
 549       variant { to_int l - to_int !i }
 550       label L in
 551       let sum = Int31.(+) (Int31.(+) x[!i] y[!i]) !carry in
 552       if Int31.(>=) sum max_digit31
 553         then begin arr[!i] <- Int31.(-) sum base31; carry := one end
 554         else
 555       if Int31.(<) sum min_digit31
 556         then begin arr[!i] <- Int31.(+) sum base31; carry := minusone end
 557         else begin arr[!i] <- sum; carry := zero end;
 558       assert {
 559         MapEq.map_eq_sub arr.elts (arr at L).elts 0 (to_int !i) };
 560       assert { value_sub arr.elts 0 (to_int !i) (to_int h + 1) =
 561          value_sub (arr at L).elts 0 (to_int !i) (to_int h + 1) };
 562       i := Int31.(+) !i one;
 563     done;
 564     while Int31.(<) !i h do
 565       invariant { to_int l <= to_int !i <= to_int h }
 566       invariant { -1 <= to_int !carry <= 1 }
 567       invariant { forall j. 0 <= j < to_int !i ->
 568         min_digit <= to_int arr[j] < max_digit }
 569       invariant {
 570         value_sub arr.elts 0 (to_int !i) (to_int h + 1)
 571         + (to_int !carry) * power base (to_int !i) =
 572         value_sub x.elts 0 (to_int l) (to_int l)
 573         + value_sub y.elts 0 (to_int !i) (to_int h) }
 574       variant { to_int h - to_int !i }
 575       label L in
 576       let sum = Int31.(+) y[!i] !carry in
 577       if Int31.(>=) sum max_digit31
 578         then begin arr[!i] <- Int31.(-) sum base31; carry := one end
 579         else
 580       if Int31.(<) sum min_digit31
 581         then begin arr[!i] <- Int31.(+) sum base31; carry := minusone end
 582         else begin arr[!i] <- sum; carry := zero end;
 583       assert {
 584         MapEq.map_eq_sub arr.elts (arr at L).elts 0 (to_int !i) };
 585       assert { value_sub arr.elts 0 (to_int !i) (to_int h + 1) =
 586          value_sub (arr at L).elts 0 (to_int !i) (to_int h + 1) };
 587       i := Int31.(+) !i one;
 588     done;
 589     label L in
 590     arr[!i] <- !carry;
 591     assert {
 592       MapEq.map_eq_sub arr.elts (arr at L).elts 0 (to_int !i) };
 593     assert { value_sub arr.elts 0 (to_int !i) (to_int h + 1) =
 594        value_sub (arr at L).elts 0 (to_int !i) (to_int h + 1) };
 595     arr
 596
 597   let add (x y:t) : t
 598     requires { ok x /\ ok y }
 599     ensures { ok result }
 600     ensures { value result = value x + value y }
 601     raises { TooManyDigits -> true }
 602   = let l1 = x.digits.length in
 603     let l2 = y.digits.length in
 604     let res =
 605       if Int31.(<=) l1 l2 then
 606         add_array x.digits y.digits
 607       else add_array y.digits x.digits
 608     in
 609     { digits = res }
 610
 611
 612 end
 613
 614
 615