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))
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))
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.IntTypes.uint8 Prims.op_LessThan Lib.IntVector.vec_from_bytes_be Lib.Sequence.sub Lib.IntVector.vec_t
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
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

    vt: Lib.IntVector.v_inttype ->
    w: Lib.IntVector.width ->
    len: Prims.nat{len * (Lib.IntTypes.numbytes vt * w) <= Lib.IntTypes.max_size_t} ->
    b: Lib.Sequence.lseq Lib.IntTypes.uint8 (len * (Lib.IntTypes.numbytes vt * w)) ->
    i: Prims.nat{i < len}
  -> Lib.IntVector.vec_t vt w