val len_of_deviceIDCRI_payload_max: Prims.unit -> GTot (asn1_value_int32_of_type SEQUENCE)
val len_of_deviceIDCRI_payload_max: Prims.unit -> GTot (asn1_value_int32_of_type SEQUENCE)
let len_of_deviceIDCRI_payload_max ()
: GTot (asn1_value_int32_of_type SEQUENCE)
// = len_of_asn1_primitive_TLV #INTEGER version +
= asn1_TLV_int32_max_of_type INTEGER +
  len_of_deviceIDCRI_subject_max () +
  len_of_subjectPublicKeyInfo +
  len_of_deviceIDCRI_attributes ()
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
}

inline_for_extraction noextract
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)

(*
 * Specification
 *)
val parse_deviceIDCRI_payload
: parser parse_deviceIDCRI_payload_kind (deviceIDCRI_payload_t)

val serialize_deviceIDCRI_payload
: serializer (parse_deviceIDCRI_payload)

val lemma_serialize_deviceIDCRI_payload_unfold
  (x: deviceIDCRI_payload_t)
: Lemma (
  serialize_deviceIDCRI_payload `serialize` x ==
 (serialize_asn1_TLV_of_type INTEGER `serialize` x.deviceIDCRI_version)
  `Seq.append`
 (serialize_deviceIDCRI_subject `serialize` x.deviceIDCRI_subject)
  `Seq.append`
 (serialize_subjectPublicKeyInfo `serialize` x.deviceIDCRI_subjectPKInfo)
  `Seq.append`
 (serialize_deviceIDCRI_attributes `serialize` x.deviceIDCRI_attributes)
)

[@@ "opaque_to_smt"]
/
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
_: Prims.unit -> Prims.GTot (ASN1.Base.asn1_value_int32_of_type ASN1.Base.SEQUENCE)
Prims.unit FStar.Integers.op_Plus FStar.Integers.Unsigned FStar.Integers.W32 ASN1.Base.asn1_TLV_int32_max_of_type ASN1.Base.INTEGER L0.X509.DeviceIDCRI.Subject.len_of_deviceIDCRI_subject_max X509.BasicFields.SubjectPublicKeyInfo.len_of_subjectPublicKeyInfo L0.X509.DeviceIDCRI.Attributes.len_of_deviceIDCRI_attributes ASN1.Base.asn1_value_int32_of_type ASN1.Base.SEQUENCE
let len_of_deviceIDCRI_payload_max () : GTot (asn1_value_int32_of_type SEQUENCE) =
  
asn1_TLV_int32_max_of_type INTEGER + len_of_deviceIDCRI_subject_max () + len_of_subjectPublicKeyInfo +
len_of_deviceIDCRI_attributes ()