val parse_compositeDeviceID:parser (parse_asn1_envelop_tag_with_TLV_kind SEQUENCE)
  (compositeDeviceID_t)
val parse_compositeDeviceID:parser (parse_asn1_envelop_tag_with_TLV_kind SEQUENCE)
  (compositeDeviceID_t)
let parse_compositeDeviceID
: parser (parse_asn1_envelop_tag_with_TLV_kind SEQUENCE) (compositeDeviceID_t)
= compositeDeviceID_t
  `coerce_parser`
  parse_asn1_sequence_TLV (serialize_compositeDeviceID_payload)
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'"

val decl : unit

(* CompositeDeviceID *)
type compositeDeviceID_payload_t
= { l0_version : datatype_of_asn1_type INTEGER;
    l0_deviceID: subjectPublicKeyInfo_t;
    l0_fwid    : fwid_t }

inline_for_extraction noextract
let parse_compositeDeviceID_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

noextract
val parse_compositeDeviceID_payload
: parser parse_compositeDeviceID_payload_kind (compositeDeviceID_payload_t)

noextract
val serialize_compositeDeviceID_payload
: serializer (parse_compositeDeviceID_payload)

val lemma_serialize_compositeDeviceID_payload_unfold
  (x: compositeDeviceID_payload_t)
: Lemma (
  serialize (serialize_compositeDeviceID_payload) x ==
  serialize (serialize_asn1_TLV_of_type INTEGER) x.l0_version
  `Seq.append`
  serialize (serialize_subjectPublicKeyInfo) x.l0_deviceID
  `Seq.append`
  serialize serialize_fwid x.l0_fwid
)

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
)

(* inbound sub type*)
let compositeDeviceID_t
= inbound_sequence_value_of (serialize_compositeDeviceID_payload)


(* TLV serializer *)
/
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.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.CompositeDeviceID.fsti
LowParse.Spec.Base.parser (ASN1.Spec.Value.Envelop.parse_asn1_envelop_tag_with_TLV_kind ASN1.Base.SEQUENCE
    )
  L0.X509.CompositeDeviceID.compositeDeviceID_t
LowParse.Spec.Base.coerce_parser L0.X509.CompositeDeviceID.compositeDeviceID_t ASN1.Spec.Value.Envelop.parse_asn1_envelop_tag_with_TLV_kind ASN1.Base.SEQUENCE ASN1.Spec.Value.SEQUENCE.inbound_sequence_value_of L0.X509.CompositeDeviceID.parse_compositeDeviceID_payload_kind L0.X509.CompositeDeviceID.compositeDeviceID_payload_t L0.X509.CompositeDeviceID.parse_compositeDeviceID_payload L0.X509.CompositeDeviceID.serialize_compositeDeviceID_payload ASN1.Spec.Value.SEQUENCE.parse_asn1_sequence_TLV
let parse_compositeDeviceID:parser (parse_asn1_envelop_tag_with_TLV_kind SEQUENCE)
  (compositeDeviceID_t) =
  
compositeDeviceID_t `coerce_parser` (parse_asn1_sequence_TLV (serialize_compositeDeviceID_payload))