Writing correct `unsafe` Rust is difficult. Performing an "`unsafe` review" of a large corpus of `unsafe` Rust is even more difficult. Reviewing changing safety requirements across many library versions in a large codebase is so difficult and time-consuming as to be nearly infeasible.

This proposal describes tooling that would significantly reduce the burden of performing `unsafe` reviews and ensuring ongoing soundness in the presence of code and library changes.

We propose:
- adopting structured safety comments;
- using automated checks that all safety requirements are discharged when invoking `unsafe` code;
- relying on automated detection of changes to safety comments that may cause soundness hazards, and
- to maximium the extent possible, automating the safety review process for such changes.

## Demonstrating the problem by example

Safety requirements and guarantees usually come in the form of a list of properties that must be upheld or can be relied upon. ([example 1](https://doc.rust-lang.org/stable/std/ptr/index.html#safety), [example 2](https://doc.rust-lang.org/stable/std/ptr/index.html#pointer-to-reference-conversion), [example 3](https://doc.rust-lang.org/std/ptr/fn.write.html#safety), etc.)

Consider this excerpt from [the Rust standard library](https://github.com/rust-lang/rust/blob/c926476d013fbb2ca43bd5259d0a7228009a9cb2/library/core/src/str/mod.rs#L481):

impl str {
    /// Returns a mutable, unchecked subslice of `str`.
    ///
    /// This is the unchecked alternative to indexing the `str`.
    /// 
    /// # Safety
    /// 
    /// Callers of this function are responsible that these preconditions are
    /// satisfied:
    ///
    /// * The starting index must not exceed the ending index;
    /// * Indexes must be within bounds of the original slice;
    /// * Indexes must lie on UTF-8 sequence boundaries.
    pub unsafe fn get_unchecked_mut<I: SliceIndex<str>>(&mut self, i: I) -> &mut I::Output {
        // SAFETY: the caller must uphold the safety contract for `get_unchecked_mut`;
        // the slice is dereferenceable because `self` is a safe reference.
        // The returned pointer is safe because impls of `SliceIndex` have to guarantee that it is.
        unsafe { &mut *i.get_unchecked_mut(self) }
    }
}

Here, the function definition describes three safety requirements.

The use of `unsafe` in the function body then uses a safety comment to discharge the safety requirements of code it calls. The safety comment relies on both the function's own safety requirements as well as guarantees provided elsewhere ("impls of `SliceIndex`").

Currently, such safety comments are unstructured text. Performing an initial safety review then means reading large blocks of text back-and-forth across many items in the codebase, then informally convincing ourselves that "all checkboxes got checked." This process requires a reviewer skilled in `unsafe` Rust, and is tedious, time-consuming, and still error-prone.

Worse, as code changes, this code may encounter many kinds of soundness hazards. For example:
- Adding a new safety requirement to the function's list of preconditions, causing a hazard for callers that may not abide by that requirement.
- Adding a new safety requirement to the code invoked inside this function's `unsafe` block.
- Removing guarantees that underpin the soundness of the local soundness argument, such as what "impls of `SliceIndex`" must guarantee.

Currently, there's no reliable way to guarantee that such soundness hazards get reviewed appropriately! For example, say the safety guarantees of `SliceIndex` impls are relaxed — how would we find which callers' `unsafe` blocks might have become unsound as a result? This is yet more tedious and error-prone work.

## Structured safety comments

We propose minor changes to safety comments both on the item requirements and guarantees side, and on the point-of-use side.

### TL;DR

Safety comments gain numbered or bulleted lists consisting of named entries.

Each such list is preceded by an unambiguous indication of whether its entries are
- requirements (preconditions),
- guarantees (post-conditions)
- invariants (both pre- and post-conditions simultaneously), or
- dischargements of preconditions.

Entries in such lists can reference named entries defined elsewhere.

Using an `unsafe` item requires explicitly discharging each of its named requirements.

### Items' safety requirements and guarantees

Items' safety requirements and guarantees should consist of a series of named entries, each describing a single requirement or guarantee.

Then:
- Adding a new named requirement or removing a named guarantee are obvious soundness hazards analogous to a SemVer-major change. Ensuring soundness requires reviewing all uses of the changed item.
- Changes to the description of an existing named entry are also a possible soundness hazard. It's possible that the old and new descriptions are equivalent, in which case there is no need to review downstream uses.

The exact syntax is up for bike-shedding later; these examples are descriptive, not normative.

In the following example, the three requirements are named
`Relative-order`, `Within-bounds`, and `Utf8-boundaries`.

/// # Safety
/// 
/// Callers of this function are responsible for the following:
///
/// Requirements:
/// * Relative-order: The starting index must not exceed the ending index;
/// * Within-bounds: Indexes must be within bounds of the original slice;
/// * Utf8-boundaries: Indexes must lie on UTF-8 sequence boundaries.
pub unsafe fn get_unchecked_mut(...) -> _ { ... }

In the following example, `Thread-safety` is an invariant, as it is both a requirement (a pre-condition for impls) and a guarantee (a post-condition available to consumers of the trait):

/// # Safety
/// 
/// Invariants:
/// * Thread-safety: Must be safe for concurrent use by multiple threads.
pub unsafe trait Sync {}

### Discharging requirements at point of use

Safety comments that argue for the soundness of a certain use of `unsafe` should, whenever possible, refer to specific named entries of items' safety guarantees

Again, all examples are descriptive not normative; exact syntax is up for bike-shedding.

In the following example:
- <code>ref:\`SliceIndex#Validity\`</code> refers to the safety guarantee named `Validity` on the in-scope item named `SliceIndex`.
- <code>ref:\`Self::get_unchecked_mut\`</code> refers to *all* named safety guarantees on that item, as a group. The meaning of `Self` is resolved according to the usual Rust rules.

impl str {
    pub unsafe fn get_unchecked_mut<I: SliceIndex<str>>(&mut self, i: I) -> &mut I::Output {
        // SAFETY:
        // * The returned pointer is safe because impls of `SliceIndex`
        //   have to guarantee that it is (ref:`SliceIndex#Validity`).
        // * The caller must uphold the contract for (ref:`Self::get_unchecked_mut`).
        unsafe { &mut *i.get_unchecked_mut(self) }
    }
}

If the used items name a list of safety requirements, those requirements must be explicitly discharged by a matching list of safety arguments at the point of use.

In the following example, the `Sync` impl for `MyMutex<T>` is required to discharge the `Sync` trait's `Thread-safety` requirement. The act of discharging the requirement is accomplished by referring to a named guarantee elsewhere, at `MyMutex#Mutual-Exclusion`:

/// # Safety
/// 
/// Invariants:
/// * Thread-safety: Must be safe for concurrent use by multiple threads.
pub unsafe trait Sync {}

/// # Safety
/// 
/// Discharges:
/// * Sync#Thread-safety: directly from (ref:`MyMutex#Mutual-Exclusion`)
unsafe impl<T: ?Sized + Send> Sync for MyMutex<T> {}

## Automation opportunities

Transforming safety comments from raw prose to a structured format allows us to relieve much of the tedium of safety reviews, both for new unsafe code and for incremental reviews of code changes.

We'll review several scenarios and describe how automation can help.

### TL;DR

1. Failure to discharge a safety requirement when calling `unsafe` code suggests high risk of unsoundness.
2. Changes to safety rules create soundness hazards.
3. Broken references to safety rules trigger a deny-by-default lint.

All below examples are descriptive not normative, with syntax bikeshedding to follow.

### Failure to discharge a safety requirement

Our proposed automation will enforce (analogously to a deny-by-default lint) that all points of use of `unsafe` code have discharged each declared safety requirement of that code. In other words, each named requirement of the called code must have a matching discharge item for that named requirement in a safety comment in the caller.

This addresses cases like:
- any addition of a new safety requirement or invariant, and
- any removal of an existing safety guarantee or invariant.

Consider this piece of `unsafe` Rust code featuring structured safety comments:

/// Convert a pointer to a reference.
///
/// # Safety
///
/// Requirements:
/// - Aligned: `ptr` must be properly aligned for `T`.
/// - Non-null: `ptr` must not be a null pointer.
/// - Dereferenceable: A `T` at address `ptr` must lie within
///   a single memory allocation.
/// - Aliasing: Creating a reference at `ptr` must adhere to Rust's
///   aliasing rules.
unsafe fn ptr_to_ref<'a, T>(ptr: *const T) -> &'a T {
    // SAFETY:
    // Discharges:
    // - Aligned: by ref:`ptr_to_ref#Aligned`.
    // - Non-null: by ref:`ptr_to_ref#Non-null`.
    // - Dereferenceable: by ref:`ptr_to_ref#Dereferenceable`.
    // - Aliasing: by ref:`ptr_to_ref#Aliasing`.
    unsafe { &*ptr }
}

This `unsafe` Rust code snippet appears to be high quality code: it is thoroughly documented and makes a list of compelling safety arguments.

There's just one problem: **it's unsound!**

These are Rust's [requirements for safely converting a pointer to a reference](https://doc.rust-lang.org/stable/std/ptr/index.html#pointer-to-reference-conversion), with the addition of (proposed) structured names:
- Aligned: The pointer must be properly aligned.
- Non-null: It must be non-null.
- Dereferenceable: It must be “dereferenceable” as defined [here](https://doc.rust-lang.org/stable/std/ptr/index.html#safety).
- Valid: The pointer must point to a valid value of type `T`.
- Aliasing: You must enforce Rust’s aliasing rules.

The code snippet is unsound because it never discharged the `Valid` safety requirement. But that requirement was neither explicitly mentioned nor implicitly obvious at the point of use! Such problems are difficult to catch when safety comments are raw, unlinked prose.

With the proposed structured safety commments, an automated tool can observe that:
- `&*ptr` for `ptr: *const T` demands five named safety requirements.
- The safety comment surrounding that use fails to discharge the `Valid` safety requirement.
- As a result, the resulting code is at high risk of being unsound and should raise a deny-by-default lint.

### Changes to the definition of safety rules

Any change to the definition (prose contents) of any safety requirement, guarantee, or invariant may cause soundness issues. We will flag such cases for human review.

As part of the report, our automation will include all places that reference the changed safety rule: all attempts to discharge its requirement, all reliance on its guarantees, etc. This will allow the human reviewer to promptly evaluate the (un)soundness of the change within its appropriate context, and without having to manually jump back-and-forth between many different code locations.

Consider the following change to this `unsafe` Rust function:

  /// # Safety
  /// Requirements:
- /// - Valid: The pointer must have valid alignment for a `T`.
+ /// - Valid: The pointer must contain valid data that can be read as `&T`.
  pub unsafe fn use_ptr<T>(ptr: *const T) {
      ...
  }

Even though this function still names the `use_ptr#Valid` safety requirement, its definition has changed!

Callers of this function (both within this crate and in downstream use cases) might not be able to abide by the new definition — their attempts to discharge the `use_ptr#Valid` safety requirement may be unsound. This is a soundness hazard!

Our proposed tool would look up all such affected points of use (when possible, even ones in downstream crates!) and assemble a safety change report. The report will make it possible for human reviewers to decide the soundness of the change without having to manually identify affected code or jumping back-and-forth between different source code locations.

### Broken references to safety rules

Unlike safety comments in raw prose, structured safety comments make it easy to find references to non-existent safety requirements or guarantees. This is an obvious soundness hazard that our automation will treat as a deny-by-default lint.

Our tool will flag both
- attempts to rely on a named guarantee or invariant that is not provided by the specified item, and
- attempts to discharge a named requirement that is not part of the specified item.

## Conclusion

Currently, safety reviews are time-consuming and tedious to the point of being impractical.

This proposal outlines a minimally-disruptive approach to changing safety processes that allows:
- easy automatic detection of soundness hazards;
- safety reviews that are both faster *and* more thorough, and
- the ability to catch more unsoundness with less overall effort.

It can be implemented in incremental stages, such that each stage of adoption produces additional benefits.

Even partial adoption of this proposal would be a significant improvement upon the current state of unsafe reviews!

## Implementation

Everything described in this proposal is only loosely coupled to build tooling and associated infrastructure.

As a rule of thumb: if you can run `rustdoc`, you can use everything described here.

### Development stages

We expect development to proceed in stages.

Initially, the tool would do only crate-local analysis:
- Did you relax an item's safety guarantees?
- Did you tighten an item's safety requirements?
- Are local safety reference links valid? etc.

For this stage, we only require rustdoc JSON and local source code. Even though the rustdoc JSON format is unstable between Rust versions, we plan to reuse the same approach that allows cargo-semver-checks to simultaneously support many (currently, eight!) mutually-incompatible rustdoc JSON formats at once. More information on how that works is available [here](https://predr.ag/blog/semver-in-rust-tooling-breakage-and-edge-cases/#cargo-semver-checks-lints-are-database-queries-in-disguise).

In subsequent iterations, we plan to add cross-crate analysis capabilities. The key requirement there will be the ability to resolve names like `some_package::Item` down to a specific crate version, with corresponding rustdoc JSON and source code.

While that will require *some* awareness of the underlying build system, source code repositories, etc., the dependence is fairly shallow and elementary. It's unlikely this would present a major obstacle — it's just a matter of performing some competent engineering.