Repository navigation
Lens hygiene: import-closure inert-lens backstop + promote 5 inert lenses to floor-discovered witnesses (§0) - #5433
Merged
Merged
Conversation
briansrls
added a commit
that referenced
this pull request
Jun 21, 2026
#5433 (jolly-ram-141) owns all *_family_eval → *_test.dag renames; keeping both PRs touching the same file causes a merge conflict. - Revert: lens_ownership_family_eval_test.dag → lens_ownership_family_eval.dag + data (not test data) — back to main-branch state - Manifest: Provenance → InertScaffolded with dissolve-on pointer to #5433 #5435 is now purely the lens_hygiene/ manifest+gate module. Both gates still pass: 4 WiredWithCorpusGate (Parallelism, Idempotency, StructuralResolution, TableDecisionTree) > 0; manifest length == 9 == registry. Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>
gunbai-bot
Bot
changed the title
Contributor
Author
|
Thanks for the review. On the non-blocking observation — `floor_corpus_has_no_inert_lenses` calling `set_current_dir`: Valid point, and agreed it is a footgun in principle. Two reasons I am not pushing a fix into this PR right now:
The clean fix is to pass absolute scan-dirs (as `wet_hermetic_equivalence_test.rs` does) and drop the `chdir` entirely — I will fold that into a fast-follow once this lands, so the discovery tests stop depending on process CWD. Tracking it as a post-merge follow-up. — sent from jolly-ram-141 |
briansrls
added a commit
that referenced
this pull request
Jun 21, 2026
Flip [ ]→[x] for unambiguously-merged work (PR-ref'd for traceability): - §0 numeric-tower grounding (#5428 — == straddle guard dead-in-corpus) - §0 inert-lens hygiene executable backstop (#5433) - §2 F2/F3 resolved_graph key derived from inputs_considered (#5425) - §3 cost-lens symbolic_max zero-absorption fix (#5437) - §4 gate existing generated testgen output (#5434) - §4 affected-set completeness (#5430) Partial/compound items left for their lane managers to flip in the PR that completes them. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
briansrls
added a commit
that referenced
this pull request
Jun 21, 2026
…gestion⁻¹ past syntax (#5442) * WIP: dsl -> v2 scoping * WIP: ROADMAP planning * WIP: ROADMAP planning * WIP: ROADMAP planning * ROADMAP: scannable dependency-ordered checklist; consolidate caching plan (de-fork zesty-deer-479 owner, absorb quick-ant-298 spine) Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> * WIP: ROADMAP planning * self-host: add bootstrap purity (no stage0 hand-edits / regen-lockstep keystone) + precise v1 cutover Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> * ROADMAP §0 fail-closed lock-down (blocks expansion) + audit doc; §4 website demo Audit: cache lossy-digest flake (resolved_graph_cache.rs:146, verified), ~inert analytical lenses (complexity/cost/etc), regen --verify unwired (#5325). Lock-down checklist gates expansion. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> * ROADMAP: flesh §2 idea->idea compiler (medium/language axes); §0 → lock-down LANE (audits→fixes→meta), name model<->realization fork as suspected root Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> * WIP: ROADMAP planning * lock-down: add CI-coverage-completeness audit (rust gate runs 3 of 60 v1 suites) + axiom/syllogism lens (DESIGN open thread #1 — lock down the reasoning) Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> * WIP: ROADMAP planning * roadmap §0/§7 + lockdown: lead with correctness-by-construction, demote lenses to residue Folds in the operator principle (relayed via quick-ant-298): a lens is validation — it concedes the bad thing is writable. Root-cause to make it unwritable (single authority / realization derived from model); reserve lenses for the genuinely- unstructurable (complexity/necessity). #5423's spec-only key lens shipped a false-green as the live proof. - ROADMAP §0: add the principle; split Fixes into tier-1 construction (dissolve model↔realization fork; cache-key derived-from-declared-inputs; self-host purity by construction) and tier-2 lens (complexity/cost; cache-redundancy; purity oracle; promote-inert). Meta-invariant → construction-justification rule. - ROADMAP §7: P1 cache-key reframed from 'realizer-key lens' to key derived from declared inputs_considered (construction). - fail-closed-lockdown.md: construction principle in the thesis; §4 checklist re-ordered construction-first / lens-residue; meta = construction-justification. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> * roadmap §0: add Disposition carrier + 'confront skipped modeling decisions' Captures the lens/coproduct disposition decision (operator). One typed carrier (Terminal{reason} | Scaffold{dissolves_to}) for BOTH lens-lifecycle tags AND coproduct dissolve-markers — today freeform 🟡 comments, unreadable by lens since comments aren't Nodes. Decision: middle path (construction-capable carrier + selectively-enforcing lens that ratchets coverage) now, #1 (substrate can't-define-untagged) as the named end-state. The lens is itself a Scaffold{dissolves_to: substrate-mandatory-tag} — self-dissolving when coverage = whole tree. Rejected jumping to #1 on sequencing (load-bearing §4 substrate change → escalate; flag-day migration; derived coproducts need disposition derived not authored), not on principle. Enforceability split: presence = construction (non-optional field, no meta-lens); redundancy (scaffold + successor both present) = hard gate; Terminal-vs-Scaffold correctness = retro/judgment (synthesis-feasibility limit). - docs/plans/disposition-carrier.md (new) - ROADMAP §0 tier-1 + meta 'confront skipped decisions' standing practice Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> * WIP: ROADMAP planning * DESIGN §5/§6: promote construction-over-validation; roadmap: scope-partition §0, testgen §1, shelve dashboard Addresses the review's four flags + sequencing nuance. - DESIGN.md §5: 'correctness by construction, not validation' is now an axiom (a check re-stating a model constraint is a 2nd representation §2/§3; prefer realization derived from a single authority; reserve checks for the unstructurable residue). §6 'enforce with lenses' reconciled: construction first, lens = residue mechanism, AND the executable inert-lens backstop is NOT superseded by the authoring-time construction-justification judgment. (flag 4 home + flag 3) - ROADMAP §0 partitioned: In-scope this window (numeric-tower grounding; cache trustworthy + warm==cold oracle shipped NOW as detective; widen rust gate; promote inert lenses) vs Fenced-OUT fan-out (Value::Null 131-site split; self-host purity gate; cross-tree import activation; Disposition carrier). Honest framing: window reduces fail-open surface, does NOT 'lock' the class — Null split stays open. (flags 1, 2, sequencing nuance) - ROADMAP §0 meta: restored executable inert-lens hygiene backstop, construction- justification layered on top (not 'supersedes'). (flag 3) - De-dup: principle no longer restated in ROADMAP/lockdown §0; both point to DESIGN §5. cache-key construction homed in §7, §0 references it. (flag 4) - ROADMAP §1 = testgen as bug-class oracle (+ affected-set completeness half + parked anemia lens); dashboard shelved to §8. - docs/plans/testgen-oracle.md (new), fail-closed-lockdown.md realigned. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> * WIP: ROADMAP planning * DESIGN §5/§6/§7: wall-vs-ratchet decidability, displaced-pain denominator, open language design Folds in the operator's product thesis + the two bounds that keep it honest. - §5: construction makes a class unwritable only when membership is DECIDABLE — trichotomy (wall now / wall after grounding / ratchet forever); 'never' is the trap (lets an undecidable ratchet masquerade as a wall — optimality by Rice). - §6: denominate the benefit — the deliverable is a displaced cost (§1 time / a paid-for pain), the lens/substrate is the moat not the product; priced in elegance the work is unbounded (the economic twin of 'never'). - §7: the recursion's payoff — language design itself opens up. It's locked by cost (a check = a compiler fork; a language = an adoption problem); both dissolve here (a wall is a row §2, applied over a medium-agnostic substrate §4), so (compiler-fork × language) → (row + medium). Sound where ingest is Lossless, fail-closed where not (DecodeFidelity §4). Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> * WIP: ROADMAP planning * ROADMAP: fix doc-graph violations from bright-eagle-46 review of #5424 Apply the apex axiom/syllogism lens (single authority / no orphan / no cycle) to the roadmap itself — manual acyclicity pass: - orphan: testgen-oracle.md backlinked §1 → repoint §4 (its own lane) - single authority: §0 cache-key now a pure pointer (= §2 F2/F3/P1); §0 numeric-tower marked the authoritative home (§5 de-fork / fork plan point here, no second checkbox) - §0↔§5 cycle: self-host purity reframed as a §5 deliverable §0's expansion-gate depends on (edge §5 → §0-gate → products), not §0-owned - undeclared edge: §7 react/html declares its dependency on §6 media - backlink sweep: the reorg had broken every numeric backlink across 7 plan docs; re-point all and anchor each to the stable section TITLE so a future renumber can't silently break them again Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> * ROADMAP §3 + plan: algorithmic-cost reduction by construction (rewrite, not budget) Reframe §3 from per-fn complexity budgets to the actual intent: rewrite common suboptimal patterns (O(n²)→O(n), O(2ⁿ)→O(n), O(n)→O(log n)) to the cheaper equivalent — construction on the cost axis, not a warning. New plan doc docs/plans/algebraic-rewrite-optimization.md captures the up-front design: the decidability split (modeled EffectShape makes the preconditions structural; equivalence stays undecidable so no optimality oracle), rewrite-rule-as-row + once-proven soundness, the common-case catalog tiered by precondition, D1 canonical-form-is-truth / D2 two seed rules / D4 constant-factor deferred, the four-witness DONE bar (incl. the non-firing control half-done versions skip), and a corpus hit-rate acceptance gate. complexity.dag is the cost oracle; synthesis.dag stays the advisory undecidable residue. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> * ROADMAP §2: Phase-0 measurement instrument done (#5431 peak-RSS) — remaining is the Phase-1 consumer Per quick-ant-298: the measurement keystone was nearly complete — model side already floor-enrolled, step timing already emitted; the only gap was peak-RSS, closed by #5431. P4's Phase-0 dependency is satisfied; remaining is the Phase-1 measured->plan feedback + width-fold (also unblocks §1-C). Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> * plan/§3: detection-vs-enforcement containment (E⊆D′⊆D) + explicit seed-rule I/O up front Grounded in cost.dag U2 + complexity.dag (investigated, not theorized): - detection is TOTAL by construction (kernel-level cost fold; arbitrary fns detectable); boundary is precision (ClassUnknown), not coverage - enforced rewrites are a strict subset structurally guaranteed by the class-drop witness: E ⊆ D′(precise) ⊆ D(all) - n√n excluded for a MODEL reason (PolynomialDegree is integer-only, n^1.5 unrepresentable); ternary search excluded (log base is not a class) - today's small gate roster = subject-production limit (fn-body reflection), NOT a detection limit - new §3a fully specifies the two seed rules up front: input→output→ precondition→non-firing control→discriminating equivalence input, so the worker builds to spec and the project can actually finish Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> * ROADMAP §0/§1: rust-gate is cadence-decoupling, not run-all (per fierce-hawk #5427) The 3-filter allowlist was COST selection, not arbitrary gatekeeping — the v1 SEED compiler costs ~tens of CPU-sec per trivial test, so run-all-per-PR is CPU-hours (off the table). True shape: per-PR cost-bounded subset + measured #[ignore="expensive: Ns"] + completeness lens (#5427); nightly --ignored lane as the destination for expensive + the 58 currently-ignored tests (owned by §1/quick-ant, after #5431, escalate for load-bearing CI-gen). Completeness = every test runs on >=1 cadence (fail-closed). Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> * plan §2a: generalize by structural-redundancy keying (O(n^x)->O(n^(x-1)) free); flag n-log-n as substitution Per operator: catalog must generalize polynomial-degree reduction without edge cases. Resolution: rules key on the structural redundancy, never on degree — degree is not evidence of redundancy (would fire on genuine O(n^x)). A structurally-keyed nested-membership->set peels one level wherever it matches; fold-to-fixpoint gives O(n^3)->O(n^2)->O(n). Cost model supports arbitrary integer degree, so witness (b) holds at every peel. Flagged OPEN (operator input invited): O(n^x)->O(n log n) is algorithmic SUBSTITUTION (different algorithms, same I/O) not redundancy elimination — verges on undecidable equivalence; tractable form is per-idiom rules (sort-based dedup, repeated-min->heap), not a parameterized rule. Seed Rule 1 now authored structurally + carries a depth-2 generalization witness. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> * plan §1b: Unknown is an anemic atom — dissolve over time (reuse Disposition), never a false pass Per operator: classifying Unknown isn't a fixed up-front split — it's the standing anemic-leaf dissolution practice (DESIGN §2 decompress->map->reduce) applied to the cost lens. UnknownCost{diagnostic} already carries its reason; the anemia is the free-form reason. Each decomposition resolves an Unknown to construction (now-precise class -> new D′) or a grounded Terminal (genuinely undecidable, positively recognized -> advisory comment). DFS-first: this IS the Disposition carrier (resolves to construction-or-justified-Terminal), so reuse it, don't fork an unknown-reason enum. Supersedes the static Undecidable|Undetermined split. Two invariants fixed up front: never a false pass (Unknown=>Violates, already holds); every Unknown on the dissolution frontier. cost.dag enrichment + un-parking Disposition are operator-gated. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> * ROADMAP: §3 reverts to budget-gate validation (stability); rewrite-engine relocated to §5 (post-stability) Operator decision 2026-06-21: budget-gate validation is fine for the stability window; the algorithmic-cost REWRITE construction design is expansion, homed with self-hosting (§5) — IR-rewrite/canonicalization is most natural once .dag is the self-hosted truth. - §3 = complexity budget gate (validation): cost-lens symbolic_max fix (#5437) + per-fn subject + budget-gates-whole-codebase (gated on fn-body reflection) + synthesis advisory. #5437 foundation stays in-window. - §5 gains an 'adjacent expansion lane' = the rewrite engine, pointing at the preserved plan doc; marked post-stability. - plan doc status -> POST-STABILITY EXPANSION, relocated to §5. Nothing deleted — the rewrite design is preserved, just fenced out of the stability window (same as Disposition / Value::Null-split). Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> * WIP: ROADMAP planning * #5442 review fix (warm-lark-306): grep-as-authority for the sidecar roster (10 not 9) The §0-guard impl PR (#5445) grepped current main and found 10 importers of extdeps.languages.bash.program, not 9 — the 10th (dsl/gunbc/ci_spec.dag) landed via #5432 after the original pre-merge grep. Rather than bump the frozen count, make the live grep the authority (the roster shrinks to 0 as the bash-sidecar arc migrates consumers, so any frozen number rots — the single-authority point). Also note the two *_test importers are intentionally not walled (guard scans consumer-source roots only). Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> * ROADMAP: check off 6 merged items (catch-up sweep) Flip [ ]→[x] for unambiguously-merged work (PR-ref'd for traceability): - §0 numeric-tower grounding (#5428 — == straddle guard dead-in-corpus) - §0 inert-lens hygiene executable backstop (#5433) - §2 F2/F3 resolved_graph key derived from inputs_considered (#5425) - §3 cost-lens symbolic_max zero-absorption fix (#5437) - §4 gate existing generated testgen output (#5434) - §4 affected-set completeness (#5430) Partial/compound items left for their lane managers to flip in the PR that completes them. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> * ROADMAP §1: add compile-clean-gate force-checks-every-fn-body box (2(ii) fail-open) New floor-coverage item: the compile-clean gate is fail-open — unreached fn bodies escape typecheck, so undefined symbols in dead code pass green (execution-proven on utf8_decode_bytes). Construction fix = typecheck total over every declared body. Owned by §1 (quick-ant); measure-first, operator-gated enforce-flip. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> * ROADMAP §0: correct the 2(ii) box — registry-leak mechanism, not unreached-bodies snappy-gull's deeper diagnosis: the fail-open is NOT unreached bodies (bodies ARE visited). utf8_decode_bytes resolves because it's a global builtin_function_registry entry (04_method.dag, a marked bridge scaffold) not scoped to the compiled tree. Reframe the box to tree-scoped builtin availability / registry partition; instance fix = real std fn + remove the registry bridge entry. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> * WIP: ROADMAP planning * plan doc: enforcement roster is a FROZEN grandfather set, not derived (warm-lark correction) Deriving the realization-vocab exception roster from a live grep would make the guard vacuous (leak = non-edge importer AND NOT-in-roster; derived roster ⇒ every importer always in it ⇒ leak_count always 0 ⇒ never fires). Distinguish the informational prose count (rots, re-grep) from the lens's enforcement roster (frozen, so a new unrostered importer goes RED = the teeth). Add the 11th importer (extdeps_external_authority_transport, the #5418→#5445 race, fixed by #5453) and the roster-completeness assertion as the steady-state race-hardening. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> * WIP: ROADMAP planning * ROADMAP refresh: §1 nightly→Pop-B (opt-level won), §2 resolve-cache GO + P2 de-fork-dependent, §0 census regression + gate-hygiene Reflects decisions/findings that landed 2026-06-21: - §1: the "expensive" tests were debug-build amplification, not intrinsic seed cost (proud-deer cause-table); opt-level=3 (#5456) restores Pop-A to per-PR; nightly lane reduced to Pop-B wet-captures only. Mirror corrected in §0. - §2: resolve-cache enable = GO (~18% floor-wall, purity-proven, #5429-gated); P2 ParseTable dissolution reclassified as a downstream consumer of the dsl→v2 de-fork (keen-otter: v2-local rewire is cosmetic); #5446 realize kernel green. - §0: stage0 clone-census ratchet went inert + the seed regressed 1138 over budget (rust-side coverage-by-illusion + thesis regression; #5427 surfaced it); gate-hygiene rule (floor-enrolled gate must be green-on-main at merge) + roster-completeness assertion promoted to should-land (the #5445 floor-skew). - §1: registry-partition instance fix = #5452 (verified sound). 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>
This was referenced Jun 21, 2026
briansrls
added a commit
that referenced
this pull request
Jun 21, 2026
…+ live census) (#5479) * docs/plans: inert-layer lens design — modeled-but-unreached, with a live census Operator ask: a lens to observe inert/unwired layers, especially ones that SEEM load-bearing but are unwired. Design + a real census (measured 2026-06-21): - inert = declared AND not reachable from a live RUN-root (reachability, not reference-count: RealizationObjective and ComputeOffer both have 4 consumers but the first is live via ci_floor_plan→realization_width, the second reaches nothing that runs). - target class (0 live consumers, load-bearing): CacheLayerPlan, WorkDemand, ParallelismShape/ IndependentShards/PartitionedReduce, Partitioner, execution_receipt_digest stub. - generalizes the #5433 inert-lens backstop (does NOT fork it): same module-reachability BFS, widened roots (run not test) + output (all modules not just v2.lens.*). - two tiers: module-level buildable now (reuse cli_run.rs:2558); symbol-level needs whole-corpus BindsTo enumeration, gated on #5364 like concept_index. - frontier: decidable ② observing lens now → ① fail-closed wall once the staged-ahead exception roster empties (same ratchet→wall as the realization-vocab guard). Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> * inert-layer-lens: add the rules section — what is a hard wall vs only looks like one Operator rule-design question (test consumers? dead transitive consumer? 1-but-should-be-10?). Classified each against the expressibility-frontier: - test-consumer: separate root set (run vs test) → 'tested but unrun' bucket; wall only on run-root-inert. ① - transitive dead consumer: never count locally — membership in the complement of the reachable set, fixpoint over the whole tree. ① - dead arms/fields ('should be 10' reading A): arm-level reachability, decidable. ① - under-consumption ('should be 10' reading B = 10 call-sites should consume it): NOT inertness — the §2/§3 redundancy/nicknaming dual; 'should be N' is ③ undecidable directly but ② detectable as hand-rolled equivalents. Keep separate from the inert rule (fusing breaks the wall). Hard rule = 0-reachability, a wall on 3 conditions (enumerable run-roots + reflective edges count + shrinking exception roster). Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> * inert-layer-lens: generalize to N substrates (docs included) + wire this doc's ROADMAP line Operator: extend the reachability rule to DOCS — a plan doc with no ROADMAP link is an orphan, the same shape as an inert carrier. Added §8 generalization (code · docs · lenses are one rule over three graphs; docs = the cheapest wall, pure link reachability) with a live census: 18 docs, 13 reachable, 5 orphans + 1 dangling ROADMAP link (expensive-test-cause-table.md referenced twice, never written). Demonstrates the rule by fixing its own orphan: adds the reachability-completeness ROADMAP §0-meta line in the SAME PR (a PR adding docs/plans/X.md must wire it — the doc-graph analog of 'an inert lens is a lie'). Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> * inert-layer-lens: repoint the dangling cause-table link + correct census count (bright-stag) bright-stag (ROADMAP owner) corrections folded in: - DANGLING REF: repoint ROADMAP line 32's [cause table] link expensive-test-cause-table.md → ci-selection-vs-scheduling.md, where the Pop-A/Pop-B debug-amplification content already lives. Do NOT create a new doc (§2/§3 — would duplicate). 0 dangling refs remain. - Corrected the §8 census: the ref was 1× (line 32), not 2× — my first census read a stale local ROADMAP behind main's terse pass; added a methodology note that the lens must run against the live tree (the discipline it enforces). 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
Jun 21, 2026
… a root, rostered, or deleted (#5484) The doc substrate of the one reachability rule the #5433 inert-lens backstop runs over the lens substrate (DESIGN §3 single authority; plan §8 one-rule-N-substrates). NOT a fork: reachable_set is the same seed→transitive-closure BFS shape as cli_run::inert_lens_modules, re-expressed over doc nodes — and cli_run.rs (the #5433 closure) is untouched. THE RULE: every docs/**/*.md must be reachable from a root (ROADMAP/DESIGN for plan docs; docs/runbooks/README.md for runbooks), reached via a reflective .dag-comment bind: ref, or deleted; no dangling ](x.md) link. Both halves FAIL-CLOSED. - doc_reachability_project.rs (NEW, self-contained): live-tree census — walks docs/**/*.md, BFS from per-kind roots over markdown links + bind: reflective edges; reports orphan + dangling counts. Same additive corpus-gate builtin seam as extdeps_external_authority_live_clean_tree_holds / fact_cardinality_* (NOT a load-bearing / pipeline edit; manager-approved). - doc_graph_orphan_count / doc_graph_dangling_link_count builtins (additive arms in v1_interpreter.rs dispatch + v1_compiler_infer_method.rs registry only). - doc_reachability_witness_test.dag: floor-discovered test fn witness; both verdicts green by execution, RED on revert (proven: remove an inbound link → orphan RED; break a link → dangling RED). RED/GREEN synthetic-graph controls in the project module unit tests. DISSOLUTION TRIGGER: the orphan half needs filesystem enumeration (no list-dir .dag host effect yet); folds into pure .dag on gunbc#5364. The dangling half alone is already pure-.dag-expressible. Ship GREEN-on-main: added the 5 missing inbound links (construction-justification, ci-merge-freshness, compile-clean-forcecheck, m4-hermetic-corpus, m5-fixture-store) + a docs/runbooks/README.md index root linking the bmc runbook. Live tree now 22 docs / 22 reachable / 0 orphans / 0 dangling. Plan §8/§9 premise corrected (the no-host-bridge claim holds only for the dangling half). Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
briansrls
added a commit
that referenced
this pull request
Jun 21, 2026
… wall (generalize #5433, no fork); see docs/plans/inert-layer-lens.md §8 (#5484) * WIP: §0 reachability-completeness lens: doc-graph instance as first gating wa * §0 doc-graph reachability-completeness wall: every doc reachable from a root, rostered, or deleted (#5484) The doc substrate of the one reachability rule the #5433 inert-lens backstop runs over the lens substrate (DESIGN §3 single authority; plan §8 one-rule-N-substrates). NOT a fork: reachable_set is the same seed→transitive-closure BFS shape as cli_run::inert_lens_modules, re-expressed over doc nodes — and cli_run.rs (the #5433 closure) is untouched. THE RULE: every docs/**/*.md must be reachable from a root (ROADMAP/DESIGN for plan docs; docs/runbooks/README.md for runbooks), reached via a reflective .dag-comment bind: ref, or deleted; no dangling ](x.md) link. Both halves FAIL-CLOSED. - doc_reachability_project.rs (NEW, self-contained): live-tree census — walks docs/**/*.md, BFS from per-kind roots over markdown links + bind: reflective edges; reports orphan + dangling counts. Same additive corpus-gate builtin seam as extdeps_external_authority_live_clean_tree_holds / fact_cardinality_* (NOT a load-bearing / pipeline edit; manager-approved). - doc_graph_orphan_count / doc_graph_dangling_link_count builtins (additive arms in v1_interpreter.rs dispatch + v1_compiler_infer_method.rs registry only). - doc_reachability_witness_test.dag: floor-discovered test fn witness; both verdicts green by execution, RED on revert (proven: remove an inbound link → orphan RED; break a link → dangling RED). RED/GREEN synthetic-graph controls in the project module unit tests. DISSOLUTION TRIGGER: the orphan half needs filesystem enumeration (no list-dir .dag host effect yet); folds into pure .dag on gunbc#5364. The dangling half alone is already pure-.dag-expressible. Ship GREEN-on-main: added the 5 missing inbound links (construction-justification, ci-merge-freshness, compile-clean-forcecheck, m4-hermetic-corpus, m5-fixture-store) + a docs/runbooks/README.md index root linking the bmc runbook. Live tree now 22 docs / 22 reachable / 0 orphans / 0 dangling. Plan §8/§9 premise corrected (the no-host-bridge claim holds only for the dangling half). Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> * WIP: §0 reachability-completeness lens: doc-graph instance as first gating wa --------- Co-authored-by: Brian Searls <briansrls@gunb.ai> Co-authored-by: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
10 tasks done
briansrls
added a commit
that referenced
this pull request
Jun 30, 2026
* WIP: Lens-hygiene wall: every lens floor-wired or deleted * WIP: Lens-hygiene wall: every lens floor-wired or deleted * Fix inert-lens builtins: derive roots and scan dirs from ci_layer_roots authority The floor witness builtins must not hardcode witness_layer_roots / witness_discovery_scan_dirs when module_path_index already projects them from gunbc.ci_layer_roots (DESIGN §3 single authority). Generalize the authority List<String> reader and wire both builtin entry points through it. Co-authored-by: Cursor <cursoragent@cursor.com> * Fix CI: cargo fmt on module_path_index witness_discovery_scan_dirs Co-authored-by: Cursor <cursoragent@cursor.com> * ci: retrigger after fleet sccache flake on rust_tests (merge commit) Prior run 28439045978 failed rustc exit 254 via sccache during nextest compile — infra EAGAIN, not a code defect. fmt/clippy/inert_lens_hygiene green locally on 2042f95. Co-authored-by: Cursor <cursoragent@cursor.com> --------- Co-authored-by: Brian Searls <briansearls1@gmail.com> Co-authored-by: Cursor <cursoragent@cursor.com>
gunbai-bot Bot
pushed a commit
that referenced
this pull request
Aug 11, 2026
… census Review 51154 caught a consistency failure in my own work: I applied the stale-authority fix to `construction_justification_rule.dag` and then judged `inert_layer_lens.dag` "historical prose" without running the same test on it. It fails that test. It is a registered plan whose §3 tells a future worker that Tier 1 is "buildable now (reuse #5433)" and to extend `inert_lens_modules` — a function this PR deletes — and §7 goes further, advising them to extend it behind a flag rather than fork it. Someone following that plan would go looking for machinery that is gone. Four rows repointed rather than deleted, since the design reasoning survives even though its cited mechanism does not: - §3 Tier 1 now leads with the supersession, names `v2.lens.module_graph` as the surviving reachability authority, and says plainly that "reuse the existing walk" now means "build the walk", which is a larger job than the paragraph reads. - §6's reuse map repoints the transitive-reachability-BFS row off `cli_run.rs:2558-2606` — a positional citation into a file that has since moved several thousand lines, which is the §3 rot mode exactly. - §7's seed caveat drops the extend-behind-a-flag advice and states the real constraint: whatever Tier 1 becomes must not reintroduce a corpus-wide walk inside floor discovery, because the placement was the defect, not the walk. - §5's "fail closed exactly as #5433 does" moves to past tense; no lens-inertness gate runs today. Also marked the two remaining historical citations, in the same plan's landed doc-graph receipt and in `axiom_syllogism_lens.dag`'s precedent table, so every surviving mention of a deleted symbol carries its deletion beside it. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_018ZrxLJrt8ASGLegiK72fAi
briansrls
pushed a commit
that referenced
this pull request
Aug 12, 2026
* Make the witness-roster walk demand-directed instead of unconditional pre-plan claim_executor ran discover_floor_witness_roster_with_snapshot once up front, BEFORE resolving the plan, on the stated ground that a naming violation should be "the cheapest possible failure". Measured, that walk is the most expensive phase in the process: 5.9 min of a 56.5-min ordinary floor (run 31477894666), and ~6 min of a ~15-min regen whose plan has exactly two nodes. It is expensive because "naming hygiene" is a misleading label. The four rules in v2.workflow.floor_naming_hygiene are string predicates over file paths and line prefixes, but the roster producer they are reached through also builds module-graph facts, runs a second strict reference-resolution pass, computes path indexes, and runs inert-lens reachability plus the construction- justification census. A two-node regen plan paid all of it to discover a roster it never reads. Hygiene is a property of the witness ROSTER, so it is now paid by the plans that have one: the walk moves to the existing `schedules_discovery` predicate, after the plan's batches settle. The roster is memoized by request digest (IN_PROCESS_ROSTER_BY_REQUEST), so plans that DO schedule discovery pay exactly what they paid before — the corpus batch hits the memo this call fills. Plans that do not schedule discovery pay nothing, and cannot be unhygienic: they have no roster. The walk-attempt id is minted unconditionally as before; it is a tracing coordinate every later phase stamps, and it is not the expensive part. This also closes the PRELUDE COVERAGE HOLE gunbc.ci_spec gunbc_ci_floor_batch_wall_budget_note already names: the walk sat outside every batch budget and could only red at the step cap. It is now inside the region the plan accounts for, or absent. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_018ZrxLJrt8ASGLegiK72fAi * Update the design authority for the demand-directed hygiene walk (review 51099) review 51099 (cursor/composer-2.5, REQUEST_CHANGES) correctly caught that #8140 changed documented CI behavior without updating its authority. DESIGN.md Building & checks stated the opposite of the new code: "the executor runs the zero-enrollment naming walk when no discovery batch is scheduled" That clause is superseded here in gunbc.design_document (DESIGN.md is generated from it; the heal job regenerates the projection). Both of the reviewer's findings are recorded rather than only the first: (a) SCOPE — discovery-free plans no longer run the corpus-wide nameability rules. Declared as a narrowing, with the honest coverage argument: every PR runs the `ci` job, whose plan schedules discovery and walks the full tree, so per-PR coverage is unchanged; what is deleted is a second redundant walk on regen-only and plan-artifact-only runs. Explicitly NOT backstopped by the affected-set falsifier, which has produced no green verdict since 2026-08-03. (b) ORDERING — for plans that DO schedule discovery the walk now runs after plan resolve/eval, so a naming violation pays ~0.5 min of plan resolution before refusing. The reviewer asked whether the trade is intentional: it is, and it is priced — ~0.5 min later on the refusing path against ~6 min saved on every regen. A dissolve-on is recorded: the clause, the separate walk, and the `__`-basename rule all retire when the placement rules move to canonical source ingestion and test identities derive from parser-produced declarations. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_018ZrxLJrt8ASGLegiK72fAi * chore: regenerate drifted generated artifacts (ci auto-heal) * Repair the stale output-policy comment left by the walk move (review 51101) review 51101 (cursor/composer-2.5) caught claim_executor.rs:10283 still asserting "The walk still runs before plan evaluation, so a naming violation stays the cheapest failure" — the exact opposite of what this PR does. Non-blocking as a defect, but it is the same class the PR itself is about: a comment standing as authority for behavior the code no longer has. #8140's own receipt was a block comment whose stated premise had been false for months. The paragraph's real subject — install output policy BEFORE the walk so the whole-tree read is funnelled rather than emitting ~2.3k `[file] read` lines — is unchanged and still correct; the walk simply moved further away from it. Rewritten to say that, rather than deleted, so the ordering requirement keeps its rationale. Swept the rest of claim_executor.rs / cli_run.rs for other assertions of the old ordering: the only remaining hits are this PR's own comment describing the prior behavior in the past tense. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_018ZrxLJrt8ASGLegiK72fAi * Delete supply-side lens enforcement from floor discovery Two censuses ran inside `discover_floor_witness_roster` — the inert-lens reach walk and the construction-justification census. Both asked a question about who authored a lens, and both answered it by acquiring a whole-corpus module graph. Every discovery run paid that: every PR, regen, and every coordinated scoped worker, all of which wanted a witness roster and nothing else. The unit of computation was the world; the unit of fact was one module's authorship. Deleted end-to-end, not merely unwired: - `v2.lens.inert_lens` (its `.dag` surface was two self-recursive stubs, `fn f() { f() }`, reachable only because the interpreter intercepted them) - its two host builtins, both interpreter dispatch registrations, the generated bridge family, the `04_method` type-table entries and the `std.primitives` roster rows - the `InertLens` registry variant, its registry row, contract row and `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`) - the long witness and its frozen deferral row (shrink logged) `build_module_graph_facts_live` still runs on this path and this change does not claim otherwise: effect-reach derivation and the cross-worker snapshot transport both consume it. `refuse_on_module_graph_read_refusals` and its two red controls are retained and re-homed, since the fail-closed arm now guards those consumers rather than the deleted censuses. This is a scope narrowing, not a climb. A new lens with no witness, and a lens recording no `construction_justification`, are both writable again and nothing detects either. Declared in DESIGN §6 with its next-rung trigger: authorship belongs on the module's own declaration, checked where the module is already parsed, rather than reconstructed corpus-wide by a consumer that wanted a roster. Two citations repaired rather than left stale (§3): the roadmap acceptance note cited a shadow witness this change renames and weakens, and `source_authority` cited the inert-lens stubs as its example of host interception. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_018ZrxLJrt8ASGLegiK72fAi * chore: regenerate drifted generated artifacts (ci auto-heal) * Reconcile the plan carrier and stale comments with the deleted enforcement Review 51113 (cursor/composer-2.5) found two second authorities still claiming enforcement the code no longer performs — DESIGN §3 dual representation and §4b rung honesty. Both confirmed against the current head, both fixed. `gunbc.plans.construction_justification_rule` said the presence check "run[s] in `discover_floor_corpus_rows`" and listed it as current status. Its retirement condition also named that check as its trigger, so after the deletion the condition could never fire — an unreachable lifecycle claim that structurally cannot report itself satisfied. The plan now leads with a supersession notice, §2/§3/§4 are marked historical rather than reworded, and a new §5 records what was deleted, what it costs (a lens added tomorrow with no justification lands green; the 35-module classification in §4 is a historical measurement, not a maintained invariant), and the next-rung trigger. The retirement condition is replaced with a reachable one and says why. `floor_discovery_snapshot.rs`'s consumer census still listed the two gates and still called the roster walk "pre-plan", which #8140 already made false. Swept the rest rather than fixing only what was reported: eight comments in `cli_run.rs` and one in `claim_executor.rs` named the inert-lens reach as a live consumer of the observation rows, the reference-edge producer, and the selection tier. Repointed to the consumers that remain. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_018ZrxLJrt8ASGLegiK72fAi * Delete the dead lens classifier and date-scope the cost claim Two bounded review corrections. `is_top_level_lens_module` survived the census deletion with no remaining caller — only its own definition. It compiled clean because the crate carries a blanket allow, which is exactly why the residue needed finding by reading rather than by warning. Deleted; the PR's bar is end-to-end with zero residue, and a dead classifier left behind is the pattern this change exists to close. The new DESIGN paragraph asserted the censuses charged "every discovery run — on every PR, on regen, in every coordinated worker". True before #8140, false on this PR's base: #8140 made the roster walk demand-directed, so a discovery-free plan such as regen already stopped paying. Both DESIGN and the plan carrier now split the claim by era — unconditional before #8140, regen exempt after it, the censuses burdening every remaining discovery-bearing execution until this deletion. A change removing stale supply-side enforcement must not land a fresh stale assertion in the same diff. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_018ZrxLJrt8ASGLegiK72fAi * chore: regenerate drifted generated artifacts (ci auto-heal) * Repoint the sibling plan authorities that still advertise the deleted census Review 51154 caught a consistency failure in my own work: I applied the stale-authority fix to `construction_justification_rule.dag` and then judged `inert_layer_lens.dag` "historical prose" without running the same test on it. It fails that test. It is a registered plan whose §3 tells a future worker that Tier 1 is "buildable now (reuse #5433)" and to extend `inert_lens_modules` — a function this PR deletes — and §7 goes further, advising them to extend it behind a flag rather than fork it. Someone following that plan would go looking for machinery that is gone. Four rows repointed rather than deleted, since the design reasoning survives even though its cited mechanism does not: - §3 Tier 1 now leads with the supersession, names `v2.lens.module_graph` as the surviving reachability authority, and says plainly that "reuse the existing walk" now means "build the walk", which is a larger job than the paragraph reads. - §6's reuse map repoints the transitive-reachability-BFS row off `cli_run.rs:2558-2606` — a positional citation into a file that has since moved several thousand lines, which is the §3 rot mode exactly. - §7's seed caveat drops the extend-behind-a-flag advice and states the real constraint: whatever Tier 1 becomes must not reintroduce a corpus-wide walk inside floor discovery, because the placement was the defect, not the walk. - §5's "fail closed exactly as #5433 does" moves to past tense; no lens-inertness gate runs today. Also marked the two remaining historical citations, in the same plan's landed doc-graph receipt and in `axiom_syllogism_lens.dag`'s precedent table, so every surviving mention of a deleted symbol carries its deletion beside it. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_018ZrxLJrt8ASGLegiK72fAi * chore: regenerate drifted generated artifacts (ci auto-heal) * Derive the bridge-family split control instead of pinning its population The floor finally evaluated this branch — main was red before, then an upstream timeout cascaded — and found exactly one red witness in 8757: `v1_interpreter_primitive_dispatch_authority_acceptance_contract_holds`. It is genuinely this PR's. Deleting `v2.lens.inert_lens` removed the last two rows carrying `EvalCallBridgeFamilySite { module: v2.lens.inert_lens }`, so the distinct bridge-family count went 9 -> 8 and distinct_bridge_family_site_count() == 9 redded. The literal was a population pin — the exact class DESIGN §5 rejects, and the exact class #7615 removed from this same carrier's census witnesses. The file's own `closing_contract_note` opens by claiming "The checks here are structural properties that survive roster growth -- not population pins", so the clause contradicted its own contract and my deletion is what surfaced it. Decrementing 9 to 8 would restore green while preserving the defect, so the control is derived instead: the number of distinct emit-site keys must equal the number of distinct modules the bridge rows themselves name, and exceed one. That is not a tautology, because the two sides come from different places — the left from `dispatch_emit_site_key`'s keying, the right from each row's own `module` field. Collapsing the families back onto one shared key (the defect the clause is named for) reds it, 1 != N. Adding or removing a family does not. The clause now measures what its name claims, in both directions. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_018ZrxLJrt8ASGLegiK72fAi --------- Co-authored-by: gunbc-ci-auto-heal <gunbc-ci-auto-heal@users.noreply.github.com> Co-authored-by: Claude Opus 5 (1M context) <noreply@anthropic.com> Co-authored-by: gunbai-bot[bot] <289086189+gunbai-bot[bot]@users.noreply.github.com>
briansrls
pushed a commit
that referenced
this pull request
Aug 12, 2026
… discovery (#8167) * Make the witness-roster walk demand-directed instead of unconditional pre-plan claim_executor ran discover_floor_witness_roster_with_snapshot once up front, BEFORE resolving the plan, on the stated ground that a naming violation should be "the cheapest possible failure". Measured, that walk is the most expensive phase in the process: 5.9 min of a 56.5-min ordinary floor (run 31477894666), and ~6 min of a ~15-min regen whose plan has exactly two nodes. It is expensive because "naming hygiene" is a misleading label. The four rules in v2.workflow.floor_naming_hygiene are string predicates over file paths and line prefixes, but the roster producer they are reached through also builds module-graph facts, runs a second strict reference-resolution pass, computes path indexes, and runs inert-lens reachability plus the construction- justification census. A two-node regen plan paid all of it to discover a roster it never reads. Hygiene is a property of the witness ROSTER, so it is now paid by the plans that have one: the walk moves to the existing `schedules_discovery` predicate, after the plan's batches settle. The roster is memoized by request digest (IN_PROCESS_ROSTER_BY_REQUEST), so plans that DO schedule discovery pay exactly what they paid before — the corpus batch hits the memo this call fills. Plans that do not schedule discovery pay nothing, and cannot be unhygienic: they have no roster. The walk-attempt id is minted unconditionally as before; it is a tracing coordinate every later phase stamps, and it is not the expensive part. This also closes the PRELUDE COVERAGE HOLE gunbc.ci_spec gunbc_ci_floor_batch_wall_budget_note already names: the walk sat outside every batch budget and could only red at the step cap. It is now inside the region the plan accounts for, or absent. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_018ZrxLJrt8ASGLegiK72fAi * Update the design authority for the demand-directed hygiene walk (review 51099) review 51099 (cursor/composer-2.5, REQUEST_CHANGES) correctly caught that #8140 changed documented CI behavior without updating its authority. DESIGN.md Building & checks stated the opposite of the new code: "the executor runs the zero-enrollment naming walk when no discovery batch is scheduled" That clause is superseded here in gunbc.design_document (DESIGN.md is generated from it; the heal job regenerates the projection). Both of the reviewer's findings are recorded rather than only the first: (a) SCOPE — discovery-free plans no longer run the corpus-wide nameability rules. Declared as a narrowing, with the honest coverage argument: every PR runs the `ci` job, whose plan schedules discovery and walks the full tree, so per-PR coverage is unchanged; what is deleted is a second redundant walk on regen-only and plan-artifact-only runs. Explicitly NOT backstopped by the affected-set falsifier, which has produced no green verdict since 2026-08-03. (b) ORDERING — for plans that DO schedule discovery the walk now runs after plan resolve/eval, so a naming violation pays ~0.5 min of plan resolution before refusing. The reviewer asked whether the trade is intentional: it is, and it is priced — ~0.5 min later on the refusing path against ~6 min saved on every regen. A dissolve-on is recorded: the clause, the separate walk, and the `__`-basename rule all retire when the placement rules move to canonical source ingestion and test identities derive from parser-produced declarations. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_018ZrxLJrt8ASGLegiK72fAi * chore: regenerate drifted generated artifacts (ci auto-heal) * Repair the stale output-policy comment left by the walk move (review 51101) review 51101 (cursor/composer-2.5) caught claim_executor.rs:10283 still asserting "The walk still runs before plan evaluation, so a naming violation stays the cheapest failure" — the exact opposite of what this PR does. Non-blocking as a defect, but it is the same class the PR itself is about: a comment standing as authority for behavior the code no longer has. #8140's own receipt was a block comment whose stated premise had been false for months. The paragraph's real subject — install output policy BEFORE the walk so the whole-tree read is funnelled rather than emitting ~2.3k `[file] read` lines — is unchanged and still correct; the walk simply moved further away from it. Rewritten to say that, rather than deleted, so the ordering requirement keeps its rationale. Swept the rest of claim_executor.rs / cli_run.rs for other assertions of the old ordering: the only remaining hits are this PR's own comment describing the prior behavior in the past tense. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_018ZrxLJrt8ASGLegiK72fAi * Delete supply-side lens enforcement from floor discovery Two censuses ran inside `discover_floor_witness_roster` — the inert-lens reach walk and the construction-justification census. Both asked a question about who authored a lens, and both answered it by acquiring a whole-corpus module graph. Every discovery run paid that: every PR, regen, and every coordinated scoped worker, all of which wanted a witness roster and nothing else. The unit of computation was the world; the unit of fact was one module's authorship. Deleted end-to-end, not merely unwired: - `v2.lens.inert_lens` (its `.dag` surface was two self-recursive stubs, `fn f() { f() }`, reachable only because the interpreter intercepted them) - its two host builtins, both interpreter dispatch registrations, the generated bridge family, the `04_method` type-table entries and the `std.primitives` roster rows - the `InertLens` registry variant, its registry row, contract row and `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`) - the long witness and its frozen deferral row (shrink logged) `build_module_graph_facts_live` still runs on this path and this change does not claim otherwise: effect-reach derivation and the cross-worker snapshot transport both consume it. `refuse_on_module_graph_read_refusals` and its two red controls are retained and re-homed, since the fail-closed arm now guards those consumers rather than the deleted censuses. This is a scope narrowing, not a climb. A new lens with no witness, and a lens recording no `construction_justification`, are both writable again and nothing detects either. Declared in DESIGN §6 with its next-rung trigger: authorship belongs on the module's own declaration, checked where the module is already parsed, rather than reconstructed corpus-wide by a consumer that wanted a roster. Two citations repaired rather than left stale (§3): the roadmap acceptance note cited a shadow witness this change renames and weakens, and `source_authority` cited the inert-lens stubs as its example of host interception. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_018ZrxLJrt8ASGLegiK72fAi * chore: regenerate drifted generated artifacts (ci auto-heal) * Reconcile the plan carrier and stale comments with the deleted enforcement Review 51113 (cursor/composer-2.5) found two second authorities still claiming enforcement the code no longer performs — DESIGN §3 dual representation and §4b rung honesty. Both confirmed against the current head, both fixed. `gunbc.plans.construction_justification_rule` said the presence check "run[s] in `discover_floor_corpus_rows`" and listed it as current status. Its retirement condition also named that check as its trigger, so after the deletion the condition could never fire — an unreachable lifecycle claim that structurally cannot report itself satisfied. The plan now leads with a supersession notice, §2/§3/§4 are marked historical rather than reworded, and a new §5 records what was deleted, what it costs (a lens added tomorrow with no justification lands green; the 35-module classification in §4 is a historical measurement, not a maintained invariant), and the next-rung trigger. The retirement condition is replaced with a reachable one and says why. `floor_discovery_snapshot.rs`'s consumer census still listed the two gates and still called the roster walk "pre-plan", which #8140 already made false. Swept the rest rather than fixing only what was reported: eight comments in `cli_run.rs` and one in `claim_executor.rs` named the inert-lens reach as a live consumer of the observation rows, the reference-edge producer, and the selection tier. Repointed to the consumers that remain. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_018ZrxLJrt8ASGLegiK72fAi * Delete the dead lens classifier and date-scope the cost claim Two bounded review corrections. `is_top_level_lens_module` survived the census deletion with no remaining caller — only its own definition. It compiled clean because the crate carries a blanket allow, which is exactly why the residue needed finding by reading rather than by warning. Deleted; the PR's bar is end-to-end with zero residue, and a dead classifier left behind is the pattern this change exists to close. The new DESIGN paragraph asserted the censuses charged "every discovery run — on every PR, on regen, in every coordinated worker". True before #8140, false on this PR's base: #8140 made the roster walk demand-directed, so a discovery-free plan such as regen already stopped paying. Both DESIGN and the plan carrier now split the claim by era — unconditional before #8140, regen exempt after it, the censuses burdening every remaining discovery-bearing execution until this deletion. A change removing stale supply-side enforcement must not land a fresh stale assertion in the same diff. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_018ZrxLJrt8ASGLegiK72fAi * chore: regenerate drifted generated artifacts (ci auto-heal) * Repoint the sibling plan authorities that still advertise the deleted census Review 51154 caught a consistency failure in my own work: I applied the stale-authority fix to `construction_justification_rule.dag` and then judged `inert_layer_lens.dag` "historical prose" without running the same test on it. It fails that test. It is a registered plan whose §3 tells a future worker that Tier 1 is "buildable now (reuse #5433)" and to extend `inert_lens_modules` — a function this PR deletes — and §7 goes further, advising them to extend it behind a flag rather than fork it. Someone following that plan would go looking for machinery that is gone. Four rows repointed rather than deleted, since the design reasoning survives even though its cited mechanism does not: - §3 Tier 1 now leads with the supersession, names `v2.lens.module_graph` as the surviving reachability authority, and says plainly that "reuse the existing walk" now means "build the walk", which is a larger job than the paragraph reads. - §6's reuse map repoints the transitive-reachability-BFS row off `cli_run.rs:2558-2606` — a positional citation into a file that has since moved several thousand lines, which is the §3 rot mode exactly. - §7's seed caveat drops the extend-behind-a-flag advice and states the real constraint: whatever Tier 1 becomes must not reintroduce a corpus-wide walk inside floor discovery, because the placement was the defect, not the walk. - §5's "fail closed exactly as #5433 does" moves to past tense; no lens-inertness gate runs today. Also marked the two remaining historical citations, in the same plan's landed doc-graph receipt and in `axiom_syllogism_lens.dag`'s precedent table, so every surviving mention of a deleted symbol carries its deletion beside it. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_018ZrxLJrt8ASGLegiK72fAi * chore: regenerate drifted generated artifacts (ci auto-heal) * Derive the bridge-family split control instead of pinning its population The floor finally evaluated this branch — main was red before, then an upstream timeout cascaded — and found exactly one red witness in 8757: `v1_interpreter_primitive_dispatch_authority_acceptance_contract_holds`. It is genuinely this PR's. Deleting `v2.lens.inert_lens` removed the last two rows carrying `EvalCallBridgeFamilySite { module: v2.lens.inert_lens }`, so the distinct bridge-family count went 9 -> 8 and distinct_bridge_family_site_count() == 9 redded. The literal was a population pin — the exact class DESIGN §5 rejects, and the exact class #7615 removed from this same carrier's census witnesses. The file's own `closing_contract_note` opens by claiming "The checks here are structural properties that survive roster growth -- not population pins", so the clause contradicted its own contract and my deletion is what surfaced it. Decrementing 9 to 8 would restore green while preserving the defect, so the control is derived instead: the number of distinct emit-site keys must equal the number of distinct modules the bridge rows themselves name, and exceed one. That is not a tautology, because the two sides come from different places — the left from `dispatch_emit_site_key`'s keying, the right from each row's own `module` field. Collapsing the families back onto one shared key (the defect the clause is named for) reds it, 1 != N. Adding or removing a family does not. The clause now measures what its name claims, in both directions. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_018ZrxLJrt8ASGLegiK72fAi * Delete the orphan-helper census and the `__` filename rule from floor discovery Two more required-path phases whose cost was denominated in the corpus and whose answer nobody consumed. Net −1446/+39. **The `__`-basename rule.** A census found ZERO offending basenames in the tree and no stated rationale anywhere for the ban — it guarded an empty population. It was not free: reaching the predicate meant collecting every `.dag` path in the corpus and then resolving a SEPARATE `.dag` entry (`FLOOR_NAMING_HYGIENE_ENTRY` -> `floor_filename_hygiene_refusal_via_producer`) on every discovery-bearing run, so a zero-population style rule cost a whole-tree walk plus an entry resolve. Both are gone, along with the snapshot's `naming_hygiene_refusal` field and the two witness controls. **The orphan-helper census.** It walked every `*_test.dag`, parsed each one, projected `DeclSurface`/`ModuleSurface` values, resolved a second interpreter context, and ran a fuelled reachability fixpoint against a hand-authored cross-module export exception roster — to decide whether a plain helper in a test file was referenced. An unreferenced test helper is dead-code hygiene. It is not evidence that the compiler or the tests are correct, and it did not justify a recurring whole-corpus traversal on a required path. `gunbc.test_module_hygiene` goes 661 -> 106 lines, the Rust bridge 835 -> ~320, and `test_module_hygiene_scaffold.dag` deletes whole (its dissolution obligation is discharged by the deletion, not carried forward). **Scope narrowing, declared rather than implied.** An unreferenced test helper and a `__` basename are both writable again and nothing detects either. The orphan class had fourteen enrolled witnesses and they are deleted with it — §4b permits that only because the class is ABANDONED, not climbing: there is no higher rung for the evidence to guard, and keeping fixtures for a fold nothing calls would be specification-without-execution one level up. Recorded in DESIGN, in the module authority note, and in the witness file that used to hold them. **What survives, and why:** the `test fn` placement rule, the file-grain expand half, and `failure_receipt_companion` — the naming convention `claim_executor` actually invokes. That last one was only ever exercised through the census's whole-corpus walk, so it would have silently lost its executing consumer; it gains direct unit and `.dag` witnesses here instead. **Not in scope, deliberately:** the line-scanned test-identity derivation. That is the second parser, and replacing it needs the canonical parser to retain the `test` marker — which `drop_leading_test_marker` discards, because `test` is a live module-path segment (`test.claim.*`, `extdeps.test.*`) and cannot be lexed as a keyword. `realization_attempt.dag` already names the prerequisite: a contextual-keyword terminal in `GrammarExpr`, which does not exist yet. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_018ZrxLJrt8ASGLegiK72fAi * Refresh the two authority notes the deletion falsified Review 51262 found `floor_naming_hygiene_note` still asserting, in a file this PR edits, that the module sits where it does so "orphan/filename hygiene resolve stays free of the Filesystem service closure" and that it dissolves the hand-Rust mirror `check_floor_filename_hygiene`. Neither survives the deletion: there is no orphan census and no filename-hygiene resolve left to keep free of anything, and the filename half of that dissolution obligation is discharged by deletion rather than by dissolution — no equivalence receipt was ever owed for a rule with a zero-row population. The note now states what remains true instead, including the part worth carrying: the test-decl line scan is still a second parser, and replacing it is not a refactor of this module — it needs the canonical parser to retain the `test` marker, which `drop_leading_test_marker` discards, and `test` cannot become a lex keyword because it is a live module-path segment. Swept for the same class rather than fixing only what was reported: `floor_discovery_dissolve_trigger` still described "the producer and filename-hygiene entries" as two typed entry values resolved through `resolve_workspace_entry`. There is one now. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_018ZrxLJrt8ASGLegiK72fAi * chore: regenerate drifted generated artifacts (ci auto-heal) * Carry the deleted-witness rationale as an authored annotation, not a prose data row `prose_row_introduction_gate` refused this change: `test_module_hygiene_orphan_witness_deletion_note` is a `data NAME_note: String` declaration introduced under `dag/test/claim/test_module_hygiene_hand_rust_equivalence_witness_test.dag`, a path already on `gunbc.prose_row_frontier` `prose_row_migration_scope`. DESIGN §4c: prose is not forbidden, unclassified prose is, and a `String` declaration whose sole purpose is commentary is misplaced data. The rationale is irreducible — it records why fourteen witnesses were deleted with the machinery they tested, and why §4b's dissolution-on-climb rule does not save them (the class is abandoned, not climbed) — so it becomes a leading `//` block attached to the declaration below it. The PR-number and section references in the prose are dropped rather than carried across: those are exactly the machine-consumed facts §4c says belong in a typed carrier, not in commentary. The two other in-scope rows this change touches (`test_module_hygiene_authority_note`, `failure_receipt_companion_note`) are pre-existing declaration names whose content was rewritten, not introductions, and the gate does not refuse them. They are left as rows rather than swept here. Green by execution: the edited witness parses and `test_module_hygiene_file_grain_empty_function_holds` returns `true`. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_018ZrxLJrt8ASGLegiK72fAi * chore: regenerate drifted generated artifacts (ci auto-heal) * Make the deleted censuses past tense in the Building & checks paragraph Review 51377: the paragraph describing the naming-hygiene walk's measured cost still said the roster producer "runs inert-lens reachability plus the construction-justification census" — present tense, about two censuses gunbc#8141 deleted. `claim_executor` already says "(until gunbc#8141 deleted them)" and the §6 bullet in this same document records the deletion in past tense, so the canonical authority contradicted both. The measurement itself stands: those censuses WERE part of what made the walk the most expensive phase when it was measured. What was wrong is the tense, which asserts a superseded population as the present one — and doing that inside a deletion diff is the exact failure #8141's own review caught, recorded a few paragraphs above in this file. Reworded to "and — until gunbc#8141 deleted them — ran", preserving the cost claim as the historical fact it is. Swept for other occurrences: the §6 bullet is already past tense; this was the only stale one. DESIGN.md is a projection of this authority and is regenerated by `heal_generated_artifacts`, so it is not hand-edited here. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_018ZrxLJrt8ASGLegiK72fAi * Drop orphan/helpers from the snapshot consumer-census row Review 51382: the module header still listed "Naming hygiene, orphan/helpers" as what the demand-directed roster walk reads, in a file this PR edits. The orphan-helper census and the `__`-basename rule are deleted here, so the row named work that no longer happens — doc drift inside the diff that removed the subject. The row now names what the walk actually still does: `test fn` placement hygiene, producer roster, module-graph facts, effect-reach derivation, with the deletion noted so a reader is not left wondering where the other two went. The same review's DESIGN.md finding is real and is NOT fixed by hand: DESIGN.md is a generated projection of `dag/gunbc/design_document.dag`, whose wording was corrected in 69009a3. Editing the projection directly would author bytes no authority produced, and `heal_generated_artifacts` reverts exactly that. Heal last ran against the previous head (a5b441b, before the authority fix); its run on this head re-projects the corrected sentence. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_018ZrxLJrt8ASGLegiK72fAi * chore: regenerate drifted generated artifacts (ci auto-heal) * Repair the comment whose contrast named a deleted function Review 51390: a comment justifying why a wiring test calls the producer seam argued by contrast with `floor_filename_hygiene_refusal_for_paths` — which this PR deletes. The live half of the argument still holds (the seam is where a wire-contract violation is observable, and the rule itself is owned content-side by `floor_discovery_equivalence_misplaced_wire_contract_refuses_holds`, so re-deriving it here would be a second representation). Only the contrast was dangling. Rewritten to state the positive reason, with the retired comparison noted as history rather than silently dropped: a reader who remembers the old sentence should find out where it went, not wonder whether the argument changed. No code, assertion, or behavior change. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_018ZrxLJrt8ASGLegiK72fAi --------- Co-authored-by: gunbc-ci-auto-heal <gunbc-ci-auto-heal@users.noreply.github.com> Co-authored-by: Claude Opus 5 (1M context) <noreply@anthropic.com> Co-authored-by: gunbai-bot[bot] <289086189+gunbai-bot[bot]@users.noreply.github.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
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.
Summary
Lands the executable inert-lens hygiene backstop (ROADMAP §0 / DESIGN.md §6: an inert lens is a lie) and promotes the 5 lenses it found inert so the gate is green, atomically (main is never red).
The backstop — a new fail-closed check inside
discover_floor_corpus_rows(cli_run.rs), beside the existingcheck_floor_filename_hygiene/test_fn_violationsfloor-discovery hygiene gates (an extension of the already-seed gates, not new cemented Rust). It computes the transitive import-closure of the discovered witness roster and returnsErr— failing the floor closed — for anyv2.lens.<name>top-level module not reached. There is no escape hatch: a lens is either reached by a discovered witness (*_test.dagcarryingtest fn/test data, or a scan-dirunified_claim_*) that transitively imports it, or it must be deleted. Canonical definition of wired = reachable in that closure.The 5 promotions (the import-closure found exactly these inert; the audit's longer list was stale — complexity/cost/etc. were wired since #5085):
ownershipownership_witnessreturnsViolatesand classifies aResourceDependsOnedgeRequiresAccessWitnesseffecteffect_witnessViolates+ expectedEffectFacton anEffectDependsOnedgeunused_parameterssubsumptionDissolutionSubsumptionrows areMechanicalReverificationand subsume their declared leaf fixesleaf_model_verificationDe-vacuuming found along the way (§5):
ownershipandeffectfamily-evals were authored to route throughrun_test_claimbut their eval harness Defers (silently green-never); repaired to assert the structural lens witness (which genuinely exercises the lens).leafhad a wrong invariant (R2b discriminates at runtime, not compile).Test plan
All run locally (sccache bypassed due to the known corruption flake).
gunbc run --source-root src/v2 --source-root dsl --entry <file> --function <witness> --claim-runfor each → allexit 0, witness= true(ownership, effect, unused_parameters, subsumption, leaf_model_verification).cargo test -p v1-compiler --lib inert_lens_hygiene_tests→test result: ok. 3 passed:floor_corpus_has_no_inert_lenses— whole-corpus discovery succeeds ⇒ 0 inert across all 33v2.lens.*modules (⊇lens_registry_v0: Parallelism / Idempotency / StructuralResolution / TableDecisionTree all reached).detector_red_on_unreached_green_on_wired— RED on an unreached lens, GREEN once a discovered witness reaches it, incl. transitive lens-imports-lens.top_level_lens_module_predicate—v2.lens.<name>vs support sub-module discrimination.RequiresAccessWitness→OwnedContainment; effect deps[..]→[]) flips both witnesses tofalse(RED); reverted clean. The structural asserts are genuinely discriminating, not green-always.Worker attestation
Closes #N— this is a dashboard work item (adhoc-460c3e15-7e5), not a GitHub issue.