val parse_deviceIDCRI_attributes_extensionRequest_payload
: parser (parse_asn1_envelop_tag_with_TLV_kind SEQUENCE) deviceIDCRI_attributes_extensionRequest_payload_t
val parse_deviceIDCRI_attributes_extensionRequest_payload
: parser (parse_asn1_envelop_tag_with_TLV_kind SEQUENCE) deviceIDCRI_attributes_extensionRequest_payload_t
let parse_deviceIDCRI_attributes_extensionRequest_payload
= parse_x509_key_usage
  `parse_synth`
  synth_deviceIDCRI_attributes_extensionRequest_payload_t
module L0.X509.DeviceIDCRI.Attributes

open ASN1.Spec
open ASN1.Low
open X509
open FStar.Integers

module B32 = FStar.Bytes

open LowParse.Spec.SeqBytes.Base
open LowParse.Spec.Bytes

(*
 *   {
 *     ...
 *     attributes    [0] Attributes{{ CRIAttributes }}
 *     ...
 *   }
 *
 *   Attributes { ATTRIBUTE:IOSet } ::= SET OF Attribute{{ IOSet }}
 *
 *    CRIAttributes  ATTRIBUTE  ::= {
 *         ... -- add any locally defined attributes here -- }
 *
 *    Attribute { ATTRIBUTE:IOSet } ::= SEQUENCE {
 *         type   ATTRIBUTE.&id({IOSet}),
 *         values SET SIZE(1..MAX) OF ATTRIBUTE.&Type({IOSet}{@type})
 *    }
 *
 *
 *    RFC 2985 PKCS #9 5.4.2:
 *
 *    extensionRequest ATTRIBUTE ::= {
 *         WITH SYNTAX ExtensionRequest
 *         SINGLE VALUE TRUE
 *         ID pkcs-9-at-extensionRequest
 *    }
 *
 *    ExtensionRequest ::= Extensions
 *
 *    pkcs-9-at-extensionRequest         OBJECT IDENTIFIER ::= {pkcs-9 14}
 *)

(*
 *   SEQUENCE {
 *      SEQUENCE {...}
 *      ...
 *   }
 *)

#set-options "--z3rlimit 128 --fuel 0 --ifuel 0 --using_facts_from '* -FStar.Tactics -FStar.Reflection'"

let decl = ()

let deviceIDCRI_attributes_extensionRequest_payload_t' = (
  key_usage_t
)

(* Conversion of message between record and tuple types *)
let synth_deviceIDCRI_attributes_extensionRequest_payload_t
  (x: deviceIDCRI_attributes_extensionRequest_payload_t')
: GTot (deviceIDCRI_attributes_extensionRequest_payload_t) = {
  deviceID_attr_ext_key_usage = x
}

inline_for_extraction noextract
let synth_deviceIDCRI_attributes_extensionRequest_payload_t'
  (x: deviceIDCRI_attributes_extensionRequest_payload_t)
: Tot (x': deviceIDCRI_attributes_extensionRequest_payload_t'
           { x == synth_deviceIDCRI_attributes_extensionRequest_payload_t x' }) = (
  x.deviceID_attr_ext_key_usage
)
/
X509.fst.checked prims.fst.checked LowParse.Spec.SeqBytes.Base.fst.checked LowParse.Spec.Bytes.fst.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
L0.X509.DeviceIDCRI.Attributes.fst
LowParse.Spec.Base.parser (ASN1.Spec.Value.Envelop.parse_asn1_envelop_tag_with_TLV_kind ASN1.Base.SEQUENCE
    )
  L0.X509.DeviceIDCRI.Attributes.deviceIDCRI_attributes_extensionRequest_payload_t
LowParse.Spec.Combinators.parse_synth ASN1.Spec.Value.Envelop.parse_asn1_envelop_tag_with_TLV_kind ASN1.Base.SEQUENCE X509.ExtFields.KeyUsage.key_usage_t L0.X509.DeviceIDCRI.Attributes.deviceIDCRI_attributes_extensionRequest_payload_t X509.ExtFields.KeyUsage.parse_x509_key_usage L0.X509.DeviceIDCRI.Attributes.synth_deviceIDCRI_attributes_extensionRequest_payload_t
let parse_deviceIDCRI_attributes_extensionRequest_payload =
  
parse_x509_key_usage `parse_synth` synth_deviceIDCRI_attributes_extensionRequest_payload_t