val lemma_serialize_subjectPublicKeyInfo_size_exact
  (x: subjectPublicKeyInfo_t)
: Lemma (
  ( length_of_opaque_serialization (serialize_subjectPublicKeyInfo) x
    == length_of_subjectPublicKeyInfo )
)
val lemma_serialize_subjectPublicKeyInfo_size_exact
  (x: subjectPublicKeyInfo_t)
: Lemma (
  ( length_of_opaque_serialization (serialize_subjectPublicKeyInfo) x
    == length_of_subjectPublicKeyInfo )
)
let lemma_serialize_subjectPublicKeyInfo_size_exact x
= lemma_serialize_subjectPublicKeyInfo_unfold x;
  lemma_serialize_subjectPublicKeyInfo_size   x;
    lemma_serialize_subjectPublicKeyInfo_payload_size x;
    lemma_serialize_algorithmIdentifier_size_exact x.subjectPubKey_alg;
    assert ( let bs: pubkey_t = x.subjectPubKey in
             length_of_asn1_primitive_TLV bs == 35 )
module X509.BasicFields.SubjectPublicKeyInfo
open ASN1.Spec
open ASN1.Low

open X509.Base
open X509.Crypto

open FStar.Integers

#set-options "--fuel 0 --ifuel 0"

let filter_subjectPublicKeyInfo_payload_t'
  (x: (algorithmIdentifier_t) `tuple2` (datatype_of_asn1_type BIT_STRING))
: GTot bool
= (snd x).bs_len = 33ul &&
  (snd x).bs_unused_bits = 0ul

let subjectPublicKeyInfo_payload_t'
= parse_filter_refine (filter_subjectPublicKeyInfo_payload_t')

let synth_subjectPublicKeyInfo_payload_t
  (x': subjectPublicKeyInfo_payload_t')
: GTot (subjectPublicKeyInfo_payload_t)
= { subjectPubKey_alg = fst x';
    subjectPubKey     = snd x' }

inline_for_extraction noextract
let synth_subjectPublicKeyInfo_payload_t'
  (x: subjectPublicKeyInfo_payload_t)
: Tot (x': subjectPublicKeyInfo_payload_t' { x == synth_subjectPublicKeyInfo_payload_t x' })
= (x.subjectPubKey_alg , x.subjectPubKey)

let parse_subjectPublicKeyInfo_payload
= parse_algorithmIdentifier
  `nondep_then`
  parse_asn1_TLV_of_type BIT_STRING
  `parse_filter`
  filter_subjectPublicKeyInfo_payload_t'
  `parse_synth`
  synth_subjectPublicKeyInfo_payload_t

let serialize_subjectPublicKeyInfo_payload
= serialize_synth
  (* p1 *) (parse_algorithmIdentifier
            `nondep_then`
            parse_asn1_TLV_of_type BIT_STRING
            `parse_filter`
            filter_subjectPublicKeyInfo_payload_t')
  (* f2 *) (synth_subjectPublicKeyInfo_payload_t)
  (* s1 *) (serialize_algorithmIdentifier
            `serialize_nondep_then`
            serialize_asn1_TLV_of_type BIT_STRING
            `serialize_filter`
            filter_subjectPublicKeyInfo_payload_t')
  (* g1 *) (synth_subjectPublicKeyInfo_payload_t')
  (* prf*) ()

let lemma_serialize_subjectPublicKeyInfo_payload_unfold x
= serialize_nondep_then_eq
  (* s1 *) (serialize_algorithmIdentifier)
  (* s2 *) (serialize_asn1_TLV_of_type BIT_STRING)
  (* in *) (synth_subjectPublicKeyInfo_payload_t' x);
  serialize_synth_eq
  (* p1 *) (parse_algorithmIdentifier
            `nondep_then`
            parse_asn1_TLV_of_type BIT_STRING
            `parse_filter`
            filter_subjectPublicKeyInfo_payload_t')
  (* f2 *) (synth_subjectPublicKeyInfo_payload_t)
  (* s1 *) (serialize_algorithmIdentifier
            `serialize_nondep_then`
            serialize_asn1_TLV_of_type BIT_STRING
            `serialize_filter`
            filter_subjectPublicKeyInfo_payload_t')
  (* g1 *) (synth_subjectPublicKeyInfo_payload_t')
  (* prf*) ()
  (* in *) x

let lemma_serialize_subjectPublicKeyInfo_payload_size x
= lemma_serialize_subjectPublicKeyInfo_payload_unfold x

let lemma_serialize_subjectPublicKeyInfo_unfold x
= lemma_serialize_asn1_sequence_TLV_unfold (serialize_subjectPublicKeyInfo_payload) x

let lemma_serialize_subjectPublicKeyInfo_size x
= lemma_serialize_asn1_sequence_TLV_size (serialize_subjectPublicKeyInfo_payload) x

(* NOTE: For a subjectPublicKeyInfo for Ed25519, it consists
         1) a 1-byte tag
         2) a 1-byte length (the value field's length can be represented by 1 byte)
         3) a 7-byte algorithmIdentifier for Ed25519, whose length has been proved is 7,
            see `lemma_serialize_algorithmIdentifier_size_exact`
         4) a 35-byte bit string TLV (1 byte for tag, 1 byte for length, 33 bytes for a 32-byte bit string),
            see `length_of_asn1_primitive_value` (without tag and length) and `length_of_asn1_primitive_TLV`
            for the length calc.
         Thus the total length should be 1 + 1 + 7 + 35 = 44 bytes.
   NOTE: For the use of lemmas:
         For primitive types
         1) lemma_serialize_..._unfold will reveal one level of the serialization.
            For example, `lemma_serialize_asn1_bit_string_TLV_unfold bs` proves
            that serialization of bs's TLV == serialization of tag appends serialization
            of length appends serialization of value (the bs)
         2) lemma_serialize_..._size will reveal the size of a TLV equals to the sum of
            the serializations of Tag, Length and Value
         For SEQUENCE, which takes a serializer `s` of the SEQUENCE body, envelops it as
         a SEQUENCE TLV `lemma_serialize_...sequence_TLV_unfold/size` reveals this level
         of SEQUENCE "envelop".
*)
/
X509.Crypto.fst.checked X509.Base.fst.checked prims.fst.checked FStar.UInt32.fsti.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Integers.fst.checked ASN1.Spec.fst.checked ASN1.Low.fst.checked
X509.BasicFields.SubjectPublicKeyInfo.fst
x: X509.BasicFields.SubjectPublicKeyInfo.subjectPublicKeyInfo_t
  -> FStar.Pervasives.Lemma
    (ensures
      ASN1.Spec.Base.length_of_opaque_serialization X509.BasicFields.SubjectPublicKeyInfo.serialize_subjectPublicKeyInfo
        x ==
      X509.BasicFields.SubjectPublicKeyInfo.length_of_subjectPublicKeyInfo)
X509.BasicFields.SubjectPublicKeyInfo.subjectPublicKeyInfo_t Prims._assert Prims.eq2 ASN1.Base.asn1_TLV_length_of_type ASN1.Base.BIT_STRING 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 ASN1.Spec.TLV.length_of_asn1_primitive_TLV Prims.l_and FStar.UInt32.t ASN1.Base.__proj__Mkbit_string_t__item__bs_len FStar.UInt32.uint_to_t ASN1.Base.__proj__Mkbit_string_t__item__bs_unused_bits X509.BasicFields.SubjectPublicKeyInfo.__proj__MksubjectPublicKeyInfo_payload_t__item__subjectPubKey Prims.unit X509.Crypto.AlgorithmIdentifier.lemma_serialize_algorithmIdentifier_size_exact X509.BasicFields.SubjectPublicKeyInfo.__proj__MksubjectPublicKeyInfo_payload_t__item__subjectPubKey_alg X509.BasicFields.SubjectPublicKeyInfo.lemma_serialize_subjectPublicKeyInfo_payload_size X509.BasicFields.SubjectPublicKeyInfo.lemma_serialize_subjectPublicKeyInfo_size X509.BasicFields.SubjectPublicKeyInfo.lemma_serialize_subjectPublicKeyInfo_unfold
let lemma_serialize_subjectPublicKeyInfo_size_exact x =
  
lemma_serialize_subjectPublicKeyInfo_unfold x;
lemma_serialize_subjectPublicKeyInfo_size x;
lemma_serialize_subjectPublicKeyInfo_payload_size x;
lemma_serialize_algorithmIdentifier_size_exact x.subjectPubKey_alg;
assert (let bs:pubkey_t = x.subjectPubKey in
    length_of_asn1_primitive_TLV bs == 35)