Repository navigation
Wiring-liveness wave-2(b): fn-arrow reflection builtin + corpus-wide lens coverage - #5722
Merged
Merged
Conversation
…lens coverage Adds fn/arrow corpus reflection (the gunbc#5364 widen trigger) and wires it into the wave-1 wiring-liveness lens so a declared fn parameter with no path to its output fails the floor -- proven green-by-execution over the live closure and red-on-perturbation. - v2.std.fn_index.fn_arrow_decl_facts_live: host SOURCE reflection (sibling of concept_decl_facts_live, ItemKind::FnItem/FuncItem) yielding one FnArrowDecl per fn -- body projected to a reachability skeleton (param references become identity Atom leaves, all else neutral Conj containers) + declared param atoms. Excludes generic type-parameters (self-named type-expr) and _-prefixed declared-inert params; resolves fn-valued params used as call callees (ExprCall node name, not a child). - v2.lens.wiring_liveness: corpus fold reusing std.dependency DependencyView/dependency_lens/ready_set (no new dependence type) -- a param is wired iff reachable from the body output. - Floor witness wiring_liveness_corpus_test with no-host-enumeration controls and synthetic dead-wire discrimination. - Declared the two NodeFold-step ignored edge params inert (_edge) per the existing node.dag convention. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Wiring-liveness wave-2(b): fn-arrow reflection + corpus-wide lens coverage
Closes the wave-1 lens's honest boundary — "the corpus has NO fn/arrow reflection ... a corpus-wide scan of real fn params is opaque today" — by landing the gunbc#5364 widen trigger: a fn/arrow corpus-reflection builtin wired into
v2.lens.wiring_livenessso a declared fn parameter with no path to its output fails the floor. Builds on wave-1 (#5679); does not fork its kernel.What lands
v2.std.fn_index.fn_arrow_decl_facts_live— host SOURCE reflection (sibling ofconcept_decl_facts_live, butItemKind::FnItem/FuncItem). Yields oneFnArrowDecl{qualified_name, name, output, params}per declared fn: the body projected to a reachability skeleton (parameter references → identityAtomleaves, everything else → neutralConjcontainers) plus the declared parameter atoms. Bridge wired inv1_interpreter.rs(STD_FN_INDEX_BRIDGE_FNS/is_v4_std_fn_index_bridge_call), conformance-checked.v2.lens.wiring_livenesscorpus fold —wiring_dead_wires_over/wiring_liveness_corpus_is_clean. Reusesstd.dependencyDependencyView/dependency_lens/ready_set(no new dependence type — that re-coining is what sank the duplicate Wiring-liveness lens wave 1: dependence carrier + wired floor witness #5702). A parameter is wired iff reachable from the body output; the per-fn reachable set is computed once viaready_set(linear), not per-parameter saturation (quadratic).wiring_liveness_corpus_test.dag(auto-enrolled) — with no-host-enumeration controls (locally-authored probe fns must appear in the enumeration, proving the read axis by execution) and a synthetic dead-wire discrimination control.Soundness (three corrections found by running it over the live corpus)
item.paramsisconcat(type_params, value_params)— generic type-params (T,K,V) are not value inputs; excluded via their self-named type-expr (T : T).predicate(x)) is stored as the call node's name, not a child — the marshaller now emits the atom forExprVarreads andExprCallcallees.NodeFoldstep's ignorededge) are declared inert via the existing_-prefix convention (node.dagstep: fn(acc, _edge, sub)); the reflection skips_-prefixed params. The two such params independency.dagare renamed_edge(plan §4).Proven by execution (not typecheck + grep)
claim_batchover--source-root dsl --source-root src/v2: GREEN (dead-wire count 0) → un-declare one inert param (_edge→edge) → RED (floor FAILs) → revert → GREEN. Wave-1's three witnesses and the bridge conformance test still pass.Honest scope
Coverage is the witness's resolve closure (the floor resolves per-entry closures), same as
concept_decl_facts_livetoday. Whole-tree widening lands with #5364's corpus-as-node accessor (ctx.modules= whole tree); this PR is its SOURCE half. The opaque Rust-seedresolve_authrealization remains the separate wave-2 perturbation witness.🤖 Generated with Claude Code