Library Coq.Numbers.Cyclic.Int63.Uint63


Require Import Utf8.
Require Export DoubleType.
Require Import Lia.
Require Import Zpow_facts.
Require Import Zgcd_alt.
Require ZArith.
Import Znumtheory.
Require Export PrimInt63.

Definition size := 63%nat.

Notation int := int (only parsing).
Notation lsl := lsl (only parsing).
Notation lsr := lsr (only parsing).
Notation land := land (only parsing).
Notation lor := lor (only parsing).
Notation lxor := lxor (only parsing).
Notation add := add (only parsing).
Notation sub := sub (only parsing).
Notation mul := mul (only parsing).
Notation mulc := mulc (only parsing).
Notation div := div (only parsing).
Notation mod := mod (only parsing).
Notation eqb := eqb (only parsing).
Notation ltb := ltb (only parsing).
Notation leb := leb (only parsing).

Local Open Scope uint63_scope.

Module Import Uint63NotationsInternalB.
Infix "<<" := lsl (at level 30, no associativity) : uint63_scope.
Infix ">>" := lsr (at level 30, no associativity) : uint63_scope.
Infix "land" := land (at level 40, left associativity) : uint63_scope.
Infix "lor" := lor (at level 40, left associativity) : uint63_scope.
Infix "lxor" := lxor (at level 40, left associativity) : uint63_scope.
Infix "+" := add : uint63_scope.
Infix "-" := sub : uint63_scope.
Infix "*" := mul : uint63_scope.
Infix "/" := div : uint63_scope.
Infix "mod" := mod (at level 40, no associativity) : uint63_scope.
Infix "=?" := eqb (at level 70, no associativity) : uint63_scope.
Infix "<?" := ltb (at level 70, no associativity) : uint63_scope.
Infix "<=?" := leb (at level 70, no associativity) : uint63_scope.
Infix "≤?" := leb (at level 70, no associativity) : uint63_scope.
End Uint63NotationsInternalB.

The number of digits as a int
Definition digits := 63.

The bigger int
Definition max_int := Eval vm_compute in 0 - 1.
Register Inline max_int.

Access to the nth digits
Definition get_digit x p := (0 <? (x land (1 << p))).

Definition set_digit x p (b:bool) :=
  if if 0 <=? p then p <? digits else false then
    if b then x lor (1 << p)
    else x land (max_int lxor (1 << p))
  else x.

Equality to 0
Definition is_zero (i:int) := i =? 0.
Register Inline is_zero.

Parity
Definition is_even (i:int) := is_zero (i land 1).
Register Inline is_even.

Bit

Definition bit i n := negb (is_zero ((i >> n) << (digits - 1))).

Extra modulo operations
Definition opp (i:int) := 0 - i.
Register Inline opp.

Definition oppcarry i := max_int - i.
Register Inline oppcarry.

Definition succ i := i + 1.
Register Inline succ.

Definition pred i := i - 1.
Register Inline pred.

Definition addcarry i j := i + j + 1.
Register Inline addcarry.

Definition subcarry i j := i - j - 1.
Register Inline subcarry.

Exact arithmetic operations

Definition addc_def x y :=
  let r := x + y in
  if r <? x then C1 r else C0 r.
Notation addc := addc (only parsing).

Definition addcarryc_def x y :=
  let r := addcarry x y in
  if r <=? x then C1 r else C0 r.
Notation addcarryc := addcarryc (only parsing).

Definition subc_def x y :=
  if y <=? x then C0 (x - y) else C1 (x - y).
Notation subc := subc (only parsing).

Definition subcarryc_def x y :=
  if y <? x then C0 (x - y - 1) else C1 (x - y - 1).
Notation subcarryc := subcarryc (only parsing).

Definition diveucl_def x y := (x/y, x mod y).
Notation diveucl := diveucl (only parsing).

Notation diveucl_21 := diveucl_21 (only parsing).

Definition addmuldiv_def p x y :=
  (x << p) lor (y >> (digits - p)).
Notation addmuldiv := addmuldiv (only parsing).

Module Import Uint63NotationsInternalC.
Notation "- x" := (opp x) : uint63_scope.
Notation "n '+c' m" := (addc n m) (at level 50, no associativity) : uint63_scope.
Notation "n '-c' m" := (subc n m) (at level 50, no associativity) : uint63_scope.
End Uint63NotationsInternalC.

Definition oppc (i:int) := 0 -c i.
Register Inline oppc.

Definition succc i := i +c 1.
Register Inline succc.

Definition predc i := i -c 1.
Register Inline predc.

Comparison
Definition compare_def x y :=
  if x <? y then Lt
  else if (x =? y) then Eq else Gt.

Notation compare := compare (only parsing).

Import Bool ZArith.
Translation to Z
Fixpoint to_Z_rec (n:nat) (i:int) :=
  match n with
  | O => 0%Z
  | S n =>
    (if is_even i then Z.double else Zdouble_plus_one) (to_Z_rec n (i >> 1))
  end.

Definition to_Z := to_Z_rec size.

Fixpoint of_pos_rec (n:nat) (p:positive) :=
  match n, p with
  | O, _ => 0
  | S n, xH => 1
  | S n, xO p => (of_pos_rec n p) << 1
  | S n, xI p => (of_pos_rec n p) << 1 lor 1
  end.

Definition of_pos := of_pos_rec size.

Definition of_Z z :=
  match z with
  | Zpos p => of_pos p
  | Z0 => 0
  | Zneg p => - (of_pos p)
  end.

Definition wB := (2 ^ (Z.of_nat size))%Z.

Module Import Uint63NotationsInternalD.
Notation "n ?= m" := (compare n m) (at level 70, no associativity) : uint63_scope.
Notation "'φ' x" := (to_Z x) (at level 0) : uint63_scope.
Notation "'Φ' x" :=
   (zn2z_to_Z wB to_Z x) (at level 0) : uint63_scope.
End Uint63NotationsInternalD.

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

Corollary to_Z_bounded : forall x, (0 <= φ x < wB)%Z.

Local Open Scope Z_scope.

Theorem Zmod_distr: forall a b r t, 0 <= a <= b -> 0 <= r -> 0 <= t < 2 ^a ->
  (2 ^a * r + t) mod (2 ^ b) = (2 ^a * r) mod (2 ^ b) + t.

Lemma pow2_pos n : 0 <= n 2 ^ n > 0.

Lemma pow2_nz n : 0 <= n 2 ^ n 0.

#[global]
Hint Resolve pow2_pos pow2_nz : zarith.


Trivial lemmas without axiom

Lemma wB_diff_0 : wB <> 0.

Lemma wB_pos : 0 < wB.

Lemma to_Z_0 : φ 0 = 0.

Lemma to_Z_1 : φ 1 = 1.

Local Open Scope Z_scope.

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

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


Axiom of_to_Z : forall x, of_Z φ x = x.

Lemma can_inj {rT aT} {f: aT -> rT} {g: rT -> aT} (K: forall a, g (f a) = a) {a a'} (e: f a = f a') : a = a'.

Lemma to_Z_inj x y : φ x = φ y x = y.

Specification of logical operations
Local Open Scope Z_scope.
Axiom lsl_spec : forall x p, φ (x << p) = φ x * 2 ^ φ p mod wB.

Axiom lsr_spec : forall x p, φ (x >> p) = φ x / 2 ^ φ p.

Axiom land_spec: forall x y i , bit (x land y) i = bit x i && bit y i.

Axiom lor_spec: forall x y i, bit (x lor y) i = bit x i || bit y i.

Axiom lxor_spec: forall x y i, bit (x lxor y) i = xorb (bit x i) (bit y i).

Specification of basic opetations



Axiom add_spec : forall x y, φ (x + y) = (φ x + φ y) mod wB.

Axiom sub_spec : forall x y, φ (x - y) = (φ x - φ y) mod wB.

Axiom mul_spec : forall x y, φ (x * y) = φ x * φ y mod wB.

Axiom mulc_spec : forall x y, φ x * φ y = φ (fst (mulc x y)) * wB + φ (snd (mulc x y)).

Axiom div_spec : forall x y, φ (x / y) = φ x / φ y.

Axiom mod_spec : forall x y, φ (x mod y) = φ x mod φ y.

Axiom eqb_correct : forall i j, (i =? j)%uint63 = true -> i = j.

Axiom eqb_refl : forall x, (x =? x)%uint63 = true.

Axiom ltb_spec : forall x y, (x <? y)%uint63 = true <-> φ x < φ y.

Axiom leb_spec : forall x y, (x <=? y)%uint63 = true <-> φ x <= φ y.

Exotic operations
I should add the definition (like for compare)
Notation head0 := head0 (only parsing).
Notation tail0 := tail0 (only parsing).

Axioms on operations which are just short cut

Axiom compare_def_spec : forall x y, compare x y = compare_def x y.

Axiom head0_spec : forall x, 0 < φ x ->
         wB/ 2 <= 2 ^ (φ (head0 x)) * φ x < wB.

Axiom tail0_spec : forall x, 0 < φ x ->
         (exists y, 0 <= y /\ φ x = (2 * y + 1) * (2 ^ φ (tail0 x)))%Z.

Axiom addc_def_spec : forall x y, (x +c y)%uint63 = addc_def x y.

Axiom addcarryc_def_spec : forall x y, addcarryc x y = addcarryc_def x y.

Axiom subc_def_spec : forall x y, (x -c y)%uint63 = subc_def x y.

Axiom subcarryc_def_spec : forall x y, subcarryc x y = subcarryc_def x y.

Axiom diveucl_def_spec : forall x y, diveucl x y = diveucl_def x y.

Axiom diveucl_21_spec : forall a1 a2 b,
   let (q,r) := diveucl_21 a1 a2 b in
   let (q',r') := Z.div_eucl (φ a1 * wB + φ a2) φ b in
   φ a1 < φ b -> φ q = q' /\ φ r = r'.

Axiom addmuldiv_def_spec : forall p x y,
  addmuldiv p x y = addmuldiv_def p x y.

Square root functions using newton iteration
Local Open Scope uint63_scope.

Definition sqrt_step (rec: int -> int -> int) (i j: int) :=
  let quo := i / j in
  if quo <? j then rec i ((j + quo) >> 1)
  else j.

Definition iter_sqrt :=
 Eval lazy beta delta [sqrt_step] in
 fix iter_sqrt (n: nat) (rec: int -> int -> int)
          (i j: int) {struct n} : int :=
  sqrt_step
   (fun i j => match n with
      O => rec i j
   | S n => (iter_sqrt n (iter_sqrt n rec)) i j
   end) i j.

Definition sqrt i :=
  match compare 1 i with
    Gt => 0
  | Eq => 1
  | Lt => iter_sqrt size (fun i j => j) i (i >> 1)
  end.

Definition high_bit := 1 << (digits - 1).

Definition sqrt2_step (rec: int -> int -> int -> int)
   (ih il j: int) :=
  if ih <? j then
    let (quo,_) := diveucl_21 ih il j in
    if quo <? j then
      match j +c quo with
      | C0 m1 => rec ih il (m1 >> 1)
      | C1 m1 => rec ih il ((m1 >> 1) + high_bit)
      end
    else j
  else j.

Definition iter2_sqrt :=
 Eval lazy beta delta [sqrt2_step] in
 fix iter2_sqrt (n: nat)
          (rec: int -> int -> int -> int)
          (ih il j: int) {struct n} : int :=
  sqrt2_step
   (fun ih il j =>
     match n with
     | O => rec ih il j
     | S n => (iter2_sqrt n (iter2_sqrt n rec)) ih il j
   end) ih il j.

Definition sqrt2 ih il :=
  let s := iter2_sqrt size (fun ih il j => j) ih il max_int in
  let (ih1, il1) := mulc s s in
  match il -c il1 with
  | C0 il2 =>
    if ih1 <? ih then (s, C1 il2) else (s, C0 il2)
  | C1 il2 =>
    if ih1 <? (ih - 1) then (s, C1 il2) else (s, C0 il2)
  end.

Gcd
Fixpoint gcd_rec (guard:nat) (i j:int) {struct guard} :=
   match guard with
   | O => 1
   | S p => if j =? 0 then i else gcd_rec p j (i mod j)
   end.

Definition gcd := gcd_rec (2*size).

equality
Lemma eqb_complete : forall x y, x = y -> (x =? y) = true.

Lemma eqb_spec : forall x y, (x =? y) = true <-> x = y.

Lemma eqb_false_spec : forall x y, (x =? y) = false <-> x <> y.

Lemma eqb_false_complete : forall x y, x <> y -> (x =? y) = false.

Lemma eqb_false_correct : forall x y, (x =? y) = false -> x <> y.

Definition eqs (i j : int) : {i = j} + { i <> j } :=
  (if i =? j as b return ((b = true -> i = j) -> (b = false -> i <> j) -> {i=j} + {i <> j} )
    then fun (Heq : true = true -> i = j) _ => left _ (Heq (eq_refl true))
    else fun _ (Hdiff : false = false -> i <> j) => right _ (Hdiff (eq_refl false)))
  (eqb_correct i j)
  (eqb_false_correct i j).

Lemma eq_dec : forall i j:int, i = j \/ i <> j.


Definition cast i j :=
     (if i =? j as b return ((b = true -> i = j) -> option (forall P : int -> Type, P i -> P j))
      then fun Heq : true = true -> i = j =>
             Some
             (fun (P : int -> Type) (Hi : P i) =>
               match Heq (eq_refl true) in (_ = y) return (P y) with
               | eq_refl => Hi
               end)
      else fun _ : false = true -> i = j => None) (eqb_correct i j).

Lemma cast_refl : forall i, cast i i = Some (fun P H => H).

Lemma cast_diff : forall i j, i =? j = false -> cast i j = None.

Definition eqo i j :=
   (if i =? j as b return ((b = true -> i = j) -> option (i=j))
    then fun Heq : true = true -> i = j =>
             Some (Heq (eq_refl true))
     else fun _ : false = true -> i = j => None) (eqb_correct i j).

Lemma eqo_refl : forall i, eqo i i = Some (eq_refl i).

Lemma eqo_diff : forall i j, i =? j = false -> eqo i j = None.

Comparison

Lemma eqbP x y : reflect (φ x = φ y ) (x =? y).

Lemma ltbP x y : reflect (φ x < φ y )%Z (x <? y).

Lemma lebP x y : reflect (φ x <= φ y )%Z (x ≤? y).

Lemma compare_spec x y : compare x y = (φ x ?= φ y)%Z.

Lemma is_zero_spec x : is_zero x = true <-> x = 0%uint63.

Lemma diveucl_spec x y :
  let (q,r) := diveucl x y in
  (φ q , φ r ) = Z.div_eucl φ x φ y .

Local Open Scope Z_scope.
Addition
Lemma addc_spec x y : [+| x +c y |] = φ x + φ y .

Lemma succ_spec x : φ (succ x) = (φ x + 1) mod wB.

Lemma succc_spec x : [+| succc x |] = φ x + 1.

Lemma addcarry_spec x y : φ (addcarry x y) = (φ x + φ y + 1) mod wB.

Lemma addcarryc_spec x y : [+| addcarryc x y |] = φ x + φ y + 1.

Subtraction
Lemma subc_spec x y : [-| x -c y |] = φ x - φ y .

Lemma pred_spec x : φ (pred x) = (φ x - 1) mod wB.

Lemma predc_spec x : [-| predc x |] = φ x - 1.

Lemma oppc_spec x : [-| oppc x |] = - φ x .

Lemma opp_spec x : φ (- x) = - φ x mod wB.

Lemma oppcarry_spec x : φ (oppcarry x) = wB - φ x - 1.

Lemma subcarry_spec x y : φ (subcarry x y) = (φ x - φ y - 1) mod wB.

Lemma subcarryc_spec x y : [-| subcarryc x y |] = φ x - φ y - 1.

GCD
Lemma to_Z_gcd : forall i j, φ (gcd i j) = Zgcdn (2 * size) (φ j) (φ i).

Lemma gcd_spec a b : Zis_gcd (φ a) (φ b) (φ (gcd a b)).

Head0, Tail0
Lemma head00_spec x : φ x = 0 -> φ (head0 x) = φ digits .

Lemma tail00_spec x : φ x = 0 -> φ (tail0 x) = φ digits.

Infix "≡" := (eqm wB) (at level 70, no associativity) : uint63_scope.

Lemma eqm_mod x y : x mod wB y mod wB x y.

Lemma eqm_sub x y : x y x - y 0.

Lemma eqmE x y : x y k, x - y = k * wB.

Lemma eqm_subE x y : x y x - y 0.

Lemma int_eqm x y : x = y φ x φ y.

Lemma eqmI x y : φ x φ y x = y.

Lemma add_assoc x y z: (x + (y + z) = (x + y) + z)%uint63.

Lemma add_comm x y: (x + y = y + x)%uint63.

Lemma add_le_r m n:
  if (n <=? m + n)%uint63 then (φ m + φ n < wB)%Z else (wB <= φ m + φ n)%Z.

Lemma add_cancel_l x y z : (x + y = x + z)%uint63 -> y = z.

Lemma add_cancel_r x y z : (y + x = z + x)%uint63 -> y = z.

Coercion b2i (b: bool) : int := if b then 1%uint63 else 0%uint63.

Lemma lsr0 i : 0 >> i = 0%uint63.

Lemma lsr_0_r i: i >> 0 = i.

Lemma lsr_1 n : 1 >> n = (n =? 0)%uint63.

Lemma lsr_add i m n: ((i >> m) >> n = if n <=? m + n then i >> (m + n) else 0)%uint63.

Lemma lsl0 i: 0 << i = 0%uint63.

Lemma lsl0_r i : i << 0 = i.

Lemma lsl_add_distr x y n: (x + y) << n = ((x << n) + (y << n))%uint63.

Lemma lsr_M_r x i (H: (digits <=? i = true)%uint63) : x >> i = 0%uint63.

Lemma bit_0_spec i: φ (bit i 0) = φ i mod 2.

Lemma bit_split i : ( i = (i >> 1 ) << 1 + bit i 0)%uint63.

Lemma bit_lsr x i j :
 (bit (x >> i) j = if j <=? i + j then bit x (i + j) else false)%uint63.

Lemma bit_b2i (b: bool) i : bit b i = (i =? 0)%uint63 && b.

Lemma bit_1 n : bit 1 n = (n =? 0)%uint63.

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

Lemma to_Z_split x : φ x = φ (x >> 1) * 2 + φ (bit x 0).

Lemma bit_M i n (H: (digits <=? n = true)%uint63): bit i n = false.

Lemma bit_half i n (H: (n <? digits = true)%uint63) : bit (i>>1) n = bit i (n+1).

Lemma bit_ext i j : (forall n, bit i n = bit j n) -> i = j.

Lemma bit_lsl x i j : bit (x << i) j =
                        (if (j <? i) || (digits <=? j) then false else bit x (j - i))%uint63.

Lemma lor_lsr i1 i2 i: (i1 lor i2) >> i = (i1 >> i) lor (i2 >> i).

Lemma lor_le x y : (y <=? x lor y)%uint63 = true.

Lemma bit_0 n : bit 0 n = false.

Lemma bit_add_or x y:
  (forall n, bit x n = true -> bit y n = true -> False) <-> (x + y)%uint63= x lor y.

Lemma addmuldiv_spec x y p :
  φ p <= φ digits ->
  φ (addmuldiv p x y) = (φ x * (2 ^ φ p) + φ y / (2 ^ (φ digits - φ p))) mod wB.

Lemma is_even_bit i : is_even i = negb (bit i 0).

Lemma is_even_spec x : if is_even x then φ x mod 2 = 0 else φ x mod 2 = 1.

Lemma is_even_0 : is_even 0 = true.

Lemma is_even_lsl_1 i : is_even (i << 1) = true.



Ltac elim_div :=
  unfold Z.div, Z.modulo;
  match goal with
  | H : context[ Z.div_eucl ?X ?Y ] |- _ =>
     generalize dependent H; generalize (Z_div_mod_full X Y) ; case (Z.div_eucl X Y)
  | |- context[ Z.div_eucl ?X ?Y ] =>
     generalize (Z_div_mod_full X Y) ; case (Z.div_eucl X Y)
  end; unfold Remainder.

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_test_false i j: 0 <= i -> 0 < j -> i/j < j -> (j + (i/j))/2 < j.

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

Lemma sqrt_step_correct rec i j:
  0 < φ i -> 0 < φ j -> φ i < (φ j + 1) ^ 2 ->
   2 * φ j < wB ->
  (forall j1 : int,
    0 < φ j1 < φ j -> φ i < (φ j1 + 1) ^ 2 ->
    φ (rec i j1) ^ 2 <= φ i < (φ (rec i j1) + 1) ^ 2) ->
  φ (sqrt_step rec i j) ^ 2 <= φ i < (φ (sqrt_step rec i j) + 1) ^ 2.

Lemma iter_sqrt_correct n rec i j: 0 < φ i -> 0 < φ j ->
  φ i < (φ j + 1) ^ 2 -> 2 * φ j < wB ->
  (forall j1, 0 < φ j1 -> 2^(Z_of_nat n) + φ j1 <= φ j ->
      φ i < (φ j1 + 1) ^ 2 -> 2 * φ j1 < wB ->
       φ (rec i j1) ^ 2 <= φ i < (φ (rec i j1) + 1) ^ 2) ->
  φ (iter_sqrt n rec i j) ^ 2 <= φ i < (φ (iter_sqrt n rec i j) + 1) ^ 2.

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

Lemma sqrt_spec : forall x,
       φ (sqrt x) ^ 2 <= φ x < (φ (sqrt x) + 1) ^ 2.

Lemma sqrt2_step_def rec ih il j:
   sqrt2_step rec ih il j =
   if (ih <? j)%uint63 then
    let quo := fst (diveucl_21 ih il j) in
    if (quo <? j)%uint63 then
     let m :=
      match j +c quo with
      | C0 m1 => m1 >> 1
      | C1 m1 => (m1 >> 1 + 1 << (digits -1))%uint63
      end in
     rec ih il m
    else j
   else j.

Lemma sqrt2_lower_bound ih il j:
   Φ (WW ih il) < (φ j + 1) ^ 2 -> φ ih <= φ j.

Lemma diveucl_21_spec_aux : forall a1 a2 b,
      wB/2 <= φ b ->
      φ a1 < φ b ->
      let (q,r) := diveucl_21 a1 a2 b in
      φ a1 *wB+ φ a2 = φ q * φ b + φ r /\
      0 <= φ r < φ b.

Lemma div2_phi ih il j: (2^62 <= φ j -> φ ih < φ j ->
  φ (fst (diveucl_21 ih il j)) = Φ (WW ih il) / φ j)%Z.

Lemma sqrt2_step_correct rec ih il j:
  2 ^ (Z_of_nat (size - 2)) <= φ ih ->
  0 < φ j -> Φ (WW ih il) < (φ j + 1) ^ 2 ->
  (forall j1, 0 < φ j1 < φ j -> Φ (WW ih il) < (φ j1 + 1) ^ 2 ->
     φ (rec ih il j1) ^ 2 <= Φ (WW ih il) < (φ (rec ih il j1) + 1) ^ 2) ->
  φ (sqrt2_step rec ih il j) ^ 2 <= Φ (WW ih il)
      < (φ (sqrt2_step rec ih il j) + 1) ^ 2.

Lemma iter2_sqrt_correct n rec ih il j:
  2^(Z_of_nat (size - 2)) <= φ ih -> 0 < φ j -> Φ (WW ih il) < (φ j + 1) ^ 2 ->
  (forall j1, 0 < φ j1 -> 2^(Z_of_nat n) + φ j1 <= φ j ->
      Φ (WW ih il) < (φ j1 + 1) ^ 2 ->
       φ (rec ih il j1) ^ 2 <= Φ (WW ih il) < (φ (rec ih il j1) + 1) ^ 2) ->
  φ (iter2_sqrt n rec ih il j) ^ 2 <= Φ (WW ih il)
      < (φ (iter2_sqrt n rec ih il j) + 1) ^ 2.

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

Lemma of_pos_rec_spec (k: nat) :
  (k <= size)%nat
   p, φ(of_pos_rec k p) = Zpos p mod 2 ^ Z.of_nat k.

Lemma is_int n :
  0 <= n < 2 ^ φ digits
  n = φ (of_Z n).

Lemma of_Z_spec n : φ (of_Z n) = n mod wB.

Lemma Z_oddE a : Z.odd a = (a mod 2 =? 1)%Z.

Lemma Z_evenE a : Z.even a = (a mod 2 =? 0)%Z.

Lemma is_zeroE n : is_zero n = Z.eqb (φ n) 0.

Lemma bitE i j : bit i j = Z.testbit φ(i) φ(j).

Lemma lt_pow_lt_log d k n :
  0 < d <= n
  0 <= k < 2 ^ d
  Z.log2 k < n.

Lemma land_spec' x y : φ (x land y) = Z.land φ(x) φ(y).

Lemma lor_spec' x y : φ (x lor y) = Z.lor φ(x) φ(y).

Lemma lxor_spec' x y : φ (x lxor y) = Z.lxor φ(x) φ(y).

Lemma landC i j : i land j = j land i.

Lemma landA i j k : i land (j land k) = i land j land k.

Lemma land0 i : 0 land i = 0%uint63.

Lemma land0_r i : i land 0 = 0%uint63.

Lemma lorC i j : i lor j = j lor i.

Lemma lorA i j k : i lor (j lor k) = i lor j lor k.

Lemma lor0 i : 0 lor i = i.

Lemma lor0_r i : i lor 0 = i.

Lemma lxorC i j : i lxor j = j lxor i.

Lemma lxorA i j k : i lxor (j lxor k) = i lxor j lxor k.

Lemma lxor0 i : 0 lxor i = i.

Lemma lxor0_r i : i lxor 0 = i.

Lemma opp_to_Z_opp (x : int) :
    φ x mod wB <> 0 ->
  (- φ (- x)) mod wB = (φ x) mod wB.

Module Export Uint63Notations.
  Local Open Scope uint63_scope.
  Export Uint63NotationsInternalB.
  Export Uint63NotationsInternalC.
  Export Uint63NotationsInternalD.
End Uint63Notations.