[Pre-RFC] BTF relocations

vad:

Miri does not work for BPF targets for unrelated reasons, and for similar reasons it does not run on embedded targets either: BPF binaries can't be executed on regular operating systems; they can be executed only by virtual machines designed for the BPF ISA, including the one provided by the Linux kernel. We don't really have any solution for testing BPF binaries in Aya right now, apart from extracting testable code into crates that can be used for unit tests with std on host targets. The same approach works for Miri as well.

Apart from the Linux kernel BPF VM, there are some user-space implementations, including rBPF and Solana's SBPF, but we haven't really tried using them to run unit tests. That said, if that ever works, I guess we could look into getting Miri running on one of them as well.

But I don't think that should be a requirement for this proposal.

I didn't mean to suggest that this should actually be implemented in Miri before an RFC can be accepted, sorry if I was unclear. What I meant is that the semantics of this type need to be described at a level of abstraction and detail that it is clear how they would be implemented in Miri. This is crucial; we should not add new pieces to the language that we don't know how to describe at the level of the Abstract Machine. "It emits this kind of machine code" is not an acceptable specification for a language feature.

I am saying this with my t-opsem hat on. It is literally the responsibility of my team to ensure we have a proper Abstract Machine with an operational semantics for Rust. We're happy to help you work this out (come find us on Zulip), but an RFC without a proper opsem discussion is not going to be accepted.

vad:

The same goes for core::mem::size_of, core::mem::align_of

FWIW this will be very non-trivial because Rust has generics. Today one can write a generic function that takes an arbitrary T (implicitly: T: Sized) and then obtain its size as a compile-time constant. This is not something we can break. That's why people are saying that the Sized hierarchy work is a prerequisite for supporting this kind of a type.