val parse_deviceIDCRI_payload
: parser parse_deviceIDCRI_payload_kind (deviceIDCRI_payload_t)
val parse_deviceIDCRI_payload
: parser parse_deviceIDCRI_payload_kind (deviceIDCRI_payload_t)
let parse_deviceIDCRI_payload
= parse_asn1_TLV_of_type INTEGER
  `nondep_then`
  parse_deviceIDCRI_subject
  `nondep_then`
  parse_subjectPublicKeyInfo
  `nondep_then`
  parse_deviceIDCRI_attributes
  `parse_synth`
  synth_deviceIDCRI_payload_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 }}
 *   }
 *
 *)

let deviceIDCRI_payload_t' = (
  datatype_of_asn1_type INTEGER `tuple2`
  deviceIDCRI_subject_t `tuple2`
  subjectPublicKeyInfo_t `tuple2`
  deviceIDCRI_attributes_t
)


(* Conversion *)
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';
}

inline_for_extraction noextract
let synth_deviceIDCRI_payload_t'
  (x: deviceIDCRI_payload_t)
: Tot (x': deviceIDCRI_payload_t'
            { x == synth_deviceIDCRI_payload_t x' }) = (
  (((x.deviceIDCRI_version),
     x.deviceIDCRI_subject),
     x.deviceIDCRI_subjectPKInfo),
     x.deviceIDCRI_attributes
)


(*
 * Specification
/
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
LowParse.Spec.Base.parser L0.X509.DeviceIDCRI.parse_deviceIDCRI_payload_kind
  L0.X509.DeviceIDCRI.deviceIDCRI_payload_t
LowParse.Spec.Combinators.parse_synth LowParse.Spec.Combinators.and_then_kind ASN1.Spec.TLV.parse_asn1_TLV_kind_of_type ASN1.Base.INTEGER ASN1.Spec.Value.Envelop.parse_asn1_envelop_tag_with_TLV_kind ASN1.Base.SEQUENCE ASN1.Base.asn1_implicit_tagging ASN1.Base.CUSTOM_TAG ASN1.Base.CONTEXT_SPECIFIC ASN1.Base.CONSTRUCTED FStar.UInt8.uint_to_t FStar.UInt8.t ASN1.Base.SET FStar.Pervasives.Native.tuple2 ASN1.Base.datatype_of_asn1_type L0.X509.DeviceIDCRI.Subject.deviceIDCRI_subject_t X509.BasicFields.SubjectPublicKeyInfo.subjectPublicKeyInfo_t L0.X509.DeviceIDCRI.Attributes.deviceIDCRI_attributes_t L0.X509.DeviceIDCRI.deviceIDCRI_payload_t LowParse.Spec.Combinators.nondep_then ASN1.Spec.TLV.parse_asn1_TLV_of_type L0.X509.DeviceIDCRI.Subject.parse_deviceIDCRI_subject X509.BasicFields.SubjectPublicKeyInfo.parse_subjectPublicKeyInfo L0.X509.DeviceIDCRI.Attributes.parse_deviceIDCRI_attributes L0.X509.DeviceIDCRI.synth_deviceIDCRI_payload_t
let parse_deviceIDCRI_payload =
  
((((parse_asn1_TLV_of_type INTEGER) `nondep_then` parse_deviceIDCRI_subject)
    `nondep_then`
    parse_subjectPublicKeyInfo)
  `nondep_then`
  parse_deviceIDCRI_attributes)
`parse_synth`
synth_deviceIDCRI_payload_t