Idea for programmatically verifying safety comments

[joshlf]

A common problem is that safety comments can easily become stale relative to the safety preconditions of the function they decorate. Relatedly, there's no way for a reviewer to know that the correct safety preconditions are justified without looking up the function's documentation.

Ideally, a basic system would at a minimum allow safety comments to refer to conditions which constitute a conjunction (an "and"). For example, given this API:

/// # Safety
/// - Condition 1
/// - Condition 2
/// - Condition 3
unsafe fn foo(bar: Bar) { ... }

A minimum bar would be to automatically verify that a safety comment references all of the bulleted conditions. A next logical step would be to also support disjunctions ("or"s):

/// # Safety
/// - Condition 1
/// - Condition 2
/// - Condition 3: At least one of the following must hold:
///   - Condition 4
///   - Condition 5
///   - Condition 6
unsafe fn foo(bar: Bar) { ... }

Safety comments could be permitted so long as they reference Conditions 1 and 2, and also mention any of Conditions 4, 5, and 6.

Design

Here's a rough sketch of an idea for how to support conjunctions and disjunctions.

Each conjunction is encoded using a struct, and each disjunction is encoded using an enum:

struct FooPreconditions {
    condition_1: (),
    condition_2: (),
    condition_3: Condition3,
}

enum Condition3 {
    Condition4,
    Condition5,
    Condition6,
}

unsafe fn foo(bar: Bar, _safety: FooPreconditions) { ... }

At the call site, the type's shape forces the caller to mention each condition. This gives reviewers confidence that the documented conditions are the right ones, and also prevents safety comments from bitrotting since, when the type representing the preconditions changes, the calling code will stop compiling.

let safety = FooPreconditons {
    // <justification for Condition 1>
    condition_1: (),
    // <justification for Condition 2>
    condition_2: (),
    // <justification for Condition 5>
    condition_3: Condition3::Condition5,
};
// SAFETY: See preceding safety comments.
unsafe { foo(bar, safety) };

Another variant on this idea might be to provide an unsafe constructor for each safety precondition, thus requiring the _safety argument to be constructed in an unsafe block. The function itself (foo, in this case) could then be made safe.