val parse_compositeDeviceID_payload_kind:parser_kind
val parse_compositeDeviceID_payload_kind:parser_kind
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
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 }
/
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_kind
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
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)