val parse_aliasKeyTBS_issuer_payload
: parser
    (parse_aliasKeyTBS_issuer_payload_kind)
    (aliasKeyTBS_issuer_payload_t)
val parse_aliasKeyTBS_issuer_payload
: parser
    (parse_aliasKeyTBS_issuer_payload_kind)
    (aliasKeyTBS_issuer_payload_t)
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
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
/
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
LowParse.Spec.Base.parser L0.X509.AliasKeyTBS.Issuer.parse_aliasKeyTBS_issuer_payload_kind
  L0.X509.AliasKeyTBS.Issuer.aliasKeyTBS_issuer_payload_t
LowParse.Spec.Combinators.parse_synth 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 L0.X509.AliasKeyTBS.Issuer.aliasKeyTBS_issuer_payload_t LowParse.Spec.Combinators.nondep_then X509.BasicFields.RelativeDistinguishedName.parse_RDN_x520_attribute L0.X509.AliasKeyTBS.Issuer.synth_aliasKeyTBS_issuer_payload_t
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