examples/multiprecision/mpz_add.mlw

   1 module Zadd
   2
   3 use int.Int
   4 use int.Power
   5 use map.Map
   6 use mach.int.Int32GMP
   7 use ref.Ref
   8 use mach.c.C
   9 use lemmas.Lemmas
  10 use util.Util
  11 use ptralias.Alias
  12 use compare.Compare
  13 use import mach.int.UInt64GMP as Limb
  14 use add.Add
  15 use sub.Sub
  16 use int.Abs
  17 use mpz.Z
  18 use mpz.Zutil
  19
  20 let wmpz_add (w u v: mpz_ptr) : unit
  21   requires { mpz.alloc[w] >= 1 /\ mpz.alloc[u] >= 1 /\ mpz.alloc[v] >= 1 }
  22   requires { mpz.readers[w] = 0 /\ mpz.readers[u] = 0 /\ mpz.readers[v] = 0 }
  23   requires { mpz.abs_size[u] < max_int32 /\ mpz.abs_size[v] < max_int32 }
  24   ensures  { value_of w mpz = old (value_of u mpz + value_of v mpz) }
  25   ensures  { forall x. x <> w -> mpz_unchanged x mpz (old mpz) }
  26   ensures  { mpz.readers[w] = 0 /\ mpz.readers[u] = 0 /\ mpz.readers[v] = 0 }
  27 = [@vc:do_not_keep_trace] (* traceability info breaks the proofs *)
  28   label Start in
  29   let ref u = u in
  30   let ref v = v in
  31   let ref usize = size_of u in
  32   let ref vsize = size_of v in
  33   let ref abs_usize = abs usize in
  34   let ref abs_vsize = abs vsize in
  35   begin
  36     ensures { mpz.abs_size[u] = abs_usize /\ mpz.abs_size[v] = abs_vsize }
  37     ensures { abs_vsize <= abs_usize < max_int32 }
  38     ensures { 0 <= abs_vsize <= mpz.alloc[v] }
  39     ensures { 0 <= abs_usize <= mpz.alloc[u] }
  40     ensures { mpz.alloc[u] > 0 /\ mpz.alloc[v] > 0 }
  41     ensures { mpz.readers[u] = 0 /\ mpz.readers[v] = 0 }
  42     ensures { abs_usize * mpz.sgn[u] = usize /\
  43               abs_vsize * mpz.sgn[v] = vsize }
  44     ensures { value_of u mpz + value_of v mpz
  45               = old (value_of u mpz + value_of v mpz) }
  46     ensures { mpz_unchanged u mpz (old mpz) }
  47     ensures { mpz_unchanged v mpz (old mpz) }
  48     if Int32.(<) abs_usize abs_vsize
  49     then begin
  50       mpz_ptr_swap u v;
  51       let ref tmp_size = vsize in
  52       vsize <- usize;
  53       usize <- tmp_size;
  54       tmp_size <- abs_vsize;
  55       abs_vsize <- abs_usize;
  56       abs_usize <- tmp_size;
  57     end
  58   end;
  59   let ref wsize = Int32.(+) abs_usize 1 in
  60   let uw = mpz_eq u w in
  61   let vw = mpz_eq v w in
  62   label Realloc in
  63   let ompz = pure { mpz } in
  64   let wp = wmpz_realloc w wsize in
  65   assert { uw \/ mpz_unchanged u mpz ompz };
  66   assert { vw \/ mpz_unchanged v mpz ompz };
  67   assert { forall x. x <> w -> mpz_unchanged x mpz (mpz at Start) };
  68   label Op in
  69   if (bxor usize vsize < 0)
  70   then begin
  71       ensures { sgn_value wp wsize
  72                 = (value_of u mpz + value_of v mpz) at Op }
  73       ensures { uw \/ mpz.readers[u] = 0 }
  74       ensures { vw \/ mpz.readers[v] = 0 }
  75       ensures { mpz.readers[w] = -1 }
  76       ensures { forall x. x <> w -> mpz_unchanged x mpz (mpz at Start) }
  77       ensures { abs wsize <= plength wp }
  78       ensures { wsize <> 0 ->
  79                 value wp (abs wsize) >= power radix (abs wsize - 1) }
  80       ensures { mpz.alloc[u] > 0 /\ mpz.alloc[v] > 0 }
  81       ensures { min wp = old min wp /\ max wp = old max wp
  82                 /\ plength wp = old plength wp }
  83     assert { (usize >= 0 /\ vsize < 0)
  84              \/ (usize < 0 /\ vsize >= 0) };
  85     if abs_usize <> abs_vsize
  86     then begin
  87       begin ensures { value wp abs_usize
  88                       = old (mpz.abs_value_of[u] - mpz.abs_value_of[v]) }
  89             ensures { uw \/ mpz.readers[u] = 0 }
  90             ensures { vw \/ mpz.readers[v] = 0 }
  91             ensures { mpz.alloc[u] > 0 /\ mpz.alloc[v] > 0 }
  92             ensures { mpz.readers[w] = -1 }
  93             ensures { forall x. x <> w -> mpz_unchanged x mpz (mpz at Start) }
  94             ensures { min wp = old min wp /\ max wp = old max wp
  95                       /\ plength wp = old plength wp }
  96       if uw
  97       then begin
  98         assert { not vw };
  99         let vp = get_read_ptr v in
 100         let _b = sub_rx wp abs_usize vp abs_vsize in
 101         assert { _b = 0 };
 102         release_reader v vp
 103       end else if vw
 104       then begin
 105         let up = get_read_ptr u in
 106         let _b = sub_ry up abs_usize wp abs_vsize in
 107         assert { _b = 0 };
 108         release_reader u up
 109       end else begin
 110         let up = get_read_ptr u in
 111         let vp = get_read_ptr v in
 112         let _b = sub wp up abs_usize vp abs_vsize in
 113         assert { _b = 0 };
 114         release_reader u up;
 115         release_reader v vp
 116       end
 117       end;
 118       wsize <- abs_usize;
 119       normalize wp wsize;
 120       if usize < 0 then wsize <- -wsize;
 121       assert { sgn_value wp wsize = old (value_of u mpz + value_of v mpz)
 122                by if usize < 0
 123                then sgn_value wp wsize = - value wp (-wsize)
 124                     = - old (mpz.abs_value_of[u] - mpz.abs_value_of[v])
 125                     = old (value_of u mpz + value_of v mpz)
 126                     by vsize >= 0
 127                else sgn_value wp wsize = value wp wsize
 128                     = old (mpz.abs_value_of[u] - mpz.abs_value_of[v])
 129                     = old (value_of u mpz + value_of v mpz)
 130                     by vsize < 0 }
 131     end
 132     else begin
 133       wsize <- abs_usize;
 134       if uw
 135       then begin
 136         assert { not vw };
 137         let vp = get_read_ptr v in
 138         if wmpn_cmp wp vp abs_usize < 0
 139         then begin
 140           let _b = sub_n_ry vp wp abs_usize in
 141           assert { _b = 0 };
 142           normalize wp wsize;
 143           if usize >= 0
 144           then wsize <- -wsize
 145         end else begin
 146           let _b = sub_n_rx wp vp abs_usize in
 147           assert { _b = 0 };
 148           normalize wp wsize;
 149           if usize < 0 then wsize <- -wsize
 150         end;
 151         release_reader v vp
 152       end else if vw
 153       then begin
 154         let up = get_read_ptr u in
 155         if wmpn_cmp up wp abs_usize < 0
 156         then begin
 157           let _b = sub_n_rx wp up abs_usize in
 158           assert { _b = 0 };
 159           normalize wp wsize;
 160           if usize >= 0 then wsize <- - wsize
 161         end else begin
 162           let _b = sub_n_ry up wp abs_usize in
 163           assert { _b = 0 };
 164           normalize wp wsize;
 165           if usize < 0 then wsize <- - wsize
 166         end;
 167         release_reader u up
 168       end else begin
 169         let up = get_read_ptr u in
 170         let vp = get_read_ptr v in
 171         if wmpn_cmp up vp abs_usize < 0
 172         then begin
 173           let _b = sub_n wp vp up abs_usize in
 174           assert { _b = 0 };
 175           normalize wp wsize;
 176           if usize >= 0 then wsize <- -wsize
 177         end else begin
 178           let _b = sub_n wp up vp abs_usize in
 179           assert { _b = 0 };
 180           normalize wp wsize;
 181           if usize < 0 then wsize <- -wsize
 182         end;
 183         release_reader u up;
 184         release_reader v vp
 185       end
 186     end
 187   end
 188   else begin
 189     assert { (usize >= 0 /\ vsize >= 0)
 190              \/ (usize < 0 /\ vsize < 0) };
 191     let ref cy = 0 in
 192     begin ensures { value wp wsize = old abs (value_of u mpz + value_of v mpz) }
 193           ensures { uw \/ mpz.readers[u] = 0 }
 194           ensures { vw \/ mpz.readers[v] = 0 }
 195           ensures { mpz.readers[w] = -1 }
 196           ensures { forall x. x <> w -> mpz_unchanged x mpz (mpz at Start) }
 197           ensures { wsize <> 0 ->
 198                     value wp (abs wsize) >= power radix (abs wsize - 1) }
 199           ensures { min wp = old min wp /\ max wp = old max wp
 200                     /\ plength wp = old plength wp }
 201           ensures { abs_usize <= wsize <= plength wp }
 202     assert { abs (value_of u mpz + value_of v mpz)
 203              = abs (value_of u mpz) + abs (value_of v mpz)
 204              by if usize >= 0
 205                 then vsize >= 0
 206                      so abs (value_of u mpz) = value_of u mpz
 207                      so abs (value_of v mpz) = value_of v mpz
 208                 else vsize <= 0
 209                      so abs (value_of u mpz) = - value_of u mpz
 210                      so abs (value_of v mpz) = - value_of v mpz };
 211     if uw
 212     then if vw
 213       then begin
 214         cy <- add_n_rxy wp abs_vsize;
 215         assert { value wp abs_usize + power radix abs_usize * cy
 216                  = abs (value_of u mpz + value_of v mpz) };
 217       end
 218       else begin
 219         let vp = get_read_ptr v in
 220         cy <- add_rx wp abs_usize vp abs_vsize;
 221         assert { value wp abs_usize + power radix abs_usize * cy
 222                  = abs (value_of u mpz + value_of v mpz)
 223                  by value vp abs_vsize = abs (value_of v mpz)
 224                  so value wp abs_usize at Op = abs (value_of u mpz)};
 225         release_reader v vp
 226       end
 227     else if vw
 228       then begin
 229         let up = get_read_ptr u in
 230         assert { value wp abs_vsize = abs (value_of v mpz) };
 231         assert { value up abs_usize = abs (value_of u mpz) };
 232         cy <- add_ry up abs_usize wp abs_vsize;
 233         assert { value wp abs_usize + power radix abs_usize * cy
 234                  = abs (value_of u mpz + value_of v mpz)
 235                  by value up abs_usize = abs (value_of u mpz) };
 236         release_reader u up
 237       end
 238       else begin
 239         let up = get_read_ptr u in
 240         let vp = get_read_ptr v in
 241         assert { value up abs_usize = abs (value_of u mpz)
 242                  /\ value vp abs_vsize = abs (value_of v mpz) };
 243         cy <- add wp up abs_usize vp abs_vsize;
 244         assert { value wp abs_usize + power radix abs_usize * cy
 245                  = abs (value_of u mpz + value_of v mpz)
 246                  by value up abs_usize = abs (value_of u mpz)
 247                  so value vp abs_vsize = abs (value_of v mpz) };
 248         release_reader u up;
 249         release_reader v vp;
 250       end;
 251     label Set in
 252     value_sub_update_no_change (pelts wp) (int32'int abs_usize)
 253                                     0 (int32'int abs_usize) cy;
 254     set_ofs wp abs_usize cy;
 255     value_tail wp abs_usize;
 256     assert { value wp (abs_usize + 1)
 257              = value wp abs_usize at Set + power radix abs_usize * cy
 258              = abs (value_of u mpz + value_of v mpz) };
 259     begin ensures { if cy = 0 then wsize = abs_usize
 260                               else wsize = abs_usize + 1 }
 261       wsize <- abs_usize + Limb.to_int32 cy;
 262       value_tail wp abs_usize;
 263     end;
 264     assert { wsize <> 0 -> value wp wsize >= power radix (wsize - 1)
 265              by
 266              if cy = 0
 267              then wsize = abs_usize
 268                   so abs_usize = ompz.abs_size u >= 1
 269                   so value wp wsize >= ompz.abs_value_of u
 270                   >= power radix (abs_usize - 1)
 271              else value wp wsize
 272                   = value wp abs_usize + power radix abs_usize * cy
 273                   >= power radix abs_usize * cy = power radix abs_usize };
 274     end;
 275     label Minus in
 276     if Int32.(<) usize 0
 277     then begin
 278       wsize <- Int32.(-_) wsize;
 279       assert { sgn_value wp wsize = - value wp (wsize at Minus)
 280                = - abs (value_of u mpz + value_of v mpz) at Op
 281                = (value_of u mpz + value_of v mpz) at Op
 282                by usize < 0 so vsize <= 0
 283                so value_of u mpz at Op < 0
 284                so value_of v mpz at Op <= 0
 285                so (value_of u mpz + value_of v mpz) at Op < 0 };
 286     end
 287     else begin
 288       assert { sgn_value wp wsize = value wp wsize
 289                = (value_of u mpz + value_of v mpz) at Op
 290                by usize >= 0 so vsize >= 0
 291                so value_of u mpz at Op >= 0
 292                so value_of v mpz at Op >= 0
 293                so abs (value_of u mpz + value_of v mpz) at Op
 294                   = (value_of u mpz + value_of v mpz) at Op
 295                so wsize >= abs_usize >= 0 }
 296     end;
 297     assert { sgn_value wp wsize = (value_of u mpz + value_of v mpz) at Op }
 298   end;
 299   set_size w wsize wp;
 300   assert { value_of w mpz = sgn_value wp wsize
 301            = (value_of u mpz + value_of v mpz) at Op };
 302   release_writer w wp
 303
 304 use add_1.Add_1
 305 use sub_1.Sub_1
 306
 307 let wmpz_add_ui (w u: mpz_ptr) (v: uint64) : unit
 308   requires { mpz.alloc[w] >= 1 /\ mpz.alloc[u] >= 1 }
 309   requires { mpz.readers[w] = 0 /\ mpz.readers[u] = 0 }
 310   requires { mpz.abs_size[u] < max_int32 }
 311   ensures  { value_of w mpz = old (value_of u mpz + v) }
 312   ensures  { forall x. x <> w -> mpz_unchanged x mpz (old mpz) }
 313   ensures  { mpz.readers[w] = 0 /\ mpz.readers[u] = 0 }
 314 =
 315   label Start in
 316   let usize = size_of u in
 317   if usize = 0
 318   then begin
 319     let wp = get_write_ptr w in
 320     C.set wp v;
 321     assert { value wp 1 = v };
 322     set_size w (if v <> 0 then 1 else 0) wp;
 323     assert { value_of w mpz = v };
 324     release_writer w wp;
 325     return;
 326   end;
 327   let abs_usize = abs usize in
 328   assert { 0 <= abs_usize <= mpz.alloc[u] };
 329   let uw = mpz_eq u w in
 330   let ref wsize = abs_usize + 1 in
 331   let ghost ompz = pure { mpz } in
 332   let wp = wmpz_realloc w wsize in
 333   assert { uw \/ mpz_unchanged u mpz ompz };
 334   assert { forall x. x <> w -> mpz_unchanged x mpz (mpz at Start) };
 335   let ref cy = 0 in
 336   if usize >= 0
 337   then begin
 338     begin ensures { value wp abs_usize + power radix abs_usize * cy
 339                     = old (value_of u mpz + v) }
 340           ensures { 0 <= cy <= 1 }
 341           ensures { uw \/ mpz.readers[u] = 0 }
 342           ensures { mpz.readers[w] = -1 }
 343           ensures { forall x. x <> w -> mpz_unchanged x mpz (mpz at Start) }
 344       if uw
 345       then
 346         cy <- wmpn_add_1_in_place wp abs_usize v
 347       else begin
 348         let up = get_read_ptr u in
 349         cy <- wmpn_add_1 wp up abs_usize v;
 350         release_reader u up;
 351       end
 352     end;
 353     label Carry in
 354     C.set_ofs wp abs_usize cy;
 355     value_tail wp abs_usize;
 356     assert { value wp (abs_usize + 1)
 357              = value wp abs_usize + power radix abs_usize * cy
 358              = (value_of u mpz at Start + v)
 359              by value wp abs_usize = value wp abs_usize at Carry };
 360     wsize <- abs_usize + (Limb.to_int32 cy);
 361     assert { value wp wsize = value wp (abs_usize + 1) };
 362     assert { value wp wsize = (value_of u mpz at Start + v) };
 363     assert { wsize <> 0 -> value wp wsize >= power radix (wsize - 1)
 364              by if cy = 0
 365                 then value wp wsize >= value_of u mpz at Start
 366                      >= power radix (usize - 1)
 367                 else value wp wsize
 368                      = value wp abs_usize + power radix abs_usize * cy
 369                      >= power radix abs_usize = power radix (wsize - 1) };
 370     end
 371   else begin
 372     begin ensures { sgn_value wp wsize = old (value_of u mpz + v) }
 373           ensures { abs wsize <= abs_usize + 1 }
 374           ensures { wsize <> 0
 375                     -> value wp (abs wsize) >= power radix (abs wsize - 1) }
 376           ensures { forall x. x <> w -> mpz_unchanged x mpz (mpz at Start) }
 377           ensures { uw \/ mpz.readers[u] = 0 }
 378           ensures { mpz.readers[w] = -1 }
 379       if uw then begin
 380         if (abs_usize = 1 && C.get wp < v)
 381         then begin
 382           assert { value_of u mpz = - (pelts wp)[0] };
 383           C.set wp (v - C.get wp);
 384           wsize <- 1;
 385           assert { value wp wsize = value wp 1
 386                    = v - old (pelts wp)[0]
 387                    = old (value_of u mpz + v) };
 388         end else begin
 389           assert { v <= value wp abs_usize };
 390           assert { value wp abs_usize = - value_of u mpz };
 391           assert { value wp abs_usize >= power radix (abs_usize - 1) };
 392           let ghost _b = wmpn_sub_1_in_place wp abs_usize v in
 393           assert { _b = 0 };
 394           assert { value wp abs_usize = - value_of u mpz - v };
 395           value_tail wp (abs_usize - 1);
 396           assert { (pelts wp)[abs_usize - 1] = 0
 397                    -> value wp (abs_usize - 1) = value wp abs_usize };
 398           wsize <- - (abs_usize
 399                       - (if C.get_ofs wp (abs_usize - 1) = 0 then 1 else 0));
 400           assert { sgn_value wp wsize = - value wp (- wsize)
 401                    = old (value_of u mpz + v) };
 402           assert { wsize = 0
 403                    \/ value wp (abs wsize) >= power radix (abs wsize - 1)
 404                    by if (pelts wp)[abs_usize - 1] = 0
 405                       then
 406                         if abs_usize >= 2
 407                         then
 408                           - wsize - 1 = abs_usize - 2
 409                           so v <= (radix - 1) * 1
 410                              <= (radix - 1) * (power radix (abs_usize - 2))
 411                           so power radix (-wsize - 1) + v
 412                              = power radix (abs_usize - 2) + v
 413                              <= power radix (abs_usize - 2)
 414                                + (radix - 1) * power radix (abs_usize - 2)
 415                              = radix * power radix (abs_usize - 2)
 416                              = power radix (abs_usize - 1)
 417                         else abs_usize = 1
 418                              so value wp abs_usize = 0
 419                              so wsize = 0
 420                       else
 421                         power radix (-wsize - 1) * 1
 422                         <=  power radix (-wsize - 1) * (pelts wp)[abs_usize - 1]
 423                         <= value wp (-wsize)
 424                    so value wp (abs wsize) = value wp (- wsize)
 425                      = old (abs_value_of mpz u - v)
 426                      >= power radix (- wsize - 1)
 427                      = power radix (abs wsize - 1) }
 428         end;
 429       end else begin
 430         let up = get_read_ptr u in
 431         if (abs_usize = 1 && C.get up < v)
 432         then begin
 433           assert { value_of u mpz = - value up 1 = - (pelts up)[0] };
 434           C.set wp (v - C.get up);
 435           wsize <- 1;
 436           assert { value wp wsize = v - (pelts up)[0]
 437                    (*= old (value_of u mpz + v)*) };
 438         end else begin
 439           assert { v <= abs_value_of mpz u };
 440           let ghost _b = wmpn_sub_1 wp up abs_usize v in
 441           assert { _b = 0 };
 442           assert { value wp abs_usize = - value_of u mpz - v };
 443           value_tail wp (abs_usize - 1);
 444           assert { (pelts wp)[abs_usize - 1] = 0
 445                    -> value wp (abs_usize - 1) = value wp abs_usize };
 446           wsize <- - (abs_usize
 447                       - (if C.get_ofs wp (abs_usize - 1) = 0 then 1 else 0));
 448           assert { sgn_value wp wsize = - value wp (- wsize)
 449                    = old (value_of u mpz + v) };
 450           assert { wsize = 0
 451                    \/ value wp (abs wsize) >= power radix (abs wsize - 1)
 452                    by if (pelts wp)[abs_usize - 1] = 0
 453                       then
 454                         if abs_usize >= 2
 455                         then
 456                           - wsize - 1 = abs_usize - 2
 457                           so v <= (radix - 1) * 1
 458                              <= (radix - 1) * (power radix (abs_usize - 2))
 459                           so power radix (-wsize - 1) + v
 460                              = power radix (abs_usize - 2) + v
 461                              <= power radix (abs_usize - 2)
 462                                + (radix - 1) * power radix (abs_usize - 2)
 463                              = radix * power radix (abs_usize - 2)
 464                              = power radix (abs_usize - 1)
 465                         else abs_usize = 1
 466                              so value wp abs_usize = 0
 467                              so wsize = 0
 468                       else
 469                         power radix (-wsize - 1) * 1
 470                         <=  power radix (-wsize - 1) * (pelts wp)[abs_usize - 1]
 471                         <= value wp (-wsize)
 472                    so value wp (abs wsize) = value wp (- wsize)
 473                      = old (abs_value_of mpz u - v)
 474                      >= power radix (- wsize - 1)
 475                      = power radix (abs wsize - 1) }
 476         end;
 477         release_reader u up;
 478       end
 479     end;
 480   end;
 481   set_size w wsize wp;
 482   release_writer w wp;
 483   return
 484
 485 end