add.mlw 18.7 KB
Newer Older
1 2
module Add

3 4
  use int.Int
  use mach.int.Int32
5
  use import mach.int.UInt64GMP as Limb
6 7 8 9 10 11 12
  use int.Power
  use ref.Ref
  use mach.c.C
  use array.Array
  use map.Map
  use types.Types
  use lemmas.Lemmas
13

14
  (** `wmpn_add_1 r x y sz` adds to `x` the value of the limb `y`,
15 16
      writes the result in `r` and returns the carry. `r` and `x`
      have size `sz`. This corresponds to the function `mpn_add_1` *)
17
  (* r and x must be separated. This is enforced by Why3 regions in typing *)
18
  let wmpn_add_1 (r x:t) (y:limb) (sz:int32) : limb
19 20 21 22 23 24 25 26 27 28
    requires { valid x sz }
    requires { valid r sz }
    requires { sz > 0 } (* ? GMP does the same for 0 and 1*)
    ensures { value r sz + (power radix sz) * result =
              value x sz + y }
    ensures { 0 <= result <= 1 }
    ensures { forall j. (j < offset r \/ offset r + sz <= j)
              -> (pelts r)[j] = old (pelts r)[j] }
    writes { r.data.elts }
  =
29
    let lx = ref (C.get x) in
30 31 32
    let res = add_mod !lx y in
    let i = ref 1 in
    let c = ref 0 in
33
    C.set r res;
34
    if (res < !lx)
35 36 37
    then begin
      c := 1;
      assert { radix + res = !lx + y };
38
      while (!i < sz) do
39 40 41 42 43 44 45 46 47 48
        invariant { 1 <= !i <= sz }
        invariant { 0 <= !c <= 1 }
        invariant { !i = sz \/ !c = 1 }
        invariant { value r !i + (power radix !i) * !c =
                    value x !i + y }
        invariant { forall j. (j < offset r \/ offset r + sz <= j)
                  -> (pelts r)[j] = old (pelts r)[j] }
        variant { sz - !i }
        assert { !c = 1 };
        lx := get_ofs x !i;
49
        let res = add_mod !lx 1 in
50 51 52 53
        set_ofs r !i res;
        assert { value r !i + (power radix !i) * !c = value x !i + y };
        value_tail r !i;
        value_tail x !i;
54 55
        i := !i + 1;
        if res <> 0
56 57 58 59 60 61 62 63 64 65 66 67
        then begin
          c := 0;
          assert { res = !lx + 1 };
          assert { value r !i = value x !i + y };
          break
        end
        else begin
          assert { radix + res = !lx + 1 };
          assert { value r !i + power radix !i = value x !i + y };
        end
     done;
    end;
68
    while !i < sz do
69
      invariant { !i = sz \/ !c = 0 }
70 71 72 73 74 75 76 77 78 79
      invariant { 0 <= !i <= sz }
      invariant { value r !i + (power radix !i) * !c =
                  value x !i + y }
      invariant { forall j. (j < offset r \/ offset r + sz <= j)
                -> (pelts r)[j] = old (pelts r)[j] }
      variant { sz - !i }
      lx := get_ofs x !i;
      set_ofs r !i !lx;
      assert { value r !i + (power radix !i) * !c =
                  value x !i + y };
80 81
      value_tail r !i;
      value_tail x !i;
82
      i := !i + 1;
83 84 85
    done;
    !c

86
  (** `wmpn_add_n r x y sz` adds `x[0..sz-1]` and `y[0..sz-1]` and writes the result in `r`.
87
      Returns the carry, either `0` or `1`. Corresponds to the function `mpn_add_n`. *)
88

89
  let wmpn_add_n (r x y:t) (sz:int32) : limb
90 91 92 93 94 95 96 97 98 99
    requires { valid x sz }
    requires { valid y sz }
    requires { valid r sz }
    ensures { 0 <= result <= 1 }
    ensures { value r sz + (power radix sz) * result =
            value x sz + value y sz }
    ensures { forall j. (j < offset r \/ offset r + sz <= j)
              -> (pelts r)[j] = old (pelts r)[j] }
    writes { r.data.elts }
    =
100 101 102 103 104
    let lx = ref 0 in
    let ly = ref 0 in
    let c = ref 0 in
    let i = ref 0 in
    while !i < sz do
105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124
      variant { sz - !i }
      invariant { 0 <= !i <= sz }
      invariant { value r !i + (power radix !i) * !c =
                value x !i + value y !i }
      invariant { 0 <= !c <= 1 }
      invariant { forall j. (j < offset r \/ offset r + sz <= j)
                -> (pelts r)[j] = old (pelts r)[j] }
      label StartLoop in
      lx := get_ofs x !i;
      ly := get_ofs y !i;
      let res, carry = add_with_carry !lx !ly !c in
      set_ofs r !i res;
      assert { value r !i + (power radix !i) * !c =
                value x !i + value y !i
               by value r !i = (value r !i at StartLoop) };
      c := carry;
      value_tail r !i;
      value_tail x !i;
      value_tail y !i;
      assert { value r (!i+1) + (power radix (!i+1)) * !c =
125
                value x (!i+1) + value y (!i+1) };
126
      i := !i + 1;
127 128 129
    done;
    !c

130
  (** `wmpn_add r x y sx sy` adds `(x, sx)` to `(y, sy)` and writes the
131 132
      result in `(r, sx)`.  `sx` must be greater than or equal to
      `sy`. Returns carry, either 0 or 1. Corresponds to `mpn_add`. *)
133
  let wmpn_add (r x y:t) (sx sy:int32) : limb
134 135 136 137 138 139 140 141 142 143 144
    requires { 0 <= sy <= sx }
    requires { valid x sx }
    requires { valid y sy }
    requires { valid r sx }
    ensures { value r sx + (power radix sx) * result =
              value x sx + value y sy }
    ensures { forall j. (j < offset r \/ offset r + sx <= j)
              -> (pelts r)[j] = old (pelts r)[j] }
    ensures { 0 <= result <= 1 }
    writes { r.data.elts }
 =
145 146 147 148 149
    let lx = ref 0 in
    let ly = ref 0 in
    let c = ref 0 in
    let i = ref 0 in
    while !i < sy do
150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167 168
      variant { sy - !i }
      invariant { 0 <= !i <= sy }
      invariant { value r !i + (power radix !i) * !c =
                value x !i + value y !i }
      invariant { 0 <= !c <= 1 }
      invariant { forall j. (j < offset r \/ offset r + sx <= j)
                -> (pelts r)[j] = old (pelts r)[j] }
      label StartLoop in
      lx := get_ofs x !i;
      ly := get_ofs y !i;
      let res, carry = add_with_carry !lx !ly !c in
      set_ofs r !i res;
      assert { value r !i + (power radix !i) * !c =
                value x !i + value y !i };
      c := carry;
      value_tail r !i;
      value_tail x !i;
      value_tail y !i;
      assert { value r (!i+1) + (power radix (!i+1)) * !c =
169
                value x (!i+1) + value y (!i+1) };
170
      i := !i + 1;
171
    done;
172
    if (!c <> 0)
173
    then begin
174
      while !i < sx do
175 176 177 178 179 180 181
        variant { sx - !i }
        invariant { sy <= !i <= sx }
        invariant { value r !i + (power radix !i) * !c =
                    value x !i + value y sy }
        invariant { 0 <= !c <= 1 }
        invariant { !i = sx \/ !c = 1 }
        invariant { forall j. (j < offset r \/ offset r + sx <= j)
182
                -> (pelts r)[j] = old (pelts r)[j] }
183 184
        assert { !c = 1 };
        lx := get_ofs x !i;
185
        let res = add_mod !lx (1:limb) in
186 187 188 189 190
        set_ofs r !i res;
        assert { value r !i + (power radix !i) =
                 value x !i + value y sy };
        value_tail r !i;
        value_tail x !i;
191 192
        i := !i + 1;
        if res <> 0
193 194 195 196 197 198 199 200 201 202 203
        then begin
          c := 0;
          assert { res = !lx + 1 };
          assert { value r !i = value x !i + value y sy };
          break
        end
        else begin
          assert { !lx + 1 = radix };
          assert { value r !i + power radix !i = value x !i + value y sy }
        end
      done
204
    end;
205
    while !i < sx do
206 207 208 209 210 211 212 213 214 215 216 217 218 219
      variant { sx - !i }
      invariant { sy <= !i <= sx }
      invariant { !i = sx \/ !c = 0 }
      invariant { value r !i + power radix !i * !c =
                value x !i + value y sy }
      invariant { forall j. (j < offset r \/ offset r + sx <= j)
                -> (pelts r)[j] = old (pelts r)[j] }
      assert { !c = 0 by !i < sx };
      lx := get_ofs x !i;
      set_ofs r !i !lx;
      value_tail r !i;
      value_tail x !i;
      assert { value r !i = value x !i + value y sy }; (* true with this, should not be needed *)
      assert { value r (!i+1) + power radix (!i+1) * !c
220
               = value x (!i+1) + value y sy };
221
      i := !i + 1;
222 223 224
    done;
    !c

225
  let wmpn_add_in_place (x y:t) (sx sy:int32) : limb
226 227 228 229 230 231 232 233 234 235 236
    requires { 0 <= sy <= sx }
    requires { valid x sx }
    requires { valid y sy }
    ensures  { value x sx + (power radix sx) * result
               = value (old x) sx + value y sy }
    ensures  { 0 <= result <= 1 }
    ensures { forall j. j < x.offset \/ x.offset + sx <= j ->
              (pelts x)[j] = (pelts (old x))[j] }
    writes   { x.data.elts }
  =
    let ghost ox = { x } in
237 238 239 240 241
    let lx = ref 0 in
    let ly = ref 0 in
    let c = ref 0 in
    let i = ref 0 in
    while !i < sy do
242 243 244 245 246 247 248 249 250 251 252 253 254 255 256 257 258 259 260 261 262 263 264 265 266 267 268
      variant   { sy - !i }
      invariant { 0 <= !i <= sy }
      invariant { value x !i + (power radix !i) * !c =
                  value ox !i + value y !i }
      invariant { 0 <= !c <= 1 }
      invariant { forall j. !i <= j < sx ->
                  (pelts x)[x.offset + j] = (pelts ox)[x.offset + j] }
      invariant { forall j. j < x.offset \/ x.offset + sx <= j ->
                  (pelts x)[j] = (pelts (old x))[j] }
      label StartLoop in
      lx := get_ofs x !i;
      assert { !lx = (pelts ox)[ox.offset + !i] };
      ly := get_ofs y !i;
      let res, carry = add_with_carry !lx !ly !c in
      set_ofs x !i res;
      assert { forall j. !i < j < sx ->
                 (pelts x)[x.offset + j]
                 = (pelts ox)[x.offset + j]
                 by (pelts x)[x.offset + j]
                 = (pelts (x at StartLoop))[x.offset + j]
                 = (pelts ox)[x.offset + j]};
      assert { value x !i + (power radix !i) * !c = value ox !i + value y !i };
      c := carry;
      value_tail x !i;
      value_tail ox !i;
      value_tail y !i;
      assert { value x (!i+1) + (power radix (!i+1)) * !c =
269
                value ox (!i+1) + value y (!i+1) };
270
      i := !i + 1;
271
    done;
272
    if (!c <> 0)
273
    then begin
274
      while !i < sx do
275 276 277 278 279 280 281 282 283 284 285 286 287
        variant   { sx - !i }
        invariant { sy <= !i <= sx }
        invariant { value x !i + (power radix !i) * !c =
                    value ox !i + value y sy }
        invariant { 0 <= !c <= 1 }
        invariant { !i = sx \/ !c = 1 }
        invariant { forall j. !i <= j < sx ->
                    (pelts x)[x.offset + j] = (pelts ox) [x.offset + j] }
        invariant { forall j. j < x.offset \/ x.offset + sx <= j ->
                    (pelts x)[j] = (pelts (old x))[j] }
        assert { !c = 1 };
        lx := get_ofs x !i;
        assert { !lx = (pelts ox)[ox.offset + !i] };
288
        let res = add_mod !lx 1 in
289 290 291 292 293 294 295 296 297
        value_sub_update_no_change (pelts x) (x.offset + p2i !i)
                                   (x.offset + p2i !i + 1)
                                   (x.offset + p2i sx) res;
        set_ofs x !i res;
        assert { value x !i + (power radix !i) * !c = value ox !i + value y sy };
        assert { forall j. !i < j < sx ->
                 (pelts x)[x.offset + j] = (pelts ox) [x.offset + j] };
        value_tail ox !i;
        value_tail x !i;
298 299
        i := !i + 1;
        if (res <> 0)
300 301 302 303 304 305 306 307 308 309 310 311 312
        then begin
          c := 0;
          assert { res = !lx + 1 };
          assert { value x !i = value ox !i + value y sy };
          break;
        end
        else begin
          assert { !lx + 1 = radix };
          assert { value x !i + power radix !i = value ox !i + value y sy }
        end
      done
    end;
    assert { forall j. x.offset + !i <= j < x.offset + sx
313 314 315 316
               -> (pelts x)[j] = (pelts ox)[j]
               by !i <= j - x.offset < sx
               so (pelts x)[x.offset + (j - x.offset)]
                  = (pelts ox)[x.offset + (j - x.offset)] };
317 318 319 320 321 322 323
    value_sub_frame (pelts x) (pelts ox) (x.offset + p2i !i)
                    (x.offset + p2i sx);
    value_sub_concat (pelts x) x.offset (x.offset + p2i !i)
                     (x.offset + p2i sx);
    value_sub_concat (pelts ox) x.offset (x.offset + p2i !i)
                       (x.offset + p2i sx);
    !c
324

325
  use int.EuclideanDivision
326

327
  (** `wmpn_incr x y sz` adds to `x` the value of the limb `y` in place.
328
      `x` has size `sz`. The addition must not overflow. This corresponds
329 330
      to `mpn_wmpn_incr` *)
  let wmpn_incr (x:t) (y:limb) (ghost sz:int32) : unit
331 332 333 334 335 336 337 338 339
    requires { valid x sz }
    requires { sz > 0 }
    requires { value x sz + y < power radix sz }
    ensures  { value x sz = value (old x) sz + y }
    ensures { forall j. j < x.offset \/ x.offset + sz <= j ->
              (pelts x)[j] = (pelts (old x))[j] }
    writes   { x.data.elts }
  =
    let ghost ox = { x } in
340 341 342
    let c = ref (0:limb) in
    let lx : ref limb = ref (C.get x) in
    let i : ref int32 = ref 1 in
343
    let res = add_mod !lx y in
344
    C.set x res;
345
    if (res < !lx)
346 347 348
    then begin
      c := 1;
      assert { radix + res = !lx + y };
349
      while (!c <> 0) do
350 351 352 353 354 355 356 357 358 359 360 361 362
        invariant { 1 <= !i <= sz }
        invariant { !i = sz -> !c = 0 }
        invariant { 0 <= !c <= 1 }
        invariant { value x !i + (power radix !i) * !c
                    = value ox !i + y }
        invariant { forall j. !i <= j < sz ->
                    (pelts x)[x.offset + j] = (pelts ox)[x.offset + j] }
        invariant { forall j. j < x.offset \/ x.offset + sz <= j ->
                    (pelts x)[j] = (pelts ox)[j] }
        variant   { sz - !i }
        assert { !c = 1 };
        lx := get_ofs x !i;
        assert { !lx = (pelts ox)[ox.offset + !i] };
363
        let res = add_mod !lx 1 in
364 365 366 367 368 369 370 371 372 373
        value_sub_update_no_change (pelts x) (x.offset + p2i !i)
                                             (x.offset + p2i !i + 1)
                                             (x.offset + p2i sz) res;
        set_ofs x !i res;
        assert { forall j. !i < j < sz ->
                   (pelts x)[x.offset + j]
                   = (pelts ox)[x.offset + j] };
        assert { value x !i + (power radix !i) * !c = value ox !i + y };
        value_tail x !i;
        value_tail ox !i;
374 375
        i := !i + 1;
        if res <> 0
376 377 378 379 380 381 382 383 384 385 386 387 388 389 390 391
        then begin
          c := 0;
          assert { res = !lx + 1 };
          assert { value x !i = value ox !i + y };
          break
        end
        else begin
          assert { radix + res = !lx + 1 };
          assert { value x !i + power radix !i = value ox !i + y };
        end;
        assert { !i = sz -> !c = 0
                 by value x sz + power radix sz * !c = value ox sz + y
                 so value ox sz + y < power radix sz
                 so 0 <= !c <= 1 };
        done
    end;
392 393 394 395 396 397 398 399 400
    value_concat x !i sz;
    value_concat ox !i sz;
    assert { forall j. x.offset + !i <= j < x.offset + sz ->
             (pelts x)[j] = (pelts ox)[j]
             by let k = j - x.offset in
                !i <= k < sz
                so (pelts x)[x.offset + k] = (pelts ox)[x.offset + k]};
    value_sub_frame (pelts x) (pelts ox) (x.offset + p2i !i) (x.offset + p2i sz)

401
  (** `wmpn_incr_1 x sz` adds 1 to `x` in place.
402
      `x` has size `sz`. The addition must not overflow.
403 404
      This corresponds to `mpn_wmpn_incr` *)
  let wmpn_incr_1 (x:t) (ghost sz:int32) : unit
405 406 407 408 409 410 411 412 413 414 415 416 417
    requires { valid x sz }
    requires { sz > 0 }
    requires { value x sz + 1 < power radix sz }
    ensures  { value x sz = value (old x) sz + 1 }
    ensures { forall j. j < x.offset \/ x.offset + sz <= j ->
              (pelts x)[j] = (pelts (old x))[j] }
    writes   { x.data.elts }
  =
    let ghost ox = { x } in
    let r : ref limb = ref 0 in
    let ghost c : ref limb = ref 1 in
    let lx : ref limb = ref 0 in
    let i : ref int32 = ref 0 in
418
    while (!r = 0) do
419 420 421 422 423 424 425 426 427 428 429 430 431 432 433 434
      invariant { 0 <= !i <= sz }
      invariant { !i = sz -> !r <> 0 }
      invariant { !r <> 0 <-> !c = 0 }
      invariant { 0 <= !c <= 1 }
      invariant { value x !i + (power radix !i) * !c
                  = value ox !i + 1 }
      invariant { forall j. !i <= j < sz ->
                  (pelts x)[x.offset + j] = (pelts ox)[x.offset + j] }
      invariant { forall j. j < x.offset \/ x.offset + sz <= j ->
                  (pelts x)[j] = (pelts ox)[j] }
      variant   { sz - !i }
      label StartLoop in
      lx := get_ofs x !i;
      assert { !lx = (pelts ox)[ox.offset + !i] };
      let res = add_mod !lx 1 in
      r := res;
435
      ghost (if res = 0 then c := 1 else c := 0);
436 437 438 439 440 441 442 443 444 445 446 447 448
      assert { res + radix * !c = !lx + 1 };
      value_sub_update_no_change (pelts x) (x.offset + p2i !i)
                                           (x.offset + p2i !i + 1)
                                           (x.offset + p2i sz) res;
      set_ofs x !i res;
      assert { forall j. !i < j < sz ->
                 (pelts x)[x.offset + j]
                 = (pelts ox)[x.offset + j] };
      assert { value x !i + (power radix !i) * (!c at StartLoop) = value ox !i + 1 };
      value_tail x !i;
      value_tail ox !i;
      assert { value x (!i+1) + power radix (!i+1) * !c =
               value ox (!i+1) + 1 };
449
      i := !i + 1;
450 451 452 453 454 455 456 457 458 459 460 461 462 463
      assert { !i = sz -> !c = 0
               by value x sz + power radix sz * !c = value ox sz + 1
                  so value ox sz + 1 < power radix sz
                  so 0 <= !c <= 1};
    done;
    value_concat x !i sz;
    value_concat ox !i sz;
    assert { forall j. x.offset + !i <= j < x.offset + sz ->
             (pelts x)[j] = (pelts ox)[j]
             by let k = j - x.offset in
                !i <= k < sz
                so (pelts x)[x.offset + k] = (pelts ox)[x.offset + k]};
    value_sub_frame (pelts x) (pelts ox) (x.offset + p2i !i) (x.offset + p2i sz)

Raphaël Rieu-Helft's avatar
Raphaël Rieu-Helft committed
464 465 466 467 468 469 470 471 472
  let wmpn_add_1_in_place (x:t) (y:limb) (sz:int32) : limb
    requires { valid x sz }
    requires { sz > 0 }
    ensures  { value x sz + (power radix sz) * result = value (old x) sz + y }
    ensures  { 0 <= result <= 1 }
    ensures  { forall j. (j < offset x \/ offset x + sz <= j)
              -> (pelts x)[j] = old (pelts x)[j] }
    writes { x.data.elts }
  = let ghost ox = { x } in
473 474 475
    let c = ref 0 in
    let lx = ref (C.get x) in
    let i = ref 1 in
476
    let res = add_mod !lx y in
477
    C.set x res;
478
    if (res < !lx)
479 480 481
    then begin
      c := 1;
      assert { radix + res = !lx + y };
482
      while !i < sz do
483 484 485 486 487 488 489 490 491 492 493
        invariant { 1 <= !i <= sz }
        invariant { 0 <= !c <= 1 }
        invariant { !c = 1 \/ !i = sz }
        invariant { value x !i + (power radix !i) * !c =
                    value ox !i + y }
        invariant { forall j. (j < offset x \/ offset x + !i <= j)
                  -> (pelts x)[j] = old (pelts x)[j] }
        variant { sz - !i }
        assert { !c = 1 };
        lx := get_ofs x !i;
        assert { !lx = (pelts ox)[offset ox + !i] };
494
        let res = add_mod !lx 1 in
495 496 497 498 499 500 501 502 503 504
        value_sub_update_no_change (pelts x) (x.offset + p2i !i)
                                             (x.offset + p2i !i + 1)
                                             (x.offset + p2i sz) res;
        set_ofs x !i res;
        assert { forall j. !i < j < sz ->
                   (pelts x)[x.offset + j]
                   = (pelts ox)[x.offset + j] };
        assert { value x !i + (power radix !i) * !c = value ox !i + y };
        value_tail x !i;
        value_tail ox !i;
505 506
        i := !i + 1;
        if (res <> 0)
507 508 509 510 511 512 513 514 515 516 517 518
        then begin
          c := 0;
          assert { res = !lx + 1 };
          assert { value x !i = value ox !i + y };
          break
        end
        else begin
          assert { radix + res = !lx + 1 };
          assert { value x !i + power radix !i = value ox !i + y };
        end;
      done;
    end;
Raphaël Rieu-Helft's avatar
Raphaël Rieu-Helft committed
519 520 521 522 523 524 525 526 527 528
    value_concat x !i sz;
    value_concat ox !i sz;
    assert { forall j. x.offset + !i <= j < x.offset + sz ->
             (pelts x)[j] = (pelts ox)[j]
             by let k = j - x.offset in
                !i <= k < sz
                so (pelts x)[x.offset + k] = (pelts ox)[x.offset + k]};
    value_sub_frame (pelts x) (pelts ox) (x.offset + p2i !i) (x.offset + p2i sz);
    !c

529
end