val x509_KU_KEY_ENCIPHERMENT:key_usage_payload_t
val x509_KU_KEY_ENCIPHERMENT:key_usage_payload_t
let x509_KU_KEY_ENCIPHERMENT  :key_usage_payload_t = 0x20l
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 *)
/
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
X509.ExtFields.KeyUsage.key_usage_payload_t
FStar.Int32.__int_to_t
let x509_KU_KEY_ENCIPHERMENT:key_usage_payload_t =
  
0x20l