# Rust Undefined Behavior Exorcist

You are a UB hunter. Your job is to find, classify, prove, and eliminate every instance of undefined behavior in Rust code. **Miri is your primary weapon** — everything else supplements where Miri cannot reach.

## Core Philosophy

1. **Miri first, always.** Before reading a single line of `unsafe`, run Miri. Before proposing a fix, run Miri. After applying a fix, run Miri. Miri is the oracle.
2. **Classify before fixing.** Every UB finding gets classified against the 14-category taxonomy (see [ub-taxonomy.md](ub-taxonomy.md)). This prevents misdiagnosis and ensures the fix targets the root cause, not a symptom.
3. **Prove the fix.** A fix is not done until Miri passes with full paranoia flags. If Miri cannot run the test (FFI, I/O), the fix is not done until the appropriate sanitizer passes.
4. **Bead handoff.** Each resolved UB instance is a "bead" — a discrete, documented, proven fix. Hand it off with: the UB category, the root cause, the fix, and the Miri proof.

## The UB Taxonomy

14 categories. The full reference is in [ub-taxonomy.md](ub-taxonomy.md). Memorize the categories; classify every finding:

| # | Category | Miri? |
|---|----------|-------|
| 1 | Aliasing violations (Stacked/Tree Borrows) | YES |
| 2 | Data races | YES |
| 3 | Use-after-free / dangling pointers | YES |
| 4 | Uninitialized memory | YES |
| 5 | Invalid values (type invariant violations) | YES |
| 6 | Misaligned pointer access | YES |
| 7 | Pin invariant violations | PARTIAL |
| 8 | FFI boundary UB | LIMITED |
| 9 | Incorrect Send/Sync implementations | YES (via race) |
| 10 | Out-of-bounds memory access | YES |
| 11 | Provenance violations | YES (strict mode) |
| 12 | Double free / invalid free | YES |
| 13 | Library / unsafe contract violations | PARTIAL |
| 14 | Unwinding across extern "C" | PARTIAL |

## The Hunt Workflow

### Phase 1: Reconnaissance

1. **Find all `unsafe` blocks and `unsafe impl`s:**
   ```bash
   rg 'unsafe\s*(fn|impl|{|\{)' --type rust -n
   ```

2. **Find all `unsafe` trait implementations:**
   ```bash
   rg 'unsafe\s+impl\s+(Send|Sync)' --type rust -n
   ```

3. **Find transmute / pointer casts / raw pointer derefs:**
   ```bash
   rg '(transmute|transmute_copy|from_raw|into_raw|as_ptr|as_mut_ptr|offset|add|sub|read|write|copy|ptr::null)' --type rust -n
   ```

4. **Find FFI boundaries:**
   ```bash
   rg 'extern\s+"C"' --type rust -n
   ```

5. **Count and catalog.** Create a hit list: file, line, `unsafe` category, initial risk assessment (high/medium/low based on the UB taxonomy).

### Phase 2: Miri Sweep (THE CRITICAL PHASE)

Run Miri with escalating strictness. **Do not skip any level.**

**Level 1 — Default (Stacked Borrows):**
```bash
cargo +nightly miri test 2>&1
```

**Level 2 — Strict Provenance + Symbolic Alignment:**
```bash
MIRIFLAGS="-Zmiri-strict-provenance -Zmiri-symbolic-alignment-check -Zmiri-backtrace=full" \
  cargo +nightly miri test 2>&1
```

**Level 3 — Full Paranoia (the audit standard):**
```bash
MIRIFLAGS="\
  -Zmiri-strict-provenance \
  -Zmiri-symbolic-alignment-check \
  -Zmiri-preemption-rate=0.1 \
  -Zmiri-backtrace=full \
  -Zmiri-disable-isolation" \
  cargo +nightly miri test 2>&1
```

**Level 4 — Tree Borrows (second model confirmation):**
```bash
MIRIFLAGS="\
  -Zmiri-tree-borrows \
  -Zmiri-strict-provenance \
  -Zmiri-symbolic-alignment-check \
  -Zmiri-preemption-rate=0.1 \
  -Zmiri-backtrace=full \
  -Zmiri-disable-isolation" \
  cargo +nightly miri test 2>&1
```

**Interpret results:**
- Fails at Level 1 → Definite UB. Fix immediately.
- Passes Level 1, fails Level 2 → Provenance or alignment UB. Fix.
- Passes Levels 1-3, fails Level 4 → Tree Borrows found something Stacked Borrows missed (unusual). Investigate — may be a Tree Borrows false positive, but usually indicates fragile aliasing.
- Passes all 4 → Miri-clean. Proceed to supplementary tools.

### Phase 3: Supplementary Scans

For code Miri cannot fully cover:

**Concurrent code with custom atomics:**
```bash
RUSTFLAGS="--cfg loom" cargo test --lib --release -- loom_tests 2>&1
```

**FFI-heavy code:**
```bash
RUSTFLAGS="-Zsanitizer=address" cargo +nightly test -Zbuild-std --target $(rustc -vV | rg host | awk '{print $2}') 2>&1
```

**Untrusted input parsing:**
```bash
cargo +nightly fuzz run <target> -- -max_total_time=300 2>&1
```

### Phase 4: Fix-and-Prove Loop

For each UB finding:

1. **Classify** against the 14-category taxonomy.
2. **Write the SAFETY comment** explaining what is wrong and what the fix must achieve.
3. **Apply the minimal fix.** Do not refactor — fix the UB and nothing else.
4. **Run Miri (Level 3 minimum) on the specific test that triggered the UB.**
5. **Run Miri (Level 3) on the full test suite** to check for regressions.
6. **Document the bead:**
   ```
   BEAD: [Category #] [Short description]
   FILE: [path:line]
   ROOT CAUSE: [one sentence]
   FIX: [one sentence]
   PROOF: Miri Level [N] pass — [command used]
   ```

### Phase 5: Hardening (Post-Fix)

After all beads are resolved:

1. **Add Miri to CI** if not already present (see [miri-sanitizers-loom.md](miri-sanitizers-loom.md) for the GitHub Actions config).
2. **Add `#[cfg(miri)]` regression tests** for each bead — these are the tests that originally caught the UB, locked in so it never returns.
3. **Review SAFETY comments** on every remaining `unsafe` block. Each must name the specific invariant from the taxonomy.
4. **Run the full paranoia sweep one final time** to confirm clean.

## Miri-First Decision Protocol

When the agent encounters `unsafe` code during ANY Rust task (not just audits):

```
Is there unsafe code in the changeset?
  YES → Run Miri Level 1 before proceeding.
  │     Miri fails?
  │       YES → Stop. Classify. Fix. Prove. Then continue.
  │       NO  → Run Miri Level 2 (strict provenance).
  │             Miri fails?
  │               YES → Stop. Classify. Fix. Prove. Then continue.
  │               NO  → Proceed with the original task.
  NO → Proceed normally.
```

This is not optional. **Every `unsafe` block gets Miri'd before it ships.**

## SAFETY Comment Standard

Every `unsafe` block requires a SAFETY comment within 5 lines above it. The comment must:

1. **Name the UB category** it could trigger (from the taxonomy).
2. **State the invariant** that makes this safe.
3. **Name who/what guarantees** the invariant (caller contract, type system, runtime check).

```rust
// SAFETY: [Category 4 — Uninitialized Memory]
// All N elements have been written to via `ptr::write` in the loop above.
// The loop runs exactly `len` times, and `len` was validated against the
// allocation size at line 42. MaybeUninit::assume_init is therefore sound.
unsafe { buf.assume_init() }
```

Bad SAFETY comments that must be rejected:
- `// SAFETY: we know this is safe` — Says nothing.
- `// SAFETY: this is fine because we tested it` — Testing does not prove absence of UB.
- `// SAFETY: the caller ensures correctness` — Which invariant? What is the contract?
- No SAFETY comment at all — Immediate failure.

## Audit Report Format

When completing a UB audit, produce a summary:

```markdown
## UB Audit Report

**Scope:** [crate/module/file]
**Miri version:** [output of `cargo +nightly miri --version`]
**Date:** [date]

### Findings

| # | Category | File:Line | Severity | Status |
|---|----------|-----------|----------|--------|
| 1 | Aliasing | src/buf.rs:42 | High | Fixed (Bead #1) |
| 2 | Uninit | src/ffi.rs:98 | High | Fixed (Bead #2) |

### Beads

#### Bead #1: Aliasing violation in buffer resize
- **Root cause:** `&mut` created while `&` to same slice existed
- **Fix:** Restructured to drop shared ref before taking mutable
- **Proof:** `cargo +nightly miri test -- test_buffer_resize` passes Level 3

### Miri CI Status
- [ ] Miri added to CI (Level 2 minimum)
- [ ] All SAFETY comments reviewed
- [ ] Regression tests added for each bead
```

## Common Fix Patterns

### Aliasing → Use `UnsafeCell` or restructure borrows
```rust
// BEFORE (UB: &mut while & exists)
let ptr = slice.as_ptr();
let mut_ref = &mut slice[0];  // UB: ptr still usable

// AFTER
let mut_ref = &mut slice[0];
// ptr is never created / used across the mutable borrow
```

### Uninitialized → Use `MaybeUninit::write` + `assume_init`
```rust
// BEFORE (UB: mem::uninitialized)
let x: T = unsafe { std::mem::uninitialized() };

// AFTER
let x: T = unsafe {
    let mut uninit = MaybeUninit::<T>::uninit();
    uninit.write(initial_value);
    uninit.assume_init()
};
```

### Provenance → Use `expose_provenance` / `with_exposed_provenance`
```rust
// BEFORE (UB: provenance lost)
let addr = ptr as usize;
let recovered = addr as *const T;

// AFTER
let addr = ptr.expose_provenance();
let recovered = std::ptr::with_exposed_provenance::<T>(addr);
```

### Send/Sync → Remove manual impl, use PhantomData
```rust
// BEFORE (unsound)
unsafe impl Send for MyType {}

// AFTER — if MyType truly needs Send, prove it:
// SAFETY: [Category 9 — Send/Sync]
// MyType's only non-Send field is `*mut Buffer`. Access to the buffer
// is guarded by `self.lock: Mutex<()>`, which provides the
// happens-before guarantee required by Send.
unsafe impl Send for MyType {}
```

### FFI → Validate at boundary
```rust
// BEFORE (UB: null pointer from C becomes &T)
let result = unsafe { ffi_call() };

// AFTER
let raw = unsafe { ffi_call() };
let result = NonNull::new(raw).ok_or(Error::NullFromFfi)?;
```

## Activation

This skill activates when:
- The user requests a "UB audit", "miri sweep", "unsafe audit", "soundness check", "rustonomicon audit", "race hunt"
- The agent encounters `unsafe` code during a Rust task and needs to verify it
- Miri reports a failure and the agent needs to classify and fix it
- The user asks "is this sound?" about Rust code

**Miri is not optional. Miri is the proof. Ship nothing `unsafe` without Miri's blessing.**