Formal Equations, Memory Identities & Mathematical Invariants

Rust's memory safety guarantees are founded on rigorous mathematical logic.

This reference lesson brings together the core formal equations, alignment formulas, memory identities, and theorems established throughout the curriculum.

Universal Fat PointerMemory Layout

16 Bytes

All standard fat pointers (&[T], &str, dyn Trait) occupy exactly 16 bytes on 64-bit hardware.

1. Hardware Alignment & Padding Equations#

For any composite struct $S$ containing field types $F_1, F_2, \dots, F_n$ with alignments $A(F_i)$ :

Aggregate Struct Alignment#

The struct's alignment requirement equals the maximum alignment of its constituent components:

\text{Align}(S) = \max\bigl(A(F_1), \, A(F_2), \, \dots, \, A(F_n)\bigr)

Field Offset Invariant#

Every field offset $O_i$ must be an integer multiple of that field's alignment requirement:

O_i \equiv 0 \pmod{A(F_i)}

Total Memory Footprint#

Total memory footprint equals the sum of field sizes plus alignment padding bytes ( $P_i$ ) and tail padding ( $P_{\text{tail}}$ ):

\text{Size}(S) = \sum_{i=1}^{n} \text{Size}(F_i) + \sum_{i=1}^{n} P_i + P_{\text{tail}}

\text{Size}(S) \equiv 0 \pmod{\text{Align}(S)}

2. The XOR Aliasing Invariant#

At any given point $p$ in program execution, for any resource $x$ , active immutable references $R(x)$ and active mutable references $W(x)$ must satisfy mutual exclusivity:

\forall x, \quad \bigl(|R(x)| \ge 0 \land |W(x)| = 0\bigr) \quad \lor \quad \bigl(|R(x)| = 0 \land |W(x)| \le 1\bigr)

\text{Valid}(p) \iff |R(x)| \times |W(x)| = 0

Architecture Diagram

Rendering diagram...

3. 64-Bit Memory Size Identities#

Understanding the exact byte footprint of primitives and pointers on 64-bit hardware is essential for cache optimization:

Type Expression	Size in Bytes	Internal Representation & Components
`&T` / `&mut T`	8 Bytes	Single 64-bit hardware memory pointer.
*`const T` / `mut T`*	8 Bytes	Bare 64-bit raw pointer address.
`Box<T>`	8 Bytes	Single 64-bit pointer pointing to heap allocation.
`Option<&T>`	8 Bytes	Niche optimization: `0x0` represents `None` (Zero tag overhead).
`&[T]` (Slice Reference)	16 Bytes	Fat Pointer: 8-byte base address + 8-byte `usize` element count.
`&str` (String Slice)	16 Bytes	Fat Pointer: 8-byte UTF-8 data address + 8-byte `usize` byte length.
`dyn Trait` (Trait Object)	16 Bytes	Fat Pointer: 8-byte payload pointer + 8-byte static vtable pointer.
`String`	24 Bytes	8-byte pointer + 8-byte capacity + 8-byte length.
`Vec<T>`	24 Bytes	8-byte buffer pointer + 8-byte capacity + 8-byte length.
`()` (Unit / ZST)	0 Bytes	Zero-Sized Type: stripped from physical memory layouts.

4. The Thread Safety Theorem#

The foundational theorem connecting Send and Sync:

T : \text{Sync} \iff \&T : \text{Send}

A type $T$ is thread-safe to share across concurrent threads if and only if an immutable borrow of $T$ ( $\&T$ ) is safe to transfer between threads.

Closure Subtyping Subset Hierarchy#

\{c \mid c \in Fn\} \subseteq \{c \mid c \in FnMut\} \subseteq \{c \mid c \in FnOnce\}

5. Concept Verification#

Test your mastery of formal equations and memory identities:

Concept check

What is the exact memory size of an Option<&T> on a 64-bit architecture?

Concept check

If a struct has three fields with alignment requirements 1 byte, 4 bytes, and 8 bytes, what is the aggregate alignment requirement of the struct?