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 BigNumPrelude.
Require Import CyclicAxioms.
Require Import ROmega.

Local Open Scope nat_scope.
Local Open Scope int31_scope.

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 n x := iter_nat n _ shiftr x.

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

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

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

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

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

Iterated shift to the left


 Definition nshiftl n x := iter_nat n _ shiftl x.

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

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

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

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

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

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

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

More advanced results about nshiftr

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

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

 Lemma nshiftr_0_firstl : forall n x, n < size ->
  nshiftr n x = 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 (size - n) x) =
  recr_aux p A case0 caserec (nshiftr (size - n) x).

 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 (size-n) x) < 2 ^ (Z.of_nat n))%Z.

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

 Lemma phibis_aux_lowerbound :
  forall n x, firstr (nshiftr n x) = 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 n x = nshiftl n y.

 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 n x) = 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 to prove 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 (size-n) x)) =
   nshiftr (size-n) x.

 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 n (snd (p2ibis n p)) = 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
}.

Section Int31_Specs.

 Local Open Scope Z_scope.

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

 Local Notation wB := (2 ^ (Z.of_nat size)).

 Lemma wB_pos : wB > 0.

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

 Notation "[-| c |]" :=
   (interp_carry (-1) wB phi c) (at level 0, x 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 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.

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

End Int31_Specs.

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