val serialize32_array
      (#k: parser_kind)
      (#t: Type)
      (#p: parser k t)
      (#s: serializer p)
      (s32: partial_serializer32 s)
      (array_byte_size: nat{array_byte_size < 4294967296})
      (elem_count: nat)
      (u: unit{fldata_array_precond k array_byte_size elem_count == true})
    : Tot (serializer32 (serialize_array s array_byte_size elem_count u))
let serialize32_array
  (#k: parser_kind)
  (#t: Type)
  (#p: parser k t)
  (#s: serializer p)
  (s32: partial_serializer32 s)
  (array_byte_size: nat { array_byte_size < 4294967296 } )
  (elem_count: nat)
  (u : unit { fldata_array_precond k array_byte_size elem_count == true } )
: Tot (serializer32 (serialize_array s array_byte_size elem_count u))
= fun x -> serialize32_array' s32 array_byte_size elem_count u x
val serialize32_array
      (#k: parser_kind)
      (#t: Type)
      (#p: parser k t)
      (#s: serializer p)
      (s32: partial_serializer32 s)
      (array_byte_size: nat{array_byte_size < 4294967296})
      (elem_count: nat)
      (u: unit{fldata_array_precond k array_byte_size elem_count == true})
    : Tot (serializer32 (serialize_array s array_byte_size elem_count u))
let serialize32_array
      (#k: parser_kind)
      (#t: Type)
      (#p: parser k t)
      (#s: serializer p)
      (s32: partial_serializer32 s)
      (array_byte_size: nat{array_byte_size < 4294967296})
      (elem_count: nat)
      (u: unit{fldata_array_precond k array_byte_size elem_count == true})
    : Tot (serializer32 (serialize_array s array_byte_size elem_count u)) =
fun x -> serialize32_array' s32 array_byte_size 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.partial_serializer32 Prims.nat Prims.b2t Prims.op_LessThan Prims.unit Prims.eq2 Prims.bool LowParse.Spec.Array.fldata_array_precond LowParse.Spec.Array.array LowParse.SLow.Array.serialize32_array' LowParse.SLow.Base.bytes32 LowParse.SLow.Base.serializer32_correct LowParse.Spec.Array.parse_array_kind LowParse.Spec.Array.parse_array LowParse.Spec.Array.serialize_array LowParse.SLow.Base.serializer32
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 } )
: 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

inline_for_extraction
let serialize32_array'
  (#k: parser_kind)
  (#t: Type)
  (#p: parser k t)
  (#s: serializer p)
  (s32: partial_serializer32 s)
  (array_byte_size: nat { array_byte_size < 4294967296 } )
  (elem_count: nat)
  (u : unit { fldata_array_precond k array_byte_size elem_count == true } )
: Tot (serializer32 (serialize_array' s array_byte_size elem_count u))
= [@inline_let]
  let _ =
    fldata_to_array_inj s array_byte_size elem_count u
  in
  [@inline_let]
  let _ =
    array_to_fldata_to_array s array_byte_size elem_count u
  in
  serialize32_synth
    _
    (fldata_to_array s array_byte_size elem_count u)
    _
    (serialize32_fldata_strong
      (partial_serialize32_list _ _ s32 ())
      array_byte_size
    )
    (array_to_fldata s array_byte_size elem_count u)
    (fun x -> array_to_fldata s array_byte_size elem_count u x)
    ()

inline_for_extraction
let serialize32_array
  (#k: parser_kind)
  (#t: Type)
  (#p: parser k t)
  (#s: serializer p)
  (s32: partial_serializer32 s)
  (array_byte_size: nat { array_byte_size < 4294967296 } )
  (elem_count: nat)
  (u : unit { fldata_array_precond k array_byte_size elem_count == true } )
val serialize32_array
      (#k: parser_kind)
      (#t: Type)
      (#p: parser k t)
      (#s: serializer p)
      (s32: partial_serializer32 s)
      (array_byte_size: nat{array_byte_size < 4294967296})
      (elem_count: nat)
      (u: unit{fldata_array_precond k array_byte_size elem_count == true})
    : Tot (serializer32 (serialize_array s array_byte_size elem_count u))

    s32: LowParse.SLow.Base.partial_serializer32 s ->
    array_byte_size: Prims.nat{array_byte_size < 4294967296} ->
    elem_count: Prims.nat ->
    u41:
      u43: Prims.unit{LowParse.Spec.Array.fldata_array_precond k array_byte_size elem_count == true}
  -> LowParse.SLow.Base.serializer32 (LowParse.Spec.Array.serialize_array s
          array_byte_size
          elem_count
          u41)