val len_of_deviceIDCSR_payload
      (cri_len:
          asn1_int32
            {length_of_deviceIDCSR_payload cri_len <= asn1_value_length_max_of_type SEQUENCE})
    : Tot (len: asn1_TLV_int32_of_type SEQUENCE {v len == length_of_deviceIDCSR_payload cri_len})
val len_of_deviceIDCSR_payload
      (cri_len:
          asn1_int32
            {length_of_deviceIDCSR_payload cri_len <= asn1_value_length_max_of_type SEQUENCE})
    : Tot (len: asn1_TLV_int32_of_type SEQUENCE {v len == length_of_deviceIDCSR_payload cri_len})
let len_of_deviceIDCSR_payload
  (cri_len: asn1_int32
            { length_of_deviceIDCSR_payload cri_len
              <= asn1_value_length_max_of_type SEQUENCE })
: Tot (len: asn1_TLV_int32_of_type SEQUENCE
            { v len == length_of_deviceIDCSR_payload cri_len })
= cri_len + 74ul
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)
)

let length_of_deviceIDCSR_payload
  (cri_len: asn1_int32)
: GTot (nat)
= v cri_len + 74
/
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
        { L0.X509.DeviceIDCSR.length_of_deviceIDCSR_payload cri_len <=
          ASN1.Base.asn1_value_length_max_of_type ASN1.Base.SEQUENCE }
  -> len:
    ASN1.Base.asn1_TLV_int32_of_type ASN1.Base.SEQUENCE
      {FStar.Integers.v len == L0.X509.DeviceIDCSR.length_of_deviceIDCSR_payload cri_len}
ASN1.Base.asn1_int32 Prims.b2t FStar.Integers.op_Less_Equals FStar.Integers.Signed FStar.Integers.Winfinite L0.X509.DeviceIDCSR.length_of_deviceIDCSR_payload ASN1.Base.asn1_value_length_max_of_type ASN1.Base.SEQUENCE FStar.Integers.op_Plus FStar.Integers.Unsigned FStar.Integers.W32 FStar.UInt32.__uint_to_t ASN1.Base.asn1_TLV_int32_of_type Prims.eq2 FStar.Integers.int_t Prims.l_or FStar.Integers.within_bounds FStar.Integers.op_Greater_Equals FStar.Integers.v
let len_of_deviceIDCSR_payload
      (cri_len:
          asn1_int32
            {length_of_deviceIDCSR_payload cri_len <= asn1_value_length_max_of_type SEQUENCE})
    : Tot (len: asn1_TLV_int32_of_type SEQUENCE {v len == length_of_deviceIDCSR_payload cri_len}) =
  
cri_len + 74ul