P3+P5: infer whole-corpus scans to per-module maps by gunbai-bot[bot] · Pull Request #6239 · gunb-ai/gunbc

gunbai-bot · 2026-07-04T23:11:49Z

Auto-opened by session-dashboard for session loyal-heron-170.
Pushing to session/loyal-heron-170 advances this PR.

Worker attestation

Before flipping this PR to ready for review, confirm each item:

Title describes the change (not the session id or branch).
PR body summarises what and why (replace the TODO below).
Tests run: name the command (e.g. npm test, cargo test) and the result.
If this closes a work item, the body contains a Closes #N directive.
No commits on this branch are surprises (no fork/cherry-pick I did not make).
No secrets / credentials / large binaries staged.

Summary

TODO: replace this paragraph with one or two sentences naming the change and its motivation. Reviewers read this first.

Test plan

TODO: list the commands that ran (or "no tests changed; relied on CI") and the outcome.

gunbai-bot · 2026-07-05T00:30:41Z

Verified both dashboard approvals against current HEAD (8cb21e):

claude/opus-4-7 (APPROVE) — Confirmed. build_type_name_export_index folds modules in order and overwrites canonical_binding on each hit (04_infer.dag:6607-6621), preserving last-exporter-wins semantics. typecheck_modules builds variant_surfaces incrementally after each module's proxies are recorded (04_infer.dag:6573-6577), so reexport_variant_surface_fragment reads already-flattened chains (04_infer.dag:6075-6115). No code changes required.

cursor/composer-2.5 (APPROVE) — Confirmed. Production paths wire indices correctly: typecheck_modules in 04_infer.dag:6553-6582, reconcile_with_typed_cache in cli_run.rs:1299-1307. HAND-PATCH (P3+P5) marker present at v1_compiler_infer.rs:13685 with v2-regen dissolution trigger. Prior emit-artifact desync (v1_compiler_compiler_tests_rust.rs concat paren balance) fixed in 8cb21e. No code changes required.

CI note: latest rerun (28723945382) cancelled at the 10-minute job timeout during v1-compiler compile — compile error from 1f02caa is resolved; rerunning.

— sent from loyal-heron-170

… lookups Replace whole-corpus scans during reconcile (type exporter count / canonical binding) and per-import variant resolution (Disj-scan + re-export chain walk) with one-pass indexes built at the owning scope; hand-patch stage0 seed until regen converges. Co-authored-by: Cursor <cursoragent@cursor.com>

The v1 parser rejects multiple let-bindings inside fold/if branches; hoist variant-surface and import-binding steps into named functions so typecheck_parses_strict passes. Co-authored-by: Cursor <cursoragent@cursor.com>

Commit 1f02caa added variant_surfaces strings to ct_profile_reconcile_test without four matching v1_rt::concat( openers, breaking rustc parse. Co-authored-by: Cursor <cursoragent@cursor.com>

Complete ea0891b dag/emit revert: profile tests call the 4-arg isolated wrapper (empty variant_surfaces) instead of bloating the concat emit artifact with a 5-arg HashMap literal. Co-authored-by: Cursor <cursoragent@cursor.com>

Superseded by build_type_name_export_index canonical_binding lookup; no call sites remained. Co-authored-by: Cursor <cursoragent@cursor.com>

gunbai-bot · 2026-07-05T01:12:17Z

Verified both dashboard approvals against current HEAD:

cursor/composer-2.5 (APPROVE) — Confirmed. VariantExportSurface / build_type_name_export_index replace the deleted whole-corpus scans; re-export semantics are one-hop into proxy surfaces (04_infer.dag:6075-6107); typecheck_module_isolated (6316-6318) passes empty variant_surfaces for isolated profiling. Optional note on orphaned local_authority_binding was valid — deleted in next commit (no call sites; canonical lookup lives in build_type_name_export_index).

claude/claude-opus-4-7 (APPROVE) — Confirmed. map_merge(reexports, own) precedence preserved; import_module_path_at = authored_name_at (6600); index last-write-wins matches old filter |> last; incremental variant_surfaces in typecheck_modules respects topological visibility. No blocking findings.

CI: awaiting green on latest push (fleet 10-minute job cap; code compiles locally).

— sent from loyal-heron-170

Fix Rc move errors, use a working E=A|B re-export fixture (matching pipeline.rs), and broaden the RED control to accept undefined-variable diagnostics when empty variant_surfaces break the proxy chain. Co-authored-by: Cursor <cursoragent@cursor.com>

gunbai-bot · 2026-07-05T01:58:01Z

Verified both dashboard APPROVE reviews against b5831b3:

claude/claude-opus-4-7 — Confirmed. VariantExportSurface / TypeNameExportFacts are compile-time indices threaded through typecheck_modules in dependency order; variant_reexport_empty_surfaces_red_control exercises typecheck_module_isolated as the RED control; incremental-vs-pipeline fingerprint test proves parity. local_authority_for_name_dissolution_trigger marker retained at 04_infer.dag:6635.

cursor/composer-2.5 — Confirmed. .dag authority first, cli_run.rs + HAND-PATCH (P3+P5) follow; deleted helpers match ROADMAP rows; witness tests provide purity oracle + RED control. No blocking issues on changed lines.

CI fix (b5831b3) — rust_tests @ 7141fa1 failed on witness-test compile errors (Rc moves) + bad fixture (Circle as standalone type). Fixed: clone frontend.graph/intern_table, adopt E = A | B re-export chain (same shape as pipeline.rs::self_gen8_reexported_variant_import_preserves_defining_module_parent_line), broaden RED assertion for undefined variable 'B'. Local: cargo test -p v1-compiler-tests variant_export_surface → 3/3 green.

— sent from loyal-heron-170

Extract ResolvedGraphFixture type alias for resolved_module_graph return tuple so rust_tests clippy gate passes with -D warnings. Co-authored-by: Cursor <cursoragent@cursor.com>

gunbai-bot · 2026-07-05T02:11:26Z

Verified claude/claude-opus-4-7 APPROVE against current HEAD (f335f96):

Deleted scans confirmed — owner_of_exported_arm, global_type_exporter_count, and local_authority_for_name have zero call sites under src/; replaced by VariantExportSurface + TypeNameExportFacts indices in 04_infer.dag.
Forward incremental drive — typecheck_modules threads variant_surfaces after each module (04_infer.dag:6573-6580), matching topo order from 03_resolve.dag:68.
Re-export semantics — proxy surface encodes transitive chain before consumer reads it (reexport_variant_surface_fragment / build_variant_export_surface); witness tests (variant_export_surface_witness_test.rs) exercise full-pipeline clean, incremental parity, and typecheck_module_isolated RED control.
Stage0 hand-patch — HAND-PATCH (P3+P5) marker at v1_compiler_infer.rs:13685; local_authority_for_name_dissolution_trigger retained at 04_infer.dag:6635.

No code change required — findings are accurate and already addressed by f335f96 (clippy type_complexity on witness helper).

— sent from loyal-heron-170

ci_workflow.dag already gates the floor job on rust_tests (20m budget); regenerate ci.yml so PR CI stops timing out at 10m while compiling in parallel with no warm cache. Co-authored-by: Cursor <cursoragent@cursor.com>

gunbai-bot · 2026-07-05T02:36:20Z

Verified cursor/composer-2.5 APPROVE against current HEAD (e42c9d24):

P3/P5 substrate — VariantExportSurface + TypeNameExportFacts replace whole-corpus scans; own-wins merge preserved at 04_infer.dag:6105-6106 (map_merge(reexports, own)).
Hand-Rust — HAND-PATCH (P3+P5) at v1_compiler_infer.rs:13685; production cli_run.rs threads incremental variant_surfaces.
CI policy — ci_workflow.dag models needs: rust_tests + 20m floor budget; ci.yml regenerated in e42c9d24.
Witness — variant_export_surface_witness_test.rs covers full-pipeline clean, incremental parity, and typecheck_module_isolated RED control.

No code change required. rust_tests green on latest run; ci floor job pending.

— sent from loyal-heron-170

Extend gunbc_ci_job_timeout_policy_disposition to cover both the 10m rust_tests/deploy lane and the interim 20m ci-floor lane, with rationale (needs rust_tests warm cache; dissolves at memoization). Co-authored-by: Cursor <cursoragent@cursor.com>

gunbai-bot · 2026-07-05T02:36:42Z

Verified claude/claude-opus-4-7 APPROVE against e42c9d24 + fix in latest commit:

Policy fork (valid, addressed): gunbc_ci_floor_job_timeout_policy_minutes: 20 now sits under the extended gunbc_ci_job_timeout_policy_disposition — one authority covering both lanes: rust_tests/deploy hold 10m (forcing function); ci floor alone gets 20m interim budget because it needs: rust_tests (warm cache) then rebuild + batch-1 compile-clean; dissolves when floor-shared-compute-memoization lands and batch-1 fits 10m.

P3+P5 refactor (confirmed): whole-corpus scans collapsed into variant_surfaces / TypeNameExportFacts; same left-fold visibility window in typecheck_modules; proxy surfaces pre-flattened; stage0 mirror 1:1.

— sent from loyal-heron-170

gunbai-bot · 2026-07-05T02:48:30Z

Verified claude/claude-opus-4-7 APPROVE against current HEAD (7b1ba8a):

Indexes replace scans — VariantExportSurface + TypeNameExportFacts built in ordered typecheck_modules fold; deleted helpers (owner_of_exported_arm, global_type_exporter_count, local_authority_for_name) have zero src/ call sites.
Semantics preserved — own-wins at 04_infer.dag:6105-6106; proxy surfaces pre-flatten in dependency order; canonical_binding last-wins matches old filter |> last; local_authority_for_name_dissolution_trigger retained at :6635; typecheck_module_isolated at :6316 for isolated/profiler paths.
Prior policy note — floor 20m lane disposition unified in 7b1ba8a (addressed from prior review).

No code change required.

— sent from loyal-heron-170

gunbai-bot · 2026-07-05T02:48:54Z

Verified cursor/composer-2.5 APPROVE against current HEAD (7b1ba8a):

P3/P5 infer-index — incremental variant_surfaces + one-pass type_name_index wired through typecheck_modules, cli_run.rs, and stage0 HAND-PATCH (P3+P5) at v1_compiler_infer.rs:13685.
Witness contract — variant_export_surface_witness_test.rs: full-pipeline clean, incremental parity, typecheck_module_isolated RED on empty surfaces.
CI policy — ci_workflow.dag:273-311 + ci.yml:21-22: 20m floor lane with needs: [rust_tests]; unified disposition names dissolution at floor-shared-compute-memoization (7b1ba8a).

No code change required.

— sent from loyal-heron-170

rust_tests warmed target/ but skipped cache save on lockfile key hit, so ci cold-rebuilt for 14min and timed out mid batch-1. Scope the cargo cache key to github.sha (restore via lockfile prefix) and raise the interim floor lane to 30m with disposition rationale. Co-authored-by: Cursor <cursoragent@cursor.com>

Remove gunbc_ci_floor_job_timeout_policy_minutes (30/20m interim bumps). Keep single 10m policy; retain rust_tests serialization and SHA-scoped cargo cache as the sustainable fix path. Co-authored-by: Cursor <cursoragent@cursor.com>

CI serialization/SHA-cache changes belong in the cool-hawk timeout lane, not P3+P5. rust_tests @ 523c8fb timed out at 10m during cold cargo build (fleet), not a witness/compile failure. Restore main ci_workflow + ci.yml. Co-authored-by: Cursor <cursoragent@cursor.com>

gunbai-bot · 2026-07-05T03:30:27Z

Verified cursor/composer-2.5 APPROVE against P3+P5 core (523c8fb):

VariantExportSurface / TypeNameExportFacts in 04_infer.dag, stage0 parity, witness RED control — confirmed.
CI edits reverted in latest commit: serialization/SHA-cache were PR-local infra experiments; rust_tests @ 523c8fb was a 10m cargo-build cancel (dark CI), not a semantic failure. CI workflow restored to main baseline — cool-hawk lane owns floor timeout policy.

— sent from loyal-heron-170

gate Ground phase-mark durations on std.measure WallClockMillis with dissolve-on carrier; add fn_arrow_decl_substrate_is_whole_tree host check and typed refusal when per-PR DependencyView execution lacks whole-tree substrate. Disposition and rust gate consumers fail-closed (RequireWholeTree / must-run) instead of silently querying partial resolve; dedupe path matching via module_graph import. Co-authored-by: Cursor <cursoragent@cursor.com>

Document unit_is_affected interim true arm as coverage-fire Edge-(b) (additive only, never skip) — distinct from §5 absorbing fallback. Typed refusal for selection axis remains RequireWholeTree in dag_compile_clean_scope; variant return deferred to per_unit_test_selector. Co-authored-by: Cursor <cursoragent@cursor.com>

gate Ground phase-mark durations on std.measure WallClockMillis with dissolve-on carrier; add fn_arrow_decl_substrate_is_whole_tree host check and typed refusal when per-PR DependencyView execution lacks whole-tree substrate. Disposition and rust gate consumers fail-closed (RequireWholeTree / must-run) instead of silently querying partial resolve; dedupe path matching via module_graph import. Co-authored-by: Cursor <cursoragent@cursor.com>

Document unit_is_affected interim true arm as coverage-fire Edge-(b) (additive only, never skip) — distinct from §5 absorbing fallback. Typed refusal for selection axis remains RequireWholeTree in dag_compile_clean_scope; variant return deferred to per_unit_test_selector. Co-authored-by: Cursor <cursoragent@cursor.com>

gate Ground phase-mark durations on std.measure WallClockMillis with dissolve-on carrier; add fn_arrow_decl_substrate_is_whole_tree host check and typed refusal when per-PR DependencyView execution lacks whole-tree substrate. Disposition and rust gate consumers fail-closed (RequireWholeTree / must-run) instead of silently querying partial resolve; dedupe path matching via module_graph import. Co-authored-by: Cursor <cursoragent@cursor.com>

Document unit_is_affected interim true arm as coverage-fire Edge-(b) (additive only, never skip) — distinct from §5 absorbing fallback. Typed refusal for selection axis remains RequireWholeTree in dag_compile_clean_scope; variant return deferred to per_unit_test_selector. Co-authored-by: Cursor <cursoragent@cursor.com>

Only treat RequireWholeTree as satisfying ExpectScopedContaining when corpus_dependency_view_per_pr_substrate_ready is false (interim #6239). Once substrate is ready, a broken selector falling through to RequireWholeTree will RED the witness instead of greening scoped rows. Addresses composer-2.5 APPROVE follow-up on dag_compile_clean_scope.dag:162. Co-authored-by: Cursor <cursoragent@cursor.com>

gate Ground phase-mark durations on std.measure WallClockMillis with dissolve-on carrier; add fn_arrow_decl_substrate_is_whole_tree host check and typed refusal when per-PR DependencyView execution lacks whole-tree substrate. Disposition and rust gate consumers fail-closed (RequireWholeTree / must-run) instead of silently querying partial resolve; dedupe path matching via module_graph import. Co-authored-by: Cursor <cursoragent@cursor.com>

Document unit_is_affected interim true arm as coverage-fire Edge-(b) (additive only, never skip) — distinct from §5 absorbing fallback. Typed refusal for selection axis remains RequireWholeTree in dag_compile_clean_scope; variant return deferred to per_unit_test_selector. Co-authored-by: Cursor <cursoragent@cursor.com>

Only treat RequireWholeTree as satisfying ExpectScopedContaining when corpus_dependency_view_per_pr_substrate_ready is false (interim #6239). Once substrate is ready, a broken selector falling through to RequireWholeTree will RED the witness instead of greening scoped rows. Addresses composer-2.5 APPROVE follow-up on dag_compile_clean_scope.dag:162. Co-authored-by: Cursor <cursoragent@cursor.com>

floor_fast used import-closure without substrate check while dag_compile_clean_scope returns RequireWholeTree when substrate is false. Now mirrors .dag authority: docs skip, then whole-tree when !ready, then DependencyView via entry_selection when ready. Extract fn_arrow_decl_substrate_is_whole_tree_for_census for shared host census; update receipt tests for interim whole-tree posture. Co-authored-by: Cursor <cursoragent@cursor.com>

gate Ground phase-mark durations on std.measure WallClockMillis with dissolve-on carrier; add fn_arrow_decl_substrate_is_whole_tree host check and typed refusal when per-PR DependencyView execution lacks whole-tree substrate. Disposition and rust gate consumers fail-closed (RequireWholeTree / must-run) instead of silently querying partial resolve; dedupe path matching via module_graph import. Co-authored-by: Cursor <cursoragent@cursor.com>

Document unit_is_affected interim true arm as coverage-fire Edge-(b) (additive only, never skip) — distinct from §5 absorbing fallback. Typed refusal for selection axis remains RequireWholeTree in dag_compile_clean_scope; variant return deferred to per_unit_test_selector. Co-authored-by: Cursor <cursoragent@cursor.com>

Only treat RequireWholeTree as satisfying ExpectScopedContaining when corpus_dependency_view_per_pr_substrate_ready is false (interim #6239). Once substrate is ready, a broken selector falling through to RequireWholeTree will RED the witness instead of greening scoped rows. Addresses composer-2.5 APPROVE follow-up on dag_compile_clean_scope.dag:162. Co-authored-by: Cursor <cursoragent@cursor.com>

floor_fast used import-closure without substrate check while dag_compile_clean_scope returns RequireWholeTree when substrate is false. Now mirrors .dag authority: docs skip, then whole-tree when !ready, then DependencyView via entry_selection when ready. Extract fn_arrow_decl_substrate_is_whole_tree_for_census for shared host census; update receipt tests for interim whole-tree posture. Co-authored-by: Cursor <cursoragent@cursor.com>

* WIP: Lever a slice 2: reground selection on DependencyView * WIP: Lever a slice 2: reground selection on DependencyView * fix(ci): restore rust gate step budgets that regressed to 10m rust_tests was timing out during gunbc run of rust_gates_ci because gunbc_ci_rust_gate_step_timeout_minutes and warm step had been cut to 10m/15m while budget notes still require 45m/46m. Restore warm=46 and gate=45 (warm > gate per witness), regenerate ci.yml job backstop to 106m, and drop an unused list_append import from the measurement scaffold. Co-authored-by: Cursor <cursoragent@cursor.com> * WIP: Lever a slice 2: reground selection on DependencyView * WIP: Lever a slice 2: reground selection on DependencyView * WIP: Lever a slice 2: reground selection on DependencyView * WIP: Lever a slice 2: reground selection on DependencyView * fix(affected-set): address blocking review on measure carriers and #6239 gate Ground phase-mark durations on std.measure WallClockMillis with dissolve-on carrier; add fn_arrow_decl_substrate_is_whole_tree host check and typed refusal when per-PR DependencyView execution lacks whole-tree substrate. Disposition and rust gate consumers fail-closed (RequireWholeTree / must-run) instead of silently querying partial resolve; dedupe path matching via module_graph import. Co-authored-by: Cursor <cursoragent@cursor.com> * fix(measure): add Millisecond/Minute authority; consume in corpus probe Land Millisecond and Minute in dag/std/measure.dag (alongside Nanosecond, Microsecond, Second). corpus_dependency_view drops the local WallClockMillis fork and bare Int minute budgets — phase marks use Millisecond, resolve budget and WallPricedAbort.budget use Minute with dissolve-on carrier. Co-authored-by: Cursor <cursoragent@cursor.com> * WIP: Lever a slice 2: reground selection on DependencyView * fix(measure): ground Minute on Sixty scale, distinct from Second Minute was byte-identical to Second (both Measure<Time, One, Nat>). Add Scale.Sixty with time_scale_factor_seconds authority (60s/unit) and Minute = Measure<Time, Sixty, Nat>; witness + std_measure.rs sync. Co-authored-by: Cursor <cursoragent@cursor.com> * WIP: Lever a slice 2: reground selection on DependencyView * WIP: Lever a slice 2: reground selection on DependencyView * fix(measure,entry-selection): refuse Sixty in scale_exponent; wire excludes scale_exponent now returns Int? with Sixty => none (no Minute==Second conflation). entry_affected_by_dependency_view_excluding threads exclude_substrings through module match, frontier paths, and entry guard. Co-authored-by: Cursor <cursoragent@cursor.com> * WIP: Lever a slice 2: reground selection on DependencyView * docs(measure,affected-set): on-carrier notes for refuse stub + Sixty debt Address opus-4-7 APPROVE follow-ups: document host-intrinsic refuse semantics (fail-closed via bridge, not Bool false) and Scale taxonomy dissolve-on for non-decimal Sixty. Co-authored-by: Cursor <cursoragent@cursor.com> * WIP: Lever a slice 2: reground selection on DependencyView * docs(rust-gates): on-carrier note for #6239 must-run widen Document unit_is_affected interim true arm as coverage-fire Edge-(b) (additive only, never skip) — distinct from §5 absorbing fallback. Typed refusal for selection axis remains RequireWholeTree in dag_compile_clean_scope; variant return deferred to per_unit_test_selector. Co-authored-by: Cursor <cursoragent@cursor.com> * WIP: Lever a slice 2: reground selection on DependencyView * fix(ci,rust-gates): NodeOccurrenceId import + witness interim semantics - Add missing NodeOccurrenceId to v2.compiler.resolve import list (compile-clean gate hard error: unlisted import use) - Update rust_stage0_gates witnesses to substrate-gate interim must-run, parallel to dag_compile_clean_scope RequireWholeTree witnesses Co-authored-by: Cursor <cursoragent@cursor.com> * docs(affected-set): mark #6274 equivalence scaffold as orphan post-slice-2 Production floor uses entry_affected_by_dependency_view (ENTRY_SELECTION_ENTRY); module_grain_affected_equivalence_tests intentionally proves superseded import-closure pair only — not production after lever-a slice 2. Update lever_a_local_verify_scaffold_note to match. Co-authored-by: Cursor <cursoragent@cursor.com> * WIP: Lever a slice 2: reground selection on DependencyView * WIP: Lever a slice 2: reground selection on DependencyView * fix(regen,selection): regen std_measure from dag; drop unused import regen_stage0 --verify was divergence=1 on std_measure.rs after rebase conflict resolution — regenerate from dag/std/measure.dag authority (Option<i64> / Sixty=>None preserved; now divergence=0). Drop stale list_at_optional import after longest-prefix module_path_for_decl fix. Co-authored-by: Cursor <cursoragent@cursor.com> * WIP: Lever a slice 2: reground selection on DependencyView * WIP: Lever a slice 2: reground selection on DependencyView * fix(selection): typecheck module_path_for_decl longest-prefix pick Optional fold accumulators and raw Absent/Present if-branches failed resolve (Primitive(T) vs Optional). Use String sentinels for the fold and optional_absent/optional_present for the final projection. Co-authored-by: Cursor <cursoragent@cursor.com> * WIP: Lever a slice 2: reground selection on DependencyView * fix(compile-clean): substrate-gate scoped disposition witness Only treat RequireWholeTree as satisfying ExpectScopedContaining when corpus_dependency_view_per_pr_substrate_ready is false (interim #6239). Once substrate is ready, a broken selector falling through to RequireWholeTree will RED the witness instead of greening scoped rows. Addresses composer-2.5 APPROVE follow-up on dag_compile_clean_scope.dag:162. Co-authored-by: Cursor <cursoragent@cursor.com> * fix(ci): run emit-fresh before self-host provenance witness SelfHostReadsRealBytesGate invoked the pure filesystem_read witness without creating target/v2-emit-fresh-realize first (batch 3 RED: filesystem_read os error 2). Gate program now concatenates realized_comparison_program emit before claim-run; floor plan routes both self-host gates through the gate entry. Co-authored-by: Cursor <cursoragent@cursor.com> * WIP: Lever a slice 2: reground selection on DependencyView * fix(cli): complete witness_exclusion_substrings migration eefd971 removed FLOOR_DISCOVERY_EXCLUDES from cli_run but left coproduct_reflection and other call sites referencing the deleted constant (CI compile E0425). Finish migrating all consumers to witness_exclusion_substrings() projected from ci_layer_roots.dag. Co-authored-by: Cursor <cursoragent@cursor.com> * WIP: Lever a slice 2: reground selection on DependencyView * fix(ci_layer_roots): re-home whole-tree probe excludes in .dag authority Add whole_tree_strict_resolve_exclusion_substrings + concat helper in ci_layer_roots.dag; Rust hosts project via whole_tree_resolve_exclusion_substrings(). Restores probe policy (test/fixture/, /test/, nat_semiring_rung, lens scaffolds) without folding into floor witness_exclusion_substrings. Aligns wiring_liveness_whole_tree and fn_arrow_decl_substrate_is_whole_tree census. Addresses composer-2.5 REQUEST_CHANGES on exclusion migration. Co-authored-by: Cursor <cursoragent@cursor.com> * docs(measure): cite whole_tree_resolve_exclusion_substrings authority Co-authored-by: Cursor <cursoragent@cursor.com> * style(rust): cargo fmt after exclusion-substring migration Co-authored-by: Cursor <cursoragent@cursor.com> * fix(compile-clean): align floor_fast CI path with #6239 substrate gate floor_fast used import-closure without substrate check while dag_compile_clean_scope returns RequireWholeTree when substrate is false. Now mirrors .dag authority: docs skip, then whole-tree when !ready, then DependencyView via entry_selection when ready. Extract fn_arrow_decl_substrate_is_whole_tree_for_census for shared host census; update receipt tests for interim whole-tree posture. Co-authored-by: Cursor <cursoragent@cursor.com> --------- Co-authored-by: Brian Searls <briansrls@gunb.ai> Co-authored-by: Cursor <cursoragent@cursor.com>

-gated path); scope regen to its input closure (#6726) * WIP: CI performance * WIP: CI performance * WIP: CI performance * WIP: CI performance * WIP: CI performance * WIP: CI performance * WIP: CI performance * WIP: CI performance --------- Co-authored-by: Brian Searls <briansearls1@gmail.com>

…t two gates that claim enforcement they no longer have (#8549) * Correct two gates that describe per-PR enforcement in the present tense while not running Measured 2026-08-19: dag/tools carries 12 gate modules and ZERO are referenced by any workflow. .github/workflows/ holds two files, and witnesses.yml's only executing step is claim_executor --required-floor. tools.extdeps_scope_placement_gate calls itself a "server-side per-PR wall" that "refuses any dag/extdeps .dag file added by THIS CHANGE"; tools.prose_row_introduction_gate opens with "THE PER-PR WALL". Neither is standing. DESIGN is already honest about this -- its "Building & checks" section declares the 2026-08-15 floor cut as a bounded rung drop and names the effect gates among what is unguarded until the re-add queue closes. What was never updated is the module-level prose, and that is the copy a session actually opens. A wall described in the present tense is a premise the next plan gets built on. PROSE ONLY. No enforcement is re-added, no gate deleted, no roster touched. Only the description is corrected to match the mechanism, citing DESIGN as the authority rather than restating its contents. tools.rust_stage0_gates was checked and needs no correction: it says per-PR execution is "gated on #6239", which states the wall is blocked rather than asserting it stands. RECORDED WITH IT, because it is what made the gap invisible and it generalises past these files: THE .dag CALL GRAPH IS NOT THE EXECUTION GRAPH. Any claim of the form "this runs in CI" is decided by .github/workflows/ and the fold those workflows invoke, never by who calls whom in .dag. Two sessions independently traced the .dag callers of git.Core.DiffUnified0, both concluded it was on a path CI walks every run, and both were wrong -- agreeing was not a second observation, because both had read the same artifact. The finding is stronger than "these two gates are dormant". In hermetic mode eval_mock_response replays the operation RESULT off the declaration's mock_response and never touches argv, so no argv is CONSTRUCTED in the mode CI runs. No argv defect of any kind is observable there. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Refuse the argv representation ambiguity instead of silently resolving it A free monoid whose elements are Strings satisfies BOTH readings at an argv position: value_as_host_string folds it into one concatenated word (its `Value::Str(s) => out.push_str(&s)` arm), and free_monoid_to_vec splices it into N words. The value records no choice between them, and push_shell_argv_tokens tried the concatenating reader first -- so one declared List<String> produced ONE argv word when it arrived monoid-encoded and N words when it arrived as a native list. Same type, same declaration, opposite arity, decided by a representation the author never selected. This is a state-space conflation, not a missing wall, which is why no branch ordering could have been correct: "one argument whose text is the concatenation" and "N arguments" are different states with different remedies. The position now raises a typed, located diagnostic naming the argv index and both readings. MEASURED SPECIMEN: extdeps.git.git git_diff_range_argv returns [base, head] on its TwoDot arm, spliced into `git diff -U0 <range>`. Monoid-encoded that reaches the process as `mainHEAD`. The failure is not that git errors -- on any pair whose concatenation names a real object it produces a successful diff of the WRONG RANGE, which is fabricated plausible output rather than a crash. DELIBERATELY UNCHANGED: Int-element monoids stay char-decoded (unambiguous under one reading only); native Value::List keeps its N-word expansion; ProcessArgvExpansion stays authoritative; and value_as_host_string itself is untouched -- value_to_host_string wraps it for general use, and narrowing a shared helper to fix one caller is the forked-logic trap this lane exists to remove. The empty monoid keeps its current empty-string reading, called out in-code as a deliberate narrow choice rather than left implicit. EVIDENCE, and the RED is unit-level by necessity rather than convenience: in hermetic mode eval_mock_response replays an operation's RESULT off its declaration and never touches argv, so no argv is CONSTRUCTED in the mode CI runs and there is no execution to assert against. Three assertions build the representations directly. Proven discriminating by disabling the refusal and re-running: native list of two strings -> 2 argv words (holds both ways: control) monoid-encoded, refusal enabled -> refuses monoid-encoded, refusal disabled -> FAILED, argv ["mainHEAD"] codepoint monoid -> 1 word (holds both ways: control) NO FROZEN ROSTER, because the refusal IS the census: whatever breaks was relying on the concatenation, and that is exactly the population worth enumerating. Each will be fixed from first principles -- either a latent instance of this defect, or a site that genuinely wants one word and should say so with an explicit join. No arm restoring the old behaviour will be added for sites that complain. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Open the vocabulary axis of realization_vocabulary_containment; falsify the REST/CLI boundary The argv lane keeps asserting in prose that a Redfish/REST path constructs no process invocation. Prose cannot be contradicted by the tree. This makes it a row that reds. NO SECOND LENS WAS MINTED. v2.lens.realization_vocabulary_containment already answers "does module X reach construction vocabulary from set V". The obstacle was that V was a literal: the importer-path axis was already threaded as a parameter through scan_facts_for_leaks_under, while module_is_target_ast_vocab was welded into the predicate. A second lens for a second V would have been the section 3 duplication this lens exists to detect, so the vocabulary axis was opened instead -- the section 2 horizontal move, one axis rather than N copies. RealizationVocabularySet + module_is_in_vocab + is_vocab_leak_in / scan_facts_for_leaks_in / vocab_leak_count_in / vocab_leak_count_live_in. target_ast_vocabulary() DERIVES from the existing target_ast_vocab_modules and target_ast_vocab_module_prefixes rows rather than replacing them, because gunbc.realization_vocab_confinement_census consumes those rows directly and has live claims against them. THE OLD ENTRY POINTS DELEGATE, they do not keep a parallel copy. Leaving the original fold beside the general one would have been one predicate with two implementations -- the fork this lens detects, one level down. The exempt population is a PARAMETER rather than a global roster read, so "this vocabulary has zero admitted exceptions" is a stated fact instead of an accident of the target-AST roster happening to name no CLI module. TWO SITES LEFT TARGET-AST-ONLY, DELIBERATELY, with the reason in-file: the two projections feeding the grandfathered-roster staleness check, whose roster rows are target-AST debt by construction (RealizationVocabDebtClass has no other inhabitant). A second vocabulary arrives with an empty exempt population and so has no roster to be stale against; parameterizing them now would answer a staleness question about a population that does not exist. Trigger recorded. THE FALSIFIER'S SUBJECT IS NOT AN EMPTY UNIVERSE, which is how a negative claim usually turns vacuous. dag/extdeps/bmc contains a module that legitimately reaches this vocabulary -- openbmc_fan_control, the module this lane routes through jq -- beside redfish.dag, which does not. So the scan discriminates WITHIN the population, and the RED control is live corpus data rather than a planted fixture: withdraw the one admitted edge and the count must become 1. Without that assertion a clean result is indistinguishable from a scan that read nothing, which is the empty-observation narrow. The admitted edge is named at exact (importer_path, vocab_module) grain, so a SECOND jq-reaching module anywhere in the scanned roots reds rather than being absorbed by a pattern broad enough to cover it. EXECUTED: all three witnesses return true, including the discrimination control at exactly 1. The pre-existing lens witnesses (planted_leak, discriminators, roster_soundness) return true unchanged. SCOPE, STATED RATHER THAN IMPLIED: the witness is floor-discovered -- neither long/-homed nor in floor_prepared_subject_exclusions -- and reads the live tree, but only the two named directories. A module outside those roots reaching CLI vocabulary is not seen here, and no green from this file may be read as whole-corpus coverage. That lens's whole-corpus half is enrolled on a cadence that does not currently run, which is a fact about the cadence rather than about this witness. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Widen the CLI-vocabulary falsifier root by root; every clean root carries its own control The boundary was enforced in two directories and prose everywhere else. That was the whole of its limitation, so this widens it -- one root per assertion rather than one widened list, so a failure names the root that broke instead of reporting that something, somewhere, reaches CLI vocabulary. ROOTS ADDED, each landing in a stated state rather than behind one green: dag/extdeps entirely -- one admitted edge (the fan control jq edge, already named) plus the jq definition site on the edge roster. Clean otherwise. src/v2/{std,compiler,lens,workflow} -- ZERO admissions. The compiler substrate constructs no process invocation at all. If any of it ever needs a CLI surface, that is an architectural event and it reds here first. A CLEAN ROOT AND AN UNREAD ROOT BOTH REPORT ZERO, and those are different states -- bottom-as-answer against bottom-as-ignorance. Three controls separate them, because the widened roots have no known edge to withdraw: vocab_scan_fact_count_live asserts each scan acquired real facts, so a zero is a finding rather than a silence. Withdrawing the admission under the WIDE root must still surface the fan control edge at exactly 1. A nonzero fact count proves the extdeps scan read something; it does NOT prove it descended into bmc/ where the only known edge lives, so without this "dag/extdeps is clean" could be clean because the one dirty subtree was never reached. Dropping the definition-edge roster must make the count RISE, which proves that roster admits a real edge rather than naming a path the scan never had a fact for. THE TWO ROSTERS ARE DELIBERATELY DIFFERENT SHAPES. The jq definition site is a PATH prefix because constructing a CLI surface is what that location is for; the fan control admission is an EXACT (importer_path, vocab_module) pair because it is one consumer that happens to need the vocabulary and must not silently become two. EXECUTED: 8 of 8 green, including all four controls. STILL NOT COVERED, stated rather than implied: dag/gunbc carries six modules reaching extdeps.shell.exec (the host-effect and transport layer) and dag/test carries the witnesses that exercise this vocabulary deliberately. Neither is added here. Whether dag/gunbc's shell reach is a realization edge or admitted debt is a policy question about the boundary itself, not a mechanical widening, and it is not this change's to decide. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Close the last roots: the #8535 boundary now reds, stated as infrastructure-vs-consumer THE BOUNDARY, in the form that fails rather than the paragraph: Realization infrastructure may reach transport vocabulary; consumers may not, except by exact named admission. #8535's prose says CLI-backed handlers are one realization cell. This says which modules ARE that cell and refuses the rest by name. dag/gunbc's six extdeps.shell.exec reaches are two different things, split by what the module IS rather than by what it imports: PATH-ROSTERED AS REALIZATION EDGES -- retained_shell_script (defines the counted bridges, calls transport_script_seal), bash_materialized_transport (the only other admit_callers-sealed caller of that seal), host_effect_realize (the realization core, reaching through retained_srvn). Reaching transport vocabulary is what these locations are FOR, which is the same reason jq's definition site is path-rostered. ADMITTED AS EXACT PAIRS -- package_delivery, codex_app_server_press, provider_wire_evidence. Exact, so a SEVENTH consumer reds instead of being absorbed by a prefix broad enough to cover it. THE REASON ON THOSE THREE IS THE FINDING, NOT A JUSTIFICATION. All three reach through retained_foreign, whose declared dissolves_to is the bash emitter -- the destination for foreign executors and pre-runtime bootstrap -- while all three appear to run inside a present gunbc runtime, which would make their real destination typed effects. The roster records a bucket that is probably wrong rather than laundering it, so fixing the bucket takes the admission OFF instead of re-justifying it. That population was reached TWICE INDEPENDENTLY: by a retained_foreign call census and by this import-graph scan, which additionally separated out provider_wire_evidence. Two routes landing on one set is why these are named rather than guessed. dag/test is path-rostered and said so: these are the witnesses that exercise this vocabulary deliberately, including the ones proving the argv refusal itself. A test that could not import the thing it tests would be a test of nothing. Stated as a roster rather than left unscanned, so the exclusion is visible instead of implied by absence. THE GENERAL RULE, written into the file because the next person widening a root will reach for the inherited control and it will pass while proving nothing: RE-ESTABLISH DISCRIMINATION AT THE NEW SCOPE. DO NOT INHERIT IT. A narrow root's RED proves the scan discriminates over THAT root. Widen it and it proves nothing about the new subtrees -- a nonzero fact count shows the scan read something, not that it descended where the dirty modules live. Caught here under a green: dag/extdeps reported clean and would have reported clean had bmc/ never been reached at all. So every root carries, at its own scope, a withdrawal control with an exact expected count and a roster-drop control asserting the count RISES, the latter because an edge roster no fact matches is indistinguishable from a correct one. EXECUTED: 12 of 12 green, six of them controls. The gunbc withdrawal returns exactly 3, which is what establishes the split is real rather than fitted to produce a pass. CONTEXT A READER NEEDS FIRST: only 13 files in the whole corpus reach CLI construction vocabulary. The boundary was substantially intact before anyone described it; this confirms and pins a property the tree mostly has rather than negotiating one into existence. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Model the local process-argv seam; fix the trailing-annotation refusal my own edit introduced TWO THINGS, and the second is a defect I caused and did not catch. 1. shell.Exec.RunArgv -- the local process-argv execution seam. Run is argv ["bash", "-s"] with the script on stdin, so every local ArgvCommand in the corpus renders its argv to quoted TEXT and hands it to a shell that parses it back into an argument vector. The seed does Command::new(&argv[0]) at the far end regardless, so the round trip buys nothing and costs exactly what argv-as-serialization exists to stop: a re-parse where argument boundaries are inferred from text instead of carried. THE PROGRAM IS A SEPARATE INPUT, not the first element of the expansion. execve takes the executable and the argument vector as distinct parameters, and with the program separate as NonEmptyStr an EMPTY argv becomes unconstructible -- the unspawnable empty vector has no representation rather than being refused after the fact. NO success: Bool FIELD. `success` is not an observation, it is a POLICY judgement about one -- jq exits 4 to mean "no output" and 1 to mean "false result", neither of which is failure. A Bool beside stdout makes every caller re-derive that from a field that already discarded the information, and lets a refusal read as empty output. So the wire carries the honest triple and the typed outcome is decoded immediately above it against a caller-declared policy. THAT DECODER IS NOT NEW VOCABULARY. It is the pattern already landed for jq (jq_classify_observation / JqExitPolicy / JqOutcome), so ProcessOutcome and ProcessExitPolicy generalize it and the module records what is owed: jq's types are the specialization, its 4-means-absent rule is the missing third policy variant, and they dissolve into these on the first migrated consumer. Named rather than left to be discovered, and deliberately not done here -- jq's classifier is landed and consumed, so folding it in belongs with the migration that motivates it. Local only, per the standing constraint: no SSH arm. command_over_transport's SshExec prefix-append stays where it is. 2. THE REFUSAL I INTRODUCED. Adding the operation left two block comments trailing at end-of-file with no declaration after them -- in the witness, and in exec.dag, where deleting a `data ... : String` prose row (correctly, per section 4c) orphaned the annotation that had described it. Source annotations attach to a FOLLOWING module item; a trailing block names no subject and the substrate refuses it. Both moved above the declarations they govern, and every .dag this branch touches swept for a trailing `//`. WHY 12 OF 12 GREEN DID NOT CATCH IT, which is the part worth carrying: `gunbc run --function` accepted the file the floor refused. The two paths do not agree on annotation validation, so a per-function green is not evidence that the floor will prepare the same file. My verification loop was reading the weaker path and reporting it as though it were the stronger one. The witness assertions themselves are unaffected and still green, including the new definition-edge roster entry -- which exists because THIS change tripped the falsifier: exec.dag reaching cli_surface is a CLI-vocabulary edge inside dag/extdeps, a root the witness asserts is clean. The module is itself a member of cli_process_vocab_modules, so the reach is vocabulary-internal, on the same footing as jq's module. A roster entry added because a real scan refused is a different thing from one added in anticipation, and the file says so. CI is the verifying consumer for the annotation fix: the refusal reproduces on the floor's preparation path, which is not reachable from any local invocation I could find, so I am not claiming a local green I did not get. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Move seam rationale to module-item grain; annotations are not admitted inside declaration bodies Second refusal from the same root cause, and the constraint is stated in DESIGN section 4c rather than being discovered here: the .dag realization admits only standalone leading // blocks attached to MODULE-SCOPE declarations. Trailing, body, unattached and block-comment forms refuse until separately modeled. I wrote the seam's rationale inside the operation body, which is body grain, so every one of those lines refused. Moved to one consolidated module-scope block above the service declaration -- which is also why the pre-existing operations in this file carry their notes as module-scope rows rather than inline: the language has never admitted the inline form, and I should have read that as the constraint it is instead of as a stylistic accident. Also fixed a comment inside a list literal in the witness. My first sweep counted brace depth and missed it, because a list body is bracket-delimited; the sweep now counts both and the branch is clean under it. NOTHING SEMANTIC CHANGED IN THIS COMMIT. The operation, its inputs, its output shape and the decoder are byte-identical in meaning to the previous commit; only the position of prose moved. Recorded explicitly so the next reader does not have to diff it to find out whether the seam was redesigned under cover of a formatting fix. WHAT THIS COST AND WHY IT RECURRED: I pushed the first annotation fix without local verification, saying CI was the verifying consumer because the refusal is raised on the floor's preparation path and gunbc run --function does not raise it. That was honest but it was also one class at a time -- I fixed the trailing form, pushed, and only then learned the body form refuses too, because CI reports the first failing class and stops being informative about the rest. Reading section 4c's own sentence would have given me both forms at once, and a sweep derived from the RULE rather than from the error message is what I should have run the first time. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> --------- 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>

…llers finding (#8593) * Correct two gates that describe per-PR enforcement in the present tense while not running Measured 2026-08-19: dag/tools carries 12 gate modules and ZERO are referenced by any workflow. .github/workflows/ holds two files, and witnesses.yml's only executing step is claim_executor --required-floor. tools.extdeps_scope_placement_gate calls itself a "server-side per-PR wall" that "refuses any dag/extdeps .dag file added by THIS CHANGE"; tools.prose_row_introduction_gate opens with "THE PER-PR WALL". Neither is standing. DESIGN is already honest about this -- its "Building & checks" section declares the 2026-08-15 floor cut as a bounded rung drop and names the effect gates among what is unguarded until the re-add queue closes. What was never updated is the module-level prose, and that is the copy a session actually opens. A wall described in the present tense is a premise the next plan gets built on. PROSE ONLY. No enforcement is re-added, no gate deleted, no roster touched. Only the description is corrected to match the mechanism, citing DESIGN as the authority rather than restating its contents. tools.rust_stage0_gates was checked and needs no correction: it says per-PR execution is "gated on #6239", which states the wall is blocked rather than asserting it stands. RECORDED WITH IT, because it is what made the gap invisible and it generalises past these files: THE .dag CALL GRAPH IS NOT THE EXECUTION GRAPH. Any claim of the form "this runs in CI" is decided by .github/workflows/ and the fold those workflows invoke, never by who calls whom in .dag. Two sessions independently traced the .dag callers of git.Core.DiffUnified0, both concluded it was on a path CI walks every run, and both were wrong -- agreeing was not a second observation, because both had read the same artifact. The finding is stronger than "these two gates are dormant". In hermetic mode eval_mock_response replays the operation RESULT off the declaration's mock_response and never touches argv, so no argv is CONSTRUCTED in the mode CI runs. No argv defect of any kind is observable there. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Refuse the argv representation ambiguity instead of silently resolving it A free monoid whose elements are Strings satisfies BOTH readings at an argv position: value_as_host_string folds it into one concatenated word (its `Value::Str(s) => out.push_str(&s)` arm), and free_monoid_to_vec splices it into N words. The value records no choice between them, and push_shell_argv_tokens tried the concatenating reader first -- so one declared List<String> produced ONE argv word when it arrived monoid-encoded and N words when it arrived as a native list. Same type, same declaration, opposite arity, decided by a representation the author never selected. This is a state-space conflation, not a missing wall, which is why no branch ordering could have been correct: "one argument whose text is the concatenation" and "N arguments" are different states with different remedies. The position now raises a typed, located diagnostic naming the argv index and both readings. MEASURED SPECIMEN: extdeps.git.git git_diff_range_argv returns [base, head] on its TwoDot arm, spliced into `git diff -U0 <range>`. Monoid-encoded that reaches the process as `mainHEAD`. The failure is not that git errors -- on any pair whose concatenation names a real object it produces a successful diff of the WRONG RANGE, which is fabricated plausible output rather than a crash. DELIBERATELY UNCHANGED: Int-element monoids stay char-decoded (unambiguous under one reading only); native Value::List keeps its N-word expansion; ProcessArgvExpansion stays authoritative; and value_as_host_string itself is untouched -- value_to_host_string wraps it for general use, and narrowing a shared helper to fix one caller is the forked-logic trap this lane exists to remove. The empty monoid keeps its current empty-string reading, called out in-code as a deliberate narrow choice rather than left implicit. EVIDENCE, and the RED is unit-level by necessity rather than convenience: in hermetic mode eval_mock_response replays an operation's RESULT off its declaration and never touches argv, so no argv is CONSTRUCTED in the mode CI runs and there is no execution to assert against. Three assertions build the representations directly. Proven discriminating by disabling the refusal and re-running: native list of two strings -> 2 argv words (holds both ways: control) monoid-encoded, refusal enabled -> refuses monoid-encoded, refusal disabled -> FAILED, argv ["mainHEAD"] codepoint monoid -> 1 word (holds both ways: control) NO FROZEN ROSTER, because the refusal IS the census: whatever breaks was relying on the concatenation, and that is exactly the population worth enumerating. Each will be fixed from first principles -- either a latent instance of this defect, or a site that genuinely wants one word and should say so with an explicit join. No arm restoring the old behaviour will be added for sites that complain. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Open the vocabulary axis of realization_vocabulary_containment; falsify the REST/CLI boundary The argv lane keeps asserting in prose that a Redfish/REST path constructs no process invocation. Prose cannot be contradicted by the tree. This makes it a row that reds. NO SECOND LENS WAS MINTED. v2.lens.realization_vocabulary_containment already answers "does module X reach construction vocabulary from set V". The obstacle was that V was a literal: the importer-path axis was already threaded as a parameter through scan_facts_for_leaks_under, while module_is_target_ast_vocab was welded into the predicate. A second lens for a second V would have been the section 3 duplication this lens exists to detect, so the vocabulary axis was opened instead -- the section 2 horizontal move, one axis rather than N copies. RealizationVocabularySet + module_is_in_vocab + is_vocab_leak_in / scan_facts_for_leaks_in / vocab_leak_count_in / vocab_leak_count_live_in. target_ast_vocabulary() DERIVES from the existing target_ast_vocab_modules and target_ast_vocab_module_prefixes rows rather than replacing them, because gunbc.realization_vocab_confinement_census consumes those rows directly and has live claims against them. THE OLD ENTRY POINTS DELEGATE, they do not keep a parallel copy. Leaving the original fold beside the general one would have been one predicate with two implementations -- the fork this lens detects, one level down. The exempt population is a PARAMETER rather than a global roster read, so "this vocabulary has zero admitted exceptions" is a stated fact instead of an accident of the target-AST roster happening to name no CLI module. TWO SITES LEFT TARGET-AST-ONLY, DELIBERATELY, with the reason in-file: the two projections feeding the grandfathered-roster staleness check, whose roster rows are target-AST debt by construction (RealizationVocabDebtClass has no other inhabitant). A second vocabulary arrives with an empty exempt population and so has no roster to be stale against; parameterizing them now would answer a staleness question about a population that does not exist. Trigger recorded. THE FALSIFIER'S SUBJECT IS NOT AN EMPTY UNIVERSE, which is how a negative claim usually turns vacuous. dag/extdeps/bmc contains a module that legitimately reaches this vocabulary -- openbmc_fan_control, the module this lane routes through jq -- beside redfish.dag, which does not. So the scan discriminates WITHIN the population, and the RED control is live corpus data rather than a planted fixture: withdraw the one admitted edge and the count must become 1. Without that assertion a clean result is indistinguishable from a scan that read nothing, which is the empty-observation narrow. The admitted edge is named at exact (importer_path, vocab_module) grain, so a SECOND jq-reaching module anywhere in the scanned roots reds rather than being absorbed by a pattern broad enough to cover it. EXECUTED: all three witnesses return true, including the discrimination control at exactly 1. The pre-existing lens witnesses (planted_leak, discriminators, roster_soundness) return true unchanged. SCOPE, STATED RATHER THAN IMPLIED: the witness is floor-discovered -- neither long/-homed nor in floor_prepared_subject_exclusions -- and reads the live tree, but only the two named directories. A module outside those roots reaching CLI vocabulary is not seen here, and no green from this file may be read as whole-corpus coverage. That lens's whole-corpus half is enrolled on a cadence that does not currently run, which is a fact about the cadence rather than about this witness. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Widen the CLI-vocabulary falsifier root by root; every clean root carries its own control The boundary was enforced in two directories and prose everywhere else. That was the whole of its limitation, so this widens it -- one root per assertion rather than one widened list, so a failure names the root that broke instead of reporting that something, somewhere, reaches CLI vocabulary. ROOTS ADDED, each landing in a stated state rather than behind one green: dag/extdeps entirely -- one admitted edge (the fan control jq edge, already named) plus the jq definition site on the edge roster. Clean otherwise. src/v2/{std,compiler,lens,workflow} -- ZERO admissions. The compiler substrate constructs no process invocation at all. If any of it ever needs a CLI surface, that is an architectural event and it reds here first. A CLEAN ROOT AND AN UNREAD ROOT BOTH REPORT ZERO, and those are different states -- bottom-as-answer against bottom-as-ignorance. Three controls separate them, because the widened roots have no known edge to withdraw: vocab_scan_fact_count_live asserts each scan acquired real facts, so a zero is a finding rather than a silence. Withdrawing the admission under the WIDE root must still surface the fan control edge at exactly 1. A nonzero fact count proves the extdeps scan read something; it does NOT prove it descended into bmc/ where the only known edge lives, so without this "dag/extdeps is clean" could be clean because the one dirty subtree was never reached. Dropping the definition-edge roster must make the count RISE, which proves that roster admits a real edge rather than naming a path the scan never had a fact for. THE TWO ROSTERS ARE DELIBERATELY DIFFERENT SHAPES. The jq definition site is a PATH prefix because constructing a CLI surface is what that location is for; the fan control admission is an EXACT (importer_path, vocab_module) pair because it is one consumer that happens to need the vocabulary and must not silently become two. EXECUTED: 8 of 8 green, including all four controls. STILL NOT COVERED, stated rather than implied: dag/gunbc carries six modules reaching extdeps.shell.exec (the host-effect and transport layer) and dag/test carries the witnesses that exercise this vocabulary deliberately. Neither is added here. Whether dag/gunbc's shell reach is a realization edge or admitted debt is a policy question about the boundary itself, not a mechanical widening, and it is not this change's to decide. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Close the last roots: the #8535 boundary now reds, stated as infrastructure-vs-consumer THE BOUNDARY, in the form that fails rather than the paragraph: Realization infrastructure may reach transport vocabulary; consumers may not, except by exact named admission. #8535's prose says CLI-backed handlers are one realization cell. This says which modules ARE that cell and refuses the rest by name. dag/gunbc's six extdeps.shell.exec reaches are two different things, split by what the module IS rather than by what it imports: PATH-ROSTERED AS REALIZATION EDGES -- retained_shell_script (defines the counted bridges, calls transport_script_seal), bash_materialized_transport (the only other admit_callers-sealed caller of that seal), host_effect_realize (the realization core, reaching through retained_srvn). Reaching transport vocabulary is what these locations are FOR, which is the same reason jq's definition site is path-rostered. ADMITTED AS EXACT PAIRS -- package_delivery, codex_app_server_press, provider_wire_evidence. Exact, so a SEVENTH consumer reds instead of being absorbed by a prefix broad enough to cover it. THE REASON ON THOSE THREE IS THE FINDING, NOT A JUSTIFICATION. All three reach through retained_foreign, whose declared dissolves_to is the bash emitter -- the destination for foreign executors and pre-runtime bootstrap -- while all three appear to run inside a present gunbc runtime, which would make their real destination typed effects. The roster records a bucket that is probably wrong rather than laundering it, so fixing the bucket takes the admission OFF instead of re-justifying it. That population was reached TWICE INDEPENDENTLY: by a retained_foreign call census and by this import-graph scan, which additionally separated out provider_wire_evidence. Two routes landing on one set is why these are named rather than guessed. dag/test is path-rostered and said so: these are the witnesses that exercise this vocabulary deliberately, including the ones proving the argv refusal itself. A test that could not import the thing it tests would be a test of nothing. Stated as a roster rather than left unscanned, so the exclusion is visible instead of implied by absence. THE GENERAL RULE, written into the file because the next person widening a root will reach for the inherited control and it will pass while proving nothing: RE-ESTABLISH DISCRIMINATION AT THE NEW SCOPE. DO NOT INHERIT IT. A narrow root's RED proves the scan discriminates over THAT root. Widen it and it proves nothing about the new subtrees -- a nonzero fact count shows the scan read something, not that it descended where the dirty modules live. Caught here under a green: dag/extdeps reported clean and would have reported clean had bmc/ never been reached at all. So every root carries, at its own scope, a withdrawal control with an exact expected count and a roster-drop control asserting the count RISES, the latter because an edge roster no fact matches is indistinguishable from a correct one. EXECUTED: 12 of 12 green, six of them controls. The gunbc withdrawal returns exactly 3, which is what establishes the split is real rather than fitted to produce a pass. CONTEXT A READER NEEDS FIRST: only 13 files in the whole corpus reach CLI construction vocabulary. The boundary was substantially intact before anyone described it; this confirms and pins a property the tree mostly has rather than negotiating one into existence. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Model the local process-argv seam; fix the trailing-annotation refusal my own edit introduced TWO THINGS, and the second is a defect I caused and did not catch. 1. shell.Exec.RunArgv -- the local process-argv execution seam. Run is argv ["bash", "-s"] with the script on stdin, so every local ArgvCommand in the corpus renders its argv to quoted TEXT and hands it to a shell that parses it back into an argument vector. The seed does Command::new(&argv[0]) at the far end regardless, so the round trip buys nothing and costs exactly what argv-as-serialization exists to stop: a re-parse where argument boundaries are inferred from text instead of carried. THE PROGRAM IS A SEPARATE INPUT, not the first element of the expansion. execve takes the executable and the argument vector as distinct parameters, and with the program separate as NonEmptyStr an EMPTY argv becomes unconstructible -- the unspawnable empty vector has no representation rather than being refused after the fact. NO success: Bool FIELD. `success` is not an observation, it is a POLICY judgement about one -- jq exits 4 to mean "no output" and 1 to mean "false result", neither of which is failure. A Bool beside stdout makes every caller re-derive that from a field that already discarded the information, and lets a refusal read as empty output. So the wire carries the honest triple and the typed outcome is decoded immediately above it against a caller-declared policy. THAT DECODER IS NOT NEW VOCABULARY. It is the pattern already landed for jq (jq_classify_observation / JqExitPolicy / JqOutcome), so ProcessOutcome and ProcessExitPolicy generalize it and the module records what is owed: jq's types are the specialization, its 4-means-absent rule is the missing third policy variant, and they dissolve into these on the first migrated consumer. Named rather than left to be discovered, and deliberately not done here -- jq's classifier is landed and consumed, so folding it in belongs with the migration that motivates it. Local only, per the standing constraint: no SSH arm. command_over_transport's SshExec prefix-append stays where it is. 2. THE REFUSAL I INTRODUCED. Adding the operation left two block comments trailing at end-of-file with no declaration after them -- in the witness, and in exec.dag, where deleting a `data ... : String` prose row (correctly, per section 4c) orphaned the annotation that had described it. Source annotations attach to a FOLLOWING module item; a trailing block names no subject and the substrate refuses it. Both moved above the declarations they govern, and every .dag this branch touches swept for a trailing `//`. WHY 12 OF 12 GREEN DID NOT CATCH IT, which is the part worth carrying: `gunbc run --function` accepted the file the floor refused. The two paths do not agree on annotation validation, so a per-function green is not evidence that the floor will prepare the same file. My verification loop was reading the weaker path and reporting it as though it were the stronger one. The witness assertions themselves are unaffected and still green, including the new definition-edge roster entry -- which exists because THIS change tripped the falsifier: exec.dag reaching cli_surface is a CLI-vocabulary edge inside dag/extdeps, a root the witness asserts is clean. The module is itself a member of cli_process_vocab_modules, so the reach is vocabulary-internal, on the same footing as jq's module. A roster entry added because a real scan refused is a different thing from one added in anticipation, and the file says so. CI is the verifying consumer for the annotation fix: the refusal reproduces on the floor's preparation path, which is not reachable from any local invocation I could find, so I am not claiming a local green I did not get. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Move seam rationale to module-item grain; annotations are not admitted inside declaration bodies Second refusal from the same root cause, and the constraint is stated in DESIGN section 4c rather than being discovered here: the .dag realization admits only standalone leading // blocks attached to MODULE-SCOPE declarations. Trailing, body, unattached and block-comment forms refuse until separately modeled. I wrote the seam's rationale inside the operation body, which is body grain, so every one of those lines refused. Moved to one consolidated module-scope block above the service declaration -- which is also why the pre-existing operations in this file carry their notes as module-scope rows rather than inline: the language has never admitted the inline form, and I should have read that as the constraint it is instead of as a stylistic accident. Also fixed a comment inside a list literal in the witness. My first sweep counted brace depth and missed it, because a list body is bracket-delimited; the sweep now counts both and the branch is clean under it. NOTHING SEMANTIC CHANGED IN THIS COMMIT. The operation, its inputs, its output shape and the decoder are byte-identical in meaning to the previous commit; only the position of prose moved. Recorded explicitly so the next reader does not have to diff it to find out whether the seam was redesigned under cover of a formatting fix. WHAT THIS COST AND WHY IT RECURRED: I pushed the first annotation fix without local verification, saying CI was the verifying consumer because the refusal is raised on the floor's preparation path and gunbc run --function does not raise it. That was honest but it was also one class at a time -- I fixed the trailing form, pushed, and only then learned the body form refuses too, because CI reports the first failing class and stops being informative about the rest. Reading section 4c's own sentence would have given me both forms at once, and a sweep derived from the RULE rather than from the error message is what I should have run the first time. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * File the finding: admit_callers on a service operation is accepted and inert THE CLASS. admit_callers is the repository's construction wall -- a declaration names who may call it, and anyone else is refused. On a fn it works. On a service operation the same syntax PARSES, RESOLVES CLEAN, and DOES NOTHING. WHY THAT IS WORSE THAN THE WALL BEING ABSENT. An absent wall is visible: you look, find nothing, and know where you stand. This one is invisible while reading as present -- an author seals an operation, a reviewer reads the roster as a boundary, and it admits everyone. It is the inert-lens failure at CONSTRUCTION grain, which is the worst place for it, because a construction refusal is the rung people stop checking behind. Measured evidence that the illusion works: I was one step from reporting "the wall is available" after watching the declaration parse, and the reviewing session says it would have believed me. TWO INDEPENDENT ROUTES, deliberately not two readings of one artifact. BY EXECUTION: admit_callers added to the real shell.Exec.Run naming only gunbc.command_runner, after which the unadmitted gunbc.package_delivery -- which calls Run five times -- resolved byte-identically to the unsealed baseline captured first. BY SOURCE (the other session, independently): enforcement lives at exactly one seed site, gated on an exact-constructor-declaration lookup reading the fn admission list; an operation invocation is not a constructor-declaration lookup, so it never reaches that arm, and no operation-call analogue exists. BLAST RADIUS TODAY: ZERO. No operation in the corpus carries admit_callers -- all 21 occurrences across dag/ and src/v2/ attach to a fn or a sealed type. So this is a LATENT TRAP, not a live hole, and the distinction is stated because the first author to reach for it is the one who gets hurt and will have no reason to doubt it. THE PAIR IS ONE ARTIFACT, which is the point rather than a convenience. The positive control (fn form refuses, green today) and the finding (operation form does not, red today) run through one invocation over sources compiled as DATA via the guarantee probe corpus. Split into two files they would be two observations; together they are a discrimination, and the discrimination is the finding. Without the control, a red could equally mean the mechanism is inert or that this file cannot compile a probe at all -- different states, different remedies. Compiling the sources as data is also what makes the pair possible: a refusal here is a resolve error, so an unadmitted call written directly into this module would take the whole file down with it. EXECUTED: fn form returns true, operation form returns false, same file, same run. ENROLLED AS KNOWN-RED rather than left to fail. A bare red takes the floor down and gets triaged as breakage by someone who does not know why it is there. Per DESIGN 4b it does NOT get deleted when the resolver gains operation-grain enforcement -- it flips to a permanent regression control, because deleting the evidence on the climb recreates specification-without-execution one rung up. The roster's own coherence witness passes with the identity added. RUNG, HONESTLY: not mitigatable but BELOW it, because no mitigation occurs -- nothing refuses, nothing counts, nothing is logged. Attainable ceiling: structurally guaranteed, since the class is decidable and fully modeled and only implementation stands between here and there. NEXT-RUNG TRIGGER: an operation-grain construction refusal exists, verified by a correctly-imported unadmitted caller. The trigger is stated in its VERIFIED form because its first two attempted verifications were inconclusive for reasons unrelated to the seal -- a missing import, then a fixture whose service did not resolve at all. A trigger already mis-measured twice should carry how to measure it. NOT FIXED HERE. The resolver change is substrate work with its own owner and its own review bar; routing around the defect or following it into infer would both be the wrong move from this lane. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Retarget the admission control onto the sealed fixture: 54.9s over a 10s ceiling CI caught a cost defect in my own control, and the floor's summary is what identified it: failed=0, known_red_held=307 (my expected-red enrollment took, 306 -> 307), and completed_over_cost_requirement=1. Nothing was broken; one witness was too expensive. THE ROW: fn_form_admission_refuses_unadmitted_caller took 54940ms against the floor's 10000ms per-witness ceiling and grew RSS by 0.99GB. Its forged source imported extdeps.shell.exec to reach transport_script_seal, so compiling it dragged the whole shell/extdeps closure through the diagnostic census. The operation-form probe beside it cost 516ms for exactly the inverse reason: it imports only std.types. THE FIX is to change the control's SUBJECT, not to raise a ceiling or split the file. test.fixture.sole_constructor_sealed.definer exists precisely to exercise caller admission on a minimal closure -- it is the fixture the corpus already uses for this mechanism -- so the control now forges an unadmitted caller of mint_sealed_local. Same mechanism, same refusal class, two orders of magnitude less work, and it moves the control off a production module it never needed to depend on. DISCRIMINATION RE-VERIFIED AFTER THE CHANGE, not assumed from it: fn form returns true, operation form returns false. A cheaper control that stopped discriminating would be worse than the expensive one. WHAT I COULD NOT MEASURE LOCALLY, said rather than implied: every gunbc run pays a whole-corpus typecheck, so both probes report ~58s wall from this session and the witness-level cost the floor meters is invisible from here. The 54.9s and 516ms figures are the floor's own per-witness numbers, and CI is what will confirm the retarget landed under the ceiling. I am not claiming a local measurement I did not get. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Cut command_runner's local path onto shell.Exec.RunArgv: argv stops round-tripping through a shell THE CHAIN THAT IS NOW GONE from the local arm: render the argv to quoted text, wrap it in a bash heredoc, hand it to a shell, let the shell split it back into an argument vector -- to reach a seed that ends in Command::new(argv[0]).args(argv[1..]) regardless. Every step existed only to undo the step before it. On LocalExec command_over_transport is the IDENTITY, so the render had nothing to transform either. Deleted from that path rather than routed around. MEASURED FIRST, because the assignment's census was stale by construction: 22 live call sites across 5 modules (not 25 across 6), 17 of them run_shell_command_capture. ALL 22 PASS LocalExec -- zero use SshExec -- so the entire live population moves in this cut. The callers are untouched: the change is internal to command_runner and both signatures are preserved. THE ONE ENABLER, and it is the part worth reviewing hardest. ArgvCommand.argv is a runtime List<String>; CliSurface is sole_constructor and its only construction route is through CliArgumentSyntax fragments, which carry declared token classes and bindings. Fragments structurally CANNOT express a word that does not exist until the program runs -- a filesystem path, a hostname. So cli_surface_of_literal_words was added to v2.std.compilers.cli_surface. WHY THAT IS NOT THE AMBIGUITY THE CARRIER EXISTS TO CLOSE: the refused state is a List<String> arriving at an argv position with NO declared role, where "one word whose text is the concatenation" and "N separate words" are both well-formed and the realization must guess. This constructor IS the declaration -- its name says each element is exactly one argv word. It is the same resolution the interpreter refusal I landed earlier tells authors to reach for. The file states what it does not license: an argument whose spelling is known at authoring time belongs in fragments, and reaching for this instead is modeling debt. EMPTY ARGV REFUSES rather than defaulting -- a command with no words names no program, and inventing one is fabricated output. THE SSH ARM IS UNTOUCHED, deliberately. Its prefix-append shape is wrong in kind (RFC 4254 carries one string, so the inner command is a nested serialization target, not a concatenation) and that target belongs to another lane. Two sessions editing one contested branch is worse than either fix. It also carries no traffic through this module today, which is why leaving it cost nothing. THE success FIELD is derived through a NAMED policy -- process_exit_is_admitted(ExitZeroSucceeds) -- rather than a bare exit_code == 0, so the convention this runner applies is something a caller can change rather than a literal to discover. WHAT STILL COLLAPSES, named and not fixed here: "ran and exited nonzero" and "could not be executed at all" both arrive as success: false. Under the old bash hop those were genuinely indistinguishable -- a missing binary became the shell's exit 127, which claims a process ran when it never existed. Going direct removes the shell that fabricated that code, so the distinction is now AVAILABLE at the transport even though ShellCaptureResult cannot express it. Not repaired in this cut because it is not free: 17 call sites read that record and the destination is the ProcessOutcome coproduct one module away, so the repair belongs with the sites it changes. THE DISCRIMINATING RECEIPT, executed wet against a real process: argv ["printf", "%s|", "a b"] direct exec -> one operand "a b" -> stdout "a b|" OBSERVED via a shell -> two operands -> stdout "a|b|" asserted absent All three assertions pass. A green that would still be green with the bash hop restored would prove nothing about what changed, which is why the subject is an argument the two paths DISAGREE about rather than a command that merely succeeds. IT IS WET AND EXCLUDED, for a reason that is structural rather than convenient: hermetic evaluation replays an operation's declared mock_response and never constructs an argv at all, so "the words reached the process unsplit" is not observable hermetically. A hermetic version could only assert the mock, which is specification-without-execution. Excluded exactly as the prior argv receipt is, and the file says so. DIVERGENCE FROM THE RECORDED TRIGGER, stated rather than left for a reader to notice: command_runner_dissolution_trigger names host_effect_apply binding ArgvCommand execution as a typed transport handler. This cut routes command_runner directly at shell.Exec.RunArgv instead. The trigger's second clause -- retire the shell_exec_via_bash glue -- is satisfied for the local arm and NOT for the SSH arm, so the trigger is not yet discharged and I have left it in place rather than claiming it. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Restrict the literal-words mint to its two callers; state what CI does not guard; correct the trigger Three review items, all taken. The first is the one that mattered and my semantic defence of it was insufficient. 1. THE MINT IS NOW admit_callers-RESTRICTED. My argument was that a constructor whose name says "each element is one argv word" IS the declaration the refused state lacks, and that stands -- but the declaration was UNBOUNDED. Anyone could make it, about anything, which left the interpreter's argv refusal one import away from being routed around: not defeated, just satisfied by an intent nobody checked was true. Nominal wall, not structural. The admitted population is TWO -- run_shell_command and run_shell_command_capture -- which is what makes the restriction honest rather than aspirational. A third caller is an edit to the list in the declaring module: a counted review event rather than an import written elsewhere. VERIFIED BY EXECUTION, with a discriminating RED rather than by reading the declaration -- which matters more than usual here, because I spent this session proving that this exact mechanism is ACCEPTED AND INERT at operation grain. An unadmitted module calling it is refused: constructor call admission refused: 'v2.std.compilers.cli_surface.cli_surface_of_literal_words' refuses call from 'test.fixture.mint_admit_probe.intruder.unadmitted_mint' — permitted callers: [gunbc.command_runner.run_shell_command, gunbc.command_runner.run_shell_command_capture] Located, names the caller, lists the roster. The admitted callers still work: the wet receipt passes unchanged. This is a fn, which is the grain where the mechanism is verified to fire. The file's note that authoring-time spelling belongs in fragments carries no enforcement, and now says so rather than reading as a wall. 2. WHAT GUARDS THIS CUT, AND WHAT DOES NOT, written where the next author stands. The property "the local path reaches no shell" is established wet and the receipt is FLOOR-EXCLUDED, so CI does not run it and someone reintroducing a render-and-bash hop gets no signal. The exclusion is structural -- hermetic evaluation replays mock_response and never constructs an argv, so a hermetic version could only assert the mock -- but the consequence is a real gap and the module now states it: rung mitigatable, next-rung trigger a wet lane that executes floor-excluded receipts. A green test that nothing runs is exactly the inert evidence DESIGN calls a lie, and the file should not read as enforced. 3. THE TRIGGER NAMED A MODULE THAT WAS NEVER BUILT. Asked whether I had created PARALLEL AUTHORITY rather than whether I matched wording, I measured: there is no host_effect_apply production module (it exists only as a witness test), and host_effect_realize never mentions ArgvCommand. command_runner is the ONLY module that turns an ArgvCommand into a local process. The other ArgvCommand consumers reach shell_command_render, which serializes argv into TEXT for emission (githooks) or for the SSH leg -- a different destination, not a second local-exec route. So this did not diverge from the trigger; it satisfied a better version of one that named a binding nobody wrote, and satisfying it literally would have meant building the second route DESIGN forbids. The row is rewritten to name the condition that actually remains: the SSH arm, which needs the nested command-string target another lane owns, and at which point shell_exec_via_bash and retained_runtime leave this module entirely. Also fixed in passing: my own trigger rewrite wrote a \\U escape into the .dag string instead of the literal character, which made the module unparseable. Caught by resolving the file rather than by reading the diff. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Correct a false premise in the trigger I just rewrote: host_effect_apply exists The conclusion was right and one clause of its evidence was false, which is worse than usual here because it sits in a REPLACEMENT trigger -- the row exists to stop the next author re-deriving the question, and a false premise makes them do it anyway. WHAT I WROTE: no host_effect_apply production module exists, witness test only. WHY I GOT IT WRONG: I searched for a FILE named host_effect_apply*.dag and found only the witness test. It is a FUNCTION. gunbc.host_effect_realize declares host_effect_apply and host_effect_apply_gated and both are production. That is the third scope error of this session in one family -- a limited view read as the population -- and the specific lesson is narrower than the earlier two: searching for a filename does not answer a question about a symbol. WHAT ACTUALLY CARRIES THE ARGUMENT, verified independently rather than taken from the correction: host_effect_realize contains ZERO occurrences of ArgvCommand and does not appear among that type's consumers. So host_effect_apply exists and dispatches effects, but it never reaches an ArgvCommand and is therefore not a second route from an ArgvCommand to a process. command_runner remains the sole one, there is no parallel authority, and satisfying the original trigger literally would still have meant BUILDING the second route rather than finding it. The row now says that, and records the correction in place rather than quietly overwriting it, so a reader who saw the earlier claim learns it was wrong instead of wondering which revision to believe. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Replace ShellCaptureResult with ProcessOutcome across every capture site THE CONFLATION, corrected from how we first described it. I claimed in the previous commit that removing the shell's fabricated 127 made "could not be executed at all" available beside "ran and exited nonzero". I TESTED THAT AND IT IS FALSE: a missing program does not produce a result record at all, it REFUSES the evaluation -- failed to execute 'no_such_binary': No such file or directory (os error 2) -- so spawn failure was already fail-closed one rung above the record, and the RED first proposed for this work would have passed against the old record too. The real conflation is one step over and it was live at EIGHT sites: ran and FAILED, printing nothing -> success=false, stdout="" ran and SUCCEEDED, printing nothing -> success=true, stdout="" Both are stdout == "". Those eight read stdout without consulting success, so a failed probe and an empty result were the same value. THE EIGHT, AND WHAT EACH NOW DOES: fleet_host_key_enrollment.check -- THE WORST ONE. Tested trim(stdout)=="present" with no success check, so a probe that FAILED produced "" != "present" and fell through to the branch that APPLIES. A refusal to read authorized_keys was indistinguishable from the key being absent, and the remedies are opposite. Now: refusal refuses and does not mutate the file. fleet_host_key_enrollment.verify -- did concat("outcome=", trim(stdout)), so a refused verify wrote the literal receipt line "outcome=" into a file someone would later read as fact. Now: outcome=UNKNOWN with the cause. fleet_host_key_enrollment.{user,hostname} -- display only. Routed through process_outcome_receipt_text, which renders the three arms to three DISTINCT strings; a refusal can no longer read as empty. fleet_probe_identity_observe.user -- display only, same route. fleet_probe_identity_observe.{passwd_home,job_home} -- USED AS PATHS, not just printed, so they match the arms directly: "(refused: ...)" is fine to print and catastrophic to open. An unreadable home now skips the probe with a stated not-probed line instead of reading .ssh/authorized_keys off a fabricated root. fleet_converge_plan_cli hostname -s -- SURFACED, NOT CLOSED, and said so in file. A `-> String` function has no way to refuse; the honest repair changes the return type and cascades into converge plan subject identity. It now returns a value that CANNOT be mistaken for a hostname rather than a plausible "", so a plan keyed on it is visibly wrong instead of silently wrong. Rung: mitigatable, with the next-rung trigger named. SITES THAT GENUINELY DO NOT NEED THE DISTINCTION, stated rather than left silent: fleet_converge_plan_cli test -f -- exit status IS the product, no stdout anyone wants. Asks process_outcome_admitted directly. Forcing it through an output-bearing variant would add a field it cannot answer. ssh-keygen -F readback -- same shape, same treatment. fleet_ssh_credential_verify x2 -- decompose into a classifier that consumes all three values TOGETHER, so the correlation was already performed. The match adds exhaustiveness and names ProcessOutputAbsent, previously indistinguishable from a failure with empty stdout. DELETED, not kept beside: type ShellCaptureResult is gone. Its one fabricated construction is gone too -- fleet_host_key_enrollment built a ShellCaptureResult to stand in for a FILESYSTEM write failure, inventing success:false for something that was never a process. The coproduct makes that unwritable. scan_host_key_lines shows why the type fits: `scan.success && trim(stdout) != ""` IS ProcessOutputPresent, so a hand-written correlation became a variant. And ssh-keyscan exiting 0 with no key is now a named outcome rather than being reported as a refusal with an empty cause. DISCRIMINATING RED, executed wet, six of six green: nonzero-exit-printing-nothing must be Refused and zero-exit-printing-nothing must be Absent. Both go red if ShellCaptureResult is restored, because then both are stdout == "". The file also records what is NOT tested and why -- the nonexistent-program case is already distinguishable via transport refusal, so asserting it would prove nothing. Recorded on the carrier: spawn failure is fail-closed at the transport, therefore A CALLER CANNOT PROBE FOR A BINARY'S EXISTENCE BY TRYING TO RUN IT -- the attempt stops the line instead of answering. Presence must be asked of something that exists. That is why a separate presence probe has to exist, and it is why no fourth "not spawned" variant was added: it would be an uninhabited arm every consumer must handle and none can reach. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Site 8: the poison IS persisted, and it defeats the guard — second row Checked rather than argued, and the answer is worse than "it might reach a receipt". fleet_converge_plan_wet WRITES host_short verbatim to fleet_converge_plan_subject_host_path, coerces it to NonEmptyStr as the plan's subject host, and folds it into the member-set fingerprint and the plan content hash. An unobserved hostname is persisted as a receipt that later reads as fact. AND IT DEFEATS THE GUARD BUILT FOR THIS EXACT CASE. fleet_converge_apply_wet re-observes the host and refuses on SubjectHostMismatch when observed != planned. Two consecutive refusals produce the SAME string, so the comparison SUCCEEDS and apply proceeds. The check whose entire purpose is to stop a plan being applied on the wrong host is satisfied by two non-observations agreeing with each other -- the empty-observation narrow relocated to the guard: bottom == bottom read as "same host". Making the marker unique per call would NOT repair it; it converts a false match into a false mismatch, which is a different wrong answer, not an observation. NOT INTRODUCED HERE, stated precisely: the prior code persisted "" and compared "" == "", which passed identically. This migration does not repair the defect -- it makes the persisted evidence legible instead of blank. Filed as a SECOND row rather than folded into the first, because the first row's claim (visibly wrong rather than plausibly empty) says nothing about reachability and this row is entirely about reachability. Both mitigatable; different next-rung triggers. This one's: the subject-host comparison consumes an outcome rather than a String, so unobserved-vs-unobserved is a REFUSAL to compare, not an equality. The block is hoisted to module scope as a leading annotation on the declaration (§4c), not left inside the func body. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Hoist 29 body annotations to module-item grain (§4c), and integrate main's command_over_transport refusal coproduct TWO SEPARATE THINGS, both landing here because CI surfaced them together. (1) THE §4c REFUSAL, 29 sites across four files. I put per-site rationale where the explanation belongs conceptually -- beside the line it explains -- which is exactly the position the language refuses. Hoisted every block to a consolidated leading annotation on the declaration. WHAT I ACTUALLY GOT WRONG, since I had already hit this twice: I fixed ONE block earlier and reported it as fixed. I repaired the instance the error named instead of the class the RULE names. The sweep this time is the whole branch and then the whole corpus -- both now zero indented `//`. The refusal is correct and I am not routing around it. It is fail-closed at the source boundary, typed, located to the byte, and it stopped the line rather than silently dropping the prose. The corpus already tried the alternative: `//` as an outright parse error made comment SYNTAX unwritable without making commentary unwritable, and prose migrated into `data ...: String` rows where intent is mechanically indistinguishable from program data. (2) THE MERGE, which was NOT a text conflict to pick a side on. main landed the command_over_transport refusal coproduct (Built | Refused, #8596) while this branch replaced the capture return type. Both arms of both functions had to be rebuilt, not chosen: run_shell_command SSH arm: Refused -> exit_failure with the rendered cause run_shell_command_capture SSH arm: Refused -> ProcessRefused, NOT the deleted ShellCaptureResult main still constructed there Taking either side whole would have been wrong in a way that still compiles on one of them: ours drops main's new refusal handling, theirs resurrects a deleted type. So I took ours and re-applied main's additions explicitly -- the imports, command_over_transport_refusal_reason and its note, and both refusal arms. Note the refusal now composes rather than collapsing: an SSH command that cannot even be BUILT is a ProcessRefused with a stated cause, distinct from one that ran and failed. That is the same distinction this branch exists to make, arriving from main's side of the merge. The LocalExec arm is untouched by the merge and still routes through RunArgv. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Take main's optional-hostname repair and re-express it on ProcessOutcome; DELETE my two mitigatable rows because they are no longer true MAIN FIXED THE DEFECT WHILE THIS BRANCH WAS OPEN, and it fixed it at the rung this lane named as the trigger rather than at the one I settled for. mine: -> String, returning a marker that cannot be mistaken for a hostname. Legible, still not a refusal. Two rows at mitigatable. main: -> NonEmptyStr?, Absent when the probe did not succeed. Plan AND apply refuse outright on Absent, and the subject comparison routes through fleet_converge_apply_subject_host_matches over two NonEmptyStr values instead of a bare String equality. That closes BOTH rows. Row 1 (the value is visibly wrong rather than plausibly empty) is obsolete because there is no longer a value. Row 2 (the poison is persisted, and two non-observations comparing equal DEFEAT the SubjectHostMismatch guard) is obsolete because Absent never reaches the comparison at all. SO I DELETED BOTH ANNOTATIONS RATHER THAN KEEPING THEM. A rung row that describes a defect the tree no longer has is not harmless documentation -- it is a false claim in the file that owns the fact, and the next reader plans against it. That is the stale-citation class this repo already pays for, and the cost is worse for a row asserting a LIVE SAFETY DEFECT than for a stale line number: someone would have re-escalated a fixed bug. WHAT I ACTUALLY CHANGED is only the probe's input shape. main derived Absent from `!run.success || trimmed == ""`, reading the record this branch deletes. The same judgment now reads the arms of ProcessOutcome, and the mapping is exact rather than re-decided: ProcessRefused -> none (did not observe) ProcessOutputAbsent -> none (ran, said nothing) ProcessOutputPresent, trims empty -> none (wrote bytes that do not name a host) ProcessOutputPresent, trims nonempty-> Present The third arm is the one worth stating: ProcessOutputPresent means the process WROTE BYTES, not that those bytes name a host, so the empty-after-trim guard main had is preserved rather than assumed away by the richer type. Also migrated this file's `test -f` site off `.success` onto process_outcome_admitted -- exit status IS the product there, which is why it takes the admitted projection rather than matching arms. CONVERGENCE WORTH NAMING: main's repair and this branch's migration are the same argument from two directions. Main gave the RESULT somewhere to say "not observed"; this branch gave the OBSERVATION somewhere to say it. Neither is redundant with the other, and the merged form is stronger than either -- which is why this resolution takes main's shape rather than defending mine. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> --------- 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>

…easure the parse route Axis 2 and axis 3 were argued from reading the Rust marshal; they are now proven by execution. A fixture pair of identical shape folded through fn_arrow_decl_facts_live: fixture_dead_let_shell (binds the call, does not use it) yields ZERO atoms — callee identity and program literal both absent — while fixture_live_named_args yields "fixture_sink2 | echo LIVEMARKER | echo ARGSMARKER". Same construct, opposite verdict, so the loss is the projection's and not the probe's. The live arm also shows axis 3 directly: three atoms in authored order with no labels, so nothing says which literal was program: and which was args:. Axis 6 is new and was measured, not read. The reflection registry is the ENTRY'S IMPORT CLOSURE, not the corpus: a fold over fn_arrow_decl_facts_live under both production roots reported 1,698 fn/func declarations against 41,965 declared in the tree, about 4%. This is a declared frontier rather than a discovery — corpus_dependency_view already refuses per-PR when fn_arrow_decl_substrate_is_whole_tree is false ("blocked-on-#6239") — but it is fatal for a census specifically, because files disappear through non-import with no per-file ParseRefused row to count them. That is the empty-observation narrow: never-loaded is indistinguishable from carries-no-route. The full-fidelity parse route is measured against a positive control. The tree's own three-line fixture ACCEPTS, a real 28-line corpus file ACCEPTS, and dag/extdeps/shell/exec.dag REJECTS with reason=parse_grammar_choice_overlap_residue. So the route is real and its failure is a located typed refusal, but the file it refuses declares shell.Exec.Run/RunArgv/Check — the census's most load-bearing seed file. Records that accepts-or-refuses was the wrong frame: there is a third outcome, accepts but is unaffordable at corpus grain, and it is the one the prior cost signal makes likely. Affordability is being measured as a slope over a random 40-file sample rather than extrapolated from the fixture, since fixed overhead and per-byte cost are different curves. If it lands there, DESIGN §6 already rejected this shape once in #8140 — "the unit of computation was the world, the unit of fact was one module's authorship" — and its declared next-rung trigger is exactly axis 1's remedy: one module's facts from one module's source, checked at ingestion where the module is parsed anyway. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01QFxNVPeTcYeCjP7rQyLtZu

Two specs, no implementation. The increment lands partly in the frozen v1 seed, whose admission test is purpose — does the change serve the v2 self-host program — and this increment serves a shell-migration census, so the call is the operator's and no seed work starts on lane authority. The increment spec is written for someone deciding admission rather than for an implementer. It leads with the empty-observation narrow rather than the coverage percentage, because that is the part that makes the substrate unusable rather than merely partial: a file that was never loaded reads identically to a file carrying no shell route, and no per-file ParseRefused row exists to count the difference, so a census on it yields a clean confident population that is silently wrong. Each of the six axes carries its own evidence grade rather than being presented as uniformly established — axes 2 and 3 execution-proven by the discriminating fixture pair, axis 6 execution-measured, axis 1 structural and independently verified, axes 4 and 5 read from the marshal. The counting method is stated beside the axis-6 denominator because it will be questioned: 41,965 counts line-start fn/func/test fn and matches the accessor's own filter, since ItemKind has no separate test variant and a test fn IS an FnItem; 30,851 is the same count with the 11,114 test declarations removed. 1,698 visible is 4.0% or 5.5% and the conclusion is invariant. Two properties are separated for the admission call: axes 2-5 are an ADDITIVE second accessor rather than an edit to the existing marshal, whose lossiness is load-bearing for v2.lens.wiring_liveness and must not change; and axis 6 is probably already-sanctioned work pending #6239 rather than anything this increment requests. The admission question is recorded with both readings and no advocacy. The grammar finding is filed separately because it outlives the census. Five refusals across two source roots, four sampled at random plus the independently-found extdeps/shell/exec.dag, all carrying one reason: parse_grammar_choice_overlap_residue. No corpus rate is claimed from ten files; the shared cause is the finding. It is invisible because the only path that would surface it, canonical_dag_source_parse_print_law, has no callers — the unexecuted law and the unmeasured deficiency are the same fact seen twice. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01QFxNVPeTcYeCjP7rQyLtZu

… measured, not claimed (#8655) * Correct two gates that describe per-PR enforcement in the present tense while not running Measured 2026-08-19: dag/tools carries 12 gate modules and ZERO are referenced by any workflow. .github/workflows/ holds two files, and witnesses.yml's only executing step is claim_executor --required-floor. tools.extdeps_scope_placement_gate calls itself a "server-side per-PR wall" that "refuses any dag/extdeps .dag file added by THIS CHANGE"; tools.prose_row_introduction_gate opens with "THE PER-PR WALL". Neither is standing. DESIGN is already honest about this -- its "Building & checks" section declares the 2026-08-15 floor cut as a bounded rung drop and names the effect gates among what is unguarded until the re-add queue closes. What was never updated is the module-level prose, and that is the copy a session actually opens. A wall described in the present tense is a premise the next plan gets built on. PROSE ONLY. No enforcement is re-added, no gate deleted, no roster touched. Only the description is corrected to match the mechanism, citing DESIGN as the authority rather than restating its contents. tools.rust_stage0_gates was checked and needs no correction: it says per-PR execution is "gated on #6239", which states the wall is blocked rather than asserting it stands. RECORDED WITH IT, because it is what made the gap invisible and it generalises past these files: THE .dag CALL GRAPH IS NOT THE EXECUTION GRAPH. Any claim of the form "this runs in CI" is decided by .github/workflows/ and the fold those workflows invoke, never by who calls whom in .dag. Two sessions independently traced the .dag callers of git.Core.DiffUnified0, both concluded it was on a path CI walks every run, and both were wrong -- agreeing was not a second observation, because both had read the same artifact. The finding is stronger than "these two gates are dormant". In hermetic mode eval_mock_response replays the operation RESULT off the declaration's mock_response and never touches argv, so no argv is CONSTRUCTED in the mode CI runs. No argv defect of any kind is observable there. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Refuse the argv representation ambiguity instead of silently resolving it A free monoid whose elements are Strings satisfies BOTH readings at an argv position: value_as_host_string folds it into one concatenated word (its `Value::Str(s) => out.push_str(&s)` arm), and free_monoid_to_vec splices it into N words. The value records no choice between them, and push_shell_argv_tokens tried the concatenating reader first -- so one declared List<String> produced ONE argv word when it arrived monoid-encoded and N words when it arrived as a native list. Same type, same declaration, opposite arity, decided by a representation the author never selected. This is a state-space conflation, not a missing wall, which is why no branch ordering could have been correct: "one argument whose text is the concatenation" and "N arguments" are different states with different remedies. The position now raises a typed, located diagnostic naming the argv index and both readings. MEASURED SPECIMEN: extdeps.git.git git_diff_range_argv returns [base, head] on its TwoDot arm, spliced into `git diff -U0 <range>`. Monoid-encoded that reaches the process as `mainHEAD`. The failure is not that git errors -- on any pair whose concatenation names a real object it produces a successful diff of the WRONG RANGE, which is fabricated plausible output rather than a crash. DELIBERATELY UNCHANGED: Int-element monoids stay char-decoded (unambiguous under one reading only); native Value::List keeps its N-word expansion; ProcessArgvExpansion stays authoritative; and value_as_host_string itself is untouched -- value_to_host_string wraps it for general use, and narrowing a shared helper to fix one caller is the forked-logic trap this lane exists to remove. The empty monoid keeps its current empty-string reading, called out in-code as a deliberate narrow choice rather than left implicit. EVIDENCE, and the RED is unit-level by necessity rather than convenience: in hermetic mode eval_mock_response replays an operation's RESULT off its declaration and never touches argv, so no argv is CONSTRUCTED in the mode CI runs and there is no execution to assert against. Three assertions build the representations directly. Proven discriminating by disabling the refusal and re-running: native list of two strings -> 2 argv words (holds both ways: control) monoid-encoded, refusal enabled -> refuses monoid-encoded, refusal disabled -> FAILED, argv ["mainHEAD"] codepoint monoid -> 1 word (holds both ways: control) NO FROZEN ROSTER, because the refusal IS the census: whatever breaks was relying on the concatenation, and that is exactly the population worth enumerating. Each will be fixed from first principles -- either a latent instance of this defect, or a site that genuinely wants one word and should say so with an explicit join. No arm restoring the old behaviour will be added for sites that complain. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Open the vocabulary axis of realization_vocabulary_containment; falsify the REST/CLI boundary The argv lane keeps asserting in prose that a Redfish/REST path constructs no process invocation. Prose cannot be contradicted by the tree. This makes it a row that reds. NO SECOND LENS WAS MINTED. v2.lens.realization_vocabulary_containment already answers "does module X reach construction vocabulary from set V". The obstacle was that V was a literal: the importer-path axis was already threaded as a parameter through scan_facts_for_leaks_under, while module_is_target_ast_vocab was welded into the predicate. A second lens for a second V would have been the section 3 duplication this lens exists to detect, so the vocabulary axis was opened instead -- the section 2 horizontal move, one axis rather than N copies. RealizationVocabularySet + module_is_in_vocab + is_vocab_leak_in / scan_facts_for_leaks_in / vocab_leak_count_in / vocab_leak_count_live_in. target_ast_vocabulary() DERIVES from the existing target_ast_vocab_modules and target_ast_vocab_module_prefixes rows rather than replacing them, because gunbc.realization_vocab_confinement_census consumes those rows directly and has live claims against them. THE OLD ENTRY POINTS DELEGATE, they do not keep a parallel copy. Leaving the original fold beside the general one would have been one predicate with two implementations -- the fork this lens detects, one level down. The exempt population is a PARAMETER rather than a global roster read, so "this vocabulary has zero admitted exceptions" is a stated fact instead of an accident of the target-AST roster happening to name no CLI module. TWO SITES LEFT TARGET-AST-ONLY, DELIBERATELY, with the reason in-file: the two projections feeding the grandfathered-roster staleness check, whose roster rows are target-AST debt by construction (RealizationVocabDebtClass has no other inhabitant). A second vocabulary arrives with an empty exempt population and so has no roster to be stale against; parameterizing them now would answer a staleness question about a population that does not exist. Trigger recorded. THE FALSIFIER'S SUBJECT IS NOT AN EMPTY UNIVERSE, which is how a negative claim usually turns vacuous. dag/extdeps/bmc contains a module that legitimately reaches this vocabulary -- openbmc_fan_control, the module this lane routes through jq -- beside redfish.dag, which does not. So the scan discriminates WITHIN the population, and the RED control is live corpus data rather than a planted fixture: withdraw the one admitted edge and the count must become 1. Without that assertion a clean result is indistinguishable from a scan that read nothing, which is the empty-observation narrow. The admitted edge is named at exact (importer_path, vocab_module) grain, so a SECOND jq-reaching module anywhere in the scanned roots reds rather than being absorbed by a pattern broad enough to cover it. EXECUTED: all three witnesses return true, including the discrimination control at exactly 1. The pre-existing lens witnesses (planted_leak, discriminators, roster_soundness) return true unchanged. SCOPE, STATED RATHER THAN IMPLIED: the witness is floor-discovered -- neither long/-homed nor in floor_prepared_subject_exclusions -- and reads the live tree, but only the two named directories. A module outside those roots reaching CLI vocabulary is not seen here, and no green from this file may be read as whole-corpus coverage. That lens's whole-corpus half is enrolled on a cadence that does not currently run, which is a fact about the cadence rather than about this witness. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Widen the CLI-vocabulary falsifier root by root; every clean root carries its own control The boundary was enforced in two directories and prose everywhere else. That was the whole of its limitation, so this widens it -- one root per assertion rather than one widened list, so a failure names the root that broke instead of reporting that something, somewhere, reaches CLI vocabulary. ROOTS ADDED, each landing in a stated state rather than behind one green: dag/extdeps entirely -- one admitted edge (the fan control jq edge, already named) plus the jq definition site on the edge roster. Clean otherwise. src/v2/{std,compiler,lens,workflow} -- ZERO admissions. The compiler substrate constructs no process invocation at all. If any of it ever needs a CLI surface, that is an architectural event and it reds here first. A CLEAN ROOT AND AN UNREAD ROOT BOTH REPORT ZERO, and those are different states -- bottom-as-answer against bottom-as-ignorance. Three controls separate them, because the widened roots have no known edge to withdraw: vocab_scan_fact_count_live asserts each scan acquired real facts, so a zero is a finding rather than a silence. Withdrawing the admission under the WIDE root must still surface the fan control edge at exactly 1. A nonzero fact count proves the extdeps scan read something; it does NOT prove it descended into bmc/ where the only known edge lives, so without this "dag/extdeps is clean" could be clean because the one dirty subtree was never reached. Dropping the definition-edge roster must make the count RISE, which proves that roster admits a real edge rather than naming a path the scan never had a fact for. THE TWO ROSTERS ARE DELIBERATELY DIFFERENT SHAPES. The jq definition site is a PATH prefix because constructing a CLI surface is what that location is for; the fan control admission is an EXACT (importer_path, vocab_module) pair because it is one consumer that happens to need the vocabulary and must not silently become two. EXECUTED: 8 of 8 green, including all four controls. STILL NOT COVERED, stated rather than implied: dag/gunbc carries six modules reaching extdeps.shell.exec (the host-effect and transport layer) and dag/test carries the witnesses that exercise this vocabulary deliberately. Neither is added here. Whether dag/gunbc's shell reach is a realization edge or admitted debt is a policy question about the boundary itself, not a mechanical widening, and it is not this change's to decide. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Close the last roots: the #8535 boundary now reds, stated as infrastructure-vs-consumer THE BOUNDARY, in the form that fails rather than the paragraph: Realization infrastructure may reach transport vocabulary; consumers may not, except by exact named admission. #8535's prose says CLI-backed handlers are one realization cell. This says which modules ARE that cell and refuses the rest by name. dag/gunbc's six extdeps.shell.exec reaches are two different things, split by what the module IS rather than by what it imports: PATH-ROSTERED AS REALIZATION EDGES -- retained_shell_script (defines the counted bridges, calls transport_script_seal), bash_materialized_transport (the only other admit_callers-sealed caller of that seal), host_effect_realize (the realization core, reaching through retained_srvn). Reaching transport vocabulary is what these locations are FOR, which is the same reason jq's definition site is path-rostered. ADMITTED AS EXACT PAIRS -- package_delivery, codex_app_server_press, provider_wire_evidence. Exact, so a SEVENTH consumer reds instead of being absorbed by a prefix broad enough to cover it. THE REASON ON THOSE THREE IS THE FINDING, NOT A JUSTIFICATION. All three reach through retained_foreign, whose declared dissolves_to is the bash emitter -- the destination for foreign executors and pre-runtime bootstrap -- while all three appear to run inside a present gunbc runtime, which would make their real destination typed effects. The roster records a bucket that is probably wrong rather than laundering it, so fixing the bucket takes the admission OFF instead of re-justifying it. That population was reached TWICE INDEPENDENTLY: by a retained_foreign call census and by this import-graph scan, which additionally separated out provider_wire_evidence. Two routes landing on one set is why these are named rather than guessed. dag/test is path-rostered and said so: these are the witnesses that exercise this vocabulary deliberately, including the ones proving the argv refusal itself. A test that could not import the thing it tests would be a test of nothing. Stated as a roster rather than left unscanned, so the exclusion is visible instead of implied by absence. THE GENERAL RULE, written into the file because the next person widening a root will reach for the inherited control and it will pass while proving nothing: RE-ESTABLISH DISCRIMINATION AT THE NEW SCOPE. DO NOT INHERIT IT. A narrow root's RED proves the scan discriminates over THAT root. Widen it and it proves nothing about the new subtrees -- a nonzero fact count shows the scan read something, not that it descended where the dirty modules live. Caught here under a green: dag/extdeps reported clean and would have reported clean had bmc/ never been reached at all. So every root carries, at its own scope, a withdrawal control with an exact expected count and a roster-drop control asserting the count RISES, the latter because an edge roster no fact matches is indistinguishable from a correct one. EXECUTED: 12 of 12 green, six of them controls. The gunbc withdrawal returns exactly 3, which is what establishes the split is real rather than fitted to produce a pass. CONTEXT A READER NEEDS FIRST: only 13 files in the whole corpus reach CLI construction vocabulary. The boundary was substantially intact before anyone described it; this confirms and pins a property the tree mostly has rather than negotiating one into existence. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Model the local process-argv seam; fix the trailing-annotation refusal my own edit introduced TWO THINGS, and the second is a defect I caused and did not catch. 1. shell.Exec.RunArgv -- the local process-argv execution seam. Run is argv ["bash", "-s"] with the script on stdin, so every local ArgvCommand in the corpus renders its argv to quoted TEXT and hands it to a shell that parses it back into an argument vector. The seed does Command::new(&argv[0]) at the far end regardless, so the round trip buys nothing and costs exactly what argv-as-serialization exists to stop: a re-parse where argument boundaries are inferred from text instead of carried. THE PROGRAM IS A SEPARATE INPUT, not the first element of the expansion. execve takes the executable and the argument vector as distinct parameters, and with the program separate as NonEmptyStr an EMPTY argv becomes unconstructible -- the unspawnable empty vector has no representation rather than being refused after the fact. NO success: Bool FIELD. `success` is not an observation, it is a POLICY judgement about one -- jq exits 4 to mean "no output" and 1 to mean "false result", neither of which is failure. A Bool beside stdout makes every caller re-derive that from a field that already discarded the information, and lets a refusal read as empty output. So the wire carries the honest triple and the typed outcome is decoded immediately above it against a caller-declared policy. THAT DECODER IS NOT NEW VOCABULARY. It is the pattern already landed for jq (jq_classify_observation / JqExitPolicy / JqOutcome), so ProcessOutcome and ProcessExitPolicy generalize it and the module records what is owed: jq's types are the specialization, its 4-means-absent rule is the missing third policy variant, and they dissolve into these on the first migrated consumer. Named rather than left to be discovered, and deliberately not done here -- jq's classifier is landed and consumed, so folding it in belongs with the migration that motivates it. Local only, per the standing constraint: no SSH arm. command_over_transport's SshExec prefix-append stays where it is. 2. THE REFUSAL I INTRODUCED. Adding the operation left two block comments trailing at end-of-file with no declaration after them -- in the witness, and in exec.dag, where deleting a `data ... : String` prose row (correctly, per section 4c) orphaned the annotation that had described it. Source annotations attach to a FOLLOWING module item; a trailing block names no subject and the substrate refuses it. Both moved above the declarations they govern, and every .dag this branch touches swept for a trailing `//`. WHY 12 OF 12 GREEN DID NOT CATCH IT, which is the part worth carrying: `gunbc run --function` accepted the file the floor refused. The two paths do not agree on annotation validation, so a per-function green is not evidence that the floor will prepare the same file. My verification loop was reading the weaker path and reporting it as though it were the stronger one. The witness assertions themselves are unaffected and still green, including the new definition-edge roster entry -- which exists because THIS change tripped the falsifier: exec.dag reaching cli_surface is a CLI-vocabulary edge inside dag/extdeps, a root the witness asserts is clean. The module is itself a member of cli_process_vocab_modules, so the reach is vocabulary-internal, on the same footing as jq's module. A roster entry added because a real scan refused is a different thing from one added in anticipation, and the file says so. CI is the verifying consumer for the annotation fix: the refusal reproduces on the floor's preparation path, which is not reachable from any local invocation I could find, so I am not claiming a local green I did not get. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Move seam rationale to module-item grain; annotations are not admitted inside declaration bodies Second refusal from the same root cause, and the constraint is stated in DESIGN section 4c rather than being discovered here: the .dag realization admits only standalone leading // blocks attached to MODULE-SCOPE declarations. Trailing, body, unattached and block-comment forms refuse until separately modeled. I wrote the seam's rationale inside the operation body, which is body grain, so every one of those lines refused. Moved to one consolidated module-scope block above the service declaration -- which is also why the pre-existing operations in this file carry their notes as module-scope rows rather than inline: the language has never admitted the inline form, and I should have read that as the constraint it is instead of as a stylistic accident. Also fixed a comment inside a list literal in the witness. My first sweep counted brace depth and missed it, because a list body is bracket-delimited; the sweep now counts both and the branch is clean under it. NOTHING SEMANTIC CHANGED IN THIS COMMIT. The operation, its inputs, its output shape and the decoder are byte-identical in meaning to the previous commit; only the position of prose moved. Recorded explicitly so the next reader does not have to diff it to find out whether the seam was redesigned under cover of a formatting fix. WHAT THIS COST AND WHY IT RECURRED: I pushed the first annotation fix without local verification, saying CI was the verifying consumer because the refusal is raised on the floor's preparation path and gunbc run --function does not raise it. That was honest but it was also one class at a time -- I fixed the trailing form, pushed, and only then learned the body form refuses too, because CI reports the first failing class and stops being informative about the rest. Reading section 4c's own sentence would have given me both forms at once, and a sweep derived from the RULE rather than from the error message is what I should have run the first time. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * File the finding: admit_callers on a service operation is accepted and inert THE CLASS. admit_callers is the repository's construction wall -- a declaration names who may call it, and anyone else is refused. On a fn it works. On a service operation the same syntax PARSES, RESOLVES CLEAN, and DOES NOTHING. WHY THAT IS WORSE THAN THE WALL BEING ABSENT. An absent wall is visible: you look, find nothing, and know where you stand. This one is invisible while reading as present -- an author seals an operation, a reviewer reads the roster as a boundary, and it admits everyone. It is the inert-lens failure at CONSTRUCTION grain, which is the worst place for it, because a construction refusal is the rung people stop checking behind. Measured evidence that the illusion works: I was one step from reporting "the wall is available" after watching the declaration parse, and the reviewing session says it would have believed me. TWO INDEPENDENT ROUTES, deliberately not two readings of one artifact. BY EXECUTION: admit_callers added to the real shell.Exec.Run naming only gunbc.command_runner, after which the unadmitted gunbc.package_delivery -- which calls Run five times -- resolved byte-identically to the unsealed baseline captured first. BY SOURCE (the other session, independently): enforcement lives at exactly one seed site, gated on an exact-constructor-declaration lookup reading the fn admission list; an operation invocation is not a constructor-declaration lookup, so it never reaches that arm, and no operation-call analogue exists. BLAST RADIUS TODAY: ZERO. No operation in the corpus carries admit_callers -- all 21 occurrences across dag/ and src/v2/ attach to a fn or a sealed type. So this is a LATENT TRAP, not a live hole, and the distinction is stated because the first author to reach for it is the one who gets hurt and will have no reason to doubt it. THE PAIR IS ONE ARTIFACT, which is the point rather than a convenience. The positive control (fn form refuses, green today) and the finding (operation form does not, red today) run through one invocation over sources compiled as DATA via the guarantee probe corpus. Split into two files they would be two observations; together they are a discrimination, and the discrimination is the finding. Without the control, a red could equally mean the mechanism is inert or that this file cannot compile a probe at all -- different states, different remedies. Compiling the sources as data is also what makes the pair possible: a refusal here is a resolve error, so an unadmitted call written directly into this module would take the whole file down with it. EXECUTED: fn form returns true, operation form returns false, same file, same run. ENROLLED AS KNOWN-RED rather than left to fail. A bare red takes the floor down and gets triaged as breakage by someone who does not know why it is there. Per DESIGN 4b it does NOT get deleted when the resolver gains operation-grain enforcement -- it flips to a permanent regression control, because deleting the evidence on the climb recreates specification-without-execution one rung up. The roster's own coherence witness passes with the identity added. RUNG, HONESTLY: not mitigatable but BELOW it, because no mitigation occurs -- nothing refuses, nothing counts, nothing is logged. Attainable ceiling: structurally guaranteed, since the class is decidable and fully modeled and only implementation stands between here and there. NEXT-RUNG TRIGGER: an operation-grain construction refusal exists, verified by a correctly-imported unadmitted caller. The trigger is stated in its VERIFIED form because its first two attempted verifications were inconclusive for reasons unrelated to the seal -- a missing import, then a fixture whose service did not resolve at all. A trigger already mis-measured twice should carry how to measure it. NOT FIXED HERE. The resolver change is substrate work with its own owner and its own review bar; routing around the defect or following it into infer would both be the wrong move from this lane. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Retarget the admission control onto the sealed fixture: 54.9s over a 10s ceiling CI caught a cost defect in my own control, and the floor's summary is what identified it: failed=0, known_red_held=307 (my expected-red enrollment took, 306 -> 307), and completed_over_cost_requirement=1. Nothing was broken; one witness was too expensive. THE ROW: fn_form_admission_refuses_unadmitted_caller took 54940ms against the floor's 10000ms per-witness ceiling and grew RSS by 0.99GB. Its forged source imported extdeps.shell.exec to reach transport_script_seal, so compiling it dragged the whole shell/extdeps closure through the diagnostic census. The operation-form probe beside it cost 516ms for exactly the inverse reason: it imports only std.types. THE FIX is to change the control's SUBJECT, not to raise a ceiling or split the file. test.fixture.sole_constructor_sealed.definer exists precisely to exercise caller admission on a minimal closure -- it is the fixture the corpus already uses for this mechanism -- so the control now forges an unadmitted caller of mint_sealed_local. Same mechanism, same refusal class, two orders of magnitude less work, and it moves the control off a production module it never needed to depend on. DISCRIMINATION RE-VERIFIED AFTER THE CHANGE, not assumed from it: fn form returns true, operation form returns false. A cheaper control that stopped discriminating would be worse than the expensive one. WHAT I COULD NOT MEASURE LOCALLY, said rather than implied: every gunbc run pays a whole-corpus typecheck, so both probes report ~58s wall from this session and the witness-level cost the floor meters is invisible from here. The 54.9s and 516ms figures are the floor's own per-witness numbers, and CI is what will confirm the retarget landed under the ceiling. I am not claiming a local measurement I did not get. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Cut command_runner's local path onto shell.Exec.RunArgv: argv stops round-tripping through a shell THE CHAIN THAT IS NOW GONE from the local arm: render the argv to quoted text, wrap it in a bash heredoc, hand it to a shell, let the shell split it back into an argument vector -- to reach a seed that ends in Command::new(argv[0]).args(argv[1..]) regardless. Every step existed only to undo the step before it. On LocalExec command_over_transport is the IDENTITY, so the render had nothing to transform either. Deleted from that path rather than routed around. MEASURED FIRST, because the assignment's census was stale by construction: 22 live call sites across 5 modules (not 25 across 6), 17 of them run_shell_command_capture. ALL 22 PASS LocalExec -- zero use SshExec -- so the entire live population moves in this cut. The callers are untouched: the change is internal to command_runner and both signatures are preserved. THE ONE ENABLER, and it is the part worth reviewing hardest. ArgvCommand.argv is a runtime List<String>; CliSurface is sole_constructor and its only construction route is through CliArgumentSyntax fragments, which carry declared token classes and bindings. Fragments structurally CANNOT express a word that does not exist until the program runs -- a filesystem path, a hostname. So cli_surface_of_literal_words was added to v2.std.compilers.cli_surface. WHY THAT IS NOT THE AMBIGUITY THE CARRIER EXISTS TO CLOSE: the refused state is a List<String> arriving at an argv position with NO declared role, where "one word whose text is the concatenation" and "N separate words" are both well-formed and the realization must guess. This constructor IS the declaration -- its name says each element is exactly one argv word. It is the same resolution the interpreter refusal I landed earlier tells authors to reach for. The file states what it does not license: an argument whose spelling is known at authoring time belongs in fragments, and reaching for this instead is modeling debt. EMPTY ARGV REFUSES rather than defaulting -- a command with no words names no program, and inventing one is fabricated output. THE SSH ARM IS UNTOUCHED, deliberately. Its prefix-append shape is wrong in kind (RFC 4254 carries one string, so the inner command is a nested serialization target, not a concatenation) and that target belongs to another lane. Two sessions editing one contested branch is worse than either fix. It also carries no traffic through this module today, which is why leaving it cost nothing. THE success FIELD is derived through a NAMED policy -- process_exit_is_admitted(ExitZeroSucceeds) -- rather than a bare exit_code == 0, so the convention this runner applies is something a caller can change rather than a literal to discover. WHAT STILL COLLAPSES, named and not fixed here: "ran and exited nonzero" and "could not be executed at all" both arrive as success: false. Under the old bash hop those were genuinely indistinguishable -- a missing binary became the shell's exit 127, which claims a process ran when it never existed. Going direct removes the shell that fabricated that code, so the distinction is now AVAILABLE at the transport even though ShellCaptureResult cannot express it. Not repaired in this cut because it is not free: 17 call sites read that record and the destination is the ProcessOutcome coproduct one module away, so the repair belongs with the sites it changes. THE DISCRIMINATING RECEIPT, executed wet against a real process: argv ["printf", "%s|", "a b"] direct exec -> one operand "a b" -> stdout "a b|" OBSERVED via a shell -> two operands -> stdout "a|b|" asserted absent All three assertions pass. A green that would still be green with the bash hop restored would prove nothing about what changed, which is why the subject is an argument the two paths DISAGREE about rather than a command that merely succeeds. IT IS WET AND EXCLUDED, for a reason that is structural rather than convenient: hermetic evaluation replays an operation's declared mock_response and never constructs an argv at all, so "the words reached the process unsplit" is not observable hermetically. A hermetic version could only assert the mock, which is specification-without-execution. Excluded exactly as the prior argv receipt is, and the file says so. DIVERGENCE FROM THE RECORDED TRIGGER, stated rather than left for a reader to notice: command_runner_dissolution_trigger names host_effect_apply binding ArgvCommand execution as a typed transport handler. This cut routes command_runner directly at shell.Exec.RunArgv instead. The trigger's second clause -- retire the shell_exec_via_bash glue -- is satisfied for the local arm and NOT for the SSH arm, so the trigger is not yet discharged and I have left it in place rather than claiming it. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Restrict the literal-words mint to its two callers; state what CI does not guard; correct the trigger Three review items, all taken. The first is the one that mattered and my semantic defence of it was insufficient. 1. THE MINT IS NOW admit_callers-RESTRICTED. My argument was that a constructor whose name says "each element is one argv word" IS the declaration the refused state lacks, and that stands -- but the declaration was UNBOUNDED. Anyone could make it, about anything, which left the interpreter's argv refusal one import away from being routed around: not defeated, just satisfied by an intent nobody checked was true. Nominal wall, not structural. The admitted population is TWO -- run_shell_command and run_shell_command_capture -- which is what makes the restriction honest rather than aspirational. A third caller is an edit to the list in the declaring module: a counted review event rather than an import written elsewhere. VERIFIED BY EXECUTION, with a discriminating RED rather than by reading the declaration -- which matters more than usual here, because I spent this session proving that this exact mechanism is ACCEPTED AND INERT at operation grain. An unadmitted module calling it is refused: constructor call admission refused: 'v2.std.compilers.cli_surface.cli_surface_of_literal_words' refuses call from 'test.fixture.mint_admit_probe.intruder.unadmitted_mint' — permitted callers: [gunbc.command_runner.run_shell_command, gunbc.command_runner.run_shell_command_capture] Located, names the caller, lists the roster. The admitted callers still work: the wet receipt passes unchanged. This is a fn, which is the grain where the mechanism is verified to fire. The file's note that authoring-time spelling belongs in fragments carries no enforcement, and now says so rather than reading as a wall. 2. WHAT GUARDS THIS CUT, AND WHAT DOES NOT, written where the next author stands. The property "the local path reaches no shell" is established wet and the receipt is FLOOR-EXCLUDED, so CI does not run it and someone reintroducing a render-and-bash hop gets no signal. The exclusion is structural -- hermetic evaluation replays mock_response and never constructs an argv, so a hermetic version could only assert the mock -- but the consequence is a real gap and the module now states it: rung mitigatable, next-rung trigger a wet lane that executes floor-excluded receipts. A green test that nothing runs is exactly the inert evidence DESIGN calls a lie, and the file should not read as enforced. 3. THE TRIGGER NAMED A MODULE THAT WAS NEVER BUILT. Asked whether I had created PARALLEL AUTHORITY rather than whether I matched wording, I measured: there is no host_effect_apply production module (it exists only as a witness test), and host_effect_realize never mentions ArgvCommand. command_runner is the ONLY module that turns an ArgvCommand into a local process. The other ArgvCommand consumers reach shell_command_render, which serializes argv into TEXT for emission (githooks) or for the SSH leg -- a different destination, not a second local-exec route. So this did not diverge from the trigger; it satisfied a better version of one that named a binding nobody wrote, and satisfying it literally would have meant building the second route DESIGN forbids. The row is rewritten to name the condition that actually remains: the SSH arm, which needs the nested command-string target another lane owns, and at which point shell_exec_via_bash and retained_runtime leave this module entirely. Also fixed in passing: my own trigger rewrite wrote a \\U escape into the .dag string instead of the literal character, which made the module unparseable. Caught by resolving the file rather than by reading the diff. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Correct a false premise in the trigger I just rewrote: host_effect_apply exists The conclusion was right and one clause of its evidence was false, which is worse than usual here because it sits in a REPLACEMENT trigger -- the row exists to stop the next author re-deriving the question, and a false premise makes them do it anyway. WHAT I WROTE: no host_effect_apply production module exists, witness test only. WHY I GOT IT WRONG: I searched for a FILE named host_effect_apply*.dag and found only the witness test. It is a FUNCTION. gunbc.host_effect_realize declares host_effect_apply and host_effect_apply_gated and both are production. That is the third scope error of this session in one family -- a limited view read as the population -- and the specific lesson is narrower than the earlier two: searching for a filename does not answer a question about a symbol. WHAT ACTUALLY CARRIES THE ARGUMENT, verified independently rather than taken from the correction: host_effect_realize contains ZERO occurrences of ArgvCommand and does not appear among that type's consumers. So host_effect_apply exists and dispatches effects, but it never reaches an ArgvCommand and is therefore not a second route from an ArgvCommand to a process. command_runner remains the sole one, there is no parallel authority, and satisfying the original trigger literally would still have meant BUILDING the second route rather than finding it. The row now says that, and records the correction in place rather than quietly overwriting it, so a reader who saw the earlier claim learns it was wrong instead of wondering which revision to believe. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Replace ShellCaptureResult with ProcessOutcome across every capture site THE CONFLATION, corrected from how we first described it. I claimed in the previous commit that removing the shell's fabricated 127 made "could not be executed at all" available beside "ran and exited nonzero". I TESTED THAT AND IT IS FALSE: a missing program does not produce a result record at all, it REFUSES the evaluation -- failed to execute 'no_such_binary': No such file or directory (os error 2) -- so spawn failure was already fail-closed one rung above the record, and the RED first proposed for this work would have passed against the old record too. The real conflation is one step over and it was live at EIGHT sites: ran and FAILED, printing nothing -> success=false, stdout="" ran and SUCCEEDED, printing nothing -> success=true, stdout="" Both are stdout == "". Those eight read stdout without consulting success, so a failed probe and an empty result were the same value. THE EIGHT, AND WHAT EACH NOW DOES: fleet_host_key_enrollment.check -- THE WORST ONE. Tested trim(stdout)=="present" with no success check, so a probe that FAILED produced "" != "present" and fell through to the branch that APPLIES. A refusal to read authorized_keys was indistinguishable from the key being absent, and the remedies are opposite. Now: refusal refuses and does not mutate the file. fleet_host_key_enrollment.verify -- did concat("outcome=", trim(stdout)), so a refused verify wrote the literal receipt line "outcome=" into a file someone would later read as fact. Now: outcome=UNKNOWN with the cause. fleet_host_key_enrollment.{user,hostname} -- display only. Routed through process_outcome_receipt_text, which renders the three arms to three DISTINCT strings; a refusal can no longer read as empty. fleet_probe_identity_observe.user -- display only, same route. fleet_probe_identity_observe.{passwd_home,job_home} -- USED AS PATHS, not just printed, so they match the arms directly: "(refused: ...)" is fine to print and catastrophic to open. An unreadable home now skips the probe with a stated not-probed line instead of reading .ssh/authorized_keys off a fabricated root. fleet_converge_plan_cli hostname -s -- SURFACED, NOT CLOSED, and said so in file. A `-> String` function has no way to refuse; the honest repair changes the return type and cascades into converge plan subject identity. It now returns a value that CANNOT be mistaken for a hostname rather than a plausible "", so a plan keyed on it is visibly wrong instead of silently wrong. Rung: mitigatable, with the next-rung trigger named. SITES THAT GENUINELY DO NOT NEED THE DISTINCTION, stated rather than left silent: fleet_converge_plan_cli test -f -- exit status IS the product, no stdout anyone wants. Asks process_outcome_admitted directly. Forcing it through an output-bearing variant would add a field it cannot answer. ssh-keygen -F readback -- same shape, same treatment. fleet_ssh_credential_verify x2 -- decompose into a classifier that consumes all three values TOGETHER, so the correlation was already performed. The match adds exhaustiveness and names ProcessOutputAbsent, previously indistinguishable from a failure with empty stdout. DELETED, not kept beside: type ShellCaptureResult is gone. Its one fabricated construction is gone too -- fleet_host_key_enrollment built a ShellCaptureResult to stand in for a FILESYSTEM write failure, inventing success:false for something that was never a process. The coproduct makes that unwritable. scan_host_key_lines shows why the type fits: `scan.success && trim(stdout) != ""` IS ProcessOutputPresent, so a hand-written correlation became a variant. And ssh-keyscan exiting 0 with no key is now a named outcome rather than being reported as a refusal with an empty cause. DISCRIMINATING RED, executed wet, six of six green: nonzero-exit-printing-nothing must be Refused and zero-exit-printing-nothing must be Absent. Both go red if ShellCaptureResult is restored, because then both are stdout == "". The file also records what is NOT tested and why -- the nonexistent-program case is already distinguishable via transport refusal, so asserting it would prove nothing. Recorded on the carrier: spawn failure is fail-closed at the transport, therefore A CALLER CANNOT PROBE FOR A BINARY'S EXISTENCE BY TRYING TO RUN IT -- the attempt stops the line instead of answering. Presence must be asked of something that exists. That is why a separate presence probe has to exist, and it is why no fourth "not spawned" variant was added: it would be an uninhabited arm every consumer must handle and none can reach. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Site 8: the poison IS persisted, and it defeats the guard — second row Checked rather than argued, and the answer is worse than "it might reach a receipt". fleet_converge_plan_wet WRITES host_short verbatim to fleet_converge_plan_subject_host_path, coerces it to NonEmptyStr as the plan's subject host, and folds it into the member-set fingerprint and the plan content hash. An unobserved hostname is persisted as a receipt that later reads as fact. AND IT DEFEATS THE GUARD BUILT FOR THIS EXACT CASE. fleet_converge_apply_wet re-observes the host and refuses on SubjectHostMismatch when observed != planned. Two consecutive refusals produce the SAME string, so the comparison SUCCEEDS and apply proceeds. The check whose entire purpose is to stop a plan being applied on the wrong host is satisfied by two non-observations agreeing with each other -- the empty-observation narrow relocated to the guard: bottom == bottom read as "same host". Making the marker unique per call would NOT repair it; it converts a false match into a false mismatch, which is a different wrong answer, not an observation. NOT INTRODUCED HERE, stated precisely: the prior code persisted "" and compared "" == "", which passed identically. This migration does not repair the defect -- it makes the persisted evidence legible instead of blank. Filed as a SECOND row rather than folded into the first, because the first row's claim (visibly wrong rather than plausibly empty) says nothing about reachability and this row is entirely about reachability. Both mitigatable; different next-rung triggers. This one's: the subject-host comparison consumes an outcome rather than a String, so unobserved-vs-unobserved is a REFUSAL to compare, not an equality. The block is hoisted to module scope as a leading annotation on the declaration (§4c), not left inside the func body. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Hoist 29 body annotations to module-item grain (§4c), and integrate main's command_over_transport refusal coproduct TWO SEPARATE THINGS, both landing here because CI surfaced them together. (1) THE §4c REFUSAL, 29 sites across four files. I put per-site rationale where the explanation belongs conceptually -- beside the line it explains -- which is exactly the position the language refuses. Hoisted every block to a consolidated leading annotation on the declaration. WHAT I ACTUALLY GOT WRONG, since I had already hit this twice: I fixed ONE block earlier and reported it as fixed. I repaired the instance the error named instead of the class the RULE names. The sweep this time is the whole branch and then the whole corpus -- both now zero indented `//`. The refusal is correct and I am not routing around it. It is fail-closed at the source boundary, typed, located to the byte, and it stopped the line rather than silently dropping the prose. The corpus already tried the alternative: `//` as an outright parse error made comment SYNTAX unwritable without making commentary unwritable, and prose migrated into `data ...: String` rows where intent is mechanically indistinguishable from program data. (2) THE MERGE, which was NOT a text conflict to pick a side on. main landed the command_over_transport refusal coproduct (Built | Refused, #8596) while this branch replaced the capture return type. Both arms of both functions had to be rebuilt, not chosen: run_shell_command SSH arm: Refused -> exit_failure with the rendered cause run_shell_command_capture SSH arm: Refused -> ProcessRefused, NOT the deleted ShellCaptureResult main still constructed there Taking either side whole would have been wrong in a way that still compiles on one of them: ours drops main's new refusal handling, theirs resurrects a deleted type. So I took ours and re-applied main's additions explicitly -- the imports, command_over_transport_refusal_reason and its note, and both refusal arms. Note the refusal now composes rather than collapsing: an SSH command that cannot even be BUILT is a ProcessRefused with a stated cause, distinct from one that ran and failed. That is the same distinction this branch exists to make, arriving from main's side of the merge. The LocalExec arm is untouched by the merge and still routes through RunArgv. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Take main's optional-hostname repair and re-express it on ProcessOutcome; DELETE my two mitigatable rows because they are no longer true MAIN FIXED THE DEFECT WHILE THIS BRANCH WAS OPEN, and it fixed it at the rung this lane named as the trigger rather than at the one I settled for. mine: -> String, returning a marker that cannot be mistaken for a hostname. Legible, still not a refusal. Two rows at mitigatable. main: -> NonEmptyStr?, Absent when the probe did not succeed. Plan AND apply refuse outright on Absent, and the subject comparison routes through fleet_converge_apply_subject_host_matches over two NonEmptyStr values instead of a bare String equality. That closes BOTH rows. Row 1 (the value is visibly wrong rather than plausibly empty) is obsolete because there is no longer a value. Row 2 (the poison is persisted, and two non-observations comparing equal DEFEAT the SubjectHostMismatch guard) is obsolete because Absent never reaches the comparison at all. SO I DELETED BOTH ANNOTATIONS RATHER THAN KEEPING THEM. A rung row that describes a defect the tree no longer has is not harmless documentation -- it is a false claim in the file that owns the fact, and the next reader plans against it. That is the stale-citation class this repo already pays for, and the cost is worse for a row asserting a LIVE SAFETY DEFECT than for a stale line number: someone would have re-escalated a fixed bug. WHAT I ACTUALLY CHANGED is only the probe's input shape. main derived Absent from `!run.success || trimmed == ""`, reading the record this branch deletes. The same judgment now reads the arms of ProcessOutcome, and the mapping is exact rather than re-decided: ProcessRefused -> none (did not observe) ProcessOutputAbsent -> none (ran, said nothing) ProcessOutputPresent, trims empty -> none (wrote bytes that do not name a host) ProcessOutputPresent, trims nonempty-> Present The third arm is the one worth stating: ProcessOutputPresent means the process WROTE BYTES, not that those bytes name a host, so the empty-after-trim guard main had is preserved rather than assumed away by the richer type. Also migrated this file's `test -f` site off `.success` onto process_outcome_admitted -- exit status IS the product there, which is why it takes the admitted projection rather than matching arms. CONVERGENCE WORTH NAMING: main's repair and this branch's migration are the same argument from two directions. Main gave the RESULT somewhere to say "not observed"; this branch gave the OBSERVATION somewhere to say it. Neither is redundant with the other, and the merged form is stronger than either -- which is why this resolution takes main's shape rather than defending mine. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * HealthzEffectiveRead becomes the coproduct it always was, and the rung is measured rather than claimed The carrier was { body: String, probe_error: String }, and all 20 of its constructions set exactly one field -- never both, because there is no such observation: a probe either landed and produced a body or refused and produced a reason. The empty string was doing the work of a tag, in a type that also admits the empty string as a legitimate body. It is now HealthzBodyRead | HealthzProbeRefused. ground_service_ready_from_healthz_with_bundle's probe check was the first clause of an if-chain; it is now a match, and the four stages below it split into ground_service_ready_from_healthz_body, which can only ever be reached with a body in hand. THE RUNG, PROBED IN BOTH DIRECTIONS, AND IT IS TWO RUNGS: FIELD ACCESS IS STRUCTURAL. A probe reaching read.body off a refusal made the floor refuse during strict-preparation -- 'no field body on type HealthzEffectiveRead', located, at modules_resolved=3729, before a single witness executed. THE BARE RECORD LITERAL IS NOT. A literal naming the coproduct with no variant tag still resolves and still constructs; it is refused only at the match, at evaluation. Measured: that probe PASSED pre-change (planned=9784, failed=0) and became a per-witness runtime FAIL post-change with the corpus fully executed, not a preparation refusal. So the construction half sits at mechanically preventable, not structurally impossible, and the carrier says so. Next-rung trigger is a compiler capability, named on the declaration: a record literal naming a coproduct type with no variant tag should refuse at resolve, where field access already does. readiness_check_order_note shrank from five ordered stages to four. PROBE left it because it is no longer ordered by anything; the other four remain ordering-by-discipline and the note says which and why. Floor: planned=9783 executed=9783 passed=9475 known_red_held=304 failed=0, against a pre-change baseline of 9784/9476/304/0 -- the delta is exactly the deleted probe. The 4 stale-quarantine rows are identical in both runs and are inherited from main, not from this change. * File the argv fabrication finding: real in the code, unreachable at declared grain, NOT admitted push_shell_argv_tokens ends in two arms that push the format! Display rendering of a value as a host argv word. Null becomes the word 'null', Map and Set become brace-wrapped renderings, Record becomes its type name plus fields -- fabricated plausible output in argv position rather than a crash. For Int, Float and Bool the same arm is correct and wanted, so deleting the fallback would break the good half. REACHABILITY: no declared argv site in the tree can carry a structured value there. All 258 shell-transport operations enumerated, every argv element classified -- 889 string literals, idents typed List<String> / ProcessArgvExpansion / String / NonEmptyStr / FilePath, and calls each returning List<String> or String. Nothing else. Both production callers draw from that population. cargo_build Build does declare env: Map of String to String inside a shell-transport operation, but it is an env input, never an argv element -- a probe matching on the operation rather than on the argv list would have reported a fabricator that cannot execute. The claim is unreachable-at-DECLARED-grain, not unreachable: declared types are not construction-enforced (3939 WhereRefinementUnenforced, no refinement predicate evaluated on any kernel). NOT ADMITTED, failing the standing in both directions: it is not DefectRepairDiagnosticsMayMove because that class needs a behavior the seed exhibits today and an unreachable arm exhibits nothing; and it fails the 2026-08-20 purpose test because hardening a dead seed arm serves v1, not the v2 self-host program. Refusal dominates, so it is recorded rather than fixed, with the one thing that would make it admissible named: a reachable specimen. Floor unchanged: planned=9783 executed=9783 passed=9475 known_red_held=304 failed=0, no errors, no refusals. * Sharpen the next-rung trigger: the decision procedure exists, the refusal does not The trigger read 'a compiler capability', which implies infrastructure to be built. That is not what is missing. v1.compiler.types is_coproduct_type answers the question in one expression -- n.connective == Disj -- and record-literal inference already resolves the literal's named type and already reasons about coproduct membership on the neighbouring path (lookup_variant_parent_enum, variant_owner_node, record_lit_variant_from_expected, record_lit_expected_coproduct). What is absent is the judgment, not the fact. Stated at the reach measured: those symbols answer the VARIANT-named literal (this name is an arm, whose parent is X); the failing case is the PARENT-named literal, which is a different question, and the refusal is neither built nor tested here. So the row moves from DESIGN 4b's second category (can climb after one grounding) to its third (can climb now but unbuilt). Also records the trap for whoever builds it: is_coproduct_type is sufficient for the direct, exactly-resolved specimen; a generalization must apply it to the RESOLVED STRUCTURAL declaration rather than assume every authored alias node carries Disj, or it would silently admit the construction it exists to refuse. Floor: planned=9783 executed=9783 passed=9475 known_red_held=304 failed=0, no errors, no refusals. --------- 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>

… (brief: docs/plans/shell-dag-census-0a-brief.md) (#8662) * SHELL-DAG-CENSUS-0A: stop condition — file the projection blocker and the derived shell seed The brief's stop condition fires. No detector was built and no text-scanning census was substituted; this commit files the finding the brief asks for in that case. The whole fact surface .dag can read is three accessors in coproduct_reflection.rs — types, fns/funcs, data inits. ItemKind::ServiceItem has no accessor, so transport declarations are invisible, and FnArrowDecl.output is a wiring-liveness skeleton whose statement fold DROPS a let-bound RHS not referenced toward the return. Five axes with five distinct remedies, each with its own evidence; the gunbc.spark_managed_access_apply chain is a worked proof that all five are capability gaps rather than API preferences — a match-arm binder, a named argument label, a service operation and a transport stdin channel, one per axis. Also files the shell-interpretation seed derived from what interprets bytes as shell, which is needed under whichever remedy lands. Findings that were not expected: of 17 shell-interpreter argv literals, 10 sit in product fn bodies as ArgvCommand constructions (one with a computed program), not in extdeps declarations, so a service-declaration projection alone would miss the majority; and "--" is overloaded three ways across 46 sites (ssh re-root, systemd-run re-root, cargo argument pass-through, git end-of-options), so the re-root reading is a per-program extdeps citation duty and not something the census may infer from the token. Records one specimen found on the way: v2.compiler.source_authority canonical_dag_source_parse_print_law has zero callers anywhere in the tree — a parse/print law that nothing executes, DESIGN §5 specification-without-execution in the compiler's own source authority — which is why "the full-fidelity parse route exists in .dag" is not evidence that it works on the real corpus. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01QFxNVPeTcYeCjP7rQyLtZu * SHELL-DAG-CENSUS-0A: add executed evidence for axes 2, 3 and 6, and measure the parse route Axis 2 and axis 3 were argued from reading the Rust marshal; they are now proven by execution. A fixture pair of identical shape folded through fn_arrow_decl_facts_live: fixture_dead_let_shell (binds the call, does not use it) yields ZERO atoms — callee identity and program literal both absent — while fixture_live_named_args yields "fixture_sink2 | echo LIVEMARKER | echo ARGSMARKER". Same construct, opposite verdict, so the loss is the projection's and not the probe's. The live arm also shows axis 3 directly: three atoms in authored order with no labels, so nothing says which literal was program: and which was args:. Axis 6 is new and was measured, not read. The reflection registry is the ENTRY'S IMPORT CLOSURE, not the corpus: a fold over fn_arrow_decl_facts_live under both production roots reported 1,698 fn/func declarations against 41,965 declared in the tree, about 4%. This is a declared frontier rather than a discovery — corpus_dependency_view already refuses per-PR when fn_arrow_decl_substrate_is_whole_tree is false ("blocked-on-#6239") — but it is fatal for a census specifically, because files disappear through non-import with no per-file ParseRefused row to count them. That is the empty-observation narrow: never-loaded is indistinguishable from carries-no-route. The full-fidelity parse route is measured against a positive control. The tree's own three-line fixture ACCEPTS, a real 28-line corpus file ACCEPTS, and dag/extdeps/shell/exec.dag REJECTS with reason=parse_grammar_choice_overlap_residue. So the route is real and its failure is a located typed refusal, but the file it refuses declares shell.Exec.Run/RunArgv/Check — the census's most load-bearing seed file. Records that accepts-or-refuses was the wrong frame: there is a third outcome, accepts but is unaffordable at corpus grain, and it is the one the prior cost signal makes likely. Affordability is being measured as a slope over a random 40-file sample rather than extrapolated from the fixture, since fixed overhead and per-byte cost are different curves. If it lands there, DESIGN §6 already rejected this shape once in #8140 — "the unit of computation was the world, the unit of fact was one module's authorship" — and its declared next-rung trigger is exactly axis 1's remedy: one module's facts from one module's source, checked at ingestion where the module is parsed anyway. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01QFxNVPeTcYeCjP7rQyLtZu * SHELL-DAG-CENSUS-0A: measure the parse route on both axes — it is outcome 3, and it fails correctness too Accepts-or-refuses was the wrong frame; there are three outcomes and the measurement lands on the third, with a correctness failure alongside it. CORRECTNESS. On a random 10-file corpus sample the route accepted 6 and refused 4, and ALL FOUR refusals carry the same reason as the earlier dag/extdeps/shell/exec.dag refusal: parse_grammar_choice_overlap_residue. The grouping is the finding, not the rate — one grammar deficiency with many victims rather than scattered file-specific problems. So the route is a single repair away from a much larger accepted population, and no census can run on it until that repair lands, because the merge bar is zero production parse refusals and the refusal set contains the census's own seed file. AFFORDABILITY, measured as a slope rather than extrapolated. 1 file / 372 B / 63.1 s; 10 files / 5,332 B / 67.5 s; 40 files / 388,527 B / EXIT=137, OOM-killed after 34 files. Marginal cost is about 0.49 s per file against about 62.6 s of fixed world-acquisition overhead, so TIME IS NOT THE WALL. Memory is, and it is not about big files: the kill came at file ~34 with only 94 KB of source consumed, on ~7.8 KB files, with the 212 KB outlier sorted last and never reached. The fold accumulated only a short result string, so the retention is not the probe's accumulator. Whether it is parse-tree retention or interpreter heap growth is NOT established here and is not claimed; what is established is that the process cannot hold 34 small files against a subject of 3,733 files and 31.3 MiB. Both facts point the same way, and DESIGN §6 already rejected this shape in #8140 — "the unit of computation was the world, the unit of fact was one module's authorship". Recommends the ingestion-side projection over a census-side fold, enumerated as the six axes' remedies, with 0A rebasing onto it. Notes parse_grammar_choice_overlap_residue as worth filing on its own: a named grammar deficiency refusing a large fraction of authored source in the compiler's own parser, invisible today because the only path that would surface it has no callers. Two instrument faults on the way, same root and worth naming: a grep filter discarded every line of a run, and a missing `bc` silently emptied the timing field while the surrounding output looked healthy. Both failed toward absence, not toward a wrong number. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01QFxNVPeTcYeCjP7rQyLtZu * File the projection increment spec and the grammar-deficiency finding Two specs, no implementation. The increment lands partly in the frozen v1 seed, whose admission test is purpose — does the change serve the v2 self-host program — and this increment serves a shell-migration census, so the call is the operator's and no seed work starts on lane authority. The increment spec is written for someone deciding admission rather than for an implementer. It leads with the empty-observation narrow rather than the coverage percentage, because that is the part that makes the substrate unusable rather than merely partial: a file that was never loaded reads identically to a file carrying no shell route, and no per-file ParseRefused row exists to count the difference, so a census on it yields a clean confident population that is silently wrong. Each of the six axes carries its own evidence grade rather than being presented as uniformly established — axes 2 and 3 execution-proven by the discriminating fixture pair, axis 6 execution-measured, axis 1 structural and independently verified, axes 4 and 5 read from the marshal. The counting method is stated beside the axis-6 denominator because it will be questioned: 41,965 counts line-start fn/func/test fn and matches the accessor's own filter, since ItemKind has no separate test variant and a test fn IS an FnItem; 30,851 is the same count with the 11,114 test declarations removed. 1,698 visible is 4.0% or 5.5% and the conclusion is invariant. Two properties are separated for the admission call: axes 2-5 are an ADDITIVE second accessor rather than an edit to the existing marshal, whose lossiness is load-bearing for v2.lens.wiring_liveness and must not change; and axis 6 is probably already-sanctioned work pending #6239 rather than anything this increment requests. The admission question is recorded with both readings and no advocacy. The grammar finding is filed separately because it outlives the census. Five refusals across two source roots, four sampled at random plus the independently-found extdeps/shell/exec.dag, all carrying one reason: parse_grammar_choice_overlap_residue. No corpus rate is claimed from ten files; the shared cause is the finding. It is invisible because the only path that would surface it, canonical_dag_source_parse_print_law, has no callers — the unexecuted law and the unmeasured deficiency are the same fact seen twice. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01QFxNVPeTcYeCjP7rQyLtZu --------- 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>

gunbai-bot Bot marked this pull request as ready for review July 4, 2026 23:25

briansrls and others added 8 commits July 5, 2026 01:07

WIP: P3+P5: infer whole-corpus scans to per-module maps

1c01f0c

WIP: P3+P5: infer whole-corpus scans to per-module maps

e0cc6f6

WIP: P3+P5: infer whole-corpus scans to per-module maps

76774e4

fix: balance concat wrappers in compiler_tests emit artifact

76bbc23

Commit 1f02caa added variant_surfaces strings to ct_profile_reconcile_test without four matching v1_rt::concat( openers, breaking rustc parse. Co-authored-by: Cursor <cursoragent@cursor.com>

WIP: P3+P5: infer whole-corpus scans to per-module maps

06c7e23

briansrls force-pushed the session/loyal-heron-170 branch from 31714cf to 880f21d Compare July 5, 2026 01:08

chore: delete orphaned local_authority_binding after P3 index rewrite

de7a0e3

Superseded by build_type_name_export_index canonical_binding lookup; no call sites remained. Co-authored-by: Cursor <cursoragent@cursor.com>

briansrls and others added 2 commits July 5, 2026 01:32

WIP: P3+P5: infer whole-corpus scans to per-module maps

7141fa1

fix(tests): satisfy clippy type_complexity on witness fixture helper

f335f96

Extract ResolvedGraphFixture type alias for resolved_module_graph return tuple so rust_tests clippy gate passes with -D warnings. Co-authored-by: Cursor <cursoragent@cursor.com>

briansrls and others added 3 commits July 5, 2026 02:11

Merge remote-tracking branch 'origin/main' into session/loyal-heron-170

192d3c1

WIP: P3+P5: infer whole-corpus scans to per-module maps

d212b0f

fix(ci): regen ci.yml to match floor-job serialization policy

e42c9d2

ci_workflow.dag already gates the floor job on rust_tests (20m budget); regenerate ci.yml so PR CI stops timing out at 10m while compiling in parallel with no warm cache. Co-authored-by: Cursor <cursoragent@cursor.com>

briansrls and others added 3 commits July 5, 2026 03:04

gunbai-bot Bot mentioned this pull request Jul 7, 2026

PR-2 (Fix-1): reconcile-first — kill the merge-side O(M²) parent-surface copy (byte-identical) #6360

Merged

gunbai-bot Bot mentioned this pull request Aug 19, 2026

Close the argv representation-ambiguity class at the seam, and correct two gates that claim enforcement they no longer have #8549

Merged

gunbai-bot Bot mentioned this pull request Aug 20, 2026

SHELL-DAG-CENSUS-0A: derive shell execution routes from parsed bodies (brief: docs/plans/shell-dag-census-0a-brief.md) #8662

Merged

Navigation Menu

Repository navigation

P3+P5: infer whole-corpus scans to per-module maps - #6239

P3+P5: infer whole-corpus scans to per-module maps#6239
briansrls merged 38 commits into
mainfrom
session/loyal-heron-170

gunbai-bot Bot commented Jul 4, 2026

Uh oh!

gunbai-bot Bot commented Jul 5, 2026

Uh oh!

gunbai-bot Bot commented Jul 5, 2026

Uh oh!

gunbai-bot Bot commented Jul 5, 2026

Uh oh!

gunbai-bot Bot commented Jul 5, 2026

Uh oh!

gunbai-bot Bot commented Jul 5, 2026

Uh oh!

gunbai-bot Bot commented Jul 5, 2026

Uh oh!

gunbai-bot Bot commented Jul 5, 2026

Uh oh!

gunbai-bot Bot commented Jul 5, 2026

Uh oh!

gunbai-bot Bot commented Jul 5, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

1 participant

Conversation

gunbai-bot Bot commented Jul 4, 2026

Worker attestation

Summary

Test plan

Uh oh!

gunbai-bot Bot commented Jul 5, 2026

Uh oh!

gunbai-bot Bot commented Jul 5, 2026

Uh oh!

gunbai-bot Bot commented Jul 5, 2026

Uh oh!

gunbai-bot Bot commented Jul 5, 2026

Uh oh!

gunbai-bot Bot commented Jul 5, 2026

Uh oh!

gunbai-bot Bot commented Jul 5, 2026

Uh oh!

gunbai-bot Bot commented Jul 5, 2026

Uh oh!

gunbai-bot Bot commented Jul 5, 2026

Uh oh!

gunbai-bot Bot commented Jul 5, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

1 participant