val len_of_aliasKeyTBS_payload_max: Prims.unit -> GTot (asn1_value_int32_of_type SEQUENCE)
val len_of_aliasKeyTBS_payload_max: Prims.unit -> GTot (asn1_value_int32_of_type SEQUENCE)
let len_of_aliasKeyTBS_payload_max ()
: GTot (asn1_value_int32_of_type SEQUENCE)
= len_of_x509_version () +
  len_of_x509_serialNumber_max +
  len_of_algorithmIdentifier () +
  len_of_aliasKeyTBS_issuer_max () +
  len_of_x509_validity () +
  len_of_aliasKeyTBS_subject_max () +
  len_of_subjectPublicKeyInfo +
  len_of_x509_extensions (len_of_aliasKeyTBS_extensions_max ())
module L0.X509.AliasKeyTBS

open ASN1.Spec
open ASN1.Low
open X509
open L0.X509.AliasKeyTBS.Issuer
open L0.X509.AliasKeyTBS.Subject
open L0.X509.AliasKeyTBS.Extensions
open FStar.Integers

open L0.X509.LengthUtils

module B32 = FStar.Bytes

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

val decl : unit

noeq
type aliasKeyTBS_payload_t = {
(*
 *       version         [0]  EXPLICIT Version DEFAULT v1,
 *)
  aliasKeyTBS_version     : x509_version_t;
(*
 *       serialNumber         CertificateSerialNumber,
 *)
  aliasKeyTBS_serialNumber: x509_serialNumber_t;
(*
 *       signature            AlgorithmIdentifier,
 *)
  aliasKeyTBS_signatureAlg: algorithmIdentifier_t;
(*
 *       issuer               Name,
 *)
  aliasKeyTBS_issuer      : aliasKeyTBS_issuer_t;
(*
 *       validity             Validity,
 *)
 aliasKeyTBS_validity     : x509_validity_t;
(*
 *       subject              Name,
 *)
  aliasKeyTBS_subject     : aliasKeyTBS_subject_t;
 (*
  *      subjectPublicKeyInfo SubjectPublicKeyInfo
  *)
  aliasKeyTBS_aliasKey_pub: subjectPublicKeyInfo_t;
 (*
  *      extensions      [3]  EXPLICIT Extensions OPTIONAL
  *)
  aliasKeyTBS_extensions  : x509_extensions_t_inbound
                              serialize_aliasKeyTBS_extensions
}

noextract
let and_then_kind (k1 k2:parser_kind) = and_then_kind k1 k2

noextract
let parse_aliasKeyTBS_payload_kind
: parser_kind
= parse_x509_version_kind
  `and_then_kind`
  parse_filter_kind parse_big_integer_as_octet_string_TLV_kind
  `and_then_kind`
  parse_asn1_envelop_tag_with_TLV_kind SEQUENCE
  `and_then_kind`
  parse_asn1_envelop_tag_with_TLV_kind SEQUENCE
  `and_then_kind`
  parse_asn1_envelop_tag_with_TLV_kind SEQUENCE
  `and_then_kind`
  parse_asn1_envelop_tag_with_TLV_kind SEQUENCE
  `and_then_kind`
  parse_asn1_envelop_tag_with_TLV_kind SEQUENCE
  `and_then_kind`
  parse_asn1_envelop_tag_with_TLV_kind x509_extensions_outmost_explicit_tag

noextract
val parse_aliasKeyTBS_payload
: parser parse_aliasKeyTBS_payload_kind aliasKeyTBS_payload_t

noextract
val serialize_aliasKeyTBS_payload
: serializer (parse_aliasKeyTBS_payload)

val lemma_serialize_aliasKeyTBS_payload_unfold
  (x: aliasKeyTBS_payload_t)
: Lemma (
  serialize_aliasKeyTBS_payload `serialize` x ==
 (serialize_x509_version `serialize` x.aliasKeyTBS_version)
  `Seq.append`
 (serialize_x509_serialNumber `serialize` x.aliasKeyTBS_serialNumber)
  `Seq.append`
 (serialize_algorithmIdentifier `serialize` x.aliasKeyTBS_signatureAlg)
  `Seq.append`
 (serialize_aliasKeyTBS_issuer `serialize` x.aliasKeyTBS_issuer)
  `Seq.append`
 (serialize_x509_validity `serialize` x.aliasKeyTBS_validity)
  `Seq.append`
 (serialize_aliasKeyTBS_subject `serialize` x.aliasKeyTBS_subject)
  `Seq.append`
 (serialize_subjectPublicKeyInfo `serialize` x.aliasKeyTBS_aliasKey_pub)
  `Seq.append`
 (serialize_x509_extensions_TLV serialize_aliasKeyTBS_extensions `serialize` x.aliasKeyTBS_extensions)
)
/
X509.fst.checked prims.fst.checked L0.X509.LengthUtils.fst.checked L0.X509.Extension.fst.checked L0.X509.AliasKeyTBS.Subject.fsti.checked L0.X509.AliasKeyTBS.Issuer.fsti.checked L0.X509.AliasKeyTBS.Extensions.fsti.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.fsti
_: Prims.unit -> Prims.GTot (ASN1.Base.asn1_value_int32_of_type ASN1.Base.SEQUENCE)
Prims.unit FStar.Integers.op_Plus FStar.Integers.Unsigned FStar.Integers.W32 X509.BasicFields.Version.len_of_x509_version X509.BasicFields.SerialNumber.len_of_x509_serialNumber_max X509.Crypto.AlgorithmIdentifier.len_of_algorithmIdentifier L0.X509.AliasKeyTBS.Issuer.len_of_aliasKeyTBS_issuer_max X509.BasicFields.Validity.len_of_x509_validity L0.X509.AliasKeyTBS.Subject.len_of_aliasKeyTBS_subject_max X509.BasicFields.SubjectPublicKeyInfo.len_of_subjectPublicKeyInfo X509.BasicFields.Extensions.len_of_x509_extensions L0.X509.AliasKeyTBS.Extensions.len_of_aliasKeyTBS_extensions_max ASN1.Base.asn1_value_int32_of_type ASN1.Base.SEQUENCE
let len_of_aliasKeyTBS_payload_max () : GTot (asn1_value_int32_of_type SEQUENCE) =
  
len_of_x509_version () + len_of_x509_serialNumber_max + len_of_algorithmIdentifier () +
len_of_aliasKeyTBS_issuer_max () +
len_of_x509_validity () +
len_of_aliasKeyTBS_subject_max () +
len_of_subjectPublicKeyInfo +
len_of_x509_extensions (len_of_aliasKeyTBS_extensions_max ())