val parse_subjectPublicKeyInfo_payload
: parser parse_subjectPublicKeyInfo_payload_kind (subjectPublicKeyInfo_payload_t)
val parse_subjectPublicKeyInfo_payload
: parser parse_subjectPublicKeyInfo_payload_kind (subjectPublicKeyInfo_payload_t)
let parse_subjectPublicKeyInfo_payload
= parse_algorithmIdentifier
  `nondep_then`
  parse_asn1_TLV_of_type BIT_STRING
  `parse_filter`
  filter_subjectPublicKeyInfo_payload_t'
  `parse_synth`
  synth_subjectPublicKeyInfo_payload_t
module X509.BasicFields.SubjectPublicKeyInfo
open ASN1.Spec
open ASN1.Low

open X509.Base
open X509.Crypto

open FStar.Integers

#set-options "--fuel 0 --ifuel 0"

let filter_subjectPublicKeyInfo_payload_t'
  (x: (algorithmIdentifier_t) `tuple2` (datatype_of_asn1_type BIT_STRING))
: GTot bool
= (snd x).bs_len = 33ul &&
  (snd x).bs_unused_bits = 0ul

let subjectPublicKeyInfo_payload_t'
= parse_filter_refine (filter_subjectPublicKeyInfo_payload_t')

let synth_subjectPublicKeyInfo_payload_t
  (x': subjectPublicKeyInfo_payload_t')
: GTot (subjectPublicKeyInfo_payload_t)
= { subjectPubKey_alg = fst x';
    subjectPubKey     = snd x' }

inline_for_extraction noextract
let synth_subjectPublicKeyInfo_payload_t'
  (x: subjectPublicKeyInfo_payload_t)
: Tot (x': subjectPublicKeyInfo_payload_t' { x == synth_subjectPublicKeyInfo_payload_t x' })
= (x.subjectPubKey_alg , x.subjectPubKey)
/
X509.Crypto.fst.checked X509.Base.fst.checked prims.fst.checked FStar.UInt32.fsti.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Integers.fst.checked ASN1.Spec.fst.checked ASN1.Low.fst.checked
X509.BasicFields.SubjectPublicKeyInfo.fst
LowParse.Spec.Base.parser X509.BasicFields.SubjectPublicKeyInfo.parse_subjectPublicKeyInfo_payload_kind
  X509.BasicFields.SubjectPublicKeyInfo.subjectPublicKeyInfo_payload_t
LowParse.Spec.Combinators.parse_synth LowParse.Spec.Combinators.parse_filter_kind LowParse.Spec.Combinators.and_then_kind ASN1.Spec.Value.Envelop.parse_asn1_envelop_tag_with_TLV_kind ASN1.Base.SEQUENCE ASN1.Spec.TLV.parse_asn1_TLV_kind_of_type ASN1.Base.BIT_STRING LowParse.Spec.Combinators.parse_filter_refine FStar.Pervasives.Native.tuple2 X509.Crypto.AlgorithmIdentifier.algorithmIdentifier_t ASN1.Base.datatype_of_asn1_type X509.BasicFields.SubjectPublicKeyInfo.filter_subjectPublicKeyInfo_payload_t' X509.BasicFields.SubjectPublicKeyInfo.subjectPublicKeyInfo_payload_t LowParse.Spec.Combinators.parse_filter LowParse.Spec.Combinators.nondep_then X509.Crypto.AlgorithmIdentifier.parse_algorithmIdentifier ASN1.Spec.TLV.parse_asn1_TLV_of_type X509.BasicFields.SubjectPublicKeyInfo.synth_subjectPublicKeyInfo_payload_t
let parse_subjectPublicKeyInfo_payload =
  
((parse_algorithmIdentifier `nondep_then` (parse_asn1_TLV_of_type BIT_STRING))
  `parse_filter`
  filter_subjectPublicKeyInfo_payload_t')
`parse_synth`
synth_subjectPublicKeyInfo_payload_t