module Z

use int.Int
use int.Abs
use mach.int.Int32
use mach.c.C
use map.Map
use types.Types
use lemmas.Lemmas
use import mach.int.UInt64GMP as Limb
use int.Power

type mpz_ptr

val predicate mpz_eq (x y: mpz_ptr)
  ensures { result <-> x = y }

type mpz_memo = abstract {
  mutable abs_value_of : map mpz_ptr int;
  mutable alloc : map mpz_ptr int;
  mutable abs_size : map mpz_ptr int;
  mutable sgn : map mpz_ptr int;
  mutable readers : map mpz_ptr int;
  mutable zones : map mpz_ptr C.zone;
} invariant { forall p. 0 <= alloc p
                        /\ (sgn p = 1 \/ sgn p = -1)
                        /\ abs_size p <= alloc p
                        /\ 0 <= abs_size p <= max_int32
                        /\ 0 <= abs_value_of p
                        /\ (abs_size p >= 1 ->
                           power radix (abs_size p - 1) <= abs_value_of p)
                        /\ abs_value_of p < power radix (abs_size p) }
  by { abs_value_of = (fun _ -> 0);
       alloc = (fun _ -> 0);
       abs_size = (fun _ -> 0);
       sgn = (fun _ -> 1);
       readers = (fun _ -> 0);
       zones = (fun _ -> null_zone) }

(* readers : = 0 means there is currently no access
             = -1 means exactly one read-write access
             = n > 0 means there are n read-only accesses
             = -2 means the pointer is invalid *)

val ghost mpz : mpz_memo

function value_of (x:mpz_ptr) (memo: mpz_memo) : int
  = memo.sgn[x] * memo.abs_value_of[x]

function sgn_value (p:ptr limb) (sz:int32) : int
  = if sz >= 0 then value p sz else - value p (- sz)

predicate mpz_unchanged (x: mpz_ptr) (memo1 memo2: mpz_memo)
  = memo1.readers[x] = memo2.readers[x]
    /\ (memo1.readers[x] > - 2 ->
       (memo1.abs_value_of[x] = memo2.abs_value_of[x]
        /\ memo1.alloc[x] = memo2.alloc[x]
        /\ memo1.abs_size[x] = memo2.abs_size[x]
        /\ memo1.sgn[x] = memo2.sgn[x]
        /\ memo1.zones[x] = memo2.zones[x]))

let ghost unchanged (x:mpz_ptr) (memo1 memo2: mpz_memo) : unit
  requires { mpz_unchanged x memo1 memo2 }
  ensures  { memo1.readers[x] = memo2.readers[x] }
  ensures  { memo1.readers[x] > - 2 ->
       (memo1.abs_value_of[x] = memo2.abs_value_of[x]
    /\ memo1.alloc[x] = memo2.alloc[x]
    /\ memo1.abs_size[x] = memo2.abs_size[x]
    /\ memo1.sgn[x] = memo2.sgn[x]
    /\ memo1.readers[x] = memo2.readers[x]
    /\ memo1.zones[x] = memo2.zones[x]) }
= ()

lemma unchanged_transitive:
  forall x m1 m2 m3. mpz_unchanged x m1 m2 -> mpz_unchanged x m2 m3
                     -> mpz_unchanged x m1 m3

(* SIZ mpz macro *)
val size_of (x: mpz_ptr) : int32
  requires { mpz.readers[x] > -2 }
  ensures { result = mpz.sgn[x] * mpz.abs_size[x] }

val alloc_of (x: mpz_ptr) : int32
  requires { mpz.readers[x] > -2 }
  ensures { result = mpz.alloc[x] }

let abs [@extraction:inline] (x:int32) : int32
  requires { x > min_int32 }
  ensures { result = abs x }
= if Int32.(>=) x 0 then x else Int32.(-_) x

(* ABSIZ mpz macro *)
let abs_size_of [@extraction:inline] (x: mpz_ptr) : int32
  requires { mpz.readers[x] > -2 }
  ensures { result = mpz.abs_size[x] }
= abs (size_of x)

type mpz_struct = { ghost addr: mpz_ptr }

end


module Zutil

use int.Int
use int.Abs
use mach.int.Int32
use mach.c.C
use map.Map
use types.Types
use lemmas.Lemmas
use import mach.int.UInt64GMP as Limb
use int.Power
use ref.Ref
use Z

(* Sets the size of an mpz_ptr, leaving other fields unchanged. *)
val set_size (x:mpz_ptr) (sz:int32) (ghost p: ptr limb) : unit
  requires { mpz.zones[x] = zone p }
  requires { mpz.readers[x] = -1 }
  requires { offset p = 0 }
  requires { min p = 0 }
  requires { max p = plength p }
  requires { abs sz <= plength p }
  requires { plength p = mpz.alloc[x] }
  requires { sz <> 0 -> value p (abs sz) >= power radix (abs sz - 1) }
  writes  { mpz.sgn }
  writes  { mpz.abs_size }
  writes  { mpz.abs_value_of }
  ensures { forall y. y <> x -> mpz_unchanged y mpz (old mpz) }
  ensures { mpz.sgn[x] = 1 <-> 0 <= sz }
  ensures { mpz.sgn[x] = - 1 <-> sz < 0 }
  ensures { mpz.abs_size[x] = abs sz }
  ensures { mpz.abs_value_of[x] = value p (abs sz) }
  (* ensures size_of x = sz *)

(* Sets the size of an mpz_ptr to 0 *)
val set_size_0 (x:mpz_ptr) : unit
  requires { mpz.readers[x] >= - 1 }
  writes   { mpz.abs_size }
  writes   { mpz.abs_value_of }
  ensures  { forall y. y <> x -> mpz_unchanged y mpz (old mpz) }
  ensures  { mpz.abs_size[x] = 0 }
  ensures  { mpz.abs_value_of[x] = 0 }

(* Sets the size of an mpz_ptr to minus its former size. *)
val wmpz_minus (x:mpz_ptr) : unit
  requires { mpz.readers[x] = -1 }
  writes   { mpz.abs_size }
  writes   { mpz.abs_value_of }
  writes   { mpz.sgn }
  ensures  { forall y. y <> x -> mpz_unchanged y mpz (old mpz) }
  ensures  { mpz.sgn[x] = - old mpz.sgn[x] }
  ensures  { mpz.abs_size[x] = old mpz.abs_size[x] }
  ensures  { mpz.abs_value_of[x] = old mpz.abs_value_of[x] }

val set_alloc (x:mpz_ptr) (al:int32) : unit
  requires { mpz.abs_size[x] <= al }
  requires { mpz.readers[x] >= -1 }
  writes   { mpz.alloc }
  ensures  { forall y. y <> x -> mpz_unchanged y mpz (old mpz) }
  ensures  { mpz.alloc[x] = al }

val set_ptr (x:mpz_ptr) (p:ptr limb) : unit
  requires { offset p = 0 }
  requires { writable p }
  requires { min p = 0 }
  requires { max p = plength p }
  requires { plength p = mpz.alloc[x] }
  requires { mpz.readers[x] = 0 \/ mpz.readers[x] = -1 }
  writes   { mpz.abs_value_of }
  writes   { mpz.zones }
  writes   { mpz.readers }
  ensures  { forall y. y <> x -> mpz_unchanged y mpz (old mpz) }
  ensures  { mpz.abs_value_of[x] = value p (mpz.abs_size[x]) }
  ensures  { mpz.readers[x] = -1 }
  ensures  { mpz.zones[x] = zone p }
  ensures  { min p = 0 }
  ensures  { max p = plength p }
  ensures  { plength p = old plength p }
  ensures  { pelts p = old pelts p }

val ghost value_of (x: mpz_ptr) : int
  ensures { result = mpz.sgn[x] * mpz.abs_value_of[x] }

val get_read_ptr (x: mpz_ptr) : ptr limb
  requires { mpz.readers[x] >= 0 }
  writes   { mpz.readers }
  ensures  { mpz.readers[x] = old mpz.readers[x] + 1 }
  ensures  { forall y. x <> y -> mpz.readers[y] = old mpz.readers[y] }
  ensures  { value result (mpz.abs_size[x]) = mpz.abs_value_of[x] }
  ensures  { plength result = mpz.alloc[x] }
  ensures  { offset result = 0 }
  ensures  { min result = 0 }
  ensures  { max result = plength result }
  ensures  { zone result = mpz.zones[x] }

val get_write_ptr (x: mpz_ptr) : ptr limb
  requires { mpz.readers[x] = 0 }
  writes   { mpz.readers }
  ensures  { mpz.readers[x] = -1 }
  ensures  { forall y. x <> y -> mpz.readers[y] = old mpz.readers[y] }
  ensures  { value result (mpz.abs_size[x]) = mpz.abs_value_of[x] }
  ensures  { plength result = mpz.alloc[x] }
  ensures  { offset result = 0 }
  ensures  { min result = 0 }
  ensures  { max result = plength result }
  ensures  { writable result }
  ensures  { zone result = mpz.zones[x] }

val release_reader (x: mpz_ptr) (p:ptr limb) : unit
  requires { mpz.zones[x] = zone p }
  requires { mpz.readers[x] >= 1 }
  requires { min p = 0 }
  requires { max p = plength p }
  writes   { mpz.readers }
  writes   { p } (* invalidates p and its aliases *)
  ensures  { mpz.readers[x] = old mpz.readers[x] - 1 }
  ensures  { forall y. y <> x -> mpz.readers[y] = old mpz.readers[y] }

val release_writer (x: mpz_ptr) (p:ptr limb) : unit
  requires { mpz.zones[x] = zone p }
  requires { mpz.readers[x] = -1 }
  requires { min p = 0 }
  requires { max p = plength p }
  requires { writable p } (* maybe not needed? *)
  writes   { mpz.readers }
  writes   { p } (* invalidates p and its aliases *)
  ensures  { mpz.readers[x] = 0 }
  ensures  { forall y. y <> x -> mpz.readers[y] = old mpz.readers[y] }

type mpz_mem = abstract { ptr: mpz_ptr; mutable ok: bool }

val wmpz_struct_to_ptr (x:mpz_struct)
    : (res:mpz_ptr, ghost memo:mpz_mem)
  writes  { mpz }
  ensures { res = x.addr }
  ensures { memo.ptr = res }
  ensures { memo.ok }
  ensures { mpz.alloc[res] = 0 }
  ensures { mpz.abs_size[res] = 0 }
  ensures { mpz.readers[res] = old mpz.readers[res] }
  ensures { forall y. y <> x.addr -> mpz_unchanged y mpz (old mpz) }

val wmpz_tmp_decl [@extraction:c_declaration] () : mpz_struct
  writes  { mpz }
  ensures { old mpz.readers[result.addr] = -2 }
  ensures { forall x. x <> result.addr -> mpz_unchanged x mpz (old mpz) }
  ensures { mpz.readers[result.addr] = 0 }
            (*result is fresh*)

val wmpz_tmp_clear (x:mpz_ptr) (memo: mpz_mem) : unit
  requires { memo.ok }
  requires { x = memo.ptr }
  requires { -1 <= mpz.readers[x] <= 0 }
  writes   { mpz }
  writes   { memo }
  ensures  { mpz.readers[x] = -2 }
  ensures  { forall y. y <> x -> mpz_unchanged y mpz (old mpz) }

let wmpz_ptr_decl [@extraction:inline] () : (ptr: mpz_ptr, ghost memo:mpz_mem)
  writes  { mpz }
  ensures { ptr = memo.ptr }
  ensures { memo.ok }
  ensures { mpz.readers[ptr] = 0 }
  ensures { mpz.alloc[ptr] = 0 }
  ensures { mpz.abs_size[ptr] = 0 }
  ensures { old mpz.readers[ptr] = -2 }
  ensures { forall x. x <> ptr -> mpz_unchanged x mpz (old mpz) }
=
  let t = wmpz_tmp_decl () in
  wmpz_struct_to_ptr t

val partial wmpz_init (p: mpz_ptr) : unit
  requires { mpz.readers[p] = 0 }
  writes  { mpz }
  ensures { forall x. x <> p -> mpz_unchanged x mpz (old mpz) }
  ensures { mpz.readers[p] = 0 }
  ensures { mpz.abs_value_of[p] = 0 }
  ensures { mpz.abs_size[p] = 0 }
  ensures { mpz.sgn[p] = 1 }
  ensures { mpz.alloc[p] = 1 }
  ensures { mpz.zones[p] <> null_zone }

val wmpz_clear (x:mpz_ptr) : unit (* scrambles mpz._[x] *)
  writes { mpz }
  requires { mpz.readers[x] = 0 }
  ensures { forall y. y <> x -> mpz_unchanged y mpz (old mpz) }

let partial wmpz_do_realloc (x:mpz_ptr) (sz:int32) : ptr limb
  requires { 1 <= sz } (* GMP does sz = max (sz,1) instead, do that if needed *)
  requires { mpz.readers[x] = 0 }
  requires { 1 <= mpz.alloc[x] }
  ensures { forall y. y <> x -> mpz_unchanged y mpz (old mpz) }
  ensures  { mpz.readers[x] = -1 }
  ensures  { mpz.alloc[x] = sz }
  ensures  { mpz.abs_value_of[x] = value result (mpz.abs_size[x]) }
  ensures  { mpz.zones[x] = zone result }
  ensures  { offset result = 0 }
  ensures  { plength result = sz }
  ensures  { min result = 0 }
  ensures  { max result = sz }
  ensures  { writable result }
  ensures  { if sz >= old mpz.abs_size[x]
             then mpz.abs_size[x] = old mpz.abs_size[x]
                  /\ value result (old mpz.abs_size[x])
                     = old mpz.abs_value_of[x]
             else mpz.abs_size[x] = 0 }
= let p = get_write_ptr x in
  assert { forall y. y <> x -> mpz_unchanged y mpz (old mpz) };
  let ghost op = { p } in
  let ghost os = abs_size_of x in
  label Realloc in
  let q = realloc p sz in
  c_assert (is_not_null q);
  if Int32.(>) (abs_size_of x) sz
  then begin
    set_size_0 x; (* data has shrunk, reset x to 0 *)
  end
  else begin
    value_sub_frame (pelts q) (pelts op) 0 (p2i os);
  end;
  set_alloc x sz;
  set_ptr x q;
  q

let wmpz_realloc (x:mpz_ptr) (sz:int32) : ptr limb
  requires { mpz.readers[x] = 0 }
  requires { 1 <= mpz.alloc[x] }
  ensures  { forall y. y <> x -> mpz_unchanged y mpz (old mpz) }
  ensures  { mpz.readers[x] = -1 }
  ensures  { mpz.abs_value_of[x] = value result (mpz.abs_size[x]) }
  ensures  { mpz.zones[x] = zone result }
  ensures  { offset result = 0 }
  ensures  { plength result = mpz.alloc[x] }
  ensures  { min result = 0 }
  ensures  { max result = plength result }
  ensures  { writable result }
  ensures  { mpz.abs_size[x] = old mpz.abs_size[x] }
  ensures  { value result (old mpz.abs_size[x])
             = old mpz.abs_value_of[x] }
  ensures  { if sz > old mpz.alloc[x]
             then mpz.alloc[x] = sz
             else mpz.alloc[x] = old mpz.alloc[x]  }
= if sz > alloc_of x
  then wmpz_do_realloc x sz
  else get_write_ptr x

let mpz_ptr_swap [@extraction:inline] (ref x y: mpz_ptr)
  requires { mpz.readers[x] = 0 /\ mpz.readers[y] = 0 }
  ensures  { mpz.readers[x] = 0 /\ mpz.readers[y] = 0 }
  ensures  { x = old y }
  ensures  { y = old x }
= let z = x in
  x <- y;
  y <- z

end