val lemma_to_nat (len:nat) (p:poly) (c:nat) : Lemma
  (requires degree p < len /\ normalize (poly_nat_eq_rec len p c len))
  (ensures p == of_nat c)
let lemma_to_nat len p c =
  lemma_bitwise_all ();
  let f (i:int) : Lemma (p.[i] == (of_nat c).[i]) =
    if 0 <= i then lemma_to_nat_rec len p c len i
    in
  FStar.Classical.forall_intro f;
  lemma_equal p (of_nat c)
val lemma_to_nat (len:nat) (p:poly) (c:nat) : Lemma
  (requires degree p < len /\ normalize (poly_nat_eq_rec len p c len))
  (ensures p == of_nat c)
let lemma_to_nat len p c =
lemma_bitwise_all ();
let f (i: int) : Lemma (p.[ i ] == (of_nat c).[ i ]) =
  if 0 <= i then lemma_to_nat_rec len p c len i
in
FStar.Classical.forall_intro f;
lemma_equal p (of_nat c)
Vale.Math.Poly2.Bits.fst.checked
Vale.Arch.TypesNative.fsti.checked prims.fst.checked FStar.UInt.fsti.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.Classical.fsti.checked
Vale.Math.Poly2.Bits.fst
Prims.nat Vale.Math.Poly2_s.poly Vale.Math.Poly2.lemma_equal Vale.Math.Poly2.Bits.of_nat Prims.unit FStar.Classical.forall_intro Prims.int Prims.eq2 Prims.bool Vale.Math.Poly2_s.op_String_Access Prims.l_True Prims.squash Vale.Math.Poly2_s.poly_index Prims.Nil FStar.Pervasives.pattern Prims.op_LessThanOrEqual Vale.Math.Poly2.Bits.lemma_to_nat_rec Vale.Math.Poly2.Lemmas.lemma_bitwise_all
module Vale.Math.Poly2.Bits
open FStar.Mul
open Vale.Arch.TypesNative

let lemma_to_of_uint n u =
  let a = of_uint n u in
  let u' = to_uint n a in
  lemma_index a;
  lemma_reverse_define_all ();
  let s = UInt.to_vec #n u in
  let s' = UInt.to_vec #n u' in
  assert (equal s s');
  ()

let rec of_nat x =
  if x = 0 then zero
  else
    let p = shift (of_nat (x / 2)) 1 in
    if x % 2 = 0 then p else p +. one

let rec lemma_of_to_vec_zero (i:nat) (n:nat) : Lemma
  (requires i < n)
  (ensures index (to_vec #n 0) i == false)
  [SMTPat (index (to_vec #n 0) i)]
  =
  if i + 1 < n then lemma_of_to_vec_zero i (n - 1)

let lemma_of_uint_zero (n:nat) : Lemma
  (ensures of_uint_ n 0 == zero)
  =
  lemma_bitwise_all ();
  lemma_equal (of_uint_ n 0) zero

let rec lemma_of_nat_of_uint n x
  =
  if n > 0 then
  (
    lemma_of_nat_of_uint (n - 1) (x / 2);
    lemma_bitwise_all ();
    lemma_equal (of_nat x) (of_uint n x)
  )

let rec lemma_to_nat_rec (len:nat) (p:poly) (c:nat) (n:nat) (i:nat) : Lemma
  (requires degree p < len /\ normalize (poly_nat_eq_rec len p c n))
  (ensures p.[len - n + i] == (of_nat c).[i])
  =
  lemma_bitwise_all ();
  if (i > 0 && n > 0) then lemma_to_nat_rec len p (c / 2) (n - 1) (i - 1)
val lemma_to_nat (len:nat) (p:poly) (c:nat) : Lemma
  (requires degree p < len /\ normalize (poly_nat_eq_rec len p c len))
  (ensures p == of_nat c)
len: Prims.nat -> p: Vale.Math.Poly2_s.poly -> c: Prims.nat
  -> FStar.Pervasives.Lemma
      (requires
        Vale.Math.Poly2_s.degree p < len /\
        FStar.Pervasives.normalize (Vale.Math.Poly2.Bits.poly_nat_eq_rec len p c len))
      (ensures p == Vale.Math.Poly2.Bits.of_nat c)