val parse_asn1_envelop_tag_with_TLV_kind (a: asn1_tag_t) : parser_kind
val parse_asn1_envelop_tag_with_TLV_kind (a: asn1_tag_t) : parser_kind
let parse_asn1_envelop_tag_with_TLV_kind
  (a: asn1_tag_t)
: parser_kind
= parse_asn1_tag_kind
  `and_then_kind`
  parse_asn1_length_kind_of_type a
  `and_then_kind`
  weak_kind_of_type a
module ASN1.Spec.Value.Envelop

open ASN1.Base
open ASN1.Spec.Base
open ASN1.Spec.Tag
open ASN1.Spec.Length
open LowParse.Spec.FLData

open FStar.Integers

(* NOTE: Read after `ASN1.Spec.Tag`, `ASN1.Spec.Length`, `ASN1.Spec.Value.*` *)

(* NOTE: Use `parse_fldata_strong` to construct fixed-length parsers (with the strong prefix proeprty),
         where these fixed-length is runtimely parsed.
 *)

// unfold
inline_for_extraction
let inbound_envelop_tag_with_value_of
  (#k: parser_kind)
  (#t: Type0)
  (#p: parser k t)
  (a: asn1_tag_t)
  (s: serializer p)
= x: t{ asn1_value_length_inbound_of_type a (length_of_opaque_serialization s x) }

/// Tagging function
///
noextract
val parser_tag_of_asn1_envelop_tag_with
  (#k: parser_kind)
  (#t: Type0)
  (#p: parser k t)
  (a: asn1_tag_t)
  (s: serializer p)
  (data: inbound_envelop_tag_with_value_of a s )
: GTot (the_asn1_tag a & asn1_value_int32_of_type a)

noextract
val synth_asn1_envelop_tag_with
  (#k: parser_kind)
  (#t: Type0)
  (#p: parser k t)
  (a: asn1_tag_t)
  (s: serializer p)
  (tag: (the_asn1_tag a & asn1_value_int32_of_type a))
  (y: parse_fldata_strong_t s (v (snd tag)))
: GTot (refine_with_tag (parser_tag_of_asn1_envelop_tag_with a s) tag)

noextract
val synth_asn1_envelop_tag_with_inverse
  (#k: parser_kind)
  (#t: Type0)
  (#p: parser k t)
  (a: asn1_tag_t)
  (s: serializer p)
  (tag: (the_asn1_tag a & asn1_value_int32_of_type a))
  (data: refine_with_tag (parser_tag_of_asn1_envelop_tag_with a s) tag)
: GTot (y: parse_fldata_strong_t s (v (snd tag)){ data == synth_asn1_envelop_tag_with a s tag y })

/// ASN.1 a value parser/serializer
///
noextract
val parse_asn1_envelop_tag_with
  (#k: parser_kind)
  (#t: Type0)
  (#p: parser k t)
  (a: asn1_tag_t)
  (s: serializer p)
  (tag: the_asn1_tag a & asn1_value_int32_of_type a)
: parser (parse_fldata_kind (v (snd tag)) k) (refine_with_tag (parser_tag_of_asn1_envelop_tag_with a s) tag)

val lemma_parse_asn1_envelop_tag_with_unfold
  (#k: parser_kind)
  (#t: Type0)
  (#p: parser k t)
  (a: asn1_tag_t)
  (s: serializer p)
  (tag: the_asn1_tag a & asn1_value_int32_of_type a)
  (input: bytes)
: Lemma (
  parse (parse_asn1_envelop_tag_with a s tag) input ==
 (match parse (parse_fldata_strong s (v (snd tag))) input with
  | None -> None
  | Some (value, consumed) -> Some (synth_asn1_envelop_tag_with a s tag value, consumed)))

noextract
val parse_asn1_envelop_tag_with_weak
  (#k: parser_kind)
  (#t: Type0)
  (#p: parser k t)
  (a: asn1_tag_t)
  (s: serializer p)
  (tag: the_asn1_tag a & asn1_value_int32_of_type a)
: parser (weak_kind_of_type a) (refine_with_tag (parser_tag_of_asn1_envelop_tag_with a s) tag)

noextract
val serialize_asn1_envelop_tag_with
  (#k: parser_kind)
  (#t: Type0)
  (#p: parser k t)
  (a: asn1_tag_t)
  (s: serializer p)
  (tag: the_asn1_tag a & asn1_value_int32_of_type a)
: serializer (parse_asn1_envelop_tag_with a s tag)

// noextract
// let predicate_serialize_asn1_envelop_tag_with_unfold
//   (#k: parser_kind)
//   (#t: Type0)
//   (#p: parser k t)
//   (a: asn1_tag_t)
//   (s: serializer p)
//   (tag: the_asn1_tag a & asn1_value_int32_of_type a)
//   (value: refine_with_tag (parser_tag_of_asn1_envelop_tag_with a s) tag)
// : Type0
// = serialize
//     (serialize_fldata_strong s (v (snd tag)))
//     (synth_asn1_envelop_tag_with_inverse a s tag value)
//   == serialize (serialize_asn1_envelop_tag_with a s tag) value

val lemma_serialize_asn1_envelop_tag_with_unfold
  (#k: parser_kind)
  (#t: Type0)
  (#p: parser k t)
  (a: asn1_tag_t)
  (s: serializer p)
  (tag: the_asn1_tag a & asn1_value_int32_of_type a)
  (value: refine_with_tag (parser_tag_of_asn1_envelop_tag_with a s) tag)
: Lemma (
  serialize
    (serialize_fldata_strong s (v (snd tag)))
    (synth_asn1_envelop_tag_with_inverse a s tag value)
  == serialize (serialize_asn1_envelop_tag_with a s tag) value
)

noextract
val serialize_asn1_envelop_tag_with_weak
  (#k: parser_kind)
  (#t: Type0)
  (#p: parser k t)
  (a: asn1_tag_t)
  (s: serializer p)
  (tag: the_asn1_tag a & asn1_value_int32_of_type a)
: serializer (parse_asn1_envelop_tag_with_weak a s tag)

/// Specialized TLV parser/serializer
///
///
/
prims.fst.checked LowParse.Spec.FLData.fst.checked FStar.Seq.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Integers.fst.checked ASN1.Spec.Tag.fsti.checked ASN1.Spec.Length.fsti.checked ASN1.Spec.Base.fst.checked ASN1.Base.fst.checked
ASN1.Spec.Value.Envelop.fsti
a: ASN1.Base.asn1_tag_t -> LowParse.Spec.Base.parser_kind
ASN1.Base.asn1_tag_t LowParse.Spec.Combinators.and_then_kind ASN1.Spec.Tag.parse_asn1_tag_kind ASN1.Spec.Length.parse_asn1_length_kind_of_type ASN1.Base.weak_kind_of_type LowParse.Spec.Base.parser_kind
let parse_asn1_envelop_tag_with_TLV_kind (a: asn1_tag_t) : parser_kind =
  
(parse_asn1_tag_kind `and_then_kind` (parse_asn1_length_kind_of_type a))
`and_then_kind`
(weak_kind_of_type a)