val parse_asn1_string_V
  (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)
  (filter_string: (len: asn1_value_int32_of_type t)
                  -> (s32: B32.lbytes32 len)
                  -> GTot (bool))
  (synth_string: (len: asn1_value_int32_of_type t)
                       -> (s32: parse_filter_refine (filter_string len))
                       -> GTot (x: datatype_of_asn1_type t
                                  { len_of_string x== len }))
  (prf: unit { forall len. synth_injective (synth_string len) })
  (tag: the_asn1_tag t `tuple2` asn1_value_int32_of_type t)
: parser (weak_kind_of_type t) (refine_with_tag (parser_tag_of_asn1_string t len_of_string) tag)
val parse_asn1_string_V
  (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)
  (filter_string: (len: asn1_value_int32_of_type t)
                  -> (s32: B32.lbytes32 len)
                  -> GTot (bool))
  (synth_string: (len: asn1_value_int32_of_type t)
                       -> (s32: parse_filter_refine (filter_string len))
                       -> GTot (x: datatype_of_asn1_type t
                                  { len_of_string x== len }))
  (prf: unit { forall len. synth_injective (synth_string len) })
  (tag: the_asn1_tag t `tuple2` asn1_value_int32_of_type t)
: parser (weak_kind_of_type t) (refine_with_tag (parser_tag_of_asn1_string t len_of_string) tag)
let parse_asn1_string_V t len_of_string filter_string synth_string prf tag
= weak_kind_of_type t
  `weaken`
  parse_asn1_string t len_of_string filter_string synth_string prf (snd tag)
  `parse_synth`
  synth_asn1_string_V t len_of_string tag
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

let parser_tag_of_asn1_string t len_of_string x
= (t, len_of_string x)

let synth_asn1_string_V t len_of_string tag value
= value

noextract inline_for_extraction
let synth_asn1_string_V_inverse t len_of_string tag value'
= value'
/
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) ->
    filter_string:
      (len: ASN1.Base.asn1_value_int32_of_type t -> s32: FStar.Bytes.lbytes32 len
          -> Prims.GTot Prims.bool) ->
    synth_string:
      (
            len: ASN1.Base.asn1_value_int32_of_type t ->
            s32: LowParse.Spec.Combinators.parse_filter_refine (filter_string len)
          -> Prims.GTot (x: ASN1.Base.datatype_of_asn1_type t {len_of_string x == len})) ->
    prf:
      Prims.unit
        { forall (len: ASN1.Base.asn1_value_int32_of_type t).
            LowParse.Spec.Combinators.synth_injective (synth_string len) } ->
    tag: (ASN1.Base.the_asn1_tag t * ASN1.Base.asn1_value_int32_of_type t)
  -> LowParse.Spec.Base.parser (ASN1.Base.weak_kind_of_type t)
      (LowParse.Spec.Base.refine_with_tag (ASN1.Spec.Value.StringCombinator.parser_tag_of_asn1_string
              t
              len_of_string)
          tag)
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.Bytes.lbytes32 Prims.bool LowParse.Spec.Combinators.parse_filter_refine Prims.unit Prims.l_Forall LowParse.Spec.Combinators.synth_injective FStar.Pervasives.Native.tuple2 ASN1.Base.the_asn1_tag LowParse.Spec.Combinators.parse_synth ASN1.Base.weak_kind_of_type FStar.Pervasives.Native.snd LowParse.Spec.Base.refine_with_tag ASN1.Spec.Value.StringCombinator.parser_tag_of_asn1_string LowParse.Spec.Base.weaken LowParse.Spec.Combinators.parse_filter_kind LowParse.Spec.Base.total_constant_size_parser_kind FStar.Integers.v FStar.Integers.Unsigned FStar.Integers.W32 ASN1.Spec.Value.StringCombinator.parse_asn1_string ASN1.Spec.Value.StringCombinator.synth_asn1_string_V LowParse.Spec.Base.parser
let parse_asn1_string_V t len_of_string filter_string synth_string prf tag =
  
((weak_kind_of_type t)
  `weaken`
  (parse_asn1_string t len_of_string filter_string synth_string prf (snd tag)))
`parse_synth`
(synth_asn1_string_V t len_of_string tag)