# Uint63 numbers defines indeed a cyclic structure : Z/(2^63)Z

Author: Arnaud Spiwack (+ Pierre Letouzey)
Require Import CyclicAxioms.
Require Export ZArith.
Require Export Uint63.
Import Zpow_facts.
Import Utf8.
Import Lia.

Local Open Scope uint63_scope.
{2 Operators }

Definition Pdigits := Eval compute in P_of_succ_nat (size - 1).

Fixpoint positive_to_int_rec (n:nat) (p:positive) :=
match n, p with
| O, _ => (Npos p, 0)
| S n, xH => (0%N, 1)
| S n, xO p =>
let (N,i) := positive_to_int_rec n p in
(N, i << 1)
| S n, xI p =>
let (N,i) := positive_to_int_rec n p in
(N, (i << 1) + 1)
end.

Definition positive_to_int := positive_to_int_rec size.

Definition mulc_WW x y :=
let (h, l) := mulc x y in
if is_zero h then
if is_zero l then W0
else WW h l
else WW h l.
Notation "n '*c' m" := (mulc_WW n m) (at level 40, no associativity) : uint63_scope.

Definition pos_mod p x :=
if p <=? digits then
let p := digits - p in
(x << p) >> p
else x.

Notation pos_mod_int := pos_mod.

Import ZnZ.

#[global]
Instance int_ops : ZnZ.Ops int :=
{|
digits := Pdigits;
zdigits := Uint63.digits;
to_Z := Uint63.to_Z;
of_pos := positive_to_int;
head0 := Uint63.head0;
tail0 := Uint63.tail0;
zero := 0;
one := 1;
minus_one := Uint63.max_int;
compare := Uint63.compare;
eq0 := Uint63.is_zero;
opp_c := Uint63.oppc;
opp := Uint63.opp;
opp_carry := Uint63.oppcarry;
succ_c := Uint63.succc;
add_c := Uint63.addc;
add_carry_c := Uint63.addcarryc;
succ := Uint63.succ;
add := Uint63.add;
add_carry := Uint63.addcarry;
pred_c := Uint63.predc;
sub_c := Uint63.subc;
sub_carry_c := Uint63.subcarryc;
pred := Uint63.pred;
sub := Uint63.sub;
sub_carry := Uint63.subcarry;
mul_c := mulc_WW;
mul := Uint63.mul;
square_c := fun x => mulc_WW x x;
div21 := diveucl_21;
div_gt := diveucl;
div := diveucl;
modulo_gt := Uint63.mod;
modulo := Uint63.mod;
gcd_gt := Uint63.gcd;
gcd := Uint63.gcd;
add_mul_div := Uint63.addmuldiv;
pos_mod := pos_mod_int;
is_even := Uint63.is_even;
sqrt2 := Uint63.sqrt2;
sqrt := Uint63.sqrt;
ZnZ.lor := Uint63.lor;
ZnZ.land := Uint63.land;
ZnZ.lxor := Uint63.lxor
|}.

Local Open Scope Z_scope.

Lemma is_zero_spec_aux : forall x : int, is_zero x = true -> φ x = 0%Z.

Lemma positive_to_int_spec :
forall p : positive,
Zpos p =
Z_of_N (fst (positive_to_int p)) * wB + to_Z (snd (positive_to_int p)).

Lemma mulc_WW_spec :
forall x y, Φ ( x *c y ) = φ x * φ y.

Lemma squarec_spec :
forall x,
Φ(x *c x) = φ x * φ x.

Lemma diveucl_spec_aux : forall a b, 0 < φ b ->
let (q,r) := diveucl a b in
φ a = φ q * φ b + φ r /\
0 <= φ r < φ b.

Lemma shift_unshift_mod_2 : forall n p a, 0 <= p <= n ->
((a * 2 ^ (n - p)) mod (2^n) / 2 ^ (n - p)) mod (2^n) =
a mod 2 ^ p.

Lemma div_le_0 : forall p x, 0 <= x -> 0 <= x / 2 ^ p.

Lemma div_lt : forall p x y, 0 <= x < y -> x / 2^p < y.

Lemma P (A B C: Prop) :
A (B C) (A B) C.

Lemma shift_unshift_mod_3:
forall n p a : Z,
0 <= p <= n ->
(a * 2 ^ (n - p)) mod 2 ^ n / 2 ^ (n - p) = a mod 2 ^ p.

Lemma pos_mod_spec w p : φ(pos_mod p w) = φ(w) mod (2 ^ φ(p)).

{2 Specification and proof}