val parse_deviceIDCRI_payload_kind:parser_kind
val parse_deviceIDCRI_payload_kind:parser_kind
let parse_deviceIDCRI_payload_kind
: parser_kind
= parse_asn1_TLV_kind_of_type INTEGER
  `and_then_kind`
  parse_asn1_envelop_tag_with_TLV_kind SEQUENCE
  `and_then_kind`
  parse_asn1_envelop_tag_with_TLV_kind SEQUENCE
  `and_then_kind`
  parse_asn1_envelop_tag_with_TLV_kind
    (CUSTOM_TAG CONTEXT_SPECIFIC CONSTRUCTED 0uy `asn1_implicit_tagging` SET)
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 128 --fuel 0 --ifuel 0 --using_facts_from '* -FStar.Tactics -FStar.Reflection'"

(*     (To-Be-Signed) DeviceID Certification Request Info
 *================================================================
 *   CertificationRequestInfo ::= SEQUENCE {
 *        version       INTEGER { v1(0) } (v1,...),
 *        subject       Name,
 *        subjectPKInfo SubjectPublicKeyInfo{{ PKInfoAlgorithms }},
 *        attributes    [0] Attributes{{ CRIAttributes }}
 *   }
 *
 *)

val decl : unit

noeq
type deviceIDCRI_payload_t = {
  deviceIDCRI_version: datatype_of_asn1_type INTEGER;
  deviceIDCRI_subject: deviceIDCRI_subject_t;
  deviceIDCRI_subjectPKInfo: subjectPublicKeyInfo_t;
  deviceIDCRI_attributes: deviceIDCRI_attributes_t
}
/
X509.fst.checked prims.fst.checked L0.X509.DeviceIDCRI.Subject.fsti.checked L0.X509.DeviceIDCRI.Attributes.fsti.checked FStar.UInt8.fsti.checked FStar.UInt32.fsti.checked FStar.Seq.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.fsti
LowParse.Spec.Base.parser_kind
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 ASN1.Base.SET
let parse_deviceIDCRI_payload_kind:parser_kind =
  
(((parse_asn1_TLV_kind_of_type INTEGER)
    `and_then_kind`
    (parse_asn1_envelop_tag_with_TLV_kind SEQUENCE))
  `and_then_kind`
  (parse_asn1_envelop_tag_with_TLV_kind SEQUENCE))
`and_then_kind`
(parse_asn1_envelop_tag_with_TLV_kind ((CUSTOM_TAG CONTEXT_SPECIFIC CONSTRUCTED 0uy)
      `asn1_implicit_tagging`
      SET))