val lemma_serialize_deviceIDCSR_size_exact
  (cri_len: asn1_int32)
  (x: deviceIDCSR_t cri_len)
: Lemma (
  let _ = lemma_serialize_deviceIDCSR_payload_size cri_len x in
  (* exact size *)
  length_of_opaque_serialization (serialize_deviceIDCSR cri_len) x
  == length_of_deviceIDCSR cri_len /\
  (* upper bound *)
  length_of_opaque_serialization (serialize_deviceIDCSR cri_len) x
  <= v cri_len + 84
)
val lemma_serialize_deviceIDCSR_size_exact
  (cri_len: asn1_int32)
  (x: deviceIDCSR_t cri_len)
: Lemma (
  let _ = lemma_serialize_deviceIDCSR_payload_size cri_len x in
  (* exact size *)
  length_of_opaque_serialization (serialize_deviceIDCSR cri_len) x
  == length_of_deviceIDCSR cri_len /\
  (* upper bound *)
  length_of_opaque_serialization (serialize_deviceIDCSR cri_len) x
  <= v cri_len + 84
)
let lemma_serialize_deviceIDCSR_size_exact cri_len x
= lemma_serialize_deviceIDCSR_size cri_len x;
  (**) lemma_serialize_deviceIDCSR_payload_size cri_len x
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'"

let decl = ()

let deviceIDCSR_payload_t' (cri_len: asn1_int32) = (
  (B32.lbytes32 cri_len `tuple2`
   algorithmIdentifier_t) `tuple2`
   x509_signature_t
)

let synth_deviceIDCSR_payload_t
  (cri_len: asn1_int32)
  (x': deviceIDCSR_payload_t' cri_len)
: GTot (deviceIDCSR_payload_t cri_len)
= { deviceIDCSR_cri     = fst (fst x');
    deviceIDCSR_sig_alg = snd (fst x');
    deviceIDCSR_sig     = snd x' }

inline_for_extraction noextract
let synth_deviceIDCSR_payload_t'
  (cri_len: asn1_int32)
  (x: deviceIDCSR_payload_t cri_len)
: Tot (x': deviceIDCSR_payload_t' cri_len { x == synth_deviceIDCSR_payload_t cri_len x' })
= (x.deviceIDCSR_cri,
   x.deviceIDCSR_sig_alg),
   x.deviceIDCSR_sig

let parse_deviceIDCSR_payload cri_len
= parse_flbytes32 cri_len
  `nondep_then`
  parse_algorithmIdentifier
  `nondep_then`
  parse_x509_signature
  `parse_synth`
  synth_deviceIDCSR_payload_t cri_len

let serialize_deviceIDCSR_payload cri_len
= serialize_synth
  (* p1 *) (parse_flbytes32 cri_len
            `nondep_then`
            parse_algorithmIdentifier
            `nondep_then`
            parse_x509_signature)
  (* f2 *) (synth_deviceIDCSR_payload_t cri_len)
  (* s1 *) (serialize_flbytes32 cri_len
            `serialize_nondep_then`
            serialize_algorithmIdentifier
            `serialize_nondep_then`
            serialize_x509_signature)
  (* g1 *) (synth_deviceIDCSR_payload_t' cri_len)
  (* prf*) ()

let lemma_serialize_deviceIDCSR_payload_unfold cri_len x
= serialize_nondep_then_eq
  (* s1 *) (serialize_flbytes32 cri_len)
  (* s2 *) (serialize_algorithmIdentifier)
  (* in *) (fst (synth_deviceIDCSR_payload_t' cri_len x));
  serialize_nondep_then_eq
  (* s1 *) (serialize_flbytes32 cri_len
            `serialize_nondep_then`
            serialize_algorithmIdentifier)
  (* s2 *) (serialize_x509_signature)
  (* in *) (synth_deviceIDCSR_payload_t' cri_len x);
  serialize_synth_eq
  (* p1 *) (parse_flbytes32 cri_len
            `nondep_then`
            parse_algorithmIdentifier
            `nondep_then`
            parse_x509_signature)
  (* f2 *) (synth_deviceIDCSR_payload_t cri_len)
  (* s1 *) (serialize_flbytes32 cri_len
            `serialize_nondep_then`
            serialize_algorithmIdentifier
            `serialize_nondep_then`
            serialize_x509_signature)
  (* g1 *) (synth_deviceIDCSR_payload_t' cri_len)
  (* prf*) ()
  (* in *) x

let lemma_serialize_deviceIDCSR_payload_size cri_len x
= lemma_serialize_deviceIDCSR_payload_unfold cri_len x;
  (**) lemma_serialize_algorithmIdentifier_size_exact x.deviceIDCSR_sig_alg;
  (**) lemma_serialize_x509_signature_size      x.deviceIDCSR_sig

let lemma_serialize_deviceIDCSR_unfold cri_len x
= lemma_serialize_asn1_sequence_TLV_unfold (serialize_deviceIDCSR_payload cri_len) x

let lemma_serialize_deviceIDCSR_size cri_len x
= lemma_serialize_asn1_sequence_TLV_size (serialize_deviceIDCSR_payload cri_len) x
/
X509.fst.checked prims.fst.checked L0.X509.DeviceIDCRI.fsti.checked FStar.Pervasives.Native.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.fst
cri_len: ASN1.Base.asn1_int32 -> x: L0.X509.DeviceIDCSR.deviceIDCSR_t cri_len
  -> FStar.Pervasives.Lemma
    (ensures
      ([@@ FStar.Pervasives.inline_let ]let _ =
          L0.X509.DeviceIDCSR.lemma_serialize_deviceIDCSR_payload_size cri_len x
        in
        ASN1.Spec.Base.length_of_opaque_serialization (L0.X509.DeviceIDCSR.serialize_deviceIDCSR cri_len
            )
          x ==
        L0.X509.DeviceIDCSR.length_of_deviceIDCSR cri_len /\
        ASN1.Spec.Base.length_of_opaque_serialization (L0.X509.DeviceIDCSR.serialize_deviceIDCSR cri_len
            )
          x <=
        FStar.Integers.v cri_len + 84))
ASN1.Base.asn1_int32 L0.X509.DeviceIDCSR.deviceIDCSR_t L0.X509.DeviceIDCSR.lemma_serialize_deviceIDCSR_payload_size Prims.unit L0.X509.DeviceIDCSR.lemma_serialize_deviceIDCSR_size
let lemma_serialize_deviceIDCSR_size_exact cri_len x =
  
lemma_serialize_deviceIDCSR_size cri_len x;
lemma_serialize_deviceIDCSR_payload_size cri_len x