val serialize_algorithmIdentifier_payload
: serializer (parse_algorithmIdentifier_payload)
val serialize_algorithmIdentifier_payload
: serializer (parse_algorithmIdentifier_payload)
let serialize_algorithmIdentifier_payload
= serialize_synth
  (* p1 *) (parse_asn1_oid_TLV_of OID_ED25519)
  (* f2 *) (synth_algorithmIdentifier_payload_t)
  (* s1 *) (serialize_asn1_oid_TLV_of OID_ED25519)
  (* g1 *) (synth_algorithmIdentifier_payload_t')
  (* prf*) ()
module X509.Crypto.AlgorithmIdentifier
open ASN1.Spec
open ASN1.Low

open X509.Base

open FStar.Integers

#set-options "--z3rlimit 32"
(* AlgorithmIdentifiers
  ======================
  NOTE: Different algorithms have identifiers in different structure.
*)

/// sequence value (body) parser
let parse_algorithmIdentifier_payload
= parse_asn1_oid_TLV_of OID_ED25519
  `parse_synth`
  synth_algorithmIdentifier_payload_t
/
X509.Base.fst.checked prims.fst.checked FStar.Pervasives.fsti.checked FStar.Integers.fst.checked ASN1.Spec.fst.checked ASN1.Low.fst.checked
X509.Crypto.AlgorithmIdentifier.fst
LowParse.Spec.Base.serializer X509.Crypto.AlgorithmIdentifier.parse_algorithmIdentifier_payload
LowParse.Spec.Combinators.serialize_synth LowParse.Spec.Combinators.parse_filter_kind ASN1.Spec.Value.OID.parse_asn1_oid_TLV_kind ASN1.Spec.Value.OID.the_asn1_oid ASN1.Base.OID_ED25519 X509.Crypto.AlgorithmIdentifier.algorithmIdentifier_payload_t ASN1.Spec.Value.OID.parse_asn1_oid_TLV_of X509.Crypto.AlgorithmIdentifier.synth_algorithmIdentifier_payload_t ASN1.Spec.Value.OID.serialize_asn1_oid_TLV_of X509.Crypto.AlgorithmIdentifier.synth_algorithmIdentifier_payload_t'
let serialize_algorithmIdentifier_payload =
  
serialize_synth (parse_asn1_oid_TLV_of OID_ED25519)
  (synth_algorithmIdentifier_payload_t)
  (serialize_asn1_oid_TLV_of OID_ED25519)
  (synth_algorithmIdentifier_payload_t')
  ()