Delete supply-side lens enforcement from floor discovery

[gunbai-bot]

What

Two censuses ran inside discover_floor_witness_roster: the inert-lens reach walk and the construction-justification census. Both ask a question about who authored a lens, and both answer it by acquiring a whole-corpus module graph.

Every discovery run paid for that acquisition, and who that was changed under this branch, so it is stated by era rather than as one population: before #8140 the roster walk was unconditional, so ordinary CI, regen, the falsifier cadence and every coordinated worker all paid; #8140 made it demand-directed and regen stopped paying; from there until this PR the two censuses burdened every remaining discovery-bearing execution — all of which wanted a witness roster and nothing else. That is the shape the floor-cost work keeps finding: the unit of computation is the world, the unit of fact is one module's authorship.

Neither census had a consumer that justified the acquisition. The inert-lens half additionally reported through two host builtins whose entire .dag surface was a pair of self-recursive stubs — fn inert_lens_unreached_module_count() -> Int { inert_lens_unreached_module_count() } — reachable only because the interpreter intercepted the spelling before the body ran.

Deleted end-to-end, not merely unwired

Per the acceptance bar: zero non-historical references, zero host dispatch, zero floor execution, zero registry obligation.

• src/v2/lens/inert_lens.dag
• both host builtins, both interpreter dispatch registrations (free-call and v4_bridge), the generated EvalCallBridgeLensInertLens family, the 04_method.dag type-table entries, the std.primitives roster rows and the four v1_interpreter_primitive_surface arms
• the InertLens registry variant, lens_registry_v0_inert_lens, lens_contract_inert_lens and the lens_module_gate invariant surface
• inert_lens_modules, inert_lens_modules_legacy, lens_justification_census, unjustified_lens_modules, declares_construction_justification, and both floor refusal arms (cli_run.rs and floor_discovery_snapshot.rs)
• dag/test/claim/long/inert_lens_hygiene_witness_test.dag and its frozen deferral row, recorded in the shrink log as a deletion-of-subject rather than a migration

Net +80 / −908 across 26 files (−828), refreshed at head 9b7626fa002 — the first three figures in this body were taken at the opening head and went stale twice as review corrections landed.

What this does NOT claim

The expensive facts build is still there. build_module_graph_facts_live has two remaining consumers on this path — effect-reach derivation, and the cross-worker snapshot transport (facts_to_snapshot → FloorDiscoverySnapshot.module_graph_facts → install_module_graph_facts_cache). Deleting both censuses does not delete the world acquisition, and an earlier draft of this work asserted it would. That was wrong; the fourth consumer is downstream in the serialization and invisible from the producer body.

The open question this leaves is the right one to leave: which exact graph facts does the coordinated scoped worker consume, and were they already produced by the ordinary execution that precedes it?

This is a scope narrowing, not a climb. A newly authored lens with no witness, and a lens recording no construction_justification, are both writable again and nothing detects either. The obligation survives as review diligence, which is strictly weaker. Declared in DESIGN §6 with its next-rung trigger rather than left to be rediscovered: an authorship fact belongs on the module's own declaration, checked at ingestion where the module is already parsed, rather than reconstructed corpus-wide by a consumer that wanted a roster.

Retained

refuse_on_module_graph_read_refusals and both of its red controls stay. The arm was written for the lens censuses, but it now guards the two live consumers; the tests moved to a module_graph_read_refusal_tests module and the unreadable-source control is renamed off its lens framing.

Citations repaired (§3)

Two live prose sites cited things this change deletes, so they are corrected in the same diff rather than left stale:

• gunbc.roadmap_authority v1_interpreter_primitive_roster_acceptance_note cited free_call_shadowing_is_exactly_the_two_inert_lens_bridges as surviving exact-set evidence. That witness becomes free_call_carries_no_shadowed_spelling — an exact set assertion over an empty set, which is genuinely weaker, and the note now says so rather than reading as though nothing changed.
• v2.compiler.source_authority used the inert-lens stubs as its worked example of host interception.

Verification

cargo check -p v1-compiler --all-targets clean; cargo fmt --all --check clean via hooks. The .dag corpus compile, the primitive-surface drift gate and the witness corpus run in CI — a whole-tree build is a CI job, not a session job.

🤖 Generated with Claude Code

https://claude.ai/code/session_018ZrxLJrt8ASGLegiK72fAi

[gunbai-bot]

Floor is red on inherited main breakage, not on this PR

build, regen and heal_generated_artifacts all pass at e585778. The ci floor fails with two compile-clean classes, and neither is caused by this change:

58 × dag/{gunbc/ci_budget_tree, product/budget_tree, test/claim/budget_tree_witness_test}.dag
        error: unresolved type 'Memory'
 2 × dag/test/claim/github_app_registry_witness_test.dag
        error: function 'unsatisfied_capabilities' not found in scope

Evidence that this is inherited rather than introduced:

• Main is red with the identical signature. Run 31518518948 on main 341d3203b fails with 92 × unresolved type 'Memory' and 20 × unsatisfied_capabilities' not found. Same classes, same files, larger counts on the wider scope.
• None of the failing files are in this diff. git diff --name-only origin/main...HEAD contains no measure, budget_tree, or github_app_registry path.
• std.measure is untouched here and identical on both sides. Memory is a Quantity variant imported as a type argument (Appropriation<Memory, One>); the last commit to touch dag/std/measure.dag is 341d3203bc2 (SPATIAL-2, SPATIAL-2: units grounding, signed components, affine space, exact Euclidean geometry #8091), which is exactly the commit at which main went red.

I am deliberately not repairing either class inside this PR. Both are someone else's lane, and folding an unrelated corpus repair into a bounded deletion is how a deletion stops being reviewable. This PR needs a green base, not a wider diff.

Merge criteria otherwise: 2/2 distinct approvals (claude, cursor), no open REQUEST_CHANGES, mergeable CLEAN, build/regen/heal green. The floor gate is blocked on main healing; once it does I will merge main in and re-run rather than push code.

Accounting refresh, prose only: the body's +80 / −908 across 26 files is the authored head 9b7626f. At the healed head e585778 GitHub reports +96 / −914 across 27 files, the difference being the auto-heal commit's regenerated DESIGN.md and docs/plans/construction-justification-rule.md projections.

— sent from eager-cat-841

[gunbai-bot]

Both red checks trace to one timeout, and it is not this diff

regen hit its 15-minute step cap; ci then refused without evaluating anything:

FloorUpstreamAlreadyRed build=… regen=failure heal=…
  "an upstream job already established this branch is red, so the floor refuses
   before spending its budget. The located cause is that job's own diagnostic;
   this step adds no verdict of its own."

So there is exactly one cause to explain, and the decisive evidence is that two runs exist on the identical head a9115935e:

run	event	regen
31537407119	workflow_dispatch	success, 7m16s
31537265997	pull_request	failure, 15m00s (step cap)

Same commit, same tree, opposite outcomes — content cannot explain that. The branch's own history agrees: regen has passed seven times here at 6:47–9:33, including twice after the main merge, and main's regen at the equivalent commits runs 6:33–7:35. The two runs were executing concurrently on the same SHA, and the failing run's siblings were slow too (heal 5m24s, build 2m03s against this branch's usual).

I am not pushing a fix, because there is no defect here to fix:

• Not a code change. The tree that timed out is the same tree that passed regen in 7m16s thirty minutes earlier.
• Not a cap raise. DESIGN is explicit — "Do not raise CI step cap first — cap lives in gunbc.ci_spec." A cap raise to absorb contention is the absorbing-fallback shape §5 forbids: it would zero the failure's frequency by construction and hide the real signal.
• Not a third concurrent run. Starting one now would compete with the dispatch run's floor and risk reproducing exactly the contention that caused this.

The dispatch run's ci floor is executing on this SHA now and will produce the real verdict. Once it settles I will re-run the pull_request regen/ci jobs so the required checks reflect what the tree does.

One finding worth keeping past this PR: regen at 6:47–9:33 against a 15-minute cap has under 2× headroom, and contention alone is now demonstrated sufficient to exhaust it. #8140 bought that margin (14:54 → 8:26); this run is evidence the margin is thinner than the numbers suggest, and that the next regen-input growth spends it.

— sent from eager-cat-841

[gunbai-bot]

Correction to the mechanism in my previous comment

I attributed the regen timeout to concurrency — two runs on the same SHA competing for runners. That was inference from the timing overlap; I did not check where the jobs ran. The observable fact is host identity, and the correction came from the operator thread rather than from me.

same SHA a9115935e:
  srv1-03   success   7.27 min
  srv4-03   FAILURE   >=15 min  (killed at the cap — CENSORED, not measured)

other regens, comparable content:
  srv1-05   success   9.35 min
  srv2-05   success   9.55 min
  srv4-01   success   8.47 min

The conclusion in that comment stands — the timeout is not caused by this diff, since the identical checkout passed in 7m16s. What changes is why, and the difference matters for anyone sizing budgets off it.

Two things this data does not support, stated because they are the easy misreadings:

• Not "srv4 is slow." srv4-01 completed in 8.47 min, mid-pack. It is srv4-03 specifically, or a condition on it, not a family property.
• Not "regen takes 15 minutes on srv4-03." The step was killed at the cap, so the true demand was never observed and cannot be quoted. It is a censored lower bound — the same honesty class gunbc.ci_spec applies to its own operator-signed raises.

The finding worth carrying past this PR. Among completing runs the fleet spread is 7.27 -> 9.55 min = 1.31x, roughly consistent with the ~1.2x spread the budget notes explicitly fund (gunbc_ci_compile_clean_clamp_note, gunbc_ci_floor_batch_wall_budget_note). srv4-03 on identical content is >=2.06x and unbounded above. Budget margins across this repository are sized on that 1.2x assumption; a host at double it is not covered by any of them, and regen at ~7-9.5 min against a 15-minute cap has the least headroom of the family.

For the record, the measured anatomy of a passing 9m21s regen, since "regen is slow" gets attributed to the wrong phase:

~2m00s   job setup (checkout, toolchain, artifact download + verify)
 1m56s   UNATTRIBUTED — nothing printed inside the regen step
 1m11s   output-policy + group-syntax install
    38s  plan resolve                      <- for a TWO-node plan
   110ms naming-hygiene walk               <- #8140; was ~6 min this morning
 2m26s   regen_verify_gate_passes          <- real work
 2m34s   self_host_realized_comparison_staleness_gate_holds  <- real work
   ~20s  receipts + upload

About five minutes is the genuine self-host fixed point. The other four are fixed prelude paid regardless of the plan asking for two nodes — the same cost shape #8140 and #8141 have been removing, surfacing in a different phase.

— sent from eager-cat-841

[gunbai-bot]

Third and final refinement on the regen red — the mechanism is a lost runner, not contention

My first comment said contention; my second corrected that to host identity. Both understated it. The operator thread pulled GitHub's own classification for the failing job:

"The self-hosted runner lost communication with the server" — naming runner termination, CPU/memory starvation, or network loss as possible causes.

The runner disappeared during regen. And it was not confined to this branch: main's regen failed the same way in the same window on srv3-01.

So the honest split is:

ESTABLISHED
  #8141 is not a semantic regen regression
  the failure varies by runner host
  srv3-01 and srv4-03 lost runner communication during regen
  srv1-03 completed the identical branch subject in 7:00

NOT ESTABLISHED
  that CPU contention caused it
  that the 15-minute step cap caused it
  which of memory, network, runner-service death or host pressure is the cause

I was wrong to say contention was proved. It was inference from a timing overlap, and I repeated the same shape after being corrected once — a confident answer to the adjacent question.

This changes the remedy, which is why it is worth a third comment rather than a footnote: the fix is fleet health, not CI tuning. A vanished runner is not absorbed by raising a cap, adding a retry, or adding a cache — each of those would zero the failure's frequency by construction and hide a host that is failing to stay alive.

A second over-generalization, corrected

I reported "1m56s unattributed" inside the regen step as if it were a property of regen. It is a property of the run I measured. Verified against step boundaries on both:

host	step wall	step start -> first print	policy install	genuinely unattributed
srv1-05	9m04s	187 s	71 s	116 s
srv1-03	7m00s	74 s	71 s	~3 s

Both measurements are correct; they are different runs. The thread is right that there is no separate unexplained block in the 7-minute run. And the delta is itself the finding: ~2 minutes of pre-install silence on one host versus ~3 seconds on another, for identical work, accounts for nearly the whole 7:00 vs 9:04 spread. That is the same host-variance axis as the lost-runner failure, showing up as cost instead of as a kill.

What is unchanged and worth restating: #8140 worked. The naming walk is 116 ms, and the ~7 minutes that remain are a different set of operations — ~1m50s executor setup, ~4m50s across the two fixed-point gates, ~20s receipts.

Branch state

Merged latest main (49402500b65) with a merge commit, no rebase, no force-push. Head is now 78bfd93039f, which also carries the one genuine content fix the floor found: the bridge-family red control, derived instead of pinned at a population literal. One CI attempt is running on that integrated head.

— sent from eager-cat-841