val parse_asn1_ia5_string_TLV : LowParse.Spec.Base.parser (ASN1.Spec.Value.StringCombinator.parse_asn1_string_TLV_kind ASN1.Base.IA5_STRING
    )
  (ASN1.Base.datatype_of_asn1_type ASN1.Base.IA5_STRING)
let parse_asn1_ia5_string_TLV
= parse_asn1_string_TLV
    (IA5_STRING)
    (dfst)
    (filter_asn1_ia5_string)
    (synth_asn1_ia5_string)
    ()
module ASN1.Spec.Value.IA5_STRING

open ASN1.Spec.Base

open ASN1.Base
open ASN1.Spec.Value.StringCombinator

open FStar.Integers

module B32 = FStar.Bytes

let filter_asn1_ia5_string
  (len: asn1_value_int32_of_type IA5_STRING)
  (s32: B32.lbytes32 len)
: GTot (bool)
= let s = B32.reveal s32 in
  Seq.for_all valid_IA5_byte s

let synth_asn1_ia5_string
  (len: asn1_value_int32_of_type IA5_STRING)
  (s32: parse_filter_refine (filter_asn1_ia5_string len))
: GTot (value: datatype_of_asn1_type IA5_STRING{(dfst value) == len})
= (|len, s32|)

noextract inline_for_extraction
val synth_asn1_ia5_string_inverse
  (len: asn1_value_int32_of_type IA5_STRING)
  (value: datatype_of_asn1_type IA5_STRING{(dfst value) == len})
: Tot (s32: parse_filter_refine (filter_asn1_ia5_string len)
             { value == synth_asn1_ia5_string len s32 })

let parse_asn1_ia5_string
= parse_asn1_string
    (IA5_STRING)
    (dfst)
    (filter_asn1_ia5_string)
    (synth_asn1_ia5_string)
    ()

let serialize_asn1_ia5_string
= serialize_asn1_string
    (IA5_STRING)
    (dfst)
    (filter_asn1_ia5_string)
    (synth_asn1_ia5_string)
    (synth_asn1_ia5_string_inverse)
    ()

let lemma_serialize_asn1_ia5_string_unfold
= lemma_serialize_asn1_string_unfold
    (IA5_STRING)
    (dfst)
    (filter_asn1_ia5_string)
    (synth_asn1_ia5_string)
    (synth_asn1_ia5_string_inverse)
    ()

let lemma_serialize_asn1_ia5_string_size
= lemma_serialize_asn1_string_size
    (IA5_STRING)
    (dfst)
    (filter_asn1_ia5_string)
    (synth_asn1_ia5_string)
    (synth_asn1_ia5_string_inverse)
    ()

inline_for_extraction noextract
let parse_asn1_ia5_string_TLV_kind = parse_asn1_string_TLV_kind IA5_STRING
/
prims.fst.checked FStar.Seq.fst.checked FStar.Pervasives.fsti.checked FStar.Integers.fst.checked FStar.Bytes.fsti.checked ASN1.Spec.Value.StringCombinator.fsti.checked ASN1.Spec.Base.fst.checked ASN1.Base.fst.checked
ASN1.Spec.Value.IA5_STRING.fsti
LowParse.Spec.Base.parser (ASN1.Spec.Value.StringCombinator.parse_asn1_string_TLV_kind ASN1.Base.IA5_STRING
    )
  (ASN1.Base.datatype_of_asn1_type ASN1.Base.IA5_STRING)
ASN1.Spec.Value.StringCombinator.parse_asn1_string_TLV ASN1.Base.IA5_STRING FStar.Pervasives.dfst ASN1.Base.asn1_value_int32_of_type ASN1.Base.character_string_lbytes32 ASN1.Spec.Value.IA5_STRING.filter_asn1_ia5_string ASN1.Spec.Value.IA5_STRING.synth_asn1_ia5_string
let parse_asn1_ia5_string_TLV =
  
parse_asn1_string_TLV (IA5_STRING) (dfst) (filter_asn1_ia5_string) (synth_asn1_ia5_string) ()