val to_quad32_def (a: poly) : quad32
let to_quad32_def (a:poly) : quad32 =
  let s = to_seq (reverse a 127) 128 in
  Mkfour
    (from_vec #32 (slice s 96 128)) // lo word contains a.[31] .. a.[0]
    (from_vec #32 (slice s 64 96))
    (from_vec #32 (slice s 32 64))
    (from_vec #32 (slice s 0 32))
val to_quad32_def (a: poly) : quad32
let to_quad32_def (a: poly) : quad32 =
let s = to_seq (reverse a 127) 128 in
Mkfour (from_vec #32 (slice s 96 128))
  (from_vec #32 (slice s 64 96))
  (from_vec #32 (slice s 32 64))
  (from_vec #32 (slice s 0 32))
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
Vale.Math.Poly2_s.poly Vale.Def.Words_s.Mkfour Vale.Def.Types_s.nat32 FStar.UInt.from_vec FStar.Seq.Base.slice Prims.bool FStar.Seq.Base.seq Vale.Math.Poly2_s.to_seq Vale.Math.Poly2_s.reverse Vale.Def.Types_s.quad32
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)

let of_uint (n:pos) (u:uint_t n) : poly =
  reverse (of_seq (to_vec #n u)) (n - 1)

let to_double32_def (a:poly) : double32 =
  let s = to_seq (reverse a 63) 64 in
  Mktwo
    (from_vec #32 (slice s 32 64)) // lo word contains a.[31] .. a.[0]
    (from_vec #32 (slice s 0 32)) // hi word contains a.[63] .. a.[32]

let of_double32_def (d:double32) : poly =
  let Mktwo d0 d1 = d in
  let s = (append (
    (to_vec #32 d1))
    (to_vec #32 d0))
    in
  reverse (of_seq s) 63
val to_quad32_def (a: poly) : quad32
a: Vale.Math.Poly2_s.poly -> Vale.Def.Types_s.quad32