val parse_x509_extension_kind : LowParse.Spec.Base.parser_kind
let parse_x509_extension_kind
= parse_asn1_TLV_kind_of_type OID
  `and_then_kind`
  parse_asn1_TLV_kind_of_type BOOLEAN
  `and_then_kind`
  parse_asn1_envelop_tag_with_TLV_kind OCTET_STRING
module X509.BasicFields.Extension

open ASN1.Spec

open X509.Base

// 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 *)
/// tuple repr
let x509_extension_t'
  (#k: parser_kind)
  (#t: Type0)
  (#p: parser k t)
  (oid: datatype_of_asn1_type OID)
  (s: serializer p)
= parse_filter_refine (filter_asn1_oid_TLV_of oid)
  `tuple2`
  datatype_of_asn1_type BOOLEAN
  `tuple2`
 (OCTET_STRING `inbound_envelop_tag_with_value_of` s)

// 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.Seq.fst.checked FStar.Pervasives.fsti.checked ASN1.Spec.fst.checked ASN1.Low.fst.checked
X509.BasicFields.Extension.fsti
LowParse.Spec.Base.parser_kind
LowParse.Spec.Combinators.and_then_kind ASN1.Spec.TLV.parse_asn1_TLV_kind_of_type ASN1.Base.OID ASN1.Base.BOOLEAN ASN1.Spec.Value.Envelop.parse_asn1_envelop_tag_with_TLV_kind ASN1.Base.OCTET_STRING
let parse_x509_extension_kind =
  
((parse_asn1_TLV_kind_of_type OID) `and_then_kind` (parse_asn1_TLV_kind_of_type BOOLEAN))
`and_then_kind`
(parse_asn1_envelop_tag_with_TLV_kind OCTET_STRING)