# Auditing Guide

Files that human reviewers should examine for safety-critical code.

## Safety Model

- **`src/tokens/mod.rs`** — `SimdToken` trait (the core safety contract), `forge_token_dangerously()`, `CompileTimeGuaranteedError`, `IntoConcreteToken` dispatch

## Generated Token Implementations

All generated from `token-registry.toml` via `cargo xtask generate`.

- **`src/tokens/generated/x86.rs`** — x86 V2/V3 tokens: runtime detection via `is_x86_feature_detected!`, atomic caching, `forge_token_dangerously()`, disable mechanism with cascading
- **`src/tokens/generated/x86_avx512.rs`** — AVX-512 tokens (V4, Modern, Fp16): same pattern, gated on `feature = "avx512"`
- **`src/tokens/generated/arm.rs`** — AArch64 tokens: runtime detection via `is_aarch64_feature_detected!`, same caching/disable pattern
- **`src/tokens/generated/wasm.rs`** — WASM token: compile-time only (no runtime detection on wasm32)

## Generated Stubs

Cross-platform stubs where `summon()` always returns `None`.

- **`src/tokens/generated/x86_stubs.rs`** — x86 stubs (used on ARM/WASM)
- **`src/tokens/generated/x86_avx512_stubs.rs`** — AVX-512 stubs
- **`src/tokens/generated/arm_stubs.rs`** — ARM stubs (used on x86/WASM)
- **`src/tokens/generated/wasm_stubs.rs`** — WASM stubs (used on x86/ARM)

## Macro Safety

- **`archmage-macros/src/lib.rs`** — `#[arcane]` generates `#[target_feature(enable = "...")]` inner function + `unsafe` call. `#[rite]` is similar but for internal helpers. The unsafe call is sound IFF the token proves the features are available.

## Code Generators

- **`xtask/src/token_gen.rs`** — Generates all token structs, `SimdToken` impls, detection logic, disable mechanism, and cascading. Wrong code here = wrong safety guarantees everywhere.
- **`xtask/src/registry.rs`** — Parses and validates `token-registry.toml`. Validates feature set consistency.

## Source of Truth

- **`token-registry.toml`** — Defines every token's feature set, trait memberships, and hierarchy. If a feature is missing here, the generated `#[target_feature]` won't include it, and LLVM won't use the corresponding instructions. If an extra feature is listed, the token will demand more than necessary (safe but overly restrictive).

## Verification Tests

- **`tests/miri_safe.rs`** — Miri-clean tests for token creation, disable, and basic operations
- **`magetypes/tests/miri_boundary_tests.rs`** — Miri tests for SIMD type boundary conditions
- **`tests/token_infrastructure.rs`** — Comprehensive token system tests: `compiled_with()`, `summon()`, disable/cascading, `CompileTimeGuaranteedError`, feature flag strings

## Counterexample

- **`examples/unsafe_counterexample.rs`** — Educational example demonstrating what happens when you bypass the safety system with `forge_token_dangerously()`

## What to Look For

1. **Every `unsafe` block** in generated code calls `forge_token_dangerously()`. Verify the safety justification: a token parameter proves runtime detection occurred.
2. **Feature lists** in `token-registry.toml` must match LLVM's x86-64 microarchitecture levels. Missing features = potential UB (code uses instructions the CPU might not have).
3. **`#[target_feature]` strings** generated by `#[arcane]` macro must match the token's feature set. The macro reads from `archmage-macros/src/generated/registry.rs`.
4. **Disable cascading** must go parent → all descendants. If V3 is disabled but V4 isn't, code could forge a V4 token that implies V3 features on a CPU that lacks them.
5. **Stubs** must never return `Some` from `summon()`. A stub returning a token on the wrong architecture = instant UB.
