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)
)
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 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
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*) ()
/
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_payload_t cri_len
  -> FStar.Pervasives.Lemma
    (ensures
      LowParse.Spec.Base.serialize (L0.X509.DeviceIDCSR.serialize_deviceIDCSR_payload cri_len) x ==
      FStar.Seq.Base.append (FStar.Seq.Base.append (LowParse.Spec.Base.serialize (ASN1.Spec.Bytes32.serialize_flbytes32
                    cri_len)
                (MkdeviceIDCSR_payload_t?.deviceIDCSR_cri x))
            (LowParse.Spec.Base.serialize X509.Crypto.AlgorithmIdentifier.serialize_algorithmIdentifier
                (MkdeviceIDCSR_payload_t?.deviceIDCSR_sig_alg x)))
        (LowParse.Spec.Base.serialize X509.Crypto.Signature.serialize_x509_signature
            (MkdeviceIDCSR_payload_t?.deviceIDCSR_sig x)))
ASN1.Base.asn1_int32 L0.X509.DeviceIDCSR.deviceIDCSR_payload_t LowParse.Spec.Combinators.serialize_synth_eq 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 FStar.Pervasives.Native.tuple2 FStar.Bytes.lbytes32 X509.Crypto.AlgorithmIdentifier.algorithmIdentifier_t X509.Crypto.Signature.x509_signature_t LowParse.Spec.Combinators.nondep_then ASN1.Spec.Bytes32.parse_flbytes32 X509.Crypto.AlgorithmIdentifier.parse_algorithmIdentifier X509.Crypto.Signature.parse_x509_signature L0.X509.DeviceIDCSR.synth_deviceIDCSR_payload_t LowParse.Spec.Combinators.serialize_nondep_then ASN1.Spec.Bytes32.serialize_flbytes32 X509.Crypto.AlgorithmIdentifier.serialize_algorithmIdentifier X509.Crypto.Signature.serialize_x509_signature L0.X509.DeviceIDCSR.synth_deviceIDCSR_payload_t' Prims.unit LowParse.Spec.Combinators.serialize_nondep_then_eq FStar.Pervasives.Native.fst
let lemma_serialize_deviceIDCSR_payload_unfold cri_len x =
  
serialize_nondep_then_eq (serialize_flbytes32 cri_len)
  (serialize_algorithmIdentifier)
  (fst (synth_deviceIDCSR_payload_t' cri_len x));
serialize_nondep_then_eq ((serialize_flbytes32 cri_len)
    `serialize_nondep_then`
    serialize_algorithmIdentifier)
  (serialize_x509_signature)
  (synth_deviceIDCSR_payload_t' cri_len x);
serialize_synth_eq (((parse_flbytes32 cri_len) `nondep_then` parse_algorithmIdentifier)
    `nondep_then`
    parse_x509_signature)
  (synth_deviceIDCSR_payload_t cri_len)
  (((serialize_flbytes32 cri_len) `serialize_nondep_then` serialize_algorithmIdentifier)
    `serialize_nondep_then`
    serialize_x509_signature)
  (synth_deviceIDCSR_payload_t' cri_len)
  ()
  x