Rearranging across the interface

Rearranging across the interface

The compiler doesn't prove anything for the danger cases; it relies on the human assertion that they've checked that this unsafe block is safe, given the code that they can see today.

The challenge is that we're talking about separating the unsafe block (in an inline function) from the unsafe fn it calls (in the shared object); this means that the human not only has to consider the unsafe code as it stands today, but all possible future and past variants on the unsafe code, otherwise Rust's safety promise is not upheld.

That's clearly an intractable problem; the question is about reducing it down to a tractable problem. There's three basic routes to make it tractable:

1. Ignore the problem, and rely on the humans being infallible and remembering to change a "version identifier" when making a change to both the unsafe fn and its inlined callers. This makes it far too likely that you'll breach Rust's safety promises for Rust to adopt this.
2. Ensure that there's an ABI change whenever anything in the body of the unsafe fn changes. This is problematic, because security fixes are likely to change the body, and those are the cases where you most want to be able to swap in a new shared object.
3. Build a reverse tree of inline functions in this library that call the unsafe fn, and ensure that if any of them changes, the unsafe fn's ABI changes. This means that you can change the unsafe fn freely as needed for a security fix, but if you change any inlined caller, or add a new inlined caller, you change the ABI of the unsafe fn and require a new shared object, even if this change was harmless.

There's room to be sophisticated with symbol versioning in all cases; for example, you can have a human assert that this version of the unsafe fn is compatible with the inlined callers from older versions (thus allowing a swap of a shared object), or in case 3 you can use it to allow new inlined callers to use a new shared object, while allowing the existing ones to use either old or new shared objects.

In all cases, though, the trouble is preventing the human proofs of correctness being invalidated by creating new combinations of inline functions and out-of-line unsafe code that weren't present in any source version; you want the combinations to be ones that a human has approved.