Require Import CyclicAxioms.
Require Export ZArith.
Require Export Uint63.
Import Zpow_facts.
Import Utf8.
Import Lia.

Local Open Scope uint63_scope.

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)).

Global Instance int_specs : ZnZ.Specs int_ops := {
    spec_to_Z := to_Z_bounded;
    spec_of_pos := positive_to_int_spec;
    spec_zdigits := refl_equal _;
    spec_more_than_1_digit:= refl_equal _;
    spec_0 := to_Z_0;
    spec_1 := to_Z_1;
    spec_m1 := refl_equal _;
    spec_compare := compare_spec;
    spec_eq0 := is_zero_spec_aux;
    spec_opp_c := oppc_spec;
    spec_opp := opp_spec;
    spec_opp_carry := oppcarry_spec;
    spec_succ_c := succc_spec;
    spec_add_c := addc_spec;
    spec_add_carry_c := addcarryc_spec;
    spec_succ := succ_spec;
    spec_add := add_spec;
    spec_add_carry := addcarry_spec;
    spec_pred_c := predc_spec;
    spec_sub_c := subc_spec;
    spec_sub_carry_c := subcarryc_spec;
    spec_pred := pred_spec;
    spec_sub := sub_spec;
    spec_sub_carry := subcarry_spec;
    spec_mul_c := mulc_WW_spec;
    spec_mul := mul_spec;
    spec_square_c := squarec_spec;
    spec_div21 := diveucl_21_spec_aux;
    spec_div_gt := fun a b _ => diveucl_spec_aux a b;
    spec_div := diveucl_spec_aux;
    spec_modulo_gt := fun a b _ _ => mod_spec a b;
    spec_modulo := fun a b _ => mod_spec a b;
    spec_gcd_gt := fun a b _ => gcd_spec a b;
    spec_gcd := gcd_spec;
    spec_head00 := head00_spec;
    spec_head0 := head0_spec;
    spec_tail00 := tail00_spec;
    spec_tail0 := tail0_spec;
    spec_add_mul_div := addmuldiv_spec;
    spec_pos_mod := pos_mod_spec;
    spec_is_even := is_even_spec;
    spec_sqrt2 := sqrt2_spec;
    spec_sqrt := sqrt_spec;
    spec_land := land_spec';
    spec_lor := lor_spec';
    spec_lxor := lxor_spec' }.

Module Uint63Cyclic <: CyclicType.
  Definition t := int.
  Definition ops := int_ops.
  Definition specs := int_specs.
End Uint63Cyclic.