Library Corelib.Numbers.Cyclic.Int63.Sint63Axioms

From Corelib Require Import BinNums PosDef IntDef.
From Corelib Require Export PrimInt63 Uint63Axioms.

Local Open Scope Z_scope.

Local Notation "2" := (Zpos 2) : Z_scope.
Local Infix "^" := Z.pow : Z_scope.
Local Notation "x <= y" := (Z.compare x y <> Gt) : Z_scope.
Local Notation "x < y" := (Z.compare x y = Lt) : Z_scope.

Definition min_int := Eval vm_compute in (lsl 1 62).

Translation to and from Z

Definition to_Z (i : int) :=
if ltb i min_int then to_Z i
else Z.opp (to_Z (sub 0 i)).

Specification of operations that differ on signed and unsigned ints

Axiom asr_spec : forall x p, to_Z (asr x p) = Z.div (to_Z x) (2 ^ (to_Z p )).

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

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

Axiom ltb_spec : forall x y, ltsb x y = true <-> to_Z x < to_Z y.

Axiom leb_spec : forall x y, lesb x y = true <-> to_Z x <= to_Z y.

Axiom compare_spec : forall x y, compares x y = Z.compare (to_Z x) (to_Z y).