val serialize_x509_extension
  (#k: parser_kind)
  (#t: Type0)
  (#p: parser k t)
  (oid: datatype_of_asn1_type OID)
  (s: serializer p)
: serializer (parse_x509_extension oid s)
val serialize_x509_extension
  (#k: parser_kind)
  (#t: Type0)
  (#p: parser k t)
  (oid: datatype_of_asn1_type OID)
  (s: serializer p)
: serializer (parse_x509_extension oid s)
let serialize_x509_extension #k #t #p oid s
= coerce_parser_serializer
    (parse_x509_extension oid s)
    (serialize_asn1_sequence_TLV
    (* s *) (serialize_x509_extension_payload oid s))
    ()
module X509.BasicFields.Extension2

open LowParse.Spec.Base
open LowParse.Spec.Combinators

open ASN1.Base
open ASN1.Spec
open ASN1.Low

open X509.Base

open FStar.Integers

module B32 = FStar.Bytes

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

let parse_x509_extension_payload #k #t #p oid s
=
  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)

let serialize_x509_extension_payload #k #t #p oid s
= (serialize_asn1_oid_TLV_of oid
   `serialize_nondep_then`
   serialize_asn1_TLV_of_type BOOLEAN
   `serialize_nondep_then`
  (OCTET_STRING
   `serialize_asn1_envelop_tag_with_TLV`
   s))

let lemma_serialize_x509_extension_payload_unfold #k #t #p oid s x
= serialize_nondep_then_eq
  (* s1 *) (serialize_asn1_oid_TLV_of oid)
  (* s2 *) (serialize_asn1_TLV_of_type BOOLEAN)
  (* in *) (fst x);
  serialize_nondep_then_eq
  (* s1 *) (serialize_asn1_oid_TLV_of oid
            `serialize_nondep_then`
            serialize_asn1_TLV_of_type BOOLEAN)
  (* s2 *) (OCTET_STRING
            `serialize_asn1_envelop_tag_with_TLV`
            s)
  (* in *) (x)

let lemma_serialize_x509_extension_payload_size #k #t #p oid s x
= lemma_serialize_x509_extension_payload_unfold oid s x;
  lemma_serialize_asn1_oid_TLV_of_size oid (fst (fst x));
  lemma_serialize_asn1_envelop_tag_with_TLV_size
    OCTET_STRING
    s
    (snd x);
  lemma_serialize_asn1_boolean_TLV_size (snd (fst x))

(*
 * X.509 Extension Combinators
 *)

let parse_x509_extension #k #t #p oid s
= x509_extension_t oid s
  `coerce_parser`
  parse_asn1_sequence_TLV
  (* s *) (serialize_x509_extension_payload oid s)
/
X509.Base.fst.checked prims.fst.checked LowParse.Spec.Combinators.fsti.checked LowParse.Spec.Base.fsti.checked FStar.Pervasives.fsti.checked FStar.Integers.fst.checked FStar.Bytes.fsti.checked ASN1.Spec.fst.checked ASN1.Low.fst.checked ASN1.Base.fst.checked
X509.BasicFields.Extension2.fst
oid: ASN1.Base.datatype_of_asn1_type ASN1.Base.OID -> s: LowParse.Spec.Base.serializer p
  -> LowParse.Spec.Base.serializer (X509.BasicFields.Extension2.parse_x509_extension oid s)
LowParse.Spec.Base.parser_kind LowParse.Spec.Base.parser ASN1.Base.datatype_of_asn1_type ASN1.Base.OID LowParse.Spec.Base.serializer ASN1.Spec.Base.coerce_parser_serializer X509.BasicFields.Extension2.x509_extension_t X509.BasicFields.Extension2.parse_x509_extension_kind ASN1.Spec.Value.SEQUENCE.inbound_sequence_value_of X509.BasicFields.Extension2.parse_x509_extension_payload_kind X509.BasicFields.Extension2.x509_extension_payload_t FStar.Ghost.hide X509.BasicFields.Extension2.parse_x509_extension_payload X509.BasicFields.Extension2.serialize_x509_extension_payload ASN1.Spec.Value.SEQUENCE.parse_asn1_sequence_TLV X509.BasicFields.Extension2.parse_x509_extension ASN1.Spec.Value.SEQUENCE.serialize_asn1_sequence_TLV
let serialize_x509_extension #k #t #p oid s =
  
coerce_parser_serializer (parse_x509_extension oid s)
  (serialize_asn1_sequence_TLV (serialize_x509_extension_payload oid s))
  ()