Library Coq.Numbers.Cyclic.Int63.Sint63

Require Import ZArith.
Import Znumtheory.
Require Export Uint63.
Require Int63.
Require Import Lia.

Declare Scope sint63_scope.
Definition printer (x : int_wrapper) : pos_neg_int63 :=
  if (int_wrap x <? 4611686018427387904)%uint63 then
    Pos (int_wrap x)
  else
    Neg ((int_wrap x) lxor max_int + 1)%uint63.
Definition parser (x : pos_neg_int63) : option int :=
  match x with
  | Pos p => if (p <? 4611686018427387904)%uint63 then Some p else None
  | Neg n => if (n <=? 4611686018427387904)%uint63
             then Some ((n - 1) lxor max_int)%uint63 else None
  end.

Module Import Sint63NotationsInternalA.
Delimit Scope sint63_scope with sint63.
Bind Scope sint63_scope with int.
End Sint63NotationsInternalA.

Module Import Sint63NotationsInternalB.
Infix "<<" := Int63.lsl (at level 30, no associativity) : sint63_scope.
Infix ">>" := asr (at level 30, no associativity) : sint63_scope.
Infix "land" := Int63.land (at level 40, left associativity) : sint63_scope.
Infix "lor" := Int63.lor (at level 40, left associativity) : sint63_scope.
Infix "lxor" := Int63.lxor (at level 40, left associativity) : sint63_scope.
Infix "+" := Int63.add : sint63_scope.
Infix "-" := Int63.sub : sint63_scope.
Infix "*" := Int63.mul : sint63_scope.
Infix "/" := divs : sint63_scope.
Infix "mod" := mods (at level 40, no associativity) : sint63_scope.
Infix "=?" := Int63.eqb (at level 70, no associativity) : sint63_scope.
Infix "<?" := ltsb (at level 70, no associativity) : sint63_scope.
Infix "<=?" := lesb (at level 70, no associativity) : sint63_scope.
Infix "≤?" := lesb (at level 70, no associativity) : sint63_scope.
Notation "- x" := (opp x) : sint63_scope.
Notation "n ?= m" := (compares n m)
  (at level 70, no associativity) : sint63_scope.
End Sint63NotationsInternalB.

Definition min_int := Eval vm_compute in (lsl 1 62).
Definition max_int := Eval vm_compute in (min_int - 1)%sint63.

Definition to_Z (i : int) :=
  if (i <? min_int)%uint63 then
    φ i%uint63
  else
    (- φ (- i)%uint63)%Z.

Lemma to_Z_0 : to_Z 0 = 0.

Lemma to_Z_min : to_Z min_int = - (wB / 2).

Lemma to_Z_max : to_Z max_int = wB / 2 - 1.

Lemma to_Z_bounded : forall x, (to_Z min_int <= to_Z x <= to_Z max_int)%Z.

Lemma of_to_Z : forall x, of_Z (to_Z x) = x.

Lemma to_Z_inj (x y : int) : to_Z x = to_Z y -> x = y.

Lemma to_Z_mod_Uint63to_Z (x : int) : to_Z x mod wB = φ x%uint63.

Definition cmod (x d : Z) : Z :=
  (x + d / 2) mod d - (d / 2).

Lemma cmod_mod (x d : Z) :
  cmod (x mod d) d = cmod x d.

Lemma cmod_small (x d : Z) :
  - (d / 2) <= x < d / 2 -> cmod x d = x.

Lemma to_Z_cmodwB (x : int) :
  to_Z x = cmod (φ x%uint63) wB.

Lemma of_Z_spec (z : Z) : to_Z (of_Z z) = cmod z wB.

Lemma of_Z_cmod (z : Z) : of_Z (cmod z wB) = of_Z z.

Lemma is_int (z : Z) :
    to_Z min_int <= z <= to_Z max_int ->
  z = to_Z (of_Z z).

Lemma of_pos_spec (p : positive) :
  to_Z (of_pos p) = cmod (Zpos p) wB.

Axiom asr_spec : forall x p, to_Z (x >> p) = (to_Z x) / 2 ^ (to_Z p).

Axiom div_spec : forall x y,
    to_Z x <> to_Z min_int \/ to_Z y <> (-1)%Z ->
  to_Z (x / y) = Z.quot (to_Z x) (to_Z y).

Axiom mod_spec : forall x y, to_Z (x mod y) = Z.rem (to_Z x) (to_Z y).

Axiom ltb_spec : forall x y, (x <? y)%sint63 = true <-> to_Z x < to_Z y.

Axiom leb_spec : forall x y, (x <=? y)%sint63 = true <-> to_Z x <= to_Z y.

Axiom compare_spec : forall x y, (x ?= y)%sint63 = (to_Z x ?= to_Z y).

Lemma add_spec (x y : int) :
  to_Z (x + y)%sint63 = cmod (to_Z x + to_Z y) wB.

Lemma sub_spec (x y : int) :
  to_Z (x - y)%sint63 = cmod (to_Z x - to_Z y) wB.

Lemma mul_spec (x y : int) :
  to_Z (x * y)%sint63 = cmod (to_Z x * to_Z y) wB.

Lemma succ_spec (x : int) :
  to_Z (succ x)%sint63 = cmod (to_Z x + 1) wB.

Lemma pred_spec (x : int) :
  to_Z (pred x)%sint63 = cmod (to_Z x - 1) wB.

Lemma opp_spec (x : int) :
  to_Z (- x)%sint63 = cmod (- to_Z x) wB.

Lemma to_Z_add (x y : int) :
    to_Z min_int <= to_Z x + to_Z y <= to_Z max_int ->
  to_Z (x + y) = to_Z x + to_Z y.

Lemma to_Z_sub (x y : int) :
    to_Z min_int <= to_Z x - to_Z y <= to_Z max_int ->
  to_Z (x - y) = to_Z x - to_Z y.

Lemma to_Z_mul (x y : int) :
    to_Z min_int <= to_Z x * to_Z y <= to_Z max_int ->
  to_Z (x * y) = to_Z x * to_Z y.

Lemma to_Z_succ (x : int) :
  x <> max_int -> to_Z (succ x) = to_Z x + 1.

Lemma to_Z_pred (x : int) :
  x <> min_int -> to_Z (pred x) = to_Z x - 1.

Lemma to_Z_opp (x : int) :
  x <> min_int -> to_Z (- x) = - to_Z x.

Lemma add_of_Z (x y : int) :
  (x + y)%sint63 = of_Z (to_Z x + to_Z y).

Lemma sub_of_Z (x y : int) :
  (x - y)%sint63 = of_Z (to_Z x - to_Z y).

Lemma mul_of_Z (x y : int) :
  (x * y)%sint63 = of_Z (to_Z x * to_Z y).

Lemma succ_of_Z (x : int) :
  (succ x)%sint63 = of_Z (to_Z x + 1).

Lemma pred_of_Z (x : int) :
  (pred x)%sint63 = of_Z (to_Z x - 1).

Lemma opp_of_Z (x : int) :
  (- x)%sint63 = of_Z (- to_Z x).

Import Bool.

Lemma eqbP x y : reflect (to_Z x = to_Z y) (x =? y)%sint63.

Lemma ltbP x y : reflect (to_Z x < to_Z y) (x <? y)%sint63.

Lemma lebP x y : reflect (to_Z x <= to_Z y) (x ≤? y)%sint63.

Definition abs (n : int) : int := if (0 <=? n)%sint63 then n else - n.

Lemma abs_spec (x : int) :
  to_Z (abs x)%sint63 = cmod (Z.abs (to_Z x)) wB.

Lemma to_Z_abs (x : int) :
  x <> min_int -> to_Z (abs x) = Z.abs (to_Z x).

Remark abs_min_int : abs min_int = min_int.

Lemma abs_of_Z (x : int) :
  abs x = of_Z (Z.abs (to_Z x)).

Lemma asr_0 (i : int) : (0 >> i)%sint63 = 0%sint63.

Lemma asr_0_r (i : int) : (i >> 0)%sint63 = i.

Lemma asr_neg_r (i n : int) : to_Z n < 0 -> (i >> n)%sint63 = 0%sint63.

Lemma asr_1 (n : int) : (1 >> n)%sint63 = (n =? 0)%sint63.

Notation asr := asr (only parsing).
Notation div := divs (only parsing).
Notation rem := mods (only parsing).
Notation ltb := ltsb (only parsing).
Notation leb := lesb (only parsing).
Notation compare := compares (only parsing).

Module Export Sint63Notations.
  Export Sint63NotationsInternalA.
  Export Sint63NotationsInternalB.
End Sint63Notations.