val lemma_serialize_RDN_size_exact
  (oid: x509_RDN_attribute_oid)
  (t: directory_string_type)
  (lb: asn1_int32)
  (ub: asn1_value_int32_of_type t { lb <= ub })
  (x: x509_RDN_t oid t lb ub)
: Lemma (
  let x': SEQUENCE `inbound_envelop_tag_with_value_of`
          (oid `serialize_envelop_OID_with`
           serialize_asn1_character_string_with_character_bound t lb ub)
         = (   (coerce_envelop
                 (SET)
                 (SEQUENCE)
                 (oid `serialize_envelop_OID_with`
                  serialize_asn1_character_string_with_character_bound t lb ub)
                 (x))) in
  let s = snd x' in
  let _ = lemma_serialize_RDN_size oid t lb ub x in
  // let _ = lemma_serialize_asn1_oid_TLV_of_size oid oid in
  length_of_opaque_serialization (serialize_RDN oid t lb ub) x <= asn1_TLV_length_max_of_type SET /\
  length_of_opaque_serialization
    (SEQUENCE `serialize_asn1_envelop_tag_with_TLV`
    (**) (oid `serialize_envelop_OID_with`
    (**)  serialize_asn1_character_string_with_character_bound t lb ub))
    (x)
  <= asn1_TLV_length_max_of_type SEQUENCE /\
  // let y = x <: x509_RDN_t oid lb ub t in
  // asn1_value_length_inbound_of_type SET
  // (length_of_opaque_serialization
  //   (SEQUENCE `serialize_asn1_envelop_tag_with_TLV`
  //   (**) (oid `serialize_envelop_OID_with`
  //   (**)  serialize_asn1_character_string_with_character_bound t lb ub))
  //   (x)) /\
  // (length_of_asn1_primitive_TLV #OID oid +
  //  length_of_asn1_primitive_TLV #t s)
  length_of_opaque_serialization
    (oid `serialize_envelop_OID_with`
     serialize_asn1_character_string_with_character_bound t lb ub)
    (x)
  <= asn1_value_length_max_of_type SEQUENCE /\
  length_of_opaque_serialization
    (oid `serialize_envelop_OID_with`
     serialize_asn1_character_string_with_character_bound t lb ub)
    (x)
  == length_of_envelop_OID_with
            (oid)
            (serialize_asn1_character_string_with_character_bound t lb ub)
            (s) /\
  length_of_opaque_serialization (serialize_asn1_character_string_with_character_bound t lb ub) (s)
  == length_of_asn1_primitive_TLV #t s /\
  length_of_opaque_serialization (serialize_asn1_oid_TLV_of oid) oid
  == length_of_asn1_primitive_TLV #OID oid /\
  length_of_opaque_serialization
    (oid `serialize_envelop_OID_with`
     serialize_asn1_character_string_with_character_bound t lb ub)
    (x)
  == (length_of_asn1_primitive_TLV #OID oid +
      length_of_asn1_primitive_TLV #t s) /\
  (SEQUENCE `length_of_TLV`
        (**) (length_of_asn1_primitive_TLV #OID oid +
              length_of_asn1_primitive_TLV #t s))
        <= asn1_TLV_length_max_of_type SEQUENCE /\
  length_of_opaque_serialization (serialize_RDN oid t lb ub) x
  == length_of_RDN oid t s /\
  True
)
val lemma_serialize_RDN_size_exact
  (oid: x509_RDN_attribute_oid)
  (t: directory_string_type)
  (lb: asn1_int32)
  (ub: asn1_value_int32_of_type t { lb <= ub })
  (x: x509_RDN_t oid t lb ub)
: Lemma (
  let x': SEQUENCE `inbound_envelop_tag_with_value_of`
          (oid `serialize_envelop_OID_with`
           serialize_asn1_character_string_with_character_bound t lb ub)
         = (   (coerce_envelop
                 (SET)
                 (SEQUENCE)
                 (oid `serialize_envelop_OID_with`
                  serialize_asn1_character_string_with_character_bound t lb ub)
                 (x))) in
  let s = snd x' in
  let _ = lemma_serialize_RDN_size oid t lb ub x in
  // let _ = lemma_serialize_asn1_oid_TLV_of_size oid oid in
  length_of_opaque_serialization (serialize_RDN oid t lb ub) x <= asn1_TLV_length_max_of_type SET /\
  length_of_opaque_serialization
    (SEQUENCE `serialize_asn1_envelop_tag_with_TLV`
    (**) (oid `serialize_envelop_OID_with`
    (**)  serialize_asn1_character_string_with_character_bound t lb ub))
    (x)
  <= asn1_TLV_length_max_of_type SEQUENCE /\
  // let y = x <: x509_RDN_t oid lb ub t in
  // asn1_value_length_inbound_of_type SET
  // (length_of_opaque_serialization
  //   (SEQUENCE `serialize_asn1_envelop_tag_with_TLV`
  //   (**) (oid `serialize_envelop_OID_with`
  //   (**)  serialize_asn1_character_string_with_character_bound t lb ub))
  //   (x)) /\
  // (length_of_asn1_primitive_TLV #OID oid +
  //  length_of_asn1_primitive_TLV #t s)
  length_of_opaque_serialization
    (oid `serialize_envelop_OID_with`
     serialize_asn1_character_string_with_character_bound t lb ub)
    (x)
  <= asn1_value_length_max_of_type SEQUENCE /\
  length_of_opaque_serialization
    (oid `serialize_envelop_OID_with`
     serialize_asn1_character_string_with_character_bound t lb ub)
    (x)
  == length_of_envelop_OID_with
            (oid)
            (serialize_asn1_character_string_with_character_bound t lb ub)
            (s) /\
  length_of_opaque_serialization (serialize_asn1_character_string_with_character_bound t lb ub) (s)
  == length_of_asn1_primitive_TLV #t s /\
  length_of_opaque_serialization (serialize_asn1_oid_TLV_of oid) oid
  == length_of_asn1_primitive_TLV #OID oid /\
  length_of_opaque_serialization
    (oid `serialize_envelop_OID_with`
     serialize_asn1_character_string_with_character_bound t lb ub)
    (x)
  == (length_of_asn1_primitive_TLV #OID oid +
      length_of_asn1_primitive_TLV #t s) /\
  (SEQUENCE `length_of_TLV`
        (**) (length_of_asn1_primitive_TLV #OID oid +
              length_of_asn1_primitive_TLV #t s))
        <= asn1_TLV_length_max_of_type SEQUENCE /\
  length_of_opaque_serialization (serialize_RDN oid t lb ub) x
  == length_of_RDN oid t s /\
  True
)
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
()
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)
/
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} ->
    x: X509.BasicFields.RelativeDistinguishedName.x509_RDN_t oid t lb ub
  -> FStar.Pervasives.Lemma
    (ensures
      (let x' =
          ASN1.Spec.Value.Envelop.coerce_envelop ASN1.Base.SET
            ASN1.Base.SEQUENCE
            (ASN1.Spec.Value.OID.serialize_envelop_OID_with oid
                (ASN1.Spec.Value.CharacterString.serialize_asn1_character_string_with_character_bound
                    t
                    lb
                    ub))
            x
        in
        let s = FStar.Pervasives.Native.snd x' in
        [@@ FStar.Pervasives.inline_let ]let _ =
          X509.BasicFields.RelativeDistinguishedName.lemma_serialize_RDN_size oid t lb ub x
        in
        ASN1.Spec.Base.length_of_opaque_serialization (X509.BasicFields.RelativeDistinguishedName.serialize_RDN
              oid
              t
              lb
              ub)
          x <=
        ASN1.Base.asn1_TLV_length_max_of_type ASN1.Base.SET /\
        ASN1.Spec.Base.length_of_opaque_serialization (ASN1.Spec.Value.Envelop.serialize_asn1_envelop_tag_with_TLV
              ASN1.Base.SEQUENCE
              (ASN1.Spec.Value.OID.serialize_envelop_OID_with oid
                  (ASN1.Spec.Value.CharacterString.serialize_asn1_character_string_with_character_bound
                      t
                      lb
                      ub)))
          x <=
        ASN1.Base.asn1_TLV_length_max_of_type ASN1.Base.SEQUENCE /\
        ASN1.Spec.Base.length_of_opaque_serialization (ASN1.Spec.Value.OID.serialize_envelop_OID_with
              oid
              (ASN1.Spec.Value.CharacterString.serialize_asn1_character_string_with_character_bound t
                  lb
                  ub))
          x <=
        ASN1.Base.asn1_value_length_max_of_type ASN1.Base.SEQUENCE /\
        ASN1.Spec.Base.length_of_opaque_serialization (ASN1.Spec.Value.OID.serialize_envelop_OID_with
              oid
              (ASN1.Spec.Value.CharacterString.serialize_asn1_character_string_with_character_bound t
                  lb
                  ub))
          x ==
        ASN1.Spec.Value.OID.length_of_envelop_OID_with oid
          (ASN1.Spec.Value.CharacterString.serialize_asn1_character_string_with_character_bound t
              lb
              ub)
          s /\
        ASN1.Spec.Base.length_of_opaque_serialization (ASN1.Spec.Value.CharacterString.serialize_asn1_character_string_with_character_bound
              t
              lb
              ub)
          s ==
        ASN1.Spec.TLV.length_of_asn1_primitive_TLV s /\
        ASN1.Spec.Base.length_of_opaque_serialization (ASN1.Spec.Value.OID.serialize_asn1_oid_TLV_of
              oid)
          oid ==
        ASN1.Spec.TLV.length_of_asn1_primitive_TLV oid /\
        ASN1.Spec.Base.length_of_opaque_serialization (ASN1.Spec.Value.OID.serialize_envelop_OID_with
              oid
              (ASN1.Spec.Value.CharacterString.serialize_asn1_character_string_with_character_bound t
                  lb
                  ub))
          x ==
        ASN1.Spec.TLV.length_of_asn1_primitive_TLV oid +
        ASN1.Spec.TLV.length_of_asn1_primitive_TLV s /\
        ASN1.Spec.TLV.length_of_TLV ASN1.Base.SEQUENCE
          (ASN1.Spec.TLV.length_of_asn1_primitive_TLV oid +
            ASN1.Spec.TLV.length_of_asn1_primitive_TLV s) <=
        ASN1.Base.asn1_TLV_length_max_of_type ASN1.Base.SEQUENCE /\
        ASN1.Spec.Base.length_of_opaque_serialization (X509.BasicFields.RelativeDistinguishedName.serialize_RDN
              oid
              t
              lb
              ub)
          x ==
        X509.BasicFields.RelativeDistinguishedName.length_of_RDN oid t s /\ Prims.l_True))
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 X509.BasicFields.RelativeDistinguishedName.x509_RDN_t Prims.unit ASN1.Spec.Value.OID.lemma_serialize_envelop_OID_with_size 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 X509.BasicFields.RelativeDistinguishedName.lemma_serialize_RDN_size X509.BasicFields.RelativeDistinguishedName.lemma_serialize_RDN_unfold
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);
()