val deviceIDCSR_payload_t' : cri_len: ASN1.Base.asn1_int32 -> Type0
let deviceIDCSR_payload_t' (cri_len: asn1_int32) = (
  (B32.lbytes32 cri_len `tuple2`
   algorithmIdentifier_t) `tuple2`
   x509_signature_t
)
module L0.X509.DeviceIDCSR

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

module B32 = FStar.Bytes

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

let decl = ()
/
X509.fst.checked prims.fst.checked L0.X509.DeviceIDCRI.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.DeviceIDCSR.fst
cri_len: ASN1.Base.asn1_int32 -> Type0
ASN1.Base.asn1_int32 FStar.Pervasives.Native.tuple2 FStar.Bytes.lbytes32 X509.Crypto.AlgorithmIdentifier.algorithmIdentifier_t X509.Crypto.Signature.x509_signature_t
let deviceIDCSR_payload_t' (cri_len: asn1_int32) =
  
(((B32.lbytes32 cri_len) `tuple2` algorithmIdentifier_t) `tuple2` x509_signature_t)