val parse_deviceIDCSR_payload_kind (cri_len: asn1_int32) : parser_kind
val parse_deviceIDCSR_payload_kind (cri_len: asn1_int32) : parser_kind
let parse_deviceIDCSR_payload_kind
  (cri_len: asn1_int32)
: parser_kind
= total_constant_size_parser_kind (v cri_len)
  `and_then_kind`
  parse_asn1_envelop_tag_with_TLV_kind SEQUENCE
  `and_then_kind`
  parse_x509_signature_kind
module L0.X509.DeviceIDCSR

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

module B32 = FStar.Bytes

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

val decl : unit

noeq
type deviceIDCSR_payload_t (cri_len: asn1_int32) = {
  deviceIDCSR_cri: B32.lbytes32 cri_len;
  deviceIDCSR_sig_alg: algorithmIdentifier_t;
  deviceIDCSR_sig: x509_signature_t
}
/
X509.fst.checked prims.fst.checked L0.X509.DeviceIDCRI.fsti.checked FStar.UInt32.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.fsti.checked FStar.Integers.fst.checked FStar.Bytes.fsti.checked ASN1.Spec.fst.checked ASN1.Low.fst.checked
L0.X509.DeviceIDCSR.fsti
cri_len: ASN1.Base.asn1_int32 -> LowParse.Spec.Base.parser_kind
ASN1.Base.asn1_int32 LowParse.Spec.Combinators.and_then_kind LowParse.Spec.Base.total_constant_size_parser_kind FStar.Integers.v FStar.Integers.Unsigned FStar.Integers.W32 ASN1.Spec.Value.Envelop.parse_asn1_envelop_tag_with_TLV_kind ASN1.Base.SEQUENCE X509.Crypto.Signature.parse_x509_signature_kind LowParse.Spec.Base.parser_kind
let parse_deviceIDCSR_payload_kind (cri_len: asn1_int32) : parser_kind =
  
((total_constant_size_parser_kind (v cri_len))
  `and_then_kind`
  (parse_asn1_envelop_tag_with_TLV_kind SEQUENCE))
`and_then_kind`
parse_x509_signature_kind