val serialize_asn1_character_string_with_character_bound
      (t: character_string_type)
      (lb: asn1_value_int32_of_type t)
      (ub: asn1_value_int32_of_type t {lb <= ub})
    : serializer (parse_asn1_character_string_with_character_bound t lb ub)
val serialize_asn1_character_string_with_character_bound
      (t: character_string_type)
      (lb: asn1_value_int32_of_type t)
      (ub: asn1_value_int32_of_type t {lb <= ub})
    : serializer (parse_asn1_character_string_with_character_bound t lb ub)
let serialize_asn1_character_string_with_character_bound
  (t: character_string_type)
  (lb: asn1_value_int32_of_type t)
  (ub: asn1_value_int32_of_type t { lb <= ub })
: serializer (parse_asn1_character_string_with_character_bound t lb ub)
= match t with
  | IA5_STRING -> assert_norm (count_ia5_character == count_character IA5_STRING);
                  serialize_asn1_ia5_string_TLV_with_character_bound lb ub
  | PRINTABLE_STRING
               -> assert_norm (count_printable_character == count_character PRINTABLE_STRING);
                  serialize_asn1_printable_string_TLV_with_character_bound lb ub
module ASN1.Spec.Value.CharacterString

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

open ASN1.Base
open ASN1.Spec.Tag
open ASN1.Spec.Length
include ASN1.Spec.Value.StringCombinator
include ASN1.Spec.Value.IA5_STRING
include ASN1.Spec.Value.PRINTABLE_STRING

open FStar.Integers

module B32 = FStar.Bytes

#set-options "--z3rlimit 32 --fuel 0 --ifuel 0"

(* ZT: I think we can leave this module exposed. *)

noextract inline_for_extraction
let len_of_character_string
  (t: character_string_type)
  (x: datatype_of_asn1_type t)
: Tot (asn1_value_int32_of_type t)
= match t with
  | IA5_STRING -> dfst (x <: datatype_of_asn1_type IA5_STRING)
  | PRINTABLE_STRING -> dfst (x <: datatype_of_asn1_type PRINTABLE_STRING)

let filter_character_string
  (t: character_string_type)
  (len: asn1_value_int32_of_type t)
  (s32: B32.lbytes32 len)
: GTot (bool)
= match t with
  | IA5_STRING -> filter_asn1_ia5_string len s32
  | PRINTABLE_STRING -> filter_asn1_printable_string len s32

let synth_character_string
  (t: character_string_type)
  (len: asn1_value_int32_of_type t)
  (s32: parse_filter_refine (filter_character_string t len))
: GTot (x: datatype_of_asn1_type t{ len_of_character_string t x == len })
= match t with
  | IA5_STRING -> synth_asn1_ia5_string len s32
  | PRINTABLE_STRING -> synth_asn1_printable_string len s32

noextract inline_for_extraction
let synth_character_string_inverse
  (t: character_string_type)
  (len: asn1_value_int32_of_type t)
  (x: datatype_of_asn1_type t{ len_of_character_string t x == len })
: Tot (s32: parse_filter_refine (filter_character_string t len)
            { x == synth_character_string t len s32 })
= match t with
  | IA5_STRING -> synth_asn1_ia5_string_inverse len x
  | PRINTABLE_STRING -> synth_asn1_printable_string_inverse len x

noextract
let string_prf
  (t: character_string_type)
= match t with
  | IA5_STRING -> ()
  | PRINTABLE_STRING -> ()

noextract inline_for_extraction
let count_character
  (t: character_string_type)
  (x: datatype_of_asn1_type t)
: Tot (asn1_int32)
= match t with
  | IA5_STRING -> count_ia5_character x
  | PRINTABLE_STRING -> count_printable_character x

let parse_asn1_character_string
  (t: character_string_type)
: parser (parse_asn1_string_TLV_kind t) (datatype_of_asn1_type t)
= match t with
  | IA5_STRING -> parse_asn1_ia5_string_TLV
  | PRINTABLE_STRING -> parse_asn1_printable_string_TLV

let serialize_asn1_character_string
  (t: character_string_type)
: serializer (parse_asn1_character_string t)
= match t with
  | IA5_STRING -> serialize_asn1_ia5_string_TLV
  | PRINTABLE_STRING -> serialize_asn1_printable_string_TLV

let parse_asn1_character_string_with_character_bound
  (t: character_string_type)
  (lb: asn1_value_int32_of_type t)
  (ub: asn1_value_int32_of_type t { lb <= ub })
: parser (parse_asn1_string_TLV_kind t) (asn1_string_with_character_bound_t t (count_character t) lb ub)
= match t with
  | IA5_STRING -> assert_norm (count_ia5_character == count_character IA5_STRING);
                  parse_asn1_ia5_string_TLV_with_character_bound lb ub
  | PRINTABLE_STRING
               -> assert_norm (count_printable_character == count_character PRINTABLE_STRING);
                  parse_asn1_printable_string_TLV_with_character_bound lb ub
/
prims.fst.checked LowParse.Spec.Bytes.fst.checked FStar.Pervasives.fsti.checked FStar.Integers.fst.checked FStar.Bytes.fsti.checked ASN1.Spec.Value.StringCombinator.fsti.checked ASN1.Spec.Value.PRINTABLE_STRING.fsti.checked ASN1.Spec.Value.IA5_STRING.fsti.checked ASN1.Spec.Tag.fsti.checked ASN1.Spec.Length.fsti.checked ASN1.Spec.Base.fst.checked ASN1.Base.fst.checked
ASN1.Spec.Value.CharacterString.fst

    t: ASN1.Base.character_string_type ->
    lb: ASN1.Base.asn1_value_int32_of_type t ->
    ub: ASN1.Base.asn1_value_int32_of_type t {lb <= ub}
  -> LowParse.Spec.Base.serializer (ASN1.Spec.Value.CharacterString.parse_asn1_character_string_with_character_bound
          t
          lb
          ub)
ASN1.Base.character_string_type ASN1.Base.asn1_value_int32_of_type Prims.b2t FStar.Integers.op_Less_Equals FStar.Integers.Unsigned FStar.Integers.W32 ASN1.Spec.Value.IA5_STRING.serialize_asn1_ia5_string_TLV_with_character_bound Prims.unit FStar.Pervasives.assert_norm Prims.eq2 ASN1.Base.datatype_of_asn1_type ASN1.Base.IA5_STRING ASN1.Base.asn1_int32 ASN1.Spec.Value.IA5_STRING.count_ia5_character ASN1.Spec.Value.CharacterString.count_character ASN1.Spec.Value.PRINTABLE_STRING.serialize_asn1_printable_string_TLV_with_character_bound ASN1.Base.PRINTABLE_STRING ASN1.Spec.Value.PRINTABLE_STRING.count_printable_character LowParse.Spec.Base.serializer ASN1.Spec.Value.StringCombinator.parse_asn1_string_TLV_kind ASN1.Spec.Value.StringCombinator.asn1_string_with_character_bound_t ASN1.Spec.Value.CharacterString.parse_asn1_character_string_with_character_bound
let serialize_asn1_character_string_with_character_bound
      (t: character_string_type)
      (lb: asn1_value_int32_of_type t)
      (ub: asn1_value_int32_of_type t {lb <= ub})
    : serializer (parse_asn1_character_string_with_character_bound t lb ub) =
  
match t with
| IA5_STRING ->
  assert_norm (count_ia5_character == count_character IA5_STRING);
  serialize_asn1_ia5_string_TLV_with_character_bound lb ub
| PRINTABLE_STRING ->
  assert_norm (count_printable_character == count_character PRINTABLE_STRING);
  serialize_asn1_printable_string_TLV_with_character_bound lb ub