val parse32_fldata_strong
      (#k: parser_kind)
      (#t: Type)
      (#p: parser k t)
      (s: serializer p)
      (p32: parser32 p)
      (sz: nat)
      (sz32: U32.t{U32.v sz32 == sz})
    : Tot (parser32 (parse_fldata_strong s sz))
let parse32_fldata_strong
  (#k: parser_kind)
  (#t: Type)
  (#p: parser k t)
  (s: serializer p)
  (p32: parser32 p)
  (sz: nat)
  (sz32: U32.t { U32.v sz32 == sz } )
: Tot (parser32 (parse_fldata_strong s sz))
= (fun (input: bytes32) -> ((
    match parse32_fldata p32 sz sz32 input with
    | Some (v, consumed) ->
      assert (
        parse_fldata_strong_correct s sz (B32.reveal input) (U32.v consumed) v;
        Seq.length (s v) == sz
      );
      Some ((v <: parse_fldata_strong_t s sz), consumed)
    | None -> None
    )   
    <: (res: option (parse_fldata_strong_t s sz * U32.t) { parser32_correct (parse_fldata_strong s sz) input res } )))
val parse32_fldata_strong
      (#k: parser_kind)
      (#t: Type)
      (#p: parser k t)
      (s: serializer p)
      (p32: parser32 p)
      (sz: nat)
      (sz32: U32.t{U32.v sz32 == sz})
    : Tot (parser32 (parse_fldata_strong s sz))
let parse32_fldata_strong
      (#k: parser_kind)
      (#t: Type)
      (#p: parser k t)
      (s: serializer p)
      (p32: parser32 p)
      (sz: nat)
      (sz32: U32.t{U32.v sz32 == sz})
    : Tot (parser32 (parse_fldata_strong s sz)) =
(fun (input: bytes32) ->
    ((match parse32_fldata p32 sz sz32 input with
        | Some (v, consumed) ->
          assert (parse_fldata_strong_correct s sz (B32.reveal input) (U32.v consumed) v;
              Seq.length (s v) == sz);
          Some ((v <: parse_fldata_strong_t s sz), consumed)
        | None -> None)
      <:
      (res:
        option (parse_fldata_strong_t s sz * U32.t)
          {parser32_correct (parse_fldata_strong s sz) input res})))
LowParse.SLow.FLData.fst.checked
prims.fst.checked LowParse.Spec.FLData.fst.checked LowParse.SLow.Combinators.fst.checked LowParse.Bytes32.fst.checked FStar.UInt32.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked
LowParse.SLow.FLData.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 LowParse.SLow.Base.bytes32 LowParse.SLow.FLData.parse32_fldata FStar.Pervasives.Native.Some FStar.Pervasives.Native.tuple2 LowParse.Spec.FLData.parse_fldata_strong_t FStar.Pervasives.Native.Mktuple2 Prims.unit Prims._assert FStar.Seq.Base.length LowParse.Bytes.byte LowParse.Spec.FLData.parse_fldata_strong_correct FStar.Bytes.reveal FStar.Pervasives.Native.None FStar.Pervasives.Native.option LowParse.SLow.Base.parser32_correct LowParse.Spec.FLData.parse_fldata_kind LowParse.Spec.FLData.parse_fldata_strong
module LowParse.SLow.FLData
include LowParse.Spec.FLData
include LowParse.SLow.Combinators

module B32 = LowParse.Bytes32
module U32 = FStar.UInt32

inline_for_extraction
let parse32_fldata
  (#k: parser_kind)
  (#t: Type)
  (#p: parser k t)
  (p32: parser32 p)
  (sz: nat)
  (sz32: U32.t { U32.v sz32 == sz } )
: Tot (parser32 (parse_fldata p sz))
= (fun (input: bytes32) -> ((
    if U32.lt (B32.len input) sz32
    then
      None
    else
      match p32 (B32.b32slice input 0ul sz32) with
      | Some (v, consumed) ->
	if consumed = sz32
	then begin
	  Some (v, consumed)
	end else None
      | None -> None
  ) <: (res: option (t * U32.t) { parser32_correct (parse_fldata p sz) input res } )))

inline_for_extraction
let parse32_fldata_strong
  (#k: parser_kind)
  (#t: Type)
  (#p: parser k t)
  (s: serializer p)
  (p32: parser32 p)
  (sz: nat)
  (sz32: U32.t { U32.v sz32 == sz } )
val parse32_fldata_strong
      (#k: parser_kind)
      (#t: Type)
      (#p: parser k t)
      (s: serializer p)
      (p32: parser32 p)
      (sz: nat)
      (sz32: U32.t{U32.v sz32 == sz})
    : Tot (parser32 (parse_fldata_strong s sz))

    s: LowParse.Spec.Base.serializer p ->
    p32: LowParse.SLow.Base.parser32 p ->
    sz: Prims.nat ->
    sz32: FStar.UInt32.t{FStar.UInt32.v sz32 == sz}
  -> LowParse.SLow.Base.parser32 (LowParse.Spec.FLData.parse_fldata_strong s sz)