val four_to_nat (size: nat) (x: four (natN (pow2 size))) : natN (pow2 (4 * size))
let four_to_nat (size:nat) (x:four (natN (pow2 size))) : natN (pow2 (4 * size)) =
  four_to_nat_unfold size x
val four_to_nat (size: nat) (x: four (natN (pow2 size))) : natN (pow2 (4 * size))
let four_to_nat (size: nat) (x: four (natN (pow2 size))) : natN (pow2 (4 * size)) =
four_to_nat_unfold size x
Vale.Def.Words.Four_s.fsti.checked
Vale.Def.Words_s.fsti.checked prims.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked
Vale.Def.Words.Four_s.fsti
Prims.nat Vale.Def.Words_s.four Vale.Def.Words_s.natN Prims.pow2 Vale.Def.Words.Four_s.four_to_nat_unfold FStar.Mul.op_Star
module Vale.Def.Words.Four_s
open Vale.Def.Words_s
open FStar.Mul

unfold let four_map (#a #b:Type) (f:a -> b) (x:four a) : four b =
  let Mkfour x0 x1 x2 x3 = x in
  Mkfour (f x0) (f x1) (f x2) (f x3)

unfold let four_map2 (#a #b:Type) (f:a -> a -> b) (x y:four a) : four b =
  let Mkfour x0 x1 x2 x3 = x in
  let Mkfour y0 y1 y2 y3 = y in
  Mkfour (f x0 y0) (f x1 y1) (f x2 y2) (f x3 y3)

let two_two_to_four (#a:Type) (x:two (two a)) : four a =
  let (Mktwo (Mktwo x0 x1) (Mktwo x2 x3)) = x in
  Mkfour x0 x1 x2 x3

let four_to_two_two (#a:Type) (x:four a) : two (two a) =
  let Mkfour x0 x1 x2 x3 = x in
  Mktwo (Mktwo x0 x1) (Mktwo x2 x3)

unfold
let nat_to_four_unfold (size:nat) (n:natN (pow2 (4 * size))) : four (natN (pow2 size)) =
  let n1 = pow2_norm size in
  let n2 = pow2_norm (2 * size) in
  let n3 = pow2_norm (3 * size) in
  let n4 = pow2_norm (4 * size) in
  Mkfour (n % n1) ((n / n1) % n1) ((n / n2) % n1) ((n / n3) % n1)

[@"opaque_to_smt"]
let nat_to_four (size:nat) (n:natN (pow2 (4 * size))) : four (natN (pow2 size)) =
  nat_to_four_unfold size n

unfold
let four_to_nat_unfold (size:nat) (x:four (natN (pow2 size))) : natN (pow2 (4 * size)) =
  let n1 = pow2_norm size in
  let n2 = pow2_norm (2 * size) in
  let n3 = pow2_norm (3 * size) in
  let n4 = pow2_norm (4 * size) in
  let Mkfour x0 x1 x2 x3 = x in
  int_to_natN n4 (x0 + x1 * n1 + x2 * n2 + x3 * n3)

[@"opaque_to_smt"]
val four_to_nat (size: nat) (x: four (natN (pow2 size))) : natN (pow2 (4 * size))
size: Prims.nat -> x: Vale.Def.Words_s.four (Vale.Def.Words_s.natN (Prims.pow2 size))
  -> Vale.Def.Words_s.natN (Prims.pow2 (4 * size))