val serialize32_asn1_character_string_with_character_bound_backwards
      (t: character_string_type)
      (lb: asn1_value_int32_of_type t)
      (ub: asn1_value_int32_of_type t {lb <= ub})
    : serializer32_backwards (serialize_asn1_character_string_with_character_bound t lb ub)
val serialize32_asn1_character_string_with_character_bound_backwards
      (t: character_string_type)
      (lb: asn1_value_int32_of_type t)
      (ub: asn1_value_int32_of_type t {lb <= ub})
    : serializer32_backwards (serialize_asn1_character_string_with_character_bound t lb ub)
let serialize32_asn1_character_string_with_character_bound_backwards
  (t: character_string_type)
  (lb: asn1_value_int32_of_type t)
  (ub: asn1_value_int32_of_type t { lb <= ub })
: serializer32_backwards (serialize_asn1_character_string_with_character_bound t lb ub)
= match t with
  | IA5_STRING -> assert_norm (count_ia5_character == count_character IA5_STRING);
                  serialize32_asn1_ia5_string_TLV_with_character_bound_backwards lb ub
  | PRINTABLE_STRING
               -> assert_norm (count_printable_character == count_character PRINTABLE_STRING);
                  serialize32_asn1_printable_string_TLV_with_character_bound_backwards lb ub
module ASN1.Low.Value.CharacterString

open ASN1.Low.Base
open LowParse.Low.Bytes

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

open FStar.Integers

module B32 = FStar.Bytes
/
prims.fst.checked LowParse.Low.Bytes.fst.checked FStar.Pervasives.fsti.checked FStar.Integers.fst.checked FStar.Bytes.fsti.checked ASN1.Spec.Value.CharacterString.fst.checked ASN1.Low.Value.StringCombinator.fsti.checked ASN1.Low.Value.PRINTABLE_STRING.fsti.checked ASN1.Low.Value.IA5_STRING.fsti.checked ASN1.Low.Tag.fsti.checked ASN1.Low.Length.fsti.checked ASN1.Low.Base.fst.checked ASN1.Base.fst.checked
ASN1.Low.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}
  -> ASN1.Low.Base.serializer32_backwards (ASN1.Spec.Value.CharacterString.serialize_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.Low.Value.IA5_STRING.serialize32_asn1_ia5_string_TLV_with_character_bound_backwards 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.Low.Value.PRINTABLE_STRING.serialize32_asn1_printable_string_TLV_with_character_bound_backwards ASN1.Base.PRINTABLE_STRING ASN1.Spec.Value.PRINTABLE_STRING.count_printable_character ASN1.Low.Base.serializer32_backwards 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 ASN1.Spec.Value.CharacterString.serialize_asn1_character_string_with_character_bound
let serialize32_asn1_character_string_with_character_bound_backwards
      (t: character_string_type)
      (lb: asn1_value_int32_of_type t)
      (ub: asn1_value_int32_of_type t {lb <= ub})
    : serializer32_backwards (serialize_asn1_character_string_with_character_bound t lb ub) =
  
match t with
| IA5_STRING ->
  assert_norm (count_ia5_character == count_character IA5_STRING);
  serialize32_asn1_ia5_string_TLV_with_character_bound_backwards lb ub
| PRINTABLE_STRING ->
  assert_norm (count_printable_character == count_character PRINTABLE_STRING);
  serialize32_asn1_printable_string_TLV_with_character_bound_backwards lb ub