val vecs_to_bytes_le: #vt:v_inttype -> #w:width -> #len:nat{len * (numbytes vt * w) <= max_size_t}
  -> vl:lseq (vec_t vt w) len -> lseq uint8 (len * (numbytes vt * w))
let vecs_to_bytes_le #vt #w #len vl =
  let a_spec (i:nat{i <= len}) = unit in
  let _, o = generate_blocks (numbytes vt * w) len len a_spec
    (vecs_to_bytes_le_f #vt #w #len vl) () in
  o
val vecs_to_bytes_le: #vt:v_inttype -> #w:width -> #len:nat{len * (numbytes vt * w) <= max_size_t}
  -> vl:lseq (vec_t vt w) len -> lseq uint8 (len * (numbytes vt * w))
let vecs_to_bytes_le #vt #w #len vl =
let a_spec (i: nat{i <= len}) = unit in
let _, o =
  generate_blocks (numbytes vt * w) len len a_spec (vecs_to_bytes_le_f #vt #w #len vl) ()
in
o
Lib.IntVector.Serialize.fst.checked
prims.fst.checked LowStar.Buffer.fst.checked FStar.ST.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked
Lib.IntVector.Serialize.fst
Lib.IntVector.v_inttype Lib.IntVector.width Prims.nat Prims.b2t Prims.op_LessThanOrEqual FStar.Mul.op_Star Lib.IntTypes.numbytes Lib.IntTypes.max_size_t Lib.Sequence.lseq Lib.IntVector.vec_t Lib.Sequence.seq Lib.IntTypes.uint8 Prims.eq2 Prims.int Lib.Sequence.length FStar.Pervasives.Native.tuple2 Lib.IntTypes.int_t Lib.IntTypes.U8 Lib.IntTypes.SEC Prims.op_Multiply Lib.Sequence.generate_blocks Lib.IntVector.Serialize.vecs_to_bytes_le_f Prims.eqtype Prims.unit
module Lib.IntVector.Serialize

// the proofs are the same as in Lib.ByteSequence and Lib.ByteBuffer

#set-options "--z3rlimit 50 --max_fuel 0 --max_ifuel 0"

val vecs_from_bytes_le_f:
    vt:v_inttype
  -> w:width
  -> len:nat{len * (numbytes vt * w) <= max_size_t}
  -> b:lseq uint8 (len * (numbytes vt * w))
  -> i:nat{i < len} ->
  vec_t vt w

let vecs_from_bytes_le_f vt w len b i =
  vec_from_bytes_le vt w (LSeq.sub b (i * (numbytes vt * w)) (numbytes vt * w))

let vecs_from_bytes_le vt w len b =
  LSeq.createi len (vecs_from_bytes_le_f vt w len b)

let index_vecs_from_bytes_le vt w len b i = ()


val vecs_from_bytes_be_f:
    vt:v_inttype
  -> w:width
  -> len:nat{len * (numbytes vt * w) <= max_size_t}
  -> b:lseq uint8 (len * (numbytes vt * w))
  -> i:nat{i < len} ->
  vec_t vt w

let vecs_from_bytes_be_f vt w len b i =
  vec_from_bytes_be vt w (LSeq.sub b (i * (numbytes vt * w)) (numbytes vt * w))

let vecs_from_bytes_be vt w len b =
  LSeq.createi len (vecs_from_bytes_be_f vt w len b)

let index_vecs_from_bytes_be vt w len b i = ()


val vecs_to_bytes_le_f:
    #vt:v_inttype
  -> #w:width
  -> #len:nat{len * (numbytes vt * w) <= max_size_t}
  -> vl:lseq (vec_t vt w) len
  -> i:nat{i < len}
  -> unit ->
  unit & lseq uint8 (numbytes vt * w)

let vecs_to_bytes_le_f #vt #w #len vl i () =
  (), vec_to_bytes_le vl.[i]
val vecs_to_bytes_le: #vt:v_inttype -> #w:width -> #len:nat{len * (numbytes vt * w) <= max_size_t}
  -> vl:lseq (vec_t vt w) len -> lseq uint8 (len * (numbytes vt * w))
vl: Lib.Sequence.lseq (Lib.IntVector.vec_t vt w) len
  -> Lib.Sequence.lseq Lib.IntTypes.uint8 (len * (Lib.IntTypes.numbytes vt * w))