module Zcmp

use int.Int
use int.Power
use map.Map
use mach.int.Int64
use mach.int.Int32GMP
use ref.Ref
use mach.c.C
use lemmas.Lemmas
use compare.Compare
use ptralias.Alias
use compare.Compare
use import mach.int.UInt64GMP as Limb
use int.Abs
use mpz.Z
use mpz.Zutil

let wmpz_cmp (u v:mpz_ptr) : int32
  requires { mpz.readers[u] >= 0 /\ mpz.readers[v] >= 0 }
  requires { Int32.in_bounds (mpz.sgn[u] * mpz.abs_size[u]
                             - mpz.sgn[v] * mpz.abs_size[v]) }
  ensures  { forall w. mpz_unchanged w mpz (old mpz) }
  ensures { result > 0 -> value_of u mpz > value_of v mpz }
  ensures { result < 0 -> value_of u mpz < value_of v mpz }
  ensures { result = 0 -> value_of u mpz = value_of v mpz }
=
  let usize = size_of u in
  let vsize = size_of v in
  let dsize = usize - vsize in
  if dsize <> 0 then return dsize;
  let asize = abs usize in
  let up = get_read_ptr u in
  let vp = get_read_ptr v in
  let cmp = wmpn_cmp up vp asize in
  release_reader u up;
  release_reader v vp;
  return (if usize >= 0 then cmp else -cmp)

use types.Types
use types.Int32Eq
use types.UInt64Eq

let wmpz_cmp_ui (u: mpz_ptr) (v_digit:limb) : int32
  requires { mpz.readers[u] >= 0 }
  ensures  { forall w. mpz_unchanged w mpz (old mpz) }
  ensures { result > 0 -> value_of u mpz > v_digit }
  ensures { result < 0 -> value_of u mpz < v_digit }
  ensures { result = 0 -> value_of u mpz = v_digit }
=
  let un = size_of u in
  if un = 0
  then return (if v_digit <> 0 then -1 else 0);
  if un = 1
  then begin
    let up = get_read_ptr u in
    let ul = C.get up in
    release_reader u up;
    if ul > v_digit then return 1;
    if ul < v_digit then return -1;
    return 0
  end;
  return (if un > 0 then 1 else -1)

use mpz_getset.Set

let wmpz_cmp_si (u: mpz_ptr) (v_digit:int64) : int32
  requires { mpz.readers[u] >= 0 }
  requires { mpz.abs_size u < max_int32 }
  ensures  { forall w. mpz_unchanged w mpz (old mpz) }
  ensures { result > 0 -> value_of u mpz > v_digit }
  ensures { result < 0 -> value_of u mpz < v_digit }
  ensures { result = 0 -> value_of u mpz = v_digit }
=
  let usize = size_of u in
  let vsize = (if v_digit > 0 then 1 else 0) - (if v_digit < 0 then 1 else 0) in
  assert { v_digit > 0 -> vsize = 1 };
  assert { v_digit < 0 -> vsize = -1 };
  if (usize = 0) || (usize <> vsize)
  then return usize - vsize
  else begin
    let up = get_read_ptr u in
    let ul = C.get up in
    let vl = abs_cast v_digit in
    release_reader u up;
    if ul = vl then return 0;
    if ul > vl then return usize else return (- usize)
  end

let wmpz_sgn (u:mpz_ptr) : int32
  requires { mpz.readers[u] >= 0 }
  ensures  { forall w. mpz_unchanged w mpz (old mpz) }
  ensures { result > 0 -> value_of u mpz > 0 }
  ensures { result < 0 -> value_of u mpz < 0 }
  ensures { result = 0 -> value_of u mpz = 0 }
=
  if size_of u < 0 then -1 else if size_of u > 0 then 1 else 0

end