val lemma_serialize_compositeDeviceID_payload_size
  (x: compositeDeviceID_payload_t)
: Lemma (
  length_of_opaque_serialization (serialize_compositeDeviceID_payload) x ==
  length_of_asn1_primitive_TLV x.l0_version +
  length_of_opaque_serialization (serialize_subjectPublicKeyInfo) x.l0_deviceID +
  length_of_opaque_serialization serialize_fwid x.l0_fwid /\
  length_of_opaque_serialization serialize_compositeDeviceID_payload x ==
  length_of_asn1_primitive_TLV x.l0_version + 91 /\
  length_of_opaque_serialization serialize_compositeDeviceID_payload x <= 97
)
val lemma_serialize_compositeDeviceID_payload_size
  (x: compositeDeviceID_payload_t)
: Lemma (
  length_of_opaque_serialization (serialize_compositeDeviceID_payload) x ==
  length_of_asn1_primitive_TLV x.l0_version +
  length_of_opaque_serialization (serialize_subjectPublicKeyInfo) x.l0_deviceID +
  length_of_opaque_serialization serialize_fwid x.l0_fwid /\
  length_of_opaque_serialization serialize_compositeDeviceID_payload x ==
  length_of_asn1_primitive_TLV x.l0_version + 91 /\
  length_of_opaque_serialization serialize_compositeDeviceID_payload x <= 97
)
let lemma_serialize_compositeDeviceID_payload_size x
= lemma_serialize_compositeDeviceID_payload_unfold x;
    lemma_serialize_subjectPublicKeyInfo_size_exact x.l0_deviceID;
    lemma_serialize_fwid_size_exact x.l0_fwid
module L0.X509.CompositeDeviceID

open LowParse.Low.Base
open LowParse.Low.Combinators

open ASN1.Spec
open ASN1.Low

open X509.Base
open X509.BasicFields.SubjectPublicKeyInfo
open X509.Crypto
open L0.X509.Base
open L0.X509.FWID

#set-options "--z3rlimit 32 --fuel 0 --ifuel 0 --using_facts_from '* -FStar.Tactics -FStar.Reflection'"

let decl = ()

(* CompositeDeviceID *)

let compositeDeviceID_payload_t'
= ((datatype_of_asn1_type INTEGER &
    subjectPublicKeyInfo_t) &
    fwid_t)

(* Serialier spec *)
let synth_compositeDeviceID_payload_t
  (x': compositeDeviceID_payload_t')
: GTot (compositeDeviceID_payload_t)
= { l0_version  = fst (fst x');
    l0_deviceID = snd (fst x');
    l0_fwid     = snd x' }

inline_for_extraction noextract
let synth_compositeDeviceID_payload_t'
  (x: compositeDeviceID_payload_t)
: Tot (x': compositeDeviceID_payload_t' { x == synth_compositeDeviceID_payload_t x' })
= ((x.l0_version, x.l0_deviceID), x.l0_fwid)

let parse_compositeDeviceID_payload
= parse_asn1_TLV_of_type INTEGER
  `nondep_then`
  parse_subjectPublicKeyInfo
  `nondep_then`
  parse_fwid
  `parse_synth`
  synth_compositeDeviceID_payload_t

let serialize_compositeDeviceID_payload
= serialize_synth
  (* p1 *) (parse_asn1_TLV_of_type INTEGER
            `nondep_then`
            parse_subjectPublicKeyInfo
            `nondep_then`
            parse_fwid)
  (* f2 *) (synth_compositeDeviceID_payload_t)
  (* s1 *) (serialize_asn1_TLV_of_type INTEGER
            `serialize_nondep_then`
            serialize_subjectPublicKeyInfo
            `serialize_nondep_then`
            serialize_fwid)
  (* g1 *) (synth_compositeDeviceID_payload_t')
  (* prf*) ()

let lemma_serialize_compositeDeviceID_payload_unfold x
= serialize_nondep_then_eq
  (* s1 *) (serialize_asn1_TLV_of_type INTEGER)
  (* s2 *) (serialize_subjectPublicKeyInfo)
  (* in *) (fst (synth_compositeDeviceID_payload_t' x));
  serialize_nondep_then_eq
  (* s1 *) (serialize_asn1_TLV_of_type INTEGER
            `serialize_nondep_then`
            serialize_subjectPublicKeyInfo)
  (* s2 *) (serialize_fwid)
  (* in *) (synth_compositeDeviceID_payload_t' x);
  serialize_synth_eq
  (* p1 *) (parse_asn1_TLV_of_type INTEGER
            `nondep_then`
            parse_subjectPublicKeyInfo
            `nondep_then`
            parse_fwid)
  (* f2 *) (synth_compositeDeviceID_payload_t)
  (* s1 *) (serialize_asn1_TLV_of_type INTEGER
            `serialize_nondep_then`
            serialize_subjectPublicKeyInfo
            `serialize_nondep_then`
            serialize_fwid)
  (* g1 *) (synth_compositeDeviceID_payload_t')
  (* prf*) ()
  (* in *) x
/
X509.Crypto.fst.checked X509.BasicFields.SubjectPublicKeyInfo.fsti.checked X509.Base.fst.checked prims.fst.checked LowParse.Low.Combinators.fsti.checked LowParse.Low.Base.fst.checked L0.X509.FWID.fsti.checked L0.X509.Base.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Integers.fst.checked ASN1.Spec.fst.checked ASN1.Low.fst.checked
L0.X509.CompositeDeviceID.fst
x: L0.X509.CompositeDeviceID.compositeDeviceID_payload_t
  -> FStar.Pervasives.Lemma
    (ensures
      ASN1.Spec.Base.length_of_opaque_serialization L0.X509.CompositeDeviceID.serialize_compositeDeviceID_payload
        x ==
      ASN1.Spec.TLV.length_of_asn1_primitive_TLV (MkcompositeDeviceID_payload_t?.l0_version x) +
      ASN1.Spec.Base.length_of_opaque_serialization X509.BasicFields.SubjectPublicKeyInfo.serialize_subjectPublicKeyInfo
        (MkcompositeDeviceID_payload_t?.l0_deviceID x) +
      ASN1.Spec.Base.length_of_opaque_serialization L0.X509.FWID.serialize_fwid
        (MkcompositeDeviceID_payload_t?.l0_fwid x) /\
      ASN1.Spec.Base.length_of_opaque_serialization L0.X509.CompositeDeviceID.serialize_compositeDeviceID_payload
        x ==
      ASN1.Spec.TLV.length_of_asn1_primitive_TLV (MkcompositeDeviceID_payload_t?.l0_version x) + 91 /\
      ASN1.Spec.Base.length_of_opaque_serialization L0.X509.CompositeDeviceID.serialize_compositeDeviceID_payload
        x <=
      97)
L0.X509.CompositeDeviceID.compositeDeviceID_payload_t L0.X509.FWID.lemma_serialize_fwid_size_exact L0.X509.CompositeDeviceID.__proj__MkcompositeDeviceID_payload_t__item__l0_fwid Prims.unit X509.BasicFields.SubjectPublicKeyInfo.lemma_serialize_subjectPublicKeyInfo_size_exact L0.X509.CompositeDeviceID.__proj__MkcompositeDeviceID_payload_t__item__l0_deviceID L0.X509.CompositeDeviceID.lemma_serialize_compositeDeviceID_payload_unfold
let lemma_serialize_compositeDeviceID_payload_size x =
  
lemma_serialize_compositeDeviceID_payload_unfold x;
lemma_serialize_subjectPublicKeyInfo_size_exact x.l0_deviceID;
lemma_serialize_fwid_size_exact x.l0_fwid