val len_of_x509_extensions
      (len_payload: asn1_value_int32_of_type x509_extensions_outmost_explicit_tag)
    : Tot
    (len:
      asn1_TLV_int32_of_type x509_extensions_outmost_explicit_tag
        {v len == length_of_x509_extensions (v len_payload)})
val len_of_x509_extensions
      (len_payload: asn1_value_int32_of_type x509_extensions_outmost_explicit_tag)
    : Tot
    (len:
      asn1_TLV_int32_of_type x509_extensions_outmost_explicit_tag
        {v len == length_of_x509_extensions (v len_payload)})
let len_of_x509_extensions
  (len_payload: asn1_value_int32_of_type x509_extensions_outmost_explicit_tag)
: Tot (len: asn1_TLV_int32_of_type x509_extensions_outmost_explicit_tag
            { v len == length_of_x509_extensions (v len_payload) })
= len_of_TLV x509_extensions_outmost_explicit_tag len_payload
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 )

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
/
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

    len_payload:
      ASN1.Base.asn1_value_int32_of_type X509.BasicFields.Extensions.x509_extensions_outmost_explicit_tag

  -> len:
    ASN1.Base.asn1_TLV_int32_of_type X509.BasicFields.Extensions.x509_extensions_outmost_explicit_tag

      { FStar.Integers.v len ==
        X509.BasicFields.Extensions.length_of_x509_extensions (FStar.Integers.v len_payload) }
ASN1.Base.asn1_value_int32_of_type X509.BasicFields.Extensions.x509_extensions_outmost_explicit_tag ASN1.Low.TLV.len_of_TLV ASN1.Base.asn1_TLV_int32_of_type Prims.eq2 FStar.Integers.int_t FStar.Integers.Signed FStar.Integers.Winfinite Prims.l_or FStar.Integers.within_bounds FStar.Integers.Unsigned FStar.Integers.W32 Prims.l_and Prims.b2t FStar.Integers.op_Greater_Equals ASN1.Base.asn1_TLV_length_inbound_of_type FStar.Integers.v X509.BasicFields.Extensions.length_of_x509_extensions
let len_of_x509_extensions
      (len_payload: asn1_value_int32_of_type x509_extensions_outmost_explicit_tag)
    : Tot
    (len:
      asn1_TLV_int32_of_type x509_extensions_outmost_explicit_tag
        {v len == length_of_x509_extensions (v len_payload)}) =
  
len_of_TLV x509_extensions_outmost_explicit_tag len_payload