val lemma_serialize_x509_extension_sequence_TLV_size
  (#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)
  (g: instance_t -> x509_extension_t' oid s)
  (prf: unit{ synth_inverse f g /\
              synth_injective f })
  (x: x509_extension_t_inbound oid s f g prf)
: Lemma ( predicate_serialize_asn1_sequence_TLV_size (serialize_x509_extension oid s f g prf) x )
val lemma_serialize_x509_extension_sequence_TLV_size
  (#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)
  (g: instance_t -> x509_extension_t' oid s)
  (prf: unit{ synth_inverse f g /\
              synth_injective f })
  (x: x509_extension_t_inbound oid s f g prf)
: Lemma ( predicate_serialize_asn1_sequence_TLV_size (serialize_x509_extension oid s f g prf) x )
let lemma_serialize_x509_extension_sequence_TLV_size #k #t #p oid s #instance_t f g prf x
= lemma_serialize_asn1_sequence_TLV_size
  (* s *) (serialize_x509_extension oid s f g prf)
  x
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

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)

let serialize_x509_extension #k #t #p oid s #instance_t f g prf
=
  serialize_synth
  (* p1 *) (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))
  (* f2 *) (f)
  (* s1 *) (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))
  (* g1 *) (g)
  (* prf*) (prf)

let lemma_serialize_x509_extension_unfold #k #t #p oid s #instance_t f g prf x
= serialize_nondep_then_eq
  (* s1 *) (serialize_asn1_oid_TLV_of oid)
  (* s2 *) (serialize_asn1_TLV_of_type BOOLEAN)
  (* in *) (fst (g 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 *) (g x);
  serialize_synth_eq
  (* p1 *) (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))
  (* f2 *) (f)
  (* s1 *) (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))
  (* g1 *) (g)
  (* prf*) (prf)
  (* in *) x

#push-options "--z3rlimit 32 --fuel 4 --ifuel 4"
let lemma_serialize_x509_extension_size #k #t #p oid s #instance_t f g prf x
= lemma_serialize_x509_extension_unfold oid s f g prf x;
  lemma_serialize_asn1_oid_TLV_of_size oid (fst (fst (g x)));
  lemma_serialize_asn1_envelop_tag_with_TLV_size
    OCTET_STRING
    s
    (snd (g x));
  lemma_serialize_asn1_boolean_TLV_size (snd (fst (g x)))
#pop-options

let lemma_serialize_x509_extension_sequence_TLV_unfold #k #t #p oid s #instance_t f g prf x
= lemma_serialize_asn1_sequence_TLV_unfold
  (* s *) (serialize_x509_extension oid s f g prf)
  x
/
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) ->
    g: (_: instance_t -> X509.BasicFields.Extension.x509_extension_t' oid s) ->
    prf:
      Prims.unit
        {LowParse.Spec.Combinators.synth_inverse f g /\ LowParse.Spec.Combinators.synth_injective f} ->
    x: X509.BasicFields.Extension.x509_extension_t_inbound oid s f g prf
  -> FStar.Pervasives.Lemma
    (ensures
      ASN1.Spec.Value.SEQUENCE.predicate_serialize_asn1_sequence_TLV_size (X509.BasicFields.Extension.serialize_x509_extension
            oid
            s
            f
            g
            prf)
        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.Extension.x509_extension_t' Prims.unit Prims.l_and LowParse.Spec.Combinators.synth_inverse LowParse.Spec.Combinators.synth_injective X509.BasicFields.Extension.x509_extension_t_inbound ASN1.Spec.Value.SEQUENCE.lemma_serialize_asn1_sequence_TLV_size X509.BasicFields.Extension.parse_x509_extension_kind X509.BasicFields.Extension.parse_x509_extension X509.BasicFields.Extension.serialize_x509_extension
let lemma_serialize_x509_extension_sequence_TLV_size #k #t #p oid s #instance_t f g prf x =
  
lemma_serialize_asn1_sequence_TLV_size (serialize_x509_extension oid s f g prf) x