Introduction

This book describes a mental model for unsafe in Rust.

Audience

This book might be for you if:

You want a coherent and future-proof mental model for unsafe (either to review such code or to improve its maintenance).
You don't mind a bit of type theory (also useful outside unsafe).
You prefer learning a few general concepts from which many facts can be deduced, rather than learning those many facts directly.
You just care about informal intuition rather than a formal description¹.
You prefer reading and writing Rust than English (Rust is somehow more formal than English).

Non-goals

This book does not try to:

Replace existing (and official) documentation regarding unsafe (see references).
Explain what behaviors are undefined or how to write sound unsafe code.
Introduce new unsafe constructs in Rust (only raise awareness of their absence).
Formalize unsafe and therefore Rust's type system.

Living document

This book is imperfect. Feel free to open an issue if something is unclear or wrong. You can also edit the page you are reading with the link in the top right.

Background

An early attempt of this book was made in this gist and discussed in this thread.

The appendix attempts to justify this informal intuition with a more formal description (if this is really what you want).

Quick start

This chapter provides an overview of the mental model with practical examples, to let you quickly decide if the book is for you or not. If you plan to read the book regardless, you can skip this chapter. It doesn't contain any information that is not already present in the rest of the book. However, you may come back to it later for a quick refresher.

Concepts

The mental model relies on the following concepts. You don't need to understand ~~all of them~~ any of them. They are quite complicated. But knowing they exist is already a first step. You can just read through and skip anything you don't understand on first read:

There is a notion of semantic types. A semantic type is a set of execution states.
Semantic types define a contract between parts of a program: the producers and the consumers. The contract is that, the producers must produce at most the execution states of the type, and the consumers must be able to consume at least the execution states of the type.
This notion of contract is closely related to the notion of subtyping. A semantic type is a subtype of another if its set of execution states is included in those of the other type. In particular, a contract holds if the producers are a subtype of the consumers (the actual type being a witness somewhere in between).
Variance is how functions over semantic types (a function that takes one or more semantic types and returns a semantic type) influence subtyping (or equivalently the roles of producers and consumers). Co-variance preserves subtyping from the result to the parameter. Contra-variance inverses that subtyping (producers of the result become consumers of the parameter, and symmetrically consumers of the result become producers of the parameter). In-variance ignores that subtyping and requires the parameter to be the same (producers of the result become both producers and consumers of the parameter, and similarly for consumers of the result).
Syntactical types map to semantic types (or functions over semantic types) by their safety invariant and are thus a subset of semantic types. So we'll just say types to mean semantic types and explicitly say syntactical otherwise.
Syntactical types also have a notion of validity invariant representing how they get compiled. The safety invariant is always a subtype of the validity invariant. Soundness relies on the safety invariant while compilation relies on the validity invariant.
The update type Update<P, T> updates the safety invariant of a syntactical type T with a type P. The validity invariant is preserved, thus P must be a subtype of that validity invariant. In practice, the type P is almost never syntactical and thus described in documentation.
The update type Update<P, T> is unsafe if P \ T is not empty, and it is robust if T \ P is not empty.
The update type can be lifted through syntactical types: Foo<Update<P, T>> is the same as Update<Foo, Foo<T>> by definition. The notions of unsafe types and robust types follow variance through lifting.
Functions fn(P) -> R are contra-variant in P (they consume it) and co-variant in R (they produce it).
Mutable references have actually 2 types with the same validity invariant. We write them &mut [T .. S] where T is the current type and S is the promised type at the end of the borrow. They are co-variant in T (they produce it) and contra-variant in S (they consume it).
Unsafe is when a contract does not hold: a value of type T is expected to have type S but T is not a subtype of S. In that case, a manual proof that the value is actually of type S is needed to restore soundness.

Examples

slice::get_unchecked()

/// Safety: P is the set of usize smaller than xs.len()
unsafe fn get_unchecked(xs: &[u8], i: Update<P, usize>) -> &u8;

The type Update<P, usize> contains all valid integers of type usize smaller than xs.len(). It is quite subtle, but notice how the definition of P mentions xs.len(). To be more precise, P is the set of execution states where i < xs.len(). It is attached to i because it must hold when i is passed as argument. It's a contract between the caller (producer of i) and the callee (consumer of i).

Using arithmetic, we can show that Update<P, usize> is at least missing usize::MAX from the safety invariant of usize. Because usize \ P is not empty (it contains usize::MAX), the type Update<P, usize> is a robust type.

Note that Update<P, usize> is also a subtype of the validity invariant of usize (because it's the same as its safety invariant) and thus doesn't break compilation. We won't check this in the future because it's not interesting.

Now we can lift the update type through the function type and get something like this:

/// Safety: P is the set of usize smaller than xs.len()
get_unchecked: Update<fn(xs: &[u8], i: P) -> &u8, fn(&[u8], usize) -> &u8>;

This very long type contains all valid functions of type fn(&[u8], usize) -> &u8 that only accept values i smaller than xs.len(). There are a few things to say:

It is important to filter from valid functions and not just safe functions. For usize it didn't make a difference because both the safety and validity invariants are the same type. But for functions they are actually different. The validity invariant contains many more functions. It contains all the unsafe functions in addition to the safe functions that the safety invariant contains.
While in Update<P, usize> we removed some values from the safety invariant, now we are actually adding values. This makes the type unsafe, which is why the function is annotated unsafe fn and documented with a Safety section. The fact that the update type changed from robust to unsafe is due to variance. It was in a contra-variant position.
We may wonder what those additional unsafe values are. One of them is actually the implementation of get_unchecked: a function that would do an out-of-bound access if it were provided a safe (more precisely valid) value at usize but unsafe at Update<P, usize>.

Now that we've looked at the type of get_unchecked, let's look at a call site (the function definition is not interesting).

// SAFETY: 3 is smaller than 11 which is b"hello world".len()
get_unchecked(b"hello world", unsafe { 3 })

By typing we have 3: usize and we need 3: Update<P, usize> to call the function. Because usize is not a subtype of Update<P, usize> (it's actually the contrary), this cast is unsafe and requires a manual proof. The manual proof refines the type of 3 from usize to Update<P, usize> by looking at the actual execution states and making sure they are all within Update<P, usize>. In this case, the value is always 3 and the value of b"hello world".len() is always 11, so the proof is rather simple.

Note that in practice, update types are usually lifted to function types. We could think that instead of casting 3 we could cast get_unchecked like that:

// SAFETY: 3 is smaller than 11 which is b"hello world".len()
unsafe { get_unchecked }(b"hello world", 3)

But we cannot cast get_unchecked back to fn(&[u8], usize) -> &u8 because get_unchecked is actually not a member of that type. The only solution is to attach the proof to the call-site itself where the arguments are accessible.

// SAFETY: 3 is smaller than 11 which is b"hello world".len()
unsafe { get_unchecked(b"hello world", 3) }

Box::into_raw()

/// Robustness: P is the set of non-null pointers
robust fn into_raw<T>(b: Box<T>) -> Update<P, *mut T>;

The type Update<P, *mut T> contains all valid (in the sense of the validity invariant, not in the sense of valid for read or write) pointers of type *mut T that are non-null. By definition, this type is missing null_mut() from the safety invariant of *mut T. It is thus a robust type.

We can lift the update type through the function type and get:

/// Robustness: P is the set of non-null pointers
into_raw: for<T> Update<fn(Box<T>) -> P, fn(Box<T>) -> *mut T>;

This type is missing some functions that are safe at for<T> fn(Box<T>) -> *mut T, in particular those that return a null pointer. So this type is also robust. This is why the function is annotated robust fn and documented with a Robustness section. The fact that lifting the update type preserved its robustness, is due to variance. It was in a co-variant position.

Let's look at the function definition first (and call-sites later).

/// Robustness: P is the set of non-null pointers
robust fn into_raw<T>(b: Box<T>) -> Update<P, *mut T> {
    let result: *mut T = [...];
    // SAFETY: The box pointer is non-null by invariant of Box.
    result
}

By typing we have result: *mut T and we need result: Update<P, *mut T> to return from the function. Because *mut T is not a subtype of Update<P, *mut T> (it's actually the contrary), this cast is unsafe and requires a manual proof. The manual proof refines the type of result from *mut T to Update<P, *mut T> by looking at the actual execution states and making sure they are all within Update<P, *mut T>. In this case, Box<T> has an internal invariant that the pointer is non-null, so the proof simply states this invariant.

Let's now look at a call-site.

let p: *mut T = Box::into_raw(b);
// SAFETY: The pointer was not modified since it was returned by Box::into_raw
// which ensures it is non-null by robustness. So it is still non-null.
unsafe { NonNull::new_unchecked(p) }

First, values may be implicitly cast by subtyping. This is what happens between the result of Box::into_raw(b) of type Update<P, *mut T> and the binding type of p which is *mut T, because Update<P, *mut T> is a subtype of *mut T. In particular, Update<P, *mut T> is not an unsafe type, it is only a robust type. And update types that are not unsafe can safely cast to the type they update (without an unsafe block and a safety comment).

The more interesting fact is how we can transfer the information about execution states after Box::into_raw() returns to the unsafe cast even though we lost the type information. We need to verify that all execution operations since the last known states produce execution states that match the contract we need to prove. This is trivially the case here because the result value is not modified.

In practice, the robustness of Box::into_raw() is much more precise than just returning a non-null pointer.

/// Robustness: Q is the set of non-aliased, aligned, allocated, and valid pointers
robust fn into_raw<T, P>(b: Box<Update<P, T>>) -> Update<Q, *mut Update<P, T>>;

The function is actually polymorphic over the type within the Box, which means it doesn't temper its content and simply returns the underlying pointer (theorem for free). This correctness property is not part of the safe type for<T> fn(Box<T>) -> *mut T, the function could just return any pointer (including a null pointer). But updating the parameter and return types we can more precisely capture the behavior of the function, which matters when proving unsafe code because of the stronger contract.

The type Q is actually a filter over *mut Update<P, T> and thus more precisely a function over types Q(P) parametric over P. So the result type is actually Update<Q(P), *mut T> (the type being updated doesn't matter, only its validity invariant does).

Functions in the standard library may usually be assumed to have such strong robustness guarantees, in contrary to other libraries for which correctness may not usually be assumed to hold when proving unsafe code.

String::as_mut_vec()

/// Safety: P is the set of safe Vec<u8> that are UTF-8
unsafe fn as_mut_vec(self: &mut String) -> &mut [Vec<u8> .. Update<P, Vec<u8>>];

The type Update<P, Vec<u8>> contains all valid values of type Vec<u8> that are safe and UTF-8. It is a robust type because it is missing values that are safe (those that are not UTF-8) and does not contain unsafe values.

We can lift the update type through the mutable reference and get:

/// Safety: P is the set of safe Vec<u8> that are UTF-8
unsafe fn as_mut_vec(self: &mut String) -> Update<&mut [Vec<u8> .. P], &mut Vec<u8>>;

We get a similar reasoning as with slice::get_unchecked() because we have a robust type in a contra-variant position. The update type contains all valid values of type &mut Vec<u8> that promise UTF-8 at the end of the borrow. So compared to the safe values of type &mut Vec<u8>, the update type contains additional values (thus unsafe at &mut Vec<u8>). This makes the update type unsafe.

We can finally lift the update type through the function type and get:

/// Safety: P is the set of Vec<u8> that are UTF-8
Update<fn(&mut String) -> &mut [Vec<u8> .. P], fn(&mut String) -> &mut Vec<u8>>

This type also has additional values compared to fn(&mut String) -> &mut Vec<u8> and is thus unsafe. This is because the result type of a function is in a co-variant position, and the result was unsafe. The function type being thus unsafe, it has a Safety section and is annotated unsafe fn.

Let's look at a call site.

/// SAFETY: At the end of the borrow, the message is ASCII, thus UTF-8.
for byte in unsafe { message.as_mut_vec() } {
    *byte &= 0x7f;
}

By typing we have message.as_mut_vec() of type &mut [Vec<u8> .. Update<P, Vec<u8>>] and we need &mut Vec<u8>, i.e. &mut [Vec<u8> .. Vec<u8>]. Because this does not hold by subtyping (the promised type is robust, making the mutable reference unsafe), we need a manual proof. We must refine the promised type from Vec<u8> to Update<P, Vec<u8>> by contra-variance of the promised type, i.e. we must prove that the promised type is UTF-8. Because we convert all bytes to ASCII before the borrow ends, and don't modify the message further, we can claim that the message at the end of the borrow is ASCII and thus UTF-8.

In practice, String::as_mut_vec() is also robust:

/// Safety and Robustness: P is the set of safe Vec<u8> that are UTF-8
robust unsafe fn as_mut_vec(self: &mut String) -> &mut Update<P, Vec<u8>>;

This function is both robust and unsafe. It is unsafe for the same reason as above (the type is robust at the end of the borrow) and it is robust because the returned type is robust at the beginning of the borrow. By being robust, this function type provides more freedom to call-sites. The following call-site would be unsound with the non-robust function type, but is sound with the robust function type.

/// SAFETY: Assuming the message is UTF-8 at the beginning of the borrow, it is still
/// UTF-8 at the end of the borrow.
for bytes in unsafe { message.as_mut_vec() }.chunks_exact_mut(2) {
    // Convert code points encoded with 2 bytes at even offsets to ASCII.
    if bytes[0] & 0xe0 == 0xc0 {
        bytes[0] &= 0x3f;
        bytes[1] &= 0x7f;
    }
}

To go even further, because String::as_mut_vec() is part of the standard library, it is even more robust than the previous function type. It is actually polymorphic over the type of self (which contains 2 types because it's a mutable reference):

/// Safety and Robustness: P and Q are sets of valid values of Vec<u8>
robust unsafe fn as_mut_vec<P, Q>(
    self: Update<&mut [P .. Q], &mut String>
) -> Update<&mut [P .. Q], &mut Vec<u8>>;

The most common case is when the parameter is safe. This means both P and Q are the safety invariant of String, i.e. the set of UTF-8 values. But it is possible to also use unsafe or robust types (with respect to String) for P and Q independently of each other. An artificial example could look like this:

/// Sanitizes a string to make it UTF-8.
///
/// # Robustness
///
/// The message doesn't need to be UTF-8.
robust fn sanitize(message: &mut [Update<Vec<u8>, String> .. String]) {
    // SAFETY: The message is ASCII at the end of the borrow.
    for byte in unsafe { message.as_mut_vec::<Vec<u8>, ASCII>() } {
        *byte &= 0x7f;
    }
    // SAFETY(parameter): The message is ASCII at the beginning of the borrow.
    // SAFETY(result): The message remains ASCII and is thus UTF-8 at the end of the
    // borrow.
    for byte in unsafe { message.as_mut_vec::<ASCII, String>() } {
        *byte ^= 0x07;
    }
}

We already discussed the first transformation, so let's focus on the second one. By typing we have message of type &mut String and message.as_mut_vec() of type Update<&mut [ASCII .. String], &mut Vec<u8>>. We need message to have type Update<&mut [ASCII .. String], &mut String> and message.as_mut_vec() to have type &mut Vec<u8>. Both casts are unsafe because they don't hold by subtyping. The first one doesn't hold because we have to prove that message is initially ASCII, which we know by preceding code. The second one doesn't hold because we have to prove that message.as_mut_vec() is UTF-8 at the end of the borrow, which we do by using the robustness that it is initially ASCII and preserving this property to the end of the borrow.

What are types?

This chapter is an informal (and possibly opinionated) overview of type systems. It is necessary to understand this chapter to understand the mental model, because according to the mental model:

Unsafe is a way to escape the type system.

Programming languages

Programming languages usually provide the following components (there may be variations):

A syntax to write programs, usually some grammar.
The meaning of programs, usually some operational semantics (how programs execute).

The most common and practical meaning of programs is their execution output (effects and/or values), which is usually why programs are written and executed. However, for most realistic programming languages, not all programs have a meaning. In particular, program execution is not always defined (think undefined behavior). This is the reason why type systems exist.

Type systems

Type systems try to decide whether programs are defined¹ in a mechanized way. They tell whether a program is defined without human interaction, but they may need non-interactive human assistance in the form of program annotations (see next section).

Type systems come with a proof of soundness: if the type system says a program is defined then the program is defined. However, this classification is an undecidable problem for non-trivial languages, which is why type systems may classify a program as possibly undefined although it is actually defined. This is the reason why unsafe exists.

Unsafe is a way to make the type system agree that a program is defined. This argumentation is done informally by a human, and is thus not mechanized. This suddenly introduces the notion of human errors. The usage of unsafe may thus break the soundness property of the type system. This is why soundness must be preserved when using unsafe.

Types

Most type systems follow the same techniques. They introduce a notion of types to classify programs. Types are an additional syntax (with its own grammar) to annotate programs and their parts (like expressions, variables, statements, functions, etc). The type system provides rules on how those types combine and interact based on the program structure.

It is natural to interpret types as sets of values (or more generally mathematical objects describing the possible runtime states at a given point in the execution of the program they are annotating), called their type interpretation and written |T|. For example, the interpretation |i32| of i32 could be all the 32-bits integers, and |*const i32| could be all the pointer-wide integers with an optional provenance. This interpretation may depend on the execution environment, like the memory.

Types can also be seen as a form of contract between different parts of the program. This is how, when all the contracts in a program are satisfied, it is possible to say something about the program's behavior. In particular, when the output of one part of a program is the input of another part of the program, the type (or contract) at this junction specifies which values are permitted. The output program promises to not output values outside the contract, and the input program promises to accept all values inside the contract.

Subtyping

Interpreting types as sets of values naturally generates a notion of subtyping through set inclusion. A type A is a subtype of B, which we'll write A <: B, if |A| is included in |B|. For example, all values of type &'static i32 are also values of type &'a i32 so &'static i32 is a subtype of &'a i32.

This notion of subtyping can be used to plug parts of a program together even when they don't have the same contract. For example, an expression of type T can be used where an expression of type S is expected as long as T is a subtype of S. Because subtyping is a reflexive and transitive relation, we can always require contracts to match exactly and let the programmer explicitly use subtyping to change one or the other to make them match.

Variance

The notions of subtyping and type-level functions naturally generate a notion of variance defining how Foo<A> and Foo relate when A is a subtype of B:

If Foo<T> is co-variant in T then Foo<A> is a subtype of Foo.
If Foo<T> is contra-variant in T then Foo is a subtype of Foo<A>.
If Foo<T> is invariant in T then there's no particular relation between Foo<A> and Foo.

A well-known example of variance is the function type fn(P) -> R. It is contra-variant in P and co-variant in R. You can call a function with an argument of type Q as long as Q <: P, and you can use its result where an expression of type S is expected as long as R <: S. Equivalently, we have fn(P) -> R <: fn(Q) -> S thus the function also has the type fn(Q) -> S.

A less-known (and possibly controversial) example is the mutable reference type &mut T. It is usually assumed to be invariant in T. In reality, there are 2 separate occurrences of T in &mut T, one of them being co-variant and the other contra-variant. This is discussed in the next chapter.

Type systems may also be used to decide other properties (like termination) or to generate parts of the program. Those alternative roles are not relevant for unsafe and will be ignored.

Mutable references

The mutable reference type in the mental model is written &mut [T .. S]. It means that you have a pointer with (temporary) exclusive access to a value of type T, and that you promise that the value will be of type S when the borrow ends. The syntax [T .. S] represents the type of the value going from T to S over the lifetime of the borrow. We'll call T the type of the mutable reference and S the promised type of the mutable reference.

Another way to look at this, is that a mutable reference is made of 2 things:

A pointer to a temporarily owned value of type T.
A function taking the same pointer but with type S. This function is automatically called when the borrow ends to return the ownership of the value to the lender.

Yet another way to look at this, is that mutable references are like reversed functions:

Functions fn(P) -> R ask for a value of type P then give back a value of type R.
Mutable references &mut [T .. S] give a value of type T then ask it back at type S.

Variance

The mutable reference type &mut [T .. S] is co-variant in T and contra-variant in S. When enforcing T and S to be syntactically equal, like this is done with the &mut T notation, the type naturally becomes invariant in T. Being able to dissociate T and S is important to understand unsafe, and mutable references in the mental model will explicitly dissociate those 2 types by using the &mut [T .. S] notation.

Borrowing

When lending a place of type T, the lender may choose the type S, that the place should have when returned by the borrower. For example, if a lender has a place x of type T and creates &mut x for a borrower, they may ask the borrower to return the place with type S, at which point the lender would get back ownership of x but with type S instead of T.

Re-borrowing is a particular case of borrowing where the initial place is already borrowed. For example, if the lender (itself a borrower) has a place x of type &mut [T .. S], they may create &mut *x of type &mut [T .. Q]. The borrower would need to return the place with type Q, thus letting the lender have the place at type &mut [Q .. S] instead of &mut [T .. S]. In particular, re-borrowing doesn't affect the final contract with the original lender, who is still expecting the place to be at type S.

What is unsafe?

This chapter provides the mental model of unsafe, relying on the concepts of the previous chapters.

Anonymous types

Unsafe is a way to locally introduce an anonymous type given its interpretation. In practice, this is done by reusing the interpretation of an existing type and documenting how that interpretation is modified. For example, an occurrence of *const i32 in the program could be documented as being restricted to values that are valid for read, aligned, and pointing to an initialized i32. That particular occurrence of *const i32 would actually be an anonymous type created for the occasion with the documented interpretation, essentially updating the contract at that location.

Proofs

Recall how using an expression of type A where a value of type B is expected requires to show that A is a subtype of B. When using unsafe, it may happen that this is not the case. This usually happens when B is an anonymous type over A, like the *const i32 example above. In those cases, one has to manually prove that the possible values of the expression are actually in B. This proof cannot rely on types and must rely on the correctness of the program.

Validity

Rust has an unusual concept compared to other type systems. It has an additional notion of type interpretation. Besides the usual interpretation of types which defines the set of safe values (as defined by the safety invariant of the type), there is an interpretation of types which defines the set of valid values (as defined by the validity invariant of the type). The compiler doesn't know that only safe values are possible, it believes that unsafe values (values that are valid but not safe) are also possible, and will not optimize if an unsafe value would invalidate the optimization.

This notion is actually necessary due to type composition: an anonymous type in a contra-variant position would actually increase the set of possible values. The validity invariant must at least contain the interpretation of the type where all types in contra-variant positions have been replaced by the bottom type (the type with an empty interpretation).

Properties

Unsafe may only update interpretations within the bounds of the validity invariant. In particular, it may add unsafe values and it may remove safe values, but it may not do anything else. An unsafe type contains at least one unsafe value and a robust type is missing at least one safe value. By those definitions, a safe type is neither unsafe nor robust, its interpretation is exactly the safe values. Only anonymous types may be unsafe and/or robust. In particular, an anonymous type may be both unsafe and robust.

An unsafe type is a type that has restrictions to use, because one needs to take care of those additional values. A robust type on the contrary is a type that provides permissions to use, because some safe but otherwise problematic values are now absent.

Let's illustrate this with the function type fn(P) -> R. By contra-variance, it is unsafe if P is robust. This is the most common case, because P has permissions to use that its safe version would otherwise not have. And by co-variance, it is unsafe if R is unsafe. This is less common, but happens when R has restrictions to use, like Pin::get_unchecked_mut() -> &mut T.

Similarly for the mutable reference type &mut [T .. S]. By contra-variance, it is unsafe if S is robust. This is the case with the result type of String::as_mut_vec() -> &mut Vec<u8> that requires permissions to use S as UTF-8 (removing the safe values of Vec<u8> that are not UTF-8). By co-variance, it is unsafe if T is unsafe. This is the case with the result type of Pin::get_unchecked_mut() -> &mut T that enforces restrictions to use T as possibly pinned (adding the unsafe values that are safe when under Pin). Note that S also has restrictions to use (the same ones as T), thus by contra-variance making the result type and thus the type of Pin::get_unchecked_mut() robust (remember that types may be both unsafe and robust).

Custom types

It is interesting to observe that for builtin types, the origin of unsafe seems to always be a robust type in contra-variant position. We could thus think that it would be enough to only update types down from the safety invariant instead of the validity invariant. But keeping the option to add unsafe values to a type is necessary for custom types and reverting the effect of an anonymous type.

A custom type gives a name to a type expression, its definition. When the custom type is used instead of its definition, anonymous types can only be introduced directly on the custom type because the definition is hidden. If one wanted to make the type unsafe by making a contra-variant type robust within the definition, now one needs to make the custom type unsafe by adding unsafe values.

Let's use the function type fn(*const i32) as initial illustration. If we define a custom type Foo with that function type as definition and we want a specific usage of Foo to actually contain unsafe functions, we can't introduce an anonymous type on *const i32 because it's hidden behind the definition of Foo. We have to introduce the anonymous type on Foo, which is the only thing visible, and add those unsafe values.

It is also possible for a custom type definition to have an anonymous type. This is for example the case of Vec<i32>. Its simplified definition is an anonymous type on { ptr: *mut i32, len: usize, cap: usize } removing some safe values. We'll focus on the safe values where not all of the first len elements pointed by ptr are initialized. The safety invariant of Vec<i32> thus doesn't contain those (otherwise safe) values, making a pointer to uninitialized data with non-zero length an unsafe value for that type. One may want to add those unsafe values for some specific occurrences of Vec<i32>, requiring again an anonymous type. This time it's not only because the definition is hidden, but also because we want to revert the effect of an anonymous type adding back values that were removed.

Note that, while anonymous types in custom types define a new safety invariant, it is also possible to define custom types with a different validity invariant using rustc annotations. For example, NonZeroI32 has the value zero removed from both the safety invariant and the validity invariant. This type doesn't have any unsafe value. It is thus not possible to create an unsafe version of that type. If you would remove the rustc annotations and keep the anonymous type, then zero would not be safe but still be valid, and thus it would be an unsafe value that can be added to create an unsafe version of that type.

Making it explicit

This last chapter gives an explicit syntax to the mental model. This may help understand it better, but most importantly it facilitates clear discussion about what is actually going on in a program.

Note that we are not actually introducing this syntax to Rust. This is a mental model. We are just making it explicit in our collective mind.

The update type

The Update type makes anonymous types explicit, including their predicate and proof.

/// Creates an anonymous type from a source type.
///
/// The created anonymous type (more precisely its interpretation) is the set of
/// valid values of the source type (its validity invariant) satisfying a
/// predicate.
///
/// The predicate is usually left implicit and defined in some documentation,
/// thus writing `Update<Source>`.
#[repr(transparent)]
pub struct Update<Predicate, Source: ?Sized> {
    /// A proof that the value satisfies the predicate.
    ///
    /// The proof is usually left implicit and defined in some comment, thus
    /// writing `Update { value }`. We may also abusively write `Update(value)`
    /// instead.
    pub proof: Predicate,

    /// The value whose type is being updated.
    ///
    /// It is a valid value of the source type that satisfies the predicate.
    pub value: Source,
}

The predicate should be documented in 2 different sections depending on the variance in which the source type is occurring within the type of the item where the documentation is attached. If the predicate makes the item type unsafe, then it should be documented in a # Safety section. If it makes the item type robust, then it should be documented in a # Robustness section. It is recommended to avoid making item types robust (and thus avoid robustness sections) until an unsafe block somewhere depends on this property, to avoid unnecessary work by unsafe reviewers.

The proof should be written in a // SAFETY: comment.

The proof type

A weird but useful special case of the update type is when applied to the unit type. In that case, the only possible interpretations are the empty set or the singleton set, thus the only information of this type is whether it is inhabited, which is defined by whether the predicate holds. This type is really only useful when the predicate depends on the execution environment (the memory, the stack, the global variables, etc). It can be used to gate parts of the program that must only execute if a predicate holds, by taking a value of that type.

/// The proof that a predicate holds.
pub type Proof<Predicate> = Update<Predicate, ()>;

Examples

Safety documentation

The most common examples of safety documentation are parameters of unsafe functions. The parameters are robust making the function unsafe due to contra-variance. And they are robust because they have less safe values, thus providing permissions to use.

/// Reads the value from a pointer without moving it.
///
/// # Safety
///
/// The pointer must be valid for reads, aligned, and pointing to a safe value.
pub fn read<T>(ptr: Update<*const T>) -> T;

Less common examples are results of unsafe functions. The results are unsafe making the function unsafe due to co-variance. And they are unsafe because they have unsafe values, thus enforcing restrictions to use.

/// Gets a mutable reference to the pinned data.
///
/// # Safety
///
/// The data in the result must not be moved.
pub fn get_unchecked_mut<T>(pin: Pin<&mut T>) -> Update<&mut T>

Robustness documentation

The most common examples of robustness documentation are results of functions. The results are robust making the function robust due to co-variance. And they are robust because they have less safe values, thus providing permissions to use.

/// Consumes a box returning its raw pointer.
///
/// # Robustness
///
/// The pointer will be properly aligned and non-null.
pub fn into_raw(b: Box<T>) -> Update<*mut T>

Less common examples are parameters of functions. The parameters are unsafe making the function robust due to contra-variance. And they are unsafe because they have unsafe values, thus enforcing restrictions to use.

/// Prints a message to the standard output.
///
/// # Robustness
///
/// The message doesn't need to be valid UTF-8.
pub fn robust_print(msg: Update<&str>);

Even though documenting robustness makes the API more precise, it has the downside of increasing the burden of unsafe reviews. A function for which correctness would otherwise not impact unsafe code, now has the potential of impacting unsafe code and must be reviewed appropriately. If this potential is not actually used, then this review is unnecessary.

That said, the standard library can be assumed to be maximally robust (correctness defines robustness). If the standard library is incorrect, then we have other problems that are as big as unsoundness of third-party crates (that would be sound if the standard library was correct).

Safety comments

Safety comments can both produce and use proofs from the update type.

/// Consumes a box returning its non-null pointer.
pub fn into_non_null(b: Box<T>) -> NonNull<T> {
    let Update(ptr) = Box::into_raw(b);
    // SAFETY: The pointer is non-null because Box::into_raw() returns a proof
    // that it's non-null and properly aligned.
    NonNull::new_unchecked(Update(ptr.value))
}

Custom types

Notice how in the previous section, into_non_null() replaces the robustness of into_raw() with the safety invariant of NonNull, essentially giving a name to its anonymous result type. This is done by having NonNull<T> be a custom type around Update<*mut T>. We'll ignore alignment and variance for simplicity. We'll also ignore the rustc annotations that shrink the validity invariant.

/// A non-null pointer.
#[repr(transparent)]
pub struct NonNull<T: ?Sized> {
    /// The wrapped pointer.
    ///
    /// # Robustness
    ///
    /// The pointer is non-null.
    ptr: Update<*mut T>,
}

Making a type robust is the most common reason to create custom types, but they can also be used to make a type unsafe.

/// A pinned pointer.
#[repr(transparent)]
pub struct Pin<P> {
    /// The wrapped pointer.
    ///
    /// # Safety
    ///
    /// The pointer cannot be moved unless it implements `Unpin`.
    ptr: Update<P>,
}

Unsafe blocks

Rust provides the following unsafe superpowers:

Dereference a raw pointer
Call an unsafe function or method
Access or modify a mutable static variable
Implement an unsafe trait
Access fields of unions

Most of them require an unsafe block. When translating an unsafe block to the mental model, the use of the unsafe superpowers are made explict, preserving the safety comment if any.

Dereference a raw pointer

Dereferencing a raw pointer can be seen as an operation that takes a value of some robust pointer type and returns a place. The exact predicate of that robust type is not part of the mental model, only making the operation take Update<*const T> or Update<*mut T> is.

// SAFETY: The pointer is valid, aligned, and points to a safe value.
unsafe { *ptr }

would translate to:

// SAFETY: The pointer is valid, aligned, and points to a safe value.
*Update(ptr)

or more pedantically:

let proof = "The pointer is valid, aligned, and points to a safe value.";
*Update { proof, value: ptr }

Call an unsafe function or method

Calling an unsafe function or method is the same as calling a regular function or method, except that the parameters using the update type (here Update<*const T>) must be adapted.

// SAFETY: <justification for add>. <justification for read>.
unsafe { ptr.add(start).read() }

would translate to:

// SAFETY: <justification for add>. <justification for read>.
Update(Update(ptr).add(start)).read()

Note how the location of the usage of both unsafe superpowers had to be made explicit. In particular, the pedantic version could use 2 distinct proofs:

let proof = "justification for add";
let ptr = Update { proof, value: ptr }.add(start);
let proof = "justification for read";
Update { proof, value: ptr }.read()

Access or modify a mutable static variable

Accessing or modifying a mutable static variable can be seen as an operation that takes a mutable static variable with a proof and returns a place. The proof states that the mutable variable is not aliased while the place is alive.

static mut COUNTER: u32 = 0;
// SAFETY: <justification>.
unsafe { COUNTER += 1 };

would translate to:

static mut COUNTER: u32 = 0;
// SAFETY: <justification>.
access_static_mut!(COUNTER, Update(())) += 1;

We have to use a macro because we need to pass the mutable static as a name without accessing it.

Implement an unsafe trait

This doesn't require an unsafe block and will be treated in its own chapter.

Access fields of unions

Accessing a field of a union can be seen as an operation that takes a place to the union, the field to access, and a proof, and returns the place of the field. The proof states that accessing that field of that union for that lifetime is valid.

// SAFETY: <justification>.
unsafe { u.f1 }

would translate to:

// SAFETY: <justification>.
access_union_field!(u, f1, Update(()))

Similarly for mutable static variables, we also need a macro because we need to pass the union as a place and its field as a name.

Unsafe functions

A function (or method) type is unsafe when its interpretation may contain an unsafe value. This is usually either because it takes a robust type or returns an unsafe type. In those cases, the appropriate parameter or result type is wrapped under the update type with its predicate defined in the safety section of the function documentation.

unsafe fn read<T>(p: *const T) -> T;
unsafe fn get_unchecked_mut<T>(pin: Pin<&mut T>) -> &mut T

would translate to (preserving any safety documentation):

fn read<T>(ptr: Update<*const T>) -> T;
fn get_unchecked_mut<T>(pin: Pin<&mut T>) -> Update<&mut T>

It is also possible that the predicate isn't about a single type, in which case it may be more elegant to use the proof type:

unsafe fn unchecked_add(x: i32, y: i32) -> i32;

would translate to (preserving any safety documentation):

fn unchecked_add(x: i32, y: i32, p: Proof) -> i32;

This is a function type translation, so it applies to all unsafe function types (i.e. within function declarations, function definitions, function pointers, and so even when nested within another type like Vec<unsafe fn()>).

Unsafe traits

A trait can be unsafe for different reasons:

One of its associated type (including inherited) or the implemented type itself must satisfy a predicate.
One of its method type (including inherited) is robust.
One of its associated constant type (including inherited) is robust.

Those are documented in the safety section of the trait documentation.

An unsafe trait is translated by adding an associated constant of the proof type, which we'll call an associated proof. The predicate of the proof type is defined in the safety section and describes why the trait is unsafe.

unsafe trait Send {}

would translate to (preserving any safety documentation):

trait Send {
    const P: Proof;
}

Unsafe implementations

An unsafe implementation is translated by implementing the associated proof.

// SAFETY: <justification>.
unsafe impl Send for Mutex {}

would translate to:

impl Send for Mutex {
    // SAFETY: <justification>.
    const P: Proof = Update(());
}

Navigating Pin

This chapter is not about an unsafe construct, but about the Pin type of the standard library. This type can be quite subtle, and this chapter may get some stuff wrong¹. But because it is strongly related to unsafe, it is a good candidate to demonstrate the mental model on a practical example.

What is Pin?

The author believes that Pin is just a set of guidelines to design a pinned typestate. The type itself doesn't need to be used. One could implement their own typestates PinFooRef, PinFooMut, and PinFooBox without using Pin. However using the Pin type directly reduces the cognitive load for users of the API, as they can reuse their knowledge about Pin instead of learning something new.

The type Pin<T> is a name for Update<P, T> where P describes what pinned values of type T are. In particular, P is specific to T. Different types T will have different predicates P to describe their pinned values.

/// Updates the safety invariant of T to contain pinned values.
pub type Pin<T> = Update<"Pinned values of type T", T>;

It is natural to wonder whether T <: P must hold². The author believes that it is not necessary but convenient to have and thus recommended when possible.

An important aspect of Pin is that it is not possible to safely access T from Pin<T> since they have different safety invariant. However it is possible to go in both directions with unsafe functions:

pub unsafe fn new_unchecked<T>(T) -> Pin<T>;
pub unsafe fn get_unchecked_mut<T>(Pin<&mut T>) -> &mut T;

When we look at both of those functions in the mental model (writing P for the predicate of a pinned T), we realize that they are just identity functions. They simply wrap or unwrap the definition of Pin.

pub unsafe fn new_unchecked<T>(Update<P, T>) -> Pin<T>;
pub unsafe fn get_unchecked_mut<T>(Pin<&mut T>) -> Update<P, &mut T>;

There are however many subtleties behind those 2 functions. Let's look at them in more details.

Wrapping Pin

Let's look at mutable references only, because that's the most complex case.

pub unsafe fn new_unchecked<T>(&mut T) -> Pin<&mut T>;

In the mental model, this function is actually polymorphic over both types of the mutable reference.

pub unsafe fn new_unchecked<T, S>(&mut [T .. S]) -> Pin<&mut [T .. S]>;

Because we know both types must have the same validity invariant, let's write Q and R predicates over the validity invariant of T. The type now becomes:

(&mut [Update<Q, T> .. Update<R, T>]) -> Pin<&mut [Update<Q, T> .. Update<R, T>]>
//     ^--- A  ---^    ^--- B  ---^                ^---  C ---^    ^---  D ---^

We'll use the notation in the comment above (A, B, C, and D) to talk about the different values at the given types. We'll also focus only on 2 predicates: T the safety invariant of T, and P the safety invariant of T in the pinned typestate.

`Q`	`R`	`A <: Q`	`R <: B`	`Q <: C`	`D <: R`
`T`	`T`	`T == T`	`T == T`	`T <: P`	`P <: T`
`T`	`P`	`T == T`	`P <: T`	`T <: P`	`P == P`
`P`	`T`	`T <: P`	`T == T`	`P == P`	`P <: T`
`P`	`P`	`T <: P`	`P <: T`	`P == P`	`P == P`

If T <: P then there is nothing to prove for those cells (and that's actually why the function is robust). However, P <: T usually does not hold and needs a proof. For each row, this cell is why the function is unsafe. We can see that the problem is always the promised type of the mutable references (B and D), i.e. what happens at the end of the borrow, because this will inject a value that is safe at P into a value that is safe at T, hence the P <: T constraint.

There are essentially 2 reasons (assuming T <: P) why the function can be unsafe:

The promised type R of the mutable reference is T, in which case the result of the function is unsafe because its promised type D is robust. One must prove that at the end of the borrow, the value is actually safe at T (i.e. not really pinned).
The promised type R of the mutable reference is P, in which case the parameter of the function is robust because its promised type B is unsafe. One must prove that at the end of the borrow, the unsafe values don't cause any problem in the rest of the program.

Unwrapping Pin

In the mental model, this function is also polymorphic over both types of the mutable reference. We'll also introduce the predicate parameters Q and R as above, and name the different values A, B, C, and D.

(Pin<&mut [Update<Q, T> .. Update<R, T>]>) -> &mut [Update<Q, T> .. Update<R, T>]
//         ^--- A  ---^    ^--- B  ---^             ^---  C ---^    ^---  D ---^

We can draw a similar table as above assuming the function is the identity function.

`Q`	`R`	`A <: Q`	`R <: B`	`Q <: C`	`D <: R`
`T`	`T`	`P <: T`	`T <: P`	`T == T`	`T == T`
`T`	`P`	`P <: T`	`P == P`	`T == T`	`T <: P`
`P`	`T`	`P == P`	`T <: P`	`P <: T`	`T == T`
`P`	`P`	`P == P`	`P == P`	`P <: T`	`T <: P`

Same as above, the function is unsafe when the subtyping relation does not hold, usually because of P <: T. Similarly, we can look at the 2 reasons (assuming T <: P) why the function can be unsafe:

The type Q of the mutable reference is T, in which case the parameter of the function is unsafe because its type A is robust. One must prove that the value is actually safe at T when calling the function.
The type Q of the mutable reference is P, in which case the result of the function is unsafe because its type C is unsafe. One must prove that the unsafe values don't cause any problem.

Unpin

A type is Unpin if P is equal to T. It essentially has no pinned typestate and a single safety invariant.

Example

To be done (see https://github.com/ia0/unsafe-mental-model/issues/2).

Please open an issue on Github if you find a bug.

Definition 3b of https://www.ralfj.de/blog/2018/04/05/a-formal-look-at-pinning.html requires this subtyping relation to hold.

The update type

An attempt to add the update type to Rust could be something like this:

/// Generic wrapper over valid values of type T.
///
/// The predicate P describes which valid values are safe at the wrapped type.
#[lang = "update"]
#[repr(transparent)]
pub struct Update<P, T> {
    predicate: PhantomData<P>,
    value: T,
}

impl<P, T> Update<P, T> {
    /// Wraps a value.
    ///
    /// # Safety
    ///
    /// The predicate P must hold for the parameter.
    ///
    /// # Robustness
    ///
    /// - The parameter doesn't need to be a safe value.
    /// - This is the identity function.
    pub robust unsafe fn wrap(value: T) -> Self {
        Update { predicate: PhantomData<P>, value }
    }

    /// Unwraps a value.
    ///
    /// # Robustness
    ///
    /// - The predicate P holds for the result.
    /// - This is the identity function.
    ///
    /// # Safety
    ///
    /// The result is not necessarily a safe value.
    pub robust unsafe fn unwrap(self) -> T {
        self.value
    }
}

It's not clear what restrictions this type needs to have to be safe. It shouldn't implement any trait that provides safe access to the value (e.g. Deref and DerefMut). Producing (resp. consuming) an update type should always be unsafe because the predicate may be robust (resp. unsafe).

Examples

Pin is a specific instance of the update type where T implements Deref and DerefMut in a specific way, such that implementing Deref and DerefMut for Pin is safe.

/// # Safety
///
/// If `T` implements Deref, it must not break "Pinned T". Idem for DerefMut.
pub struct Pin<T>(Update<"Pinned T", T>);

The robust keyword

Robust is the dual of unsafe with respect to variance. It is thus natural to imagine a notation for it. The main reason this doesn't exist is because it is not recommended to actively document a type as robust. This should only be done when the robustness of the type is needed for a proof, thus justifying the burden of making sure the implementation is actually robust.

Let's look at a world where robust is the dual keyword of unsafe. We'll make the update type explicit for clarity, but it may be omitted.

/// Prints a message to the standard output.
///
/// # Robustness
///
/// The message doesn't need to be valid UTF-8.
pub robust fn supersafe_print(msg: &Update<str>);

/// Consumes a box returning its raw pointer.
///
/// # Robustness
///
/// The pointer will be properly aligned and non-null.
pub robust fn into_raw(b: Box<T>) -> Update<*mut T>

Note that a function may be both robust and unsafe.

/// Returns the n-th valid `char` of a string.
///
/// # Robustness
///
/// The string doesn't need to be valid UTF-8.
///
/// # Safety
///
/// There must be at least `n` valid `char`s in `s`. A `char` is valid in the
/// string if it is the first sequence of bytes that form a UTF-8 `char` since
/// the previous valid `char` in the string (or the beginning of the string).
pub robust unsafe fn chars_nth(s: &Update<str>, n: Update<usize>) -> char;

The robust keyword would also bring clarity to unsafe traits. When a trait is unsafe only because some of its non-inherited methods or associated constants are robust, then it actually doesn't need to be unsafe.

/// Dynamic management of some large owned allocation.
trait Allocator {
    /// Allocates a small allocation from the large allocation.
    ///
    /// # Errors
    ///
    /// Returns an error in the following conditions:
    /// - The layout is not supported by the allocator.
    /// - There is not enough available space in the large allocation.
    ///
    /// # Robustness
    ///
    /// The result points to a small allocation from the large allocation with
    /// the following properties:
    /// - It does not alias with any previously allocated (and not yet
    ///   deallocated) small allocations.
    /// - It is not null (a consequence of coming from the large allocation).
    /// - It satisfies the layout (correct size and alignment).
    ///
    /// Note that the small allocation is uninitialized and thus not valid for
    /// read.
    robust fn allocate(&self, layout: Layout) -> Result<Update<*mut u8>, AllocError>;

    /// Deallocates a small allocation back to the large allocation.
    ///
    /// # Safety
    ///
    /// The following properties must hold:
    /// - The pointer comes from a previous call to `allocate()` with the same
    ///   layout.
    /// - The pointer has not yet been deallocated yet (a consequence of the
    ///   next point).
    /// - The pointer will not be used anymore. The ownership of the small
    ///   allocation it represents is given back to the allocator.
    unsafe fn deallocate(&self, ptr: Update<*mut u8>, layout: Layout);
}

Notice how implementing the trait is safe. Implementing allocate() will require some proof of robustness and thus be "unsafe" to implement. Implementing deallocate() on the other hand is "safe". One can simply leak the pointer. However in practice, one will probably modify the allocator internal state to be able to reuse that small allocation. This will require some proofs that some allocator invariant is preserved, which is "unsafe". The next chapter discusses exactly this topic of invariants.

Proof fields

Fields may use anonymous types, either to be robust and/or unsafe. This usually encodes the invariant of the struct (or more generally any custom type). Writing to those fields require to update the proof too. More generally, modifying anything that the predicate relies on, requires to update the proof.

/// Vectors of at most 1024 bytes.
pub struct Vec1024 {
    /// Storage of the vector.
    ///
    /// # Robustness
    ///
    /// Points to an allocation of 1024 bytes and is owned.
    ptr: Update<*mut u8>,

    /// Length of the vector.
    ///
    /// # Robustness
    ///
    /// - Always smaller than or equal to 1024.
    /// - The storage prefix of that length is initialized.
    len: Update<usize>,
}

impl Vec1024 {
    pub fn push(&mut self, x: u8) {
        assert!(self.len < 1024);

        // SAFETY: The addition stays within the allocation by the check above.
        // The write is thus also valid.
        unsafe { self.ptr.add(self.len).write(x) };

        // SAFETY: The new length is safe because:
        // - The old length was smaller than 1024 by the check above and only 1
        //   is added, it is thus smaller than or equal to 1024.
        // - The pointed prefix is initialized because it was initialized up to
        //   the last byte and we just wrote the last byte.
        unsafe { self.len += 1 };
    }
}

It is sometimes more convenient to have a single proof field to gather all invariants. One needs to prove the invariant is preserved each time a field (or something else) referred by the predicate is modified.

/// Vectors of at most 1024 bytes.
pub struct Vec1024 {
    ptr: *mut u8,
    len: usize,

    /// Invariant.
    ///
    /// # Robustness
    ///
    /// - The pointer points to an allocation of 1024 bytes and is owned.
    /// - The length is always smaller than or equal to 1024.
    /// - The pointed prefix of size length is initialized.
    inv: Proof,
}

impl Vec1024 {
    pub fn push(&mut self, x: u8) {
        assert!(self.len < 1024);

        // SAFETY: The invariant is trivially preserved (neither the pointer nor
        // the length have been modified). The addition stays within the
        // allocation by the check above. The write is thus also valid.
        unsafe { self.ptr.add(self.len).write(x) };

        // SAFETY: The invariant is preserved:
        // - The length is smaller than or equal to 1024 because it was smaller
        //   than 1024 and only 1 is added.
        // - The pointed prefix is initialized because it was initialized up to
        //   the last byte before and we just wrote the last byte.
        unsafe { self.len += 1 };
    }
}

Unsafe reviews

Unsafe reviews is the process of reviewing unsafe code for soundness. For those reviews to be sustainable on code change, it is important to not trigger a review too often while still triggering each time it is needed. The current approach is to trigger a review when a file containing the unsafe keyword is modified. This is a good approximation in the sense that if files with the unsafe keyword are kept small then reviews won't trigger too often. However, it may also miss some reviews when unsafe code relies on properties outside files with the unsafe keyword (like robust implementations).

Sound triggering

If the robust keyword existed, unsafe reviews could trigger on files containing any of those 2 keywords. By making sure during unsafe review that proofs only rely on documented robust properties (parameter of unsafe function or result of robust function), this would make sure that unsafe review will trigger each time it is needed.

Here are some examples of proofs that depended on undocumented or incorrect robustness:

Burden of proof

To avoid increasing the burden of unsafe reviews, it is important that items are not documented as robust unless it is known that a proof relies on them. To ensure this, robust items should also document in their robustness section which crates rely on their robustness. This could alternatively be tracked in a separate global tool like cargo-vet.

For example, one should not implement TrustedLen unless it is relied upon somewhere. This is deliberately a borderline example to show that it is actually a trade-off between increasing the burden of proof and implementing possibly useful functionalities.

Recommended lints

It is almost obligatory to enable unsafe-op-in-unsafe-fn which is allowed-by-default up to edition 2021 and warn-by-default starting from edition 2024. Not using this lint will:

give you a wrong mental model conflating unsafe in types (properties) and unsafe in code (proofs) as described in the RFC,
conflict with undocumented-unsafe-blocks described below,
conflict with multiple-unsafe-ops-per-block described below.

The following lints will help unsafe review further:

undocumented-unsafe-blocks is the most important one. Without it, unsafe reviewers have to reverse the invariants by reading all the code. Anything non-local should be avoided during reviews.
multiple-unsafe-ops-per-block is related but secondary. Without it, the safety comment may either (best case scenario) be proving multiple unsafe superpowers being used at the same time resulting in possible confusion, or (worst case scenario) forgetting to prove one of the unsafe superpowers being used resulting in the same issue as if undocumented-unsafe-blocks was not enabled.

Finally, unused-unsafe (which is warn-by-default) is the other side of multiple-unsafe-ops-per-block. Both together ensure that there is a one-to-one correspondence between the usage of unsafe superpower and the safety comment proving its soundness, thus simplifying unsafe reviews.

Type theory

This chapter is meant for those looking for something more formal. Either how the mental model could be made more formal, or where does the mental model come from. It is work in progress and can use your help. Feel free to open issues or pull requests.

Existing work

The mental model is inspired by the following concepts:

The Curry-Howard isomorphism for internalizing the notions of predicates and proofs in the programming language. The decision of doing so being that programmers may be able to translate their intuition regarding code and types to proofs and predicates, in particular to understand that receiving a proof means you can use it to produce another proof, and that a proof implements a predicate.
Dependent types for predicates to depend on the execution environment (the memory, variables, etc). In particular, the update type is the sigma type.
Denotational semantics for interpreting types as their set of values.
RustBelt for letting unsafe escape the syntactic type system but capturing it within the semantic type system.
Erasable coercions for considering all the typing (in particular the environment) as part of the semantics for subtyping. This is why we can talk about the execution environment in type interpretations: we are actually interpreting the whole typing, not just the type. This is only done for functional programming languages and would need to be adapted for imperative ones.
RustHornBelt for the idea of prophecies to explain the promised type of mutable references.
Refinement types which the update type is similar to. The main difference is that the update refines the validity invariant, not the type itself.

Breaking the dependency

Using documentation and comments instead of types and code is mostly for practical reasons.

It is impractical to write types like Proof<"# Safety\n\nThe absolute value of the result is smaller than or equal to 1000."> and code like Update { proof: "// SAFETY: We know that arguments are small, so some small linear combination is only slightly bigger.", value: () }.

But moving predicates out of types also breaks the dependency they have on the execution environment. A consequence of this choice is that it looks like we get some form of type erasure, but this is only in appearance. Even though the properties are erased from the types, the programmer must know at runtime the properties of all proofs (both parameters and results). For example, having a vector of function pointers like Vec<fn(Proof)> would need the programmer to know for each element, what are the properties expected to hold to call the function, because they may differ from one element to the other.

Glossary

anonymous type: A type built from its interpretation, thus without syntax.
associated proof: An associated constant of the proof type.
bottom type: The type with an empty interpretation.
permissions to use: Characteristic of a robust type.
promised type: The type at the end of a borrow of a mutable reference.
restrictions to use: Characteristic of an unsafe type.
robust type: An anonymous type missing some safe values.
safe type: A Rust type (its interpretation is exactly the safe values).
safe value: A value satisfying the safety invariant.
soundness: The property of type systems that only accept defined programs.
subtyping: The inclusion relation between type interpretations.
type interpretation: A mapping from types to their set of values.
unsafe type: An anonymous type containing some unsafe values.
unsafe value: A valid but not safe value.
valid value: A value satisfying the validity invariant.
value: A part of the execution of a program.
variance: Type-level functions behavior regarding subtyping.

References

Some useful (and official) documentation regarding unsafe:

The unsafe Rust section of the Rust book.
The unsafe keyword documentation in the standard library.
The unsafe keyword section in the Rust reference.
The unsafe code guidelines.
The Rustonomicon.
The subtyping and variance section of the Rust reference.

Mental model for unsafe in Rust