# Production reachability evidence

Fold's whole-program reachability lane is distinct from translation-unit
`unused-function`, local `dead`, and CFG-only `unreachable` analysis. It uses
versioned, TU-owned graph contributions and linkage-aware semantic USRs.

## Root inventory

Each parsed translation unit contributes evidence for:

- executable `main` definitions;
- explicit entrypoints from a versioned configuration profile (USR or qualified
  name; ambiguous qualified names conservatively match every overload);
- explicitly exported ABI functions (`extern "C"`, default visibility, or
  platform export attributes);
- functions invoked by static initializers;
- function addresses passed as callbacks or otherwise escaping;
- concrete-class virtual methods, retained as conditional candidates until
  reachable construction and target closure are established;
- test, benchmark, example, and third-party entrypoints, retained separately
  from production roots.

Root records preserve the function USR, owning source, evidence location, root
kind, production/test domain, and whether activation is conditional. They are
persisted transactionally with the owning TU. Warm graph assembly reuses them;
source/header/flag/profile/schema changes invalidate them with the rest of the
contribution.

## Proof boundary

Root discovery does not itself classify or delete code. The inventory is
closed-world only when:

- every explicit root selector resolves;
- persisted rows pass schema and enum validation; and
- no unresolved virtual or indirect callsite remains.

Missing selectors and unresolved dynamic calls are coverage failures, never
proof that a function is dead. Exported ABI functions and escaped callbacks are
conservative roots. Virtual candidates require the guarded reachability phase
to establish that a concrete owner is instantiated from a reachable path.

Profile telemetry reports bounded counts for production, test, conditional, and
unresolved explicit roots plus the closed-world flag. It does not emit selectors
or source expressions.

## Guarded classification

Enable the project pass with `--detectors production-reachability` (also part of
`quality` and `dead-code`). Fold forces this detector through one in-process,
whole-project graph rather than merging unsound per-worker classifications.
Guarded callsites sharing a caller and target are alternatives: their guards are
ORed, never ANDed.

The classifier uses bounded Z3 reachability constraints with a strictly
increasing path distance. This prevents a disconnected recursive SCC from
proving itself reachable. It evaluates paths under profile assumptions and with
configuration symbols existentially free, then assigns one mutually exclusive
class:

- `production-reachable`: a production-root path is feasible, or conservative
  evidence prevents a stronger conclusion;
- `test-only`: reachable from test roots but not production roots in a closed
  graph;
- `default-inactive`: infeasible under the supplied profile but feasible under
  another configuration;
- `configuration-infeasible`: structurally connected but UNSAT for all modeled
  configurations;
- `unreachable-production`: disconnected from production and test roots in a
  closed graph;
- `compile-variant-absent`: reserved for explicit finite variant manifests and
  never inferred from one compile database.

Unknown guards are treated as feasible. Solver timeout, budget exhaustion,
unresolved selectors or dispatch, missing roots, conditional virtual roots, and
escaped functions produce conservative `production-reachable` records with
blockers. A reachability-only scan may reuse direct-edge TU contributions when
unresolved callsites remain, but it preserves `closed_world=false`, performs no
solver queries, and emits no removal candidate. Other graph consumers retain
the exhaustive fallback. SAT or UNKNOWN never becomes a removal candidate.
Only a complete,
closed-world `unreachable-production` record sets `removal_candidate=true`;
`test-only`, `default-inactive`, and `configuration-infeasible` remain review
evidence.

The detector emits function-level `production-reachability` findings with a
stable semantic identity and structured native-JSON/SARIF evidence. It does not
emit branch/callsite findings and therefore does not duplicate local
`branch-infeasible`, `dead-statement`, or `always-condition` results. Source
locations remain absent when the persisted graph has only semantic identity and
source-file provenance; Fold does not fabricate line numbers.