val deviceIDCRI_payload_t' : Type0
let deviceIDCRI_payload_t' = (
  datatype_of_asn1_type INTEGER `tuple2`
  deviceIDCRI_subject_t `tuple2`
  subjectPublicKeyInfo_t `tuple2`
  deviceIDCRI_attributes_t
)
module L0.X509.DeviceIDCRI

open ASN1.Spec
open ASN1.Low
open X509
open L0.X509.DeviceIDCRI.Subject
open L0.X509.DeviceIDCRI.Attributes
open FStar.Integers

module B32 = FStar.Bytes

#set-options "--z3rlimit 256 --fuel 0 --ifuel 0"

let decl = ()

(*     (To-Be-Signed) DeviceID Certification Request Info
 *================================================================
 *   CertificationRequestInfo ::= SEQUENCE {
 *        version       INTEGER { v1(0) } (v1,...),
 *        subject       Name,
 *        subjectPKInfo SubjectPublicKeyInfo{{ PKInfoAlgorithms }},
 *        attributes    [0] Attributes{{ CRIAttributes }}
 *   }
 *
 *)
/
X509.fst.checked prims.fst.checked L0.X509.DeviceIDCRI.Subject.fsti.checked L0.X509.DeviceIDCRI.Attributes.fsti.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Integers.fst.checked FStar.Bytes.fsti.checked ASN1.Spec.fst.checked ASN1.Low.fst.checked
L0.X509.DeviceIDCRI.fst
Type0
FStar.Pervasives.Native.tuple2 ASN1.Base.datatype_of_asn1_type ASN1.Base.INTEGER L0.X509.DeviceIDCRI.Subject.deviceIDCRI_subject_t X509.BasicFields.SubjectPublicKeyInfo.subjectPublicKeyInfo_t L0.X509.DeviceIDCRI.Attributes.deviceIDCRI_attributes_t
let deviceIDCRI_payload_t' =
  
((((datatype_of_asn1_type INTEGER) `tuple2` deviceIDCRI_subject_t) `tuple2` subjectPublicKeyInfo_t)
  `tuple2`
  deviceIDCRI_attributes_t)