val predicate_serialize_asn1_envelop_tag_with_TLV_unfold
      (#k: parser_kind)
      (#t: Type0)
      (#p: parser k t)
      (a: asn1_tag_t)
      (s: serializer p)
      (value: inbound_envelop_tag_with_value_of a s)
    : Type0
val predicate_serialize_asn1_envelop_tag_with_TLV_unfold
      (#k: parser_kind)
      (#t: Type0)
      (#p: parser k t)
      (a: asn1_tag_t)
      (s: serializer p)
      (value: inbound_envelop_tag_with_value_of a s)
    : Type0
let predicate_serialize_asn1_envelop_tag_with_TLV_unfold
  (#k: parser_kind)
  (#t: Type0)
  (#p: parser k t)
  (a: asn1_tag_t)
  (s: serializer p)
  (value: inbound_envelop_tag_with_value_of a s)
: Type0
= serialize (serialize_asn1_envelop_tag_with_TLV a s) value ==
  serialize (serialize_asn1_tag_of_type a) a
  `Seq.append`
  serialize (serialize_asn1_length_of_type a) (u (length_of_opaque_serialization (serialize_asn1_envelop_tag_with a s (parser_tag_of_asn1_envelop_tag_with a s value)) value))
  `Seq.append`
  serialize (serialize_asn1_envelop_tag_with a s (parser_tag_of_asn1_envelop_tag_with a s value)) value
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
///
///

inline_for_extraction noextract
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

noextract
val parse_asn1_envelop_tag_with_TLV
  (#k: parser_kind)
  (#t: Type0)
  (#p: parser k t)
  (a: asn1_tag_t)
  (s: serializer p)
: parser (parse_asn1_envelop_tag_with_TLV_kind a) (inbound_envelop_tag_with_value_of a s)

noextract
val serialize_asn1_envelop_tag_with_TLV
  (#k: parser_kind)
  (#t: Type0)
  (#p: parser k t)
  (a: asn1_tag_t)
  (s: serializer p)
: (serializer (parse_asn1_envelop_tag_with_TLV a s))
/
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 ->
    s: LowParse.Spec.Base.serializer p ->
    value: ASN1.Spec.Value.Envelop.inbound_envelop_tag_with_value_of a s
  -> Type0
LowParse.Spec.Base.parser_kind LowParse.Spec.Base.parser ASN1.Base.asn1_tag_t LowParse.Spec.Base.serializer ASN1.Spec.Value.Envelop.inbound_envelop_tag_with_value_of Prims.eq2 FStar.Seq.Base.seq LowParse.Bytes.byte LowParse.Spec.Base.serialize ASN1.Spec.Value.Envelop.parse_asn1_envelop_tag_with_TLV_kind ASN1.Spec.Value.Envelop.parse_asn1_envelop_tag_with_TLV ASN1.Spec.Value.Envelop.serialize_asn1_envelop_tag_with_TLV FStar.Seq.Base.append ASN1.Spec.Tag.parse_asn1_tag_kind ASN1.Base.the_asn1_tag ASN1.Spec.Tag.parse_asn1_tag_of_type ASN1.Spec.Tag.serialize_asn1_tag_of_type ASN1.Spec.Length.parse_asn1_length_kind_of_type ASN1.Base.asn1_value_int32_of_type ASN1.Spec.Length.parse_asn1_length_of_type ASN1.Spec.Length.serialize_asn1_length_of_type FStar.Integers.u FStar.Integers.Unsigned FStar.Integers.W32 ASN1.Spec.Base.length_of_opaque_serialization LowParse.Spec.Base.refine_with_tag FStar.Pervasives.Native.tuple2 ASN1.Spec.Value.Envelop.parser_tag_of_asn1_envelop_tag_with LowParse.Spec.FLData.parse_fldata_kind FStar.Integers.v FStar.Pervasives.Native.snd ASN1.Spec.Value.Envelop.parse_asn1_envelop_tag_with ASN1.Spec.Value.Envelop.serialize_asn1_envelop_tag_with
let predicate_serialize_asn1_envelop_tag_with_TLV_unfold
      (#k: parser_kind)
      (#t: Type0)
      (#p: parser k t)
      (a: asn1_tag_t)
      (s: serializer p)
      (value: inbound_envelop_tag_with_value_of a s)
    : Type0 =
  
serialize (serialize_asn1_envelop_tag_with_TLV a s) value ==
((serialize (serialize_asn1_tag_of_type a) a)
  `Seq.append`
  (serialize (serialize_asn1_length_of_type a)
      (u (length_of_opaque_serialization (serialize_asn1_envelop_tag_with a
                  s
                  (parser_tag_of_asn1_envelop_tag_with a s value))
              value))))
`Seq.append`
(serialize (serialize_asn1_envelop_tag_with a s (parser_tag_of_asn1_envelop_tag_with a s value))
    value)