val lemma_serialize_asn1_string_TLV_unfold
  (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) })
  (x: datatype_of_asn1_type t)
: Lemma (
  predicate_serialize_asn1_string_TLV_unfold t len_of_string filter_string synth_string synth_string_inverse prf x
)
val lemma_serialize_asn1_string_TLV_unfold
  (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) })
  (x: datatype_of_asn1_type t)
: Lemma (
  predicate_serialize_asn1_string_TLV_unfold t len_of_string filter_string synth_string synth_string_inverse prf x
)
let lemma_serialize_asn1_string_TLV_unfold t len_of_string filter_string synth_string synth_string_inverse prf x
= serialize_nondep_then_eq
  (* s1 *) (serialize_asn1_tag_of_type t)
  (* s2 *) (serialize_asn1_length_of_type t)
  (* in *) (parser_tag_of_asn1_string t len_of_string x);
  lemma_serialize_asn1_string_V_unfold t len_of_string filter_string synth_string synth_string_inverse prf (parser_tag_of_asn1_string t len_of_string x) x;
  serialize_tagged_union_eq
  (* st *) (serialize_asn1_tag_of_type t
            `serialize_nondep_then`
            serialize_asn1_length_of_type t)
  (* tg *) (parser_tag_of_asn1_string t len_of_string)
  (* s  *) (serialize_asn1_string_V t len_of_string filter_string synth_string synth_string_inverse prf)
  (* in *) (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

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'

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

let serialize_asn1_string_V t len_of_string filter_string synth_string synth_string_inverse prf tag
= serialize_synth
  (* p1 *) (weak_kind_of_type t
            `weaken`
            parse_asn1_string t len_of_string filter_string synth_string prf (snd tag))
  (* f2 *) (synth_asn1_string_V t len_of_string tag)
  (* s1 *) (weak_kind_of_type t
            `serialize_weaken`
            serialize_asn1_string t len_of_string filter_string synth_string synth_string_inverse prf (snd tag))
  (* g1 *) (synth_asn1_string_V_inverse t len_of_string tag)
  (* prf*) (prf)

let lemma_serialize_asn1_string_V_unfold
  (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) })
  (tag: the_asn1_tag t `tuple2` asn1_value_int32_of_type t)
  (x: refine_with_tag (parser_tag_of_asn1_string t len_of_string) tag)
: Lemma (
  serialize (serialize_asn1_string_V t len_of_string filter_string synth_string synth_string_inverse prf tag) x ==
  serialize (serialize_asn1_string t len_of_string filter_string synth_string synth_string_inverse prf (snd tag)) x
)
= serialize_synth_eq
  (* p1 *) (weak_kind_of_type t
            `weaken`
            parse_asn1_string t len_of_string filter_string synth_string prf (snd tag))
  (* f2 *) (synth_asn1_string_V t len_of_string tag)
  (* s1 *) (weak_kind_of_type t
            `serialize_weaken`
            serialize_asn1_string t len_of_string filter_string synth_string synth_string_inverse prf (snd tag))
  (* g1 *) (synth_asn1_string_V_inverse t len_of_string tag)
  (* prf*) (prf)
  (* in *) (x)

let parse_asn1_string_TLV t len_of_string filter_string synth_string prf
= parse_tagged_union
  (* pt *) (parse_asn1_tag_of_type t
            `nondep_then`
            parse_asn1_length_of_type t)
  (* tg *) (parser_tag_of_asn1_string t len_of_string)
  (* p  *) (parse_asn1_string_V t len_of_string filter_string synth_string prf)

let serialize_asn1_string_TLV t len_of_string filter_string synth_string synth_string_inverse prf
= serialize_tagged_union
  (* st *) (serialize_asn1_tag_of_type t
            `serialize_nondep_then`
            serialize_asn1_length_of_type t)
  (* tg *) (parser_tag_of_asn1_string t len_of_string)
  (* s  *) (serialize_asn1_string_V t len_of_string filter_string synth_string synth_string_inverse prf)
/
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) } ->
    x: ASN1.Base.datatype_of_asn1_type t
  -> FStar.Pervasives.Lemma
    (ensures
      ASN1.Spec.Value.StringCombinator.predicate_serialize_asn1_string_TLV_unfold t
        len_of_string
        filter_string
        synth_string
        synth_string_inverse
        prf
        x)
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_tagged_union_eq LowParse.Spec.Combinators.and_then_kind ASN1.Spec.Tag.parse_asn1_tag_kind ASN1.Spec.Length.parse_asn1_length_kind_of_type FStar.Pervasives.Native.tuple2 ASN1.Base.the_asn1_tag LowParse.Spec.Combinators.nondep_then ASN1.Spec.Tag.parse_asn1_tag_of_type ASN1.Spec.Length.parse_asn1_length_of_type LowParse.Spec.Combinators.serialize_nondep_then ASN1.Spec.Tag.serialize_asn1_tag_of_type ASN1.Spec.Length.serialize_asn1_length_of_type ASN1.Spec.Value.StringCombinator.parser_tag_of_asn1_string ASN1.Base.weak_kind_of_type ASN1.Spec.Value.StringCombinator.parse_asn1_string_V ASN1.Spec.Value.StringCombinator.serialize_asn1_string_V ASN1.Spec.Value.StringCombinator.lemma_serialize_asn1_string_V_unfold LowParse.Spec.Combinators.serialize_nondep_then_eq
let lemma_serialize_asn1_string_TLV_unfold
      t
      len_of_string
      filter_string
      synth_string
      synth_string_inverse
      prf
      x
     =
  
serialize_nondep_then_eq (serialize_asn1_tag_of_type t)
  (serialize_asn1_length_of_type t)
  (parser_tag_of_asn1_string t len_of_string x);
lemma_serialize_asn1_string_V_unfold t
  len_of_string
  filter_string
  synth_string
  synth_string_inverse
  prf
  (parser_tag_of_asn1_string t len_of_string x)
  x;
serialize_tagged_union_eq ((serialize_asn1_tag_of_type t)
    `serialize_nondep_then`
    (serialize_asn1_length_of_type t))
  (parser_tag_of_asn1_string t len_of_string)
  (serialize_asn1_string_V t len_of_string filter_string synth_string synth_string_inverse prf)
  (x)