val parser_tag_of_asn1_string
  (t: asn1_type { t == IA5_STRING \/ t == PRINTABLE_STRING \/ t == OCTET_STRING })
  (len_of_string: datatype_of_asn1_type t -> asn1_value_int32_of_type t)
  (x: datatype_of_asn1_type t)
: Tot (the_asn1_tag t `tuple2` asn1_value_int32_of_type t)
val parser_tag_of_asn1_string
  (t: asn1_type { t == IA5_STRING \/ t == PRINTABLE_STRING \/ t == OCTET_STRING })
  (len_of_string: datatype_of_asn1_type t -> asn1_value_int32_of_type t)
  (x: datatype_of_asn1_type t)
: Tot (the_asn1_tag t `tuple2` asn1_value_int32_of_type t)
let parser_tag_of_asn1_string t len_of_string x
= (t, len_of_string x)
module ASN1.Spec.Value.StringCombinator

open ASN1.Spec.Base
open LowParse.Spec.Bytes

open ASN1.Base
open ASN1.Spec.Tag
open ASN1.Spec.Length

open FStar.Integers

module B32 = FStar.Bytes

let parse_asn1_string t len_of_string filter_string synth_string prf len
= parse_flbytes (v len)
  `parse_filter`
  filter_string len
  `parse_synth`
  synth_string len

let serialize_asn1_string t len_of_string filter_string synth_string synth_string_inverse prf len
= serialize_synth
  (* p1 *) (parse_flbytes (v len)
            `parse_filter`
            filter_string len)
  (* f2 *) (synth_string len)
  (* s1 *) (serialize_flbytes (v len)
            `serialize_filter`
            filter_string len)
  (* g1 *) (synth_string_inverse len)
  (* Prf*) (prf)

let lemma_serialize_asn1_string_unfold t len_of_string filter_string synth_string synth_string_inverse prf len x
= serialize_synth_eq
  (* p1 *) (parse_flbytes (v len)
            `parse_filter`
            filter_string len)
  (* f2 *) (synth_string len)
  (* s1 *) (serialize_flbytes (v len)
            `serialize_filter`
            filter_string len)
  (* g1 *) (synth_string_inverse len)
  (* Prf*) (prf)
  (* in *) (x)

let lemma_serialize_asn1_string_size t len_of_string filter_string synth_string synth_string_inverse prf len x
= lemma_serialize_asn1_string_unfold t len_of_string filter_string synth_string synth_string_inverse prf len x
/
prims.fst.checked LowParse.Spec.Bytes.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Integers.fst.checked FStar.Bytes.fsti.checked ASN1.Spec.Tag.fsti.checked ASN1.Spec.Length.fsti.checked ASN1.Spec.Base.fst.checked ASN1.Base.fst.checked
ASN1.Spec.Value.StringCombinator.fst

    t:
      ASN1.Base.asn1_type
        { t == ASN1.Base.IA5_STRING \/ t == ASN1.Base.PRINTABLE_STRING \/
          t == ASN1.Base.OCTET_STRING } ->
    len_of_string: (_: ASN1.Base.datatype_of_asn1_type t -> ASN1.Base.asn1_value_int32_of_type t) ->
    x: ASN1.Base.datatype_of_asn1_type t
  -> ASN1.Base.the_asn1_tag t * ASN1.Base.asn1_value_int32_of_type t
ASN1.Base.asn1_type Prims.l_or Prims.eq2 ASN1.Base.asn1_tag_t ASN1.Base.IA5_STRING ASN1.Base.PRINTABLE_STRING ASN1.Base.OCTET_STRING ASN1.Base.datatype_of_asn1_type ASN1.Base.asn1_value_int32_of_type FStar.Pervasives.Native.Mktuple2 ASN1.Base.the_asn1_tag FStar.Pervasives.Native.tuple2
let parser_tag_of_asn1_string t len_of_string x =
  
(t, len_of_string x)