val 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'})
val 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'})
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)
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' }
/
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: L0.X509.Extension.l0_extension_payload_t
  -> x':
    X509.BasicFields.Extension.x509_extension_t' ASN1.Base.OID_RIOT
      L0.X509.CompositeDeviceID.serialize_compositeDeviceID
      {x == L0.X509.Extension.synth_l0_extension_payload_t x'}
L0.X509.Extension.l0_extension_payload_t FStar.Pervasives.Native.Mktuple2 FStar.Pervasives.Native.tuple2 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.OID_RIOT ASN1.Base.BOOLEAN ASN1.Spec.Value.Envelop.inbound_envelop_tag_with_value_of 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.OCTET_STRING L0.X509.CompositeDeviceID.serialize_compositeDeviceID L0.X509.Extension.__proj__Mkl0_extension_payload_t__item__x509_extID_l0 L0.X509.Extension.__proj__Mkl0_extension_payload_t__item__x509_extCritical_l0 L0.X509.Extension.__proj__Mkl0_extension_payload_t__item__x509_extValue_l0 X509.BasicFields.Extension.x509_extension_t' Prims.eq2 L0.X509.Extension.synth_l0_extension_payload_t
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)