val x509_get_compositeDeviceID
      (version: datatype_of_asn1_type INTEGER)
      (deviceKeyPub fwid: B32.lbytes32 32ul)
    : Tot (compositeDeviceID_t)
val x509_get_compositeDeviceID
      (version: datatype_of_asn1_type INTEGER)
      (deviceKeyPub fwid: B32.lbytes32 32ul)
    : Tot (compositeDeviceID_t)
let x509_get_compositeDeviceID
  (version: datatype_of_asn1_type INTEGER)
  (deviceKeyPub: B32.lbytes32 32ul)
  (fwid: B32.lbytes32 32ul)
: Tot (compositeDeviceID_t)
= let deviceIDPublicKeyInfo: subjectPublicKeyInfo_t = x509_get_subjectPublicKeyInfo deviceKeyPub in
  (* Prf *) lemma_serialize_subjectPublicKeyInfo_size_exact deviceIDPublicKeyInfo;

  let fwid: fwid_payload_t = x509_get_fwid fwid in
  (* Prf *) lemma_serialize_fwid_size_exact fwid;

  let compositeDeviceID: compositeDeviceID_payload_t = {
    l0_version  = version;
    l0_deviceID = deviceIDPublicKeyInfo;
    l0_fwid     = fwid
  } in
  (* Prf *) lemma_serialize_compositeDeviceID_payload_size compositeDeviceID;
  (* Prf *) (**) lemma_serialize_asn1_integer_TLV_size compositeDeviceID.l0_version;

(* return *) compositeDeviceID
module L0.X509.CompositeDeviceID

open LowParse.Low.Base
open LowParse.Low.Combinators

open ASN1.Spec
open ASN1.Low

open X509.Base
open X509.BasicFields.SubjectPublicKeyInfo
open X509.Crypto
open L0.X509.Base
open L0.X509.FWID

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

val decl : unit

(* CompositeDeviceID *)
type compositeDeviceID_payload_t
= { l0_version : datatype_of_asn1_type INTEGER;
    l0_deviceID: subjectPublicKeyInfo_t;
    l0_fwid    : fwid_t }

inline_for_extraction noextract
let parse_compositeDeviceID_payload_kind
: parser_kind
= parse_asn1_TLV_kind_of_type INTEGER
  `and_then_kind`
  parse_asn1_envelop_tag_with_TLV_kind SEQUENCE
  `and_then_kind`
  parse_asn1_envelop_tag_with_TLV_kind SEQUENCE

noextract
val parse_compositeDeviceID_payload
: parser parse_compositeDeviceID_payload_kind (compositeDeviceID_payload_t)

noextract
val serialize_compositeDeviceID_payload
: serializer (parse_compositeDeviceID_payload)

val lemma_serialize_compositeDeviceID_payload_unfold
  (x: compositeDeviceID_payload_t)
: Lemma (
  serialize (serialize_compositeDeviceID_payload) x ==
  serialize (serialize_asn1_TLV_of_type INTEGER) x.l0_version
  `Seq.append`
  serialize (serialize_subjectPublicKeyInfo) x.l0_deviceID
  `Seq.append`
  serialize serialize_fwid x.l0_fwid
)

val lemma_serialize_compositeDeviceID_payload_size
  (x: compositeDeviceID_payload_t)
: Lemma (
  length_of_opaque_serialization (serialize_compositeDeviceID_payload) x ==
  length_of_asn1_primitive_TLV x.l0_version +
  length_of_opaque_serialization (serialize_subjectPublicKeyInfo) x.l0_deviceID +
  length_of_opaque_serialization serialize_fwid x.l0_fwid /\
  length_of_opaque_serialization serialize_compositeDeviceID_payload x ==
  length_of_asn1_primitive_TLV x.l0_version + 91 /\
  length_of_opaque_serialization serialize_compositeDeviceID_payload x <= 97
)

(* inbound sub type*)
let compositeDeviceID_t
= inbound_sequence_value_of (serialize_compositeDeviceID_payload)


(* TLV serializer *)
noextract
let parse_compositeDeviceID
: parser (parse_asn1_envelop_tag_with_TLV_kind SEQUENCE) (compositeDeviceID_t)
= compositeDeviceID_t
  `coerce_parser`
  parse_asn1_sequence_TLV (serialize_compositeDeviceID_payload)

noextract
let serialize_compositeDeviceID
: serializer (parse_compositeDeviceID)
= coerce_parser_serializer
  (* t *) (parse_compositeDeviceID)
  (* s *) (serialize_asn1_sequence_TLV (serialize_compositeDeviceID_payload))
  (*prf*) ()

(* manually unfolding `lemma_serialize_asn1_sequence_TLV_size` to avoid stuck here.  *)
val lemma_serialize_compositeDeviceID_unfold
  (x: compositeDeviceID_t)
: Lemma ( predicate_serialize_asn1_sequence_TLV_unfold serialize_compositeDeviceID_payload x )

val lemma_serialize_compositeDeviceID_size
  (x: compositeDeviceID_t)
: Lemma ( predicate_serialize_asn1_sequence_TLV_size serialize_compositeDeviceID_payload x )

open FStar.Integers
val lemma_serialize_compositeDeviceID_size_exact
  (x: compositeDeviceID_t)
: Lemma (
  length_of_opaque_serialization serialize_compositeDeviceID x ==
  length_of_asn1_primitive_TLV x.l0_version + 93 /\
  length_of_opaque_serialization serialize_compositeDeviceID_payload x <= 99
)

val serialize32_compositeDeviceID_payload_backwards
: serializer32_backwards (serialize_compositeDeviceID_payload)

val serialize32_compositeDeviceID_backwards
: serializer32_backwards (serialize_compositeDeviceID)

(* helpers *)
module B32 = FStar.Bytes
/
X509.Crypto.fst.checked X509.BasicFields.SubjectPublicKeyInfo.fsti.checked X509.Base.fst.checked prims.fst.checked LowParse.Low.Combinators.fsti.checked LowParse.Low.Base.fst.checked L0.X509.FWID.fsti.checked L0.X509.Base.fst.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.CompositeDeviceID.fsti

    version: ASN1.Base.datatype_of_asn1_type ASN1.Base.INTEGER ->
    deviceKeyPub: FStar.Bytes.lbytes32 32ul ->
    fwid: FStar.Bytes.lbytes32 32ul
  -> L0.X509.CompositeDeviceID.compositeDeviceID_t
ASN1.Base.datatype_of_asn1_type ASN1.Base.INTEGER FStar.Bytes.lbytes32 FStar.UInt32.__uint_to_t Prims.unit ASN1.Spec.Value.INTEGER.lemma_serialize_asn1_integer_TLV_size L0.X509.CompositeDeviceID.__proj__MkcompositeDeviceID_payload_t__item__l0_version L0.X509.CompositeDeviceID.lemma_serialize_compositeDeviceID_payload_size L0.X509.CompositeDeviceID.compositeDeviceID_payload_t L0.X509.CompositeDeviceID.MkcompositeDeviceID_payload_t L0.X509.FWID.lemma_serialize_fwid_size_exact L0.X509.FWID.fwid_payload_t L0.X509.FWID.x509_get_fwid X509.BasicFields.SubjectPublicKeyInfo.lemma_serialize_subjectPublicKeyInfo_size_exact X509.BasicFields.SubjectPublicKeyInfo.subjectPublicKeyInfo_t X509.BasicFields.SubjectPublicKeyInfo.x509_get_subjectPublicKeyInfo L0.X509.CompositeDeviceID.compositeDeviceID_t
let x509_get_compositeDeviceID
      (version: datatype_of_asn1_type INTEGER)
      (deviceKeyPub fwid: B32.lbytes32 32ul)
    : Tot (compositeDeviceID_t) =
  
let deviceIDPublicKeyInfo:subjectPublicKeyInfo_t = x509_get_subjectPublicKeyInfo deviceKeyPub in
lemma_serialize_subjectPublicKeyInfo_size_exact deviceIDPublicKeyInfo;
let fwid:fwid_payload_t = x509_get_fwid fwid in
lemma_serialize_fwid_size_exact fwid;
let compositeDeviceID:compositeDeviceID_payload_t =
  { l0_version = version; l0_deviceID = deviceIDPublicKeyInfo; l0_fwid = fwid }
in
lemma_serialize_compositeDeviceID_payload_size compositeDeviceID;
lemma_serialize_asn1_integer_TLV_size compositeDeviceID.l0_version;
compositeDeviceID