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)
)
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)
)
let lemma_serialize_deviceIDCRI_payload_unfold x
= serialize_nondep_then_eq
  (* s1 *) (serialize_asn1_TLV_of_type INTEGER)
  (* s2 *) (serialize_deviceIDCRI_subject)
  (* in *) (fst (fst (synth_deviceIDCRI_payload_t' x)));
  serialize_nondep_then_eq
  (* s1 *) (serialize_asn1_TLV_of_type INTEGER
            `serialize_nondep_then`
            serialize_deviceIDCRI_subject)
  (* s2 *) (serialize_subjectPublicKeyInfo)
  (* in *) (fst (synth_deviceIDCRI_payload_t' x));
  serialize_nondep_then_eq
  (* s1 *) (serialize_asn1_TLV_of_type INTEGER
            `serialize_nondep_then`
            serialize_deviceIDCRI_subject
            `serialize_nondep_then`
            serialize_subjectPublicKeyInfo)
  (* s2 *) (serialize_deviceIDCRI_attributes)
  (* in *) (synth_deviceIDCRI_payload_t' x);
  serialize_synth_eq
  (* p1 *) (parse_asn1_TLV_of_type INTEGER
            `nondep_then`
            parse_deviceIDCRI_subject
            `nondep_then`
            parse_subjectPublicKeyInfo
            `nondep_then`
            parse_deviceIDCRI_attributes)
  (* f2 *) (synth_deviceIDCRI_payload_t)
  (* s1 *) (serialize_asn1_TLV_of_type INTEGER
            `serialize_nondep_then`
            serialize_deviceIDCRI_subject
            `serialize_nondep_then`
            serialize_subjectPublicKeyInfo
            `serialize_nondep_then`
            serialize_deviceIDCRI_attributes)
  (* g1 *) (synth_deviceIDCRI_payload_t')
  (* prf*) ()
  (* in *) (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
)


(* 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
 *)
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

let serialize_deviceIDCRI_payload
= serialize_synth
  (* p1 *) (parse_asn1_TLV_of_type INTEGER
            `nondep_then`
            parse_deviceIDCRI_subject
            `nondep_then`
            parse_subjectPublicKeyInfo
            `nondep_then`
            parse_deviceIDCRI_attributes)
  (* f2 *) (synth_deviceIDCRI_payload_t)
  (* s1 *) (serialize_asn1_TLV_of_type INTEGER
            `serialize_nondep_then`
            serialize_deviceIDCRI_subject
            `serialize_nondep_then`
            serialize_subjectPublicKeyInfo
            `serialize_nondep_then`
            serialize_deviceIDCRI_attributes)
  (* g1 *) (synth_deviceIDCRI_payload_t')
  (* prf*) ()
/
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
  -> FStar.Pervasives.Lemma
    (ensures
      LowParse.Spec.Base.serialize L0.X509.DeviceIDCRI.serialize_deviceIDCRI_payload x ==
      FStar.Seq.Base.append (FStar.Seq.Base.append (FStar.Seq.Base.append (LowParse.Spec.Base.serialize
                    (ASN1.Spec.TLV.serialize_asn1_TLV_of_type ASN1.Base.INTEGER)
                    (MkdeviceIDCRI_payload_t?.deviceIDCRI_version x))
                (LowParse.Spec.Base.serialize L0.X509.DeviceIDCRI.Subject.serialize_deviceIDCRI_subject
                    (MkdeviceIDCRI_payload_t?.deviceIDCRI_subject x)))
            (LowParse.Spec.Base.serialize X509.BasicFields.SubjectPublicKeyInfo.serialize_subjectPublicKeyInfo
                (MkdeviceIDCRI_payload_t?.deviceIDCRI_subjectPKInfo x)))
        (LowParse.Spec.Base.serialize L0.X509.DeviceIDCRI.Attributes.serialize_deviceIDCRI_attributes
            (MkdeviceIDCRI_payload_t?.deviceIDCRI_attributes x)))
L0.X509.DeviceIDCRI.deviceIDCRI_payload_t LowParse.Spec.Combinators.serialize_synth_eq 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 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 LowParse.Spec.Combinators.serialize_nondep_then ASN1.Spec.TLV.serialize_asn1_TLV_of_type L0.X509.DeviceIDCRI.Subject.serialize_deviceIDCRI_subject X509.BasicFields.SubjectPublicKeyInfo.serialize_subjectPublicKeyInfo L0.X509.DeviceIDCRI.Attributes.serialize_deviceIDCRI_attributes L0.X509.DeviceIDCRI.synth_deviceIDCRI_payload_t' Prims.unit LowParse.Spec.Combinators.serialize_nondep_then_eq FStar.Pervasives.Native.fst
let lemma_serialize_deviceIDCRI_payload_unfold x =
  
serialize_nondep_then_eq (serialize_asn1_TLV_of_type INTEGER)
  (serialize_deviceIDCRI_subject)
  (fst (fst (synth_deviceIDCRI_payload_t' x)));
serialize_nondep_then_eq ((serialize_asn1_TLV_of_type INTEGER)
    `serialize_nondep_then`
    serialize_deviceIDCRI_subject)
  (serialize_subjectPublicKeyInfo)
  (fst (synth_deviceIDCRI_payload_t' x));
serialize_nondep_then_eq (((serialize_asn1_TLV_of_type INTEGER)
      `serialize_nondep_then`
      serialize_deviceIDCRI_subject)
    `serialize_nondep_then`
    serialize_subjectPublicKeyInfo)
  (serialize_deviceIDCRI_attributes)
  (synth_deviceIDCRI_payload_t' x);
serialize_synth_eq ((((parse_asn1_TLV_of_type INTEGER) `nondep_then` parse_deviceIDCRI_subject)
      `nondep_then`
      parse_subjectPublicKeyInfo)
    `nondep_then`
    parse_deviceIDCRI_attributes)
  (synth_deviceIDCRI_payload_t)
  ((((serialize_asn1_TLV_of_type INTEGER) `serialize_nondep_then` serialize_deviceIDCRI_subject)
      `serialize_nondep_then`
      serialize_subjectPublicKeyInfo)
    `serialize_nondep_then`
    serialize_deviceIDCRI_attributes)
  (synth_deviceIDCRI_payload_t')
  ()
  (x)