module Zadd

use int.Int
use int.Power
use map.Map
use mach.int.Int32GMP
use ref.Ref
use mach.c.C
use lemmas.Lemmas
use util.Util
use ptralias.Alias
use compare.Compare
use import mach.int.UInt64GMP as Limb
use add.Add
use sub.Sub
use int.Abs
use mpz.Z
use mpz.Zutil

let wmpz_add (w u v: mpz_ptr) : unit
  requires { mpz.alloc[w] >= 1 /\ mpz.alloc[u] >= 1 /\ mpz.alloc[v] >= 1 }
  requires { mpz.readers[w] = 0 /\ mpz.readers[u] = 0 /\ mpz.readers[v] = 0 }
  requires { mpz.abs_size[u] < max_int32 /\ mpz.abs_size[v] < max_int32 }
  ensures  { value_of w mpz = old (value_of u mpz + value_of v mpz) }
  ensures  { forall x. x <> w -> mpz_unchanged x mpz (old mpz) }
  ensures  { mpz.readers[w] = 0 /\ mpz.readers[u] = 0 /\ mpz.readers[v] = 0 }
= [@vc:do_not_keep_trace] (* traceability info breaks the proofs *)
  label Start in
  let ref u = u in
  let ref v = v in
  let ref usize = size_of u in
  let ref vsize = size_of v in
  let ref abs_usize = abs usize in
  let ref abs_vsize = abs vsize in
  begin
    ensures { mpz.abs_size[u] = abs_usize /\ mpz.abs_size[v] = abs_vsize }
    ensures { abs_vsize <= abs_usize < max_int32 }
    ensures { 0 <= abs_vsize <= mpz.alloc[v] }
    ensures { 0 <= abs_usize <= mpz.alloc[u] }
    ensures { mpz.alloc[u] > 0 /\ mpz.alloc[v] > 0 }
    ensures { mpz.readers[u] = 0 /\ mpz.readers[v] = 0 }
    ensures { abs_usize * mpz.sgn[u] = usize /\
              abs_vsize * mpz.sgn[v] = vsize }
    ensures { value_of u mpz + value_of v mpz
              = old (value_of u mpz + value_of v mpz) }
    ensures { mpz_unchanged u mpz (old mpz) }
    ensures { mpz_unchanged v mpz (old mpz) }
    if Int32.(<) abs_usize abs_vsize
    then begin
      mpz_ptr_swap u v;
      let ref tmp_size = vsize in
      vsize <- usize;
      usize <- tmp_size;
      tmp_size <- abs_vsize;
      abs_vsize <- abs_usize;
      abs_usize <- tmp_size;
    end
  end;
  let ref wsize = Int32.(+) abs_usize 1 in
  let uw = mpz_eq u w in
  let vw = mpz_eq v w in
  label Realloc in
  let ompz = pure { mpz } in
  let wp = wmpz_realloc w wsize in
  assert { uw \/ mpz_unchanged u mpz ompz };
  assert { vw \/ mpz_unchanged v mpz ompz };
  assert { forall x. x <> w -> mpz_unchanged x mpz (mpz at Start) };
  label Op in
  if (bxor usize vsize < 0)
  then begin
      ensures { sgn_value wp wsize
                = (value_of u mpz + value_of v mpz) at Op }
      ensures { uw \/ mpz.readers[u] = 0 }
      ensures { vw \/ mpz.readers[v] = 0 }
      ensures { mpz.readers[w] = -1 }
      ensures { forall x. x <> w -> mpz_unchanged x mpz (mpz at Start) }
      ensures { abs wsize <= plength wp }
      ensures { wsize <> 0 ->
                value wp (abs wsize) >= power radix (abs wsize - 1) }
      ensures { mpz.alloc[u] > 0 /\ mpz.alloc[v] > 0 }
      ensures { min wp = old min wp /\ max wp = old max wp
                /\ plength wp = old plength wp }
    assert { (usize >= 0 /\ vsize < 0)
             \/ (usize < 0 /\ vsize >= 0) };
    if abs_usize <> abs_vsize
    then begin
      begin ensures { value wp abs_usize
                      = old (mpz.abs_value_of[u] - mpz.abs_value_of[v]) }
            ensures { uw \/ mpz.readers[u] = 0 }
            ensures { vw \/ mpz.readers[v] = 0 }
            ensures { mpz.alloc[u] > 0 /\ mpz.alloc[v] > 0 }
            ensures { mpz.readers[w] = -1 }
            ensures { forall x. x <> w -> mpz_unchanged x mpz (mpz at Start) }
            ensures { min wp = old min wp /\ max wp = old max wp
                      /\ plength wp = old plength wp }
      if uw
      then begin
        assert { not vw };
        let vp = get_read_ptr v in
        let _b = sub_rx wp abs_usize vp abs_vsize in
        assert { _b = 0 };
        release_reader v vp
      end else if vw
      then begin
        let up = get_read_ptr u in
        let _b = sub_ry up abs_usize wp abs_vsize in
        assert { _b = 0 };
        release_reader u up
      end else begin
        let up = get_read_ptr u in
        let vp = get_read_ptr v in
        let _b = sub wp up abs_usize vp abs_vsize in
        assert { _b = 0 };
        release_reader u up;
        release_reader v vp
      end
      end;
      wsize <- abs_usize;
      normalize wp wsize;
      if usize < 0 then wsize <- -wsize;
      assert { sgn_value wp wsize = old (value_of u mpz + value_of v mpz)
               by if usize < 0
               then sgn_value wp wsize = - value wp (-wsize)
                    = - old (mpz.abs_value_of[u] - mpz.abs_value_of[v])
                    = old (value_of u mpz + value_of v mpz)
                    by vsize >= 0
               else sgn_value wp wsize = value wp wsize
                    = old (mpz.abs_value_of[u] - mpz.abs_value_of[v])
                    = old (value_of u mpz + value_of v mpz)
                    by vsize < 0 }
    end
    else begin
      wsize <- abs_usize;
      if uw
      then begin
        assert { not vw };
        let vp = get_read_ptr v in
        if wmpn_cmp wp vp abs_usize < 0
        then begin
          let _b = sub_n_ry vp wp abs_usize in
          assert { _b = 0 };
          normalize wp wsize;
          if usize >= 0
          then wsize <- -wsize
        end else begin
          let _b = sub_n_rx wp vp abs_usize in
          assert { _b = 0 };
          normalize wp wsize;
          if usize < 0 then wsize <- -wsize
        end;
        release_reader v vp
      end else if vw
      then begin
        let up = get_read_ptr u in
        if wmpn_cmp up wp abs_usize < 0
        then begin
          let _b = sub_n_rx wp up abs_usize in
          assert { _b = 0 };
          normalize wp wsize;
          if usize >= 0 then wsize <- - wsize
        end else begin
          let _b = sub_n_ry up wp abs_usize in
          assert { _b = 0 };
          normalize wp wsize;
          if usize < 0 then wsize <- - wsize
        end;
        release_reader u up
      end else begin
        let up = get_read_ptr u in
        let vp = get_read_ptr v in
        if wmpn_cmp up vp abs_usize < 0
        then begin
          let _b = sub_n wp vp up abs_usize in
          assert { _b = 0 };
          normalize wp wsize;
          if usize >= 0 then wsize <- -wsize
        end else begin
          let _b = sub_n wp up vp abs_usize in
          assert { _b = 0 };
          normalize wp wsize;
          if usize < 0 then wsize <- -wsize
        end;
        release_reader u up;
        release_reader v vp
      end
    end
  end
  else begin
    assert { (usize >= 0 /\ vsize >= 0)
             \/ (usize < 0 /\ vsize < 0) };
    let ref cy = 0 in
    begin ensures { value wp wsize = old abs (value_of u mpz + value_of v mpz) }
          ensures { uw \/ mpz.readers[u] = 0 }
          ensures { vw \/ mpz.readers[v] = 0 }
          ensures { mpz.readers[w] = -1 }
          ensures { forall x. x <> w -> mpz_unchanged x mpz (mpz at Start) }
          ensures { wsize <> 0 ->
                    value wp (abs wsize) >= power radix (abs wsize - 1) }
          ensures { min wp = old min wp /\ max wp = old max wp
                    /\ plength wp = old plength wp }
          ensures { abs_usize <= wsize <= plength wp }
    assert { abs (value_of u mpz + value_of v mpz)
             = abs (value_of u mpz) + abs (value_of v mpz)
             by if usize >= 0
                then vsize >= 0
                     so abs (value_of u mpz) = value_of u mpz
                     so abs (value_of v mpz) = value_of v mpz
                else vsize <= 0
                     so abs (value_of u mpz) = - value_of u mpz
                     so abs (value_of v mpz) = - value_of v mpz };
    if uw
    then if vw
      then begin
        cy <- add_n_rxy wp abs_vsize;
        assert { value wp abs_usize + power radix abs_usize * cy
                 = abs (value_of u mpz + value_of v mpz) };
      end
      else begin
        let vp = get_read_ptr v in
        cy <- add_rx wp abs_usize vp abs_vsize;
        assert { value wp abs_usize + power radix abs_usize * cy
                 = abs (value_of u mpz + value_of v mpz)
                 by value vp abs_vsize = abs (value_of v mpz)
                 so value wp abs_usize at Op = abs (value_of u mpz)};
        release_reader v vp
      end
    else if vw
      then begin
        let up = get_read_ptr u in
        assert { value wp abs_vsize = abs (value_of v mpz) };
        assert { value up abs_usize = abs (value_of u mpz) };
        cy <- add_ry up abs_usize wp abs_vsize;
        assert { value wp abs_usize + power radix abs_usize * cy
                 = abs (value_of u mpz + value_of v mpz)
                 by value up abs_usize = abs (value_of u mpz) };
        release_reader u up
      end
      else begin
        let up = get_read_ptr u in
        let vp = get_read_ptr v in
        assert { value up abs_usize = abs (value_of u mpz)
                 /\ value vp abs_vsize = abs (value_of v mpz) };
        cy <- add wp up abs_usize vp abs_vsize;
        assert { value wp abs_usize + power radix abs_usize * cy
                 = abs (value_of u mpz + value_of v mpz)
                 by value up abs_usize = abs (value_of u mpz)
                 so value vp abs_vsize = abs (value_of v mpz) };
        release_reader u up;
        release_reader v vp;
      end;
    label Set in
    value_sub_update_no_change (pelts wp) (int32'int abs_usize)
                                    0 (int32'int abs_usize) cy;
    set_ofs wp abs_usize cy;
    value_tail wp abs_usize;
    assert { value wp (abs_usize + 1)
             = value wp abs_usize at Set + power radix abs_usize * cy
             = abs (value_of u mpz + value_of v mpz) };
    begin ensures { if cy = 0 then wsize = abs_usize
                              else wsize = abs_usize + 1 }
      wsize <- abs_usize + Limb.to_int32 cy;
      value_tail wp abs_usize;
    end;
    assert { wsize <> 0 -> value wp wsize >= power radix (wsize - 1)
             by
             if cy = 0
             then wsize = abs_usize
                  so abs_usize = ompz.abs_size u >= 1
                  so value wp wsize >= ompz.abs_value_of u
                  >= power radix (abs_usize - 1)
             else value wp wsize
                  = value wp abs_usize + power radix abs_usize * cy
                  >= power radix abs_usize * cy = power radix abs_usize };
    end;
    label Minus in
    if Int32.(<) usize 0
    then begin
      wsize <- Int32.(-_) wsize;
      assert { sgn_value wp wsize = - value wp (wsize at Minus)
               = - abs (value_of u mpz + value_of v mpz) at Op
               = (value_of u mpz + value_of v mpz) at Op
               by usize < 0 so vsize <= 0
               so value_of u mpz at Op < 0
               so value_of v mpz at Op <= 0
               so (value_of u mpz + value_of v mpz) at Op < 0 };
    end
    else begin
      assert { sgn_value wp wsize = value wp wsize
               = (value_of u mpz + value_of v mpz) at Op
               by usize >= 0 so vsize >= 0
               so value_of u mpz at Op >= 0
               so value_of v mpz at Op >= 0
               so abs (value_of u mpz + value_of v mpz) at Op
                  = (value_of u mpz + value_of v mpz) at Op
               so wsize >= abs_usize >= 0 }
    end;
    assert { sgn_value wp wsize = (value_of u mpz + value_of v mpz) at Op }
  end;
  set_size w wsize wp;
  assert { value_of w mpz = sgn_value wp wsize
           = (value_of u mpz + value_of v mpz) at Op };
  release_writer w wp

use add_1.Add_1
use sub_1.Sub_1

let wmpz_add_ui (w u: mpz_ptr) (v: uint64) : unit
  requires { mpz.alloc[w] >= 1 /\ mpz.alloc[u] >= 1 }
  requires { mpz.readers[w] = 0 /\ mpz.readers[u] = 0 }
  requires { mpz.abs_size[u] < max_int32 }
  ensures  { value_of w mpz = old (value_of u mpz + v) }
  ensures  { forall x. x <> w -> mpz_unchanged x mpz (old mpz) }
  ensures  { mpz.readers[w] = 0 /\ mpz.readers[u] = 0 }
=
  label Start in
  let usize = size_of u in
  if usize = 0
  then begin
    let wp = get_write_ptr w in
    C.set wp v;
    assert { value wp 1 = v };
    set_size w (if v <> 0 then 1 else 0) wp;
    assert { value_of w mpz = v };
    release_writer w wp;
    return;
  end;
  let abs_usize = abs usize in
  assert { 0 <= abs_usize <= mpz.alloc[u] };
  let uw = mpz_eq u w in
  let ref wsize = abs_usize + 1 in
  let ghost ompz = pure { mpz } in
  let wp = wmpz_realloc w wsize in
  assert { uw \/ mpz_unchanged u mpz ompz };
  assert { forall x. x <> w -> mpz_unchanged x mpz (mpz at Start) };
  let ref cy = 0 in
  if usize >= 0
  then begin
    begin ensures { value wp abs_usize + power radix abs_usize * cy
                    = old (value_of u mpz + v) }
          ensures { 0 <= cy <= 1 }
          ensures { uw \/ mpz.readers[u] = 0 }
          ensures { mpz.readers[w] = -1 }
          ensures { forall x. x <> w -> mpz_unchanged x mpz (mpz at Start) }
      if uw
      then
        cy <- wmpn_add_1_in_place wp abs_usize v
      else begin
        let up = get_read_ptr u in
        cy <- wmpn_add_1 wp up abs_usize v;
        release_reader u up;
      end
    end;
    label Carry in
    C.set_ofs wp abs_usize cy;
    value_tail wp abs_usize;
    assert { value wp (abs_usize + 1)
             = value wp abs_usize + power radix abs_usize * cy
             = (value_of u mpz at Start + v)
             by value wp abs_usize = value wp abs_usize at Carry };
    wsize <- abs_usize + (Limb.to_int32 cy);
    assert { value wp wsize = value wp (abs_usize + 1) };
    assert { value wp wsize = (value_of u mpz at Start + v) };
    assert { wsize <> 0 -> value wp wsize >= power radix (wsize - 1)
             by if cy = 0
                then value wp wsize >= value_of u mpz at Start
                     >= power radix (usize - 1)
                else value wp wsize
                     = value wp abs_usize + power radix abs_usize * cy
                     >= power radix abs_usize = power radix (wsize - 1) };
    end
  else begin
    begin ensures { sgn_value wp wsize = old (value_of u mpz + v) }
          ensures { abs wsize <= abs_usize + 1 }
          ensures { wsize <> 0
                    -> value wp (abs wsize) >= power radix (abs wsize - 1) }
          ensures { forall x. x <> w -> mpz_unchanged x mpz (mpz at Start) }
          ensures { uw \/ mpz.readers[u] = 0 }
          ensures { mpz.readers[w] = -1 }
      if uw then begin
        if (abs_usize = 1 && C.get wp < v)
        then begin
          assert { value_of u mpz = - (pelts wp)[0] };
          C.set wp (v - C.get wp);
          wsize <- 1;
          assert { value wp wsize = value wp 1
                   = v - old (pelts wp)[0]
                   = old (value_of u mpz + v) };
        end else begin
          assert { v <= value wp abs_usize };
          assert { value wp abs_usize = - value_of u mpz };
          assert { value wp abs_usize >= power radix (abs_usize - 1) };
          let ghost _b = wmpn_sub_1_in_place wp abs_usize v in
          assert { _b = 0 };
          assert { value wp abs_usize = - value_of u mpz - v };
          value_tail wp (abs_usize - 1);
          assert { (pelts wp)[abs_usize - 1] = 0
                   -> value wp (abs_usize - 1) = value wp abs_usize };
          wsize <- - (abs_usize
                      - (if C.get_ofs wp (abs_usize - 1) = 0 then 1 else 0));
          assert { sgn_value wp wsize = - value wp (- wsize)
                   = old (value_of u mpz + v) };
          assert { wsize = 0
                   \/ value wp (abs wsize) >= power radix (abs wsize - 1)
                   by if (pelts wp)[abs_usize - 1] = 0
                      then
                        if abs_usize >= 2
                        then
                          - wsize - 1 = abs_usize - 2
                          so v <= (radix - 1) * 1
                             <= (radix - 1) * (power radix (abs_usize - 2))
                          so power radix (-wsize - 1) + v
                             = power radix (abs_usize - 2) + v
                             <= power radix (abs_usize - 2)
                               + (radix - 1) * power radix (abs_usize - 2)
                             = radix * power radix (abs_usize - 2)
                             = power radix (abs_usize - 1)
                        else abs_usize = 1
                             so value wp abs_usize = 0
                             so wsize = 0
                      else
                        power radix (-wsize - 1) * 1
                        <=  power radix (-wsize - 1) * (pelts wp)[abs_usize - 1]
                        <= value wp (-wsize)
                   so value wp (abs wsize) = value wp (- wsize)
                     = old (abs_value_of mpz u - v)
                     >= power radix (- wsize - 1)
                     = power radix (abs wsize - 1) }
        end;
      end else begin
        let up = get_read_ptr u in
        if (abs_usize = 1 && C.get up < v)
        then begin
          assert { value_of u mpz = - value up 1 = - (pelts up)[0] };
          C.set wp (v - C.get up);
          wsize <- 1;
          assert { value wp wsize = v - (pelts up)[0]
                   (*= old (value_of u mpz + v)*) };
        end else begin
          assert { v <= abs_value_of mpz u };
          let ghost _b = wmpn_sub_1 wp up abs_usize v in
          assert { _b = 0 };
          assert { value wp abs_usize = - value_of u mpz - v };
          value_tail wp (abs_usize - 1);
          assert { (pelts wp)[abs_usize - 1] = 0
                   -> value wp (abs_usize - 1) = value wp abs_usize };
          wsize <- - (abs_usize
                      - (if C.get_ofs wp (abs_usize - 1) = 0 then 1 else 0));
          assert { sgn_value wp wsize = - value wp (- wsize)
                   = old (value_of u mpz + v) };
          assert { wsize = 0
                   \/ value wp (abs wsize) >= power radix (abs wsize - 1)
                   by if (pelts wp)[abs_usize - 1] = 0
                      then
                        if abs_usize >= 2
                        then
                          - wsize - 1 = abs_usize - 2
                          so v <= (radix - 1) * 1
                             <= (radix - 1) * (power radix (abs_usize - 2))
                          so power radix (-wsize - 1) + v
                             = power radix (abs_usize - 2) + v
                             <= power radix (abs_usize - 2)
                               + (radix - 1) * power radix (abs_usize - 2)
                             = radix * power radix (abs_usize - 2)
                             = power radix (abs_usize - 1)
                        else abs_usize = 1
                             so value wp abs_usize = 0
                             so wsize = 0
                      else
                        power radix (-wsize - 1) * 1
                        <=  power radix (-wsize - 1) * (pelts wp)[abs_usize - 1]
                        <= value wp (-wsize)
                   so value wp (abs wsize) = value wp (- wsize)
                     = old (abs_value_of mpz u - v)
                     >= power radix (- wsize - 1)
                     = power radix (abs wsize - 1) }
        end;
        release_reader u up;
      end
    end;
  end;
  set_size w wsize wp;
  release_writer w wp;
  return

end