val parse_asn1_tag_kind : LowParse.Spec.Base.parser_kind
let parse_asn1_tag_kind = strong_parser_kind 1 1 None
module ASN1.Spec.Tag

open ASN1.Spec.Base
open LowParse.Spec.Int

open ASN1.Base

(* NOTE: This module defines:
         1) the _generic_ ASN1 Tag parser/serializer for _any_ ASN1 Tag
         2) the _specialized_ ASN1 Tag parser/serializer for a _given_ ASN1 Tag

         And each part is organized as:
         1) Aux (ghost) functions with prefix `filter_` to filter out invalid input bytes
         2) Aux (ghost) functions with prefix `synth_` to decode the valid input bytes/synthesize
            ASN1 tags. These functions are injective.
         3) Aux (ghost) functions with prefix `synth_` and suffix `_inverse` to encode ASN1 tags to
            bytes. These functions are the inverse of corresponding synth functions.
         4) Functions with the prefix `parse_` are parsers constructed using parser combinators and
            aux functions.
         5) Functions with the prefix `serialize_` are serializers constructed using serializer
            combinators and aux functions.
         6) Lemma with suffix `_unfold` reveals the computation of parser/serialzier.
         7) Lemma with suffix `_size` reveals the length of a serialization.
*)


/////////////////////////////////////////
////   Generic ASN1 Tag Parser
/////////////////////////////////////////

/// filter valid input bytes

val filter_asn1_tag
  (b: byte)
: GTot bool

/// decode input bytes

val synth_asn1_tag
  (b: parse_filter_refine filter_asn1_tag)
: GTot asn1_tag_t

/// encode input bytes

val synth_asn1_tag_inverse
  (a: asn1_tag_t)
: GTot (b: parse_filter_refine filter_asn1_tag{a == synth_asn1_tag b})
/
prims.fst.checked LowParse.Spec.Int.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.fsti.checked ASN1.Spec.Base.fst.checked ASN1.Base.fst.checked
ASN1.Spec.Tag.fsti
LowParse.Spec.Base.parser_kind
LowParse.Spec.Base.strong_parser_kind FStar.Pervasives.Native.None LowParse.Spec.Base.parser_kind_metadata_some
let parse_asn1_tag_kind =
  
strong_parser_kind 1 1 None