val parse32_array
      (#k: parser_kind)
      (#t: Type)
      (#p: parser k t)
      (s: serializer p)
      (p32: parser32 p)
      (array_byte_size: nat)
      (array_byte_size32: U32.t{U32.v array_byte_size32 == array_byte_size})
      (elem_count: nat)
      (u: unit{fldata_array_precond k array_byte_size elem_count == true})
    : Tot (parser32 (parse_array s array_byte_size elem_count))
let parse32_array
  (#k: parser_kind)
  (#t: Type)
  (#p: parser k t)
  (s: serializer p)
  (p32: parser32 p)
  (array_byte_size: nat)
  (array_byte_size32: U32.t { U32.v array_byte_size32 == array_byte_size } )
  (elem_count: nat)
  (u : unit { fldata_array_precond k array_byte_size elem_count == true } )
: Tot (parser32 (parse_array s array_byte_size elem_count))
= fun x -> parse32_array' s p32 array_byte_size array_byte_size32 elem_count u x
val parse32_array
      (#k: parser_kind)
      (#t: Type)
      (#p: parser k t)
      (s: serializer p)
      (p32: parser32 p)
      (array_byte_size: nat)
      (array_byte_size32: U32.t{U32.v array_byte_size32 == array_byte_size})
      (elem_count: nat)
      (u: unit{fldata_array_precond k array_byte_size elem_count == true})
    : Tot (parser32 (parse_array s array_byte_size elem_count))
let parse32_array
      (#k: parser_kind)
      (#t: Type)
      (#p: parser k t)
      (s: serializer p)
      (p32: parser32 p)
      (array_byte_size: nat)
      (array_byte_size32: U32.t{U32.v array_byte_size32 == array_byte_size})
      (elem_count: nat)
      (u: unit{fldata_array_precond k array_byte_size elem_count == true})
    : Tot (parser32 (parse_array s array_byte_size elem_count)) =
fun x -> parse32_array' s p32 array_byte_size array_byte_size32 elem_count u x
LowParse.SLow.Array.fst.checked
prims.fst.checked LowParse.Spec.Array.fst.checked LowParse.SLow.VLData.fst.checked LowParse.SLow.List.fst.checked LowParse.SLow.FLData.fst.checked FStar.UInt32.fsti.checked FStar.Pervasives.fsti.checked
LowParse.SLow.Array.fst
LowParse.Spec.Base.parser_kind LowParse.Spec.Base.parser LowParse.Spec.Base.serializer LowParse.SLow.Base.parser32 Prims.nat FStar.UInt32.t Prims.eq2 Prims.int Prims.l_or FStar.UInt.size FStar.UInt32.n Prims.b2t Prims.op_GreaterThanOrEqual FStar.UInt32.v Prims.unit Prims.bool LowParse.Spec.Array.fldata_array_precond LowParse.SLow.Base.bytes32 LowParse.SLow.Array.parse32_array' FStar.Pervasives.Native.option FStar.Pervasives.Native.tuple2 LowParse.Spec.Array.array LowParse.SLow.Base.parser32_correct LowParse.Spec.Array.parse_array_kind LowParse.Spec.Array.parse_array
module LowParse.SLow.Array
include LowParse.SLow.FLData
include LowParse.SLow.VLData
include LowParse.SLow.List
include LowParse.Spec.Array

module U32 = FStar.UInt32

inline_for_extraction
let parse32_array'
  (#k: parser_kind)
  (#t: Type)
  (#p: parser k t)
  (s: serializer p)
  (p32: parser32 p)
  (array_byte_size: nat)
  (array_byte_size32: U32.t { U32.v array_byte_size32 == array_byte_size } )
  (elem_count: nat)
  (u : unit { fldata_array_precond k array_byte_size elem_count == true } )
: Tot (parser32 (parse_array' s array_byte_size elem_count))
= [@inline_let]
  let _ =
    fldata_to_array_inj s array_byte_size elem_count u
  in
  parse32_synth
    _
    (fldata_to_array s array_byte_size elem_count u)
    (fun x -> fldata_to_array s array_byte_size elem_count u x)
    (parse32_fldata_strong
      (serialize_list _ s)
      (parse32_list p32)
      array_byte_size
      array_byte_size32
    )
    ()

inline_for_extraction
let parse32_array
  (#k: parser_kind)
  (#t: Type)
  (#p: parser k t)
  (s: serializer p)
  (p32: parser32 p)
  (array_byte_size: nat)
  (array_byte_size32: U32.t { U32.v array_byte_size32 == array_byte_size } )
  (elem_count: nat)
  (u : unit { fldata_array_precond k array_byte_size elem_count == true } )
val parse32_array
      (#k: parser_kind)
      (#t: Type)
      (#p: parser k t)
      (s: serializer p)
      (p32: parser32 p)
      (array_byte_size: nat)
      (array_byte_size32: U32.t{U32.v array_byte_size32 == array_byte_size})
      (elem_count: nat)
      (u: unit{fldata_array_precond k array_byte_size elem_count == true})
    : Tot (parser32 (parse_array s array_byte_size elem_count))

    s: LowParse.Spec.Base.serializer p ->
    p32: LowParse.SLow.Base.parser32 p ->
    array_byte_size: Prims.nat ->
    array_byte_size32: FStar.UInt32.t{FStar.UInt32.v array_byte_size32 == array_byte_size} ->
    elem_count: Prims.nat ->
    u26:
      u28: Prims.unit{LowParse.Spec.Array.fldata_array_precond k array_byte_size elem_count == true}
  -> LowParse.SLow.Base.parser32 (LowParse.Spec.Array.parse_array s array_byte_size elem_count)