Wiring-liveness lens wave 1: reachability kernel + wired floor witness

[gunbai-bot]

Wave 1 of the wiring-liveness oracle (ROADMAP §4; authority = the merged plan carrier dsl/gunbc/plans/wiring_liveness_preflight.dag, #5664). The spine: the input→output dependence kernel + a fail-closed floor witness, proven green-by-execution and red-on-perturbation.

The principle

Wiring-liveness is the cache-purity perturbation oracle read backwards:

• purity (caching): same input ⇒ same output — a declared input absent from the cache key is impure.
• liveness (wiring): different input ⇒ different output — a declared input with no structural path to the output it feeds is a dead wire.

One kernel, two readings (DESIGN §2-horizontal). Reuses std.dependency DependencyView/dependency_lens as the dependence carrier — no new dependence type minted. Distinct from unused_parameters: that asks referenced ≥1×; this asks transitive path to an output (RED when an input is referenced only inside structure that itself never reaches the output).

What landed

• v2.lens.wiring_liveness — forward transitive reachability over the DependencyView graph; WiringRelation / WiringVerdict = Wired | Unwired verdict carrier.
• src/v2/lens/wiring_liveness_test.dag — three positive test fns (true-when-correct, red-on-revert), floor-discovered like the landed inert_carrier_test.dag:
  • wiring_liveness_wired_input_reaches_output — wired synthetic tree (via real dependency_lens) ⇒ Wired. Proven RED when the subject wire is cut.
  • wiring_liveness_dead_input_is_unwired — a declared input disconnected from the output ⇒ Unwired. Proven RED when the lens goes lenient-always-Wired (no fabricated-green).
  • wiring_liveness_real_reflected_type_field_reachable — real-corpus: reflects a live type via resolve_type_node and runs the same kernel over its real dependence graph.

Discrimination (the operator's explicit ask — verified by execution)

perturbation	test that goes RED
subject wire cut (input no longer reaches output)	…wired_input_reaches_output → false
lens made lenient (always Wired)	…dead_input_is_unwired → false (wired test stays green = control)

The two positive tests pin the kernel from both sides.

Honest boundary (DESIGN §5/§6 — stated in the lens construction_justification)

This is the compile-time wall and covers only .dag-modeled / reflectable structure. The motivating GCP IAM auth_input bug lives in the Rust-seed resolve_auth realization — opaque to compile-time reflection = the wave-2 opaque-realization witness, not this slice. The corpus also has no fn/arrow/service-operation reflection (resolve_type_node + concept_decl_facts_live yield only ItemKind::TypeItem), so wiring_liveness_real_reflected_type_field_reachable is a real-DATA kernel smoke over type-dependence (proves the kernel runs on live reflected structure, not inert), not "covers real wiring bugs." WIDEN trigger: realization self-host (§5/§7) + gunbc#5364 (.dag fn reflection) — the lens widens to real fn/operation corpus coverage when fn reflection lands.

🤖 Generated with Claude Code

[gunbai-bot]

Thanks — both findings addressed in 9174fb7 (both valid, both fixed):

1. WiringVerdict Bool-isomorphic — flattened. Dropped WiringVerdict = Wired | Unwired + wiring_verdict_is_wired; wiring_relation_is_wired now returns Bool directly. Kept WiringRelation (3-field dependence bundle, not Bool-isomorphic). A richer verdict re-enters when the plan's declared-inert vs dead-wire 3rd state actually lands (model just-in-time, so it carries info Bool can't at that point) — flattening now avoids the clone-the-wrapper risk you flagged.
2. No convergence early-exit — added. wiring_reach_saturate now folds a WiringReachState { reached, stable } with a stop-when-the-reached-set-stops-growing short-circuit, faithfully mirroring the affected_set closure fixpoint it was modeled on (which I'd cited but hadn't fully reused). Worst-case is still inherent to list-based reachability, but it no longer runs dead passes after convergence.

Re-verified by execution (claim_batch): all 3 witnesses green; two-sided discriminating pin intact (lenient lens ⇒ dead-input RED; strict lens ⇒ wired RED).

— sent from nimble-ibex-318