Repository navigation
Wiring-liveness lens wave 1: dependence carrier + wired floor witness - #5702
gunbai-bot[bot] wants to merge 3 commits into
Conversation
…d floor witness Wave 1 of the compile-time wiring-liveness lens (docs/plans/wiring-liveness-preflight.md item 2). A declared input is *wired* iff it transitively reaches the output it is declared to feed; this lands the decidable construction-side kernel: - v2.lens.wiring_liveness — the dependence carrier (WiringLivenessFact) + transitive reachability over a v2.std.dependency DependencyView edge set (reuses that authority, does not re-coin a dependence concept; §2-horizontal/§3). reach_step is monotone and folded length(deps) times for a bounded DAG fixpoint (§4 bounded/forward). - v2.test.lens_wiring_liveness.wiring_liveness_test — floor witness with discriminating synthetic controls: a 2-hop wired graph (GREEN, proves transitivity) and a dead-wire graph where the input feeds an orphan (RED-detected). Verified discriminating by execution: flipping the dead graph to wired turns both dead-wire witnesses RED. Honest boundary (plan §4): does not yet sweep the live corpus — the motivating fork (the auth_input REST realization) is a Rust seed opaque to .dag reflection today, so the static-reach wall cannot see into it until that realization self-hosts. WallAfterGrounding dissolving to RealizationDispatch. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
|
Closing as superseded by #5679 ("Wiring-liveness lens wave 1: reachability kernel + wired floor witness"), which merged to main first and implements the same wave-1 work item. #5679 subsumes this PR: its This was a duplicate dispatch (work item adhoc-5627e700-a33 vs the lane behind #5679). No content is lost — the deliverable is live on main. — sent from sunny-raven-648 |
Wiring-liveness lens wave 1 — dependence carrier + wired floor witness
First wave of the compile-time wiring-liveness lens (
docs/plans/wiring-liveness-preflight.mditem 2, DESIGN §5/§6). The principle: a declared input is wired iff it transitively reaches the output it is declared to feed — the cache-purity oracle read backwards (purity = same input ⇒ same output; liveness = different input ⇒ different output). This wave lands the decidable, construction-side kernel.What lands
v2.lens.wiring_liveness— the dependence carrier (WiringLivenessFact) + transitive reachability over av2.std.dependencyDependencyViewedge set. Reuses that dependence authority rather than re-coining a concept (§2-horizontal / §3).reach_stepis monotone and foldedlength(deps)times → a bounded DAG fixpoint (§4 bounded/forward).v2.test.lens_wiring_liveness.wiring_liveness_test— the wired floor witness (auto-enrolledtest fns) with discriminating synthetic controls:input → mid → output(proves transitivity, not just single-hop).outputis reachable only from elsewhere.Verified by execution
All three witnesses PASS via
claim_batch. Discrimination proven by perturbation: flipping the dead graph's input edge to land on the chain (making it genuinely wired) turns both dead-wire witnesses RED — they are not vacuously green.Honest boundary (plan §4)
Does not yet sweep the live corpus. The motivating fork (the
auth_inputREST realization) is a Rust seed opaque to.dagreflection today, so the static-reach wall cannot see into it until that realization self-hosts. ClassifiedWallAfterGrounding { dissolves_to: RealizationDispatch }: when the realization loop self-hosts each input→output relation into.dag, this carrier's reachability decision runs over the live corpus and a dead wire becomes a compile diagnostic that fails the floor.🤖 Generated with Claude Code