val lemma_serialize_x509_extension_size_exact
  (#k: parser_kind)
  (#t: Type0)
  (#p: parser k t)
  (oid: datatype_of_asn1_type OID)
  (s: serializer p)
  (x: x509_extension_t oid s)
  (x_length: asn1_value_length_of_type OCTET_STRING
             { length_of_opaque_serialization s (snd x) == x_length /\
               length_of_x509_extension_payload_unbounded oid s (snd x) x_length
               <= asn1_value_length_max_of_type SEQUENCE })
: Lemma (
  length_of_opaque_serialization (serialize_x509_extension oid s) x ==
  length_of_x509_extension oid s (snd x) x_length
)
val lemma_serialize_x509_extension_size_exact
  (#k: parser_kind)
  (#t: Type0)
  (#p: parser k t)
  (oid: datatype_of_asn1_type OID)
  (s: serializer p)
  (x: x509_extension_t oid s)
  (x_length: asn1_value_length_of_type OCTET_STRING
             { length_of_opaque_serialization s (snd x) == x_length /\
               length_of_x509_extension_payload_unbounded oid s (snd x) x_length
               <= asn1_value_length_max_of_type SEQUENCE })
: Lemma (
  length_of_opaque_serialization (serialize_x509_extension oid s) x ==
  length_of_x509_extension oid s (snd x) x_length
)
let lemma_serialize_x509_extension_size_exact #k #t #p oid s x x_length
= lemma_serialize_x509_extension_size oid s x;
  lemma_serialize_x509_extension_payload_size oid s x
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)

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))
    ()

/// Helpers
///

let lemma_serialize_x509_extension_unfold #k #t #p oid s x
= lemma_serialize_asn1_sequence_TLV_unfold
  (* s *) (serialize_x509_extension_payload oid s)
  x

let lemma_serialize_x509_extension_size #k #t #p oid s x
= lemma_serialize_asn1_sequence_TLV_size
  (* s *) (serialize_x509_extension_payload oid s)
  x
/
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 ->
    x: X509.BasicFields.Extension2.x509_extension_t oid s ->
    x_length:
      ASN1.Base.asn1_value_length_of_type ASN1.Base.OCTET_STRING
        { ASN1.Spec.Base.length_of_opaque_serialization s (FStar.Pervasives.Native.snd x) ==
          x_length /\
          X509.BasicFields.Extension2.length_of_x509_extension_payload_unbounded oid
            s
            (FStar.Pervasives.Native.snd x)
            x_length <=
          ASN1.Base.asn1_value_length_max_of_type ASN1.Base.SEQUENCE }
  -> FStar.Pervasives.Lemma
    (ensures
      ASN1.Spec.Base.length_of_opaque_serialization (X509.BasicFields.Extension2.serialize_x509_extension
            oid
            s)
        x ==
      X509.BasicFields.Extension2.length_of_x509_extension oid
        s
        (FStar.Pervasives.Native.snd x)
        x_length)
LowParse.Spec.Base.parser_kind LowParse.Spec.Base.parser ASN1.Base.datatype_of_asn1_type ASN1.Base.OID LowParse.Spec.Base.serializer X509.BasicFields.Extension2.x509_extension_t ASN1.Base.asn1_value_length_of_type ASN1.Base.OCTET_STRING Prims.l_and Prims.eq2 Prims.nat ASN1.Spec.Base.length_of_opaque_serialization FStar.Pervasives.Native.snd FStar.Pervasives.Native.tuple2 LowParse.Spec.Combinators.parse_filter_refine ASN1.Spec.Value.OID.filter_asn1_oid_TLV_of ASN1.Base.BOOLEAN ASN1.Spec.Value.Envelop.inbound_envelop_tag_with_value_of FStar.Ghost.reveal FStar.Ghost.hide Prims.b2t FStar.Integers.op_Less_Equals FStar.Integers.Signed FStar.Integers.Winfinite X509.BasicFields.Extension2.length_of_x509_extension_payload_unbounded ASN1.Base.asn1_value_length_max_of_type ASN1.Base.SEQUENCE X509.BasicFields.Extension2.lemma_serialize_x509_extension_payload_size Prims.unit X509.BasicFields.Extension2.lemma_serialize_x509_extension_size
let lemma_serialize_x509_extension_size_exact #k #t #p oid s x x_length =
  
lemma_serialize_x509_extension_size oid s x;
lemma_serialize_x509_extension_payload_size oid s x