val serialize_aliasKeyTBS_payload
: serializer (parse_aliasKeyTBS_payload)
val serialize_aliasKeyTBS_payload
: serializer (parse_aliasKeyTBS_payload)
let serialize_aliasKeyTBS_payload
=
  serialize_synth
  (* p1 *) (parse_x509_version
            `nondep_then`
            parse_x509_serialNumber
            `nondep_then`
            parse_algorithmIdentifier
            `nondep_then`
            parse_aliasKeyTBS_issuer
            `nondep_then`
            parse_x509_validity
            `nondep_then`
            parse_aliasKeyTBS_subject
            `nondep_then`
            parse_subjectPublicKeyInfo
            `nondep_then`
            parse_x509_extensions_TLV serialize_aliasKeyTBS_extensions)
  (* f2 *) (synth_aliasKeyTBS_payload_t)
  (* s1 *) (serialize_x509_version
            `serialize_nondep_then`
            serialize_x509_serialNumber
            `serialize_nondep_then`
            serialize_algorithmIdentifier
            `serialize_nondep_then`
            serialize_aliasKeyTBS_issuer
            `serialize_nondep_then`
            serialize_x509_validity
            `serialize_nondep_then`
            serialize_aliasKeyTBS_subject
            `serialize_nondep_then`
            serialize_subjectPublicKeyInfo
            `serialize_nondep_then`
            serialize_x509_extensions_TLV serialize_aliasKeyTBS_extensions
            `coerce_parser_serializer _`
            ())
  (* g1 *) (synth_aliasKeyTBS_payload_t')
  (* prf*) ()
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

module B32 = FStar.Bytes

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

let decl = ()

let aliasKeyTBS_payload_t' = (
(*
//  *       version         [0]  EXPLICIT Version DEFAULT v1,
//  *)
  x509_version_t `tuple2`
(*
//  *       serialNumber         CertificateSerialNumber,
//  *)
  x509_serialNumber_t `tuple2`
(*
//  *       signature            AlgorithmIdentifier,
//  *)
  algorithmIdentifier_t `tuple2`
(*
//  *       issuer               Name,
//  *)
  aliasKeyTBS_issuer_t `tuple2`
(*
//  *       validity             Validity,
//  *)
  x509_validity_t `tuple2`
(*
//  *       subject              Name,
//  *)
  aliasKeyTBS_subject_t `tuple2`
(*
//  *      subjectPublicKeyInfo SubjectPublicKeyInfo
//  *)
  subjectPublicKeyInfo_t `tuple2`
(*
//  *      extensions      [3]  EXPLICIT Extensions OPTIONAL
//  *)
  x509_extensions_t_inbound serialize_aliasKeyTBS_extensions
)

let synth_aliasKeyTBS_payload_t
  (x': aliasKeyTBS_payload_t')
: GTot (aliasKeyTBS_payload_t)
= { aliasKeyTBS_version      = fst (fst (fst (fst (fst (fst (fst x'))))));
    aliasKeyTBS_serialNumber = snd (fst (fst (fst (fst (fst (fst x'))))));
    aliasKeyTBS_signatureAlg = snd (fst (fst (fst (fst (fst x')))));
    aliasKeyTBS_issuer       = snd (fst (fst (fst (fst x'))));
    aliasKeyTBS_validity     = snd (fst (fst (fst x')));
    aliasKeyTBS_subject      = snd (fst (fst x'));
    aliasKeyTBS_aliasKey_pub = snd (fst x');
    aliasKeyTBS_extensions   = snd x' }

inline_for_extraction noextract
let synth_aliasKeyTBS_payload_t'
  (x: aliasKeyTBS_payload_t)
: Tot (x': aliasKeyTBS_payload_t' { x == synth_aliasKeyTBS_payload_t x' })
= ((((((x.aliasKeyTBS_version,
        x.aliasKeyTBS_serialNumber),
        x.aliasKeyTBS_signatureAlg),
        x.aliasKeyTBS_issuer),
        x.aliasKeyTBS_validity),
        x.aliasKeyTBS_subject),
        x.aliasKeyTBS_aliasKey_pub),
        x.aliasKeyTBS_extensions

let parse_aliasKeyTBS_payload
= parse_x509_version
  `nondep_then`
  parse_x509_serialNumber
  `nondep_then`
  parse_algorithmIdentifier
  `nondep_then`
  parse_aliasKeyTBS_issuer
  `nondep_then`
  parse_x509_validity
  `nondep_then`
  parse_aliasKeyTBS_subject
  `nondep_then`
  parse_subjectPublicKeyInfo
  `nondep_then`
  parse_x509_extensions_TLV serialize_aliasKeyTBS_extensions
  `parse_synth`
  synth_aliasKeyTBS_payload_t
/
X509.fst.checked prims.fst.checked L0.X509.AliasKeyTBS.Subject.fsti.checked L0.X509.AliasKeyTBS.Issuer.fsti.checked L0.X509.AliasKeyTBS.Extensions.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.Native.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.fst
LowParse.Spec.Base.serializer L0.X509.AliasKeyTBS.parse_aliasKeyTBS_payload
LowParse.Spec.Combinators.serialize_synth LowParse.Spec.Combinators.and_then_kind X509.BasicFields.Version.parse_x509_version_kind LowParse.Spec.Combinators.parse_filter_kind ASN1.Spec.Value.BigInteger.parse_big_integer_as_octet_string_TLV_kind ASN1.Spec.Value.Envelop.parse_asn1_envelop_tag_with_TLV_kind ASN1.Base.SEQUENCE X509.BasicFields.Extensions.x509_extensions_outmost_explicit_tag FStar.Pervasives.Native.tuple2 X509.BasicFields.Version.x509_version_t X509.BasicFields.SerialNumber.x509_serialNumber_t X509.Crypto.AlgorithmIdentifier.algorithmIdentifier_t L0.X509.AliasKeyTBS.Issuer.aliasKeyTBS_issuer_t X509.BasicFields.Validity.x509_validity_t L0.X509.AliasKeyTBS.Subject.aliasKeyTBS_subject_t X509.BasicFields.SubjectPublicKeyInfo.subjectPublicKeyInfo_t X509.BasicFields.Extensions.x509_extensions_t_inbound L0.X509.AliasKeyTBS.Extensions.aliasKeyTBS_extensions_t L0.X509.AliasKeyTBS.Extensions.parse_aliasKeyTBS_extensions L0.X509.AliasKeyTBS.Extensions.serialize_aliasKeyTBS_extensions L0.X509.AliasKeyTBS.aliasKeyTBS_payload_t LowParse.Spec.Combinators.nondep_then X509.BasicFields.Version.parse_x509_version X509.BasicFields.SerialNumber.parse_x509_serialNumber X509.Crypto.AlgorithmIdentifier.parse_algorithmIdentifier L0.X509.AliasKeyTBS.Issuer.parse_aliasKeyTBS_issuer X509.BasicFields.Validity.parse_x509_validity L0.X509.AliasKeyTBS.Subject.parse_aliasKeyTBS_subject X509.BasicFields.SubjectPublicKeyInfo.parse_subjectPublicKeyInfo X509.BasicFields.Extensions.parse_x509_extensions_TLV L0.X509.AliasKeyTBS.synth_aliasKeyTBS_payload_t ASN1.Spec.Base.coerce_parser_serializer LowParse.Spec.Combinators.serialize_nondep_then X509.BasicFields.Version.serialize_x509_version X509.BasicFields.SerialNumber.serialize_x509_serialNumber X509.Crypto.AlgorithmIdentifier.serialize_algorithmIdentifier L0.X509.AliasKeyTBS.Issuer.serialize_aliasKeyTBS_issuer X509.BasicFields.Validity.serialize_x509_validity L0.X509.AliasKeyTBS.Subject.serialize_aliasKeyTBS_subject X509.BasicFields.SubjectPublicKeyInfo.serialize_subjectPublicKeyInfo X509.BasicFields.Extensions.serialize_x509_extensions_TLV L0.X509.AliasKeyTBS.synth_aliasKeyTBS_payload_t'
let serialize_aliasKeyTBS_payload =
  
serialize_synth (((((((parse_x509_version `nondep_then` parse_x509_serialNumber)
              `nondep_then`
              parse_algorithmIdentifier)
            `nondep_then`
            parse_aliasKeyTBS_issuer)
          `nondep_then`
          parse_x509_validity)
        `nondep_then`
        parse_aliasKeyTBS_subject)
      `nondep_then`
      parse_subjectPublicKeyInfo)
    `nondep_then`
    (parse_x509_extensions_TLV serialize_aliasKeyTBS_extensions))
  (synth_aliasKeyTBS_payload_t)
  (coerce_parser_serializer _
      (((((((serialize_x509_version `serialize_nondep_then` serialize_x509_serialNumber)
                  `serialize_nondep_then`
                  serialize_algorithmIdentifier)
                `serialize_nondep_then`
                serialize_aliasKeyTBS_issuer)
              `serialize_nondep_then`
              serialize_x509_validity)
            `serialize_nondep_then`
            serialize_aliasKeyTBS_subject)
          `serialize_nondep_then`
          serialize_subjectPublicKeyInfo)
        `serialize_nondep_then`
        (serialize_x509_extensions_TLV serialize_aliasKeyTBS_extensions))
      ())
  (synth_aliasKeyTBS_payload_t')
  ()