Building a safe abstraction on an unsafe core

Lesson 19 ended with unsafe handing the proof to a human: stating obligations is not discharging them. This lesson discharges them twice: in split_at_mut, which rescues a safe program the checker refuses, and in MyVec<T>, a minimal vector whose proof spans a whole module. The move is the same both times: state the invariants, keep their state private, and show that every public function keeps them on every path. That buys an API no safe caller, however hostile, can drive into undefined behavior.

The thesis, here

Soundness belongs to an API, not to a block. An unsafe block is right only relative to facts around it — a length, a capacity, which slots hold values — so its proof covers every line that can change them. Privacy bounds those lines to one module; the invariants say what it must keep true.

Linear position

Forced by: The keyword unsafe hands the proof to a human: the obligations are stated, but stating them is not discharging them. How do you build a safe abstraction on an unsafe core so that no safe caller, however hostile, can break it?
New idea: state the invariants the unsafe code reads, keep them on every path (unwinding and caller-supplied code included), and make their fields private. Invariants plus privacy turn an unsafe core into a safe API: only the module can break the proof, so only the module must be audited.
Forces next: A sound abstraction survives only while its invariants stay private. How is code organized into modules and crates so that privacy is enforced, dependencies are managed, and other teams can rely on what you promise?

The plan

Six moves. (1) Split a slice into two exclusive halves: safe, refused, proved by hand. (2) Turn the proof into four obligations. (3) Apply them to a minimal Vec. (4) Run a model of it. (5) Break it one line at a time. (6) Name the rule underneath: trust nothing you do not control, not even a destructor.

1 · A safe program the checker refuses

A frame buffer holds six samples, and we want to swap its front half with its back half in place, borrowing each half exclusively:

fn main() {
    let mut frame = vec![1, 2, 3, 4, 5, 6];
    let mid = frame.len() / 2;
    let front = &mut frame[..mid];      // an exclusive borrow of frame...
    let back = &mut frame[mid..];       // ...and a second one, while front is live
    for (a, b) in front.iter_mut().zip(back.iter_mut()) {
        std::mem::swap(a, b);
    }
    println!("{frame:?}");
}

Reading the error

error[E0499]: cannot borrow `frame` as mutable more than once at a time
 --> src/main.rs:5:21
  |
4 |     let front = &mut frame[..mid];      // an exclusive borrow of frame...
  |                      ----- first mutable borrow occurs here
5 |     let back = &mut frame[mid..];       // ...and a second one, while front is live
  |                     ^^^^^ second mutable borrow occurs here
6 |     for (a, b) in front.iter_mut().zip(back.iter_mut()) {
  |                   ----- first borrow later used here
  |
  = help: use `.split_at_mut(position)` to obtain two mutable non-overlapping sub-slices

The three labels are Lesson 07's anatomy, and all three are true. What the checker cannot know is that ..mid and mid.. are disjoint — arithmetic on a run-time value — so it cannot tell this split from an overlapping one. The help names a library function that did that proof once, with unsafe inside; unsafe { } around these borrows would change nothing (Lesson 19).

The program is safe — [0, 3) and [3, 6) share no element — and refused, because the checker is sound but not complete (Lesson 07). Three roads: index one element at a time (a bounds check per access, and no halves to hand to two functions); copy one half into a fresh buffer (an allocation nobody asked for); or prove it once, by hand, behind a safe signature:

use std::slice;

// A safe signature over an unsafe body: both halves borrow from v, for as long as v is borrowed.
fn split_at_mut<T>(v: &mut [T], mid: usize) -> (&mut [T], &mut [T]) {
    let len = v.len();
    let ptr = v.as_mut_ptr();
    assert!(mid <= len);                                    // (1) both ranges lie inside v
    unsafe {
        (slice::from_raw_parts_mut(ptr, mid),                // [0, mid)
         slice::from_raw_parts_mut(ptr.add(mid), len - mid)) // [mid, len): (2) disjoint, (3) all of v
    }
}

fn main() {
    let mut frame = vec![1, 2, 3, 4, 5, 6];
    let (front, back) = split_at_mut(&mut frame, 3);
    for (a, b) in front.iter_mut().zip(back.iter_mut()) {
        std::mem::swap(a, b);
    }
    println!("{frame:?}");
}

[4, 5, 6, 1, 2, 3]

slice::from_raw_parts_mut(ptr, n) builds an exclusive slice from an address and a length, and is an unsafe fn because it believes them. The function around it is safe to call: its signature promises every caller two exclusive halves of v. So the body owes four facts, each checkable against a line:

What the unsafe calls rely on	Where the body makes it true
(1) `mid <= len`: both ranges lie inside `v`	the `assert!`: a panic, which is defined, instead of a pointer past the end
(2) `[0, mid)` and `[mid, len)` do not overlap	they meet at `mid`, so the two `&mut` never alias
(3) together they are exactly `v`	`mid + (len - mid) == len`: nothing outside `v` is handed out
(4) both results borrow `v`, for its lifetime	the elided signature (Lesson 08): while a half lives, `frame` stays borrowed

Now the counterexamples. Delete the assert!, and a caller passing 8 gets ptr.add(8), two past the end and undefined by itself, and a length 6 - 8 that wraps in a default release build: the signature is unchanged and safe code writes outside the buffer. Start the back half at mid - 1, and two live exclusive references reach one element: undefined even if neither is written. split_at_mut is the easy case: no state, one function. A type whose invariant several functions share needs a recipe.

2 · What a safe abstraction owes

Lesson 19 set the standard: unsafe code is sound when no safe client can use it to cause undefined behavior, and that is its author's responsibility. A function's proof is local; a type's is not. A vector's push writes slot len believing the slot exists, a belief other functions established, and Lesson 19's Nomicon example shows how far that reaches: a safe method that bumps cap makes the unsafe push unsound. So the proof covers every line that can change what the unsafe blocks read. It owes four things:

(a) Write the invariants

Every fact an unsafe block reads that the compiler does not check — a length, a capacity, which slots hold values — stated beside the fields.

(b) Make their state private

Then only the module can break an invariant, so only the module needs auditing (the unit of audit, Lesson 19).

Each public function starts and ends in the invariants — also when it panics halfway, since unwinding runs destructors on the half-done state, and when it runs caller-supplied code (a clone, a comparison) whose correctness is never part of the proof.

(d) Need nothing else

A hostile caller reaches the state only through functions that keep the invariants, so it only ever sees states that satisfy them: induction over calls.

Road not taken · make the caller prove it

The other honest design is an unsafe fn whose caller promises mid <= len; std ships one, split_at_mut_unchecked, undefined for mid > len even if the result is unused. It moves the proof to every call site, which pays when callers can prove the fact more cheaply than the callee can check it. A safe signature claims that no caller has anything to prove.

The smallest type that needs all four is the one this track has used since Lesson 00: a growable array.

3 · A minimal Vec: MyVec<T>

A vector is three words: a pointer to a heap buffer, the buffer's capacity, and how many of its slots hold values. The buffer comes from the global allocator, alloc(layout), where Layout::array::<T>(n) is the size and alignment of n values of T. Every unsafe line reads the three fields and believes them, so the invariants are about them:

#	Invariant	Unsafe code that relies on it
I1	`len <= cap`	`Deref` lends `len` values out of `cap` slots
I2	slots `0..len` hold values it owns: written, not moved out, each once	`pop` and `Deref` read them; `Drop` drops them
I3	slots `len..cap` are spare: allocated, owed no drop	`push` writes slot `len`, dropping nothing
I4	`ptr` came from `alloc(Layout::array::<T>(cap))` and is this vector's alone; if `cap == 0`, nothing is allocated and `ptr` is a dangling, aligned placeholder	growing and `Drop` free it with that layout, never when `cap == 0`

Here is the core, each unsafe line marked with the invariant it relies on or restores:

use std::alloc::{alloc, dealloc, handle_alloc_error, Layout};
use std::{marker::PhantomData, mem, ops::Deref, ptr::{self, NonNull}, slice};

pub struct MyVec<T> {
    ptr: NonNull<T>,      // I4: from alloc(Layout::array::<T>(cap)), or dangling when cap == 0
    cap: usize,           // I1: len <= cap
    len: usize,           // I2: slots 0..len hold values; I3: slots len..cap are spare
    _own: PhantomData<T>, // "owns T values", for what the compiler derives from fields
}
impl<T> MyVec<T> {
    pub fn new() -> Self {
        assert!(mem::size_of::<T>() != 0, "zero-sized types are not handled");
        MyVec { ptr: NonNull::dangling(), cap: 0, len: 0, _own: PhantomData }   // I1-I4 hold
    }
    pub fn capacity(&self) -> usize { self.cap }
    fn grow_to(&mut self, new_cap: usize) {
        let layout = Layout::array::<T>(new_cap).expect("capacity overflow");
        let new = unsafe { alloc(layout) } as *mut T;
        let new = NonNull::new(new).unwrap_or_else(|| handle_alloc_error(layout));
        if self.cap != 0 {
            unsafe {
                ptr::copy_nonoverlapping(self.ptr.as_ptr(), new.as_ptr(), self.len); // keep I2
                dealloc(self.ptr.as_ptr() as *mut u8, Layout::array::<T>(self.cap).unwrap());
            }
        }
        self.ptr = new;                                          // I4 for the new capacity
        self.cap = new_cap;
    }
    fn grow(&mut self) { self.grow_to(if self.cap == 0 { 1 } else { 2 * self.cap }); }
    pub fn push(&mut self, x: T) {
        if self.len == self.cap { self.grow(); }                 // now slot len is spare (I3)
        unsafe { ptr::write(self.ptr.as_ptr().add(self.len), x); } // fill it, dropping nothing
        self.len += 1;                                           // then count it (I2)
    }
    pub fn pop(&mut self) -> Option<T> {
        if self.len == 0 { return None; }
        self.len -= 1;                                           // uncount the last slot...
        Some(unsafe { ptr::read(self.ptr.as_ptr().add(self.len)) }) // ...then move its value out
    }
}
impl<T> Deref for MyVec<T> {
    type Target = [T];
    fn deref(&self) -> &[T] { unsafe { slice::from_raw_parts(self.ptr.as_ptr(), self.len) } } // I1, I2, I4
}
impl<T> Drop for MyVec<T> {
    fn drop(&mut self) {
        while self.pop().is_some() {}                            // drop exactly the len values (I2)...
        if self.cap != 0 {                                       // ...then free what was allocated (I4)
            unsafe { dealloc(self.ptr.as_ptr() as *mut u8, Layout::array::<T>(self.cap).unwrap()); }
        }
    }
}
unsafe impl<T: Send> Send for MyVec<T> {}  // I2, I4: it owns its Ts alone, so sending it sends them
unsafe impl<T: Sync> Sync for MyVec<T> {}  // a &MyVec<T> lends out only &T

fn main() {
    let mut v = MyVec::new();
    for word in ["red", "green", "blue"] { v.push(word.to_string()); }   // cap 0 → 1 → 2 → 4
    let last = v.pop();
    println!("{:?} {:?} len {} cap {}", last, &v[..], v.len(), v.capacity()); // [..], len(): Deref
}

Some("blue") ["red", "green"] len 2 cap 4

Three orderings carry the proof: push writes before it counts, pop uncounts before it reads, grow_to copies before it frees. ptr::write fills a slot without dropping its old contents (assignment would drop garbage); ptr::read moves a value out and leaves the slot logically uninitialized. Deref<Target = [T]>, sound by I1, I2 and I4, gives MyVec every slice method: len(), iteration, indexing.

What this MyVec does not cover

Zero-sized types: allocating zero bytes is undefined, so the Nomicon treats them apart (capacity usize::MAX, no allocation) and new refuses them here. Allocation failure: handle_alloc_error aborts rather than panics; capacities past isize::MAX bytes stop at Layout::array's error. We stop before IntoIter, Drain and RawVec, the same proof over more code. Doubling is the Nomicon's tutorial choice; std promises amortized constant-time push, not a factor.

The compiler also derives properties from the field types, so they must be the right ones. Variance (Lesson 08's sidebar): hold a *mut T, and MyVec becomes invariant in T, so a vector of &'static str cannot be lent where one of &'a str is expected:

pub struct MyVec<T> { ptr: *mut T, cap: usize, len: usize }                 // a raw *mut T instead
pub fn shrink<'a>(v: &'a MyVec<&'static str>) -> &'a MyVec<&'a str> { v }   // rejected: MyVec<T> is invariant in T

NonNull<T> is covariant, which is Lesson 06's direction (a longer borrow may stand where a shorter one is expected), and never null, so we hold one. PhantomData<T> says "owns a T" where fields do not: a zero-sized field treated as owning a T for variance, the auto traits and the drop check (dropping a MyVec<T> drops Ts, so every borrow inside one must still be valid when the vector is dropped). Send and Sync come out "no", as NonNull<T> is neither; the two unsafe impls are promises justified by I2 and I4 (Lesson 16). The compiler checked none of this proof. So test it.

4 · Try it: the invariant checker, with fault injection

The widget runs a model of MyVec on an allocation table (buffers of slots; values owned, moved out or dropped; headers with ptr, cap, len), each method transliterated from the Rust on this page. Each raw operation checks its precondition, and the model stops at the first undefined behavior, after which nothing has a meaning; after every operation, and at every panic before unwinding, it checks I1–I4. A mutant is one edit. On 508 scripts run by rustc, the model predicted every length, capacity and result of the real MyVec, which matched std::Vec with every value dropped exactly once. The mutants were not run: a program with undefined behavior has no output to trust, so an independently written interpreter checked the model's verdicts on 2,400 mutant scripts, and the "silent unless" conditions of §5, with no disagreement.

Vec from raw parts, with fault injection

Green slots hold counted values, hatched ones are spare, red ones are counted but hold no value, dashed ones lie outside the buffer; a clone gets its own row. The slider replays the script, drop(v) last. Script: push a, pop, insert 1 x, remove 0, truncate 2, clone, len = 3 (compiles only with pub len); ! is a value whose clone() panics.

step: 9 preset: mutant:

len / cap

—

first broken invariant

—

undefined behavior

—

leaked (safe)

—

Show the core JS

// The four invariants of one MyVec header, checked against the allocation table.
function check(m, v) {
  var bad = [], a = v.ptr ? m.heap[v.ptr] : null, mine = {}, i, t, why;
  var others = m.vecs.filter(function (w) { return w !== v && w.ptr && w.ptr === v.ptr; });
  if (v.len > v.cap) bad.push([1, 'len is ' + v.len + ' but cap is ' + v.cap]);
  for (i = 0; i < v.len; i++) {                          // I2: every slot in 0..len holds a value it owns
    t = a && a.live && i < a.n ? a.cells[i] : null;
    why = !a || !a.live || i >= a.n ? 'is outside any live buffer' : !t ? 'was never written'
        : t.st === 'dropped' ? 'holds ' + t.name + ', already dropped' : t.st !== 'vec' ? 'holds ' + t.name + ', moved out'
        : mine[t.id] ? 'holds ' + t.name + ' twice' : others.some(function (w) { return i < w.len; }) ? 'holds ' + t.name + ', also owned by ' + others[0].name : '';
    if (why) { bad.push([2, 'slot ' + i + ' ' + why]); break; }
    mine[t.id] = true;
  }
  for (i = v.len; a && a.live && i < Math.min(v.cap, a.n); i++) {   // I3: no spare slot is still owed a drop
    t = a.cells[i];
    if (t && t.st === 'vec' && !mine[t.id]) { bad.push([3, 'spare slot ' + i + ' still holds ' + t.name + ', which nobody will drop']); break; }
  }
  if (v.cap === 0 ? v.ptr !== 0 : !(a && a.live && a.n === v.cap)) bad.push([4, 'ptr is not a live buffer of ' + v.cap + ' slots']);
  else if (others.length) bad.push([4, 'A' + a.id + ' is also held by ' + others[0].name]);   // I4: its own buffer
  return bad;
}

What to try. The tour keeps I1–I4 green through three growths, a pop, an insert, a remove, a clone and a truncate, and drops every value once. Pick "the second growth": I2 breaks at step 2, when the new buffer arrives without the old values, and the UB comes only at step 4, when Drop reads a slot nothing wrote. The same script with "correct MyVec" stays green. Then take "insert with one free slot" (UB at step 4, a copy to slot 4 of a 4-slot buffer) and delete one push: the insert now grows the buffer to 4 slots, so two are spare when the shift runs, and the same mutant passes. A green run clears a line only for the script it ran.

5 · What each broken line breaks

The model also runs the rest of MyVec, which continues the program above and was run with it against std::Vec:

impl<T> MyVec<T> {
    pub fn insert(&mut self, i: usize, x: T) {
        assert!(i <= self.len, "insertion index out of bounds");
        if self.len == self.cap { self.grow(); }
        unsafe {
            let p = self.ptr.as_ptr();
            ptr::copy(p.add(i), p.add(i + 1), self.len - i);  // shift slots i..len up by one
            ptr::write(p.add(i), x);
        }
        self.len += 1;
    }
    pub fn remove(&mut self, i: usize) -> T {
        assert!(i < self.len, "removal index out of bounds");
        self.len -= 1;
        unsafe {
            let p = self.ptr.as_ptr();
            let x = ptr::read(p.add(i));
            ptr::copy(p.add(i + 1), p.add(i), self.len - i);  // shift slots i+1..=len down by one
            x
        }
    }
    pub fn truncate(&mut self, n: usize) { while self.len > n { self.pop(); } }
}
impl<T: Clone> Clone for MyVec<T> {
    fn clone(&self) -> Self {
        let mut out = Self::new();
        if self.len > 0 { out.grow_to(self.len); }
        for x in self.iter() {
            unsafe { ptr::write(out.ptr.as_ptr().add(out.len), x.clone()); }  // T::clone may panic...
            out.len += 1;                                                     // ...so count after
        }
        out
    }
}

Each preset pairs a mutant with a script that exposes it. What the widget reports, and when the same mutant stays silent:

Mutant (one edit)	Flagged first	Then	Silent unless…
push forgets to grow	UB at step 1: a write through the dangling pointer	—	a push meets `len == cap` (the first push always does)
grow forgets to copy	I2 at step 2: slot 0 never written	an uninitialized read in `Drop`, step 4	the vector grows while it holds values
`len += 1` before the write	I2 of the copy, at the panic in step 4	the copy's `Drop` reads the unwritten slot	an element's `clone()` panics
pop forgets `len -= 1`	I2 at step 3: slot 1 holds `b`, already dropped	a use-after-free in `Drop`, step 5	a pop returns a value (`truncate` and `Drop` pop too)
`Drop` forgets to free	nothing: no invariant, no UB	a leak: buffer A3 is never freed	anything was ever allocated
`#[derive(Clone)]`	I2 at step 3: slot 0 also owned by the copy	a use-after-free at step 4, as `push` copies from the freed buffer	the cloned vector has a buffer
insert shifts one slot too many	UB at step 4: a copy to slot 4 of a 4-slot buffer	—	exactly one slot is spare when the shift runs
`pub len`	I1 at step 3: len is 4 but cap is 2	an out-of-bounds read in `Drop`, step 4	a caller writes a different `len`

Two mutants go straight to UB, because the broken line is the one that relied on the invariant: a write to slot len with no spare slot, a copy one past the end. The others break an invariant and let the damage land later, in code that did nothing wrong — usually Drop, the most trusting function of all. The families are Lesson 01's, reached from inside. The last column is why tests do not settle soundness: the off-by-one shift is silent unless exactly one slot is spare, the early len += 1 unless a clone() panics.

That reordering is about panic safety. In push the two lines may swap, since nothing between them can panic. In clone the caller's T::clone runs between them; if it panics, unwinding drops the half-built copy, whose Drop trusts len — the Nomicon's own example, a set_len before a loop of clones. The rule: wherever a panic can escape, the invariants hold; the state may be incomplete, never unsafe.

The derived Clone passes the compiler:

use std::ptr::NonNull;
#[derive(Clone)]                          // accepted: clones ptr, cap and len, not the buffer
pub struct MyVec<T> { ptr: NonNull<T>, cap: usize, len: usize }
impl<T> Drop for MyVec<T> { fn drop(&mut self) { /* frees ptr, as in §3 */ } }

#[derive(Clone, Copy)]                    // refused: a type with a destructor cannot be Copy
pub struct Header<T> { ptr: NonNull<T>, cap: usize, len: usize }
impl<T> Drop for Header<T> { fn drop(&mut self) {} }

The only error is on Header: a type with a destructor cannot be Copy, so no owner is duplicated implicitly. But Clone is the programmer's promise, and the derived one copies the pointer: two headers, one buffer, two drops. In C++ terms: a destructor with the compiler's copy left in place, the double free behind the rule of five (C++ track, Lesson 11).

The last mutant contains no unsafe code at all. With the fields private, the hostile line does not compile outside the module:

mod myvec {
    pub struct MyVec<T> { ptr: std::ptr::NonNull<T>, cap: usize, len: usize } // no pub on fields
    impl<T> MyVec<T> {
        pub fn new() -> Self { MyVec { ptr: std::ptr::NonNull::dangling(), cap: 0, len: 0 } }
    }
}
fn main() {
    let mut v: myvec::MyVec<String> = myvec::MyVec::new();
    v.len = 3;                    // a hostile caller: "trust me, there are three" — E0616
}

Mark the field pub and the line compiles, since anyone who can name a pub field may write it: the preset "a caller writes len" is then a program with no unsafe in main and undefined behavior at its end. Privacy is the part of the proof the compiler enforces; it cannot enforce what a caller's own code does, such as a clone that panics.

6 · The rule underneath

Two mutants failed through code the vector's author did not write: a panicking clone, a caller writing a field. The rule: unsafe code may trust code it chose — its own module, a dependency picked on purpose — never the correctness of safe code its clients supply, such as the impls behind a generic bound. The Nomicon's example is BTreeMap, which requires K: Ord and contains unsafe code: an Ord impl is safe to write and may lie, so a lying key may make the map erratic, never undefined:

use std::cmp::Ordering;
use std::collections::BTreeMap;

#[derive(PartialEq, Eq)]
struct Key(u32);
impl PartialOrd for Key { fn partial_cmp(&self, o: &Self) -> Option<Ordering> { Some(self.cmp(o)) } }
impl Ord for Key { fn cmp(&self, _: &Self) -> Ordering { Ordering::Less } }  // a lie: "always smaller"

fn main() {
    let mut map = BTreeMap::new();
    for k in [3, 1, 2] { map.insert(Key(k), k); }
    let keys: Vec<u32> = map.keys().map(|k| k.0).collect();
    println!("{} entries {:?}, get(&Key(1)) = {:?}", map.len(), keys, map.get(&Key(1)));
}

3 entries [2, 1, 3], get(&Key(1)) = None

The map cannot find a key it holds, and nothing worse happens. The other road, an unsafe trait the map may trust, moves the burden to every implementor; Rust has historically avoided unsafe traits, since they spread unsafe everywhere.

Destructors fall under the same rule. Leaks are safe (Lesson 03), so no proof may depend on a destructor running: Lesson 17's thread::scoped kept part of its proof in a guard's destructor, and leaking the guard broke it. For a vector it is the ordering we already used: make the state safe first; let a destructor only tidy up.

So the soundness of MyVec is a statement about one module: the author proves the invariants, the compiler enforces the privacy, the caller needs nothing — as long as nobody can reach past the privacy.

Common mistakes / failure modes

"Unsafe code makes the whole crate unsafe"

Only the module that owns the invariants is at risk: with its fields private, everything else goes through functions that keep them (§2).

"The checker rejected it, so it must be unsafe"

Rejected means not shown safe: the half-swap is safe and refused (E0499); one hand proof in split_at_mut serves every caller (§1).

"Just use Vec<Option<T>> and avoid all this"

Often right: None for "uninitialized" makes every slot a value and safe code suffices, at a check per access. Better still, use std's Vec; raw parts are for building the container itself.

"Drop will clean up if my unsafe code panics"

Drop cleans up what the invariants say is there: if len already counts a slot nobody wrote, unwinding drops garbage (§5).

"Destructors always run, so Drop can finish the proof"

Leaks are safe: after mem::forget, or in an Rc cycle, a destructor never runs, so the proof must hold without it — why thread::scoped was removed (§6).

"Wrapping unsafe in a function makes it safe"

Only if no caller can break the precondition: without its assert!, split_at_mut keeps a safe signature and is unsound. If the caller must promise something, it is an unsafe fn (§1, §2).

Checkpoint exercise

Try it

(1) With the mutant "insert shifts one slot too many", find a script of at most four operations that ends all green and one that ends in UB; state the exact condition on len and cap when the shift runs, and test it on a third script. (2) In a scratch file, add pub fn swap_remove(&mut self, i: usize) -> T to MyVec — move slot i's value out, move the last value into slot i, shrink by one — and write beside each line the invariant it relies on or restores. Test it against the same steps on a std::Vec, including i equal to the last index.

Where this points next

Every proof here rested on a fact the language enforced: code outside the module could not touch the fields. One keyword, pub, turned a sound vector into one safe code breaks in a line. But a module is only the innermost boundary: real abstractions live in crates that other teams compile against, and "no safe caller can break this" must survive that too. So the question becomes organization: how do modules and crates keep privacy enforced, dependencies managed, and your promises reliable for other teams?

Takeaway

A safe abstraction over unsafe code is a proof about one module. Write down every fact the unsafe code reads (for MyVec: len <= cap, slots 0..len hold owned values, slots len..cap are spare, ptr is its own buffer of cap slots), keep those fields private, and show that each public function keeps those facts true on every path, a panic and the caller's code included: then no safe caller can reach a bad state. split_at_mut is the one-function case. A broken line usually breaks an invariant silently and lets Drop commit the UB later. A leak is safe, so no proof may rely on a destructor running, nor on caller-supplied safe code being correct.

Interview prompts

How do you build a safe API on top of unsafe code? (§2 — state the invariants the unsafe code reads, keep their fields private, and prove every public function keeps them on every path, panics and caller code included.)
Why is split_at_mut sound, and why does the naive version not compile? (§1 — the checker sees two exclusive loans on one place and does not evaluate ranges; the function asserts mid <= len and builds disjoint [0, mid) and [mid, len) tied to the input's lifetime.)
What are a Vec's invariants, and how does it grow without breaking them? (§3 — len ≤ cap; 0..len owned values; len..cap spare; ptr its own buffer of cap slots, dangling at cap 0. Growth allocates, copies the len values, frees the old buffer, then updates ptr and cap.)
What is PhantomData for, and why NonNull<T> rather than *mut T? (§3 — a zero-sized field treated as owning a T for variance, drop check and auto traits; *mut T would make the vector invariant, NonNull<T> is covariant and non-null.)
What is panic safety? Give a bug. (§5 — the invariants hold wherever a panic can escape, since unwinding runs Drop; counting a slot before T::clone fills it lets the half-built copy's Drop read garbage.)
Why can't unsafe code trust Ord, and is a leak a soundness bug? (§6 — an Ord impl is safe to write and may lie, so a lie may only make BTreeMap erratic; leaks are safe (mem::forget), so no proof may lean on a destructor.)

Companion reads: C++ · 11 Resource-safe design (the rule of five; §5's shallow copy), C++ · 13 STL containers (vector growth), C++ · 19 Undefined behavior (what the mutants become).