val serialize32_aliasKeyTBS_issuer_payload_backwards
: serializer32_backwards (serialize_aliasKeyTBS_issuer_payload)
val serialize32_aliasKeyTBS_issuer_payload_backwards
: serializer32_backwards (serialize_aliasKeyTBS_issuer_payload)
let serialize32_aliasKeyTBS_issuer_payload_backwards
= serialize32_synth_backwards
  (* s32*) (serialize32_RDN_COMMON_NAME
            `serialize32_nondep_then_backwards`
            serialize32_RDN_ORGANIZATION
            `serialize32_nondep_then_backwards`
            serialize32_RDN_COUNTRY)
  (* f2 *) (synth_aliasKeyTBS_issuer_payload_t)
  (* g1 *) (synth_aliasKeyTBS_issuer_payload_t')
  (* g1'*) (synth_aliasKeyTBS_issuer_payload_t')
  (* prf*) ()
module L0.X509.AliasKeyTBS.Issuer

open ASN1.Spec
open ASN1.Low
open X509
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_issuer_payload_t' = (
  x509_RDN_x520_attribute_t COMMON_NAME  IA5_STRING `tuple2`
  x509_RDN_x520_attribute_t ORGANIZATION IA5_STRING `tuple2`
  x509_RDN_x520_attribute_t COUNTRY      PRINTABLE_STRING
)

let synth_aliasKeyTBS_issuer_payload_t
  (x': aliasKeyTBS_issuer_payload_t')
: GTot (aliasKeyTBS_issuer_payload_t)
= { aliasKeyTBS_issuer_Common       = fst (fst x');
    aliasKeyTBS_issuer_Organization = snd (fst x');
    aliasKeyTBS_issuer_Country      = snd x' }

inline_for_extraction noextract
let synth_aliasKeyTBS_issuer_payload_t'
  (x: aliasKeyTBS_issuer_payload_t)
: Tot (x': aliasKeyTBS_issuer_payload_t'
           { x == synth_aliasKeyTBS_issuer_payload_t x' })
= (x.aliasKeyTBS_issuer_Common,
   x.aliasKeyTBS_issuer_Organization),
   x.aliasKeyTBS_issuer_Country

let parse_aliasKeyTBS_issuer_payload
= parse_RDN_x520_attribute COMMON_NAME  IA5_STRING
  `nondep_then`
  parse_RDN_x520_attribute ORGANIZATION IA5_STRING
  `nondep_then`
  parse_RDN_x520_attribute COUNTRY      PRINTABLE_STRING
  `parse_synth`
  synth_aliasKeyTBS_issuer_payload_t

let serialize_aliasKeyTBS_issuer_payload
= serialize_synth
  (* p1 *) (parse_RDN_x520_attribute COMMON_NAME  IA5_STRING
            `nondep_then`
            parse_RDN_x520_attribute ORGANIZATION IA5_STRING
            `nondep_then`
            parse_RDN_x520_attribute COUNTRY      PRINTABLE_STRING)
  (* f2 *) (synth_aliasKeyTBS_issuer_payload_t)
  (* s1 *) (serialize_RDN_x520_attribute COMMON_NAME  IA5_STRING
            `serialize_nondep_then`
            serialize_RDN_x520_attribute ORGANIZATION IA5_STRING
            `serialize_nondep_then`
            serialize_RDN_x520_attribute COUNTRY      PRINTABLE_STRING)
  (* g1 *) (synth_aliasKeyTBS_issuer_payload_t')
  (* prf*) ()

let lemma_serialize_aliasKeyTBS_issuer_payload_unfold x
= serialize_nondep_then_eq
  (* s1 *) (serialize_RDN_x520_attribute COMMON_NAME  IA5_STRING)
  (* s2 *) (serialize_RDN_x520_attribute ORGANIZATION IA5_STRING)
  (* in *) (fst (synth_aliasKeyTBS_issuer_payload_t' x));
  serialize_nondep_then_eq
  (* s1 *) (serialize_RDN_x520_attribute COMMON_NAME  IA5_STRING
            `serialize_nondep_then`
            serialize_RDN_x520_attribute ORGANIZATION IA5_STRING)
  (* s2 *) (serialize_RDN_x520_attribute COUNTRY      PRINTABLE_STRING)
  (* in *) (synth_aliasKeyTBS_issuer_payload_t' x);
  serialize_synth_eq
  (* p1 *) (parse_RDN_x520_attribute COMMON_NAME  IA5_STRING
            `nondep_then`
            parse_RDN_x520_attribute ORGANIZATION IA5_STRING
            `nondep_then`
            parse_RDN_x520_attribute COUNTRY      PRINTABLE_STRING)
  (* f2 *) (synth_aliasKeyTBS_issuer_payload_t)
  (* s1 *) (serialize_RDN_x520_attribute COMMON_NAME  IA5_STRING
            `serialize_nondep_then`
            serialize_RDN_x520_attribute ORGANIZATION IA5_STRING
            `serialize_nondep_then`
            serialize_RDN_x520_attribute COUNTRY      PRINTABLE_STRING)
  (* g1 *) (synth_aliasKeyTBS_issuer_payload_t')
  (* prf*) ()
  (* in *) (x)

let lemma_serialize_aliasKeyTBS_issuer_payload_size x
= lemma_serialize_aliasKeyTBS_issuer_payload_unfold x;
    lemma_serialize_RDN_x520_attribute_size_exact x.aliasKeyTBS_issuer_Common;
    lemma_serialize_RDN_x520_attribute_size_exact x.aliasKeyTBS_issuer_Organization;
    lemma_serialize_RDN_x520_attribute_size_exact x.aliasKeyTBS_issuer_Country

(*
 *
 *)

let lemma_serialize_aliasKeyTBS_issuer_unfold x
= lemma_serialize_asn1_sequence_TLV_unfold (serialize_aliasKeyTBS_issuer_payload) x

let lemma_serialize_aliasKeyTBS_issuer_size x
= lemma_serialize_asn1_sequence_TLV_size (serialize_aliasKeyTBS_issuer_payload) x

let lemma_serialize_aliasKeyTBS_issuer_size_exact x
= lemma_serialize_aliasKeyTBS_issuer_size x;
  (**) lemma_serialize_aliasKeyTBS_issuer_payload_size x

(* Low *)
/
X509.fst.checked prims.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.Issuer.fst
ASN1.Low.Base.serializer32_backwards L0.X509.AliasKeyTBS.Issuer.serialize_aliasKeyTBS_issuer_payload
ASN1.Low.Base.serialize32_synth_backwards LowParse.Spec.Combinators.and_then_kind ASN1.Spec.Value.Envelop.parse_asn1_envelop_tag_with_TLV_kind ASN1.Base.SET FStar.Pervasives.Native.tuple2 X509.BasicFields.RelativeDistinguishedName.x509_RDN_x520_attribute_t X509.BasicFields.RelativeDistinguishedName.COMMON_NAME ASN1.Base.IA5_STRING X509.BasicFields.RelativeDistinguishedName.ORGANIZATION X509.BasicFields.RelativeDistinguishedName.COUNTRY ASN1.Base.PRINTABLE_STRING LowParse.Spec.Combinators.nondep_then X509.BasicFields.RelativeDistinguishedName.parse_RDN_x520_attribute LowParse.Spec.Combinators.serialize_nondep_then X509.BasicFields.RelativeDistinguishedName.serialize_RDN_x520_attribute ASN1.Low.Base.serialize32_nondep_then_backwards X509.BasicFields.RelativeDistinguishedName.serialize32_RDN_COMMON_NAME X509.BasicFields.RelativeDistinguishedName.serialize32_RDN_ORGANIZATION X509.BasicFields.RelativeDistinguishedName.serialize32_RDN_COUNTRY L0.X509.AliasKeyTBS.Issuer.aliasKeyTBS_issuer_payload_t L0.X509.AliasKeyTBS.Issuer.synth_aliasKeyTBS_issuer_payload_t L0.X509.AliasKeyTBS.Issuer.synth_aliasKeyTBS_issuer_payload_t'
let serialize32_aliasKeyTBS_issuer_payload_backwards =
  
serialize32_synth_backwards ((serialize32_RDN_COMMON_NAME
      `serialize32_nondep_then_backwards`
      serialize32_RDN_ORGANIZATION)
    `serialize32_nondep_then_backwards`
    serialize32_RDN_COUNTRY)
  (synth_aliasKeyTBS_issuer_payload_t)
  (synth_aliasKeyTBS_issuer_payload_t')
  (synth_aliasKeyTBS_issuer_payload_t')
  ()