val lemma_serialize_algorithmIdentifier_payload_unfold
  (x: algorithmIdentifier_payload_t)
: Lemma (
  serialize (serialize_algorithmIdentifier_payload) x ==
  serialize (serialize_asn1_oid_TLV_of OID_ED25519) OID_ED25519 /\
  length_of_opaque_serialization (serialize_algorithmIdentifier_payload) x ==
  5
)
val lemma_serialize_algorithmIdentifier_payload_unfold
  (x: algorithmIdentifier_payload_t)
: Lemma (
  serialize (serialize_algorithmIdentifier_payload) x ==
  serialize (serialize_asn1_oid_TLV_of OID_ED25519) OID_ED25519 /\
  length_of_opaque_serialization (serialize_algorithmIdentifier_payload) x ==
  5
)
let lemma_serialize_algorithmIdentifier_payload_unfold x
= serialize_synth_eq
  (* 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*) ()
  (* in *) (x);
  assert_norm (length_of_asn1_primitive_TLV OID_ED25519 == 5)
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

/// sequence value serializer
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*) ()
/
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
x: X509.Crypto.AlgorithmIdentifier.algorithmIdentifier_payload_t
  -> FStar.Pervasives.Lemma
    (ensures
      LowParse.Spec.Base.serialize X509.Crypto.AlgorithmIdentifier.serialize_algorithmIdentifier_payload
        x ==
      LowParse.Spec.Base.serialize (ASN1.Spec.Value.OID.serialize_asn1_oid_TLV_of ASN1.Base.OID_ED25519
          )
        ASN1.Base.OID_ED25519 /\
      ASN1.Spec.Base.length_of_opaque_serialization X509.Crypto.AlgorithmIdentifier.serialize_algorithmIdentifier_payload
        x ==
      5)
X509.Crypto.AlgorithmIdentifier.algorithmIdentifier_payload_t FStar.Pervasives.assert_norm Prims.eq2 Prims.int ASN1.Spec.TLV.length_of_asn1_primitive_TLV ASN1.Base.OID ASN1.Base.OID_ED25519 Prims.unit LowParse.Spec.Combinators.serialize_synth_eq LowParse.Spec.Combinators.parse_filter_kind ASN1.Spec.Value.OID.parse_asn1_oid_TLV_kind ASN1.Spec.Value.OID.the_asn1_oid 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 lemma_serialize_algorithmIdentifier_payload_unfold x =
  
serialize_synth_eq (parse_asn1_oid_TLV_of OID_ED25519)
  (synth_algorithmIdentifier_payload_t)
  (serialize_asn1_oid_TLV_of OID_ED25519)
  (synth_algorithmIdentifier_payload_t')
  ()
  (x);
assert_norm (length_of_asn1_primitive_TLV OID_ED25519 == 5)