val len_of_deviceIDCRI_subject_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)
    : Tot
    (len: asn1_value_int32_of_type SEQUENCE {v len <= v (len_of_deviceIDCRI_subject_payload_max ())}
    )
val len_of_deviceIDCRI_subject_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)
    : Tot
    (len: asn1_value_int32_of_type SEQUENCE {v len <= v (len_of_deviceIDCRI_subject_payload_max ())}
    )
let len_of_deviceIDCRI_subject_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)
: Tot (len: asn1_value_int32_of_type SEQUENCE
            { v len <= v (len_of_deviceIDCRI_subject_payload_max ()) })
= len_of_RDN_x520_attribute s_common +
  len_of_RDN_x520_attribute s_org +
  len_of_RDN_x520_attribute s_country
module L0.X509.DeviceIDCRI.Subject

open ASN1.Spec
open ASN1.Low
open X509
open FStar.Integers

open L0.X509.LengthUtils

module B32 = FStar.Bytes

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

val decl : unit

let x509_rdn_string_t = ASN1.Base.oid_t & ASN1.Base.character_string_t IA5_STRING

noeq
type deviceIDCRI_subject_payload_t = {
  deviceIDCRI_subject_Common      : x509_RDN_x520_attribute_t COMMON_NAME  IA5_STRING;
  deviceIDCRI_subject_Organization: x509_RDN_x520_attribute_t ORGANIZATION IA5_STRING;
  deviceIDCRI_subject_Country     : x509_RDN_x520_attribute_t COUNTRY      PRINTABLE_STRING
}

inline_for_extraction noextract
let parse_deviceIDCRI_subject_payload_kind
: parser_kind
= parse_asn1_envelop_tag_with_TLV_kind SET
  `and_then_kind`
  parse_asn1_envelop_tag_with_TLV_kind SET
  `and_then_kind`
  parse_asn1_envelop_tag_with_TLV_kind SET

noextract
val parse_deviceIDCRI_subject_payload
: parser
    (parse_deviceIDCRI_subject_payload_kind)
    (deviceIDCRI_subject_payload_t)

noextract
val serialize_deviceIDCRI_subject_payload
: serializer (parse_deviceIDCRI_subject_payload)

// unfold
// [@@ "opaque_to_smt"]
let len_of_deviceIDCRI_subject_payload_max ()
: GTot (asn1_value_int32_of_type SEQUENCE)
= len_of_RDN_x520_attribute_max COMMON_NAME  IA5_STRING +
  len_of_RDN_x520_attribute_max ORGANIZATION IA5_STRING +
  len_of_RDN_x520_attribute_max COUNTRY      PRINTABLE_STRING

// unfold
/
X509.fst.checked prims.fst.checked L0.X509.LengthUtils.fst.checked FStar.Seq.fst.checked FStar.Pervasives.fsti.checked FStar.Integers.fst.checked FStar.Bytes.fsti.checked ASN1.Spec.fst.checked ASN1.Low.fst.checked ASN1.Base.fst.checked
L0.X509.DeviceIDCRI.Subject.fsti

    s_common:
      X509.BasicFields.RelativeDistinguishedName.x509_RDN_x520_attribute_string_t X509.BasicFields.RelativeDistinguishedName.COMMON_NAME
        ASN1.Base.IA5_STRING ->
    s_org:
      X509.BasicFields.RelativeDistinguishedName.x509_RDN_x520_attribute_string_t X509.BasicFields.RelativeDistinguishedName.ORGANIZATION
        ASN1.Base.IA5_STRING ->
    s_country:
      X509.BasicFields.RelativeDistinguishedName.x509_RDN_x520_attribute_string_t X509.BasicFields.RelativeDistinguishedName.COUNTRY
        ASN1.Base.PRINTABLE_STRING
  -> len:
    ASN1.Base.asn1_value_int32_of_type ASN1.Base.SEQUENCE
      { FStar.Integers.v len <=
        FStar.Integers.v (L0.X509.DeviceIDCRI.Subject.len_of_deviceIDCRI_subject_payload_max ()) }
X509.BasicFields.RelativeDistinguishedName.x509_RDN_x520_attribute_string_t X509.BasicFields.RelativeDistinguishedName.COMMON_NAME ASN1.Base.IA5_STRING X509.BasicFields.RelativeDistinguishedName.ORGANIZATION X509.BasicFields.RelativeDistinguishedName.COUNTRY ASN1.Base.PRINTABLE_STRING FStar.Integers.op_Plus FStar.Integers.Unsigned FStar.Integers.W32 X509.BasicFields.RelativeDistinguishedName.len_of_RDN_x520_attribute ASN1.Base.asn1_value_int32_of_type ASN1.Base.SEQUENCE Prims.b2t FStar.Integers.op_Less_Equals FStar.Integers.Signed FStar.Integers.Winfinite FStar.Integers.v L0.X509.DeviceIDCRI.Subject.len_of_deviceIDCRI_subject_payload_max
let len_of_deviceIDCRI_subject_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)
    : Tot
    (len: asn1_value_int32_of_type SEQUENCE {v len <= v (len_of_deviceIDCRI_subject_payload_max ())}
    ) =
  
len_of_RDN_x520_attribute s_common + len_of_RDN_x520_attribute s_org +
len_of_RDN_x520_attribute s_country