When the Rust borrow checker says no, see why — it recomputes the compiler's Polonius relations and renders the exact chain of facts that produced your E0499/E0502 rejection as a navigable, source-mapped derivation trace. A trace, not a guess.

---

Rust's borrow checker rejects code with a verdict and two spans; you reconstruct the rest in your head. why-borrowck recomputes the Polonius outlives / loan-liveness relations that rustc's consumer API exposes and renders the exact chain of facts that produced the rejection (E0499 / E0502) as a navigable derivation trace — every node is a relation instance the solver actually computed, mapped to its source span. You walk the tree from the error back to the borrow that caused it, clicking each fact to jump to its line.

Existing visual tools — RustOwl, Flowistry, Aquascope — all explain programs that accept (they paint where values live and where borrows are valid). Nobody renders why a program was rejected at the level of the constraint graph. why-borrowck does.

A borrow-check rejection should be as inspectable as a type error in a good theorem prover.

What this is — and is not

• Is: a rustc driver + LSP server + VS Code extension that, for an E0499 ("cannot borrow as mutable more than once") or E0502 ("cannot borrow as mutable because also borrowed as immutable") rejection, shows the backward derivation reject → loan-live → origin-live + the outlives chain → loan issuance → the invalidating access, each node source-mapped.
• Is NOT a proof. It visualizes the relation instances the solver computed; it does not re-prove E0499 from first principles. Approximate nodes (the subset establishment chain) are labeled as such.
• It recomputes the Polonius model, not rustc's NLL. Polonius accepts strictly more programs than the borrow checker that actually shipped your error, so the two can disagree. When they do, why-borrowck lights a divergence flag and shows both verdicts — it never claims to be "the compiler's own truth."
• Scope is explicit: E0499 / E0502 / the loan-invalidation family only. Moves (E0382) and region-mismatch / placeholder errors are out of scope and surfaced as "not compared," never silently mishandled.

Requirements (read this first)

This is not a brew install tool. It links against rustc internals (rustc_borrowck::consumers, rustc_middle, rustc_driver, polonius_engine), which exist only on a pinned nightly with the rustc-dev + rust-src components. The driver and server therefore build only inside the provided dev container:

• Docker (to build the pinned-nightly container — the only supported build env for the rustc_private parts). The toolchain is nightly-2026-01-16; see rust-toolchain.toml.
• A host Rust toolchain (stable is fine) to run the fast pure-logic test loop and build the host-stable pieces (the LSP server, the divergence orchestrator).
• Node.js (for the VS Code extension client, if you want the editor UI).

The architecture is split so most of it is host-stable: all the borrow-check logic lives in a rustc_private-free library (src/lib.rs), and only the thin fact-extraction layer (whyborrowckc) needs the container.

Build & run

# 1. Fast pure-logic loop — host, stable Rust, no container. 89 tests incl. the
#    must-fail negative control (an accepting program can never produce a rejection).
cargo test --lib

# 2. Build the pinned-nightly container (the only env that can build the driver).
docker build -t why-borrowck-dev .

# 3. End-to-end through the REAL compiler, in the container: the derivation trace
#    (M3), then orphan rendering + the cache + the divergence flag (M4).
docker run --rm -v "$PWD":/work -w /work why-borrowck-dev \
  bash -c 'RUSTC_BOOTSTRAP=1 scripts/smoke_m3.sh && RUSTC_BOOTSTRAP=1 scripts/smoke_m4.sh'

# 4. The LSP server is rustc_private-free and host-stable. Smoke it end to end
#    (driver/rustc stubbed with REAL captured oracles — no nightly needed), 9 beats:
cargo build --features lsp --bin why-borrowck-lsp
./scripts/smoke_m5_lsp.sh

# 5. The VS Code extension client.
cd client && npm install && npm run compile   # then press F5 in VS Code to launch it

See DEMO.md for the guided walkthrough (the live trace, the cache-hit beat, and the divergence honesty beat).

The proof — why you can trust the trace

A faithfulness tool with no oracle is worthless, so the trace is checked, not asserted:

• A differential suite asserts the generated trace matches hand-checked expectations for textbook E0499/E0502 snippets (fixtures/), through the real compiler.
• A must-fail negative control: an accepting program must produce exactly an accept node and no rejection trace. A Reject node can only ever be built by iterating the solver's recomputed Output.errors — so the tool is structurally unable to invent a rejection. This is enforced at every layer (the trace builder, the position query, the LSP response) and re-run live in the smoke suites.
• The verdict cannot drift from the explanation: the boolean accept/reject verdict is flattened from the trace tree, never set beside it — so the explanation and the decision cannot disagree.

The flagship honesty case (fixtures/divergence_case3.rs) is a program where Polonius accepts what rustc's NLL rejects — proven live: the divergence flag lights and both verdicts are shown.

How it works (one breath)

whyborrowckc runs as a RUSTC_WORKSPACE_WRAPPER, overrides the mir_borrowck query (adapting RustOwl's driver shape), recomputes Polonius keeping Output.errors (which RustOwl discards), walks the loan-liveness + subset relations backward from a recorded error to the invalidating access, and emits the result as a $-tagged ReadingNode tree (one JSON line per body). The rustc_private-free why-borrowck-lsp server runs that driver plus plain rustc, and serves whyborrowck/explain {uri, position} → an ExplainResponse (the covering trace + flattened verdict + model: polonius-datafrogopt banner + divergence flag). The VS Code client renders it as an expandable tree, click-to-reveal-span.

Repo map

README.md            ← this file
DEMO.md              ← guided walkthrough (what to run, what you see, why it's honest)
CONTRIBUTING.md      ← the load-bearing discipline (negative controls, scope, the container loop)
LICENSE              ← MIT
Dockerfile           ← the pinned-nightly build container (mandatory for the driver/server)
rust-toolchain.toml  ← pins nightly-2026-01-16 + rustc-dev / rust-src
src/
  lib.rs             ← the rustc_private-FREE borrow-check brain (trace builder, cache,
                       divergence, LSP response logic) — host-stable, the fast test loop
  bin/
    whyborrowckc.rs        ← the parasitic rustc driver (needs the container)
    why_borrowck_lsp.rs    ← the LSP server (host-stable; `--features lsp`)
    divergence.rs          ← the Polonius-vs-NLL cross-check orchestrator
    m0_errors_probe.rs     ← the load-bearing `Output.errors` validation probe
    m3_facts_probe.rs / m4_hash_probe.rs  ← investigation tools
client/              ← the thin VS Code TreeView extension (TypeScript)
fixtures/            ← E0499/E0502 + chain/orphan/divergence test programs
tests/fixtures_captured/  ← captured real driver + rustc oracles (host-stable test ground truth)
scripts/             ← the smoke suites (M1–M5) + the LSP test clients
docs/
  spec.md            ← what & why (the canonical spec)
  design.md          ← how it works (architecture, the as-built notes)
  prior-art.md       ← prior art & how this differs (the honest comparison)
STATUS.md            ← current build state, how to verify, known limitations

Contributing

See CONTRIBUTING.md. The one non-negotiable: every correctness test ships a must-fail negative control, and the headline proof (the negative control + the divergence flag) must re-pass before merge.

License

MIT — see LICENSE.