val parse_x509_extension
  (#k: parser_kind)
  (#t: Type0)
  (#p: parser k t)
  (oid: datatype_of_asn1_type OID)
  (s: serializer p)
  (#instance_t: Type0)
  (f: x509_extension_t' oid s -> GTot instance_t)
  (prf: unit{synth_injective f})
: parser parse_x509_extension_kind (instance_t)
val parse_x509_extension
  (#k: parser_kind)
  (#t: Type0)
  (#p: parser k t)
  (oid: datatype_of_asn1_type OID)
  (s: serializer p)
  (#instance_t: Type0)
  (f: x509_extension_t' oid s -> GTot instance_t)
  (prf: unit{synth_injective f})
: parser parse_x509_extension_kind (instance_t)
let parse_x509_extension #k #t #p oid s #instance_t f prf
=
  parse_asn1_oid_TLV_of oid
  `nondep_then`
  parse_asn1_TLV_of_type BOOLEAN
  `nondep_then`
 (OCTET_STRING
  `parse_asn1_envelop_tag_with_TLV`
  s)
  `parse_synth`
  (prf; f)
module X509.BasicFields.Extension

open X509.Base

#set-options "--z3rlimit 32 --fuel 0 --ifuel 0"

// inline_for_extraction
// type x509_extension_t
//   (#k: parser_kind)
//   (#t: Type0)
//   (#p: parser k t)
//   (oid: datatype_of_asn1_type OID)
//   (s: serializer p)
// = { x509_extID      : x:datatype_of_asn1_type OID {x == oid};
//     x509_extCritical: datatype_of_asn1_type BOOLEAN;
//     x509_extValue   : OCTET_STRING `inbound_envelop_tag_with_value_of` s }

(* one extension *)

// let synth_x509_extension_t
//   (#k: parser_kind)
//   (#t: Type0)
//   (#p: parser k t)
//   (oid: datatype_of_asn1_type OID)
//   (s: serializer p)
//   (x': x509_extension_t' oid s)
// : GTot (x509_extension_t oid s)
// = { x509_extID       = fst (fst x');
//     x509_extCritical = snd (fst x');
//     x509_extValue    = snd x' }

// let synth_x509_extension_t'
//   (#k: parser_kind)
//   (#t: Type0)
//   (#p: parser k t)
//   (oid: datatype_of_asn1_type OID)
//   (s: serializer p)
//   (x: x509_extension_t oid s)
// : GTot (x': x509_extension_t' oid s { x == synth_x509_extension_t oid s x' })
// = (x.x509_extID, x.x509_extCritical), x.x509_extValue
/
X509.Base.fst.checked prims.fst.checked FStar.Pervasives.fsti.checked ASN1.Low.fst.checked
X509.BasicFields.Extension.fst

    oid: ASN1.Base.datatype_of_asn1_type ASN1.Base.OID ->
    s: LowParse.Spec.Base.serializer p ->
    f: (_: X509.BasicFields.Extension.x509_extension_t' oid s -> Prims.GTot instance_t) ->
    prf: Prims.unit{LowParse.Spec.Combinators.synth_injective f}
  -> LowParse.Spec.Base.parser X509.BasicFields.Extension.parse_x509_extension_kind instance_t
LowParse.Spec.Base.parser_kind LowParse.Spec.Base.parser ASN1.Base.datatype_of_asn1_type ASN1.Base.OID LowParse.Spec.Base.serializer X509.BasicFields.Extension.x509_extension_t' Prims.unit LowParse.Spec.Combinators.synth_injective LowParse.Spec.Combinators.parse_synth LowParse.Spec.Combinators.and_then_kind LowParse.Spec.Combinators.parse_filter_kind ASN1.Spec.Value.OID.parse_asn1_oid_TLV_kind ASN1.Spec.TLV.parse_asn1_TLV_kind_of_type ASN1.Base.BOOLEAN ASN1.Spec.Value.Envelop.parse_asn1_envelop_tag_with_TLV_kind ASN1.Base.OCTET_STRING FStar.Pervasives.Native.tuple2 ASN1.Spec.Value.OID.the_asn1_oid ASN1.Spec.Value.Envelop.inbound_envelop_tag_with_value_of LowParse.Spec.Combinators.nondep_then ASN1.Spec.Value.OID.parse_asn1_oid_TLV_of ASN1.Spec.TLV.parse_asn1_TLV_of_type ASN1.Spec.Value.Envelop.parse_asn1_envelop_tag_with_TLV X509.BasicFields.Extension.parse_x509_extension_kind
let parse_x509_extension #k #t #p oid s #instance_t f prf =
  
(((parse_asn1_oid_TLV_of oid) `nondep_then` (parse_asn1_TLV_of_type BOOLEAN))
  `nondep_then`
  (OCTET_STRING `parse_asn1_envelop_tag_with_TLV` s))
`parse_synth`
(prf;
  f)