val length_of_deviceIDCSR_payload (cri_len: asn1_int32) : GTot (nat)
val length_of_deviceIDCSR_payload (cri_len: asn1_int32) : GTot (nat)
let length_of_deviceIDCSR_payload
  (cri_len: asn1_int32)
: GTot (nat)
= v cri_len + 74
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
}

inline_for_extraction noextract
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

noextract
val parse_deviceIDCSR_payload
  (cri_len: asn1_int32)
: parser
  (parse_deviceIDCSR_payload_kind cri_len)
  (deviceIDCSR_payload_t cri_len)

noextract
val serialize_deviceIDCSR_payload
  (cri_len: asn1_int32)
: serializer (parse_deviceIDCSR_payload cri_len)

val lemma_serialize_deviceIDCSR_payload_unfold
  (cri_len: asn1_int32)
  (x: deviceIDCSR_payload_t cri_len)
: Lemma (
  serialize_deviceIDCSR_payload cri_len `serialize` x ==
 (serialize_flbytes32 cri_len `serialize` x.deviceIDCSR_cri)
  `Seq.append`
 (serialize_algorithmIdentifier `serialize` x.deviceIDCSR_sig_alg)
  `Seq.append`
 (serialize_x509_signature `serialize` x.deviceIDCSR_sig)
)
/
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 -> Prims.GTot FStar.Integers.nat
ASN1.Base.asn1_int32 FStar.Integers.op_Plus FStar.Integers.Signed FStar.Integers.Winfinite FStar.Integers.v FStar.Integers.Unsigned FStar.Integers.W32 FStar.Integers.nat
let length_of_deviceIDCSR_payload (cri_len: asn1_int32) : GTot (nat) =
  
v cri_len + 74