module Zneg

use int.Int
use int.Power
use map.Map
use mach.int.Int32GMP
use mach.c.C
use lemmas.Lemmas
use util.Util
use compare.Compare
use import mach.int.UInt64GMP as Limb
use int.Abs
use mpz.Z
use mpz.Zutil

let wmpz_neg (w u: mpz_ptr) : unit
  requires { mpz.readers[u] = 0 /\ mpz.readers[w] = 0 }
  requires { mpz.alloc[w] >= 1 /\ mpz.alloc[u] >= 1 }
  ensures { mpz.readers[u] = 0 /\ mpz.readers[w] = 0 }
  ensures { value_of w mpz = - (old value_of u mpz) }
  ensures { forall x. x <> w -> mpz_unchanged x mpz (old mpz) }
=
  let ghost ompz = pure { mpz } in
  let usize = size_of u in
  let wsize = - usize in
  if (not mpz_eq u w)
  then begin
    let size = abs usize in
    let wp = wmpz_realloc w size in
    unchanged u mpz ompz;
    let up = get_read_ptr u in
    assert { value up size = ompz.abs_value_of u };
    wmpn_copyd_sep wp up size;
    assert { sgn_value wp size = ompz.abs_value_of u };
    release_reader u up;
    set_size w wsize wp;
    release_writer w wp;
  end
  else begin
    let ghost wp = get_write_ptr w in
    set_size w wsize wp;
    release_writer w wp;
  end

end