`Eligibility::from_builtins` degrades `auto-generated (plugin-excluded)`, which is package-independent by construction #219

New issue

Closed

opened 2026-09-07 18:12:30 +02:00 by buildagent · 1 comment

buildagent commented

2026-09-07 18:12:30 +02:00

Member

Found by the #210 lane while adopting from_builtins' completeness gate. Small, and it strengthens two surfaces at once with no RPC.

The gap

Eligibility::from_builtins degrades every builtin Ineligible verdict when packages are installed, on the sound principle that a package might claim the extension. That is correct for ineligible_extension.

It is not correct for PathEligibility::Ineligible("auto-generated (plugin-excluded)"). That verdict means a builtin claims the extension and excluded the file as generated. Since Manifest::validate refuses at discovery any package whose claims intersect a compiled-in language's, no installed package can ever claim an extension a builtin already claims. So this verdict cannot be overturned by any package set — it is package-independent by construction — and degrading it under BuiltinPartial throws away a proof that was already sound.

Why it was not fixed in #210

The lane deliberately mirrored the existing behaviour rather than make doctor stronger than index_coverage, which is the right instinct: two surfaces disagreeing is the defect #210 exists to remove, and a lane fixing doctor should not unilaterally widen the shared ladder.

Fixing it in from_builtins moves both surfaces together, which is the correct place.

What the fix must do

Distinguish the two Ineligible reasons in from_builtins: keep degrading ineligible_extension (a package could claim it), stop degrading auto_generated (no admissible package can). The justification rests on Manifest::validate's intersection refusal, so the fix should cite it — if that refusal is ever relaxed, this exemption must go with it.

Mutations

Degrade auto_generated again → the assertion that a generated file is proved never with packages installed must go RED.
Stop degrading ineligible_extension → the assertion that .wasm is NOT proved never with packages installed must go RED. Both directions need grading or the fix is a one-way widening.
Remove Manifest::validate's intersection refusal → a test pinning that refusal must go RED, since this exemption is only sound while it holds. That is the guard worth most: it stops a future change from quietly invalidating the reasoning here.

Related: #210 (the fix that surfaced it), #218 (the RPC that would close the rest of the same gap).

Found by the #210 lane while adopting `from_builtins`' completeness gate. Small, and it strengthens two surfaces at once with no RPC. ## The gap `Eligibility::from_builtins` degrades every builtin `Ineligible` verdict when packages are installed, on the sound principle that a package might claim the extension. That is correct for `ineligible_extension`. It is **not** correct for `PathEligibility::Ineligible("auto-generated (plugin-excluded)")`. That verdict means a *builtin* claims the extension and excluded the file as generated. Since `Manifest::validate` refuses at discovery any package whose claims intersect a compiled-in language's, **no installed package can ever claim an extension a builtin already claims**. So this verdict cannot be overturned by any package set — it is package-independent by construction — and degrading it under `BuiltinPartial` throws away a proof that was already sound. ## Why it was not fixed in #210 The lane deliberately mirrored the existing behaviour rather than make `doctor` stronger than `index_coverage`, which is the right instinct: two surfaces disagreeing is the defect #210 exists to remove, and a lane fixing `doctor` should not unilaterally widen the shared ladder. Fixing it in `from_builtins` moves both surfaces together, which is the correct place. ## What the fix must do Distinguish the two `Ineligible` reasons in `from_builtins`: keep degrading `ineligible_extension` (a package could claim it), stop degrading `auto_generated` (no admissible package can). The justification rests on `Manifest::validate`'s intersection refusal, so the fix should cite it — if that refusal is ever relaxed, this exemption must go with it. ## Mutations * Degrade `auto_generated` again → the assertion that a generated file is proved `never` with packages installed must go RED. * Stop degrading `ineligible_extension` → the assertion that `.wasm` is NOT proved `never` with packages installed must go RED. Both directions need grading or the fix is a one-way widening. * Remove `Manifest::validate`'s intersection refusal → a test pinning that refusal must go RED, since this exemption is only sound while it holds. That is the guard worth most: it stops a future change from quietly invalidating the reasoning here. Related: #210 (the fix that surfaced it), #218 (the RPC that would close the rest of the same gap).

buildagent commented

2026-09-07 19:22:36 +02:00

Author

Member

REFUTED. Closing without the fix, and the counterexample is now pinned so it cannot be silently re-implemented.

The premise this issue rests on — "no installed package can ever claim an extension a builtin already claims" — was true before #84 and is not true now.

Manifest::validate (crates/package/src/manifest.rs:1142) no longer calls check_against(&builtin_claim_table(), Scope::PackageVsBuiltin). It calls self.displacements() → builtin::displaced_by, which refuses an intersection only when [[displaces]] did not declare it. Intersection is now consent-gated, not forbidden.

And it lands exactly on this verdict rather than near it:

builtin csharp claims includes: ext:cs with excludes: suffix .Designer.cs, suffix .g.cs (crates/package/src/builtin.rs:97) — those excluded files are the entire population behind auto-generated (plugin-excluded);
a consented Displacement carries the builtin's key, ext:cs, which is wider than what the builtin actually indexes, and Displaced::covers tests that key — so it covers Foo.Designer.cs;
path_eligibility_in consults displacing_route before the builtins, so the package wins.

Measured end-to-end through the production door — packed by Container::pack, signed, installed into a real Store, approved via ApprovalRecord, discovered by PackageSet::discover_with_store — with a package claiming ext:cs plus [[displaces]] csharp ext:cs:

svc/Foo.Designer.cs   builtins-only = ineligible:auto-generated (plugin-excluded)
                      with-packages = package:de.h-dv.displacer/probe
svc/Foo.g.cs          builtins-only = ineligible:auto-generated (plugin-excluded)
                      with-packages = package:de.h-dv.displacer/probe
svc/Foo.cs            builtins-only = builtin:csharp
                      with-packages = package:de.h-dv.displacer/probe

Half this evidence was already in the tree: crates/package/tests/builtin_displacement.rs:225 (a_conservative_intersection_is_still_a_consented_displacement) uses Foo.Designer.cs against csharp as its fixture and asserts consent admits it.

The fix would have been actively harmful

Under Source::BuiltinPartial (daemon silent, packages installed) the exemption would emit never / auto_generated for a file the daemon's own eligibility::claims (crates/daemon/src/eligibility.rs:477) reports as code / claimed_by: "package". Two surfaces of one binary disagreeing about one path — the exact defect #210 exists to remove — reintroduced by the change meant to strengthen it. It would also be a negative finding drawn from an answer nobody asked for, which is what eligibility.rs is built to prevent.

The neighbouring `Code` exemption is unaffected

Worth stating because the two look identical. Displacement can only turn Code(builtin) into Package(route), never into Text/Ineligible — path_eligibility_in falls through to select_plugin when displacing_route declines. Both map to Claim::Code, so the claim does not move. Row 3 above measures that. Ineligible → Package does move it, which is why only this verdict is affected.

What landed instead

crates/package/tests/displaced_builtin_exclusions.rs — a guard, not a fix, pinning both halves of the premise, merged as ed139ff. Two mutations run, each reddening only its own test:

Gate Displaced::covers on the builtin route (the change that would make #219 true) → svc/Foo.Designer.cs is inside the displaced domain, so the compiled-in csharp lost it.
displaced_by's if !consent.contains(&c.right) → if false (this issue's own third mutation; the refusal's only remaining site) → a package claiming .cs with no consent must be refused.

So the next lane that reads this issue and reaches for the "obvious" exemption gets a RED naming the counterexample.

If the proof is still wanted

It is not obtainable from a ladder clause. A sound version needs the displacement half of the package state — precisely the state from_builtins does not have and cannot get. That points at #218's RPC, not here.

Correction to the issue as filed: from_builtins is in crates/mcp-server/src/eligibility.rs:366, not crates/indexer/src/index.rs. My error in the original report. It also has substantial existing coverage — 15 call sites, 14 in tests — so unlike #209/#211/#217 this was not a zero-test surface.

**REFUTED. Closing without the fix, and the counterexample is now pinned so it cannot be silently re-implemented.** The premise this issue rests on — *"no installed package can ever claim an extension a builtin already claims"* — **was true before #84 and is not true now.** `Manifest::validate` (`crates/package/src/manifest.rs:1142`) no longer calls `check_against(&builtin_claim_table(), Scope::PackageVsBuiltin)`. It calls `self.displacements()` → `builtin::displaced_by`, which refuses an intersection **only when `[[displaces]]` did not declare it**. Intersection is now consent-gated, not forbidden. And it lands exactly on this verdict rather than near it: * builtin csharp claims `includes: ext:cs` with `excludes: suffix .Designer.cs, suffix .g.cs` (`crates/package/src/builtin.rs:97`) — those excluded files are the **entire** population behind `auto-generated (plugin-excluded)`; * a consented `Displacement` carries the **builtin's** key, `ext:cs`, which is *wider* than what the builtin actually indexes, and `Displaced::covers` tests that key — so it covers `Foo.Designer.cs`; * `path_eligibility_in` consults `displacing_route` **before** the builtins, so the package wins. Measured end-to-end through the production door — packed by `Container::pack`, signed, installed into a real `Store`, approved via `ApprovalRecord`, discovered by `PackageSet::discover_with_store` — with a package claiming `ext:cs` plus `[[displaces]] csharp ext:cs`: ``` svc/Foo.Designer.cs builtins-only = ineligible:auto-generated (plugin-excluded) with-packages = package:de.h-dv.displacer/probe svc/Foo.g.cs builtins-only = ineligible:auto-generated (plugin-excluded) with-packages = package:de.h-dv.displacer/probe svc/Foo.cs builtins-only = builtin:csharp with-packages = package:de.h-dv.displacer/probe ``` Half this evidence was already in the tree: `crates/package/tests/builtin_displacement.rs:225` (`a_conservative_intersection_is_still_a_consented_displacement`) uses **`Foo.Designer.cs` against csharp** as its fixture and asserts consent admits it. ## The fix would have been actively harmful Under `Source::BuiltinPartial` (daemon silent, packages installed) the exemption would emit `never / auto_generated` for a file the daemon's own `eligibility::claims` (`crates/daemon/src/eligibility.rs:477`) reports as `code` / `claimed_by: "package"`. **Two surfaces of one binary disagreeing about one path — the exact defect #210 exists to remove — reintroduced by the change meant to strengthen it.** It would also be a negative finding drawn from an answer nobody asked for, which is what `eligibility.rs` is built to prevent. ## The neighbouring `Code` exemption is unaffected Worth stating because the two look identical. Displacement can only turn `Code(builtin)` into `Package(route)`, never into `Text`/`Ineligible` — `path_eligibility_in` falls through to `select_plugin` when `displacing_route` declines. Both map to `Claim::Code`, so the claim does not move. Row 3 above measures that. `Ineligible → Package` **does** move it, which is why only this verdict is affected. ## What landed instead `crates/package/tests/displaced_builtin_exclusions.rs` — a guard, not a fix, pinning both halves of the premise, merged as `ed139ff`. Two mutations run, each reddening only its own test: 1. Gate `Displaced::covers` on the builtin route (the change that would *make* #219 true) → `svc/Foo.Designer.cs is inside the displaced domain, so the compiled-in csharp lost it`. 2. `displaced_by`'s `if !consent.contains(&c.right)` → `if false` (this issue's own third mutation; the refusal's only remaining site) → `a package claiming `.cs` with no consent must be refused`. So the next lane that reads this issue and reaches for the "obvious" exemption gets a RED naming the counterexample. ## If the proof is still wanted It is not obtainable from a ladder clause. A sound version needs the **displacement** half of the package state — precisely the state `from_builtins` does not have and cannot get. That points at #218's RPC, not here. Correction to the issue as filed: `from_builtins` is in `crates/mcp-server/src/eligibility.rs:366`, not `crates/indexer/src/index.rs`. My error in the original report. It also has substantial existing coverage — 15 call sites, 14 in tests — so unlike #209/#211/#217 this was **not** a zero-test surface.

buildagent closed this issue

2026-09-07 19:22:40 +02:00

buildagent referenced this issue

2026-09-07 19:23:09 +02:00

A git-worktree agent cannot index its own edits — worktrees live under .claude/, which the walker excludes, so the index silently serves someone else's tree #220