val len_of_x509_key_usage_payload: Prims.unit
  -> Tot (len: asn1_value_int32_of_type SEQUENCE {v len == length_of_x509_key_usage_payload ()})
val len_of_x509_key_usage_payload: Prims.unit
  -> Tot (len: asn1_value_int32_of_type SEQUENCE {v len == length_of_x509_key_usage_payload ()})
let len_of_x509_key_usage_payload ()
: Tot (len: asn1_value_int32_of_type SEQUENCE
            { v len == length_of_x509_key_usage_payload () })
= 5ul
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
/
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
_: Prims.unit
  -> len:
    ASN1.Base.asn1_value_int32_of_type ASN1.Base.SEQUENCE
      {FStar.Integers.v len == X509.ExtFields.KeyUsage.length_of_x509_key_usage_payload ()}
Prims.unit FStar.UInt32.__uint_to_t ASN1.Base.asn1_value_int32_of_type ASN1.Base.SEQUENCE Prims.eq2 FStar.Integers.int_t FStar.Integers.Signed FStar.Integers.Winfinite Prims.l_or FStar.Integers.within_bounds FStar.Integers.Unsigned FStar.Integers.W32 Prims.b2t FStar.Integers.op_Greater_Equals FStar.Integers.v X509.ExtFields.KeyUsage.length_of_x509_key_usage_payload
let len_of_x509_key_usage_payload ()
    : Tot (len: asn1_value_int32_of_type SEQUENCE {v len == length_of_x509_key_usage_payload ()}) =
  
5ul