/unsafe-review                           # Audit all unsafe in the codebase
/unsafe-review @src/engine/hit_pool.rs   # Audit specific file
/unsafe-review @src/runtime.rs:450-530   # Audit specific line range

/unsafe-review @target
    │
    ├─ Phase 1: Discovery & Inventory
    │   └─ Find every unsafe block/fn/impl in scope, classify each
    │
    ├─ Phase 2: Safety Invariant Audit (parallel per file)
    │   └─ For each unsafe block: check documented invariants, verify they hold
    │
    ├─ Phase 3: Performance Justification Audit
    │   └─ For each unsafe block: demand benchmark + ASM evidence
    │
    ├─ Phase 4: Test Coverage Audit (parallel agents)
    │   ├─ Agent A: Miri coverage check
    │   ├─ Agent B: Kani proof coverage check
    │   ├─ Agent C: Fuzz target coverage check
    │   └─ Agent D: Property test coverage check
    │
    ├─ Phase 5: Verdict & Gap Report
    │   └─ Per-block verdict, missing test list, action items
    │
    └─ Phase 6: Test Generation (if requested)
        └─ Write missing Miri tests, Kani proofs, fuzz targets, property tests

| # | File:Line | Category | Purpose (1-line) | Has Safety Comment | In Hot Path |
|---|-----------|----------|------------------|--------------------|-------------|
| 1 | hit_pool.rs:172 | block | Unchecked index into sorted array | Yes | Yes |
| 2 | hit_pool.rs:184 | block | ptr::copy_nonoverlapping for bulk move | No | Yes |

// GOOD ✓
// SAFETY: `idx` is bounded by `self.len` which is checked at line 165.
// The backing allocation is guaranteed to be at least `self.cap` elements
// by the constructor invariant (see `new()`).
unsafe { *self.ptr.add(idx) }

// BAD ✗
unsafe { *self.ptr.add(idx) }  // No safety comment

// BAD ✗
// SAFETY: this is safe because we know it works
unsafe { *self.ptr.add(idx) }  // Vacuous justification

// GOOD ✓ — minimal unsafe scope
let val = unsafe { *ptr.add(idx) };
process(val);  // safe code outside unsafe block

// BAD ✗ — unnecessary code inside unsafe block
unsafe {
    let val = *ptr.add(idx);
    process(val);        // This doesn't need unsafe
    log::debug!("{val}"); // Neither does this
}

### Block #N: file.rs:LINE

**Category**: [block | fn | impl | FFI | intrinsic]
**Purpose**: [one-line description]
**Safety comment**: [Present/Missing/Insufficient]
**Invariant claimed**: [what the safety comment says]
**Invariant verified**: [Yes — traced to LINE | No — EXPLAIN GAP]
**Scope minimal**: [Yes | No — EXPLAIN what can move outside]
**Status**: [SOUND | REVIEW | UNSOUND]

### Block #N: file.rs:LINE

**Benchmark coverage**: [bench_name — COVERED | NONE — needs benchmark]
**Safe alternative tried**: [Yes — git SHA / PR# | No — UNJUSTIFIED]
**Measured speedup**: [X% on bench_name | Unknown — UNJUSTIFIED]
**ASM evidence**: [bounds check eliminated / SIMD enabled / etc. | NONE]
**Hot path**: [Yes — appears in profiling | No — UNJUSTIFIED | FFI — exempt]
**Verdict**: [JUSTIFIED | UNJUSTIFIED | EXEMPT (FFI/Send/Sync)]

# Current Miri command (from CI):
cargo +nightly miri test --lib -- \
  --skip engine:: \
  --skip git_scan:: \
  --skip scheduler::affinity \
  --skip scheduler::device_slots \
  --skip scheduler::rusage \
  --skip scheduler::local_fs_uring \
  --skip scheduler::engine_impl \
  --skip scheduler::parallel_scan \
  --skip rules::yaml \
  --skip archive::

# Find existing Kani proofs
grep -rn '#\[kani::proof\]' src/ tests/

# List fuzz targets
ls fuzz/fuzz_targets/

# Find property tests
grep -rn 'proptest!' src/ tests/

## Test Coverage Matrix

| # | File:Line | Purpose | Miri | Kani | Fuzz | Proptest | Verdict |
|---|-----------|---------|------|------|------|----------|---------|
| 1 | hit_pool.rs:172 | unchecked index | ✓ | ✗ | ✗ | ✓ | GAPS |
| 2 | hit_pool.rs:184 | copy_nonoverlapping | ✓ | ✗ | ✗ | ✗ | GAPS |
| 3 | spsc.rs:45 | atomic load | ✓ (loom) | ✓ | ✗ | ✗ | OK |
| 4 | vectorscan.rs:317 | FFI call | SKIP(FFI) | N/A | ✓ | N/A | OK |

### Legend
- ✓ = Covered with meaningful test
- ✗ = Missing — needs test
- SKIP(reason) = Intentionally skipped with justification
- N/A = Not applicable for this unsafe category

# Unsafe Review Report: [scope]

**Date**: YYYY-MM-DD
**Reviewer**: Claude (automated)
**Scope**: [files reviewed]

## Summary

| Verdict | Count |
|---------|-------|
| APPROVED | N |
| APPROVED-FFI | N |
| NEEDS-TESTS | N |
| NEEDS-JUSTIFICATION | N |
| NEEDS-SAFETY-COMMENT | N |
| UNJUSTIFIED | N |
| UNSOUND | N |

## Critical Findings (UNSOUND / UNJUSTIFIED)

[List any blocks that need immediate attention]

## Detailed Audit

### File: src/engine/hit_pool.rs

#### Block #1: line 172 — `get_unchecked` in sorted lookup

**Safety**: SOUND — bounds proven by binary search result (line 168)
**Performance**: JUSTIFIED — 8.3% speedup in `hit_pool` bench (commit abc123)
**Tests**:
- Miri: ✓ (test_sorted_lookup exercises this path)
- Kani: ✗ MISSING — need proof that binary search result < len
- Fuzz: ✗ MISSING — no fuzz target reaches hit_pool
- Proptest: ✓ (prop_sorted_invariant in hit_pool_tests.rs)
**Verdict**: NEEDS-TESTS

**Action items**:
1. Add Kani proof: `verify_sorted_lookup_bounds`
2. Add fuzz target or extend existing target to reach this path

[... repeat for each block ...]

## Missing Test Summary

### Kani Proofs to Write
1. `verify_sorted_lookup_bounds` — hit_pool.rs:172
2. `verify_bulk_copy_nonoverlap` — hit_pool.rs:184

### Miri Tests to Write
1. `test_edge_empty_pool` — hit_pool.rs (exercises empty-pool unsafe path)

### Fuzz Targets to Write/Extend
1. `fuzz_hit_pool_accumulate` — new target for hit_pool adversarial input

### Property Tests to Write
1. `prop_copy_preserves_order` — hit_pool.rs:184 bulk move preserves sort

// Tests in this module are designed to be run under Miri for
// undefined behavior detection. Run with:
//   cargo +nightly miri test --lib module::tests::miri_
//
// Miri flags (match CI):
//   MIRIFLAGS="-Zmiri-strict-provenance -Zmiri-symbolic-alignment-check"

#[cfg(test)]
mod tests {
    use super::*;

    /// Exercises [unsafe operation] with [edge case description].
    /// Under Miri, this catches: [what Miri would detect].
    #[test]
    fn miri_edge_case_description() {
        // Setup: construct minimal state that reaches the unsafe path
        // Exercise: call the function with edge-case input
        // Verify: assert the result is correct
        // Miri implicitly checks: no UB, valid provenance, proper alignment
    }

    /// Boundary condition: [description]
    #[test]
    fn miri_boundary_description() {
        // ... tests at capacity limits, zero-size, max-size
    }
}

#[cfg(kani)]
mod verification {
    use super::*;

    /// Proves [unsafe operation] cannot cause [UB type].
    /// Covers: [input domain description]
    #[kani::proof]
    #[kani::unwind(N)]  // Set to max loop iterations + 1
    fn verify_operation_safety() {
        let size: usize = kani::any();
        kani::assume(size <= MAX_REASONABLE_BOUND);

        // Construct the data structure
        // Perform the operation
        // Kani proves no panics, no UB, no out-of-bounds
    }

    /// Proves [invariant] holds for all valid inputs.
    #[kani::proof]
    fn verify_invariant_name() {
        // Use kani::any() for symbolic inputs
        // Use kani::assume() to constrain to valid domain
        // Assert the invariant
    }
}

// fuzz/fuzz_targets/fuzz_<component>.rs
#![no_main]
use libfuzzer_sys::fuzz_target;
use arbitrary::Arbitrary;

/// Fuzz target for [component] unsafe operations.
/// Exercises: [list of unsafe paths reached]
///
/// Run: cargo +nightly fuzz run fuzz_<component> -- -max_len=4096
#[derive(Arbitrary, Debug)]
struct FuzzInput {
    // Structured input that exercises the unsafe paths
    // Use Arbitrary derive for automatic generation
}

fuzz_target!(|input: FuzzInput| {
    // Construct component from fuzz input
    // Exercise the operations that contain unsafe
    // No explicit asserts needed — fuzz catches panics and UB (with sanitizers)
});

[[bin]]
name = "fuzz_<component>"
path = "fuzz_targets/fuzz_<component>.rs"

#[cfg(all(test, feature = "stdx-proptest"))]
mod prop_tests {
    use super::*;
    use proptest::prelude::*;

    /// Property: [invariant description]
    /// Exercises unsafe path at [file:line] through safe API.
    proptest! {
        #[test]
        fn prop_invariant_name(input in strategy()) {
            // Exercise through safe public API
            // Assert the invariant that the unsafe code relies on
            // e.g., roundtrip, bounds preservation, ordering
        }
    }

    /// Property: [description] — specifically targets edge cases
    /// for the unsafe operation at [file:line].
    proptest! {
        #[test]
        fn prop_edge_case_name(
            size in 0usize..=MAX_CAP,
            idx in 0usize..=MAX_CAP,
        ) {
            prop_assume!(idx < size);
            // Test the operation at various sizes and indices
        }
    }
}

# Run Miri on a single module's tests
MIRIFLAGS="-Zmiri-strict-provenance -Zmiri-symbolic-alignment-check" \
  cargo +nightly miri test --lib <module>::tests

# Run Miri on a specific test
MIRIFLAGS="-Zmiri-strict-provenance -Zmiri-symbolic-alignment-check" \
  cargo +nightly miri test --lib <module>::tests::miri_test_name

# Run a single Kani proof
cargo kani --features kani --harness verify_proof_name

# Run all proofs in a module
cargo kani --features kani --module module_name

# Short fuzz run to verify target compiles and finds no immediate crashes
cargo +nightly fuzz run fuzz_target_name -- -max_total_time=30

# All Miri tests (matching CI)
MIRIFLAGS="-Zmiri-strict-provenance -Zmiri-symbolic-alignment-check -Zmiri-preemption-rate=0.1 -Zmiri-disable-isolation" \
  cargo +nightly miri test --lib -- \
    --skip engine:: --skip git_scan:: --skip scheduler::affinity \
    --skip scheduler::device_slots --skip scheduler::rusage \
    --skip scheduler::local_fs_uring --skip scheduler::engine_impl \
    --skip scheduler::parallel_scan --skip rules::yaml --skip archive::

# All Kani proofs
cargo kani --features kani

# All property tests
cargo test --features stdx-proptest

## Unsafe Review Checklist

### Safety
- [ ] Every `unsafe` block has a `// SAFETY:` comment
- [ ] Every claimed invariant is traced to its enforcement point
- [ ] Unsafe scope is minimal (no safe code inside unsafe blocks)
- [ ] No undefined behavior paths identified

### Performance Justification
- [ ] Benchmark exists covering this unsafe code path
- [ ] Safe alternative was benchmarked and is measurably slower
- [ ] ASM diff shows concrete codegen improvement (e.g., bounds check eliminated)
- [ ] Speedup is significant enough to justify the maintenance cost

### Test Coverage
- [ ] Miri: Tests exercise this unsafe path with strict provenance + alignment checks
- [ ] Kani: Formal proof covers the safety-critical invariant
- [ ] Fuzz: Target reaches this code with adversarial inputs (or justification for skip)
- [ ] Proptest: Property test verifies the invariant through the safe public API
- [ ] Edge cases: Empty input, zero-size, max capacity, boundary values tested

### Documentation
- [ ] Safety invariants documented in `// SAFETY:` comments
- [ ] Performance justification documented (benchmark results, ASM evidence)
- [ ] Test coverage documented (which tests verify which unsafe blocks)