val serialize32_RDN_payload_backwards
  (oid: x509_RDN_attribute_oid)
  (t: directory_string_type)
  (lb: asn1_int32)
  (ub: asn1_value_int32_of_type t { lb <= ub })
: serializer32_backwards (serialize_RDN_payload oid t lb ub)
val serialize32_RDN_payload_backwards
  (oid: x509_RDN_attribute_oid)
  (t: directory_string_type)
  (lb: asn1_int32)
  (ub: asn1_value_int32_of_type t { lb <= ub })
: serializer32_backwards (serialize_RDN_payload oid t lb ub)
let serialize32_RDN_payload_backwards oid t lb ub
= (oid `serialize32_envelop_OID_with_backwards`
   serialize32_asn1_character_string_with_character_bound_backwards t lb ub)
module X509.BasicFields.RelativeDistinguishedName

open LowParse.Low.Base

open ASN1.Spec
open ASN1.Low

open X509.Base

open FStar.Integers

#set-options "--z3rlimit 32 --fuel 0 --ifuel 0 --using_facts_from '* -FStar.Tactics -FStar.Reflection'"

(*
 *   Name ::= CHOICE { -- only one possibility for now --
 *     rdnSequence  RDNSequence }
 *
 *   RDNSequence ::= SEQUENCE OF RelativeDistinguishedName
 *
 *   RelativeDistinguishedName ::=
 *     SET SIZE (1..MAX) OF AttributeTypeAndValue
 *
 *   AttributeTypeAndValue ::= SEQUENCE {
 *     type     AttributeType,
 *     value    AttributeValue }
 *
 *   AttributeType ::= OBJECT IDENTIFIER
 *
 *   AttributeValue ::= ANY -- DEFINED BY AttributeType
 *
 *   DirectoryString ::= CHOICE {
 *         teletexString           TeletexString (SIZE (1..MAX)),
 *         printableString         PrintableString (SIZE (1..MAX)),
 *         universalString         UniversalString (SIZE (1..MAX)),
 *         utf8String              UTF8String (SIZE (1..MAX)),
 *         bmpString               BMPString (SIZE (1..MAX)) }
 *)

// let directory_string_value
//   (t: directory_string_type)
// = datatype_of_asn1_type t

// type x509_RDN_payload_t =
// | RDN_CN          : t: directory_string_type -> directory_string_value t -> x509_RDN_payload_t
// | RDN_COUNTRY     : t: directory_string_type -> directory_string_value t -> x509_RDN_payload_t
// | RDN_ORGANIZATION: t: directory_string_type -> directory_string_value t -> x509_RDN_payload_t

// #push-options "--fuel 0 --ifuel 1"
// let oid_of_RDN
//   (rdn: x509_RDN_payload_t)
// : Tot (x509_RDN_attribute_oid)
// = match rdn with
//   | RDN_CN           _ _ -> OID_AT_CN
//   | RDN_COUNTRY      _ _ -> OID_AT_COUNTRY
//   | RDN_ORGANIZATION _ _ -> OID_AT_ORGANIZATION

// let asn1_type_of_RDN
//   (rdn: x509_RDN_payload_t)
// : Tot (directory_string_type)
// = match rdn with
//   | RDN_CN           t _ -> t
//   | RDN_COUNTRY      t _ -> t
//   | RDN_ORGANIZATION t _ -> t
// #pop-options
/
X509.Base.fst.checked prims.fst.checked LowParse.Low.Base.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Integers.fst.checked ASN1.Spec.fst.checked ASN1.Low.fst.checked
X509.BasicFields.RelativeDistinguishedName.fst

    oid: X509.BasicFields.RelativeDistinguishedName.x509_RDN_attribute_oid ->
    t: X509.BasicFields.RelativeDistinguishedName.directory_string_type ->
    lb: ASN1.Base.asn1_int32 ->
    ub: ASN1.Base.asn1_value_int32_of_type t {lb <= ub}
  -> ASN1.Low.Base.serializer32_backwards (X509.BasicFields.RelativeDistinguishedName.serialize_RDN_payload
          oid
          t
          lb
          ub)
X509.BasicFields.RelativeDistinguishedName.x509_RDN_attribute_oid X509.BasicFields.RelativeDistinguishedName.directory_string_type ASN1.Base.asn1_int32 ASN1.Base.asn1_value_int32_of_type Prims.b2t FStar.Integers.op_Less_Equals FStar.Integers.Unsigned FStar.Integers.W32 ASN1.Low.Value.OID.serialize32_envelop_OID_with_backwards ASN1.Spec.Value.StringCombinator.parse_asn1_string_TLV_kind ASN1.Spec.Value.StringCombinator.asn1_string_with_character_bound_t ASN1.Spec.Value.CharacterString.count_character ASN1.Spec.Value.CharacterString.parse_asn1_character_string_with_character_bound ASN1.Spec.Value.CharacterString.serialize_asn1_character_string_with_character_bound ASN1.Low.Value.CharacterString.serialize32_asn1_character_string_with_character_bound_backwards ASN1.Low.Base.serializer32_backwards LowParse.Spec.Combinators.and_then_kind LowParse.Spec.Combinators.parse_filter_kind ASN1.Spec.Value.OID.parse_asn1_oid_TLV_kind X509.BasicFields.RelativeDistinguishedName.x509_RDN_payload_t X509.BasicFields.RelativeDistinguishedName.parse_RDN_payload X509.BasicFields.RelativeDistinguishedName.serialize_RDN_payload
let serialize32_RDN_payload_backwards oid t lb ub =
  
(oid
  `serialize32_envelop_OID_with_backwards`
  (serialize32_asn1_character_string_with_character_bound_backwards t lb ub))