val parse_deplen_payload_unfold
      (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)
      (input: bytes)
    : Lemma
    (parse (parse_deplen_payload min max dlf ps h) input ==
      (match (parse (parse_fldata_strong ps (U32.v (dlf h))) input) with
        | None -> None
        | Some (x, consumed) -> Some (synth_deplen_data min max dlf ps h x, consumed)))
let parse_deplen_payload_unfold
  (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)
  (input: bytes)
: Lemma
  (parse (parse_deplen_payload min max dlf ps h) input == (match (parse (parse_fldata_strong ps (U32.v (dlf h))) input) with
    | None -> None
    | Some (x, consumed) -> Some (synth_deplen_data min max dlf ps h x, consumed)))
 = 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 ()
   else
     parse_synth_eq
       (parse_fldata_strong ps sz)
       (synth_deplen_data min max dlf ps h)
       input
val parse_deplen_payload_unfold
      (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)
      (input: bytes)
    : Lemma
    (parse (parse_deplen_payload min max dlf ps h) input ==
      (match (parse (parse_fldata_strong ps (U32.v (dlf h))) input) with
        | None -> None
        | Some (x, consumed) -> Some (synth_deplen_data min max dlf ps h x, consumed)))
let parse_deplen_payload_unfold
      (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)
      (input: bytes)
    : Lemma
    (parse (parse_deplen_payload min max dlf ps h) input ==
      (match (parse (parse_fldata_strong ps (U32.v (dlf h))) input) with
        | None -> None
        | Some (x, consumed) -> Some (synth_deplen_data min max dlf ps h x, consumed))) =
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 ()
else parse_synth_eq (parse_fldata_strong ps sz) (synth_deplen_data min max dlf ps h) input
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.Bytes.bytes Prims.bool LowParse.Spec.Combinators.parse_synth_eq LowParse.Spec.FLData.parse_fldata_kind LowParse.Spec.FLData.parse_fldata_strong_t LowParse.Spec.Base.refine_with_tag LowParse.Spec.DepLen.parse_deplen_data_t LowParse.Spec.DepLen.calc_tag_of_deplen_data LowParse.Spec.FLData.parse_fldata_strong LowParse.Spec.DepLen.synth_deplen_data Prims.unit 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 Prims.l_True Prims.squash Prims.eq2 FStar.Pervasives.Native.option FStar.Pervasives.Native.tuple2 LowParse.Spec.Base.consumed_length LowParse.Spec.Base.parse LowParse.Spec.DepLen.parse_deplen_payload FStar.Pervasives.Native.None FStar.Pervasives.Native.Some FStar.Pervasives.Native.Mktuple2 Prims.Nil FStar.Pervasives.pattern
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)
: 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)


(* unfold is a more human readable version and do double-check of the definition

   This lemma says using the parser defined above is equivalent to using a fixed-length
   parser with the calculated size and then attach the header
*) 

let parse_deplen_payload_unfold
  (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)
  (input: bytes)
: Lemma
  (parse (parse_deplen_payload min max dlf ps h) input == (match (parse (parse_fldata_strong ps (U32.v (dlf h))) input) with
    | None -> None
val parse_deplen_payload_unfold
      (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)
      (input: bytes)
    : Lemma
    (parse (parse_deplen_payload min max dlf ps h) input ==
      (match (parse (parse_fldata_strong ps (U32.v (dlf h))) input) with
        | None -> None
        | Some (x, consumed) -> Some (synth_deplen_data min max dlf ps h x, consumed)))

    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 ->
    input: LowParse.Bytes.bytes
  -> FStar.Pervasives.Lemma
    (ensures
      LowParse.Spec.Base.parse (LowParse.Spec.DepLen.parse_deplen_payload min max dlf ps h) input ==
      (match
          LowParse.Spec.Base.parse (LowParse.Spec.FLData.parse_fldata_strong ps
                (FStar.UInt32.v (dlf h)))
            input
        with
        | FStar.Pervasives.Native.None #_ -> FStar.Pervasives.Native.None
        | FStar.Pervasives.Native.Some #_ (FStar.Pervasives.Native.Mktuple2 #_ #_ x consumed) ->
          FStar.Pervasives.Native.Some
          (LowParse.Spec.DepLen.synth_deplen_data min max dlf ps h x, consumed)))