val tag_of_bounded_vlgen_payload
      (min: nat)
      (max: nat{min <= max /\ max < 4294967296})
      (#k: parser_kind)
      (#t: Type)
      (#p: parser k t)
      (s: serializer p)
      (x: parse_bounded_vldata_strong_t min max s)
    : GTot (bounded_int32 min max)
let tag_of_bounded_vlgen_payload
  (min: nat)
  (max: nat { min <= max /\ max < 4294967296 } )
  (#k: parser_kind)
  (#t: Type)
  (#p: parser k t)
  (s: serializer p)
  (x: parse_bounded_vldata_strong_t min max s)
: GTot (bounded_int32 min max)
= U32.uint_to_t (Seq.length (serialize s x))
val tag_of_bounded_vlgen_payload
      (min: nat)
      (max: nat{min <= max /\ max < 4294967296})
      (#k: parser_kind)
      (#t: Type)
      (#p: parser k t)
      (s: serializer p)
      (x: parse_bounded_vldata_strong_t min max s)
    : GTot (bounded_int32 min max)
let tag_of_bounded_vlgen_payload
      (min: nat)
      (max: nat{min <= max /\ max < 4294967296})
      (#k: parser_kind)
      (#t: Type)
      (#p: parser k t)
      (s: serializer p)
      (x: parse_bounded_vldata_strong_t min max s)
    : GTot (bounded_int32 min max) =
U32.uint_to_t (Seq.length (serialize s x))
LowParse.Spec.VLGen.fst.checked
prims.fst.checked LowParse.Spec.VLData.fsti.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.VLGen.fst
Prims.nat Prims.l_and Prims.b2t Prims.op_LessThanOrEqual Prims.op_LessThan LowParse.Spec.Base.parser_kind LowParse.Spec.Base.parser LowParse.Spec.Base.serializer LowParse.Spec.VLData.parse_bounded_vldata_strong_t FStar.UInt32.uint_to_t FStar.Seq.Base.length LowParse.Bytes.byte LowParse.Spec.Base.serialize LowParse.Spec.BoundedInt.bounded_int32
module LowParse.Spec.VLGen
include LowParse.Spec.Combinators
include LowParse.Spec.AllIntegers
include LowParse.Spec.VLData // for parse_bounded_vldata_strong_t

(* TODO: this module should deprecate and replace LowParse.Spec.VLData *)

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

let tag_of_bounded_vlgen_payload
  (min: nat)
  (max: nat { min <= max /\ max < 4294967296 } )
  (#k: parser_kind)
  (#t: Type)
  (#p: parser k t)
  (s: serializer p)
  (x: parse_bounded_vldata_strong_t min max s)
val tag_of_bounded_vlgen_payload
      (min: nat)
      (max: nat{min <= max /\ max < 4294967296})
      (#k: parser_kind)
      (#t: Type)
      (#p: parser k t)
      (s: serializer p)
      (x: parse_bounded_vldata_strong_t min max s)
    : GTot (bounded_int32 min max)

    min: Prims.nat ->
    max: Prims.nat{min <= max /\ max < 4294967296} ->
    s: LowParse.Spec.Base.serializer p ->
    x: LowParse.Spec.VLData.parse_bounded_vldata_strong_t min max s
  -> Prims.GTot (LowParse.Spec.BoundedInt.bounded_int32 min max)