val serialize_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)
  (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 }))
  (synth_string_inverse: (len: asn1_value_int32_of_type t)
                         -> (x: datatype_of_asn1_type t { len_of_string x== len })
                         -> (s32: parse_filter_refine (filter_string len)
                                 { x == synth_string len s32 }))
  (prf: unit { forall len. synth_injective (synth_string len) })
  (len: asn1_value_int32_of_type t)
: serializer (parse_asn1_string t len_of_string filter_string synth_string prf len)
val serialize_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)
  (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 }))
  (synth_string_inverse: (len: asn1_value_int32_of_type t)
                         -> (x: datatype_of_asn1_type t { len_of_string x== len })
                         -> (s32: parse_filter_refine (filter_string len)
                                 { x == synth_string len s32 }))
  (prf: unit { forall len. synth_injective (synth_string len) })
  (len: asn1_value_int32_of_type t)
: serializer (parse_asn1_string t len_of_string filter_string synth_string prf 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)
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
/
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})) ->
    synth_string_inverse:
      (
            len: ASN1.Base.asn1_value_int32_of_type t ->
            x: ASN1.Base.datatype_of_asn1_type t {len_of_string x == len}
          -> s32:
            LowParse.Spec.Combinators.parse_filter_refine (filter_string len)
              {x == synth_string len s32}) ->
    prf:
      Prims.unit
        { forall (len: ASN1.Base.asn1_value_int32_of_type t).
            LowParse.Spec.Combinators.synth_injective (synth_string len) } ->
    len: ASN1.Base.asn1_value_int32_of_type t
  -> LowParse.Spec.Base.serializer (ASN1.Spec.Value.StringCombinator.parse_asn1_string t
          len_of_string
          filter_string
          synth_string
          prf
          len)
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 LowParse.Spec.Combinators.serialize_synth LowParse.Spec.Combinators.parse_filter_kind LowParse.Spec.Base.total_constant_size_parser_kind FStar.Integers.v FStar.Integers.Unsigned FStar.Integers.W32 FStar.Bytes.lbytes LowParse.Spec.Combinators.parse_filter LowParse.Spec.Bytes.parse_flbytes LowParse.Spec.Combinators.serialize_filter LowParse.Spec.Bytes.serialize_flbytes LowParse.Spec.Base.serializer ASN1.Spec.Value.StringCombinator.parse_asn1_string
let serialize_asn1_string t len_of_string filter_string synth_string synth_string_inverse prf len =
  
serialize_synth ((parse_flbytes (v len)) `parse_filter` (filter_string len))
  (synth_string len)
  ((serialize_flbytes (v len)) `serialize_filter` (filter_string len))
  (synth_string_inverse len)
  (prf)