val parse_aliasKeyTBS_extensions_payload_kind:parser_kind
val parse_aliasKeyTBS_extensions_payload_kind:parser_kind
let parse_aliasKeyTBS_extensions_payload_kind
: parser_kind
= parse_asn1_envelop_tag_with_TLV_kind SEQUENCE
  `and_then_kind`
  X509.BasicFields.Extension2.parse_x509_extension_kind
  `and_then_kind`
  X509.BasicFields.Extension2.parse_x509_extension_kind
  `and_then_kind`
  X509.BasicFields.Extension2.parse_x509_extension_kind
  `and_then_kind`
  parse_x509_extension_sequence_TLV_kind
module L0.X509.AliasKeyTBS.Extensions

open ASN1.Spec
open ASN1.Low
open X509
open L0.X509.Base
open L0.X509.FWID
open L0.X509.CompositeDeviceID
open L0.X509.Extension
open L0.X509.AliasKeyTBS.Extensions.BasicConstraints
open L0.X509.AliasKeyTBS.Extensions.AuthKeyIdentifier
open L0.X509.AliasKeyTBS.Extensions.ExtendedKeyUsage
open FStar.Integers

module B32 = FStar.Bytes

#set-options "--z3rlimit 128 --fuel 0 --ifuel 0 --using_facts_from '* -FStar.Tactics -FStar.Reflection'"

val decl : unit

(* Extensions of the AliasKey Certificate
 * Includes the L0 Extension (`CompositeDeviceID`) and others
 * This is the SEQUENCE under the outmost explicit tag
 * Contains SEQUENCEs of individual extensions ({extID, extValue})
 * [3] {               <--- The outmost explicit tag
 *   SEQUENCE {        <--- *HERE*
 *     SEQUENCE {      <--- Individual extension
 *       extID   : OID
 *       extValue: OCTET STRING {..}  <--- Actual extension content enveloped by tag OCTET STRING
 *     };
 *     SEQUENCE {..};
 *     SEQUENCE {..};  <--- Other extensions
 *   }
 * }
 *)

noeq
type aliasKeyTBS_extensions_payload_t = {
  (* More extensions could be added here.
   * For example:
   * aliasKeyTBS_extensions_key_usage: key_usage_t;
   *)
  aliasKeyTBS_extensions_key_usage: key_usage_t;
  aliasKeyTBS_extensions_extendedKeyUsage: aliasKeyTBS_extensions_extendedKeyUsage_t;
                                           //P.norm
                                           // (norm_steps_x509_keyPurposeIDs (`%aliasKeyCrt_extendedKeyUsage_oids))
                                           // (x509_ext_key_usage_t aliasKeyCrt_extendedKeyUsage_oids);
  aliasKeyTBS_extensions_basicConstraints: aliasKeyTBS_extensions_basicConstraints_t;
  aliasKeyTBS_extensions_authKeyID: aliasKeyTBS_extensions_authKeyID_t;
  aliasKeyTBS_extensions_l0: l0_extension_t
}
/
X509.BasicFields.Extension2.fsti.checked X509.fst.checked prims.fst.checked L0.X509.FWID.fsti.checked L0.X509.Extension.fst.checked L0.X509.CompositeDeviceID.fsti.checked L0.X509.Base.fst.checked L0.X509.AliasKeyTBS.Extensions.ExtendedKeyUsage.fst.checked L0.X509.AliasKeyTBS.Extensions.BasicConstraints.fst.checked L0.X509.AliasKeyTBS.Extensions.AuthKeyIdentifier.fst.checked FStar.UInt32.fsti.checked FStar.Seq.fst.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
L0.X509.AliasKeyTBS.Extensions.fsti
LowParse.Spec.Base.parser_kind
LowParse.Spec.Combinators.and_then_kind ASN1.Spec.Value.Envelop.parse_asn1_envelop_tag_with_TLV_kind ASN1.Base.SEQUENCE X509.BasicFields.Extension2.parse_x509_extension_kind X509.BasicFields.Extension.parse_x509_extension_sequence_TLV_kind
let parse_aliasKeyTBS_extensions_payload_kind:parser_kind =
  
((((parse_asn1_envelop_tag_with_TLV_kind SEQUENCE)
      `and_then_kind`
      X509.BasicFields.Extension2.parse_x509_extension_kind)
    `and_then_kind`
    X509.BasicFields.Extension2.parse_x509_extension_kind)
  `and_then_kind`
  X509.BasicFields.Extension2.parse_x509_extension_kind)
`and_then_kind`
parse_x509_extension_sequence_TLV_kind