val coerce_x509_rdn_attribute_t_string_to_asn1_string_org
      (x: x509_RDN_x520_attribute_string_t ORGANIZATION IA5_STRING)
    : y:
    datatype_of_asn1_type IA5_STRING
      {x520_attribute_lb ORGANIZATION <= dfst y /\ dfst y <= x520_attribute_ub ORGANIZATION}
val coerce_x509_rdn_attribute_t_string_to_asn1_string_org
      (x: x509_RDN_x520_attribute_string_t ORGANIZATION IA5_STRING)
    : y:
    datatype_of_asn1_type IA5_STRING
      {x520_attribute_lb ORGANIZATION <= dfst y /\ dfst y <= x520_attribute_ub ORGANIZATION}
let coerce_x509_rdn_attribute_t_string_to_asn1_string_org
  (x:x509_RDN_x520_attribute_string_t ORGANIZATION IA5_STRING)
  : y:datatype_of_asn1_type IA5_STRING{
      x520_attribute_lb ORGANIZATION <= dfst y /\
      dfst y <= x520_attribute_ub ORGANIZATION
    }
  = x
module L0.X509.LengthUtils

open ASN1.Spec
open X509
open FStar.Integers

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

// let lemma_length_of_aliasKeyTBS_issuer_payload
//   (s_common:  x509_RDN_x520_attribute_string_t COMMON_NAME  IA5_STRING)
//   (s_org:     x509_RDN_x520_attribute_string_t ORGANIZATION IA5_STRING)
//   (s_country: x509_RDN_x520_attribute_string_t COUNTRY      PRINTABLE_STRING)
//   : Lemma
//       ((v (len_of_RDN_x520_attribute s_common) +
//         v (len_of_RDN_x520_attribute s_org) +
//         v (len_of_RDN_x520_attribute s_country)) <= asn1_value_length_max_of_type SEQUENCE)
//   = ()

let lemma_length_of_l0_extension (version:datatype_of_asn1_type INTEGER)
  : Lemma (length_of_TLV SEQUENCE (length_of_asn1_primitive_TLV version + 109) <=
           asn1_value_length_max_of_type SEQUENCE)
  = ()

let lemma_length_of_l0_extension_l0_version (x:datatype_of_asn1_type INTEGER)
  : Lemma (length_of_TLV SEQUENCE (length_of_asn1_primitive_TLV x + 110) <= 118)
  = ()

unfold noextract
let coerce_x509_rdn_attribute_t_string_to_asn1_string_cn
  (x:x509_RDN_x520_attribute_string_t COMMON_NAME IA5_STRING)
  : y:datatype_of_asn1_type IA5_STRING{
      x520_attribute_lb COMMON_NAME <= dfst y /\
      dfst y <= x520_attribute_ub COMMON_NAME
    }
  = x
/
X509.fst.checked prims.fst.checked FStar.Pervasives.fsti.checked FStar.Integers.fst.checked ASN1.Spec.fst.checked
L0.X509.LengthUtils.fst

    x:
      X509.BasicFields.RelativeDistinguishedName.x509_RDN_x520_attribute_string_t X509.BasicFields.RelativeDistinguishedName.ORGANIZATION
        ASN1.Base.IA5_STRING
  -> y:
    ASN1.Base.datatype_of_asn1_type ASN1.Base.IA5_STRING
      { X509.BasicFields.RelativeDistinguishedName.x520_attribute_lb X509.BasicFields.RelativeDistinguishedName.ORGANIZATION
         <=
        FStar.Pervasives.dfst y /\
        FStar.Pervasives.dfst y <=
        X509.BasicFields.RelativeDistinguishedName.x520_attribute_ub X509.BasicFields.RelativeDistinguishedName.ORGANIZATION
         }
X509.BasicFields.RelativeDistinguishedName.x509_RDN_x520_attribute_string_t X509.BasicFields.RelativeDistinguishedName.ORGANIZATION ASN1.Base.IA5_STRING ASN1.Base.datatype_of_asn1_type Prims.l_and Prims.b2t FStar.Integers.op_Less_Equals FStar.Integers.Unsigned FStar.Integers.W32 X509.BasicFields.RelativeDistinguishedName.x520_attribute_lb FStar.Pervasives.dfst ASN1.Base.asn1_value_int32_of_type ASN1.Base.character_string_lbytes32 X509.BasicFields.RelativeDistinguishedName.x520_attribute_ub
let coerce_x509_rdn_attribute_t_string_to_asn1_string_org
      (x: x509_RDN_x520_attribute_string_t ORGANIZATION IA5_STRING)
    : y:
    datatype_of_asn1_type IA5_STRING
      {x520_attribute_lb ORGANIZATION <= dfst y /\ dfst y <= x520_attribute_ub ORGANIZATION} =
  
x