val lemma_serialize_algorithmIdentifier_payload_size
  (x: algorithmIdentifier_payload_t)
: Lemma (
  length_of_opaque_serialization (serialize_algorithmIdentifier_payload) x
  == (v (len_of_algorithmIdentifier_payload ()))
)
val lemma_serialize_algorithmIdentifier_payload_size
  (x: algorithmIdentifier_payload_t)
: Lemma (
  length_of_opaque_serialization (serialize_algorithmIdentifier_payload) x
  == (v (len_of_algorithmIdentifier_payload ()))
)
let lemma_serialize_algorithmIdentifier_payload_size x
= lemma_serialize_algorithmIdentifier_payload_unfold x;
  assert_norm (length_of_asn1_primitive_TLV #OID x.algID_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*) ()

/// lemma: unfold sequence value serializer
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)
/
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
      ASN1.Spec.Base.length_of_opaque_serialization X509.Crypto.AlgorithmIdentifier.serialize_algorithmIdentifier_payload
        x ==
      FStar.Integers.v (X509.Crypto.AlgorithmIdentifier.len_of_algorithmIdentifier_payload ()))
X509.Crypto.AlgorithmIdentifier.algorithmIdentifier_payload_t FStar.Pervasives.assert_norm Prims.eq2 ASN1.Base.asn1_TLV_length_of_type ASN1.Base.OID Prims.nat FStar.Seq.Base.length LowParse.Bytes.byte LowParse.Spec.Base.serialize ASN1.Spec.TLV.parse_asn1_TLV_kind_of_type ASN1.Base.datatype_of_asn1_type ASN1.Spec.TLV.parse_asn1_TLV_of_type ASN1.Spec.TLV.serialize_asn1_TLV_of_type X509.Crypto.AlgorithmIdentifier.__proj__MkalgorithmIdentifier_Ed25519_t__item__algID_ed25519 ASN1.Spec.TLV.length_of_asn1_primitive_TLV Prims.unit X509.Crypto.AlgorithmIdentifier.lemma_serialize_algorithmIdentifier_payload_unfold
let lemma_serialize_algorithmIdentifier_payload_size x =
  
lemma_serialize_algorithmIdentifier_payload_unfold x;
assert_norm (length_of_asn1_primitive_TLV #OID x.algID_ed25519 == 5)