val parse_compositeDeviceID_payload
: parser parse_compositeDeviceID_payload_kind (compositeDeviceID_payload_t)
val parse_compositeDeviceID_payload
: parser parse_compositeDeviceID_payload_kind (compositeDeviceID_payload_t)
let parse_compositeDeviceID_payload
= parse_asn1_TLV_of_type INTEGER
  `nondep_then`
  parse_subjectPublicKeyInfo
  `nondep_then`
  parse_fwid
  `parse_synth`
  synth_compositeDeviceID_payload_t
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)
/
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
LowParse.Spec.Base.parser L0.X509.CompositeDeviceID.parse_compositeDeviceID_payload_kind
  L0.X509.CompositeDeviceID.compositeDeviceID_payload_t
LowParse.Spec.Combinators.parse_synth 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 FStar.Pervasives.Native.tuple2 ASN1.Base.datatype_of_asn1_type X509.BasicFields.SubjectPublicKeyInfo.subjectPublicKeyInfo_t L0.X509.FWID.fwid_t L0.X509.CompositeDeviceID.compositeDeviceID_payload_t LowParse.Spec.Combinators.nondep_then ASN1.Spec.TLV.parse_asn1_TLV_of_type X509.BasicFields.SubjectPublicKeyInfo.parse_subjectPublicKeyInfo L0.X509.FWID.parse_fwid L0.X509.CompositeDeviceID.synth_compositeDeviceID_payload_t
let parse_compositeDeviceID_payload =
  
(((parse_asn1_TLV_of_type INTEGER) `nondep_then` parse_subjectPublicKeyInfo)
  `nondep_then`
  parse_fwid)
`parse_synth`
synth_compositeDeviceID_payload_t