val two_to_nat_unfold (size: nat) (x: two (natN (pow2 size))) : natN (pow2 (2 * size))
let two_to_nat_unfold (size:nat) (x:two (natN (pow2 size))) : natN (pow2 (2 * size)) =
  let n1 = pow2_norm size in
  let n2 = pow2_norm (2 * size) in
  let Mktwo x0 x1 = x in
  int_to_natN n2 (x0 + x1 * n1)
val two_to_nat_unfold (size: nat) (x: two (natN (pow2 size))) : natN (pow2 (2 * size))
let two_to_nat_unfold (size: nat) (x: two (natN (pow2 size))) : natN (pow2 (2 * size)) =
let n1 = pow2_norm size in
let n2 = pow2_norm (2 * size) in
let Mktwo x0 x1 = x in
int_to_natN n2 (x0 + x1 * n1)
Vale.Def.Words.Two_s.fsti.checked
Vale.Def.Words_s.fsti.checked prims.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked
Vale.Def.Words.Two_s.fsti
Prims.nat Vale.Def.Words_s.two Vale.Def.Words_s.natN Prims.pow2 Vale.Def.Words_s.int_to_natN Prims.op_Addition FStar.Mul.op_Star Prims.pos Vale.Def.Words_s.pow2_norm
module Vale.Def.Words.Two_s
open Vale.Def.Words_s
open FStar.Mul

unfold let two_map (#a #b:Type) (f:a -> b) (x:two a) : two b =
  let Mktwo x0 x1 = x in
  Mktwo (f x0) (f x1)

unfold let two_map2 (#a #b:Type) (f:a -> a -> b) (x y:two a) : two b =
  let Mktwo x0 x1 = x in
  let Mktwo y0 y1 = y in
  Mktwo (f x0 y0) (f x1 y1)

unfold
let nat_to_two_unfold (size:nat) (n:natN (pow2 (2 * size))) : two (natN (pow2 size)) =
  let n1 = pow2_norm size in
  let n2 = pow2_norm (2 * size) in
  Mktwo (n % n1) ((n / n1) % n1)

let nat_to_two (size:nat) (n:natN (pow2 (2 * size))) : two (natN (pow2 size)) =
  nat_to_two_unfold size n
val two_to_nat_unfold (size: nat) (x: two (natN (pow2 size))) : natN (pow2 (2 * size))
size: Prims.nat -> x: Vale.Def.Words_s.two (Vale.Def.Words_s.natN (Prims.pow2 size))
  -> Vale.Def.Words_s.natN (Prims.pow2 (2 * size))