unsafe Blocks and the Soundness Contract

unsafe does not disable Rust's type and borrow checking. It allows expressing certain operations that the compiler cannot fully verify, while requiring the programmer to prove they adhere to a safety contract. Whether a library containing unsafe is sound depends on whether its public safe interfaces can be invoked by ordinary safe code without causing undefined behavior.

"Ordinary safe code" here also includes strange inputs, early returns, panics, mem::forget, or unexpected trait implementations. A safe interface must not secretly offload preconditions not written into the type or checks onto the caller.

Different unsafe Locations Bear Different Responsibilities

You cannot say that an unsafe block "enables the ability to implement an unsafe trait"; unsafe impl is its own syntactic location. Rust 2024 warns by default for dangerous operations inside unsafe fn that are not explicitly wrapped in an unsafe block, aiming to separate caller obligations from implementer proofs. unsafe_op_in_unsafe_fn

Ordinary reference code within unsafe is still constrained by the borrow checker; however, when artificially creating conflicting references from raw pointers, the compiler may not necessarily reject them. Therefore, "violating aliasing conditions is still an error" is different from "the compiler will definitely catch it for you."

Building a Proof Using the Logic of split_at_mut

Production code should directly use the standard library's split_at_mut. Below, we rewrite a teaching function separately to demonstrate how a safe interface converts dynamic index constraints into preconditions for unsafe operations:

pub fn split_checked<T>(slice: &mut [T], mid: usize)
    -> (&mut [T], &mut [T])
{
    let len = slice.len();
    assert!(mid <= len);
    let pointer = slice.as_mut_ptr();
    // SAFETY: The input slice guarantees that the entire memory range is valid, aligned, initialized, and exclusively borrowed.
    // mid <= len ensures the offset and length are legal; the ranges of elements in the two segments do not overlap.
    // The lifetime of the returned references is bounded by the input slice, after which the original pointer is no longer accessed.
    unsafe {
        (
            std::slice::from_raw_parts_mut(pointer, mid),
            std::slice::from_raw_parts_mut(pointer.add(mid), len - mid),
        )
    }
}

fn main() {
    let mut values = [1, 2, 3];
    let (left, right) = split_checked(&mut values, 1);
    left[0] = 10;
    right[0] = 20;
    assert_eq!(values, [10, 20, 3]);
    for mid in 0..=values.len() {
        let (left, right) = split_checked(&mut values, mid);
        assert_eq!(left.len(), mid);
        assert_eq!(left.len() + right.len(), 3);
    }
    let mut empty: [u8; 0] = [];
    let (left, right) = split_checked(&mut empty, 0);
    assert!(left.is_empty() && right.is_empty());
    let mut zst = [(); 3];
    let (left, right) = split_checked(&mut zst, 2);
    assert_eq!((left.len(), right.len()), (2, 1));
    let rejected = std::panic::catch_unwind(|| {
        let mut bytes = [1u8, 2];
        let _ = split_checked(&mut bytes, 3);
    });
    assert!(rejected.is_err());
}

assert does not guarantee everything on its own. The proof also relies on the properties of the valid input &mut [T], the source of the pointer, element initialization, and lifetimes. For any external raw pointer, even if mid <= len, this argument cannot be directly copied. from_raw_parts_mut

When mid is 0 or len, empty slices are produced, which still satisfy the interface requirements. For zero-sized type (ZST) elements, addresses might be identical; the argument should be based on element ranges and access semantics, not just claiming proof is complete because two different numeric addresses are drawn.

Mapping Proof Preconditions to Specific Code

In the tests, mid=len produces an empty right slice at the one-past-the-end position; dereferencing past the last element is not allowed; length-zero slices still need to satisfy the corresponding pointer contracts. The ZST example reminds us that we cannot replace the argument about element ranges with "pointer values are different."

Safe Functions Can Also Break unsafe Dependencies

The following function merely demonstrates the relationship between checks and dangerous operations; ordinary code should just use slice.get:

fn lookup(slice: &[u8], index: usize) -> Option<u8> {
    if index >= slice.len() { return None; }
    // SAFETY: The check above guarantees that index is strictly less than the length of this slice.
    Some(unsafe { *slice.get_unchecked(index) })
}
fn main() {
    assert_eq!(lookup(&[7, 8], 1), Some(8));
    assert_eq!(lookup(&[7, 8], 2), None);
    assert_eq!(lookup(&[], 0), None);
    assert_eq!(lookup(&[7], usize::MAX), None);
}

If index >= len is changed to index > len, the modification occurs in safe code, yet index=len will pass the check. The proof relied upon by the dangerous operation has already failed; you cannot skip review just because the unsafe block hasn't moved a single line. For persistent containers, all internal methods that modify length, capacity, and pointers fall within the same proof scope. Working with Unsafe

Where does a one-position error break the proof?

Changing the right start from mid to mid−1 makes exclusive slices share an element; changing it to mid+1 while retaining length len−mid can cross the allocation end. The input reference already establishes storage validity; these controls check only ranges, not arbitrary pointer safety.

Invariants Cross unsafe Block Boundaries

If a container internally uses len to represent the number of initialized elements, all safe methods that modify len fall within the proof scope. Resizing, insertion, cloning, destruction, and error branches must guarantee: uninitialized slots are not read or dropped as T, and the same resource is not freed twice.

When a panic occurs after partial initialization, you must also know which elements already exist and which resources need cleanup. You cannot assume Drop and interruption paths are safe just because the normal path tests pass. Conversely, safe code is allowed to leak resources; the abstraction cannot treat "the caller must run destructors" as the sole condition to avoid UB.

You Cannot Treat "Honesty" of Ordinary Traits as a Memory Safety Precondition

trait Position { fn index(&self) -> usize; }
struct Outside;
impl Position for Outside {
    fn index(&self) -> usize { usize::MAX }
}
fn selected<P: Position>(values: &[u8], position: &P) -> Option<u8> {
    let index = position.index();
    values.get(index).copied()
}
fn main() {
    assert_eq!(selected(&[1, 2], &Outside), None);
}

Position is a safe trait, and external implementations can return excessively large indices. Even if the documentation suggests returning a valid index, the safe wrapper cannot directly pass it to get_unchecked; it should check the actual return value this time. If index is called twice, with validation on the first call and access on the second, internal mutability might cause the results to differ, so you must save the value that was validated.

Similar issues appear in sorters, iterators, comparators, and callbacks. When logical contracts are violated, the library can report errors, panic, or produce logically permissible consequences, but it cannot let erroneous implementations of safe traits directly trigger UB. If a guarantee truly requires the implementer to bear memory safety responsibilities, design an explicit unsafe trait and evaluate whether this is worth adding the proof burden to the calling ecosystem.

If the Guard Is Forgotten, the Underlying Object Must Still Remain Safely Accessible

Imagine a drain guard has moved some Strings out of the container, planning to correct len in Drop. If the safe caller mem::forgets this guard, the original container will still be dropped according to the old len, potentially double-freeing the moved-out strings. Safe design must ensure that before allowing the guard to leave, the original container enters a state where UB will not occur even if the guard is never dropped; normal Drop then tries to restore the complete logical result. Destructors Leaking and Proxy Objects

This allows leaking some resources in the worst case, but does not allow use-after-free. It also illustrates that "using RAII means you don't need to think about failure paths" does not apply to custom unsafe containers: the RAII destruction path itself is one of the implementations that needs to be proven.

Separate Undefined Behavior from Ordinary Errors

Typical UB includes illegal memory access, data races, violating reference aliasing conventions, creating invalid bool/char/reference values, and calling functions with the wrong ABI. Merely creating an empty raw pointer is not UB; forming a reference that requires non-null or performing an access that does not meet conditions crosses the boundary.

Panics, deadlocks, memory leaks, and returning erroneous results are typically not UB at the language level, but may be serious business issues. Integer overflow requires judgment based on the operation and compilation settings; do not apply C's signed overflow rules to interpret all Rust operations. Rust Undefined Behavior

FFI unwinding must be distinguished by ABI: Rust panics at the ordinary C ABI boundary terminate the process, which is different from C-unwind or external exceptions that allow unwinding; they should not all be listed as the same UB item.

Answer Specific Questions When Writing Safety Comments

A useful comment should indicate who holds the current pointer, why this range is valid, whether it is initialized, whether it is exclusive or synchronized during access, and who is responsible for freeing it after the function returns. Simply writing "this is safe here" or "the compiler doesn't know" does not allow subsequent maintainers to verify.

Documentation for unsafe fn is for callers, describing how to legally invoke it; comments for unsafe blocks are for implementer reviewers, explaining why preconditions are already met here. Try to minimize the scope of dangerous operations, but do not hide the invariants truly relied upon just by minimizing line count.

Miri: Checks Executed Paths, Not Soundness Proofs

Miri interprets MIR execution and can find many out-of-bounds, use-after-free, misaligned, invalid value, and aliasing/concurrency issues. The common project workflow is to configure a nightly toolchain including the miri component and then run:

cargo +nightly miri test

This command relies on corresponding toolchain management and components; not every environment with rustc installed has this available. Miri has capability boundaries for native FFI, inline assembly, and some system interfaces; it cannot treat unexecuted external operations as verified.

Tests should cover empty inputs, boundary indices, zero-sized types, objects with Drop, and failure paths. Even if all tests pass, it only checks these executions and the current model; you still need to manually check invariants of public safe APIs and all call paths. Miri

Write Test Results as Verifiable Evidence

Do not run known UB examples and judge safety by "no crash." For rejectable inputs, assert that they are rejected before dangerous operations; for safe usages violating lifetimes, verify with compilation failure cases; for unsafe call preconditions that must be met, explicitly define boundaries with documentation and valid input tests.

When modifications come from performance optimizations, you should also record why unsafe is needed and what the standard safe interfaces lack for the target workload. If the optimization cannot demonstrate benefit, retaining the extra proof cost is usually worthless; if there is benefit, performance data cannot replace the soundness argument.