val parse_deplen_payload
      (min: nat)
      (max: nat{min <= max /\ max < 4294967296})
      (#ht #pt: Type)
      (dlf: (ht -> Tot (bounded_int32 min max)))
      (#pk: parser_kind)
      (#pp: parser pk pt)
      (ps: serializer pp)
      (h: ht)
    : Tot
    (parser (parse_deplen_payload_kind min max pk)
        (refine_with_tag (calc_tag_of_deplen_data min max dlf ps) h))
let parse_deplen_payload
  (min : nat)
  (max : nat { min <= max /\ max < 4294967296 } )
  (#ht : Type)
  (#pt : Type)
  (dlf : ht -> Tot (bounded_int32 min max) )
  (#pk : parser_kind)
  (#pp : parser pk pt)
  (ps : serializer pp)
  (h : ht)
: Tot (parser (parse_deplen_payload_kind min max pk) (refine_with_tag (calc_tag_of_deplen_data min max dlf ps) h)) 
= let sz = (U32.v (dlf h)) in
  let bounds_off =
    pk.parser_kind_low > sz || (
    match pk.parser_kind_high with
    | None -> false
    | Some pkmax -> pkmax < sz
  )
  in
  if bounds_off
  then fail_parser (parse_deplen_payload_kind min max pk) (refine_with_tag (calc_tag_of_deplen_data min max dlf ps) h)
  else
    weaken (parse_deplen_payload_kind min max pk)
      (parse_fldata_strong ps sz
      `parse_synth`
      synth_deplen_data min max dlf ps h)
val parse_deplen_payload
      (min: nat)
      (max: nat{min <= max /\ max < 4294967296})
      (#ht #pt: Type)
      (dlf: (ht -> Tot (bounded_int32 min max)))
      (#pk: parser_kind)
      (#pp: parser pk pt)
      (ps: serializer pp)
      (h: ht)
    : Tot
    (parser (parse_deplen_payload_kind min max pk)
        (refine_with_tag (calc_tag_of_deplen_data min max dlf ps) h))
let parse_deplen_payload
      (min: nat)
      (max: nat{min <= max /\ max < 4294967296})
      (#ht #pt: Type)
      (dlf: (ht -> Tot (bounded_int32 min max)))
      (#pk: parser_kind)
      (#pp: parser pk pt)
      (ps: serializer pp)
      (h: ht)
    : Tot
    (parser (parse_deplen_payload_kind min max pk)
        (refine_with_tag (calc_tag_of_deplen_data min max dlf ps) h)) =
let sz = (U32.v (dlf h)) in
let bounds_off =
  pk.parser_kind_low > sz ||
  (match pk.parser_kind_high with
    | None -> false
    | Some pkmax -> pkmax < sz)
in
if bounds_off
then
  fail_parser (parse_deplen_payload_kind min max pk)
    (refine_with_tag (calc_tag_of_deplen_data min max dlf ps) h)
else
  weaken (parse_deplen_payload_kind min max pk)
    ((parse_fldata_strong ps sz) `parse_synth` (synth_deplen_data min max dlf ps h))
LowParse.Spec.DepLen.fst.checked
prims.fst.checked LowParse.Spec.VLGen.fst.checked LowParse.Spec.Combinators.fsti.checked LowParse.Spec.AllIntegers.fst.checked FStar.UInt32.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked
LowParse.Spec.DepLen.fst
Prims.nat Prims.l_and Prims.b2t Prims.op_LessThanOrEqual Prims.op_LessThan LowParse.Spec.BoundedInt.bounded_int32 LowParse.Spec.Base.parser_kind LowParse.Spec.Base.parser LowParse.Spec.Base.serializer LowParse.Spec.Combinators.fail_parser LowParse.Spec.DepLen.parse_deplen_payload_kind LowParse.Spec.Base.refine_with_tag LowParse.Spec.DepLen.parse_deplen_data_t LowParse.Spec.DepLen.calc_tag_of_deplen_data Prims.bool LowParse.Spec.Base.weaken LowParse.Spec.FLData.parse_fldata_kind LowParse.Spec.Combinators.parse_synth LowParse.Spec.FLData.parse_fldata_strong_t LowParse.Spec.FLData.parse_fldata_strong LowParse.Spec.DepLen.synth_deplen_data Prims.op_BarBar Prims.op_GreaterThan LowParse.Spec.Base.__proj__Mkparser_kind'__item__parser_kind_low LowParse.Spec.Base.__proj__Mkparser_kind'__item__parser_kind_high FStar.UInt.uint_t FStar.UInt32.v
module LowParse.Spec.DepLen

(* LowParse specification module for parsing structures with dependent length

   Example:

   struct {
     uint len;
     uint foo;
     uint buf[len];
   };

*)

include LowParse.Spec.Combinators
include LowParse.Spec.AllIntegers
include LowParse.Spec.VLGen

module U32 = FStar.UInt32
module Seq = FStar.Seq


(* arguments

     @min     :
     @max     : integer bounds
     @ht      : header type
     @hk      : header parser metadata
     @hp      : header parser
     @h       : header data
     @dlf     : dependent length function
     @pt      : payload type
     @pk      : payload parser metadata
     @pp      : payload parser
     @ps      : payload serializer
     @x       : data

*)

(* data type of the dependent length parser, which is a pair of the header and the payload *)

let parse_deplen_data_t 
  (min : nat)
  (max : nat { min <= max /\ max < 4294967296 } )
  (#ht : Type)
  (#pt : Type)
  (dlf : ht -> Tot (bounded_int32 min max) )
  (#pk : parser_kind)
  (#pp : parser pk pt)
  (ps : serializer pp)
= x:(ht & pt) {U32.v (dlf (fst x)) == Seq.length (serialize ps (snd x) ) }


(* the tag for a piece of dependent length data is just its header *)

let calc_tag_of_deplen_data
  (min : nat)
  (max : nat { min <= max /\ max < 4294967296 } )
  (#ht : Type)
  (#pt : Type)
  (dlf : ht -> Tot (bounded_int32 min max) )
  (#pk : parser_kind)
  (#pp : parser pk pt)
  (ps : serializer pp)
  (x : parse_deplen_data_t min max dlf ps)
: GTot ht
= fst x


(* synth put the header and the payload together to get the data *)

let synth_deplen_data
  (min : nat)
  (max : nat { min <= max /\ max < 4294967296 } )
  (#ht : Type)
  (#pt : Type)
  (dlf : ht -> Tot (bounded_int32 min max) )
  (#pk : parser_kind)
  (#pp : parser pk pt)
  (ps : serializer pp)
  (h : ht)
  (x : parse_fldata_strong_t ps (U32.v (dlf h)))
: Tot (refine_with_tag (calc_tag_of_deplen_data min max dlf ps) h) 
= (h, x)


(* metadata of the payload, reuse bounded_vlgen_payload *)

let parse_deplen_payload_kind = parse_bounded_vlgen_payload_kind


(* parser spec for the dependent length payload which attaches the header to generate the data *)

let parse_deplen_payload
  (min : nat)
  (max : nat { min <= max /\ max < 4294967296 } )
  (#ht : Type)
  (#pt : Type)
  (dlf : ht -> Tot (bounded_int32 min max) )
  (#pk : parser_kind)
  (#pp : parser pk pt)
  (ps : serializer pp)
  (h : ht)
val parse_deplen_payload
      (min: nat)
      (max: nat{min <= max /\ max < 4294967296})
      (#ht #pt: Type)
      (dlf: (ht -> Tot (bounded_int32 min max)))
      (#pk: parser_kind)
      (#pp: parser pk pt)
      (ps: serializer pp)
      (h: ht)
    : Tot
    (parser (parse_deplen_payload_kind min max pk)
        (refine_with_tag (calc_tag_of_deplen_data min max dlf ps) h))

    min: Prims.nat ->
    max: Prims.nat{min <= max /\ max < 4294967296} ->
    dlf: (_: ht -> LowParse.Spec.BoundedInt.bounded_int32 min max) ->
    ps: LowParse.Spec.Base.serializer pp ->
    h: ht
  -> LowParse.Spec.Base.parser (LowParse.Spec.DepLen.parse_deplen_payload_kind min max pk)
      (LowParse.Spec.Base.refine_with_tag (LowParse.Spec.DepLen.calc_tag_of_deplen_data min
              max
              dlf
              ps)
          h)