Repository navigation
Dependency-fidelity: §6 wall caught an unsound input-reachability enrollment on real code (finding + receipt) - #6584
Merged
Merged
Conversation
Reviewer (claude-opus-4-7 APPROVE) flagged FidelitySurface as declared with no producer/consumer — speculative dead scaffold (DESIGN §5 wall-now / §2 don't grow concepts ahead of a consumer). The §3 surface is already implicit in the FidelityDiscrepancy variant (input/output/interaction), and the design doc holds the three-surface concept, so the enum earned no place yet. Reintroduce with a consumer when the output-reachability / interaction arms land. Witnesses still green (clean_input_surface_is_faithful, one_unused_param_flips_to_discrepant). Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
…imitive
The coverage side of the §7 engine. Coverage of a relationship R = the witness
set such that every one-step mutation of R's declared structure is KILLED. This
lands the adequacy verdict grounded on v2.lens.discrimination's authority for
"killed" (a mutation's discriminating_unit is killed iff unit_is_discriminating
holds — a green plus a perturbed red), so "killed" is not re-minted (§3). A
surviving mutation is a located coverage hole (Inadequate{survivors}).
Mutation enumeration from a declared structure (DependencyView one-step
neighbors) is the staged producer this verdict feeds (§4/§7).
Green by execution (local claim_batch):
- adequate_when_every_mutation_has_a_discriminating_witness — real discriminating
unit (green CompilesClaim + perturbed-input red DiagnosticClaim) → PASS
- surviving_mutation_is_inadequate — non-discriminating Empty unit → survivor → PASS
A discriminating pair exercising the real unit_is_discriminating grounding both
directions. inert-lens hygiene green (module reached by its witness).
Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
…ecord the finding
Attempted to enroll input-reachability as a live tree-lens over the corpus
(run unused_parameters over each FnArrowDecl). It was green on synthetic tests
but flagged FALSE POSITIVES the moment it ran over real compiled fns — the
mature unused_parameters lens flagged its own module. Root cause: FnArrowDecl is
{ output: Node, params: List<FnArrowParam> } — output is the return node only;
params are a separate field. Feeding dependency_lens(decl.output) to a parameter
analyzer analyzes the wrong tree. This is the §1 keystone lesson on our own code:
synthetic-green lies where a lens is fed the wrong real input; only running over
real code exposes it (DESIGN §5/§6).
Removed the unsound v2.lens.dependency_fidelity_corpus (never landed a gate that
false-positives). Recorded the finding + the sound path (param-aware full-arrow
feed; per-module run is fast at ~236ms, whole-corpus is WallPricedAbort so the
subject must be affected-set-scoped) as a receipt in the design doc §11.
Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
gunbai-bot
Bot
changed the title
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
1 participant
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.
What happened
Attempted the next increment — enroll input-reachability as a live tree-lens that runs over compiled fns (the "whatever is compiled is lens-tested" goal). Building it surfaced a genuine soundness result, so this PR lands the finding, not a gate.
The finding (this is the dependency-fidelity thesis, on our own code)
The enrollment ran
unused_parametersover eachFnArrowDeclviadependency_lens(decl.output). It was green on synthetic unit tests, but the moment it ran over real compiled fns it flagged false positives — the matureunused_parameterslens flagged its own module.Root cause:
FnArrowDecl = { output: Node, params: List<FnArrowParam> }—outputis the return node only; parameters are a separate field. Feedingdependency_lens(decl.output)to a parameter-usage analyzer analyzes the wrong tree. This is §1's keystone lesson recapitulated: synthetic-green lies exactly where a lens is fed the wrong real input; only running over real code exposes it (DESIGN §5/§6 — the reason we treat our own green output as unverified).What this PR does
dependency_fidelity_corpusgate (a false-positive gate is worse than none — hard reject by our own review bar).docs/plans/dependency-fidelity-design.md §11.Verified along the way
discrimination/mutation_adequacyscan clean), confirming affected-set-scoped is the right substrate — a whole-corpus sweepWallPricedAborts (~53 min reconcile wedge).unused_parametersexists to copy.