val lemma_serialize_x509_extension_payload_unfold
  (#k: parser_kind)
  (#t: Type0)
  (#p: parser k t)
  (oid: datatype_of_asn1_type OID)
  (s: serializer p)
  (x: x509_extension_payload_t oid s)
: Lemma (
  serialize (serialize_x509_extension_payload oid s) x ==
  serialize (serialize_asn1_oid_TLV_of oid) (fst (fst x))
  `Seq.append`
  serialize (serialize_asn1_TLV_of_type BOOLEAN) (snd (fst x))
  `Seq.append`
  serialize (OCTET_STRING `serialize_asn1_envelop_tag_with_TLV` s) (snd x)
)
val lemma_serialize_x509_extension_payload_unfold
  (#k: parser_kind)
  (#t: Type0)
  (#p: parser k t)
  (oid: datatype_of_asn1_type OID)
  (s: serializer p)
  (x: x509_extension_payload_t oid s)
: Lemma (
  serialize (serialize_x509_extension_payload oid s) x ==
  serialize (serialize_asn1_oid_TLV_of oid) (fst (fst x))
  `Seq.append`
  serialize (serialize_asn1_TLV_of_type BOOLEAN) (snd (fst x))
  `Seq.append`
  serialize (OCTET_STRING `serialize_asn1_envelop_tag_with_TLV` s) (snd x)
)
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)
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))
/
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_payload_t oid (FStar.Ghost.hide s)
  -> FStar.Pervasives.Lemma
    (ensures
      LowParse.Spec.Base.serialize (X509.BasicFields.Extension2.serialize_x509_extension_payload oid
            s)
        x ==
      FStar.Seq.Base.append (FStar.Seq.Base.append (LowParse.Spec.Base.serialize (ASN1.Spec.Value.OID.serialize_asn1_oid_TLV_of
                    oid)
                (FStar.Pervasives.Native.fst (FStar.Pervasives.Native.fst x)))
            (LowParse.Spec.Base.serialize (ASN1.Spec.TLV.serialize_asn1_TLV_of_type ASN1.Base.BOOLEAN
                  )
                (FStar.Pervasives.Native.snd (FStar.Pervasives.Native.fst x))))
        (LowParse.Spec.Base.serialize (ASN1.Spec.Value.Envelop.serialize_asn1_envelop_tag_with_TLV ASN1.Base.OCTET_STRING
                s)
            (FStar.Pervasives.Native.snd x)))
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_payload_t FStar.Ghost.hide LowParse.Spec.Combinators.serialize_nondep_then_eq 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 FStar.Pervasives.Native.tuple2 ASN1.Spec.Value.OID.the_asn1_oid LowParse.Spec.Combinators.nondep_then ASN1.Spec.Value.OID.parse_asn1_oid_TLV_of ASN1.Spec.TLV.parse_asn1_TLV_of_type LowParse.Spec.Combinators.serialize_nondep_then ASN1.Spec.Value.OID.serialize_asn1_oid_TLV_of ASN1.Spec.TLV.serialize_asn1_TLV_of_type ASN1.Spec.Value.Envelop.parse_asn1_envelop_tag_with_TLV_kind ASN1.Base.OCTET_STRING ASN1.Spec.Value.Envelop.inbound_envelop_tag_with_value_of ASN1.Spec.Value.Envelop.parse_asn1_envelop_tag_with_TLV ASN1.Spec.Value.Envelop.serialize_asn1_envelop_tag_with_TLV Prims.unit FStar.Pervasives.Native.fst LowParse.Spec.Combinators.parse_filter_refine ASN1.Spec.Value.OID.filter_asn1_oid_TLV_of FStar.Ghost.reveal
let lemma_serialize_x509_extension_payload_unfold #k #t #p oid s x =
  
serialize_nondep_then_eq (serialize_asn1_oid_TLV_of oid)
  (serialize_asn1_TLV_of_type BOOLEAN)
  (fst x);
serialize_nondep_then_eq ((serialize_asn1_oid_TLV_of oid)
    `serialize_nondep_then`
    (serialize_asn1_TLV_of_type BOOLEAN))
  (OCTET_STRING `serialize_asn1_envelop_tag_with_TLV` s)
  (x)