val seq_to_seq_four_LE (#a: Type) (x: seq a {length x % 4 == 0})
    : (z: seq (four a) {length z == length x / 4})
let seq_to_seq_four_LE (#a:Type) (x:seq a{length x % 4 == 0}) : (z:seq (four a){length z == length x / 4}) =
  let f (n:nat{n < length x / 4}) = Mkfour
    (index x (n * 4)) (index x (n * 4 + 1)) (index x (n * 4 + 2)) (index x (n * 4 + 3))
    in
  init (length x / 4) f
val seq_to_seq_four_LE (#a: Type) (x: seq a {length x % 4 == 0})
    : (z: seq (four a) {length z == length x / 4})
let seq_to_seq_four_LE (#a: Type) (x: seq a {length x % 4 == 0})
    : (z: seq (four a) {length z == length x / 4}) =
let f (n: nat{n < length x / 4}) =
  Mkfour (index x (n * 4)) (index x (n * 4 + 1)) (index x (n * 4 + 2)) (index x (n * 4 + 3))
in
init (length x / 4) f
Vale.Def.Words.Seq_s.fsti.checked
Vale.Lib.Seqs_s.fst.checked Vale.Def.Words_s.fsti.checked Vale.Def.Words.Two_s.fsti.checked Vale.Def.Words.Four_s.fsti.checked prims.fst.checked FStar.UInt8.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked
Vale.Def.Words.Seq_s.fsti
FStar.Seq.Base.seq Prims.eq2 Prims.int Prims.op_Modulus FStar.Seq.Base.length FStar.Seq.Base.init Vale.Def.Words_s.four Prims.op_Division Prims.nat Prims.b2t Prims.op_LessThan Vale.Def.Words_s.Mkfour FStar.Seq.Base.index FStar.Mul.op_Star Prims.op_Addition
module Vale.Def.Words.Seq_s
open Vale.Def.Words_s
open Vale.Def.Words.Two_s
open Vale.Def.Words.Four_s
open FStar.Seq
open FStar.Mul
open Vale.Lib.Seqs_s

let seqn (n:nat) (a:Type) : Type = s:seq a{length s == n}
let seq2 (a:Type) = seqn 2 a
let seq4 (a:Type) = seqn 4 a
let seq8 (a:Type) = seqn 8 a
let seq16 (a:Type) = seqn 16 a

let seq_to_two_LE (#a:Type) (s:seq2 a) : two a =
  Mktwo (index s 0) (index s 1)

let seq_to_two_BE (#a:Type) (s:seq2 a) : two a =
  Mktwo (index s 1) (index s 0)

let seq_to_four_LE (#a:Type) (s:seq4 a) : four a =
  Mkfour (index s 0) (index s 1) (index s 2) (index s 3)

let seq_to_four_BE (#a:Type) (s:seq4 a) : four a =
  Mkfour (index s 3) (index s 2) (index s 1) (index s 0)

val two_to_seq_LE (#a:Type) (x:two a) : Pure (seq2 a)
  (requires True)
  (ensures fun s ->
    index s 0 == x.lo /\
    index s 1 == x.hi
  )

val two_to_seq_BE (#a:Type) (x:two a) : Pure (seq2 a)
  (requires True)
  (ensures fun s ->
    index s 1 == x.lo /\
    index s 0 == x.hi
  )

val four_to_seq_LE (#a:Type) (x:four a) : Pure (seq4 a)
  (requires True)
  (ensures fun s ->
    index s 0 == x.lo0 /\
    index s 1 == x.lo1 /\
    index s 2 == x.hi2 /\
    index s 3 == x.hi3
  )

val four_to_seq_BE (#a:Type) (x:four a) : Pure (seq4 a)
  (requires True)
  (ensures fun s ->
    index s 3 == x.lo0 /\
    index s 2 == x.lo1 /\
    index s 1 == x.hi2 /\
    index s 0 == x.hi3
  )

[@"opaque_to_smt"]
let seq_two_to_seq_LE (#a:Type) (x:seq (two a)) : (z:seq a{length z == length x * 2}) =
  let f (n:nat{n < length x * 2}) = two_select (index x (n / 2)) (n % 2) in
  init (length x * 2) f

[@"opaque_to_smt"]
let seq_two_to_seq_BE (#a:Type) (x:seq (two a)) : (z:seq a{length z == length x * 2}) =
  let f (n:nat{n < length x * 2}) = two_select (index x (n / 2)) (1 - n % 2) in
  init (length x * 2) f

[@"opaque_to_smt"]
let seq_four_to_seq_LE (#a:Type) (x:seq (four a)) : (z:seq a{length z == length x * 4}) =
  let f (n:nat{n < length x * 4}) = four_select (index x (n / 4)) (n % 4) in
  init (length x * 4) f

[@"opaque_to_smt"]
let seq_four_to_seq_BE (#a:Type) (x:seq (four a)) : (z:seq a{length z == length x * 4}) =
  let f (n:nat{n < length x * 4}) = four_select (index x (n / 4)) (3 - n % 4) in
  init (length x * 4) f

[@"opaque_to_smt"]
let seq_to_seq_two_LE (#a:Type) (x:seq a{length x % 2 == 0}) : (z:seq (two a){length z == length x / 2}) =
  let f (n:nat{n < length x / 2}) = Mktwo (index x (n * 2)) (index x (n * 2 + 1)) in
  init (length x / 2) f

[@"opaque_to_smt"]
let seq_to_seq_two_BE (#a:Type) (x:seq a{length x % 2 == 0}) : (z:seq (two a){length z == length x / 2}) =
  let f (n:nat{n < length x / 2}) = Mktwo (index x (n * 2 + 1)) (index x (n * 2)) in
  init (length x / 2) f
val seq_to_seq_four_LE (#a: Type) (x: seq a {length x % 4 == 0})
    : (z: seq (four a) {length z == length x / 4})
x: FStar.Seq.Base.seq a {FStar.Seq.Base.length x % 4 == 0}
  -> z:
    FStar.Seq.Base.seq (Vale.Def.Words_s.four a)
      {FStar.Seq.Base.length z == FStar.Seq.Base.length x / 4}