val of_uint (n: pos) (u: uint_t n) : poly
let of_uint (n:pos) (u:uint_t n) : poly =
  reverse (of_seq (to_vec #n u)) (n - 1)
val of_uint (n: pos) (u: uint_t n) : poly
let of_uint (n: pos) (u: uint_t n) : poly =
reverse (of_seq (to_vec #n u)) (n - 1)
Vale.Math.Poly2.Bits_s.fsti.checked
Vale.Math.Poly2_s.fsti.checked Vale.Def.Words_s.fsti.checked Vale.Def.Types_s.fst.checked prims.fst.checked FStar.UInt.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked
Vale.Math.Poly2.Bits_s.fsti
Prims.pos FStar.UInt.uint_t Vale.Math.Poly2_s.reverse Vale.Math.Poly2_s.of_seq FStar.UInt.to_vec Prims.op_Subtraction Vale.Math.Poly2_s.poly
module Vale.Math.Poly2.Bits_s
open FStar.Mul
open Vale.Def.Words_s
open Vale.Def.Types_s
open Vale.Math.Poly2_s
open FStar.Seq
open FStar.UInt

// Bit-level representations of poly, expressed in terms of FStar.UInt.uint_t.
// Least-significant bit represents x^0, next bit represents x^1, etc.
// (Note that FStar.UInt uses 0 for most-significant bit,
// so definitions below use "reverse" to compensate.)

let to_uint (n:pos) (a:poly) : uint_t n =
  from_vec #n (to_seq (reverse a (n - 1)) n)
val of_uint (n: pos) (u: uint_t n) : poly
n: Prims.pos -> u5: FStar.UInt.uint_t n -> Vale.Math.Poly2_s.poly