val length_of_x509_extensions (l: asn1_value_length_of_type x509_extensions_outmost_explicit_tag)
    : GTot (asn1_TLV_length_of_type x509_extensions_outmost_explicit_tag)
val length_of_x509_extensions (l: asn1_value_length_of_type x509_extensions_outmost_explicit_tag)
    : GTot (asn1_TLV_length_of_type x509_extensions_outmost_explicit_tag)
let length_of_x509_extensions
  (l: asn1_value_length_of_type x509_extensions_outmost_explicit_tag)
: GTot (asn1_TLV_length_of_type x509_extensions_outmost_explicit_tag)
= length_of_TLV x509_extensions_outmost_explicit_tag l
module X509.BasicFields.Extensions

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

let x509_extensions_outmost_explicit_tag: asn1_tag_t
= CUSTOM_TAG CONTEXT_SPECIFIC CONSTRUCTED 3uy

inline_for_extraction
let x509_extensions_t_inbound
  (#k: parser_kind)
  (#t: Type0)
  (#p: parser k t)
  (s: serializer p)
= inbound_envelop_tag_with_value_of
  (* tag *) x509_extensions_outmost_explicit_tag
  (*  s  *) s

let parse_x509_extensions_TLV
  (#k: parser_kind)
  (#t: Type0)
  (#p: parser k t)
  (s: serializer p)
: parser (parse_asn1_envelop_tag_with_TLV_kind x509_extensions_outmost_explicit_tag) (x509_extensions_t_inbound s)
= x509_extensions_t_inbound s
  `coerce_parser`
  parse_asn1_envelop_tag_with_TLV
  (* tag *) x509_extensions_outmost_explicit_tag
  (*  s  *) s

let serialize_x509_extensions_TLV
  (#k: parser_kind)
  (#t: Type0)
  (#p: parser k t)
  (s: serializer p)
: serializer (parse_x509_extensions_TLV s)
= coerce_parser_serializer
  (* p *) (parse_x509_extensions_TLV s)
  (* s *) (serialize_asn1_envelop_tag_with_TLV
           (* tag *) x509_extensions_outmost_explicit_tag
           (*  s  *) s)
  (*prf*) ()

val lemma_serialize_x509_extensions_TLV_unfold
  (#k: parser_kind)
  (#t: Type0)
  (#p: parser k t)
  (s: serializer p)
  (x: x509_extensions_t_inbound s)
: Lemma ( predicate_serialize_asn1_envelop_tag_with_TLV_unfold x509_extensions_outmost_explicit_tag s x )

val lemma_serialize_x509_extensions_TLV_size
  (#k: parser_kind)
  (#t: Type0)
  (#p: parser k t)
  (s: serializer p)
  (x: x509_extensions_t_inbound s)
: Lemma ( predicate_serialize_asn1_envelop_tag_with_TLV_size x509_extensions_outmost_explicit_tag s x )
/
X509.Base.fst.checked prims.fst.checked LowParse.Spec.Combinators.fsti.checked LowParse.Spec.Base.fsti.checked FStar.UInt8.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.Extensions.fsti

    l:
      ASN1.Base.asn1_value_length_of_type X509.BasicFields.Extensions.x509_extensions_outmost_explicit_tag

  -> Prims.GTot
    (ASN1.Base.asn1_TLV_length_of_type X509.BasicFields.Extensions.x509_extensions_outmost_explicit_tag
      )
ASN1.Base.asn1_value_length_of_type X509.BasicFields.Extensions.x509_extensions_outmost_explicit_tag ASN1.Spec.TLV.length_of_TLV ASN1.Base.asn1_TLV_length_of_type
let length_of_x509_extensions (l: asn1_value_length_of_type x509_extensions_outmost_explicit_tag)
    : GTot (asn1_TLV_length_of_type x509_extensions_outmost_explicit_tag) =
  
length_of_TLV x509_extensions_outmost_explicit_tag l