val synth_l0_extension_payload_t (x': x509_extension_t' OID_RIOT serialize_compositeDeviceID)
    : GTot (l0_extension_payload_t)
val synth_l0_extension_payload_t (x': x509_extension_t' OID_RIOT serialize_compositeDeviceID)
    : GTot (l0_extension_payload_t)
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' }
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 }
/
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

    x':
      X509.BasicFields.Extension.x509_extension_t' ASN1.Base.OID_RIOT
        L0.X509.CompositeDeviceID.serialize_compositeDeviceID
  -> Prims.GTot L0.X509.Extension.l0_extension_payload_t
X509.BasicFields.Extension.x509_extension_t' 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.Mkl0_extension_payload_t FStar.Pervasives.Native.fst LowParse.Spec.Combinators.parse_filter_refine ASN1.Base.datatype_of_asn1_type ASN1.Base.OID ASN1.Spec.Value.OID.filter_asn1_oid_TLV_of ASN1.Base.BOOLEAN FStar.Pervasives.Native.tuple2 ASN1.Spec.Value.Envelop.inbound_envelop_tag_with_value_of ASN1.Base.OCTET_STRING FStar.Pervasives.Native.snd L0.X509.Extension.l0_extension_payload_t
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' }