Pre-RFC: Safety Property System

libs
23

Quote my comments from #all-hands-2025 > Naming safety requirements & invariants @ :speech_balloon::

Goal for Safety Standard: Always use the same wording for the same situation.

In our proposal, each unsafe requirement is represented as a tag to clarify a safety property (SP). The definition of an SP is stored in a project configuration JSON file. The format for an SP spec includes:

  • Tag name: Must be an identifier.
  • Tag arguments: Parameters associated with the tag.
  • Tag type: One of precond, hazard, or option. Precond as default.
  • Tag description: A static string or a dynamic string interpolation related to the arguments.

This ensures that everyone understands the semantics of each SP, eliminating any potential misinterpretation of direct and indirect safety requirements for unsafe functions or calls. Tags are rendered through rustdoc from their descriptions, ensuring that safety documentation is as accurate as the spec.

Before submitting a PR or patch, our tool automatically checks that these tags are correctly defined and discharged. This strongly ensures the rigid consistency of safety properties, requirements, and documentation.

Our tool provides detailed reports on any changes to SP specifications, SP usage, or referenced entities. These reports help reviewers assess the nature of the changes and their potential impacts.

An example of the snippet from Banno's slides

/// # Safety
///
/// The provided pointer must point at a valid struct of type `Self`.
#[inline]
unsafe fn raw_get_work(ptr: *mut Self) -> *mut Work<T, ID> {
    let ptr = ptr as *mut u8;
    // SAFETY: The caller promises that the pointer is valid.
    unsafe { ptr.add(Self::OFFSET).cast() }
}

our syntax of SP usage is:

#[safety { ValidPtr(ptr) }]
unsafe fn raw_get_work(ptr: *mut Self) -> *mut Work<T, ID> {
    let ptr = ptr as *mut u8;

    #[safety { InBound, ValidNum }]
    unsafe { ptr.add(Self::OFFSET).cast() }
}

InBound and ValidNum are SPs from the safety doc of ptr.add(count), so they are just discharged on the unsafe call. These SPs can be found in primitive-sp and json data.

If entity reference is supported and preferred, we can write this:

#[safety { ValidPtr(ptr): ref(HasWorkInvariant) }]
unsafe fn raw_get_work(ptr: *mut Self) -> *mut Work<T, ID> { ... }

#[ref(HasWorkInvariant)]
pub unsafe trait HasWork<T, const ID: u64 = 0> {...}