val vecs_load_le:
    #vt:v_inttype
  -> #w:width
  -> #len:size_t{v len * (numbytes vt * w) <= max_size_t}
  -> o:lbuffer (vec_t vt w) len
  -> i:lbuffer uint8 (len *! (size (numbytes vt) *! size w)) ->
  Stack unit
    (requires fun h -> live h i /\ live h o /\ B.disjoint i o)
    (ensures  fun h0 _ h1 ->
      modifies1 o h0 h1 /\
      as_seq h1 o == vecs_from_bytes_le vt w (v len) (as_seq h0 i))
let vecs_load_le #vt #w #len o i =
  let h0 = ST.get () in
  fill h0 len o
  (fun h -> vecs_from_bytes_le_f vt w (v len) (as_seq h i))
  (fun j ->
    let h = ST.get () in
    let bj = sub i (j *! (size (numbytes vt) *! size w)) (size (numbytes vt) *! size w) in
    let r = vec_load_le vt w bj in
    as_seq_gsub h i (j *! (size (numbytes vt) *! size w)) (size (numbytes vt) *! size w);
    r);
  let h1 = ST.get () in
  eq_intro (as_seq h1 o) (vecs_from_bytes_le vt w (v len) (as_seq h0 i))
val vecs_load_le:
    #vt:v_inttype
  -> #w:width
  -> #len:size_t{v len * (numbytes vt * w) <= max_size_t}
  -> o:lbuffer (vec_t vt w) len
  -> i:lbuffer uint8 (len *! (size (numbytes vt) *! size w)) ->
  Stack unit
    (requires fun h -> live h i /\ live h o /\ B.disjoint i o)
    (ensures  fun h0 _ h1 ->
      modifies1 o h0 h1 /\
      as_seq h1 o == vecs_from_bytes_le vt w (v len) (as_seq h0 i))
let vecs_load_le #vt #w #len o i =
let h0 = ST.get () in
fill h0
  len
  o
  (fun h -> vecs_from_bytes_le_f vt w (v len) (as_seq h i))
  (fun j ->
      let h = ST.get () in
      let bj = sub i (j *! (size (numbytes vt) *! size w)) (size (numbytes vt) *! size w) in
      let r = vec_load_le vt w bj in
      as_seq_gsub h i (j *! (size (numbytes vt) *! size w)) (size (numbytes vt) *! size w);
      r);
let h1 = ST.get () in
eq_intro (as_seq h1 o) (vecs_from_bytes_le vt w (v len) (as_seq h0 i))
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 Lib.IntTypes.size_t Prims.b2t Prims.op_LessThanOrEqual FStar.Mul.op_Star Lib.IntTypes.v Lib.IntTypes.U32 Lib.IntTypes.PUB Lib.IntTypes.numbytes Lib.IntTypes.max_size_t Lib.Buffer.lbuffer Lib.IntVector.vec_t Lib.IntTypes.uint8 Lib.IntTypes.op_Star_Bang Lib.IntTypes.size Lib.Sequence.eq_intro Lib.Buffer.as_seq Lib.Buffer.MUT Lib.IntVector.Serialize.vecs_from_bytes_le Prims.unit FStar.Monotonic.HyperStack.mem FStar.HyperStack.ST.get Lib.Buffer.fill Lib.IntVector.Serialize.vecs_from_bytes_le_f Lib.IntTypes.size_nat Prims.op_LessThan Lib.Buffer.as_seq_gsub Lib.IntVector.vec_load_le Lib.Buffer.lbuffer_t Lib.IntTypes.int_t Lib.IntTypes.U8 Lib.IntTypes.SEC Lib.IntTypes.mul Lib.IntTypes.mk_int Lib.Buffer.sub
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]

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

let index_vecs_to_bytes_le #vt #w #len vl i =
  index_generate_blocks (numbytes vt * w) len len
    (vecs_to_bytes_le_f #vt #w #len vl) i


val vecs_to_bytes_be_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_be_f #vt #w #len vl i () =
  (), vec_to_bytes_be vl.[i]

let vecs_to_bytes_be #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_be_f #vt #w #len vl) () in
  o

let index_vecs_to_bytes_be #vt #w #len vl i =
  index_generate_blocks (numbytes vt * w) len len
    (vecs_to_bytes_be_f #vt #w #len vl) i
val vecs_load_le:
    #vt:v_inttype
  -> #w:width
  -> #len:size_t{v len * (numbytes vt * w) <= max_size_t}
  -> o:lbuffer (vec_t vt w) len
  -> i:lbuffer uint8 (len *! (size (numbytes vt) *! size w)) ->
  Stack unit
    (requires fun h -> live h i /\ live h o /\ B.disjoint i o)
    (ensures  fun h0 _ h1 ->
      modifies1 o h0 h1 /\
      as_seq h1 o == vecs_from_bytes_le vt w (v len) (as_seq h0 i))

    o: Lib.Buffer.lbuffer (Lib.IntVector.vec_t vt w) len ->
    i:
      Lib.Buffer.lbuffer Lib.IntTypes.uint8
        (len *! (Lib.IntTypes.size (Lib.IntTypes.numbytes vt) *! Lib.IntTypes.size w))
  -> FStar.HyperStack.ST.Stack Prims.unit