val synth_deviceIDCRI_payload_t (x': deviceIDCRI_payload_t') : GTot (deviceIDCRI_payload_t)
val synth_deviceIDCRI_payload_t (x': deviceIDCRI_payload_t') : GTot (deviceIDCRI_payload_t)
let synth_deviceIDCRI_payload_t
  (x': deviceIDCRI_payload_t')
: GTot (deviceIDCRI_payload_t) = {
  deviceIDCRI_version       = fst (fst (fst x'));
  deviceIDCRI_subject       = snd (fst (fst x'));
  deviceIDCRI_subjectPKInfo = snd (fst x');
  deviceIDCRI_attributes    = snd x';
}
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 }}
 *   }
 *
 *)

let deviceIDCRI_payload_t' = (
  datatype_of_asn1_type INTEGER `tuple2`
  deviceIDCRI_subject_t `tuple2`
  subjectPublicKeyInfo_t `tuple2`
  deviceIDCRI_attributes_t
)
/
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
x': L0.X509.DeviceIDCRI.deviceIDCRI_payload_t'
  -> Prims.GTot L0.X509.DeviceIDCRI.deviceIDCRI_payload_t
L0.X509.DeviceIDCRI.deviceIDCRI_payload_t' L0.X509.DeviceIDCRI.MkdeviceIDCRI_payload_t FStar.Pervasives.Native.fst ASN1.Base.datatype_of_asn1_type ASN1.Base.INTEGER L0.X509.DeviceIDCRI.Subject.deviceIDCRI_subject_t FStar.Pervasives.Native.tuple2 X509.BasicFields.SubjectPublicKeyInfo.subjectPublicKeyInfo_t L0.X509.DeviceIDCRI.Attributes.deviceIDCRI_attributes_t FStar.Pervasives.Native.snd L0.X509.DeviceIDCRI.deviceIDCRI_payload_t
let synth_deviceIDCRI_payload_t (x': deviceIDCRI_payload_t') : GTot (deviceIDCRI_payload_t) =
  
{
  deviceIDCRI_version = fst (fst (fst x'));
  deviceIDCRI_subject = snd (fst (fst x'));
  deviceIDCRI_subjectPKInfo = snd (fst x');
  deviceIDCRI_attributes = snd x'
}