val synth_deviceIDCSR_payload_t (cri_len: asn1_int32) (x': deviceIDCSR_payload_t' cri_len)
    : GTot (deviceIDCSR_payload_t cri_len)
val synth_deviceIDCSR_payload_t (cri_len: asn1_int32) (x': deviceIDCSR_payload_t' cri_len)
    : GTot (deviceIDCSR_payload_t cri_len)
let synth_deviceIDCSR_payload_t
  (cri_len: asn1_int32)
  (x': deviceIDCSR_payload_t' cri_len)
: GTot (deviceIDCSR_payload_t cri_len)
= { deviceIDCSR_cri     = fst (fst x');
    deviceIDCSR_sig_alg = snd (fst x');
    deviceIDCSR_sig     = snd x' }
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 = ()

let deviceIDCSR_payload_t' (cri_len: asn1_int32) = (
  (B32.lbytes32 cri_len `tuple2`
   algorithmIdentifier_t) `tuple2`
   x509_signature_t
)
/
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 -> x': L0.X509.DeviceIDCSR.deviceIDCSR_payload_t' cri_len
  -> Prims.GTot (L0.X509.DeviceIDCSR.deviceIDCSR_payload_t cri_len)
ASN1.Base.asn1_int32 L0.X509.DeviceIDCSR.deviceIDCSR_payload_t' L0.X509.DeviceIDCSR.MkdeviceIDCSR_payload_t FStar.Pervasives.Native.fst FStar.Bytes.lbytes32 X509.Crypto.AlgorithmIdentifier.algorithmIdentifier_t FStar.Pervasives.Native.tuple2 X509.Crypto.Signature.x509_signature_t FStar.Pervasives.Native.snd L0.X509.DeviceIDCSR.deviceIDCSR_payload_t
let synth_deviceIDCSR_payload_t (cri_len: asn1_int32) (x': deviceIDCSR_payload_t' cri_len)
    : GTot (deviceIDCSR_payload_t cri_len) =
  
{ deviceIDCSR_cri = fst (fst x'); deviceIDCSR_sig_alg = snd (fst x'); deviceIDCSR_sig = snd x' }