val parse_l0_extension_payload:parser parse_x509_extension_kind l0_extension_payload_t
val parse_l0_extension_payload:parser parse_x509_extension_kind l0_extension_payload_t
let parse_l0_extension_payload
: parser parse_x509_extension_kind l0_extension_payload_t
= parse_x509_extension
    OID_RIOT
    serialize_compositeDeviceID
    synth_l0_extension_payload_t
    ()
module L0.X509.Extension

open ASN1.Spec
open ASN1.Low
open X509.BasicFields.Extension
include L0.X509.CompositeDeviceID

open FStar.Integers

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

type l0_extension_payload_t: Type
= { x509_extID_l0      : x:datatype_of_asn1_type OID {x == OID_RIOT};
    x509_extCritical_l0: datatype_of_asn1_type BOOLEAN;
    x509_extValue_l0   : OCTET_STRING `inbound_envelop_tag_with_value_of`
                           (**) serialize_compositeDeviceID }

let synth_l0_extension_payload_t
  (x': x509_extension_t' OID_RIOT serialize_compositeDeviceID)
: GTot (l0_extension_payload_t)
= { x509_extID_l0       = fst (fst x');
    x509_extCritical_l0 = snd (fst x');
    x509_extValue_l0    = snd x' }

inline_for_extraction noextract
let synth_l0_extension_payload_t_inverse
  (x: l0_extension_payload_t)
: Tot (x': x509_extension_t' OID_RIOT serialize_compositeDeviceID
           { x == synth_l0_extension_payload_t x' })
= ((x.x509_extID_l0,
    x.x509_extCritical_l0),
    x.x509_extValue_l0)
/
X509.BasicFields.Extension.fsti.checked prims.fst.checked L0.X509.LengthUtils.fst.checked L0.X509.CompositeDeviceID.fsti.checked FStar.UInt32.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.Extension.fst
LowParse.Spec.Base.parser X509.BasicFields.Extension.parse_x509_extension_kind
  L0.X509.Extension.l0_extension_payload_t
X509.BasicFields.Extension.parse_x509_extension ASN1.Spec.Value.Envelop.parse_asn1_envelop_tag_with_TLV_kind ASN1.Base.SEQUENCE L0.X509.CompositeDeviceID.compositeDeviceID_t L0.X509.CompositeDeviceID.parse_compositeDeviceID ASN1.Base.OID_RIOT L0.X509.CompositeDeviceID.serialize_compositeDeviceID L0.X509.Extension.l0_extension_payload_t L0.X509.Extension.synth_l0_extension_payload_t
let parse_l0_extension_payload:parser parse_x509_extension_kind l0_extension_payload_t =
  
parse_x509_extension OID_RIOT serialize_compositeDeviceID synth_l0_extension_payload_t ()