Skip to content

Dependency-fidelity increment 1: the FidelityVerdict spine (single-authority verdict + input-reachability surface) - #6567

Merged
briansrls merged 3 commits into
mainfrom
session/merry-cat-180
Jul 14, 2026
Merged

briansrls merged 3 commits into
mainfrom
session/merry-cat-180

Conversation

@gunbai-bot

@gunbai-bot gunbai-bot Bot commented Jul 14, 2026 •

Copy link
Copy Markdown
Contributor

Summary

First implementation increment of the dependency-fidelity design (framing A: I own the engine/coverage spine; the arms feed it). This lands the single-authority verdict model every arm reports into — the §2 law made a type (declared ≡ witnessed ⟺ Faithful), the §3 three surfaces, and the §5 located-discrepancy classes:

  • FidelitySurface = InputReachability | OutputReachability | InteractionFidelity (§3)
  • FidelityDiscrepancy = UnreachedDeclaredInput | UnreachedDeclaredOutput | UnderClaimedEdge | OverClaimedCoupling (§5 — one authority; each arm plugs its located findings into these slots so no arm mints a parallel verdict type, §3 fork-prevention)
  • FidelityVerdict = Faithful | Discrepant { findings }

The input-reachability surface is wired first by consuming the already-live sound arm v2.lens.unused_parameters (no re-mint) — input_reachability_verdict(UnusedParametersFact) -> FidelityVerdict.

Output-reachability (the Node-body arm, §8.4) and the under-claim/over-claim edge arms are declared slots, built in follow-up increments (the under-claim detector is in flight as #6556; it will report into UnderClaimedEdge).

Verification (green by execution, local claim_batch)

  • clean_input_surface_is_faithful — empty unused set → Faithful — PASS
  • one_unused_param_flips_to_discrepant — one unused param → Discrepant — PASS

These are a discriminating pair (§5): the verdict flips between the two inputs, so breaking input_reachability_verdict to always-Faithful reds the second witness.

Corpus hygiene re-run against the tree with the new module — all green:

  • inert-lens hygiene (inert_lens_hygiene_has_no_unreached_modules) — module reached by its witness
  • wiring-liveness corpus (wiring_liveness_corpus_witnesses)
  • compile-clean (resolves in closure)

Not yet

Registration in lens_registry_v0 / enforcement-intent LensContract is deferred to the increment that adds the affected-set-scoped runner (§7) — registry membership is selective today and the co-located witness already reaches the module.

@gunbai-bot gunbai-bot Bot changed the title dependency fidelity Dependency-fidelity increment 1: the FidelityVerdict spine (single-authority verdict + input-reachability surface) Jul 14, 2026
@gunbai-bot
gunbai-bot Bot marked this pull request as ready for review July 14, 2026 02:23
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>
@briansrls
briansrls merged commit 6381765 into main Jul 14, 2026
3 checks passed
@briansrls
briansrls deleted the session/merry-cat-180 branch July 14, 2026 03:00
briansrls added a commit that referenced this pull request Jul 14, 2026
…imitive (#6577)

* WIP: dependency fidelity

* WIP: dependency fidelity

* dependency-fidelity: delete unused FidelitySurface enum (review #6567)

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>

* dependency-fidelity increment 2: the §4 mutation-adequacy coverage primitive

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>

---------

Co-authored-by: Brian Searls <briansrls@gunb.ai>
Co-authored-by: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
briansrls added a commit that referenced this pull request Jul 14, 2026
…ollment on real code (finding + receipt) (#6584)

* WIP: dependency fidelity

* WIP: dependency fidelity

* dependency-fidelity: delete unused FidelitySurface enum (review #6567)

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>

* dependency-fidelity increment 2: the §4 mutation-adequacy coverage primitive

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>

* WIP: dependency fidelity

* dependency-fidelity: do NOT enroll unsound input-reachability gate; record 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>

---------

Co-authored-by: Brian Searls <briansrls@gunb.ai>
Co-authored-by: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant