val len_of_aliasKeyTBS_extensions_basicConstraints: Prims.unit
  -> Tot
    (len:
      asn1_TLV_int32_of_type SEQUENCE
        {v len == length_of_aliasKeyTBS_extensions_basicConstraints ()})
val len_of_aliasKeyTBS_extensions_basicConstraints: Prims.unit
  -> Tot
    (len:
      asn1_TLV_int32_of_type SEQUENCE
        {v len == length_of_aliasKeyTBS_extensions_basicConstraints ()})
let len_of_aliasKeyTBS_extensions_basicConstraints ()
: Tot (len: asn1_TLV_int32_of_type SEQUENCE
            { v len == length_of_aliasKeyTBS_extensions_basicConstraints () })
= len_of_x509_basicConstraints aliasKeyTBS_extensions_basicConstraints_isCA
module L0.X509.AliasKeyTBS.Extensions.BasicConstraints

open ASN1.Spec
open ASN1.Low
open X509
open FStar.Integers

module B32 = FStar.Bytes

#set-options "--z3rlimit 64 --fuel 0 --ifuel 0"

noextract inline_for_extraction
let aliasKeyTBS_extensions_basicConstraints_isCA: bool = false

let aliasKeyTBS_extensions_basicConstraints_t: Type
= x509_basicConstraints_t aliasKeyTBS_extensions_basicConstraints_isCA

let parse_aliasKeyTBS_extensions_basicConstraints
// : parser parse_x509_extension_kind aliasKeyTBS_extensions_basicConstraints_t
= aliasKeyTBS_extensions_basicConstraints_t
  `coerce_parser`
  parse_x509_basicConstraints aliasKeyTBS_extensions_basicConstraints_isCA

let serialize_aliasKeyTBS_extensions_basicConstraints
: serializer parse_aliasKeyTBS_extensions_basicConstraints
= coerce_parser_serializer
    (parse_aliasKeyTBS_extensions_basicConstraints)
    (serialize_x509_basicConstraints aliasKeyTBS_extensions_basicConstraints_isCA)
    ()

//noextract inline_for_extraction
let serialize32_aliasKeyTBS_extensions_basicConstraints_backwards
: serializer32_backwards serialize_aliasKeyTBS_extensions_basicConstraints
= coerce_serializer32_backwards
    (serialize_aliasKeyTBS_extensions_basicConstraints)
    (serialize32_x509_basicConstraints_backwards aliasKeyTBS_extensions_basicConstraints_isCA)
    ()

let length_of_aliasKeyTBS_extensions_basicConstraints ()
: GTot (asn1_TLV_length_of_type SEQUENCE)
= length_of_x509_basicConstraints aliasKeyTBS_extensions_basicConstraints_isCA

noextract inline_for_extraction unfold
/
X509.fst.checked prims.fst.checked FStar.Pervasives.fsti.checked FStar.Integers.fst.checked FStar.Bytes.fsti.checked ASN1.Spec.fst.checked ASN1.Low.fst.checked
L0.X509.AliasKeyTBS.Extensions.BasicConstraints.fst
_: Prims.unit
  -> len:
    ASN1.Base.asn1_TLV_int32_of_type ASN1.Base.SEQUENCE
      { FStar.Integers.v len ==
        L0.X509.AliasKeyTBS.Extensions.BasicConstraints.length_of_aliasKeyTBS_extensions_basicConstraints
          () }
Prims.unit X509.ExtFields.BasicConstraints.len_of_x509_basicConstraints L0.X509.AliasKeyTBS.Extensions.BasicConstraints.aliasKeyTBS_extensions_basicConstraints_isCA ASN1.Base.asn1_TLV_int32_of_type ASN1.Base.SEQUENCE 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 L0.X509.AliasKeyTBS.Extensions.BasicConstraints.length_of_aliasKeyTBS_extensions_basicConstraints
let len_of_aliasKeyTBS_extensions_basicConstraints ()
    : Tot
    (len:
      asn1_TLV_int32_of_type SEQUENCE
        {v len == length_of_aliasKeyTBS_extensions_basicConstraints ()}) =
  
len_of_x509_basicConstraints aliasKeyTBS_extensions_basicConstraints_isCA