val lemma_serialize_x509_authKeyID_keyIdentifier_unfold : value: ASN1.Base.datatype_of_asn1_type ASN1.Base.OCTET_STRING
  -> FStar.Pervasives.Lemma
    (ensures
      LowParse.Spec.Base.serialize (ASN1.Spec.Value.OCTET_STRING.serialize_asn1_octet_string_TLV_with_tag
            X509.ExtFields.AuthorityKeyIdentifier.x509_authKeyID_keyIdentifier_tag)
        value ==
      FStar.Seq.Base.append (FStar.Seq.Base.append (LowParse.Spec.Base.serialize (ASN1.Spec.Tag.serialize_asn1_tag_of_type
                    X509.ExtFields.AuthorityKeyIdentifier.x509_authKeyID_keyIdentifier_tag)
                X509.ExtFields.AuthorityKeyIdentifier.x509_authKeyID_keyIdentifier_tag)
            (LowParse.Spec.Base.serialize (ASN1.Spec.Length.serialize_asn1_length_of_type ASN1.Base.OCTET_STRING
                  )
                (Mkoctet_string_t?.len value)))
        (LowParse.Spec.Base.serialize (ASN1.Spec.Value.OCTET_STRING.serialize_asn1_octet_string (FStar.Integers.v
                    (Mkoctet_string_t?.len value)))
            value))
let lemma_serialize_x509_authKeyID_keyIdentifier_unfold
= lemma_serialize_asn1_octet_string_TLV_with_tag_unfold x509_authKeyID_keyIdentifier_tag
module X509.ExtFields.AuthorityKeyIdentifier

open LowParse.Spec.Base
open LowParse.Spec.Combinators

open ASN1.Base
open ASN1.Spec
open ASN1.Low


open X509.Base

module B32 = FStar.Bytes

open FStar.Integers

// open X509.BasicFields.RelativeDistinguishedName
// open X509.BasicFields.SerialNumber

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

(* 4.2.1.1.  Authority Key Identifier

   ...

   The value of the keyIdentifier field SHOULD be derived from the
   public key used to verify the certificate's signature or a method
   that generates unique values.  Two common methods for generating key
   identifiers from the public key are described in Section 4.2.1.2.
   Where a key identifier has not been previously established, this
   specification RECOMMENDS use of one of these methods for generating
   keyIdentifiers or use of a similar method that uses a different hash
   algorithm.  Where a key identifier has been previously established,
   the CA SHOULD use the previously established identifier.

   This profile RECOMMENDS support for the key identifier method by all
   certificate users.

   Conforming CAs MUST mark this extension as non-critical.

   id-ce-authorityKeyIdentifier OBJECT IDENTIFIER ::=  { id-ce 35 }

   AuthorityKeyIdentifier ::= SEQUENCE {
      keyIdentifier             [0] KeyIdentifier           OPTIONAL,
      authorityCertIssuer       [1] GeneralNames            OPTIONAL,
      authorityCertSerialNumber [2] CertificateSerialNumber OPTIONAL  }

   KeyIdentifier ::= OCTET STRING

 *)

let x509_authKeyID_keyIdentifier_tag: asn1_tag_t
= (CUSTOM_TAG CONTEXT_SPECIFIC PRIMITIVE 0uy)

(* Not supporting them for now *)
// let x509_authKeyID_CertIssuer_tag: asn1_tag_t
// = (CUSTOM_TAG CONTEXT_SPECIFIC CONSTRUCTED 1uy)

// let x509_authKeyID_CertSN_tag: asn1_tag_t
// = (CUSTOM_TAG CONTEXT_SPECIFIC CONSTRUCTED 2uy)

(* keyIdentifier *)

let x509_authKeyID_keyIdentifier_t
= datatype_of_asn1_type OCTET_STRING

let parse_x509_authKeyID_keyIdentifier
: parser _ x509_authKeyID_keyIdentifier_t
= parse_asn1_octet_string_TLV_with_tag x509_authKeyID_keyIdentifier_tag

let serialize_x509_authKeyID_keyIdentifier
: serializer parse_x509_authKeyID_keyIdentifier
= serialize_asn1_octet_string_TLV_with_tag x509_authKeyID_keyIdentifier_tag

noextract inline_for_extraction
val serialize32_x509_authKeyID_keyIdentifier_backwards
: serializer32_backwards serialize_x509_authKeyID_keyIdentifier
/
X509.Base.fst.checked prims.fst.checked LowParse.Spec.Combinators.fsti.checked LowParse.Spec.Base.fsti.checked FStar.UInt8.fsti.checked FStar.Pervasives.fsti.checked FStar.Integers.fst.checked FStar.Bytes.fsti.checked ASN1.Spec.fst.checked ASN1.Low.fst.checked ASN1.Base.fst.checked
X509.ExtFields.AuthorityKeyIdentifier.fsti
value: ASN1.Base.datatype_of_asn1_type ASN1.Base.OCTET_STRING
  -> FStar.Pervasives.Lemma
    (ensures
      LowParse.Spec.Base.serialize (ASN1.Spec.Value.OCTET_STRING.serialize_asn1_octet_string_TLV_with_tag
            X509.ExtFields.AuthorityKeyIdentifier.x509_authKeyID_keyIdentifier_tag)
        value ==
      FStar.Seq.Base.append (FStar.Seq.Base.append (LowParse.Spec.Base.serialize (ASN1.Spec.Tag.serialize_asn1_tag_of_type
                    X509.ExtFields.AuthorityKeyIdentifier.x509_authKeyID_keyIdentifier_tag)
                X509.ExtFields.AuthorityKeyIdentifier.x509_authKeyID_keyIdentifier_tag)
            (LowParse.Spec.Base.serialize (ASN1.Spec.Length.serialize_asn1_length_of_type ASN1.Base.OCTET_STRING
                  )
                (Mkoctet_string_t?.len value)))
        (LowParse.Spec.Base.serialize (ASN1.Spec.Value.OCTET_STRING.serialize_asn1_octet_string (FStar.Integers.v
                    (Mkoctet_string_t?.len value)))
            value))
ASN1.Spec.Value.OCTET_STRING.lemma_serialize_asn1_octet_string_TLV_with_tag_unfold X509.ExtFields.AuthorityKeyIdentifier.x509_authKeyID_keyIdentifier_tag
let lemma_serialize_x509_authKeyID_keyIdentifier_unfold =
  
lemma_serialize_asn1_octet_string_TLV_with_tag_unfold x509_authKeyID_keyIdentifier_tag