fold/docs/architecture/production-reachability.md

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.