val parse_RDN_x520_attribute
  (t: x520_attribute_t)
  (string_t: directory_string_type { ((t == COUNTRY) ==> (string_t == PRINTABLE_STRING)) })
: parser (parse_asn1_envelop_tag_with_TLV_kind (SET)) (x509_RDN_x520_attribute_t t string_t)
val parse_RDN_x520_attribute
  (t: x520_attribute_t)
  (string_t: directory_string_type { ((t == COUNTRY) ==> (string_t == PRINTABLE_STRING)) })
: parser (parse_asn1_envelop_tag_with_TLV_kind (SET)) (x509_RDN_x520_attribute_t t string_t)
let parse_RDN_x520_attribute t string_t
= (x509_RDN_x520_attribute_t t string_t)
  `coerce_parser`
  (parse_RDN (x520_attribute_oid t) (string_t) (x520_attribute_lb t) (x520_attribute_ub t))
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

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)

let parse_RDN oid t lb ub
= (x509_RDN_t oid t lb ub)
  `coerce_parser`
  (SET `parse_asn1_envelop_tag_with_TLV`
  (**) (SEQUENCE `serialize_asn1_envelop_tag_with_TLV`
       (**) (serialize_RDN_payload oid t lb ub)))

let serialize_RDN oid t lb ub
= coerce_parser_serializer
    (parse_RDN oid t lb ub)
    (SET `serialize_asn1_envelop_tag_with_TLV`
    (**) (SEQUENCE `serialize_asn1_envelop_tag_with_TLV`
       (**) (serialize_RDN_payload oid t lb ub)))
    ()

let lemma_serialize_RDN_unfold oid t lb ub x
= lemma_serialize_asn1_envelop_tag_with_TLV_unfold
    (SET)
    (**) (SEQUENCE `serialize_asn1_envelop_tag_with_TLV`
         (**) (oid `serialize_envelop_OID_with`
         (**)  serialize_asn1_character_string_with_character_bound t lb ub))
    (x);
  lemma_serialize_asn1_envelop_tag_with_TLV_unfold
    (SEQUENCE)
    (**) (oid `serialize_envelop_OID_with`
    (**)  serialize_asn1_character_string_with_character_bound t lb ub)
    (x);
  lemma_serialize_envelop_OID_with_unfold
    (oid)
    (serialize_asn1_character_string_with_character_bound t lb ub)
    (x)

let lemma_serialize_RDN_size oid t lb ub x
= lemma_serialize_asn1_envelop_tag_with_TLV_size
    (SET)
    (**) (SEQUENCE `serialize_asn1_envelop_tag_with_TLV`
         (**) (oid `serialize_envelop_OID_with`
         (**)  serialize_asn1_character_string_with_character_bound t lb ub))
    (x);
  lemma_serialize_asn1_envelop_tag_with_TLV_size
    (SEQUENCE)
    (**) (oid `serialize_envelop_OID_with`
    (**)  serialize_asn1_character_string_with_character_bound t lb ub)
    (x);
  lemma_serialize_envelop_OID_with_size
    (oid)
    (serialize_asn1_character_string_with_character_bound t lb ub)
    (x)

let lemma_serialize_RDN_size_exact oid t lb ub x
= lemma_serialize_RDN_unfold oid t lb ub x;
  lemma_serialize_RDN_size   oid t lb ub x;
  lemma_serialize_envelop_OID_with_size
    (oid)
    (serialize_asn1_character_string_with_character_bound t lb ub)
    (x);
  // lemma_serialize_asn1_oid_TLV_of_size oid oid
()

#push-options "--ifuel 1"

let serialize32_RDN_backwards oid t lb ub
= coerce_serializer32_backwards
  (* s2  *) (serialize_RDN oid t lb ub)
  (* s32 *) (SET `serialize32_asn1_envelop_tag_with_TLV_backwards`
            (**) (SEQUENCE `serialize32_asn1_envelop_tag_with_TLV_backwards`
                 (**) (serialize32_RDN_payload_backwards oid t lb ub)))
  (* prf *) ()

(*  *)

let lemma_RDN_x520_attribute_size #t #string_t s
= lemma_serialize_character_string_size string_t s;
  lemma_serialize_asn1_oid_TLV_of_size (x520_attribute_oid t) (x520_attribute_oid t);
  lemma_serialize_envelop_OID_with_size
    (x520_attribute_oid t)
    (serialize_asn1_TLV_of_type string_t)
    ((x520_attribute_oid t), s)
/
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

    t: X509.BasicFields.RelativeDistinguishedName.x520_attribute_t ->
    string_t:
      X509.BasicFields.RelativeDistinguishedName.directory_string_type
        { t == X509.BasicFields.RelativeDistinguishedName.COUNTRY ==>
          string_t == ASN1.Base.PRINTABLE_STRING }
  -> LowParse.Spec.Base.parser (ASN1.Spec.Value.Envelop.parse_asn1_envelop_tag_with_TLV_kind ASN1.Base.SET
        )
      (X509.BasicFields.RelativeDistinguishedName.x509_RDN_x520_attribute_t t string_t)
X509.BasicFields.RelativeDistinguishedName.x520_attribute_t X509.BasicFields.RelativeDistinguishedName.directory_string_type Prims.l_imp Prims.eq2 X509.BasicFields.RelativeDistinguishedName.COUNTRY ASN1.Base.asn1_tag_t ASN1.Base.PRINTABLE_STRING LowParse.Spec.Base.coerce_parser X509.BasicFields.RelativeDistinguishedName.x509_RDN_x520_attribute_t ASN1.Spec.Value.Envelop.parse_asn1_envelop_tag_with_TLV_kind ASN1.Base.SET X509.BasicFields.RelativeDistinguishedName.x509_RDN_t X509.BasicFields.RelativeDistinguishedName.x520_attribute_oid X509.BasicFields.RelativeDistinguishedName.x520_attribute_lb X509.BasicFields.RelativeDistinguishedName.x520_attribute_ub X509.BasicFields.RelativeDistinguishedName.parse_RDN LowParse.Spec.Base.parser
let parse_RDN_x520_attribute t string_t =
  
(x509_RDN_x520_attribute_t t string_t)
`coerce_parser`
(parse_RDN (x520_attribute_oid t) (string_t) (x520_attribute_lb t) (x520_attribute_ub t))