val serialize_subjectPublicKeyInfo:serializer parse_subjectPublicKeyInfo
val serialize_subjectPublicKeyInfo:serializer parse_subjectPublicKeyInfo
let serialize_subjectPublicKeyInfo
: serializer parse_subjectPublicKeyInfo
= coerce_parser_serializer
    parse_subjectPublicKeyInfo
    (serialize_asn1_sequence_TLV (serialize_subjectPublicKeyInfo_payload))
    ()
module X509.BasicFields.SubjectPublicKeyInfo

open LowParse.Low.Base

open ASN1.Spec
open ASN1.Low

open X509.Base
open X509.Crypto

open FStar.Integers

type subjectPublicKeyInfo_payload_t
= { subjectPubKey_alg : algorithmIdentifier_t;
    subjectPubKey     : pubkey_t }

inline_for_extraction noextract
let parse_subjectPublicKeyInfo_payload_kind
: parser_kind
= parse_filter_kind
  (parse_asn1_envelop_tag_with_TLV_kind SEQUENCE
   `and_then_kind`
   parse_asn1_TLV_kind_of_type BIT_STRING)

val parse_subjectPublicKeyInfo_payload
: parser parse_subjectPublicKeyInfo_payload_kind (subjectPublicKeyInfo_payload_t)

val serialize_subjectPublicKeyInfo_payload
: serializer (parse_subjectPublicKeyInfo_payload)

val lemma_serialize_subjectPublicKeyInfo_payload_unfold
  (x: subjectPublicKeyInfo_payload_t)
: Lemma (
  serialize (serialize_subjectPublicKeyInfo_payload) x ==
  serialize (serialize_algorithmIdentifier) x.subjectPubKey_alg
  `Seq.append`
  serialize (serialize_asn1_TLV_of_type BIT_STRING) x.subjectPubKey
)

val lemma_serialize_subjectPublicKeyInfo_payload_size
  (x: subjectPublicKeyInfo_payload_t)
: Lemma (
  Seq.length (serialize (serialize_subjectPublicKeyInfo_payload) x) ==
  Seq.length (serialize (serialize_algorithmIdentifier) x.subjectPubKey_alg) +
  Seq.length (serialize (serialize_asn1_TLV_of_type BIT_STRING) x.subjectPubKey)
)

let subjectPublicKeyInfo_t
= inbound_sequence_value_of (serialize_subjectPublicKeyInfo_payload)

/// TLV
///
let parse_subjectPublicKeyInfo
: parser _ subjectPublicKeyInfo_t
= subjectPublicKeyInfo_t
  `coerce_parser`
  parse_asn1_sequence_TLV (serialize_subjectPublicKeyInfo_payload)
/
X509.Crypto.AlgorithmIdentifier.fsti.checked X509.Crypto.fst.checked X509.Base.fst.checked prims.fst.checked LowParse.Low.Base.fst.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
X509.BasicFields.SubjectPublicKeyInfo.fsti
LowParse.Spec.Base.serializer X509.BasicFields.SubjectPublicKeyInfo.parse_subjectPublicKeyInfo
ASN1.Spec.Base.coerce_parser_serializer X509.BasicFields.SubjectPublicKeyInfo.subjectPublicKeyInfo_t ASN1.Spec.Value.Envelop.parse_asn1_envelop_tag_with_TLV_kind ASN1.Base.SEQUENCE ASN1.Spec.Value.SEQUENCE.inbound_sequence_value_of X509.BasicFields.SubjectPublicKeyInfo.parse_subjectPublicKeyInfo_payload_kind X509.BasicFields.SubjectPublicKeyInfo.subjectPublicKeyInfo_payload_t X509.BasicFields.SubjectPublicKeyInfo.parse_subjectPublicKeyInfo_payload X509.BasicFields.SubjectPublicKeyInfo.serialize_subjectPublicKeyInfo_payload ASN1.Spec.Value.SEQUENCE.parse_asn1_sequence_TLV X509.BasicFields.SubjectPublicKeyInfo.parse_subjectPublicKeyInfo ASN1.Spec.Value.SEQUENCE.serialize_asn1_sequence_TLV
let serialize_subjectPublicKeyInfo:serializer parse_subjectPublicKeyInfo =
  
coerce_parser_serializer parse_subjectPublicKeyInfo
  (serialize_asn1_sequence_TLV (serialize_subjectPublicKeyInfo_payload))
  ()