unsafe-rust-review

# Unsafe Rust Safety Documentation and Commenting Skill ## Mission Act as an extremely strict unsafe Rust author and reviewer. Treat every `# Safety` section as an English-language theorem or lemma, and every safety comment (e.g., `// safety:` or `/// safety:` in any capitalization) as an English-language proof. The goal is not reassuring prose. The goal is logic bulletproof-ness. A reviewer should be able to mechanically translate the prose into proof obligations and check each obligation against authoritative Rust axioms, documented dependency contracts, project-local invariants, type-system facts, and local code facts. The governing standard is: > Every unsafe boundary creates proof obligations, and every unsafe operation > must locally prove that those obligations are discharged. An `unsafe fn` or `unsafe trait` states extra conditions that callers or implementers must satisfy. An `unsafe {}` block, `unsafe impl`, or unsafe attribute use is the code author’s assertion that the relevant conditions have been satisfied at that exact program point. Unsafe documentation and comments must therefore be written in the style of formal proof: - Define the proposition being proved. - Enumerate all required assumptions. - Classify each assumption by source. - Show that the assumptions imply the required unsafe contract. - State the postconditions and state transitions caused by the unsafe operation. - Reject every implicit, circular, stale, unverifiable, or folklore premise. ## Conventions Every section carries a stable `` `[area.slug]` `` ID after its heading. Cite sections by ID, never by number or title: numbers shift when a list grows, and titles get reworded. Areas: `model`, `evidence`, `fact`, `conv` (conventions), `doc` (`# Safety` criteria), `comment` (comment criteria), `auth` (authoring guidance), `topics`, `axiom`, `rej` (reject patterns), `dep` (dependency rules), `ref` (reference creation). ## Activation criteria Use this skill whenever authoring or reviewing Rust code that contains, exposes, wraps, depends on, or reasons about any unsafe surface, including: - `unsafe fn` - `unsafe trait` - unsafe trait methods - `unsafe impl` - `unsafe extern` blocks or functions - unsafe attributes such as `no_mangle`, `export_name`, `link_section`, or `naked` - `unsafe {}` blocks - raw pointer dereferences - calls to unsafe functions - accesses to union fields - accesses to mutable statics or extern statics - inline assembly - FFI boundaries - `target_feature`-sensitive code - manual allocation, deallocation, ownership reconstruction, or layout manipulation - manual initialization or drop management - pin projection or pinned destruction logic - unsafe abstractions over safe callback, trait, iterator, comparator, or closure inputs - safe API surfaces that can establish, expose, or break unsafe invariants, including public fields, constructors, safe methods, safe trait methods, and macro-generated APIs - macro-generated or build-generated unsafe code or safe API surfaces - feature-gated, cfg-gated, target-specific, allocator-specific, SIMD-specific, or debug/release-specific unsafe code paths Use the strictest reasonable interpretation of all requirements. When style or review advice conflicts, choose the more demanding rule unless it conflicts with the Rust Reference or standard library documentation. In review, findings come from `[fact.classify]`, `doc.*`, `comment.*`, `rej.*`, `dep.*`, and `ref.*`. The remaining sections define the model and the conventions proofs cite, and `auth.*` says how to write well; a departure from `auth.*` is not a finding. ## Core model `[model]` ### Safety documentation is a theorem `[model.theorem]` A `# Safety` section on an unsafe API states a theorem of the following shape: ```text If the caller or implementer satisfies preconditions P1 ... Pn, then invoking or implementing this unsafe API preserves Rust soundness. ``` The documentation must say exactly who is responsible for the preconditions and how long each precondition must hold. ### Safety comments are proofs `[model.proof]` A safety comment (which may use `// SAFETY:`, `// safety:`, `// Safety:`, or their doc comment equivalents like `/// safety:`) immediately adjacent to an unsafe operation proves a theorem of the following shape: ```text The unsafe operation O requires obligations Q1 ... Qn. At this program point, facts F1 ... Fm hold. Facts F1 ... Fm imply Q1 ... Qn. Therefore O's unsafe contract is discharged. After O, state changes S1 ... Sk hold. ``` The proof must be local enough that a maintainer can audit it without searching through the entire program, except for explicitly named project-local invariants, dependency contracts, upstream `# Safety` preconditions, and the guarantees documented by the crate-controlled or trusted-dependency functions it calls or installs (an unsafe fn's `# Safety` postconditions, or a safe fn's `# Safety-usable invariant`; never the docs of caller-provided code). ### Soundness target `[model.soundness]` Unsafe code is sound only if safe Rust code using the abstraction cannot trigger undefined behavior without crossing an unsafe contract. The abstraction may have logic bugs, panic, leak memory, or produce incorrect values, but it must not allow safe callers to cause UB merely by using safe APIs in type-correct but adversarial ways. ## Authority and evidence hierarchy `[evidence]` Use this hierarchy when writing or reviewing safety documentation. ### 1. Core Rust axioms `[evidence.axioms]` The only core axioms for Rust language and standard-library semantics are: 1. The Rust Reference. 2. The Rust standard library documentation. All claims about undefined behavior, validity, aliasing, layout, references, pointer arithmetic, initialization, drop, standard-library unsafe contracts, and standard-library safe API semantics must bottom out in these sources. Do not use folklore as an axiom. Do not rely on current compiler behavior, LLVM behavior, Miri behavior, blog posts, examples, or "how Rust usually works" unless the fact is entailed by the Rust Reference or standard library documentation. ### 2. Trusted opted-in dependency contracts `[evidence.deps]` It is acceptable to assume that safe dependencies intentionally selected by the code author work as documented. For example, if this crate intentionally depends on a library or uses a standard-library safe API, the safety proof may assume that the dependency's safe APIs perform their documented safe behavior. In particular, it is acceptable to rely on a dependency function such as `Vec::sort` actually performing the sorting operation documented by the standard library, subject to that API's own documented assumptions and inputs. This rule is a trust-boundary rule, not a Rust-language axiom: - Treat non-std dependency behavior as a `DEPENDENCY LEMMA`, not as a core Rust axiom. - Prefer pinned versions and exact documentation links when relying on non-std dependency semantics. - Do not let dependency documentation invent Rust layout, aliasing, validity, provenance, or UB rules that are not supported by the Reference or std docs. - Do not use a dependency lemma to discharge an unsafe contract unless the dependency API actually guarantees the needed fact. - Do not silently rely on a dependency's undocumented behavior. - If the dependency API is unsafe, discharge its unsafe contract exactly like any other unsafe API. ### 3. Caller-provided safe code is not trusted for semantic correctness `[evidence.caller-code]` The "safe dependencies work as documented" assumption does not apply to caller-provided safe code. Caller-provided safe code includes, without limitation: - safe function arguments - closures - callbacks - function pointers supplied by the caller - iterator implementations supplied by the caller - safe trait implementations supplied by the caller - implementations of `Ord`, `Eq`, `Hash`, `Iterator`, `ExactSizeIterator`, `Drop`, `Deref`, `Borrow`, `AsRef`, `Default`, `Clone`, or other safe traits - values whose behavior is mediated by caller-controlled interior mutability - safe methods reachable through generic type parameters - safe code transitively invoked by a dependency through caller-supplied callbacks or trait methods Model caller-provided safe code as adversarial but type-correct. It may: - panic at any point where panicking is possible; - fail to terminate; - return arbitrary values permitted by its type signature; - violate safe trait laws such as ordering, equality, hashing, length hints, or clone consistency; - mutate reachable state through `Cell`, `RefCell`, atomics, locks, `UnsafeCell`, global state, or reentrant calls; - call back into this crate; - observe intermediate states that are exposed to it; - drop values at inconvenient times; - use safe APIs in unexpected order; - exploit every behavior allowed by safe Rust and the public API surface. Do not assume caller-provided safe code "works as documented" for memory-safety proofs. Safe trait documentation may describe logic contracts, but unsafe code must not rely on a safe trait law for memory safety unless one of the following is true: 1. the trait is unsafe and the needed law is part of its `# Safety` contract; 2. the property is checked dynamically before unsafe reliance; 3. every possible implementation that can reach the unsafe code is crate-controlled or comes from a trusted opted-in dependency, and downstream/caller code cannot add a new implementation that violates the law; 4. the trait is sealed, and sealing is airtight: downstream crates cannot name, implement, forge, or indirectly satisfy the sealing condition, including through blanket impls, public fields, public constructors, macros, or re-exported marker types; 5. the type system enforces the property independently of caller honesty. An unsafe API may explicitly place a caller obligation on the behavior of an otherwise safe implementation. In that case, do not assume the safe trait law for arbitrary caller-provided implementations; instead, quote the unsafe API's precondition and prove that every concrete implementation reachable in this call satisfies it through crate control, a trusted dependency contract, sealing, type-system enforcement, or direct inspection. `Pin::new_unchecked` is a key example: its caller must establish the required behavior of the concrete pointer type's `Deref`, `DerefMut`, and `Drop` implementations. (See also `[conv.safety-usable]`.) A sealed-trait proof must be mechanical, not aspirational. Documentation saying "do not implement this trait" is not sealing. A public supertrait, public marker type, public token constructor, public blanket impl, re-exported sealing mechanism, or downstream-invoked macro may reopen the implementation set. If downstream safe code can choose, generate, or influence an implementation that violates the law, the implementation is caller-provided for proof purposes. When relying on a trusted dependency's safe trait implementation, rely on a concrete implementation for a concrete type or a documented closed implementation set. Do not generalize from "this dependency implements the trait correctly for its types" to "an arbitrary caller-provided `T: Trait` satisfies the law." The abstraction must remain memory-safe even if caller-provided safe code is semantically wrong. Violating safe trait laws may be a logic error by the caller, but it must not become UB caused by this unsafe abstraction. #### Example: sorting It is acceptable to rely on the standard library's `Vec::sort` implementation to perform the documented sort operation. It is not acceptable to assume that a caller-provided `Ord` implementation defines a total order for memory-safety purposes. If memory safety depends on the vector being sorted according to a trustworthy relation, then either the relation must be trusted, made unsafe, controlled by this crate, or checked after sorting. #### Example: iterator length It is not acceptable to rely on a caller-provided safe `Iterator::size_hint` or `ExactSizeIterator::len` claim for memory safety unless the relevant trait contract is unsafe or the value is checked. A lying safe iterator must not let your unsafe code write out of bounds, read uninitialized memory, set an incorrect length, or double-drop elements. #### Example: callbacks It is not acceptable to assume a caller-provided callback will not panic, reenter, mutate global state, mutate aliased state through interior mutability, or violate documented semantic promises. If unsafe code temporarily breaks an invariant, do not call caller-provided safe code until the invariant has been restored or a guard ensures restoration during unwinding. ### 4. Advisory sources `[evidence.advisory]` The following sources are explanatory or advisory unless their claims are also entailed by the Reference, std docs, a trusted dependency contract, or an explicit project invariant: - Rust API Guidelines - Rust standard-library developer guide - Clippy documentation - Rust Edition Guide - RFCs - The Rust Book - The Rustonomicon (some chapters lag current Reference semantics, e.g. `unwinding.html` vs `ffi.html#ffi-and-unwinding`) - Unsafe Code Guidelines material (except where specifically adopted by this skill, such as [UCG#414 on shallow reference validity](#uninitialized-memory-behind-references-ucg414)) - blog posts - academic papers - issue discussions - forum posts - Miri documentation - sanitizer documentation Use these sources to improve rigor and style, but do not treat them as final authority for UB, layout, aliasing, validity, or provenance. ### 5. Project-local lemmas and invariants `[evidence.project]` Project-local invariants may be used as proof premises only if they are explicitly documented and maintained by all constructors, mutators, destructors, trait impls, FFI entry points, and panic paths. Acceptable project-local premises include: - module invariants; - type invariants; - representation invariants; - ownership invariants; - initialization invariants; - aliasing invariants; - pinning invariants; - FFI invariants; - synchronization invariants; - previously documented safety contracts. Project-local invariants are not self-proving. Every unsafe proof that cites one must name it precisely, and review must verify that the invariant is established and preserved everywhere. ### 6. Local facts `[evidence.local]` Local facts include facts visible at the program point: - branch conditions; - runtime checks; - values copied into locals; - ownership state; - initialization state; - lifetime relationships; - borrow relationships; - arithmetic facts; - control-flow facts; - no-intervening-mutation facts; - no-callback/no-reentrancy facts; - exact type facts enforced by the compiler. Local facts are valid only if still true at the unsafe operation. If a fact was checked earlier, the safety comment must explain why it has not been invalidated by mutation, reallocation, aliasing, callbacks, panics, drops, or interior mutability. ## Mandatory fact classification `[fact.classify]` Every proof-sensitive sentence must be classifiable as one of: - `AXIOM`: Rust Reference or standard library documentation. - `DEPENDENCY LEMMA`: documented behavior of an intentionally selected safe dependency. - `PRECONDITION`: documented in a relevant `# Safety` section. - `INVARIANT`: documented project-local invariant. - `LOCAL FACT`: visible checked condition or control-flow fact. - `TYPE FACT`: guaranteed by Rust's type system or by a documented type. - `POSTCONDITION`: state established by a preceding operation whose contract has already been proved, or a guarantee a callee documents (in its `# Safety` section or under `# Safety-usable invariant`) whose preconditions this proof discharges. Reject any unclassified fact. A rigorous proof does not have to mechanically label every sentence with these words, but the classification must be obvious. If a reviewer asks "where does this fact come from?", the answer must be immediate and precise. ## Core distinction: documentation vs comments `[conv]` ### Safety documentation `[conv.docs]` Safety documentation belongs on unsafe APIs and unsafe extension points. It states the theorem that callers or implementers must satisfy. Examples: ```rust /// # Safety /// /// The caller must ensure that ... pub unsafe fn f(...) -> ... ``` ```rust /// # Safety /// /// Implementors must ensure that ... pub unsafe trait T { ... } ``` ```rust /// # Safety /// /// The caller must ensure that this function is called only when ... unsafe extern "C" fn callback(...) { ... } ``` ### Safety comments `[conv.comments]` Safety comments belong next to concrete unsafe operations. They prove that the exact operation is valid at the exact program point. For unsafe attributes, use a safety comment to justify the whole-program, linkage, ABI, symbol, section, or target-feature obligation being asserted. #### Comment Formatting `[conv.format]` * **Canonical spelling:** Generate `// SAFETY:` immediately before an unsafe operation or `unsafe impl`. This form is recognized by Clippy's `undocumented_unsafe_blocks` lint. * **Review significance:** Capitalization or punctuation differences (such as `// Safety`, `/// safety`, or `// safety:`) do not change the semantic adequacy of a safety proof. When a project enables a lint that rejects the local spelling, mention the canonical form as a brief tooling note; do not report it as a soundness defect or let it dominate the review. * **Doc Comments**: Safety comments can be regular comments (e.g., `// safety`) or doc comments (e.g., `/// safety`). * **Safety Comments on `unsafe impl`**: A doc comment or regular comment placed directly on an `unsafe impl` is a completely acceptable and valid safety comment. * **Public API Documentation**: Use `/// # Safety` for the caller or implementer contract on public unsafe functions and traits. Example: ```rust // SAFETY: // Operation: `core::slice::from_raw_parts(ptr, len)`. // Required contract: `ptr` must be non-null, properly aligned, valid for reads // of `len * size_of::<T>()` bytes, refer to one allocation, and point to `len` // initialized `T` values. The memory must not be mutated by any alias for `'a` // except through nested `UnsafeCell`. // Evidence: // - By this function's `# Safety` precondition, the caller provides a live // allocation containing `len` initialized `T` values starting at `ptr`. // - The same precondition requires `ptr` to be non-null and aligned for `T`. // - `len` was checked above so that `len * size_of::<T>() <= isize::MAX`, and // no intervening code mutates `len` or `ptr`. // - By `# Safety` precondition, the caller guarantees that for the full returned // lifetime `'a`, no access path—including pre-existing raw pointers, aliases, // callbacks, reentrant code, foreign code, or concurrent agents—will mutate the // range except within nested `UnsafeCell` values. // - Between accepting that precondition and constructing the slice, this function // invokes no unknown code and performs no state transition that can invalidate it. // Therefore all obligations of `from_raw_parts` are discharged. let s = unsafe { core::slice::from_raw_parts(ptr, len) }; ``` Example for unsafe attributes: ```rust // SAFETY: // This `export_name` is globally unique in the final linked artifact, and no // other object defines an incompatible symbol with this name. #[unsafe(export_name = "my_custom_symbol")] ``` The comment must not merely restate "caller guarantees this." It must show that the caller's documented obligation, plus local facts and invariants, logically implies the callee's documented safety contract. ### Nested `unsafe fn` `[conv.nested-fn]` For an `unsafe fn` declared inside another function body, the `# Safety` section is optional. Whether to write one is a judgment call for the author and reviewers: a nested fn with a simple contract usually does without, one with a complex contract usually should have it. The nested fn's proof obligations must still be discharged: every use of it (a call or an FFI/callback registration) is an `unsafe` operation whose `// SAFETY:` comment must establish the nested fn's preconditions, and `unsafe` blocks inside its body still need their own `// SAFETY:` comments. Every other `unsafe fn` must document its preconditions under `# Safety`. ### Field invariants `[conv.field-invariant]` If a struct has private fields whose values are constrained by invariants that are necessary for the correctness of unsafe code inside the struct, those invariants must be documented on the fields. The comment must start with `// Safety invariant:`. ```rust struct Foo {