val deviceIDCRI_t : Type0
let deviceIDCRI_t
= inbound_sequence_value_of (serialize_deviceIDCRI_payload)
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"]
unfold noextract
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 ()

let len_of_deviceIDCRI_payload
  (version: datatype_of_asn1_type INTEGER)
  (s_common:  x509_RDN_x520_attribute_string_t COMMON_NAME  IA5_STRING)
  (s_org:     x509_RDN_x520_attribute_string_t ORGANIZATION IA5_STRING)
  (s_country: x509_RDN_x520_attribute_string_t COUNTRY      PRINTABLE_STRING)
: Tot (asn1_value_int32_of_type SEQUENCE)
= len_of_asn1_primitive_TLV #INTEGER version +
  len_of_deviceIDCRI_subject s_common s_org s_country +
  len_of_subjectPublicKeyInfo +
  len_of_deviceIDCRI_attributes ()

val lemma_serialize_deviceIDCRI_payload_size
  (x: deviceIDCRI_payload_t)
: Lemma (
  let attrs' = coerce_envelop
                (CUSTOM_TAG CONTEXT_SPECIFIC CONSTRUCTED 0uy `asn1_implicit_tagging` SET)
                (SEQUENCE)
                (OID_PKCS9_CSR_EXT_REQ `serialize_envelop_OID_with`
                (**) (SET `serialize_asn1_envelop_tag_with_TLV`
                     (**) (SEQUENCE `serialize_asn1_envelop_tag_with_TLV`
                          (**) serialize_deviceIDCRI_attributes_extensionRequest_payload)))
                (x.deviceIDCRI_attributes) in
  length_of_opaque_serialization (serialize_deviceIDCRI_payload)      x ==
  length_of_opaque_serialization (serialize_asn1_TLV_of_type INTEGER) x.deviceIDCRI_version +
  length_of_opaque_serialization (serialize_deviceIDCRI_subject)      x.deviceIDCRI_subject +
  length_of_opaque_serialization (serialize_subjectPublicKeyInfo)     x.deviceIDCRI_subjectPKInfo +
  length_of_opaque_serialization (serialize_deviceIDCRI_attributes)   x.deviceIDCRI_attributes /\
  length_of_opaque_serialization (serialize_deviceIDCRI_payload)      x
  == v (len_of_deviceIDCRI_payload
       (x.deviceIDCRI_version)
       (get_RDN_x520_attribute_string x.deviceIDCRI_subject.deviceIDCRI_subject_Common)
       (get_RDN_x520_attribute_string x.deviceIDCRI_subject.deviceIDCRI_subject_Organization)
       (get_RDN_x520_attribute_string x.deviceIDCRI_subject.deviceIDCRI_subject_Country))
)

(*
 *
/
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
Type0
ASN1.Spec.Value.SEQUENCE.inbound_sequence_value_of L0.X509.DeviceIDCRI.parse_deviceIDCRI_payload_kind L0.X509.DeviceIDCRI.deviceIDCRI_payload_t L0.X509.DeviceIDCRI.parse_deviceIDCRI_payload L0.X509.DeviceIDCRI.serialize_deviceIDCRI_payload
let deviceIDCRI_t =
  
inbound_sequence_value_of (serialize_deviceIDCRI_payload)