Library Coq.Numbers.Cyclic.Int31.Cyclic31

Int31 numbers defines indeed a cyclic structure : Z/(2^31)Z

Author: Arnaud Spiwack (+ Pierre Letouzey)

Require Import List.
Require Import Min.
Require Export Int31.
Require Import Znumtheory.
Require Import Zgcd_alt.
Require Import Zpow_facts.
Require Import CyclicAxioms.
Require Import Lia.

Local Open Scope nat_scope.
Local Open Scope int31_scope.

Local Hint Resolve Z.lt_gt Z.div_pos : zarith.

Section Basics.

Basic results about iszero, shiftl, shiftr

Lemma iszero_eq0 : forall x, iszero x = true -> x =0.

Lemma iszero_not_eq0 : forall x, iszero x = false -> x <>0.

Lemma sneakl_shiftr : forall x,
  x = sneakl (firstr x) (shiftr x).

Lemma sneakr_shiftl : forall x,
  x = sneakr (firstl x) (shiftl x).

Lemma twice_zero : forall x,
  twice x = 0 <-> twice_plus_one x = 1.

Lemma twice_or_twice_plus_one : forall x,
  x = twice (shiftr x) \/ x = twice_plus_one (shiftr x).

Iterated shift to the right

Definition nshiftr x := nat_rect _ x (fun _ => shiftr).

Lemma nshiftr_S :
  forall n x, nshiftr x (S n) = shiftr (nshiftr x n).

Lemma nshiftr_S_tail :
  forall n x, nshiftr x (S n) = nshiftr (shiftr x) n.

Lemma nshiftr_n_0 : forall n, nshiftr 0 n = 0.

Lemma nshiftr_size : forall x, nshiftr x size = 0.

Lemma nshiftr_above_size : forall k x, size <=k ->
  nshiftr x k = 0.

Iterated shift to the left

Definition nshiftl x := nat_rect _ x (fun _ => shiftl).

Lemma nshiftl_S :
  forall n x, nshiftl x (S n) = shiftl (nshiftl x n).

Lemma nshiftl_S_tail :
  forall n x, nshiftl x (S n) = nshiftl (shiftl x) n.

Lemma nshiftl_n_0 : forall n, nshiftl 0 n = 0.

Lemma nshiftl_size : forall x, nshiftl x size = 0.

Lemma nshiftl_above_size : forall k x, size <=k ->
  nshiftl x k = 0.

Lemma firstr_firstl :
  forall x, firstr x = firstl (nshiftl x (pred size)).

Lemma firstl_firstr :
  forall x, firstl x = firstr (nshiftr x (pred size)).

More advanced results about nshiftr

Lemma nshiftr_predsize_0_firstl : forall x,
  nshiftr x (pred size) = 0 -> firstl x = D0.

Lemma nshiftr_0_propagates : forall n p x, n <= p ->
  nshiftr x n = 0 -> nshiftr x p = 0.

Lemma nshiftr_0_firstl : forall n x, n < size ->
  nshiftr x n = 0 -> firstl x = D0.

Some induction principles over int31

Not used for the moment. Are they really useful ?

Lemma int31_ind_sneakl : forall P : int31 ->Prop,
  P 0 ->
  (forall x d, P x -> P (sneakl d x)) ->
  forall x, P x.

Lemma int31_ind_twice : forall P : int31 ->Prop,
  P 0 ->
  (forall x, P x -> P (twice x)) ->
  (forall x, P x -> P (twice_plus_one x)) ->
  forall x, P x.

Some generic results about recr

Section Recr.

recr satisfies the fixpoint equation used for its definition.

Variable (A:Type)(case0:A)(caserec:digits ->int31 ->A ->A).

Lemma recr_aux_eqn : forall n x, iszero x = false ->
   recr_aux (S n) A case0 caserec x =
   caserec (firstr x) (shiftr x) (recr_aux n A case0 caserec (shiftr x)).

Lemma recr_aux_converges :
  forall n p x, n <= size -> n <= p ->
  recr_aux n A case0 caserec (nshiftr x (size - n)) =
  recr_aux p A case0 caserec (nshiftr x (size - n)).

Lemma recr_eqn : forall x, iszero x = false ->
  recr A case0 caserec x =
  caserec (firstr x) (shiftr x) (recr A case0 caserec (shiftr x)).

recr is usually equivalent to a variant recrbis written without iszero check.

Fixpoint recrbis_aux (n:nat)(A:Type)(case0:A)(caserec:digits ->int31 ->A ->A)
(i:int31) : A :=
  match n with
  | O => case0
  | S next =>
      let si := shiftr i in
      caserec (firstr i) si (recrbis_aux next A case0 caserec si)
  end.

Definition recrbis := recrbis_aux size.

Hypothesis case0_caserec : caserec D0 0 case0 = case0.

Lemma recrbis_aux_equiv : forall n x,
   recrbis_aux n A case0 caserec x = recr_aux n A case0 caserec x.

Lemma recrbis_equiv : forall x,
   recrbis A case0 caserec x = recr A case0 caserec x.

End Recr.

Incrementation

Section Incr.

Variant of incr via recrbis

Let Incr (b : digits) (si rec : int31) :=
  match b with
   | D0 => sneakl D1 si
   | D1 => sneakl D0 rec
  end.

Definition incrbis_aux n x := recrbis_aux n _ In Incr x.

Lemma incrbis_aux_equiv : forall x, incrbis_aux size x = incr x.

Recursive equations satisfied by incr

Lemma incr_eqn1 :
  forall x, firstr x = D0 -> incr x = twice_plus_one (shiftr x).

Lemma incr_eqn2 :
  forall x, firstr x = D1 -> incr x = twice (incr (shiftr x)).

Lemma incr_twice : forall x, incr (twice x) = twice_plus_one x.

Lemma incr_twice_plus_one_firstl :
  forall x, firstl x = D0 -> incr (twice_plus_one x) = twice (incr x).

The previous result is actually true even without the constraint on firstl, but this is harder to prove (see later).

End Incr.

Conversion to Z : the phi function

Section Phi.

Variant of phi via recrbis

Let Phi := fun b (_:int31) =>
match b with D0 => Z.double | D1 => Z.succ_double end.

Definition phibis_aux n x := recrbis_aux n _ Z0 Phi x.

Lemma phibis_aux_equiv : forall x, phibis_aux size x = phi x.

Recursive equations satisfied by phi

Lemma phi_eqn1 : forall x, firstr x = D0 ->
  phi x = Z.double (phi (shiftr x)).

Lemma phi_eqn2 : forall x, firstr x = D1 ->
  phi x = Z.succ_double (phi (shiftr x)).

Lemma phi_twice_firstl : forall x, firstl x = D0 ->
  phi (twice x) = Z.double (phi x).

Lemma phi_twice_plus_one_firstl : forall x, firstl x = D0 ->
  phi (twice_plus_one x) = Z.succ_double (phi x).

End Phi.

phi x is positive and lower than 2^31

Lemma phibis_aux_pos : forall n x, (0 <= phibis_aux n x)%Z.

Lemma phibis_aux_bounded :
  forall n x, n <= size ->
  (phibis_aux n (nshiftr x (size -n)) < 2 ^ (Z.of_nat n ))%Z.

Lemma phi_nonneg : forall x, (0 <= phi x)%Z.

Hint Resolve phi_nonneg : zarith.

Lemma phi_bounded : forall x, (0 <= phi x < 2 ^ (Z.of_nat size ))%Z.

Lemma phibis_aux_lowerbound :
  forall n x, firstr (nshiftr x n) = D1 ->
  (2 ^ Z.of_nat n <= phibis_aux (S n) x)%Z.

Lemma phi_lowerbound :
  forall x, firstl x = D1 -> (2^(Z.of_nat (pred size)) <= phi x)%Z.

Equivalence modulo 2^n

Section EqShiftL.

After killing n bits at the left, are the numbers equal ?

Definition EqShiftL n x y :=
  nshiftl x n = nshiftl y n.

Lemma EqShiftL_zero : forall x y, EqShiftL O x y <-> x = y.

Lemma EqShiftL_size : forall k x y, size <=k -> EqShiftL k x y.

Lemma EqShiftL_le : forall k k' x y, k <= k' ->
   EqShiftL k x y -> EqShiftL k' x y.

Lemma EqShiftL_firstr : forall k x y, k < size ->
  EqShiftL k x y -> firstr x = firstr y.

Lemma EqShiftL_twice : forall k x y,
  EqShiftL k (twice x) (twice y) <-> EqShiftL (S k) x y.

From int31 to list of digits.

Lower (=rightmost) bits comes first.

Definition i2l := recrbis _ nil (fun d _ rec => d ::rec).

Lemma i2l_length : forall x, length (i2l x) = size.

Fixpoint lshiftl l x :=
   match l with
     | nil => x
     | d::l => sneakl d (lshiftl l x)
   end.

Definition l2i l := lshiftl l On.

Lemma l2i_i2l : forall x, l2i (i2l x) = x.

Lemma i2l_sneakr : forall x d,
   i2l (sneakr d x) = tail (i2l x) ++ d ::nil.

Lemma i2l_sneakl : forall x d,
   i2l (sneakl d x) = d :: removelast (i2l x).

Lemma i2l_l2i : forall l, length l = size ->
  i2l (l2i l) = l.

Fixpoint cstlist (A:Type)(a:A) n :=
  match n with
   | O => nil
   | S n => a ::cstlist _ a n
  end.

Lemma i2l_nshiftl : forall n x, n <=size ->
  i2l (nshiftl x n) = cstlist _ D0 n ++ firstn (size -n) (i2l x).

i2l can be used to define a relation equivalent to EqShiftL

Lemma EqShiftL_i2l : forall k x y,
EqShiftL k x y <-> firstn (size -k) (i2l x) = firstn (size -k) (i2l y).

This equivalence allows proving easily the following delicate result

Lemma EqShiftL_twice_plus_one : forall k x y,
  EqShiftL k (twice_plus_one x) (twice_plus_one y) <-> EqShiftL (S k) x y.

Lemma EqShiftL_shiftr : forall k x y, EqShiftL k x y ->
  EqShiftL (S k) (shiftr x) (shiftr y).

Lemma EqShiftL_incrbis : forall n k x y, n <=size ->
  (n +k =S size)%nat ->
  EqShiftL k x y ->
  EqShiftL k (incrbis_aux n x) (incrbis_aux n y).

Lemma EqShiftL_incr : forall x y,
  EqShiftL 1 x y -> EqShiftL 1 (incr x) (incr y).

End EqShiftL.

More equations about incr

Lemma incr_twice_plus_one :
forall x, incr (twice_plus_one x) = twice (incr x).

Lemma incr_firstr : forall x, firstr (incr x) <> firstr x.

Lemma incr_inv : forall x y,
incr x = twice_plus_one y -> x = twice y.

Conversion from Z : the phi_inv function

First, recursive equations

Lemma phi_inv_double_plus_one : forall z,
   phi_inv (Z.succ_double z) = twice_plus_one (phi_inv z).

Lemma phi_inv_double : forall z,
   phi_inv (Z.double z) = twice (phi_inv z).

Lemma phi_inv_incr : forall z,
  phi_inv (Z.succ z) = incr (phi_inv z).

phi_inv o inv, the always-exact and easy-to-prove trip : from int31 to Z and then back to int31.

Lemma phi_inv_phi_aux :
  forall n x, n <= size ->
   phi_inv (phibis_aux n (nshiftr x (size -n))) =
   nshiftr x (size -n).

Lemma phi_inv_phi : forall x, phi_inv (phi x) = x.

The other composition phi o phi_inv is harder to prove correct. In particular, an overflow can happen, so a modulo is needed. For the moment, we proceed via several steps, the first one being a detour to positive_to_in31.

positive_to_int31

A variant of p2i with twice and twice_plus_one instead of 2*i and 2*i+1

Fixpoint p2ibis n p : (N *int31)%type :=
  match n with
    | O => (Npos p , On )
    | S n => match p with
               | xO p => let (r,i) := p2ibis n p in (r , twice i )
               | xI p => let (r,i) := p2ibis n p in (r , twice_plus_one i )
               | xH => (N0 , In )
             end
  end.

Lemma p2ibis_bounded : forall n p,
  nshiftr (snd (p2ibis n p)) n = 0.

Local Open Scope Z_scope.

Lemma p2ibis_spec : forall n p, (n <=size)%nat ->
    Zpos p = (Z.of_N (fst (p2ibis n p)))*2^(Z.of_nat n ) +
             phi (snd (p2ibis n p)).

We now prove that this p2ibis is related to phi_inv_positive

Lemma phi_inv_positive_p2ibis : forall n p, (n <=size)%nat ->
EqShiftL (size -n) (phi_inv_positive p) (snd (p2ibis n p)).

This gives the expected result about phi o phi_inv, at least for the positive case.

Lemma phi_phi_inv_positive : forall p,
phi (phi_inv_positive p) = (Zpos p ) mod (2^(Z.of_nat size )).

Moreover, p2ibis is also related with p2i and hence with positive_to_int31.

Lemma double_twice_firstl : forall x, firstl x = D0 ->
  (Twon *x = twice x)%int31.

Lemma double_twice_plus_one_firstl : forall x, firstl x = D0 ->
  (Twon *x +In = twice_plus_one x)%int31.

Lemma p2i_p2ibis : forall n p, (n <=size)%nat ->
  p2i n p = p2ibis n p.

Lemma positive_to_int31_phi_inv_positive : forall p,
   snd (positive_to_int31 p) = phi_inv_positive p.

Lemma positive_to_int31_spec : forall p,
    Zpos p = (Z.of_N (fst (positive_to_int31 p)))*2^(Z.of_nat size ) +
               phi (snd (positive_to_int31 p)).

Thanks to the result about phi o phi_inv_positive, we can now establish easily the most general results about phi o twice and so one.

Lemma phi_twice : forall x,
   phi (twice x) = (Z.double (phi x)) mod 2^(Z.of_nat size ).

Lemma phi_twice_plus_one : forall x,
   phi (twice_plus_one x) = (Z.succ_double (phi x)) mod 2^(Z.of_nat size ).

Lemma phi_incr : forall x,
   phi (incr x) = (Z.succ (phi x)) mod 2^(Z.of_nat size ).

With the previous results, we can deal with phi o phi_inv even in the negative case

Lemma phi_phi_inv_negative :
  forall p, phi (incr (complement_negative p)) = (Zneg p ) mod 2^(Z.of_nat size ).

Lemma phi_phi_inv :
  forall z, phi (phi_inv z) = z mod 2 ^ (Z.of_nat size ).

End Basics.

Instance int31_ops : ZnZ.Ops int31 :=
{
digits := 31%positive;
zdigits := 31;
to_Z := phi;
of_pos := positive_to_int31;
head0 := head031;
tail0 := tail031;
zero := 0;
one := 1;
minus_one := Tn;
compare := compare31;
eq0 := fun i => match i ?= 0 with Eq => true | _ => false end;
opp_c := fun i => 0 -c i;
opp := opp31;
opp_carry := fun i => 0-i -1;
succ_c := fun i => i +c 1;
add_c := add31c;
add_carry_c := add31carryc;
succ := fun i => i + 1;
add := add31;
add_carry := fun i j => i + j + 1;
pred_c := fun i => i -c 1;
sub_c := sub31c;
sub_carry_c := sub31carryc;
pred := fun i => i - 1;
sub := sub31;
sub_carry := fun i j => i - j - 1;
mul_c := mul31c;
mul := mul31;
square_c := fun x => x *c x;
div21 := div3121;
div_gt := div31;
div := div31;
modulo_gt := fun i j => let (_,r) := i /j in r;
modulo := fun i j => let (_,r) := i /j in r;
gcd_gt := gcd31;
gcd := gcd31;
add_mul_div := addmuldiv31;
pos_mod :=
  fun p i =>
  match p ?= 31 with
    | Lt => addmuldiv31 p 0 (addmuldiv31 (31-p) i 0)
    | _ => i
  end;
is_even :=
  fun i => let (_,r) := i /2 in
  match r ?= 0 with Eq => true | _ => false end;
sqrt2 := sqrt312;
sqrt := sqrt31;
lor := lor31;
land := land31;
lxor := lxor31
}.

Section Int31_Specs.

Local Open Scope Z_scope.

Notation "[| x |]" := (phi x) (at level 0, x at level 99).

Lemma wB_pos : wB > 0.

Notation "[+| c |]" :=
   (interp_carry 1 wB phi c) (at level 0, c at level 99).

Notation "[-| c |]" :=
   (interp_carry (-1) wB phi c) (at level 0, c at level 99).

Notation "[|| x ||]" :=
   (zn2z_to_Z wB phi x) (at level 0, x at level 99).

Lemma spec_zdigits : [| 31 |] = 31.

Lemma spec_more_than_1_digit: 1 < 31.

Lemma spec_0 : [| 0 |] = 0.

Lemma spec_1 : [| 1 |] = 1.

Lemma spec_m1 : [| Tn |] = wB - 1.

Lemma spec_compare : forall x y,
   (x ?= y)%int31 = ([|x |] ?= [|y |]).

Addition

Lemma spec_add_c : forall x y, [+|add31c x y |] = [|x |] + [|y |].

Lemma spec_succ_c : forall x, [+|add31c x 1|] = [|x |] + 1.

Lemma spec_add_carry_c : forall x y, [+|add31carryc x y |] = [|x |] + [|y |] + 1.

Lemma spec_add : forall x y, [|x +y |] = ([|x |] + [|y |]) mod wB.

Lemma spec_add_carry :
forall x y, [|x +y +1|] = ([|x |] + [|y |] + 1) mod wB.

Lemma spec_succ : forall x, [|x +1|] = ([|x |] + 1) mod wB.

Substraction

Lemma spec_sub_c : forall x y, [-|sub31c x y |] = [|x |] - [|y |].

Lemma spec_sub_carry_c : forall x y, [-|sub31carryc x y |] = [|x |] - [|y |] - 1.

Lemma spec_sub : forall x y, [|x -y |] = ([|x |] - [|y |]) mod wB.

Lemma spec_sub_carry :
forall x y, [|x -y -1|] = ([|x |] - [|y |] - 1) mod wB.

Lemma spec_opp_c : forall x, [-|sub31c 0 x |] = -[|x |].

Lemma spec_opp : forall x, [|0 - x |] = (-[|x |]) mod wB.

Lemma spec_opp_carry : forall x, [|0 - x - 1|] = wB - [|x |] - 1.

Lemma spec_pred_c : forall x, [-|sub31c x 1|] = [|x |] - 1.

Lemma spec_pred : forall x, [|x -1|] = ([|x |] - 1) mod wB.

Multiplication

Lemma phi2_phi_inv2 : forall x, [||phi_inv2 x ||] = x mod (wB ^2).

Lemma spec_mul_c : forall x y, [|| mul31c x y ||] = [|x |] * [|y |].

Lemma spec_mul : forall x y, [|x *y |] = ([|x |] * [|y |]) mod wB.

Lemma spec_square_c : forall x, [|| mul31c x x ||] = [|x |] * [|x |].

Division

Lemma spec_div21 : forall a1 a2 b,
      wB /2 <= [|b |] ->
      [|a1 |] < [|b |] ->
      let (q,r) := div3121 a1 a2 b in
      [|a1 |] *wB + [|a2 |] = [|q |] * [|b |] + [|r |] /\
      0 <= [|r |] < [|b |].

Lemma spec_div : forall a b, 0 < [|b |] ->
      let (q,r) := div31 a b in
      [|a |] = [|q |] * [|b |] + [|r |] /\
      0 <= [|r |] < [|b |].

Lemma spec_mod : forall a b, 0 < [|b |] ->
      [|let (_,r) := (a /b)%int31 in r |] = [|a |] mod [|b |].

Lemma phi_gcd : forall i j,
  [|gcd31 i j |] = Zgcdn (2*size) [|j |] [|i |].

Lemma spec_gcd : forall a b, Zis_gcd [|a |] [|b |] [|gcd31 a b |].

Lemma iter_int31_iter_nat : forall A f i a,
  iter_int31 i A f a = iter_nat (Z.abs_nat [|i |]) A f a.

Fixpoint addmuldiv31_alt n i j :=
  match n with
    | O => i
    | S n => addmuldiv31_alt n (sneakl (firstl j) i) (shiftl j)
  end.

Lemma addmuldiv31_equiv : forall p x y,
  addmuldiv31 p x y = addmuldiv31_alt (Z.abs_nat [|p |]) x y.

Lemma spec_add_mul_div : forall x y p, [|p |] <= Zpos 31 ->
   [| addmuldiv31 p x y |] =
   ([|x |] * (2 ^ [|p |]) + [|y |] / (2 ^ ((Zpos 31) - [|p |]))) mod wB.

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 spec_pos_mod : forall w p,
       [|ZnZ.pos_mod p w |] = [|w |] mod (2 ^ [|p |]).

Shift operations

Lemma spec_head00: forall x, [|x |] = 0 -> [|head031 x |] = Zpos 31.

Fixpoint head031_alt n x :=
  match n with
    | O => 0%nat
    | S n => match firstl x with
               | D0 => S (head031_alt n (shiftl x))
               | D1 => 0%nat
             end
  end.

Lemma head031_equiv :
   forall x, [|head031 x |] = Z.of_nat (head031_alt size x).

Lemma phi_nz : forall x, 0 < [|x |] <-> x <> 0%int31.

Lemma spec_head0 : forall x, 0 < [|x |] ->
         wB / 2 <= 2 ^ ([|head031 x |]) * [|x |] < wB.

Lemma spec_tail00: forall x, [|x |] = 0 -> [|tail031 x |] = Zpos 31.

Fixpoint tail031_alt n x :=
  match n with
    | O => 0%nat
    | S n => match firstr x with
               | D0 => S (tail031_alt n (shiftr x))
               | D1 => 0%nat
             end
  end.

Lemma tail031_equiv :
   forall x, [|tail031 x |] = Z.of_nat (tail031_alt size x).

Lemma spec_tail0 : forall x, 0 < [|x |] ->
         exists y, 0 <= y /\ [|x |] = (2 * y + 1) * (2 ^ [|tail031 x |]).

Lemma quotient_by_2 a: a - 1 <= (a /2) + (a /2).

Lemma sqrt_main_trick j k: 0 <= j -> 0 <= k ->
   (j * k ) + j <= ((j + k )/2 + 1) ^ 2.

Lemma sqrt_main i j: 0 <= i -> 0 < j -> i < ((j + (i /j ))/2 + 1) ^ 2.

Lemma sqrt_init i: 1 < i -> i < (i /2 + 1) ^ 2.

Lemma sqrt_test_true i j: 0 <= i -> 0 < j -> i /j >= j -> j ^ 2 <= i.

Lemma sqrt_test_false i j: 0 <= i -> 0 < j -> i /j < j -> (j + (i /j ))/2 < j.

Lemma sqrt31_step_def rec i j:
   sqrt31_step rec i j =
   match (fst (i /j) ?= j)%int31 with
     Lt => rec i (fst ((j + fst(i /j))/2))%int31
   | _ => j
   end.

Lemma div31_phi i j: 0 < [|j |] -> [|fst (i /j)%int31|] = [|i |]/[|j |].

Lemma sqrt31_step_correct rec i j:
  0 < [|i |] -> 0 < [|j |] -> [|i |] < ([|j |] + 1) ^ 2 ->
   2 * [|j |] < wB ->
  (forall j1 : int31,
    0 < [|j1 |] < [|j |] -> [|i |] < ([|j1 |] + 1) ^ 2 ->
    [|rec i j1 |] ^ 2 <= [|i |] < ([|rec i j1 |] + 1) ^ 2) ->
  [|sqrt31_step rec i j |] ^ 2 <= [|i |] < ([|sqrt31_step rec i j |] + 1) ^ 2.

Lemma iter31_sqrt_correct n rec i j: 0 < [|i |] -> 0 < [|j |] ->
  [|i |] < ([|j |] + 1) ^ 2 -> 2 * [|j |] < 2 ^ (Z.of_nat size ) ->
  (forall j1, 0 < [|j1 |] -> 2^(Z.of_nat n ) + [|j1 |] <= [|j |] ->
      [|i |] < ([|j1 |] + 1) ^ 2 -> 2 * [|j1 |] < 2 ^ (Z.of_nat size ) ->
       [|rec i j1 |] ^ 2 <= [|i |] < ([|rec i j1 |] + 1) ^ 2) ->
  [|iter31_sqrt n rec i j |] ^ 2 <= [|i |] < ([|iter31_sqrt n rec i j |] + 1) ^ 2.

Lemma spec_sqrt : forall x,
       [|sqrt31 x |] ^ 2 <= [|x |] < ([|sqrt31 x |] + 1) ^ 2.

Lemma sqrt312_step_def rec ih il j:
   sqrt312_step rec ih il j =
   match (ih ?= j)%int31 with
      Eq => j
    | Gt => j
    | _ =>
       match (fst (div3121 ih il j) ?= j)%int31 with
         Lt => let m := match j +c fst (div3121 ih il j) with
                       C0 m1 => fst (m1/2)%int31
                     | C1 m1 => (fst (m1/2) + v30)%int31
                     end in rec ih il m
       | _ => j
       end
   end.

Lemma sqrt312_lower_bound ih il j:
   phi2 ih il < ([|j |] + 1) ^ 2 -> [|ih |] <= [|j |].

Lemma div312_phi ih il j: (2^30 <= [|j |] -> [|ih |] < [|j |] ->
  [|fst (div3121 ih il j)|] = phi2 ih il /[|j |])%Z.

Lemma sqrt312_step_correct rec ih il j:
  2 ^ 29 <= [|ih |] -> 0 < [|j |] -> phi2 ih il < ([|j |] + 1) ^ 2 ->
  (forall j1, 0 < [|j1 |] < [|j |] -> phi2 ih il < ([|j1 |] + 1) ^ 2 ->
     [|rec ih il j1 |] ^ 2 <= phi2 ih il < ([|rec ih il j1 |] + 1) ^ 2) ->
  [|sqrt312_step rec ih il j |] ^ 2 <= phi2 ih il
      < ([|sqrt312_step rec ih il j |] + 1) ^ 2.

Lemma iter312_sqrt_correct n rec ih il j:
  2^29 <= [|ih |] -> 0 < [|j |] -> phi2 ih il < ([|j |] + 1) ^ 2 ->
  (forall j1, 0 < [|j1 |] -> 2^(Z.of_nat n ) + [|j1 |] <= [|j |] ->
      phi2 ih il < ([|j1 |] + 1) ^ 2 ->
       [|rec ih il j1 |] ^ 2 <= phi2 ih il < ([|rec ih il j1 |] + 1) ^ 2) ->
  [|iter312_sqrt n rec ih il j |] ^ 2 <= phi2 ih il
      < ([|iter312_sqrt n rec ih il j |] + 1) ^ 2.

Lemma spec_sqrt2 : forall x y,
       wB / 4 <= [|x |] ->
       let (s,r) := sqrt312 x y in
          [||WW x y ||] = [|s |] ^ 2 + [+|r |] /\
          [+|r |] <= 2 * [|s |].

iszero

Lemma spec_eq0 : forall x, ZnZ.eq0 x = true -> [|x |] = 0.

Lemma spec_is_even : forall x,
      if ZnZ.is_even x then [|x |] mod 2 = 0 else [|x |] mod 2 = 1.

Lemma log2_phi_bounded x : Z.log2 [|x |] < Z.of_nat size.

Lemma spec_lor x y : [| ZnZ.lor x y |] = Z.lor [|x |] [|y |].

Lemma spec_land x y : [| ZnZ.land x y |] = Z.land [|x |] [|y |].

Lemma spec_lxor x y : [| ZnZ.lxor x y |] = Z.lxor [|x |] [|y |].

Global Instance int31_specs : ZnZ.Specs int31_ops := {
    spec_to_Z := phi_bounded;
    spec_of_pos := positive_to_int31_spec;
    spec_zdigits := spec_zdigits;
    spec_more_than_1_digit := spec_more_than_1_digit;
    spec_0 := spec_0;
    spec_1 := spec_1;
    spec_m1 := spec_m1;
    spec_compare := spec_compare;
    spec_eq0 := spec_eq0;
    spec_opp_c := spec_opp_c;
    spec_opp := spec_opp;
    spec_opp_carry := spec_opp_carry;
    spec_succ_c := spec_succ_c;
    spec_add_c := spec_add_c;
    spec_add_carry_c := spec_add_carry_c;
    spec_succ := spec_succ;
    spec_add := spec_add;
    spec_add_carry := spec_add_carry;
    spec_pred_c := spec_pred_c;
    spec_sub_c := spec_sub_c;
    spec_sub_carry_c := spec_sub_carry_c;
    spec_pred := spec_pred;
    spec_sub := spec_sub;
    spec_sub_carry := spec_sub_carry;
    spec_mul_c := spec_mul_c;
    spec_mul := spec_mul;
    spec_square_c := spec_square_c;
    spec_div21 := spec_div21;
    spec_div_gt := fun a b _ => spec_div a b;
    spec_div := spec_div;
    spec_modulo_gt := fun a b _ => spec_mod a b;
    spec_modulo := spec_mod;
    spec_gcd_gt := fun a b _ => spec_gcd a b;
    spec_gcd := spec_gcd;
    spec_head00 := spec_head00;
    spec_head0 := spec_head0;
    spec_tail00 := spec_tail00;
    spec_tail0 := spec_tail0;
    spec_add_mul_div := spec_add_mul_div;
    spec_pos_mod := spec_pos_mod;
    spec_is_even := spec_is_even;
    spec_sqrt2 := spec_sqrt2;
    spec_sqrt := spec_sqrt;
    spec_lor := spec_lor;
    spec_land := spec_land;
    spec_lxor := spec_lxor }.

End Int31_Specs.

Module Int31Cyclic <: CyclicType.
  Definition t := int31.
  Definition ops := int31_ops.
  Definition specs := int31_specs.
End Int31Cyclic.