val serialize_x509_key_usage:serializer (parse_x509_key_usage)
val serialize_x509_key_usage:serializer (parse_x509_key_usage)
let serialize_x509_key_usage
: serializer (parse_x509_key_usage)
= coerce_parser_serializer
  (* p *) (parse_x509_key_usage)
  (* s *) (serialize_asn1_sequence_TLV
            (OID_KEY_USAGE
             `serialize_envelop_OID_with`
            (OCTET_STRING
             `serialize_asn1_envelop_tag_with_TLV`
             _serialize_x509_key_usage_payload)))
  (*prf*) ()
module X509.ExtFields.KeyUsage

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

(*
 * /*
 *  * X.509 v3 Key Usage Extension flags
 *  * Reminder: update x509_info_key_usage() when adding new flags.
 *  */
 * #define MBEDTLS_X509_KU_DIGITAL_SIGNATURE            (0x80)  /* bit 0 */
 * #define MBEDTLS_X509_KU_NON_REPUDIATION              (0x40)  /* bit 1 */
 * #define MBEDTLS_X509_KU_KEY_ENCIPHERMENT             (0x20)  /* bit 2 */
 * #define MBEDTLS_X509_KU_DATA_ENCIPHERMENT            (0x10)  /* bit 3 */
 * #define MBEDTLS_X509_KU_KEY_AGREEMENT                (0x08)  /* bit 4 */
 * #define MBEDTLS_X509_KU_KEY_CERT_SIGN                (0x04)  /* bit 5 */
 * #define MBEDTLS_X509_KU_CRL_SIGN                     (0x02)  /* bit 6 */
 * #define MBEDTLS_X509_KU_ENCIPHER_ONLY                (0x01)  /* bit 7 */
 * #define MBEDTLS_X509_KU_DECIPHER_ONLY              (0x8000)  /* bit 8 */
 *)

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

let valid_key_usage
  (i: int_32)
: Type0
= 0l < i /\ (* at least one usage *)
  (i <= 0xFFl \/ i / 0x100l == 0x80l)

let key_usage_payload_t = i: int_32
                     { valid_key_usage i }

let x509_KU_DIGITAL_SIGNATURE :key_usage_payload_t = 0x80l    (* bit 0 *)
let x509_KU_NON_REPUDIATION   :key_usage_payload_t = 0x40l    (* bit 1 *)
let x509_KU_KEY_ENCIPHERMENT  :key_usage_payload_t = 0x20l    (* bit 2 *)
let x509_KU_DATA_ENCIPHERMENT :key_usage_payload_t = 0x10l    (* bit 3 *)
let x509_KU_KEY_AGREEMENT     :key_usage_payload_t = 0x08l    (* bit 4 *)
let x509_KU_KEY_CERT_SIGN     :key_usage_payload_t = 0x04l    (* bit 5 *)
let x509_KU_CRL_SIGN          :key_usage_payload_t = 0x02l    (* bit 6 *)
let x509_KU_ENCIPHER_ONLY     :key_usage_payload_t = 0x01l    (* bit 7 *)
let x509_KU_DECIPHER_ONLY     :key_usage_payload_t = 0x8000l  (* bit 8 *)

// val lemma_key_usage_close_under_or
//   (ku1 ku2: key_usage_payload_t)
// : Lemma (
//   valid_key_usage (ku1 |^ ku2)
// )

// val op_ku_with
//   (ku1 ku2: key_usage_payload_t)
// : Tot (ku: key_usage_payload_t
//            { ku == (ku1 |^ ku2) })

inline_for_extraction noextract
let _parse_x509_key_usage_payload_kind
: parser_kind
= parse_filter_kind (parse_asn1_TLV_kind_of_type BIT_STRING)

val _parse_x509_key_usage_payload
: parser _parse_x509_key_usage_payload_kind key_usage_payload_t

val _serialize_x509_key_usage_payload
: serializer _parse_x509_key_usage_payload

// NOTE: Drop the support for reasoning about actual byte content for now
// val lemma_serialize_x509_key_usage_payload_unfold
//   (ku: key_usage_payload_t)
// : Lemma (
//   serialize _serialize_x509_key_usage_payload ku ==
//   serialize (serialize_asn1_TLV_of_type BIT_STRING) (_synth_x509_key_usage_payload_inverse ku)
// )

let length_of_x509_key_usage_payload ()
: GTot (nat)
= 5

let len_of_x509_key_usage_payload ()
: Tot (len: asn1_value_int32_of_type SEQUENCE
            { v len == length_of_x509_key_usage_payload () })
= 5ul

val lemma_serialize_x509_key_usage_payload_size
  (ku: key_usage_payload_t)
: Lemma (
  length_of_opaque_serialization _serialize_x509_key_usage_payload ku ==
  length_of_x509_key_usage_payload ()
)

(* Complete X509 Key Usage Parser and Serializer for
 *
 *  SEQUENCE {
 *    extID   : OID
 *    extValue: OCTET_STRING {
 *      key_usage    : key_usage_payload_t
 *    }
 *  }
 *
 *)

let key_usage_t
= inbound_sequence_value_of
    (OID_KEY_USAGE
     `serialize_envelop_OID_with`
    (OCTET_STRING
     `serialize_asn1_envelop_tag_with_TLV`
     _serialize_x509_key_usage_payload))

let parse_x509_key_usage
: parser (parse_asn1_envelop_tag_with_TLV_kind SEQUENCE) key_usage_t
= key_usage_t
  `coerce_parser`
 (parse_asn1_sequence_TLV
    (OID_KEY_USAGE
     `serialize_envelop_OID_with`
    (OCTET_STRING
     `serialize_asn1_envelop_tag_with_TLV`
     _serialize_x509_key_usage_payload)))
/
X509.Base.fst.checked prims.fst.checked LowParse.Spec.Combinators.fsti.checked LowParse.Spec.Base.fsti.checked FStar.UInt32.fsti.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Integers.fst.checked FStar.Int32.fsti.checked FStar.Bytes.fsti.checked ASN1.Spec.fst.checked ASN1.Low.fst.checked ASN1.Base.fst.checked
X509.ExtFields.KeyUsage.fsti
LowParse.Spec.Base.serializer X509.ExtFields.KeyUsage.parse_x509_key_usage
ASN1.Spec.Base.coerce_parser_serializer X509.ExtFields.KeyUsage.key_usage_t ASN1.Spec.Value.Envelop.parse_asn1_envelop_tag_with_TLV_kind ASN1.Base.SEQUENCE ASN1.Spec.Value.SEQUENCE.inbound_sequence_value_of LowParse.Spec.Combinators.and_then_kind LowParse.Spec.Combinators.parse_filter_kind ASN1.Spec.Value.OID.parse_asn1_oid_TLV_kind ASN1.Base.OCTET_STRING ASN1.Spec.Value.OID.envelop_OID_with_t ASN1.Base.OID_KEY_USAGE ASN1.Spec.Value.Envelop.inbound_envelop_tag_with_value_of X509.ExtFields.KeyUsage._parse_x509_key_usage_payload_kind X509.ExtFields.KeyUsage.key_usage_payload_t X509.ExtFields.KeyUsage._parse_x509_key_usage_payload X509.ExtFields.KeyUsage._serialize_x509_key_usage_payload ASN1.Spec.Value.OID.parse_envelop_OID_with ASN1.Spec.Value.Envelop.parse_asn1_envelop_tag_with_TLV ASN1.Spec.Value.Envelop.serialize_asn1_envelop_tag_with_TLV ASN1.Spec.Value.OID.serialize_envelop_OID_with ASN1.Spec.Value.SEQUENCE.parse_asn1_sequence_TLV X509.ExtFields.KeyUsage.parse_x509_key_usage ASN1.Spec.Value.SEQUENCE.serialize_asn1_sequence_TLV
let serialize_x509_key_usage:serializer (parse_x509_key_usage) =
  
coerce_parser_serializer (parse_x509_key_usage)
  (serialize_asn1_sequence_TLV (OID_KEY_USAGE
        `serialize_envelop_OID_with`
        (OCTET_STRING `serialize_asn1_envelop_tag_with_TLV` _serialize_x509_key_usage_payload)))
  ()