val lemma_serialize_algorithmIdentifier_unfold
  (x: algorithmIdentifier_t)
: Lemma ( predicate_serialize_asn1_sequence_TLV_unfold (serialize_algorithmIdentifier_payload) x )
val lemma_serialize_algorithmIdentifier_unfold
  (x: algorithmIdentifier_t)
: Lemma ( predicate_serialize_asn1_sequence_TLV_unfold (serialize_algorithmIdentifier_payload) x )
let lemma_serialize_algorithmIdentifier_unfold x
= lemma_serialize_asn1_sequence_TLV_unfold (serialize_algorithmIdentifier_payload) x
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)

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)

/// TLV
// unfold
let parse_algorithmIdentifier
= parse_asn1_sequence_TLV (serialize_algorithmIdentifier_payload)

let serialize_algorithmIdentifier
= serialize_asn1_sequence_TLV (serialize_algorithmIdentifier_payload)
/
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_t
  -> FStar.Pervasives.Lemma
    (ensures
      ASN1.Spec.Value.SEQUENCE.predicate_serialize_asn1_sequence_TLV_unfold X509.Crypto.AlgorithmIdentifier.serialize_algorithmIdentifier_payload
        x)
X509.Crypto.AlgorithmIdentifier.algorithmIdentifier_t ASN1.Spec.Value.SEQUENCE.lemma_serialize_asn1_sequence_TLV_unfold X509.Crypto.AlgorithmIdentifier.parse_algorithmIdentifier_payload_kind X509.Crypto.AlgorithmIdentifier.algorithmIdentifier_payload_t X509.Crypto.AlgorithmIdentifier.parse_algorithmIdentifier_payload X509.Crypto.AlgorithmIdentifier.serialize_algorithmIdentifier_payload Prims.unit
let lemma_serialize_algorithmIdentifier_unfold x =
  
lemma_serialize_asn1_sequence_TLV_unfold (serialize_algorithmIdentifier_payload) x