Repository navigation
Exclusive cost partition + selected-set closure overlap (Lane B slice 1, measurement only) - #7483
Conversation
…only) Lane B slice 1, subject entry-graph-union-construction. No union implementation, no eviction/retention change, no walk_memo or #6999 memo fork. A. The resolve-split counters could not be quoted as shares because the children and the parent are drawn from DIFFERENT UNIVERSES, not because they nest. ResolveStageNanos accumulates over every resolve the thread runs -- witness entries and machinery entries alike -- while the receipts printing it quote a parent covering only one of those sets. Executed receipt: a single-entry claim_batch reports load=48468ms against a 45308ms parent, and the span account shows why -- two top-level resolves ran (the witness entry plus dag/gunbc/output_policy.dag), so the rows summed 65.3s of spans against a 41.0s denominator. ResolveSpanAccount adds the one window that contains every stage row by construction, and exclusive_cost_partition reports against it. The law parent == sum_exclusive + remainder holds by construction (remainder is derived, tolerance 0ns); what makes it non-vacuous is that it refuses -- OverAttributed, NestedSpanAttribution, NoSpans -- instead of clamping, which is the shape the existing saturating_sub `other=` row uses to hide exactly this condition. share_of_parent returns None unless Reconciled. Basis is named and additive: summed top-level resolve span nanos, thread-sequential. Elapsed wall is not additive over concurrent worker spans, so it is carried under `observations` and never partitioned. assembly_rewire's three sub-passes are carried as explicit inclusive rows and never enter the exclusive sum. B. measure_selected_closure_overlap composes the production machinery -- discover_floor_witness_roster, the floor_diff_observe unified and name-status observations, entry_eligible_for_discovery_skip_before_resolve, and collect_both_closure_module_names_for_entry -- so the measurement reads the floor's own selection rather than a parallel hand-written model. It resolves and typechecks nothing: the output is an upper bound on repeated module membership, not a wall-time saving. A selector or diff-observation refusal propagates rather than widening to measure-everything. Both probes carry the same dissolution trigger as ResolveStageNanos: a .dag PerformanceReceipt carrier consumed by a floor witness. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…etic Ten controls, green by execution, plus a mutation proving they refuse. The law holds by construction, so the tests that carry weight are the ones that make it fail. Disabling the OverAttributed arm (the saturating_sub shape that hid this condition in the first place) turns exactly refuses_over_attribution_instead_of_clamping_to_zero and json_marks_a_refused_partition_unquotable RED and leaves the other four green -- so the controls discriminate rather than merely pass. Each refusal arm has an input reaching it (OverAttributed, NestedSpanAttribution, NoSpans), and every refused state asserts share_of_parent == None: a share quoted off a non-partition is the fabricated plausible output DESIGN §5 forbids. The rewire sub-rows get a double-count control fixing them as inclusive. The overlap arithmetic pins both degenerate poles, including the one that would CLOSE the union program (fully disjoint closures -> factor 1.0, upper bound 0) and the empty selection that must report null rather than let 0/0 become 1.0. Executing them caught a real arithmetic error in the percentile control's own expected values (3+2+1+2 = 8, not 7) -- the implementation was right and the test was wrong, which is the direction that only execution can tell apart. measure_whole_tree_resolve now emits the partition too. It runs the monolithic compile_to_resolved path, which fills no stage row and opens no resolve span, so it refuses with NoSpans -- making "this probe carries no stage attribution" an executed receipt rather than a prose claim. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
REQUEST_CHANGES was correct: this file has an established SCAFFOLD (§7 HAND-RUST — <marker>) convention -- ROADMAP lane, Unblock, an explicit DELETE WHEN list, a greppable receipt, and a declaration test -- and a generic "a .dag PerformanceReceipt carrier" trigger is not that. Both scaffolds now carry the full block. A (cli_run_exclusive_cost_partition_probe) names the concrete lane the ResolveStageNanos rows it partitions already declare: ROADMAP §2 Minimal work — caching by realization / realization-measurement-loop.md Phase 0, dissolving when compute_fabric.PerformanceReceipt keyed by cache-subject hash rolls into CostAccount.time = Measured and a floor witness consumes it. It adds no second measurement authority; it makes the existing rows' denominator honest. B (cli_run_selected_closure_overlap_probe) is typed as a ONE-SHOT INSTRUMENT with an explicit deferral: delete when the slice-2 union verdict is taken, WHICHEVER WAY IT GOES -- if the program proceeds its own receipts supersede this, and if it is shrunk or closed the probe has discharged its purpose. A standing closure-overlap reader belongs in v2.lens.affected_set over the containment tree, not in seed Rust, so this deliberately does not become permanent host-side machinery by default. The receipt lines report their real hit count instead of inheriting the convention's error: both older markers in this file claim `== 1` and actually sit at 5 and 4 hits, so a copied claim would have been false on arrival. What the receipt checks is that the marker reaches 0 at deletion, not a fixed count. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
|
Addressed in What was wrong. A — B — One correction to the convention rather than a copy of it. Both older markers assert On the line count: of the 1,291 added, 234 are the two control modules and 124 the probe bin. 21/21 controls green by execution, including the two new marker declaration tests. The |
The probe defaulted its exclusions to whole_tree_probe_exclusion_substrings, which is the floor's witness_exclusion_substrings UNION the whole-tree strict-resolve exclusions. That is the right list for a whole-tree RSS probe and the wrong one here: it made the roster 45 entries against 579 *_test.dag files under the same scan dirs, so the overlap statistics were being drawn from roughly 8% of the corpus the floor actually selects over. A subject drawn from 8% of the corpus cannot answer a question about the corpus, and the failure is invisible in the output -- every derived quantity is internally consistent and simply describes a different, much smaller population. Defaulting to gunbc.ci_layer_roots.witness_exclusion_substrings (the floor discovery authority, the same list run_discovery_corpus passes) puts the measurement on production's population. Caught by checking the reported roster size against the corpus rather than against the receipt's own internals. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Both halves measured, machine-readable receipts stored beside the writeup. A. Exclusive partition reconciles (tolerance 0ns, remainder 55.1ms of 73158.3ms). load is 68.2% of resolve-span time, typecheck_compute 24.4%, everything else 7.4%. Machinery is 37.7% of all resolve-span time even in a single-entry run. The load-bearing detail: load IS the closure walk, and its inner scan referenced_module_paths_in_text is a full-content byte scan run once per (entry, module) pair with no memo -- so B's duplication factor is not an abstract ratio, it is the multiplier on the dominant cost. B. Three real subjects from already-known main commits. Duplication factor 35.9 / 38.4 / 38.3 across 3 / 13 / 29 changed paths -- stable across a 10x range of diff breadth, so overlap is a property of the corpus shape, not of the diff. 97.2-97.4% of closure memberships are repeats. The union is nearly saturated at the narrow subject: N grows 37% while the union grows 15%. Max fanout is ~N in every subject; the median module is rare and falls as N rises, so the shape is a universal std core plus a long private tail. Verdict: STRENGTHENS the premise and RELOCATES the prize. The pole that would have closed the program (disjoint closures, factor 1.0) is decisively absent. But the prize is in load, not typecheck -- typecheck_compute is already content-key memoized through typed_module_cache, so a union justified as "typecheck once" would buy something largely already owned. And because the repeated unit is a pure function of source content, a per-source memo keyed on content hash would collapse the same 35.9-38.4x on the scan portion with NO union graph. Slice 2 should price that rival before committing. Recorded as a finding, deliberately not implemented -- this deliverable is measurement. resolution_divergence_census is kept separate as instructed: it runs as its own binary, so its closure-scoped resolve is a different process that an in-process union cannot displace. The receipt also records a fidelity defect caught mid-measurement: the first run's probe exclusions produced a 45-entry roster against 579 files, and every derived quantity was internally consistent while describing 8% of the corpus. Invisible from inside the receipt; caught only by checking the roster against the corpus on disk. Those numbers are withdrawn. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
|
Measurement complete — both halves, with the verdict. Receipts committed at A — exclusive partition (verdict
Machinery is 37.7% of resolve-span time even in a single-entry run. B — closure overlap over the production-selected set, three already-known main commits:
Verdict: strengthens the premise, relocates the prize. The pole that would have closed the program (disjoint closures → 1.0) is decisively absent. But
Two corrections worth flagging:
The last red ( No local timing figure here is offered as implementation acceptance; arm64 fleet receipts remain required before any implementation. — sent from smart-moth-595 |
My previous fix edited DESIGN.md directly and the CI auto-heal bot reverted it in 9d63c73 -- correctly. DESIGN.md is a GENERATED artifact (gunbc.generated_artifact DesignArtifact -> gunbc.design_document expected_design_md), so a hand edit to it is a change to the projection while the authority still says otherwise, and the drift gate regenerates it away. The authority is dag/gunbc/design_document.dag. That is the same shape DESIGN §5 names from the other side: a check satisfied by editing the declaration while the realization lies. Here the realization was edited while the declaration lay, and the healer is what made it observable rather than silent. The citation now lives in design_document.dag and DESIGN.md is regenerated from it via the declared regenerator (main_wet on dag/tools/generated_artifact_gate.dag), so the two are a fixed point. Verified by execution before push: doc_graph_has_no_orphan_docs on both entries, doc_graph_is_clean, and the drift witnesses witness_committed_is_fixed_point, witness_committed_fixed_point_red_control, witness_all_known_committed, witness_registry_complete all pass. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
|
Self-correction, posted before more reviews land on it: the A.6 mechanism claim in this PR is REFUTED by my own follow-up instrumentation. Reviewers approving the DESIGN.md quantification should know it is partly false. The claim was: Measured, after instrumenting that exact call: The two functions I named account for ~10 ms of ~51,000 ms. The mechanism was inferred from reading the call path, never measured — the "specification without execution" trap of DESIGN §5, committed while writing about it. What is actually there. Consequences, stated plainly:
The DESIGN.md / Also in flight from operator review: the partition repeated across 2 entries × 2 runs (it previously rested on a single run of a single entry), byte-weighted overlap ( I would not merge this until the correction lands. — sent from smart-moth-595 |
Operator review point 1 (repeat the partition) and my own sub-attribution falsified three claims. They are retracted in the receipt and in the DESIGN authority rather than edited out, because how they failed is the reusable part. RETRACTED 1 -- "load is dominated by referenced_module_paths_in_text, an unmemoized per-(entry,module) content scan." Measured: 3.9-23.0ms, ~0.0% of load. It was inferred from reading the call path and never measured -- the §5 specification-without-execution trap, committed while writing about it. The missed step: load_sources_for_entry_with_pool calls load_sources_for_entry_with_index AND THEN extend_sources_to_both_closure_fixpoint, which the first instrumentation never timed. RETRACTED 2 -- "load is the dominant cost." True at 67-68% on a 159-module closure; FALSE at 38-40% on a 504-module one, where typecheck_compute is ~50%. Run-to-run within an entry is stable (67.0/68.0, 37.9/39.5), so the partition is sound and the generalization was not: it came from one run of one entry. RETRACTED 3 -- the A x B join and the per-source content-hash memo that followed from it. Both depended on claim 1. MEASURED INSTEAD: load is ~100% build_both_closure_edge_index, a CORPUS-wide edge index memoized per MultiEntryIndex at ~25.6s per index, INDEPENDENT of the entry's closure size (159 and 504 module closures pay the same). So it is fixed per index -- not per entry, not per membership. The claim_batch harness pays it twice only because two indices exist on that path (its own build_multi_entry_index plus process_shared_index for machinery). THE BOUND THAT MATTERS: because the dominant row is a fixed per-index construction, every share in section A describes a fixed-cost-dominated harness, NOT the floor, where one index amortizes across hundreds of entries. The verdict is therefore "not answerable from this data" rather than the strengthens-and-relocates claim it previously carried -- a union program justified by these shares would be justified by an artifact of the instrument. The deciding measurement is a partition from the claim_executor discovery path: wired in this PR, and never run. B's membership numbers are unaffected -- they are counts, not timings, and the disjoint-closure pole that would close the program outright is still decisively absent. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
review 45321 asked for symbolic citations in place of line ranges. Verifying the three sites found that one was not merely fragile but wrong: compute_fabric.dag:414-423 — that file is 139 lines. PerformanceReceipt is not in it at all; it lives in gunbc.fleet_intent. The field list was wrong too: `wall_duration` is not a field, the time axis is `cost: CostAccount<Nano>`. Corrected to name the real symbols: gunbc.fleet_intent.PerformanceReceipt, its roll-up fn cost_account_from_performance_receipts, and the std.realization_schedule.CostAccount / CostBasis it feeds — all verified present. The other two (realization_schedule.dag:25-26,33-39 and cli_run.rs:2062) resolved correctly; ranges dropped since the symbols were already named. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
|
review 45321 (REQUEST_CHANGES) — fixed in 41b72a6, with a correction to the premise. Fixed. All three positional citations are gone; the symbols were already named alongside them, so nothing was lost. But verifying the sites before editing turned up something worse than fragility at one of them:
So the review found a real defect, and the symbolic form is what exposed it: a line range cannot be checked against the thing it claims to point at, whereas The premise is not accurate, and I would rather say so than let it stand as a rule. The review cites "DESIGN §3's standing rule to cite symbols rather than unstable positions." §3 has no such rule. Its nearest text is That drift history is the actual argument, and it is stronger than the one the review made: a line number is a claim no reader can verify without opening the file, and mine had already rotted before it was ever read. Made on those grounds, not on a rule that does not exist. — sent from smart-moth-595 |
It was the only one of 31 bin files without a [[bin]] entry. Cargo auto-discovers it (edition 2021, autobins defaults true) so it built and ran, but matching the surrounding convention costs nothing and removes the discrepancy. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
|
review 45328 (cursor, REQUEST_CHANGES) — entry added in 66572a4; the stated reason is incorrect. Done. But the finding's mechanism is wrong, and it matters because the conclusion drawn from it was that the deliverable is unreproducible. The claim is: "With an explicit bin roster, Cargo does not auto-build undeclared I built that binary by name and ran it against three real subjects before this review arrived; the committed receipts in What was actually true is a smaller thing, and it is why I made the change anyway: of the 31 files in — sent from smart-moth-595 |
…refutes it Operator review point 1 asked for >=2 entries x >=2 runs showing the share ordering holds. It does not hold, and the previous table hid that by quoting figures from a run set that was never committed. Real committed receipts, all four: ci_floor_measurement r1 parent 75.2s load 51.24s/68.11% tc 18.48s/24.57% ci_floor_measurement r2 parent 66.4s load 44.96s/67.68% tc 16.57s/24.95% generated_artifact_drift r1 parent 131.0s load 50.98s/38.93% tc 65.56s/50.06% generated_artifact_drift r2 parent 155.7s load 77.11s/49.52% tc 64.55s/41.46% The ordering flips between two runs of the SAME entry (drift r1 typecheck leads, r2 load leads), so the earlier "inverts across entries" reading was an artifact of comparing two runs that happened to agree. What survives is in the absolute columns: typecheck_compute is stable per entry and scales with closure size (18.5/16.6s at 159 modules vs 65.6/64.6s at 504), while load does not track closure size at all (51.24s vs 50.98s) and its magnitude swings 44.96-77.11s across runs. Corpus-fixed and noise-dominated. Confound disclosed: these runs shared the host with concurrent cargo builds. Retraction (b) is itself corrected here rather than silently replaced -- its "false at 38-40% on a 504-module closure" replacement rested on the same unretained run set. Adds cost-partition-generated_artifact_drift-r2.json so every quoted figure has a committed receipt behind it. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Operator review point 3: the overlap figures carried an unstated uniformity assumption -- every membership counted as one regardless of module size. Stated: the B table is module-count weighted. Redone byte-weighted on the same subject, same selection (roster 809 / selected 316 / skipped 493, identical to the committed typical receipt): duplication factor 38.42 by count -> 47.92 by bytes (+24.7%) repeats as share 97.40% -> 97.91% union 1,243 modules -> 11.45 MB of 548.90 MB summed The count-weighted figure was the conservative one: high-fanout modules are systematically larger than average, which is consistent with the universal core being std.algebra / std.types / std.error_primitives rather than small leaves. This moves the weighting in the direction that favours the union program, and the section says explicitly that it does not rescue it -- A.7 is why no membership count here converts into a displaced cost. It is a better-weighted upper bound, not a different kind of claim. Receipt: closure-overlap-typical-byte-weighted.json. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…es its target
A.7 said load's share on a floor run "must be smaller -- by how much is
unmeasured." Measured here on the explicit-entry path, which puts N entries
against ONE shared index with everything else held fixed:
N=1 (2 spans) N=6 (7 spans) growth
parent 69.97s 114.12s 1.63x
load 47.44s 51.32s 1.08x
load_bare_edge_index 47.40s 51.18s 1.08x
typecheck_compute 17.34s 49.64s 2.86x
parse 1.14s 3.66s 3.21x
resolve_modules 0.02s 0.11s 4.40x
load share of parent 67.79% 44.97%
Entry count rises 6x and every per-entry row rises with it; load rises 8%, which
is inside the noise band already established for that row. load is paid once per
INDEX, and the existing per-index memo already amortizes it. The N=1 run
reproduces the discovery-path receipts (67.79% vs 68.11/67.68%), so the
explicit-entry path measures the same thing.
THE REDIRECTION: a union graph cannot displace a cost that is already paid once,
so the program's apparent target -- the row that dominated every single-entry
partition at 67-68% -- is eliminated, not merely unproven. The only measured row
scaling with both entry count and closure size is typecheck_compute, whose unit of
work is module membership. That is the only surviving candidate and it is NOT
established: converting repeated membership into repeated computation needs
per-entry typecheck attribution against a shared env, which nobody has measured.
The duplication factor must not be quoted as a multiplier on typecheck time.
Projection to floor-scale N is marked as a projection, not a receipt (two points,
six small entries). Whole-corpus floor runs OOM-killed twice (exit 137, at 1,513
and 1,046 entries) including under GUNBC_MEMORY_BUDGET_BYTES=44GiB, which governs
realization admission rather than resolve-pool retention.
Also completes the byte weighting across all three subjects (43.04 / 47.92 /
49.25 against 35.89 / 38.42 / 38.27 by count) and corrects B.1 read 1: "stable
across breadth" holds by module count but not by bytes, where the factor rises
monotonically.
Receipts: cost-partition-amortization-n{1,6}.json,
closure-overlap-{narrow,broad}-byte-weighted.json.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
|
All four operator review points are addressed, and the fourth measurement changed the verdict. Point 1 — repeat A on ≥2 entries × ≥2 runs. Done, and the share ordering does not hold. It flips between two runs of the same entry ( Point 2 — the ratio inside
Point 3 — the weighting. Stated (it was module-count) and redone byte-weighted across all three subjects: 43.04 / 47.92 / 49.25 against 35.89 / 38.42 / 38.27. Count-weighted was the conservative one — high-fanout modules are systematically larger. It also changes a reading, not just a magnitude: by count the factor plateaus and dips at the broad subject, by bytes it rises monotonically. B.1 read 1 is corrected in place. Note this moves the weighting in the direction that favours the union program, which is worth saying plainly given the verdict cuts the other way. Point 4 — stale PR body. Rewritten; every figure now traces to a file in What I could not get. The whole-corpus floor run OOM-killed twice (exit 137, at 1,513 and 1,046 entries), including under — sent from smart-moth-595 |
… of a count rewire_sub_rows_are_inclusive_and_never_enter_the_exclusive_sum asserted p.inclusive.len() == 3 -- a count over EVERY inclusive row, not just the rewire ones. Adding the load_* sub-attribution earlier in this PR took that to 10 and turned the control red. It went unnoticed because the rust suite was removed from CI on 2026-07-11 and runs locally only. Two changes: - Filter to contained_in == "assembly_rewire" and assert those three rows account for all 300ns of the parent. A global count makes this control fail whenever an unrelated row gains a sub-row, which is exactly what happened. - Add the invariant the count was standing in for: every inclusive row names a parent that is itself an exclusive or inclusive row, so it is already counted and can never be attributed to nothing. Proven to discriminate by mutation -- repointing load_bare_edge_index at a nonexistent parent goes red with the located diagnostic, and only that test. Also corrects InclusiveCostRow.contained_in's doc comment, which claimed the parent is always an exclusive row. It is not: load_bare_edge_index nests under load_bare_reference_closure, which nests under load. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Bootstrapping the seed required a compiler that could emit the merged .dag, so I ran `git checkout origin/main -- src/v1/stage0/src/`. origin/main had advanced past this branch's merge base (da37e37) to b519142, so that path-scoped checkout imported the stage0 slice of #7483 ("Exclusive cost partition + selected-set closure overlap") — its hand-maintained bins — while leaving the rest of that PR behind. The result was four files in this diff that are not this PR's work: measure_selected_closure_overlap.rs (a new file, and orphaned — Cargo.toml at this branch's base does not declare the bin, so nothing built it), plus edits to claim_batch.rs, claim_executor.rs and measure_whole_tree_resolve.rs. Half of someone else's merged change, presented as mine, is not something to carry to review: it misattributes the work and it is a partial import whose .dag half is absent. All four are restored to the merge base; main's own versions land normally when this branch merges. Caught by reading the diff surface after a reviewer's summary described "two new measurement bins" I had not written — a reminder that a path-scoped checkout against a moving ref imports whatever else has landed there. Verified after the strip: cargo build clean, regen_stage0 --verify regen_divergence_count=0. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…-fold Finding 1 (census inconsistency) — REAL, and wider than reported. The merge-repair row's prose still read "+7 lines" after the scalar, the file list and the total were corrected to 4. Fixed. Auditing every numeric claim in the carrier then found a second stale pair the review had not reached: the cli_run row carried an absolute before/after LOC pair, and #7483 grew that file by ~1,556 lines, so both halves were false while the delta stayed exactly right. The row's own stated method already says a delta is the correct measure for a 32k-line host module, so the absolutes were a second representation of a fact it already owned — deleted rather than re-pinned, since re-pinning only resets the clock on the same rot. Every number in the carrier now ties: 104 = 348-244, 83, 14, 4, total 205. New witnesses close the class rather than just the instance. The total already had a sum-and-prose tie, which is why the total stayed correct; the per-row prose had none. merge_repair_growth_is_censused now pins the scalar at 4 AND requires "+4 lines" in its note, and cli_run_carries_no_stale_absolutes refuses the deleted absolute. That second witness caught its own bug on first run: the explanation I wrote quoted the stale number, so the note still carried it. Now described rather than quoted — a dead number reprinted in prose is still a number this carrier appears to assert. Finding 2 (substrate any-fold) — REAL, and the delete arm is the right one. occurrence_containment_path_contains_ancestor had ZERO consumers corpus-wide (dag, src/v2, src/v1): its declaration, its own note, its own emission. The review 45014/45081 correction is what orphaned it — once prefix stopped consulting ancestor-membership alone it had no callers — so deleting it completes that fix instead of leaving a dead second surface. Not routed through a canonical any, deliberately: any exists ONLY in src/v2/std/algebra.dag (v2.std.algebra, the compiler's private copy of std). dag/std/algebra.dag, the authority, has none. Importing it would point the authority at a copy of itself — a §3 inversion. With zero consumers there is no surface to preserve, so deletion is both smaller and correct. regen_stage0 --verify: regen_divergence_count=0. 9/9 census witnesses, 11/11 binding witnesses green.
* Typecheck perf: sink the where-refinement peel, wire the once-per-closure variant base, share the process index (#7490)
* Sink where-refinement peel to the refusal path (#7438 cost-shape fix)
where_refinement_mismatch_diags runs on every infer_expr with an expected
type; peel_nominal_alias_identity (an unmemoized resolve_node_bounded
rebuild) was computed eagerly and discarded on the 97% of calls that find
zero predicates — 6.5s of 6.7s measured on the host_effect_realize entry
compile (79,168 calls, 76,773 zero-predicate). formal_checked is consumed
only by where_refinement_diags_for_predicate, so it now computes inside
the uncovered-predicates else, the only branch that reads it.
Behavior-identical by receipt: host_effect_realize compile diagnostics
byte-identical pre/post (915 advisory, 0 blocking); direct RED probe
(0 at PositiveInt return) still hard-refuses; all 16
where_refinement_enforcement_witness rows PASS including every refusal
control. Rationale carried in-tree as where_refinement_peel_cost_note
(the corpus has no comment syntax; data-note is the idiom).
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01UaAWvG3LgBAM9tGF1D2bG1
* Wire the once-per-closure variant base #7398 authored but never called
merge_global_bare_variant_locals rescanned the whole global_bare census
and re-inserted every eligible variant-owner pair into every module's
locals map: 464 modules x 12,554 census keys = 5.8M iterations and
1,286,399 persistent-map inserts = 31.4s (14%) of the host_effect_realize
entry compile. The eligible pairs depend only on (global_bare, si) — a
whole-closure fact — and #7398 landed build_global_bare_variant_locals
computing exactly that base map, with zero callers.
This wires it: typecheck_with_census_extra computes the base once per
closure and threads it down realize_module -> typecheck_module ->
build_module_context; the merge becomes map_merge(base, state.locals) —
overlay wins, exactly the old skip-if-present arm, and the old
checked-insert collision arm was unreachable (presence checked before
insert), so the global merge contributes zero collision errors then and
now. The cli_run resolve leg (the floor/claim path) computes the base
beside each composed per-root index in tree_symbol_index_memo, keyed to
the index it belongs to. Cost per module drops from O(|census|) inserts
to O(|module locals|).
Measured on the same entry: merge inserts 1,286,399 -> 7,263 (177x),
merge self 31.4s -> 0.08s, build_module_context 34.6s -> 2.6s,
compile.reconcile 72-76s -> 44s. Behavior receipts: compile diagnostics
byte-identical (915 advisory, 0 blocking); witness suites green by
execution — where_refinement 16/16, e0599_probe_census 18/18,
namespace_import_closure (wet) PASS.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01UaAWvG3LgBAM9tGF1D2bG1
* Route the strict entry-closure loader through the process-shared index
A `gunbc compile --entry` process built its closure index in
load_sources_for_entry_with_pool_index, dropped it, and then the first
compile-clean diagnostic classification rebuilt the same index from
scratch inside resolve_entry_graph_shared — to evaluate the one
compile_clean_diagnostic_policy Bool. Measured on the
host_effect_realize entry compile: 2 index builds, pool_parse over
5,450 files for a 2,725-module pool, 4 tree censuses (2 per root) —
the whole corpus full-parsed twice per process.
Strict pool policy now routes through process_shared_index (the same
construction fn and canonical roots key), so the policy read is a cache
hit; primary-precedence keeps its own fresh build since the shared index
only builds strict. Measured after: index_builds=1, pool_parse
files=2,725, tree_census calls=2, loader fixpoint 60.0s -> 27.3s, whole
compile 3m01s -> 2m13s on the same box. Diagnostics byte-identical
(915 advisory, 0 blocking).
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01UaAWvG3LgBAM9tGF1D2bG1
---------
Co-authored-by: Claude <noreply@anthropic.com>
* Design note: seamless deploys — ground the four items, re-cut two of them (#7477)
* WIP: server deploy untangling
* Design note: seamless deploys — ground the four items, re-cut two of them
Modeling-first draft for the seamless-deploys brief. No behavior changes; the
only code is the typed doc-graph binding the note needs to be reachable.
Grounded every claim against the tree. Three items confirm line-exact; two
side claims correct:
- The restart count resolves opposite to the brief's caveat. 40
deploy_dashboard_srv1 jobs ran in the 24h window ending 2026-07-30T20:11Z
(38 success, 2 failure), every one running the unconditional restart arm —
so deploys alone exceed the 24 observed restarts and need no manual
restarts to explain them. Bounded honestly: no srv1 access from this
session, so what is measured is restart commands issued.
- "208 sources" matches neither figure the tree records (a 91-source closure,
2,356 files read). Corpus is now 2,719 files, up ~15% in nine days, so the
40s startup expectation is already drifting.
Two items re-cut along model seams rather than as stated:
- Item 2 is a §3 de-fork, not a standalone outage fix. Readiness is modeled
twice — systemd's Type=simple (ready at spawn, wrong by ~35-40s, every
time) and live_deploy's healthz poll (correct). The second exists because
the first lies. The deploy already routes around it, so its independent
cost today is small; its value is that it is the prerequisite for any
handover.
- Item 3's fix is construction, not validation. The apply pole passes
observed: [] (emit.dag:158), so both poles are degenerate and
Unchanged-to-noop is structurally unreachable — the deploy cannot diff. The
fix is supplying the observed set, not adding a changed-predicate to the
restart step. Notes that this makes the spine's ownership refusal arms live
on a path that today always applies, and that "could not observe" must
refuse rather than widen to restart-everything.
Also flags that socket activation makes item 1's new sentence unreachable in
the case it was written for, and that the transport arm must not assert
"deploying" — a cause it cannot establish.
Doc-graph binding uses the typed HandAuthoredDocBind row; the prose "bind:"
scan is deleted. RED control observed: the orphan wall went true -> false ->
true across adding the doc unbound and then binding it.
* Restore the trailing blank line in service_ready.dag
Unrelated churn from removing the staging prose row — the file's trailing
blank line is now byte-identical to main.
* WIP: server deploy untangling
* Correct two re-cuts that prescribed models they could not establish (review 45229)
codex/codex-default requested changes on two central claims. Both verified
against the tree and both correct; fixed in place with the correction
recorded rather than silently restated.
Item 3 — the observed-set claim was wrong, and dangerously so. The draft said
supplying `observed` needs "no new comparison logic, no new authority."
spec.dag:38-41 declares DeploymentArtifactStep { kind, path } with no content
identity, and deployment_step_value_eq is `a == b` over exactly that. Supplying
observed rows at the same paths therefore returns Unchanged for every member
always — not "cannot distinguish changed from unchanged" but an inversion into
a silent never-deploy, strictly worse than today's always-restart. It is also
the shape DESIGN §5 names: satisfiable by editing the declaration while the
realization lies. Split into 2a (model the comparable artifact value at its
single authority) then 2b (supply the provider), with the ordering load-bearing.
Item 2 — the de-fork framing was wrong; the draft committed the same
state-space conflation it accused systemd of. There are two facts, not two
representations of one: F1 process-bind readiness (systemd asserts it via
Type=simple and is false by ~35-40s; sd_notify genuinely fixes this) and F2
deployment surface identity (only the digest establishes it; systemd can never
know it). readiness.dag's service_ready_means_serving_this_tree_note records
why, with a dated receipt: gunbc serve binds its graph once at start, so the
pre-restart process keeps answering during the replacement's load, and on
2026-07-24 srv1 served a stale surface with every check green. sd_notify fires
exactly when F2 is still unproven, so on that axis it is weaker than what
exists today. The digest check must survive slice 3 — now a red control, not a
caution.
Downstream sections updated to match: sequencing (2a before 2b; slice 3 does
not touch the digest), red controls (a binary-content-only change must still
restart — the control that discriminates the 2a defect; and the 2026-07-24
shape must still refuse after notify lands), and the sign-off questions (item 3
is gated on a load-bearing carrier change, not the cheap slice first implied).
Verified: doc_graph_roots.dag compiles 0 blocking errors; orphan, dangling-link,
and slug-collision witnesses green.
* Derive the restart from the service's inputs, not from the unit file (review 45232)
Third defect found in item 3, and the deepest: content identity alone still
does not restart the service.
Reconciliation is per member, and the only restart of gunbc-roadmap.service is
emit.dag:288 inside the SystemdUnit upsert arm (emit.dag:219 restarts
gunbc-tree-sync.service, a different unit). So under a real diff a binary-only
change installs the new binary, leaves the unit file untouched, and
SystemdUnit reports Unchanged -> noop: new binary on disk, old process still
serving it. The discriminating control added after review 45229 would have
FAILED against the design as written — the re-cut omitted the dependency that
makes its own control pass.
Root cause is a conflation the degenerate pole has been hiding. SystemdUnit
names two things: the unit FILE (an artifact, valued by its text) and the
RUNNING SERVICE (a process, whose correctness depends on the binary and tree it
started from). emit_deploy_member_effect_note fuses the restart onto the file
— harmless while every member always applies, the defect the moment the diff is
real. The dependency itself is already known and already single-authority, but
only in prose: deployment_apply_order_note says "all before the unit (ExecStart
references binary + tree)".
Construction answer: model the running service as its own member whose value
derives from the identities it was started from, so a binary change makes the
service Modified and it restarts by construction — no impact table, no
restart_required_by adjacency (which would re-represent the dependency the
apply order already asserts). New binary installed with the old process serving
becomes unwritable rather than checked for.
Item 3 is now three steps: 2a comparable value -> 2b de-fuse the service from
the unit file -> 2c observed provider. Every partial order typechecks and
silently under-deploys (2c without 2a never deploys; 2c without 2b deploys the
files but not the service), so the binary-only control is stated as item 3's
acceptance bar rather than a nicety — checking only that the binary reached
disk is what makes both failures look green.
§7 q3 sharpened: item 3 is the one item NOT required for the headline outcome
(slices 1, 3, 4 make deploys invisible; item 3 only makes them rarer), so if
the two carrier changes are out of scope it should be dropped entirely rather
than attempted partially.
Verified: doc_graph_roots.dag compiles 0 blocking errors; orphan and
dangling-link witnesses green.
* State item 4's dependency once, authoritatively: it needs B, not C (review 45241)
Internal contradiction, correctly caught. One section headed "Item 4 is
downstream of B and C" and treated the two jointly, while §2 Concept B named
only item 2 as the handover prerequisite and §7 q3 said item 3 is not required
for the headline outcome at all. Read as a plan, that would have gated the
cheap handover work on the most expensive item in the ticket.
The truth, now stated in one place:
- B IS a prerequisite. Handover means move traffic when the replacement is
ready, and there is no trustworthy "the replacement has bound" signal without
it.
- C is NOT. It changes how often a handover runs, never whether it works. A
handover built with C outstanding is correct — it just runs on all ~40
deploys/day instead of the subset that changed something. Nothing in item 4's
design reads a reconciliation fact.
§5 restructured around the dependency graph rather than a numbered list that
implied an order:
slice 1 — no dependencies
slice 3 -> slice 4 — the ONLY hard edge in this ticket
slice 2a -> 2b -> 2c — internally ordered, independent of 1, 3, 4
with the recommended order now headline-first, cost-last (1, 3, 4, then 2),
since slice 2 is both the most expensive item and the only one that does not
serve the headline. Slice labels are named as labels, not sequence.
Audited every remaining "prerequisite"/"downstream"/"gated" statement in the
note for consistency with this; item 3's internal 2a->2b->2c gating is the only
other one and it is correct.
Verified: orphan and dangling-link witnesses green. Doc-only change.
* WIP: server deploy untangling
* Deploy reconciles to intent with minimal items (operator direction 2026-07-30)
Operator: "i'd like deploy to use our existing apply/delete/reconcile type
process (i.e. bmc/srvN apply) — i want to deploy the minimal possible items to
update to intent."
This answers §7 q3 and re-prioritises the ticket. Item 3 was written as an
optional scope reducer to be dropped if expensive; it is the deployment ask.
"Minimal possible items to update to intent" IS the spine's Unchanged -> noop,
and the vocabulary maps one-to-one: apply = MemberUpsert, delete =
MemberTeardown (owned-only, else typed refusal), reconcile = the diff, with
unchanged members producing no hunk and no effect.
Grounded against the siblings, which changes the cost estimate materially —
this is instantiation, not invention. live_deploy is the ONLY degenerate
consumer of a spine others already drive non-degenerately:
- 2a comparable value — precedent gunbc.host_authorized_keys_reconcile:
value_eq compares content (algorithm + material + comment) while key_of
returns identity (key material), so content drift is Modified -> re-upsert,
never Remove + Add. That identity/value split is exactly what
DeploymentArtifactStep lacks.
- 2c observation — precedent gunbc.tool_readiness, live today: reconciles
desired Pin<CliTool> against an observed one from
extdeps.realization.emit_on_demand_host.observed_tool_identity, with three
typed outcomes (Found/Missing/Duplicate). Its observed_pin_projection_note
solves deploy's projection problem too — build the observed member from
desired, replacing only the observed field.
- The apply site is gunbc.host_effect_realize (:990, :1076), already running
reconciles inside srvN apply — the process named in the direction.
So 2a and 2c are patterned work. 2b — de-fusing the running service from the
unit file — remains the only part with NO precedent (no sibling has an artifact
whose realization is a running process), and is where design attention belongs.
Two decisions surfaced, both deliberately left to a human by the sibling
modules: (1) observed scope and delete semantics — deploy's members are a
closed set of owned artifacts at known paths, unlike authorized_keys'
everything-on-host scope, so wholesale-refuse is defensible, but Removed ->
teardown becomes reachable on the apply path for the first time; (2) Missing
means Added -> upsert, while an observation that could not be TAKEN must refuse
typed/located/counted, never degrade to reinstall-everything — the absorbing
fallback wearing this ticket's own clothes.
§5 recommended order revised: slice 2 is no longer the item to cut under
pressure. It still gates nothing (graph unchanged), and can run in parallel
with 3/4 since they share no seam.
Verified: orphan and dangling-link witnesses green. Doc-only change.
* Correct an over-pessimistic claim: 2b composes two existing patterns
Verified rather than left asserted, because the claim drives the cost estimate
the operator is budgeting against.
The note said no sibling has an artifact whose realization is a running
process, so de-fusing the service from the unit file had no precedent. That is
wrong. gunbc.roadmap_belt reconciles LIVE DISPATCH SESSIONS — running processes
— with a genuine observed provider (belt_observed_members(live:
List<DispatchLiveSession>)), ownership lifted from an actuator observation, and
R5 teardown meaning reap a live session, refusing when it cannot prove
ownership. Process-as-member, live observation of processes, and owned-only
teardown of a running thing are all precedented.
The genuinely new cell is narrower, and naming it precisely is what makes 2b
tractable — it is one cell of a 2x2:
inert artifact running process
presence-only — roadmap_belt
content-sensitive authorized_keys, tool_readiness deploy (empty)
The belt's member value is deliberately degenerate: dispatch_member_value_eq
returns constant true, so it never produces a Modified hunk. A session exists
(Unchanged), is missing (Added -> spawn), or is extra (Removed -> reap). It has
no notion of "this running thing is stale relative to the inputs it was started
from" — which is exactly deploy's requirement, and exactly the axis on which
today's always-restart is hiding.
So 2b composes belt's process-member machinery with the siblings'
content-sensitive value. Materially smaller and lower-risk than "no precedent"
implied. The remaining design question is one thing: what are the running
service's inputs, such that its value changes exactly when a restart is
genuinely required — answered by 2a's identities.
Verified: orphan and dangling-link witnesses green. Doc-only change.
* Measure the serve closure: 208 is correct, the tree's figure is the stale one
Settled §7 q5 by running the unit's exact ExecStart on a spare port rather than
leaving it as a question for the operator.
[t+56s] resolved 208 sources
[t+59s] compile.frontend done in 3 seconds
[t+59s] compile.normalize done in 298ms
[t+74s] compile.reconcile done in 14 seconds
[t+74s] compile.analyses done in 213ms
[t+74s] gunbc serve listening -> roadmap_serve_handle()
The brief's "208 sources" is the real resolved-closure count. This note's
earlier objection to it was WRONG, and it is the tree that is stale:
live_deploy_service_ready_poll_bound_reason's "a closure of 91" does not match
what the entry actually resolves. Corrected in §1 and q5 marked resolved.
The phase split is the more valuable half and confirms the load-dominant
diagnosis by execution: 56s of 74s (76%) elapses BEFORE "resolved 208 sources"
prints — the load phase — with the whole compile accounting for 18s, of which
reconcile is 14s. That is the deep fix's premise measured rather than cited.
Honest caveat recorded in the note: 74s is this build box under concurrent
load, NOT srv1, and must not be read as a regression against srv1's recorded
35/36/36/39s. Machine-independent are the source count (exact) and the
load-vs-compile ratio. It does suggest expected_startup = 40s wants
re-measurement on srv1 given ~15% corpus growth since it was calibrated.
Also fixed: a missing blank line that broke the operator-direction block out of
its list, and the §1 intro sentence which no longer described the two side
claims below it.
Verified: orphan and dangling-link witnesses green; no stray serve process, port
18080 free. Doc-only change.
* Retire two stale cross-references my own corrections created (review 45260)
Both findings verified and both real. Same root cause: I corrected §2 across
successive reviews and left downstream sections pointing at the superseded text,
so the operator-facing summary disagreed with the analysis it summarised.
1. §7 q3 still called 2b "the only part with no precedent" — superseded by the
roadmap_belt finding, which showed 2b composes belt's process-member
machinery with the siblings' content-sensitive value_eq. q3 now states all
three sub-slices have precedent and names roadmap_belt alongside
host_authorized_keys_reconcile and tool_readiness. The reviewer's concern is
the operative one: a reader jumping to §7 for the operator answer would have
planned virgin territory the note already refutes.
2. The review-45241 correction block cited "item 3 is not required for the
headline outcome (§7 q3)" as a live claim, but q3 was answered — item 3 is in
scope and not droppable. Rewritten to rest only on §2 Concept B, with an
explicit scope note separating the two axes that were being conflated:
PRIORITY (in scope, not droppable) versus DEPENDENCY (item 4 does not depend
on item 3). Both are true; only the dependency claim belongs in that section.
Swept the whole class rather than fixing only the two reported, since this is
the second stale-cross-reference finding. That surfaced a third, unreported
issue: "scope reducer" was being used to both reject a framing (§2: item 3 is
"not an optional scope reducer to be dropped") and assert one (§2/§5: "C is an
independent scope reducer"), which reads as self-contradiction. Disambiguated —
priority language at the first site, and the second now says C is a scope
reducer in FUNCTION while stating that this says nothing about its priority.
Verified: orphan and dangling-link witnesses green. Doc-only change.
* WIP: server deploy untangling
* Reconcile the boundary and sequencing with the operator decision (review 45264)
Both findings real, both the same class that has now produced most of this PR's
review traffic: correcting §2 and leaving downstream text describing the
superseded state.
1. §5 listed item 3 "whenever it is worth its cost" — discretionary language
directly contradicting the operator direction that it is in scope and not
droppable. As an executable plan that turns a mandatory requirement into
optional work, which is the reviewer's operative point. Now: "Required, not
discretionary. Listed last because it gates nothing and can run in parallel
with 1/3/4 — NOT because it is optional."
2. The opening boundary still carried the brief's original "not what the deploy
installs", which predates the reconcile-to-intent direction and reads as
excluding item 3. Amended with the distinction the two halves need, since
item 3 sits across the seam:
- still OUT: the desired set — which artifacts constitute the deployment
and what is inside them. This ticket adds no member and changes no
artifact's contents.
- now IN: how that set is applied — whether an unchanged member is
re-applied, and the member modeling that makes "unchanged" decidable
(content identity; the running service as a member distinct from the
unit file).
So the ticket does not change WHAT the deploy installs, it changes HOW MUCH
OF IT IS RE-APPLIED to reach intent. The rest of the brief's out_of_scope
stands verbatim.
Swept the class again rather than fixing only the two reported. Remaining
"optional"/"worth its cost" hedges: none. Also refreshed the Provenance block,
which was itself stale in the same way — it cited only the original base commit
and omitted every receipt added since (the six reconcile precedents, the
readiness F1/F2 carrier, spec.dag's DeploymentArtifactStep, and both
measurements).
Separately, on my own judgement rather than a finding: shortened this note's
HandAuthoredDocBind dissolution trigger from 201 words to 63. Sibling triggers
run 5-58 words (median ~15), and the excess was restating the note's analysis
inside the row — duplicating content that has a single authority and must then
be maintained in lockstep. It had already needed updating twice in six
revisions. The trigger now states the checkable condition and points at the note
for reasoning.
Verified: doc_graph_roots.dag compiles 0 blocking errors; orphan, dangling-link,
and slug-collision witnesses green.
* Cite by symbol, not position — 5 of 7 receipts had already rotted (review 45281)
The reviewer's stated rule does not exist, but its concern was empirically
correct and worse than reported, so the fix is made on the evidence rather than
on the claimed rule.
ON THE CLAIMED RULE: review 45281 cites a "locked 'cite the symbol, not the
position' rule" in DESIGN §3. No such rule is in DESIGN.md — grep for both
phrases returns zero. What §3 actually says about paths is "a fact's home is its
LAYER, not its file (paths are discriminators, not gospel)", which is about
where facts live, not citation format. DESIGN.md itself carries 5 positional
file:line citations (algebra.dag:38, v1_interpreter.rs:8672,
v1_compiler_emit_rust.rs:746, ctrl_session_witness.dag:93/97/101). So the rule
as stated is not the authority's.
ON THE UNDERLYING CONCERN: verified against the tree, and it is decisive. FIVE
OF THIS NOTE'S SEVEN positional receipts had already drifted onto the wrong
declaration, within a day of being written:
emit.dag:123 Type=simple -> a Description= line
emit.dag:158 observed: [] -> deployment_step_ownership_opt
emit.dag:288 roadmap restart -> tree_sync_restart_step_with_diagnosis
spec.dag:38 DeploymentArtifactStep -> a TailscaleServeMapping coproduct arm
cli_run.rs:11918 TcpListener::bind -> a println!
Every underlying claim still holds — only the positions moved as main advanced
and was merged. But a document whose entire value is traceable evidence cannot
carry receipts with that half-life.
Converted every receipt to module + declaration:
workflow_fetch_request_statements, emit_systemd_unit_doc, deployment_apply_plan,
emit_artifact_upsert, tree_sync_restart_step_with_diagnosis,
DeploymentArtifactStep, handle_serve, the v1-materialization-kernel node row,
srv3_realize_os_install_actuator_toolchain_ensure_body,
realize_provision_build_cache_body. Verified each symbol exists and still
carries its claim. Zero positional citations remain outside the new citation
note, where the rotted five are quoted AS the evidence for the convention.
Also dropped the now-false "line-exact" qualifier on item 1's verdict.
Verified: orphan and dangling-link witnesses green. Doc-only change.
* WIP: server deploy untangling
* State one authoritative scope: the ticket does change deployed content (review 45289)
Finding verified and real, and the defect is broader than the instance reported.
The boundary amendment claimed the ticket "adds no member and changes no
artifact's contents." That is false for nearly every item in it — an
over-tightening I introduced while fixing the PREVIOUS boundary finding:
- item 1 edits roadmap_component.dag, which emits the dashboard JS — a change to
the served tree, and the brief explicitly puts "how the browser is told what it
is seeing" IN scope;
- item 2 changes the unit file's own text (Type=notify) and the seed binary
(sd_notify), both deployment artifacts;
- item 4 may ADD a .socket unit — a new deployment MEMBER, not merely new
contents.
The reviewer reached this through the staleness cue, which is the mildest
instance; the socket unit is the one that actually adds a member.
Resolved by amending the boundary rather than dropping the cue, because the cue
is in scope by the brief's own words ("how the browser is told what it is
seeing") and exists to stop socket activation from silently showing stale data.
The honest boundary is not "no artifact changes" — it is that the ticket does not
change WHAT THE DEPLOY IS FOR: the dashboard's product behavior, what it shows
beyond the honesty fixes the brief asks for, and which artifacts constitute the
deployment as a product decision, plus the brief's own dispatch/belt exclusions.
Also recorded a coordination consequence nothing else in the note captured: if
slice 4 adds a .socket member AND slice 2 has made membership non-degenerate,
that member needs the same bundle as its siblings (identity, content-sensitive
value, ownership stance). Neither gates the other, so the §5 dependency graph is
unchanged — but whichever lands second inherits the join, and it should not be
discovered then.
Verified: orphan and dangling-link witnesses green. Doc-only change.
* Socket activation does not meet the handback: in-flight fetches die (review 45291)
The best finding on this PR — a substantive design defect, not bookkeeping, and
correct.
The backlog holds only connections that have NOT yet been accepted. A fetch the
old process already accepted dies with the process: client sees a reset, the
browser's fetch rejects, and it lands in exactly the .catch arm this ticket
exists to quiet. Verified in the seed rather than reasoned about:
- handle_serve installs NO SIGTERM handler (grep SIGTERM in cli_run.rs: nothing);
- the only SIGTERM machinery lives in phase_profile, is gated on profiling being
enabled, and even then calls std::process::exit(143) after flushing — it does
not drain;
- so systemctl restart -> default SIGTERM disposition -> immediate termination
mid-request.
Exposure is small per deploy (roughly request-duration / 2s poll of viewers are
mid-flight at the restart instant) but nonzero, and across ~40 deploys/day it
will fire. The brief's handback is "a deploy run against a live viewer with no
visible interruption", so a rare banner still fails it: socket activation ALONE
does not meet the acceptance bar.
Three consequences recorded:
1. §3 states the limitation and names the fix — a SIGTERM drain: stop accepting,
finish in-flight, exit within TimeoutStopSec so a hung request cannot stall
the deploy.
2. §6's handback control now says explicitly that it is NOT established by socket
activation, is a control on slice 4 AS A WHOLE, and must be narrowed to "no
banner for connections initiated after the restart began" if the drain is out
of scope — a weaker promise than the brief asked for, flagged as such rather
than quietly delivered.
3. §7 q4 widened: the seed seam is THREE things, not one — LISTEN_FDS (inherit
the listener), sd_notify (honest F1 readiness), and the SIGTERM drain
(graceful handover). Answering no forecloses all three, so slices 3 AND 4 both
lose their route, not just socket activation. Slice 4 in §5 updated to carry
the drain as required rather than polish.
Verified: orphan and dangling-link witnesses green. Doc-only change.
* WIP: server deploy untangling
---------
Co-authored-by: Brian Searls <briansearls1@gmail.com>
* Exclusive cost partition + selected-set closure overlap (Lane B slice 1, measurement only) (#7483)
* WIP: Lane B
* Exclusive cost partition + selected-set closure overlap (measurement only)
Lane B slice 1, subject entry-graph-union-construction. No union
implementation, no eviction/retention change, no walk_memo or #6999 memo
fork.
A. The resolve-split counters could not be quoted as shares because the
children and the parent are drawn from DIFFERENT UNIVERSES, not because
they nest. ResolveStageNanos accumulates over every resolve the thread
runs -- witness entries and machinery entries alike -- while the receipts
printing it quote a parent covering only one of those sets. Executed
receipt: a single-entry claim_batch reports load=48468ms against a
45308ms parent, and the span account shows why -- two top-level resolves
ran (the witness entry plus dag/gunbc/output_policy.dag), so the rows
summed 65.3s of spans against a 41.0s denominator.
ResolveSpanAccount adds the one window that contains every stage row by
construction, and exclusive_cost_partition reports against it. The law
parent == sum_exclusive + remainder holds by construction (remainder is
derived, tolerance 0ns); what makes it non-vacuous is that it refuses --
OverAttributed, NestedSpanAttribution, NoSpans -- instead of clamping,
which is the shape the existing saturating_sub `other=` row uses to hide
exactly this condition. share_of_parent returns None unless Reconciled.
Basis is named and additive: summed top-level resolve span nanos,
thread-sequential. Elapsed wall is not additive over concurrent worker
spans, so it is carried under `observations` and never partitioned.
assembly_rewire's three sub-passes are carried as explicit inclusive rows
and never enter the exclusive sum.
B. measure_selected_closure_overlap composes the production machinery --
discover_floor_witness_roster, the floor_diff_observe unified and
name-status observations, entry_eligible_for_discovery_skip_before_resolve,
and collect_both_closure_module_names_for_entry -- so the measurement
reads the floor's own selection rather than a parallel hand-written
model. It resolves and typechecks nothing: the output is an upper bound
on repeated module membership, not a wall-time saving. A selector or
diff-observation refusal propagates rather than widening to
measure-everything.
Both probes carry the same dissolution trigger as ResolveStageNanos: a
.dag PerformanceReceipt carrier consumed by a floor witness.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
* Discriminating controls for the accounting law and the overlap arithmetic
Ten controls, green by execution, plus a mutation proving they refuse.
The law holds by construction, so the tests that carry weight are the ones
that make it fail. Disabling the OverAttributed arm (the saturating_sub
shape that hid this condition in the first place) turns exactly
refuses_over_attribution_instead_of_clamping_to_zero and
json_marks_a_refused_partition_unquotable RED and leaves the other four
green -- so the controls discriminate rather than merely pass.
Each refusal arm has an input reaching it (OverAttributed,
NestedSpanAttribution, NoSpans), and every refused state asserts
share_of_parent == None: a share quoted off a non-partition is the
fabricated plausible output DESIGN §5 forbids. The rewire sub-rows get a
double-count control fixing them as inclusive.
The overlap arithmetic pins both degenerate poles, including the one that
would CLOSE the union program (fully disjoint closures -> factor 1.0,
upper bound 0) and the empty selection that must report null rather than
let 0/0 become 1.0. Executing them caught a real arithmetic error in the
percentile control's own expected values (3+2+1+2 = 8, not 7) -- the
implementation was right and the test was wrong, which is the direction
that only execution can tell apart.
measure_whole_tree_resolve now emits the partition too. It runs the
monolithic compile_to_resolved path, which fills no stage row and opens
no resolve span, so it refuses with NoSpans -- making "this probe carries
no stage attribution" an executed receipt rather than a prose claim.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
* WIP: Lane B
* Give both probes a §7 HAND-RUST scaffold receipt (codex review 45272)
REQUEST_CHANGES was correct: this file has an established
SCAFFOLD (§7 HAND-RUST — <marker>) convention -- ROADMAP lane, Unblock,
an explicit DELETE WHEN list, a greppable receipt, and a declaration test
-- and a generic "a .dag PerformanceReceipt carrier" trigger is not that.
Both scaffolds now carry the full block.
A (cli_run_exclusive_cost_partition_probe) names the concrete lane the
ResolveStageNanos rows it partitions already declare: ROADMAP §2 Minimal
work — caching by realization / realization-measurement-loop.md Phase 0,
dissolving when compute_fabric.PerformanceReceipt keyed by cache-subject
hash rolls into CostAccount.time = Measured and a floor witness consumes
it. It adds no second measurement authority; it makes the existing rows'
denominator honest.
B (cli_run_selected_closure_overlap_probe) is typed as a ONE-SHOT
INSTRUMENT with an explicit deferral: delete when the slice-2 union
verdict is taken, WHICHEVER WAY IT GOES -- if the program proceeds its
own receipts supersede this, and if it is shrunk or closed the probe has
discharged its purpose. A standing closure-overlap reader belongs in
v2.lens.affected_set over the containment tree, not in seed Rust, so this
deliberately does not become permanent host-side machinery by default.
The receipt lines report their real hit count instead of inheriting the
convention's error: both older markers in this file claim `== 1` and
actually sit at 5 and 4 hits, so a copied claim would have been false on
arrival. What the receipt checks is that the marker reaches 0 at
deletion, not a fixed count.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
* Measure over the floor's corpus, not the probe's narrower one
The probe defaulted its exclusions to whole_tree_probe_exclusion_substrings,
which is the floor's witness_exclusion_substrings UNION the whole-tree
strict-resolve exclusions. That is the right list for a whole-tree RSS
probe and the wrong one here: it made the roster 45 entries against 579
*_test.dag files under the same scan dirs, so the overlap statistics were
being drawn from roughly 8% of the corpus the floor actually selects over.
A subject drawn from 8% of the corpus cannot answer a question about the
corpus, and the failure is invisible in the output -- every derived
quantity is internally consistent and simply describes a different, much
smaller population. Defaulting to gunbc.ci_layer_roots.witness_exclusion_substrings
(the floor discovery authority, the same list run_discovery_corpus passes)
puts the measurement on production's population.
Caught by checking the reported roster size against the corpus rather than
against the receipt's own internals.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
* Receipt: exclusive attribution + selected-entry overlap, and the verdict
Both halves measured, machine-readable receipts stored beside the writeup.
A. Exclusive partition reconciles (tolerance 0ns, remainder 55.1ms of
73158.3ms). load is 68.2% of resolve-span time, typecheck_compute 24.4%,
everything else 7.4%. Machinery is 37.7% of all resolve-span time even in
a single-entry run. The load-bearing detail: load IS the closure walk, and
its inner scan referenced_module_paths_in_text is a full-content byte scan
run once per (entry, module) pair with no memo -- so B's duplication factor
is not an abstract ratio, it is the multiplier on the dominant cost.
B. Three real subjects from already-known main commits. Duplication factor
35.9 / 38.4 / 38.3 across 3 / 13 / 29 changed paths -- stable across a 10x
range of diff breadth, so overlap is a property of the corpus shape, not of
the diff. 97.2-97.4% of closure memberships are repeats. The union is
nearly saturated at the narrow subject: N grows 37% while the union grows
15%. Max fanout is ~N in every subject; the median module is rare and falls
as N rises, so the shape is a universal std core plus a long private tail.
Verdict: STRENGTHENS the premise and RELOCATES the prize. The pole that
would have closed the program (disjoint closures, factor 1.0) is decisively
absent. But the prize is in load, not typecheck -- typecheck_compute is
already content-key memoized through typed_module_cache, so a union
justified as "typecheck once" would buy something largely already owned.
And because the repeated unit is a pure function of source content, a
per-source memo keyed on content hash would collapse the same 35.9-38.4x
on the scan portion with NO union graph. Slice 2 should price that rival
before committing. Recorded as a finding, deliberately not implemented --
this deliverable is measurement.
resolution_divergence_census is kept separate as instructed: it runs as its
own binary, so its closure-scoped resolve is a different process that an
in-process union cannot displace.
The receipt also records a fidelity defect caught mid-measurement: the
first run's probe exclusions produced a 45-entry roster against 579 files,
and every derived quantity was internally consistent while describing 8% of
the corpus. Invisible from inside the receipt; caught only by checking the
roster against the corpus on disk. Those numbers are withdrawn.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
* WIP: Lane B
* chore: regenerate drifted generated artifacts (ci auto-heal)
* Cite the receipt from the DESIGN authority, not the projection
My previous fix edited DESIGN.md directly and the CI auto-heal bot
reverted it in 9d63c7318d -- correctly. DESIGN.md is a GENERATED artifact
(gunbc.generated_artifact DesignArtifact -> gunbc.design_document
expected_design_md), so a hand edit to it is a change to the projection
while the authority still says otherwise, and the drift gate regenerates
it away. The authority is dag/gunbc/design_document.dag.
That is the same shape DESIGN §5 names from the other side: a check
satisfied by editing the declaration while the realization lies. Here the
realization was edited while the declaration lay, and the healer is what
made it observable rather than silent.
The citation now lives in design_document.dag and DESIGN.md is regenerated
from it via the declared regenerator (main_wet on
dag/tools/generated_artifact_gate.dag), so the two are a fixed point.
Verified by execution before push: doc_graph_has_no_orphan_docs on both
entries, doc_graph_is_clean, and the drift witnesses
witness_committed_is_fixed_point, witness_committed_fixed_point_red_control,
witness_all_known_committed, witness_registry_complete all pass.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
* WIP: Lane B
* RETRACT three claims this PR asserted; measure what load actually is
Operator review point 1 (repeat the partition) and my own sub-attribution
falsified three claims. They are retracted in the receipt and in the
DESIGN authority rather than edited out, because how they failed is the
reusable part.
RETRACTED 1 -- "load is dominated by referenced_module_paths_in_text, an
unmemoized per-(entry,module) content scan." Measured: 3.9-23.0ms, ~0.0%
of load. It was inferred from reading the call path and never measured --
the §5 specification-without-execution trap, committed while writing about
it. The missed step: load_sources_for_entry_with_pool calls
load_sources_for_entry_with_index AND THEN
extend_sources_to_both_closure_fixpoint, which the first instrumentation
never timed.
RETRACTED 2 -- "load is the dominant cost." True at 67-68% on a
159-module closure; FALSE at 38-40% on a 504-module one, where
typecheck_compute is ~50%. Run-to-run within an entry is stable (67.0/68.0,
37.9/39.5), so the partition is sound and the generalization was not: it
came from one run of one entry.
RETRACTED 3 -- the A x B join and the per-source content-hash memo that
followed from it. Both depended on claim 1.
MEASURED INSTEAD: load is ~100% build_both_closure_edge_index, a
CORPUS-wide edge index memoized per MultiEntryIndex at ~25.6s per index,
INDEPENDENT of the entry's closure size (159 and 504 module closures pay
the same). So it is fixed per index -- not per entry, not per membership.
The claim_batch harness pays it twice only because two indices exist on
that path (its own build_multi_entry_index plus process_shared_index for
machinery).
THE BOUND THAT MATTERS: because the dominant row is a fixed per-index
construction, every share in section A describes a fixed-cost-dominated
harness, NOT the floor, where one index amortizes across hundreds of
entries. The verdict is therefore "not answerable from this data" rather
than the strengthens-and-relocates claim it previously carried -- a union
program justified by these shares would be justified by an artifact of the
instrument. The deciding measurement is a partition from the
claim_executor discovery path: wired in this PR, and never run.
B's membership numbers are unaffected -- they are counts, not timings, and
the disjoint-closure pole that would close the program outright is still
decisively absent.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
* Fix three positional citations, one of which pointed at nothing
review 45321 asked for symbolic citations in place of line ranges. Verifying the
three sites found that one was not merely fragile but wrong:
compute_fabric.dag:414-423 — that file is 139 lines. PerformanceReceipt is not
in it at all; it lives in gunbc.fleet_intent. The field list was wrong too:
`wall_duration` is not a field, the time axis is `cost: CostAccount<Nano>`.
Corrected to name the real symbols: gunbc.fleet_intent.PerformanceReceipt, its
roll-up fn cost_account_from_performance_receipts, and the
std.realization_schedule.CostAccount / CostBasis it feeds — all verified present.
The other two (realization_schedule.dag:25-26,33-39 and cli_run.rs:2062) resolved
correctly; ranges dropped since the symbols were already named.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
* Register measure_selected_closure_overlap in the explicit bin roster
It was the only one of 31 bin files without a [[bin]] entry. Cargo auto-discovers
it (edition 2021, autobins defaults true) so it built and ran, but matching the
surrounding convention costs nothing and removes the discrepancy.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
* The A.7 table quoted an unretained run; the committed fourth receipt refutes it
Operator review point 1 asked for >=2 entries x >=2 runs showing the share
ordering holds. It does not hold, and the previous table hid that by quoting
figures from a run set that was never committed.
Real committed receipts, all four:
ci_floor_measurement r1 parent 75.2s load 51.24s/68.11% tc 18.48s/24.57%
ci_floor_measurement r2 parent 66.4s load 44.96s/67.68% tc 16.57s/24.95%
generated_artifact_drift r1 parent 131.0s load 50.98s/38.93% tc 65.56s/50.06%
generated_artifact_drift r2 parent 155.7s load 77.11s/49.52% tc 64.55s/41.46%
The ordering flips between two runs of the SAME entry (drift r1 typecheck leads,
r2 load leads), so the earlier "inverts across entries" reading was an artifact of
comparing two runs that happened to agree.
What survives is in the absolute columns: typecheck_compute is stable per entry
and scales with closure size (18.5/16.6s at 159 modules vs 65.6/64.6s at 504),
while load does not track closure size at all (51.24s vs 50.98s) and its magnitude
swings 44.96-77.11s across runs. Corpus-fixed and noise-dominated. Confound
disclosed: these runs shared the host with concurrent cargo builds.
Retraction (b) is itself corrected here rather than silently replaced -- its
"false at 38-40% on a 504-module closure" replacement rested on the same
unretained run set.
Adds cost-partition-generated_artifact_drift-r2.json so every quoted figure has a
committed receipt behind it.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
* State B's weighting, and redo it byte-weighted
Operator review point 3: the overlap figures carried an unstated uniformity
assumption -- every membership counted as one regardless of module size.
Stated: the B table is module-count weighted. Redone byte-weighted on the same
subject, same selection (roster 809 / selected 316 / skipped 493, identical to the
committed typical receipt):
duplication factor 38.42 by count -> 47.92 by bytes (+24.7%)
repeats as share 97.40% -> 97.91%
union 1,243 modules -> 11.45 MB of 548.90 MB summed
The count-weighted figure was the conservative one: high-fanout modules are
systematically larger than average, which is consistent with the universal core
being std.algebra / std.types / std.error_primitives rather than small leaves.
This moves the weighting in the direction that favours the union program, and the
section says explicitly that it does not rescue it -- A.7 is why no membership
count here converts into a displaced cost. It is a better-weighted upper bound,
not a different kind of claim.
Receipt: closure-overlap-typical-byte-weighted.json.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
* WIP: Lane B
* Measure the amortization: load is per-index, so the union program loses its target
A.7 said load's share on a floor run "must be smaller -- by how much is
unmeasured." Measured here on the explicit-entry path, which puts N entries
against ONE shared index with everything else held fixed:
N=1 (2 spans) N=6 (7 spans) growth
parent 69.97s 114.12s 1.63x
load 47.44s 51.32s 1.08x
load_bare_edge_index 47.40s 51.18s 1.08x
typecheck_compute 17.34s 49.64s 2.86x
parse 1.14s 3.66s 3.21x
resolve_modules 0.02s 0.11s 4.40x
load share of parent 67.79% 44.97%
Entry count rises 6x and every per-entry row rises with it; load rises 8%, which
is inside the noise band already established for that row. load is paid once per
INDEX, and the existing per-index memo already amortizes it. The N=1 run
reproduces the discovery-path receipts (67.79% vs 68.11/67.68%), so the
explicit-entry path measures the same thing.
THE REDIRECTION: a union graph cannot displace a cost that is already paid once,
so the program's apparent target -- the row that dominated every single-entry
partition at 67-68% -- is eliminated, not merely unproven. The only measured row
scaling with both entry count and closure size is typecheck_compute, whose unit of
work is module membership. That is the only surviving candidate and it is NOT
established: converting repeated membership into repeated computation needs
per-entry typecheck attribution against a shared env, which nobody has measured.
The duplication factor must not be quoted as a multiplier on typecheck time.
Projection to floor-scale N is marked as a projection, not a receipt (two points,
six small entries). Whole-corpus floor runs OOM-killed twice (exit 137, at 1,513
and 1,046 entries) including under GUNBC_MEMORY_BUDGET_BYTES=44GiB, which governs
realization admission rather than resolve-pool retention.
Also completes the byte weighting across all three subjects (43.04 / 47.92 /
49.25 against 35.89 / 38.42 / 38.27 by count) and corrects B.1 read 1: "stable
across breadth" holds by module count but not by bytes, where the factor rises
monotonically.
Receipts: cost-partition-amortization-n{1,6}.json,
closure-overlap-{narrow,broad}-byte-weighted.json.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
* Fix a control this PR broke, and make it assert the invariant instead of a count
rewire_sub_rows_are_inclusive_and_never_enter_the_exclusive_sum asserted
p.inclusive.len() == 3 -- a count over EVERY inclusive row, not just the rewire
ones. Adding the load_* sub-attribution earlier in this PR took that to 10 and
turned the control red. It went unnoticed because the rust suite was removed from
CI on 2026-07-11 and runs locally only.
Two changes:
- Filter to contained_in == "assembly_rewire" and assert those three rows account
for all 300ns of the parent. A global count makes this control fail whenever an
unrelated row gains a sub-row, which is exactly what happened.
- Add the invariant the count was standing in for: every inclusive row names a
parent that is itself an exclusive or inclusive row, so it is already counted
and can never be attributed to nothing. Proven to discriminate by mutation --
repointing load_bare_edge_index at a nonexistent parent goes red with the
located diagnostic, and only that test.
Also corrects InclusiveCostRow.contained_in's doc comment, which claimed the
parent is always an exclusive row. It is not: load_bare_edge_index nests under
load_bare_reference_closure, which nests under load.
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>
* WIP: PR #7485: does identity coercion (node already inhabits the target model
* Separate identity admission from semantic grounding
* Tie identity admission to target model authority
* Revert "Merge remote-tracking branch 'origin/main' into agent/identity-coercion-grounding"
This reverts commit 64bf6c2b6050e0435592c868489fbc06b1fd94b3, reversing
changes made to 3d177ac304852224852c03d588495d0df56d1572.
* Repair #7490: stale v1-compiler-tests callers + compile gate (#7494)
* WIP: repair 7490
* Repair #7490 fallout: fix stale typecheck_module callers and enroll compile gate.
PR #7490 added global_variant_base to typecheck_module but left four
v1-compiler-tests integration callers stale; main would not compile that
crate. Wire the seventh argument (empty_map for incremental helpers;
global_bare_variant_locals in the receipt test) and add a build-job
cargo check -p v1-compiler-tests --tests step so future signature
migrations cannot land without compiling direct Rust test call sites.
Co-authored-by: Cursor <cursoragent@cursor.com>
* Fix CI compile gate: drop unused import under -D warnings.
The new v1-compiler-tests compile check runs with RUSTFLAGS=-D warnings;
module_authority_resolution_test.rs had a stale diagnostic_to_message import.
Co-authored-by: Cursor <cursoragent@cursor.com>
* Fix witness parse error: replace invalid `..` rest pattern in match.
The .dag parser rejects RunStep { run: cmd, .. }; use explicit field
patterns like ci_heal_job_witness_test.dag.
Co-authored-by: Cursor <cursoragent@cursor.com>
* Address review 45392: scaffold compile gate on cargo.Build.Check authority.
Add extdeps.cargo_build.Check, move the build-job step to
ci_v1_compiler_tests_compile_gate_emit with Disposition=Scaffold +
dissolve-on marker in the emitted script (same class as
ci_release_build_script), and enroll scaffold/dissolve witnesses.
Co-authored-by: Cursor <cursoragent@cursor.com>
* WIP: repair 7490
* Fix CI: parse error in HAND-RUST witness and typed CARGO_BIN emit.
The regen/heal jobs failed because v1_compiler_tests_typecheck_module_callers_hand_rust_witness_test.dag split == across lines (parse error). Route CARGO_BIN through ShellExecutablePosition HostEnvVar on BoundOperationInvocation so effect_plan_bash_materialize emits via bash_build_word_var instead of post-processing emitted shell strings; regen ci.yml for grammar-quoted argv.
Co-authored-by: Cursor <cursoragent@cursor.com>
* WIP: repair 7490
* Address review 45415: move executable override to Bash layer.
Revert ShellExecutablePosition from v2.std.operation_argv BoundOperationInvocation; add BashBoundOperationInvocation wrapper in effect_plan_bash_materialize with bash_bind_operation_invocation_host_env_executable for CARGO_BIN grammar emission. Keeps operation intent (ref + bindings) transport-agnostic per DESIGN §3.
Co-authored-by: Cursor <cursoragent@cursor.com>
---------
Co-authored-by: gunbc-ci-auto-heal <gunbc-ci-auto-heal@users.noreply.github.com>
Co-authored-by: Cursor <cursoragent@cursor.com>
* Stop re-walking the string to read one character (Lane A: process_escapes_loop onto source_chars) (#7491)
* WIP: Lane A
* WIP: Lane A
* Count the escape receipt as v1 seed growth with a dissolution trigger
Addresses review 45369. The cited hand-maintained stage0 ratchet does not
reach a tests/ target, but the discipline point stands: the receipt is hand
Rust in the v1 seed tree and was silent. escape_receipt_seed_growth_mark
records what it carries, why it is not a .dag witness today (the resolve-count
bump is operator-signed), and the two triggers that delete it.
* Demote the escape cost separation to a non-gating benchmark
Addresses review 45416. Gating correctness on wall clock can red correct
code when the larger run is the one that catches contention. The three
deterministic decode tests keep gating; the ratio test is #[ignore]d and
runnable with --ignored. The on-carrier mark and the lane doc now say which
half gates, why the deterministic-counter alternative lands non-gating too,
and that the durable guard for this class is a structural lens.
---------
Co-authored-by: Brian Searls <briansearls1@gmail.com>
* Require canonical shape for literal grounding
* Revert "Merge remote-tracking branch 'origin/main' into agent/identity-coercion-grounding"
This reverts commit a7c3ef1b33ee457f19b8906630e2cfe03ab20e4c, reversing
changes made to 56460cc48722818f9274d01f94210b7d38aa0165.
* WIP: PR #7485: does identity coercion (node already inhabits the target model
---------
Co-authored-by: Brian Searls <11205878+briansrls@users.noreply.github.com>
Co-authored-by: Claude <noreply@anthropic.com>
Co-authored-by: Brian Searls <briansearls1@gmail.com>
Co-authored-by: gunbai-bot[bot] <289086189+gunbai-bot[bot]@users.noreply.github.com>
Co-authored-by: gunbc-ci-auto-heal <gunbc-ci-auto-heal@users.noreply.github.com>
Co-authored-by: Cursor <cursoragent@cursor.com>
…t the replacement compiler) (#7485) * WIP: p0 - protect the replacement compmiler * WIP: p0 - protect the replacement compmiler * v2 no longer treats source identity as semantic grounding v2's infer routed nine of the closed vocabulary's twelve node kinds (6 connectives + 6 behaviors; only Branch/Match/Loop had a derivation) through a wildcard arm into solve_constraints with the singleton candidate set [root], under a predicate reducing to root == root. The grounding it minted carried the source node as its own structural evidence — and inferred_facts_resolved_type reads exactly that field, so every literal, binding, type and operation in v2 was typed as itself. Measured on main: canonical_grounding_for_node returned evidence == source for TypeNode{Conj} and TypeNode{Disj}, feeding 06_translate's coerce_grounded_node. - canonical_grounding_from_derived_type is now the single construction authority and refuses derived_type == node (^grounding_evidence_is_source) - InferredFacts.grounding becomes DerivedGrounding | GroundingNotDerived, so candidate == source is not expressible as a grounding - infer_gather_fold_init enumerates all twelve kinds; no wildcard arm - consumers refuse rather than silently consume: canonical_grounding_for_node, the Witness-returning accessors, eval's acceptance witnesses, and the branch/match/loop operand-type reads - the frontier is typed, located and counted on the Accepted path (^infer_grounding_not_derived), with a per-kind dissolution trigger - canonical_grounding_admits_infer_facts gains evidence != node as the backstop for hand-built records the constructor cannot reach solve_constraints is untouched: the solve-design authority says extend, never fork, and DESIGN already records that it closes only a singleton scaffold. This stops infer from reading that tautology as a derivation. Witnesses: src/v2/test/claim/infer_self_grounding_wall_test.dag (8, RED controls both directions). branch_infer_test 4/4 and loop_infer_iteration_test 5/5 stay green. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * WIP: p0 - protect the replacement compmiler * Withdraw the evidence!=node read-path proxy; record the compile-entry refusal CI surfaced two things the local witness set had not. 1. The `evidence != node` conjunct added to canonical_grounding_admits_infer_facts was a PROXY for "was this grounding derived?", which the NodeGrounding carrier already answers exactly. It false-positived: v2_evaluator's bool fixture uses one atom as both the evaluand and the runtime value's primitive_type, so resolved == algebra there is that fixture's coherent encoding of "this atom denotes Bool", not a fabrication. Keeping the conjunct would have meant rewriting a thesis-proof fixture so a check went green — the inversion DESIGN §5 names. Withdrawn; the wall stays where it is exact (the construction authority for every grounding the compiler mints, plus the carrier). The hand-built residue is now asserted by a witness rather than left implicit. 2. compile_eval_bool_via_compile_entry_holds went through the REAL infer and passed only because the fabrication made eval's resolved_type check compare the pin against itself. v2 has no derivation rule for TypeNode{Atom}, so it now refuses, typed and located (^infer_grounding_not_derived). Renamed to say so, with a dissolution trigger. The compile->eval thesis is unchanged and still proven by the compile_inferred path (isolate_t1/t3); what is no longer claimed is that v2 can infer those facts itself. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * WIP: p0 - protect the replacement compmiler * WIP: p0 - protect the replacement compmiler * Reword two note strings whose braces the .dag lexer read as interpolation The heal_generated_artifacts CI failure — `cannot apply Div to Variant and Variant` — was not a semantic consequence of the grounding wall. It was a lexing accident in prose I wrote in this same PR. Located by execution, not inspection: instrumenting the interpreter's ExprBinOp arm to print its locus gave `[TEMP-LOCUS src/v2/compiler/04_infer.dag:10694..10697]`, which is line 334, inside a `data ... : String` note reading ...which is precisely why TypeNode{Conj}/{Disj} self-groundings walked through it... `{...}` inside a .dag string literal is an interpolation. So `{Conj}` and `{Disj}` were parsed as coproduct Variant expressions and the `/` between them as division — a well-typed-looking string that is really an arithmetic expression over two variants. Reworded to `Conj/Disj type-node self-groundings`, and the same hazard in compile_eval_thesis_proof_test.dag's `TypeNode{Atom}` to `the Atom type-node kind`. The instrumentation is reverted; no interpreter change is part of this commit. Worth recording because it is an instance of the class this lane exists to close: an unescaped brace in a string is statically decidable (the corpus already ships the `\{` escape), yet it compiles clean and fails only when the interpreter reaches an operator it cannot apply, with a diagnostic that names neither the file nor the string. Not fixed here — noted so it is tracked rather than absorbed. Also removes dag/tools/artifact_div_probe.dag, a throwaway bisect probe that autocommit picked up twice. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Separate identity admission from semantic grounding (#7495) * Typecheck perf: sink the where-refinement peel, wire the once-per-closure variant base, share the process index (#7490) * Sink where-refinement peel to the refusal path (#7438 cost-shape fix) where_refinement_mismatch_diags runs on every infer_expr with an expected type; peel_nominal_alias_identity (an unmemoized resolve_node_bounded rebuild) was computed eagerly and discarded on the 97% of calls that find zero predicates — 6.5s of 6.7s measured on the host_effect_realize entry compile (79,168 calls, 76,773 zero-predicate). formal_checked is consumed only by where_refinement_diags_for_predicate, so it now computes inside the uncovered-predicates else, the only branch that reads it. Behavior-identical by receipt: host_effect_realize compile diagnostics byte-identical pre/post (915 advisory, 0 blocking); direct RED probe (0 at PositiveInt return) still hard-refuses; all 16 where_refinement_enforcement_witness rows PASS including every refusal control. Rationale carried in-tree as where_refinement_peel_cost_note (the corpus has no comment syntax; data-note is the idiom). Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01UaAWvG3LgBAM9tGF1D2bG1 * Wire the once-per-closure variant base #7398 authored but never called merge_global_bare_variant_locals rescanned the whole global_bare census and re-inserted every eligible variant-owner pair into every module's locals map: 464 modules x 12,554 census keys = 5.8M iterations and 1,286,399 persistent-map inserts = 31.4s (14%) of the host_effect_realize entry compile. The eligible pairs depend only on (global_bare, si) — a whole-closure fact — and #7398 landed build_global_bare_variant_locals computing exactly that base map, with zero callers. This wires it: typecheck_with_census_extra computes the base once per closure and threads it down realize_module -> typecheck_module -> build_module_context; the merge becomes map_merge(base, state.locals) — overlay wins, exactly the old skip-if-present arm, and the old checked-insert collision arm was unreachable (presence checked before insert), so the global merge contributes zero collision errors then and now. The cli_run resolve leg (the floor/claim path) computes the base beside each composed per-root index in tree_symbol_index_memo, keyed to the index it belongs to. Cost per module drops from O(|census|) inserts to O(|module locals|). Measured on the same entry: merge inserts 1,286,399 -> 7,263 (177x), merge self 31.4s -> 0.08s, build_module_context 34.6s -> 2.6s, compile.reconcile 72-76s -> 44s. Behavior receipts: compile diagnostics byte-identical (915 advisory, 0 blocking); witness suites green by execution — where_refinement 16/16, e0599_probe_census 18/18, namespace_import_closure (wet) PASS. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01UaAWvG3LgBAM9tGF1D2bG1 * Route the strict entry-closure loader through the process-shared index A `gunbc compile --entry` process built its closure index in load_sources_for_entry_with_pool_index, dropped it, and then the first compile-clean diagnostic classification rebuilt the same index from scratch inside resolve_entry_graph_shared — to evaluate the one compile_clean_diagnostic_policy Bool. Measured on the host_effect_realize entry compile: 2 index builds, pool_parse over 5,450 files for a 2,725-module pool, 4 tree censuses (2 per root) — the whole corpus full-parsed twice per process. Strict pool policy now routes through process_shared_index (the same construction fn and canonical roots key), so the policy read is a cache hit; primary-precedence keeps its own fresh build since the shared index only builds strict. Measured after: index_builds=1, pool_parse files=2,725, tree_census calls=2, loader fixpoint 60.0s -> 27.3s, whole compile 3m01s -> 2m13s on the same box. Diagnostics byte-identical (915 advisory, 0 blocking). Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01UaAWvG3LgBAM9tGF1D2bG1 --------- Co-authored-by: Claude <noreply@anthropic.com> * Design note: seamless deploys — ground the four items, re-cut two of them (#7477) * WIP: server deploy untangling * Design note: seamless deploys — ground the four items, re-cut two of them Modeling-first draft for the seamless-deploys brief. No behavior changes; the only code is the typed doc-graph binding the note needs to be reachable. Grounded every claim against the tree. Three items confirm line-exact; two side claims correct: - The restart count resolves opposite to the brief's caveat. 40 deploy_dashboard_srv1 jobs ran in the 24h window ending 2026-07-30T20:11Z (38 success, 2 failure), every one running the unconditional restart arm — so deploys alone exceed the 24 observed restarts and need no manual restarts to explain them. Bounded honestly: no srv1 access from this session, so what is measured is restart commands issued. - "208 sources" matches neither figure the tree records (a 91-source closure, 2,356 files read). Corpus is now 2,719 files, up ~15% in nine days, so the 40s startup expectation is already drifting. Two items re-cut along model seams rather than as stated: - Item 2 is a §3 de-fork, not a standalone outage fix. Readiness is modeled twice — systemd's Type=simple (ready at spawn, wrong by ~35-40s, every time) and live_deploy's healthz poll (correct). The second exists because the first lies. The deploy already routes around it, so its independent cost today is small; its value is that it is the prerequisite for any handover. - Item 3's fix is construction, not validation. The apply pole passes observed: [] (emit.dag:158), so both poles are degenerate and Unchanged-to-noop is structurally unreachable — the deploy cannot diff. The fix is supplying the observed set, not adding a changed-predicate to the restart step. Notes that this makes the spine's ownership refusal arms live on a path that today always applies, and that "could not observe" must refuse rather than widen to restart-everything. Also flags that socket activation makes item 1's new sentence unreachable in the case it was written for, and that the transport arm must not assert "deploying" — a cause it cannot establish. Doc-graph binding uses the typed HandAuthoredDocBind row; the prose "bind:" scan is deleted. RED control observed: the orphan wall went true -> false -> true across adding the doc unbound and then binding it. * Restore the trailing blank line in service_ready.dag Unrelated churn from removing the staging prose row — the file's trailing blank line is now byte-identical to main. * WIP: server deploy untangling * Correct two re-cuts that prescribed models they could not establish (review 45229) codex/codex-default requested changes on two central claims. Both verified against the tree and both correct; fixed in place with the correction recorded rather than silently restated. Item 3 — the observed-set claim was wrong, and dangerously so. The draft said supplying `observed` needs "no new comparison logic, no new authority." spec.dag:38-41 declares DeploymentArtifactStep { kind, path } with no content identity, and deployment_step_value_eq is `a == b` over exactly that. Supplying observed rows at the same paths therefore returns Unchanged for every member always — not "cannot distinguish changed from unchanged" but an inversion into a silent never-deploy, strictly worse than today's always-restart. It is also the shape DESIGN §5 names: satisfiable by editing the declaration while the realization lies. Split into 2a (model the comparable artifact value at its single authority) then 2b (supply the provider), with the ordering load-bearing. Item 2 — the de-fork framing was wrong; the draft committed the same state-space conflation it accused systemd of. There are two facts, not two representations of one: F1 process-bind readiness (systemd asserts it via Type=simple and is false by ~35-40s; sd_notify genuinely fixes this) and F2 deployment surface identity (only the digest establishes it; systemd can never know it). readiness.dag's service_ready_means_serving_this_tree_note records why, with a dated receipt: gunbc serve binds its graph once at start, so the pre-restart process keeps answering during the replacement's load, and on 2026-07-24 srv1 served a stale surface with every check green. sd_notify fires exactly when F2 is still unproven, so on that axis it is weaker than what exists today. The digest check must survive slice 3 — now a red control, not a caution. Downstream sections updated to match: sequencing (2a before 2b; slice 3 does not touch the digest), red controls (a binary-content-only change must still restart — the control that discriminates the 2a defect; and the 2026-07-24 shape must still refuse after notify lands), and the sign-off questions (item 3 is gated on a load-bearing carrier change, not the cheap slice first implied). Verified: doc_graph_roots.dag compiles 0 blocking errors; orphan, dangling-link, and slug-collision witnesses green. * Derive the restart from the service's inputs, not from the unit file (review 45232) Third defect found in item 3, and the deepest: content identity alone still does not restart the service. Reconciliation is per member, and the only restart of gunbc-roadmap.service is emit.dag:288 inside the SystemdUnit upsert arm (emit.dag:219 restarts gunbc-tree-sync.service, a different unit). So under a real diff a binary-only change installs the new binary, leaves the unit file untouched, and SystemdUnit reports Unchanged -> noop: new binary on disk, old process still serving it. The discriminating control added after review 45229 would have FAILED against the design as written — the re-cut omitted the dependency that makes its own control pass. Root cause is a conflation the degenerate pole has been hiding. SystemdUnit names two things: the unit FILE (an artifact, valued by its text) and the RUNNING SERVICE (a process, whose correctness depends on the binary and tree it started from). emit_deploy_member_effect_note fuses the restart onto the file — harmless while every member always applies, the defect the moment the diff is real. The dependency itself is already known and already single-authority, but only in prose: deployment_apply_order_note says "all before the unit (ExecStart references binary + tree)". Construction answer: model the running service as its own member whose value derives from the identities it was started from, so a binary change makes the service Modified and it restarts by construction — no impact table, no restart_required_by adjacency (which would re-represent the dependency the apply order already asserts). New binary installed with the old process serving becomes unwritable rather than checked for. Item 3 is now three steps: 2a comparable value -> 2b de-fuse the service from the unit file -> 2c observed provider. Every partial order typechecks and silently under-deploys (2c without 2a never deploys; 2c without 2b deploys the files but not the service), so the binary-only control is stated as item 3's acceptance bar rather than a nicety — checking only that the binary reached disk is what makes both failures look green. §7 q3 sharpened: item 3 is the one item NOT required for the headline outcome (slices 1, 3, 4 make deploys invisible; item 3 only makes them rarer), so if the two carrier changes are out of scope it should be dropped entirely rather than attempted partially. Verified: doc_graph_roots.dag compiles 0 blocking errors; orphan and dangling-link witnesses green. * State item 4's dependency once, authoritatively: it needs B, not C (review 45241) Internal contradiction, correctly caught. One section headed "Item 4 is downstream of B and C" and treated the two jointly, while §2 Concept B named only item 2 as the handover prerequisite and §7 q3 said item 3 is not required for the headline outcome at all. Read as a plan, that would have gated the cheap handover work on the most expensive item in the ticket. The truth, now stated in one place: - B IS a prerequisite. Handover means move traffic when the replacement is ready, and there is no trustworthy "the replacement has bound" signal without it. - C is NOT. It changes how often a handover runs, never whether it works. A handover built with C outstanding is correct — it just runs on all ~40 deploys/day instead of the subset that changed something. Nothing in item 4's design reads a reconciliation fact. §5 restructured around the dependency graph rather than a numbered list that implied an order: slice 1 — no dependencies slice 3 -> slice 4 — the ONLY hard edge in this ticket slice 2a -> 2b -> 2c — internally ordered, independent of 1, 3, 4 with the recommended order now headline-first, cost-last (1, 3, 4, then 2), since slice 2 is both the most expensive item and the only one that does not serve the headline. Slice labels are named as labels, not sequence. Audited every remaining "prerequisite"/"downstream"/"gated" statement in the note for consistency with this; item 3's internal 2a->2b->2c gating is the only other one and it is correct. Verified: orphan and dangling-link witnesses green. Doc-only change. * WIP: server deploy untangling * Deploy reconciles to intent with minimal items (operator direction 2026-07-30) Operator: "i'd like deploy to use our existing apply/delete/reconcile type process (i.e. bmc/srvN apply) — i want to deploy the minimal possible items to update to intent." This answers §7 q3 and re-prioritises the ticket. Item 3 was written as an optional scope reducer to be dropped if expensive; it is the deployment ask. "Minimal possible items to update to intent" IS the spine's Unchanged -> noop, and the vocabulary maps one-to-one: apply = MemberUpsert, delete = MemberTeardown (owned-only, else typed refusal), reconcile = the diff, with unchanged members producing no hunk and no effect. Grounded against the siblings, which changes the cost estimate materially — this is instantiation, not invention. live_deploy is the ONLY degenerate consumer of a spine others already drive non-degenerately: - 2a comparable value — precedent gunbc.host_authorized_keys_reconcile: value_eq compares content (algorithm + material + comment) while key_of returns identity (key material), so content drift is Modified -> re-upsert, never Remove + Add. That identity/value split is exactly what DeploymentArtifactStep lacks. - 2c observation — precedent gunbc.tool_readiness, live today: reconciles desired Pin<CliTool> against an observed one from extdeps.realization.emit_on_demand_host.observed_tool_identity, with three typed outcomes (Found/Missing/Duplicate). Its observed_pin_projection_note solves deploy's projection problem too — build the observed member from desired, replacing only the observed field. - The apply site is gunbc.host_effect_realize (:990, :1076), already running reconciles inside srvN apply — the process named in the direction. So 2a and 2c are patterned work. 2b — de-fusing the running service from the unit file — remains the only part with NO precedent (no sibling has an artifact whose realization is a running process), and is where design attention belongs. Two decisions surfaced, both deliberately left to a human by the sibling modules: (1) observed scope and delete semantics — deploy's members are a closed set of owned artifacts at known paths, unlike authorized_keys' everything-on-host scope, so wholesale-refuse is defensible, but Removed -> teardown becomes reachable on the apply path for the first time; (2) Missing means Added -> upsert, while an observation that could not be TAKEN must refuse typed/located/counted, never degrade to reinstall-everything — the absorbing fallback wearing this ticket's own clothes. §5 recommended order revised: slice 2 is no longer the item to cut under pressure. It still gates nothing (graph unchanged), and can run in parallel with 3/4 since they share no seam. Verified: orphan and dangling-link witnesses green. Doc-only change. * Correct an over-pessimistic claim: 2b composes two existing patterns Verified rather than left asserted, because the claim drives the cost estimate the operator is budgeting against. The note said no sibling has an artifact whose realization is a running process, so de-fusing the service from the unit file had no precedent. That is wrong. gunbc.roadmap_belt reconciles LIVE DISPATCH SESSIONS — running processes — with a genuine observed provider (belt_observed_members(live: List<DispatchLiveSession>)), ownership lifted from an actuator observation, and R5 teardown meaning reap a live session, refusing when it cannot prove ownership. Process-as-member, live observation of processes, and owned-only teardown of a running thing are all precedented. The genuinely new cell is narrower, and naming it precisely is what makes 2b tractable — it is one cell of a 2x2: inert artifact running process presence-only — roadmap_belt content-sensitive authorized_keys, tool_readiness deploy (empty) The belt's member value is deliberately degenerate: dispatch_member_value_eq returns constant true, so it never produces a Modified hunk. A session exists (Unchanged), is missing (Added -> spawn), or is extra (Removed -> reap). It has no notion of "this running thing is stale relative to the inputs it was started from" — which is exactly deploy's requirement, and exactly the axis on which today's always-restart is hiding. So 2b composes belt's process-member machinery with the siblings' content-sensitive value. Materially smaller and lower-risk than "no precedent" implied. The remaining design question is one thing: what are the running service's inputs, such that its value changes exactly when a restart is genuinely required — answered by 2a's identities. Verified: orphan and dangling-link witnesses green. Doc-only change. * Measure the serve closure: 208 is correct, the tree's figure is the stale one Settled §7 q5 by running the unit's exact ExecStart on a spare port rather than leaving it as a question for the operator. [t+56s] resolved 208 sources [t+59s] compile.frontend done in 3 seconds [t+59s] compile.normalize done in 298ms [t+74s] compile.reconcile done in 14 seconds [t+74s] compile.analyses done in 213ms [t+74s] gunbc serve listening -> roadmap_serve_handle() The brief's "208 sources" is the real resolved-closure count. This note's earlier objection to it was WRONG, and it is the tree that is stale: live_deploy_service_ready_poll_bound_reason's "a closure of 91" does not match what the entry actually resolves. Corrected in §1 and q5 marked resolved. The phase split is the more valuable half and confirms the load-dominant diagnosis by execution: 56s of 74s (76%) elapses BEFORE "resolved 208 sources" prints — the load phase — with the whole compile accounting for 18s, of which reconcile is 14s. That is the deep fix's premise measured rather than cited. Honest caveat recorded in the note: 74s is this build box under concurrent load, NOT srv1, and must not be read as a regression against srv1's recorded 35/36/36/39s. Machine-independent are the source count (exact) and the load-vs-compile ratio. It does suggest expected_startup = 40s wants re-measurement on srv1 given ~15% corpus growth since it was calibrated. Also fixed: a missing blank line that broke the operator-direction block out of its list, and the §1 intro sentence which no longer described the two side claims below it. Verified: orphan and dangling-link witnesses green; no stray serve process, port 18080 free. Doc-only change. * Retire two stale cross-references my own corrections created (review 45260) Both findings verified and both real. Same root cause: I corrected §2 across successive reviews and left downstream sections pointing at the superseded text, so the operator-facing summary disagreed with the analysis it summarised. 1. §7 q3 still called 2b "the only part with no precedent" — superseded by the roadmap_belt finding, which showed 2b composes belt's process-member machinery with the siblings' content-sensitive value_eq. q3 now states all three sub-slices have precedent and names roadmap_belt alongside host_authorized_keys_reconcile and tool_readiness. The reviewer's concern is the operative one: a reader jumping to §7 for the operator answer would have planned virgin territory the note already refutes. 2. The review-45241 correction block cited "item 3 is not required for the headline outcome (§7 q3)" as a live claim, but q3 was answered — item 3 is in scope and not droppable. Rewritten to rest only on §2 Concept B, with an explicit scope note separating the two axes that were being conflated: PRIORITY (in scope, not droppable) versus DEPENDENCY (item 4 does not depend on item 3). Both are true; only the dependency claim belongs in that section. Swept the whole class rather than fixing only the two reported, since this is the second stale-cross-reference finding. That surfaced a third, unreported issue: "scope reducer" was being used to both reject a framing (§2: item 3 is "not an optional scope reducer to be dropped") and assert one (§2/§5: "C is an independent scope reducer"), which reads as self-contradiction. Disambiguated — priority language at the first site, and the second now says C is a scope reducer in FUNCTION while stating that this says nothing about its priority. Verified: orphan and dangling-link witnesses green. Doc-only change. * WIP: server deploy untangling * Reconcile the boundary and sequencing with the operator decision (review 45264) Both findings real, both the same class that has now produced most of this PR's review traffic: correcting §2 and leaving downstream text describing the superseded state. 1. §5 listed item 3 "whenever it is worth its cost" — discretionary language directly contradicting the operator direction that it is in scope and not droppable. As an executable plan that turns a mandatory requirement into optional work, which is the reviewer's operative point. Now: "Required, not discretionary. Listed last because it gates nothing and can run in parallel with 1/3/4 — NOT because it is optional." 2. The opening boundary still carried the brief's original "not what the deploy installs", which predates the reconcile-to-intent direction and reads as excluding item 3. Amended with the distinction the two halves need, since item 3 sits across the seam: - still OUT: the desired set — which artifacts constitute the deployment and what is inside them. This ticket adds no member and changes no artifact's contents. - now IN: how that set is applied — whether an unchanged member is re-applied, and the member modeling that makes "unchanged" decidable (content identity; the running service as a member distinct from the unit file). So the ticket does not change WHAT the deploy installs, it changes HOW MUCH OF IT IS RE-APPLIED to reach intent. The rest of the brief's out_of_scope stands verbatim. Swept the class again rather than fixing only the two reported. Remaining "optional"/"worth its cost" hedges: none. Also refreshed the Provenance block, which was itself stale in the same way — it cited only the original base commit and omitted every receipt added since (the six reconcile precedents, the readiness F1/F2 carrier, spec.dag's DeploymentArtifactStep, and both measurements). Separately, on my own judgement rather than a finding: shortened this note's HandAuthoredDocBind dissolution trigger from 201 words to 63. Sibling triggers run 5-58 words (median ~15), and the excess was restating the note's analysis inside the row — duplicating content that has a single authority and must then be maintained in lockstep. It had already needed updating twice in six revisions. The trigger now states the checkable condition and points at the note for reasoning. Verified: doc_graph_roots.dag compiles 0 blocking errors; orphan, dangling-link, and slug-collision witnesses green. * Cite by symbol, not position — 5 of 7 receipts had already rotted (review 45281) The reviewer's stated rule does not exist, but its concern was empirically correct and worse than reported, so the fix is made on the evidence rather than on the claimed rule. ON THE CLAIMED RULE: review 45281 cites a "locked 'cite the symbol, not the position' rule" in DESIGN §3. No such rule is in DESIGN.md — grep for both phrases returns zero. What §3 actually says about paths is "a fact's home is its LAYER, not its file (paths are discriminators, not gospel)", which is about where facts live, not citation format. DESIGN.md itself carries 5 positional file:line citations (algebra.dag:38, v1_interpreter.rs:8672, v1_compiler_emit_rust.rs:746, ctrl_session_witness.dag:93/97/101). So the rule as stated is not the authority's. ON THE UNDERLYING CONCERN: verified against the tree, and it is decisive. FIVE OF THIS NOTE'S SEVEN positional receipts had already drifted onto the wrong declaration, within a day of being written: emit.dag:123 Type=simple -> a Description= line emit.dag:158 observed: [] -> deployment_step_ownership_opt emit.dag:288 roadmap restart -> tree_sync_restart_step_with_diagnosis spec.dag:38 DeploymentArtifactStep -> a TailscaleServeMapping coproduct arm cli_run.rs:11918 TcpListener::bind -> a println! Every underlying claim still holds — only the positions moved as main advanced and was merged. But a document whose entire value is traceable evidence cannot carry receipts with that half-life. Converted every receipt to module + declaration: workflow_fetch_request_statements, emit_systemd_unit_doc, deployment_apply_plan, emit_artifact_upsert, tree_sync_restart_step_with_diagnosis, DeploymentArtifactStep, handle_serve, the v1-materialization-kernel node row, srv3_realize_os_install_actuator_toolchain_ensure_body, realize_provision_build_cache_body. Verified each symbol exists and still carries its claim. Zero positional citations remain outside the new citation note, where the rotted five are quoted AS the evidence for the convention. Also dropped the now-false "line-exact" qualifier on item 1's verdict. Verified: orphan and dangling-link witnesses green. Doc-only change. * WIP: server deploy untangling * State one authoritative scope: the ticket does change deployed content (review 45289) Finding verified and real, and the defect is broader than the instance reported. The boundary amendment claimed the ticket "adds no member and changes no artifact's contents." That is false for nearly every item in it — an over-tightening I introduced while fixing the PREVIOUS boundary finding: - item 1 edits roadmap_component.dag, which emits the dashboard JS — a change to the served tree, and the brief explicitly puts "how the browser is told what it is seeing" IN scope; - item 2 changes the unit file's own text (Type=notify) and the seed binary (sd_notify), both deployment artifacts; - item 4 may ADD a .socket unit — a new deployment MEMBER, not merely new contents. The reviewer reached this through the staleness cue, which is the mildest instance; the socket unit is the one that actually adds a member. Resolved by amending the boundary rather than dropping the cue, because the cue is in scope by the brief's own words ("how the browser is told what it is seeing") and exists to stop socket activation from silently showing stale data. The honest boundary is not "no artifact changes" — it is that the ticket does not change WHAT THE DEPLOY IS FOR: the dashboard's product behavior, what it shows beyond the honesty fixes the brief asks for, and which artifacts constitute the deployment as a product decision, plus the brief's own dispatch/belt exclusions. Also recorded a coordination consequence nothing else in the note captured: if slice 4 adds a .socket member AND slice 2 has made membership non-degenerate, that member needs the same bundle as its siblings (identity, content-sensitive value, ownership stance). Neither gates the other, so the §5 dependency graph is unchanged — but whichever lands second inherits the join, and it should not be discovered then. Verified: orphan and dangling-link witnesses green. Doc-only change. * Socket activation does not meet the handback: in-flight fetches die (review 45291) The best finding on this PR — a substantive design defect, not bookkeeping, and correct. The backlog holds only connections that have NOT yet been accepted. A fetch the old process already accepted dies with the process: client sees a reset, the browser's fetch rejects, and it lands in exactly the .catch arm this ticket exists to quiet. Verified in the seed rather than reasoned about: - handle_serve installs NO SIGTERM handler (grep SIGTERM in cli_run.rs: nothing); - the only SIGTERM machinery lives in phase_profile, is gated on profiling being enabled, and even then calls std::process::exit(143) after flushing — it does not drain; - so systemctl restart -> default SIGTERM disposition -> immediate termination mid-request. Exposure is small per deploy (roughly request-duration / 2s poll of viewers are mid-flight at the restart instant) but nonzero, and across ~40 deploys/day it will fire. The brief's handback is "a deploy run against a live viewer with no visible interruption", so a rare banner still fails it: socket activation ALONE does not meet the acceptance bar. Three consequences recorded: 1. §3 states the limitation and names the fix — a SIGTERM drain: stop accepting, finish in-flight, exit within TimeoutStopSec so a hung request cannot stall the deploy. 2. §6's handback control now says explicitly that it is NOT established by socket activation, is a control on slice 4 AS A WHOLE, and must be narrowed to "no banner for connections initiated after the restart began" if the drain is out of scope — a weaker promise than the brief asked for, flagged as such rather than quietly delivered. 3. §7 q4 widened: the seed seam is THREE things, not one — LISTEN_FDS (inherit the listener), sd_notify (honest F1 readiness), and the SIGTERM drain (graceful handover). Answering no forecloses all three, so slices 3 AND 4 both lose their route, not just socket activation. Slice 4 in §5 updated to carry the drain as required rather than polish. Verified: orphan and dangling-link witnesses green. Doc-only change. * WIP: server deploy untangling --------- Co-authored-by: Brian Searls <briansearls1@gmail.com> * Exclusive cost partition + selected-set closure overlap (Lane B slice 1, measurement only) (#7483) * WIP: Lane B * Exclusive cost partition + selected-set closure overlap (measurement only) Lane B slice 1, subject entry-graph-union-construction. No union implementation, no eviction/retention change, no walk_memo or #6999 memo fork. A. The resolve-split counters could not be quoted as shares because the children and the parent are drawn from DIFFERENT UNIVERSES, not because they nest. ResolveStageNanos accumulates over every resolve the thread runs -- witness entries and machinery entries alike -- while the receipts printing it quote a parent covering only one of those sets. Executed receipt: a single-entry claim_batch reports load=48468ms against a 45308ms parent, and the span account shows why -- two top-level resolves ran (the witness entry plus dag/gunbc/output_policy.dag), so the rows summed 65.3s of spans against a 41.0s denominator. ResolveSpanAccount adds the one window that contains every stage row by construction, and exclusive_cost_partition reports against it. The law parent == sum_exclusive + remainder holds by construction (remainder is derived, tolerance 0ns); what makes it non-vacuous is that it refuses -- OverAttributed, NestedSpanAttribution, NoSpans -- instead of clamping, which is the shape the existing saturating_sub `other=` row uses to hide exactly this condition. share_of_parent returns None unless Reconciled. Basis is named and additive: summed top-level resolve span nanos, thread-sequential. Elapsed wall is not additive over concurrent worker spans, so it is carried under `observations` and never partitioned. assembly_rewire's three sub-passes are carried as explicit inclusive rows and never enter the exclusive sum. B. measure_selected_closure_overlap composes the production machinery -- discover_floor_witness_roster, the floor_diff_observe unified and name-status observations, entry_eligible_for_discovery_skip_before_resolve, and collect_both_closure_module_names_for_entry -- so the measurement reads the floor's own selection rather than a parallel hand-written model. It resolves and typechecks nothing: the output is an upper bound on repeated module membership, not a wall-time saving. A selector or diff-observation refusal propagates rather than widening to measure-everything. Both probes carry the same dissolution trigger as ResolveStageNanos: a .dag PerformanceReceipt carrier consumed by a floor witness. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Discriminating controls for the accounting law and the overlap arithmetic Ten controls, green by execution, plus a mutation proving they refuse. The law holds by construction, so the tests that carry weight are the ones that make it fail. Disabling the OverAttributed arm (the saturating_sub shape that hid this condition in the first place) turns exactly refuses_over_attribution_instead_of_clamping_to_zero and json_marks_a_refused_partition_unquotable RED and leaves the other four green -- so the controls discriminate rather than merely pass. Each refusal arm has an input reaching it (OverAttributed, NestedSpanAttribution, NoSpans), and every refused state asserts share_of_parent == None: a share quoted off a non-partition is the fabricated plausible output DESIGN §5 forbids. The rewire sub-rows get a double-count control fixing them as inclusive. The overlap arithmetic pins both degenerate poles, including the one that would CLOSE the union program (fully disjoint closures -> factor 1.0, upper bound 0) and the empty selection that must report null rather than let 0/0 become 1.0. Executing them caught a real arithmetic error in the percentile control's own expected values (3+2+1+2 = 8, not 7) -- the implementation was right and the test was wrong, which is the direction that only execution can tell apart. measure_whole_tree_resolve now emits the partition too. It runs the monolithic compile_to_resolved path, which fills no stage row and opens no resolve span, so it refuses with NoSpans -- making "this probe carries no stage attribution" an executed receipt rather than a prose claim. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * WIP: Lane B * Give both probes a §7 HAND-RUST scaffold receipt (codex review 45272) REQUEST_CHANGES was correct: this file has an established SCAFFOLD (§7 HAND-RUST — <marker>) convention -- ROADMAP lane, Unblock, an explicit DELETE WHEN list, a greppable receipt, and a declaration test -- and a generic "a .dag PerformanceReceipt carrier" trigger is not that. Both scaffolds now carry the full block. A (cli_run_exclusive_cost_partition_probe) names the concrete lane the ResolveStageNanos rows it partitions already declare: ROADMAP §2 Minimal work — caching by realization / realization-measurement-loop.md Phase 0, dissolving when compute_fabric.PerformanceReceipt keyed by cache-subject hash rolls into CostAccount.time = Measured and a floor witness consumes it. It adds no second measurement authority; it makes the existing rows' denominator honest. B (cli_run_selected_closure_overlap_probe) is typed as a ONE-SHOT INSTRUMENT with an explicit deferral: delete when the slice-2 union verdict is taken, WHICHEVER WAY IT GOES -- if the program proceeds its own receipts supersede this, and if it is shrunk or closed the probe has discharged its purpose. A standing closure-overlap reader belongs in v2.lens.affected_set over the containment tree, not in seed Rust, so this deliberately does not become permanent host-side machinery by default. The receipt lines report their real hit count instead of inheriting the convention's error: both older markers in this file claim `== 1` and actually sit at 5 and 4 hits, so a copied claim would have been false on arrival. What the receipt checks is that the marker reaches 0 at deletion, not a fixed count. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Measure over the floor's corpus, not the probe's narrower one The probe defaulted its exclusions to whole_tree_probe_exclusion_substrings, which is the floor's witness_exclusion_substrings UNION the whole-tree strict-resolve exclusions. That is the right list for a whole-tree RSS probe and the wrong one here: it made the roster 45 entries against 579 *_test.dag files under the same scan dirs, so the overlap statistics were being drawn from roughly 8% of the corpus the floor actually selects over. A subject drawn from 8% of the corpus cannot answer a question about the corpus, and the failure is invisible in the output -- every derived quantity is internally consistent and simply describes a different, much smaller population. Defaulting to gunbc.ci_layer_roots.witness_exclusion_substrings (the floor discovery authority, the same list run_discovery_corpus passes) puts the measurement on production's population. Caught by checking the reported roster size against the corpus rather than against the receipt's own internals. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Receipt: exclusive attribution + selected-entry overlap, and the verdict Both halves measured, machine-readable receipts stored beside the writeup. A. Exclusive partition reconciles (tolerance 0ns, remainder 55.1ms of 73158.3ms). load is 68.2% of resolve-span time, typecheck_compute 24.4%, everything else 7.4%. Machinery is 37.7% of all resolve-span time even in a single-entry run. The load-bearing detail: load IS the closure walk, and its inner scan referenced_module_paths_in_text is a full-content byte scan run once per (entry, module) pair with no memo -- so B's duplication factor is not an abstract ratio, it is the multiplier on the dominant cost. B. Three real subjects from already-known main commits. Duplication factor 35.9 / 38.4 / 38.3 across 3 / 13 / 29 changed paths -- stable across a 10x range of diff breadth, so overlap is a property of the corpus shape, not of the diff. 97.2-97.4% of closure memberships are repeats. The union is nearly saturated at the narrow subject: N grows 37% while the union grows 15%. Max fanout is ~N in every subject; the median module is rare and falls as N rises, so the shape is a universal std core plus a long private tail. Verdict: STRENGTHENS the premise and RELOCATES the prize. The pole that would have closed the program (disjoint closures, factor 1.0) is decisively absent. But the prize is in load, not typecheck -- typecheck_compute is already content-key memoized through typed_module_cache, so a union justified as "typecheck once" would buy something largely already owned. And because the repeated unit is a pure function of source content, a per-source memo keyed on content hash would collapse the same 35.9-38.4x on the scan portion with NO union graph. Slice 2 should price that rival before committing. Recorded as a finding, deliberately not implemented -- this deliverable is measurement. resolution_divergence_census is kept separate as instructed: it runs as its own binary, so its closure-scoped resolve is a different process that an in-process union cannot displace. The receipt also records a fidelity defect caught mid-measurement: the first run's probe exclusions produced a 45-entry roster against 579 files, and every derived quantity was internally consistent while describing 8% of the corpus. Invisible from inside the receipt; caught only by checking the roster against the corpus on disk. Those numbers are withdrawn. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * WIP: Lane B * chore: regenerate drifted generated artifacts (ci auto-heal) * Cite the receipt from the DESIGN authority, not the projection My previous fix edited DESIGN.md directly and the CI auto-heal bot reverted it in 9d63c7318d -- correctly. DESIGN.md is a GENERATED artifact (gunbc.generated_artifact DesignArtifact -> gunbc.design_document expected_design_md), so a hand edit to it is a change to the projection while the authority still says otherwise, and the drift gate regenerates it away. The authority is dag/gunbc/design_document.dag. That is the same shape DESIGN §5 names from the other side: a check satisfied by editing the declaration while the realization lies. Here the realization was edited while the declaration lay, and the healer is what made it observable rather than silent. The citation now lives in design_document.dag and DESIGN.md is regenerated from it via the declared regenerator (main_wet on dag/tools/generated_artifact_gate.dag), so the two are a fixed point. Verified by execution before push: doc_graph_has_no_orphan_docs on both entries, doc_graph_is_clean, and the drift witnesses witness_committed_is_fixed_point, witness_committed_fixed_point_red_control, witness_all_known_committed, witness_registry_complete all pass. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * WIP: Lane B * RETRACT three claims this PR asserted; measure what load actually is Operator review point 1 (repeat the partition) and my own sub-attribution falsified three claims. They are retracted in the receipt and in the DESIGN authority rather than edited out, because how they failed is the reusable part. RETRACTED 1 -- "load is dominated by referenced_module_paths_in_text, an unmemoized per-(entry,module) content scan." Measured: 3.9-23.0ms, ~0.0% of load. It was inferred from reading the call path and never measured -- the §5 specification-without-execution trap, committed while writing about it. The missed step: load_sources_for_entry_with_pool calls load_sources_for_entry_with_index AND THEN extend_sources_to_both_closure_fixpoint, which the first instrumentation never timed. RETRACTED 2 -- "load is the dominant cost." True at 67-68% on a 159-module closure; FALSE at 38-40% on a 504-module one, where typecheck_compute is ~50%. Run-to-run within an entry is stable (67.0/68.0, 37.9/39.5), so the partition is sound and the generalization was not: it came from one run of one entry. RETRACTED 3 -- the A x B join and the per-source content-hash memo that followed from it. Both depended on claim 1. MEASURED INSTEAD: load is ~100% build_both_closure_edge_index, a CORPUS-wide edge index memoized per MultiEntryIndex at ~25.6s per index, INDEPENDENT of the entry's closure size (159 and 504 module closures pay the same). So it is fixed per index -- not per entry, not per membership. The claim_batch harness pays it twice only because two indices exist on that path (its own build_multi_entry_index plus process_shared_index for machinery). THE BOUND THAT MATTERS: because the dominant row is a fixed per-index construction, every share in section A describes a fixed-cost-dominated harness, NOT the floor, where one index amortizes across hundreds of entries. The verdict is therefore "not answerable from this data" rather than the strengthens-and-relocates claim it previously carried -- a union program justified by these shares would be justified by an artifact of the instrument. The deciding measurement is a partition from the claim_executor discovery path: wired in this PR, and never run. B's membership numbers are unaffected -- they are counts, not timings, and the disjoint-closure pole that would close the program outright is still decisively absent. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Fix three positional citations, one of which pointed at nothing review 45321 asked for symbolic citations in place of line ranges. Verifying the three sites found that one was not merely fragile but wrong: compute_fabric.dag:414-423 — that file is 139 lines. PerformanceReceipt is not in it at all; it lives in gunbc.fleet_intent. The field list was wrong too: `wall_duration` is not a field, the time axis is `cost: CostAccount<Nano>`. Corrected to name the real symbols: gunbc.fleet_intent.PerformanceReceipt, its roll-up fn cost_account_from_performance_receipts, and the std.realization_schedule.CostAccount / CostBasis it feeds — all verified present. The other two (realization_schedule.dag:25-26,33-39 and cli_run.rs:2062) resolved correctly; ranges dropped since the symbols were already named. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Register measure_selected_closure_overlap in the explicit bin roster It was the only one of 31 bin files without a [[bin]] entry. Cargo auto-discovers it (edition 2021, autobins defaults true) so it built and ran, but matching the surrounding convention costs nothing and removes the discrepancy. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * The A.7 table quoted an unretained run; the committed fourth receipt refutes it Operator review point 1 asked for >=2 entries x >=2 runs showing the share ordering holds. It does not hold, and the previous table hid that by quoting figures from a run set that was never committed. Real committed receipts, all four: ci_floor_measurement r1 parent 75.2s load 51.24s/68.11% tc 18.48s/24.57% ci_floor_measurement r2 parent 66.4s load 44.96s/67.68% tc 16.57s/24.95% generated_artifact_drift r1 parent 131.0s load 50.98s/38.93% tc 65.56s/50.06% generated_artifact_drift r2 parent 155.7s load 77.11s/49.52% tc 64.55s/41.46% The ordering flips between two runs of the SAME entry (drift r1 typecheck leads, r2 load leads), so the earlier "inverts across entries" reading was an artifact of comparing two runs that happened to agree. What survives is in the absolute columns: typecheck_compute is stable per entry and scales with closure size (18.5/16.6s at 159 modules vs 65.6/64.6s at 504), while load does not track closure size at all (51.24s vs 50.98s) and its magnitude swings 44.96-77.11s across runs. Corpus-fixed and noise-dominated. Confound disclosed: these runs shared the host with concurrent cargo builds. Retraction (b) is itself corrected here rather than silently replaced -- its "false at 38-40% on a 504-module closure" replacement rested on the same unretained run set. Adds cost-partition-generated_artifact_drift-r2.json so every quoted figure has a committed receipt behind it. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * State B's weighting, and redo it byte-weighted Operator review point 3: the overlap figures carried an unstated uniformity assumption -- every membership counted as one regardless of module size. Stated: the B table is module-count weighted. Redone byte-weighted on the same subject, same selection (roster 809 / selected 316 / skipped 493, identical to the committed typical receipt): duplication factor 38.42 by count -> 47.92 by bytes (+24.7%) repeats as share 97.40% -> 97.91% union 1,243 modules -> 11.45 MB of 548.90 MB summed The count-weighted figure was the conservative one: high-fanout modules are systematically larger than average, which is consistent with the universal core being std.algebra / std.types / std.error_primitives rather than small leaves. This moves the weighting in the direction that favours the union program, and the section says explicitly that it does not rescue it -- A.7 is why no membership count here converts into a displaced cost. It is a better-weighted upper bound, not a different kind of claim. Receipt: closure-overlap-typical-byte-weighted.json. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * WIP: Lane B * Measure the amortization: load is per-index, so the union program loses its target A.7 said load's share on a floor run "must be smaller -- by how much is unmeasured." Measured here on the explicit-entry path, which puts N entries against ONE shared index with everything else held fixed: N=1 (2 spans) N=6 (7 spans) growth parent 69.97s 114.12s 1.63x load 47.44s 51.32s 1.08x load_bare_edge_index 47.40s 51.18s 1.08x typecheck_compute 17.34s 49.64s 2.86x parse 1.14s 3.66s 3.21x resolve_modules 0.02s 0.11s 4.40x load share of parent 67.79% 44.97% Entry count rises 6x and every per-entry row rises with it; load rises 8%, which is inside the noise band already established for that row. load is paid once per INDEX, and the existing per-index memo already amortizes it. The N=1 run reproduces the discovery-path receipts (67.79% vs 68.11/67.68%), so the explicit-entry path measures the same thing. THE REDIRECTION: a union graph cannot displace a cost that is already paid once, so the program's apparent target -- the row that dominated every single-entry partition at 67-68% -- is eliminated, not merely unproven. The only measured row scaling with both entry count and closure size is typecheck_compute, whose unit of work is module membership. That is the only surviving candidate and it is NOT established: converting repeated membership into repeated computation needs per-entry typecheck attribution against a shared env, which nobody has measured. The duplication factor must not be quoted as a multiplier on typecheck time. Projection to floor-scale N is marked as a projection, not a receipt (two points, six small entries). Whole-corpus floor runs OOM-killed twice (exit 137, at 1,513 and 1,046 entries) including under GUNBC_MEMORY_BUDGET_BYTES=44GiB, which governs realization admission rather than resolve-pool retention. Also completes the byte weighting across all three subjects (43.04 / 47.92 / 49.25 against 35.89 / 38.42 / 38.27 by count) and corrects B.1 read 1: "stable across breadth" holds by module count but not by bytes, where the factor rises monotonically. Receipts: cost-partition-amortization-n{1,6}.json, closure-overlap-{narrow,broad}-byte-weighted.json. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Fix a control this PR broke, and make it assert the invariant instead of a count rewire_sub_rows_are_inclusive_and_never_enter_the_exclusive_sum asserted p.inclusive.len() == 3 -- a count over EVERY inclusive row, not just the rewire ones. Adding the load_* sub-attribution earlier in this PR took that to 10 and turned the control red. It went unnoticed because the rust suite was removed from CI on 2026-07-11 and runs locally only. Two changes: - Filter to contained_in == "assembly_rewire" and assert those three rows account for all 300ns of the parent. A global count makes this control fail whenever an unrelated row gains a sub-row, which is exactly what happened. - Add the invariant the count was standing in for: every inclusive row names a parent that is itself an exclusive or inclusive row, so it is already counted and can never be attributed to nothing. Proven to discriminate by mutation -- repointing load_bare_edge_index at a nonexistent parent goes red with the located diagnostic, and only that test. Also corrects InclusiveCostRow.contained_in's doc comment, which claimed the parent is always an exclusive row. It is not: load_bare_edge_index nests under load_bare_reference_closure, which nests under load. 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> * WIP: PR #7485: does identity coercion (node already inhabits the target model * Separate identity admission from semantic grounding * Tie identity admission to target model authority * Revert "Merge remote-tracking branch 'origin/main' into agent/identity-coercion-grounding" This reverts commit 64bf6c2b6050e0435592c868489fbc06b1fd94b3, reversing changes made to 3d177ac304852224852c03d588495d0df56d1572. * Repair #7490: stale v1-compiler-tests callers + compile gate (#7494) * WIP: repair 7490 * Repair #7490 fallout: fix stale typecheck_module callers and enroll compile gate. PR #7490 added global_variant_base to typecheck_module but left four v1-compiler-tests integration callers stale; main would not compile that crate. Wire the seventh argument (empty_map for incremental helpers; global_bare_variant_locals in the receipt test) and add a build-job cargo check -p v1-compiler-tests --tests step so future signature migrations cannot land without compiling direct Rust test call sites. Co-authored-by: Cursor <cursoragent@cursor.com> * Fix CI compile gate: drop unused import under -D warnings. The new v1-compiler-tests compile check runs with RUSTFLAGS=-D warnings; module_authority_resolution_test.rs had a stale diagnostic_to_message import. Co-authored-by: Cursor <cursoragent@cursor.com> * Fix witness parse error: replace invalid `..` rest pattern in match. The .dag parser rejects RunStep { run: cmd, .. }; use explicit field patterns like ci_heal_job_witness_test.dag. Co-authored-by: Cursor <cursoragent@cursor.com> * Address review 45392: scaffold compile gate on cargo.Build.Check authority. Add extdeps.cargo_build.Check, move the build-job step to ci_v1_compiler_tests_compile_gate_emit with Disposition=Scaffold + dissolve-on marker in the emitted script (same class as ci_release_build_script), and enroll scaffold/dissolve witnesses. Co-authored-by: Cursor <cursoragent@cursor.com> * WIP: repair 7490 * Fix CI: parse error in HAND-RUST witness and typed CARGO_BIN emit. The regen/heal jobs failed because v1_compiler_tests_typecheck_module_callers_hand_rust_witness_test.dag split == across lines (parse error). Route CARGO_BIN through ShellExecutablePosition HostEnvVar on BoundOperationInvocation so effect_plan_bash_materialize emits via bash_build_word_var instead of post-processing emitted shell strings; regen ci.yml for grammar-quoted argv. Co-authored-by: Cursor <cursoragent@cursor.com> * WIP: repair 7490 * Address review 45415: move executable override to Bash layer. Revert ShellExecutablePosition from v2.std.operation_argv BoundOperationInvocation; add BashBoundOperationInvocation wrapper in effect_plan_bash_materialize with bash_bind_operation_invocation_host_env_executable for CARGO_BIN grammar emission. Keeps operation intent (ref + bindings) transport-agnostic per DESIGN §3. Co-authored-by: Cursor <cursoragent@cursor.com> --------- Co-authored-by: gunbc-ci-auto-heal <gunbc-ci-auto-heal@users.noreply.github.com> Co-authored-by: Cursor <cursoragent@cursor.com> * Stop re-walking the string to read one character (Lane A: process_escapes_loop onto source_chars) (#7491) * WIP: Lane A * WIP: Lane A * Count the escape receipt as v1 seed growth with a dissolution trigger Addresses review 45369. The cited hand-maintained stage0 ratchet does not reach a tests/ target, but the discipline point stands: the receipt is hand Rust in the v1 seed tree and was silent. escape_receipt_seed_growth_mark records what it carries, why it is not a .dag witness today (the resolve-count bump is operator-signed), and the two triggers that delete it. * Demote the escape cost separation to a non-gating benchmark Addresses review 45416. Gating correctness on wall clock can red correct code when the larger run is the one that catches contention. The three deterministic decode tests keep gating; the ratio test is #[ignore]d and runnable with --ignored. The on-carrier mark and the lane doc now say which half gates, why the deterministic-counter alternative lands non-gating too, and that the durable guard for this class is a structural lens. --------- Co-authored-by: Brian Searls <briansearls1@gmail.com> * Require canonical shape for literal grounding * Revert "Merge remote-tracking branch 'origin/main' into agent/identity-coercion-grounding" This reverts commit a7c3ef1b33ee457f19b8906630e2cfe03ab20e4c, reversing changes made to 56460cc48722818f9274d01f94210b7d38aa0165. * WIP: PR #7485: does identity coercion (node already inhabits the target model --------- Co-authored-by: Brian Searls <11205878+briansrls@users.noreply.github.com> Co-authored-by: Claude <noreply@anthropic.com> Co-authored-by: Brian Searls <briansearls1@gmail.com> Co-authored-by: gunbai-bot[bot] <289086189+gunbai-bot[bot]@users.noreply.github.com> Co-authored-by: gunbc-ci-auto-heal <gunbc-ci-auto-heal@users.noreply.github.com> Co-authored-by: Cursor <cursoragent@cursor.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> Co-authored-by: gunbai-bot[bot] <289086189+gunbai-bot[bot]@users.noreply.github.com> Co-authored-by: Brian Searls <11205878+briansrls@users.noreply.github.com> Co-authored-by: Brian Searls <briansearls1@gmail.com> Co-authored-by: Cursor <cursoragent@cursor.com>
* WIP: p0 - protect the live system
* Refuse an unresolved method instead of inheriting the receiver type
An unknown method reached `method_pipe_map_keys_values_fallback`'s else-arm,
which returned the RECEIVER's type with an empty diagnostic list. So
`xs |> filter_map(..)` on a `List<Int>` typed as another `List<Int>` — a
success-shaped answer that survives a whole collection pipeline and looks
plausible to downstream inference, with the expression stamped
`PlainMethodSemantics` as if it had resolved. Nothing refused until the
interpreter hit its closed dispatch default and returned
`InterpError::Unimplemented { what: "method 'filter_map'" }`: whole-tree
compile reported zero blocking errors while live dispatch returned HTTP 500
(#7479).
That arm is deleted. Method absence is now decided at compile time and split
into the two states it actually has (DESIGN §5 — state-space conflation):
MethodNotFound receiver type fully resolved, so the method is
PROVABLY absent — the decidable refusal.
MethodExistenceUndecided receiver under-resolved (type variables present),
so absence cannot be proven — a typed, located,
COUNTED frontier refusal, never a silent widen
back to `recv_rt`.
Both arms return `error_type`, not `recv_rt`: `node_type_compatible` treats
`error_type` as compatible with everything, so one located refusal does not
cascade into derived mismatches at every downstream consumer.
Green by execution, with the controls:
xs |> deliberately_nonexistent_method() RED, names method + receiver type
xs |> filter_map(x => x) RED — the literal #7479 incident
xs |> filter(..) |> map(..) GREEN — algebra templates resolve
at tier0 and never reach the arm
Rationale rides on the carrier (`method_existence_wall_note`) with its
dissolve-on: primitive-realization-single-authority, at which point existence
is decided against one PrimitiveDefinition identity rather than the
structural/service tier pair, and the Undecided frontier closes.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
* WIP: p0 - protect the live system
* Decide method existence and declared-type conformance at compile time
Two v1 fail-opens in the same shape: knowledge is missing, so the compiler
constructs a success-shaped answer and the lie surfaces at runtime.
METHOD EXISTENCE. An unresolved method fell through
`method_pipe_map_keys_values_fallback`'s else-arm, which returned the
RECEIVER's type with an empty diagnostic list, and the expression was stamped
`PlainMethodSemantics` as if it had resolved. So `xs |> filter_map(..)` on a
`List<Int>` typed as another `List<Int>` and survived the whole pipeline;
nothing refused until `InterpError::Unimplemented { what: "method
'filter_map'" }` — whole-tree compile green, live dispatch HTTP 500 (#7479).
The predicate deciding absence is the load-bearing part, and the two obvious
ones are unsound — both rejected on measured whole-tree evidence, not taste:
is_fully_resolved alone A type can carry no type variables and still be
an inference artifact. `NonEmptyStr` (declared
`String where non_empty`) arrives as
Product(NonEmptyStr) instead of peeling to its
String base, reding 8 correct `.length()` sites
in extdeps/filesystem/linux.dag while the
identical `text.length()` in extdeps/mercurial
stays green; a coproduct payload bound by
pattern destructuring arrives typed
Primitive(ok) and reds a correct `list_push`.
the receiver algebra profile free_monoid_scalar_templates omits `count`
while the interpreter dispatches it natively,
so `String.count()` reds against a profile the
runtime contradicts — the five-way primitive
fork, measured.
Fabricating a refusal is the mirror image of the fabricated success being
deleted, so the predicate is composed of two declared authorities rather than
one minted here: refuse when the name is absent from `std.methods`
declared_method_names AND the receiver is fully resolved. The roster answers
"is this a substrate method at all"; the receiver gate answers "could this be
a product field holding a callable" — exactly the legitimate
`LexMatchThunk { apply: fn(s) }` idiom in v2's tokenizer, whose 7 sites would
red without it. Whole-corpus verdict: zero false positives, and a second real
latent defect caught beside #7479 — `env.clone()` (05_emit_rust.dag:9009,9831),
a Rust-ism with no .dag definition and no interpreter arm, fixed here.
The undecidable residue is `MethodExistenceUndecided`: typed, located and
COUNTED but non-blocking (the is_error_diagnostic partition, UnlistedImportUse
precedent), so the frequency of the frontier stays observable rather than
zeroed by construction. Both arms return error_type, never recv_rt, so one
located refusal does not cascade downstream.
DECLARED-TYPE CONFORMANCE. infer_item passed the declared return into body
inference as `expected` but then kept the declaration's inferred return
regardless of what the body produced, so `fn f() -> Int { "wrong" }`
typechecked with zero diagnostics. Three positions now check against their
declaration — fn body vs declared return (both arms) and `data` value vs
annotation — through the EXISTING node_type_compatible, which is permissive by
design: an error type, type variable, or under-resolved shape answers
compatible, so the wall fires only where the mismatch is proven.
Green by execution. REDs: `deliberately_nonexistent_method`, `filter_map`,
`fn f() -> Int { "a string" }`, `data d: Int = "a string"`. GREENs:
filter/map/fold/flat_map pipelines, `String |> count`, `Int?` from `first`,
and the full [src/v1, dag] closure through regen.
Two upstream defects are named by the measurement and deliberately not fixed
here, each a promotion trigger that would let the wall decide more: a
where-refinement alias resolving to a Product instead of peeling to its base,
and a coproduct payload binding typed as the variant name.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
* Narrow the conformance wall to what it can actually prove
The method-existence wall landed sound. The declared-type conformance wall
did not: running it over the corpus found FOUR independent classes of correct
code that node_type_compatible reports as a mismatch, because it compares
names across representations it never peels.
optionality, two ways `-> String?` carries optionality in
return_cardinality while the body produces the
nominal Optional coproduct — 4 correct sites in
05_emit_rust.dag
brand aliases `Hash` is `ContentHash` is a branded String — 3
correct sites in dag_collect_support.dag, the same
class as NonEmptyStr arriving as Product(NonEmptyStr)
anonymous literals the corpus writes `[ { name: .., .. } ]` without
repeating the nominal type — 8+ correct rows in
dag/std/algebra.dag
cardinality location resolved_type() drops the declaration's optional
marker (fixed: the declared side now goes through
preserve_outer_optional_cardinality)
Each was found by RUNNING the wall, never by reasoning about it, and the list
is not known to be exhaustive — which is exactly why chasing them with
exemptions was the wrong move. Four ad-hoc carve-outs leave a wall that is
neither principled nor trustworthy, and fabricating a refusal is the mirror
image of the fabricated success the wall exists to delete.
So conformance uses the same predicate shape the method wall settled on:
positive establishment. Judge only when both sides are ground kernel scalars —
plain shape, Required cardinality, name in std.types kernel_type_set — because
then a name difference IS a real difference, with no alias, brand, container,
coproduct or cardinality representation in between. That admits the whole class
the report named and admits nothing it cannot prove. Everything wider is
UNJUDGED rather than silently passed: it is the wall's declared frontier, and
each class above is a promotion trigger carried on the carrier note.
Witnesses are enrolled and executing, not scratchpad probes:
method_existence_wall_witness and declared_type_conformance_witness in the
emitted compiler_tests, both green, both discriminating (the asserted
diagnostic lists were empty before the walls).
4 REDs deliberately_nonexistent_method · filter_map · fn f() -> Int
{ "a string" } · data d: Int = "a string"
8 GREEN filter/map/fold/flat_map pipelines · String |> count · Int? from
first · conforming returns and data
regen_stage0 --verify: regen_divergence_count=0 — committed stage0 matches a
fresh self-compile, so the seed is at its fixed point with both walls active.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
* WIP: p0 - protect the live system
* chore: regenerate drifted generated artifacts (ci auto-heal)
* WIP: p0 - protect the live system
* Restore the seed the auto-WIP commit stripped
7b0ecdd8ea ("WIP: p0 - protect the live system") captured my working tree
mid-experiment and committed it. The tree at that moment held a deliberately
reverted seed: I had checked out the pre-wall stage0 to run a CONTROL — to
establish whether the OOM in
module_grain_affected_decision_discriminates_under_wiring_perturbation was
caused by this PR or pre-existing. (It is pre-existing: the test is SIGKILLed
identically on the pre-wall seed with 101 GB free, consistent with the repo's
own "whole-tree resolve OOM risk in test harness" note.)
The commit therefore deleted the walls from the seed while leaving them in the
.dag authority: 300 deletions across v1_std_core.rs (both diagnostic variants),
v1_compiler_infer.rs (the composed predicate and the conformance gate),
cli_run.rs (the histogram arms), compiler_tests.rs (both witnesses), and
lib.rs (the std_methods module). That is the exact drift the regen gate exists
to catch, and it was pushed.
The seed is restored byte-identical to 2b4380df3c ("chore: regenerate drifted
generated artifacts"), the last state where authority and seed agreed.
Re-verified after restore, not assumed:
regen_stage0 --verify regen_divergence_count=0 — committed stage0 matches a
fresh self-compile
control matrix 4 REDs (deliberately_nonexistent_method, filter_map,
fn f() -> Int { "a string" }, data d: Int =
"a string"), 8 positive controls green
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
* Decide method existence per receiver, not per name (codex review 45327)
The review is correct, and confirmed by execution. Gating on membership in a
declared method-NAME roster admits any rostered name on ANY receiver, so:
fn g(xs: List<Int>) -> Bool { xs |> starts_with("x") } compiled clean
fn h(xs: List<Int>) -> String { xs |> to_upper() } compiled clean
Both landed in MethodExistenceUndecided, which is non-blocking, so
`emittable_graph` accepted them — a fail-open route to exactly the runtime
failure this P0 wall exists to remove. Worse, the diagnostic LIED about its
cause: it reported the receiver as "under-resolved" when
Container(List,Primitive(Int)) is fully resolved. I had also reported
`String |> count` as a passing positive control; it was passing through this
same hole and emitting an advisory, so that green was hollow.
The predicate is now PER-RECEIVER: refuse when kernel_profile_lookup returns a
profile for the receiver's canonical container kind. tier0 has already
consulted that profile's algebra templates and missed, so reaching this arm
with a kernel-profiled receiver PROVES absence from the receiver's complete
declared surface. Same authority tier0 reads; no second relation.
That predicate was blocked by ONE thing, and it is a real §3 fork now fixed
rather than worked around: the kernel profiles disagreed with the interpreter
about `count`. The interpreter dispatches "length" | "count" | "size" natively,
while free_monoid_scalar_templates (String) and partial_function_templates
(Map) declared only `length`. Measured over the whole [src/v1, dag] closure the
gap was exactly two shapes — String |> count and Map |> count (9 sites) — and
both profiles now declare `count`, mirroring their own `length` row. So those
calls resolve at tier0 and never reach the wall.
Non-kernel receivers stay Undecided, and refusing there WOULD fabricate: a
where-refinement alias arrives as Product(NonEmptyStr) rather than peeling to
String, a coproduct payload arrives typed Primitive(ok), and `apply` is a
product FIELD holding a callable (the LexMatchThunk idiom). Undecided now means
exactly one thing — receiver surface not established — instead of doubling as a
name-grain escape hatch.
The name roster added in the previous commit is deleted along with its
generated module and registry row: the per-receiver predicate does not consult
it, and an unused authority is dead scaffolding.
6 REDs deliberately_nonexistent_method · filter_map · starts_with · to_upper
· fn f() -> Int { "a string" } · data d: Int = "a string"
9 GREEN 0 diagnostics, not merely no MethodNotFound — incl. String |> count
and Map |> count, now genuinely resolved rather than fail-open
The witness carries the review's two cases as REDs, so a regression to a
name-grain predicate fails the test rather than passing it.
regen_stage0 --verify: regen_divergence_count=0.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
* Fix the missing list separator, and re-derive the seed after the main merge
TWO defects, one found by review and one by the merge.
MISSING SEPARATOR (claude review 45347, correct). The `count` row added to
`partial_function_templates` was not comma-separated from the `length` row
above it, so two record literals sat adjacent inside the list. Fixed.
The reason it survived is worth recording, because it is the same class this
PR is about: THE PARSER SILENTLY ACCEPTS A MISSING LIST SEPARATOR. Probed
directly — `[ { name: "a" }, { name: "b" } { name: "c" } ]` compiles with 0
diagnostics. So the malformed literal passed regen, a whole-corpus compile,
the fixed-point verify, and a 15-case control matrix without a murmur, and
`Map |> count` resolved green off it. No amount of execution would have caught
this; it took someone reading the diff. A grammar that accepts juxtaposed
elements cannot tell a two-element list from a three-element one, which makes
a dropped comma a silent semantic change — unowned, and named here.
STALE SEED AFTER THE MERGE. Merging origin/main brought #7481, which added
literal CR/NUL characters to dag/std/types.dag AND the emitter fix that
escapes them (\x0d / \x00, target-independent). The merge kept my side of the
seed, which predates that fix, so the committed stage0 could no longer emit
the .dag it is derived from: `regen_stage0 --verify` failed with "bare CR not
allowed in string" in a freshly emitted std_types.rs. Authority and seed had
diverged — precisely the drift the regen gate exists to catch, caught.
Re-derived by bootstrapping from main's seed (which carries the escaping fix)
and running the two-pass regen, rather than by hand-patching the seed.
Re-verified after both fixes, not assumed:
regen_stage0 --verify regen_divergence_count=0
control matrix 6 REDs; positive controls 0 diagnostics
witnesses method_existence_wall_witness ok,
declared_type_conformance_witness ok
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
* WIP: p0 - protect the live system
* Make the positive controls assert zero diagnostics (codex review 45357)
The review's second finding is correct: both witnesses filtered the green
module's diagnostics to the BLOCKING variant only (MethodNotFound /
TypeMismatch), so an advisory MethodExistenceUndecided passed unnoticed.
That is not hypothetical — it is exactly how I came to report `String |> count`
as a passing positive control when it was in fact resolving through the
non-blocking arm and emitting an advisory. The witness was structurally unable
to tell "this call resolves" from "this call does not resolve but the arm is
advisory", which is the whole distinction the wall turns on.
Both controls now assert `green_result.diagnostics.is_empty()` — no diagnostic
of any severity. A legitimate method that stops resolving, or a conforming
declaration that starts producing an advisory, now fails the witness instead of
passing it.
Verified: both witnesses green under the strengthened assertion, so the
positive controls demonstrably resolve rather than being admitted by an arm.
regen_stage0 --verify: regen_divergence_count=0.
The review's first finding — that MethodExistenceUndecided is non-blocking, so
emittable_graph still emits — is answered separately on the PR with the
measured site list, because the fix is not available in this PR: 7 of the
Undecided sites are the v2 tokenizer's own LexMatchThunk { apply: fn(s) }
idiom, so blocking today refuses the compiler v2 depends on.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
* Remove a foreign PR's Rust slice that a bootstrap checkout dragged in
Bootstrapping the seed required a compiler that could emit the merged .dag, so
I ran `git checkout origin/main -- src/v1/stage0/src/`. origin/main had
advanced past this branch's merge base (da37e37f9b) to b519142647, so that
path-scoped checkout imported the stage0 slice of #7483 ("Exclusive cost
partition + selected-set closure overlap") — its hand-maintained bins — while
leaving the rest of that PR behind.
The result was four files in this diff that are not this PR's work:
measure_selected_closure_overlap.rs (a new file, and orphaned — Cargo.toml at
this branch's base does not declare the bin, so nothing built it), plus edits
to claim_batch.rs, claim_executor.rs and measure_whole_tree_resolve.rs.
Half of someone else's merged change, presented as mine, is not something to
carry to review: it misattributes the work and it is a partial import whose
.dag half is absent. All four are restored to the merge base; main's own
versions land normally when this branch merges.
Caught by reading the diff surface after a reviewer's summary described "two
new measurement bins" I had not written — a reminder that a path-scoped
checkout against a moving ref imports whatever else has landed there.
Verified after the strip: cargo build clean, regen_stage0 --verify
regen_divergence_count=0.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
* WIP: p0 - protect the live system
* WIP: p0 - protect the live system
* Peel the refinement base so the wall DECIDES, and key the frontier on receiver shape
Two independent signals said the same thing about the (module, method)
frontier key: codex review 45398 found it as a fail-open (a NEW `apply` in
v2.compiler.tokenize inherited the pass on any receiver, so the note's claim
that no new fail-open could enter was false), and the first whole-corpus CI run
found it as an undercount — the roster was measured over the v1 self-compile
closure alone and seven sites in three unseen modules went red.
The larger finding is that the biggest "undecidable" class was never
undecidable. resolve_method_receiver_type short-circuits on connective == Conj,
and a where-refinement type IS a Conj, so `String where non_empty` reached
method lookup as Product(NonEmptyStr) and String's algebra profile was never
consulted. Peeling to the base moves 12 corpus sites out of the residue in both
directions at once: the correct `.length()` calls resolve, AND a method genuinely
absent from the base now refuses as MethodNotFound instead of resting in the
frontier. Widening what the wall can decide is the only move that shrinks the
frontier without fabricating either a success or a refusal.
codex review 45410 then caught that the first peel hand-rolled a SECOND walker
over the refinement shape while this note asserted it was "one traversal
authority, second consumer" — the prose claiming a property the code did not
establish. where_refinement_chain is now the one walk, with exactly two
consumers: predicate collection flat_maps over it, base peeling takes its last
link. The shape test is held once in is_where_refinement_type.
The residue is 13 sites in four shapes, each an upstream receiver-resolution
defect rather than a method-existence fact, and the frontier key now carries the
receiver shape as its third component — so a new call is refused unless it
reproduces the exact unestablished shape the row was measured on. The residual
widening (a second identically-failing call in the same module) is stated in the
note rather than claimed away; closing it needs the content-addressed occurrence
identity the namespace lane is landing.
Verified by execution: two-pass bootstrap + regen_stage0 --verify
(regen_divergence_count=0); the whole dag + src/v2 corpus compiles clean, which
is what proves the 12 peeled sites were DECIDED and not excused (their roster
rows are deleted); the wall witness gains a both-directions RED for the peel and
a control asserting each frontier key component is load-bearing.
Pre-existing and NOT from this PR, reported not fixed:
compiler_tests::rust_btree_set_ord_eligibility_requires_nominal_carrier_shape
fails here and at origin/main — rust_btree_set_element_ord_eligible,
rust_nominal_ord_type_eligible and the test body are all byte-identical to main,
so identical inputs to an identical pure function. The Rust suite was removed
from CI 2026-07-11, which is why it sits unnoticed.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
* WIP: p0 - protect the live system
* Reach the wall from every arm, and judge containers of ground scalars
Two review findings, both verified against the code and both real.
codex review 45430: the method-existence decision lived inline in the FINAL
else of method_pipe_map_keys_values_fallback, so an unresolved map_keys,
sorted_map_keys or map_values whose receiver is not a keyed collection took an
earlier branch and returned recv_rt with an empty diagnostic list — the identical
success-shaped fallback this PR deletes, preserved in the two arms that ran
before it. A wall reachable only from the default arm is not a wall. The
decision is now method_existence_decision, held once and called from all three.
codex review 45398 (second finding): the conformance gate required a plain
shape, so a List is not one, and a declared List<Int> whose body produced a
List<String> was indistinguishable from a conforming declaration. The widening
is the same positive-establishment argument rather than an exception to it — a
container of a ground kernel scalar has no alias, brand, coproduct,
anonymous-literal or cardinality representation standing between the two sides
either, so a difference in the element name is a real difference exactly as a
difference in a scalar name is. Keyed collections are deliberately NOT admitted:
the key and value axes need their own corpus measurement, and assuming the
element argument transfers is the move these notes refuse elsewhere.
Both controls were run against the PRIOR binary rather than reasoned about,
because a predicate that looks discriminating is exactly the artifact that isn't:
List<Int> |> map_keys / |> map_values exit 0 before, 2 located refusals now
fn f() -> List<Int> { ["a","b"] } exit 0 before, 2 located refusals now
Verified by execution: two-pass bootstrap + regen_stage0 --verify
(regen_divergence_count=0); whole dag + src/v2 corpus clean, which is the same
instrument that found the four conformance false-positive classes; both witnesses
green with the new REDs; compiler_tests 30 passed / 1 failed, that one being the
pre-existing rust_btree_set_ord_eligibility failure reported in the previous
commit (byte-identical to origin/main, Rust suite not in CI since 2026-07-11).
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
* WIP: p0 - protect the live system
* WIP: p0 - protect the live system
* Split the residue on a decidable line, and fix the instrument that hid 12 sites
The most transferable finding here is that the INSTRUMENT was wrong before the
wall was. This wall had been measured with `gunbc run --entry
dag/tools/generated_artifact_gate.dag`, which reaches only that gate's import
closure. It reported CLEAN while twelve real sites sat outside it, and they
surfaced from CI instead. The whole-corpus instrument is the compile-clean gate
CI actually runs — `gunbc compile --source-root dag --source-root src/v2
--target dag` — which resolves 1629 sources against 2740 indexed modules. A
narrow instrument reporting clean is indistinguishable from a wall that works.
What the wide instrument found, and what each turned out to be:
TWO REAL DEFECTS, caught by the container widening from the previous commit.
`pure_dag_seam_unreachable() -> Int { 1 / 0 }` is a divergent seam, and the simd
and wgsl FLOAT kernels declared `-> List<Float>` while returning `List<Int>`
from it. The declarations are the correct half — those are float kernels taking
List<Float> arguments. The bodies are unreachable, so nothing ever misbehaved,
which is exactly why this had to be caught by construction rather than by a
consumer. Fixed with a Float projection of the same seam, marked as one
duplication with a bottom-type dissolution trigger: a divergent expression has
no result type to project from, so typing it Int alone was a silent lie
wherever the enclosing declaration was not Int.
EIGHT MORE UNESTABLISHED RECEIVERS, which forced a better model rather than more
roster rows. A receiver with NO AUTHORED NAME is not weak evidence about the
method — it is no evidence about anything, because the receiver's own type was
never established upstream. That is a different judgment failure from "this
receiver has a surface and the method is not on it", so it now gets its own
typed, counted, non-blocking ReceiverTypeUnestablished keyed on the CAUSE (empty
authored name — a decidable test) instead of a row per site. It cannot hide the
case the reviews worried about, because a receiver that DID resolve never
reaches it. That collapsed the roster from six rows to four.
ONE SHAPE NOT FIXED, and the machinery for it deleted. A brand alias can also
arrive as a plain qualified LEAF, Primitive(std.types.NonEmptyStr), rather than
the refinement Conj the peel walks. Three head-resolution strategies were
implemented and measured — lookup_type_for on the node, lookup_type_by_name on
the qualified name, and on its last segment — and none recovered the refinement.
The machinery was deleted rather than shipped unproven, and the site is a
declared row that says plainly that the cause is not yet understood. Unproven
machinery that decides nothing is worse than a declared row that admits what it
cannot decide.
Verified by execution: whole-tree compile-clean 12 blocking diagnostics -> 0,
with 18 ReceiverTypeUnestablished + 4 MethodExistenceFrontierAdmitted counted as
advisories so both classes stay observable; two-pass bootstrap + regen_stage0
--verify (regen_divergence_count=0); compiler_tests 30 passed / 1 failed, that
one the pre-existing rust_btree_set_ord_eligibility failure byte-identical to
origin/main.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
* WIP: p0 - protect the live system
* Pin the ReceiverTypeUnestablished classification, and say what the evidence is
The behavioural evidence for this class is the corpus census — 18 sites
whole-tree, counted as advisories with the compile-clean gate at zero blocking
diagnostics — not a synthetic source. A synthetic reproducer WAS attempted, an
untyped lambda parameter inside a record-field fn, which is the shape the real
sites have; it produced no diagnostic at all, so it did not reproduce the shape
and is not asserted here as though it did. Recording the failed attempt beside
the control, because a witness that quietly asserts something weaker than its
comment claims is the same defect as prose asserting what code does not
establish — the one the reviews caught twice already in this PR.
What the control does pin is the classification, which is the part a later edit
could silently flip in either direction: blocking it fabricates a refusal over
18 correct sites, dropping it restores the #7479 silence. Both directions are
asserted against the three severity partitions directly.
Verified: regen_stage0 --verify (regen_divergence_count=0); wall witness green.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
* WIP: p0 - protect the live system
* Bound the anonymous-receiver admission on the roster (codex review 45459)
The finding is correct and the correction is worth stating precisely, because
the original reasoning was sound about one thing and wrong about another.
When a receiver has NO authored name, the wall cannot tell an existing method
from a nonexistent one — the receiver's own type was never established upstream.
That is true, and it is why refusing the whole class would refuse 18 correct
corpus sites. But it is a fact about DECIDABILITY, and I used it to justify
ADMISSION: every anonymous-receiver call was admitted on the cause alone,
non-blocking, which made every FUTURE such call green including one whose method
does not exist. Unbounded, exactly where existence is unknown. Counting a
diagnostic does not stop invalid code reaching the live system.
The two halves are now separated. The diagnostic still names the real cause —
ReceiverTypeUnestablished says the receiver's type was never established rather
than implying the method is missing, which is the review 45327 lesson. But
admission is gated on the same declared roster as every other unestablished
shape, keyed (module, method, "Primitive()"). The seven measured occurrences are
declared; a new anonymous-receiver call anywhere else REFUSES as
MethodExistenceUndecided. That is a ratchet that can only shrink, and blocking a
new instance of a known deficit class is the factory model, not an
inconvenience.
The gate is already covered by the existing witness: the perturbation loop
asserts, for every one of the 11 rows, that changing the module, the method, or
the receiver shape withdraws the admission.
Verified by execution: whole-tree compile-clean 0 blocking, with 18
ReceiverTypeUnestablished + 4 MethodExistenceFrontierAdmitted counted, so the
roster exactly covers the corpus and nothing is admitted that is not declared;
two-pass bootstrap + regen_stage0 --verify (regen_divergence_count=0);
compiler_tests 30 passed / 1 failed, that one the pre-existing
rust_btree_set_ord_eligibility failure byte-identical to origin/main.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
* WIP: p0 - protect the live system
* Make the frontier a ratchet: declare each row's occurrence count and refuse excess
codex review 45464: the (module, method, receiver_shape) key bounds WHERE an
unresolved call may live but not HOW MANY, so a second call in the same module,
on the same method, failing to resolve the same way, inherited the admission.
That is not hypothetical — the measured rows are not singletons.
v2.compiler.tokenize admits seven `apply`, extdeps.mercurial three `any`,
gunbc.scm_compatibility.mercurial three `map` — so a row admitting seven would
silently admit an eighth.
Each row now declares its measured occurrence count and a per-module fold
refuses the excess with a located, typed FrontierOccurrenceBudgetExceeded. The
comparison is observed > declared, NEVER observed != declared, and that
asymmetry is load-bearing: a narrower compile closure legitimately sees fewer
occurrences, so equality would red any partial build, while fixing a call
legitimately lowers the count and must never red. The budget can only be
exceeded, never undershot — it ratchets down for free and refuses upward
movement.
Why not a stable per-occurrence key, which would close this exactly:
std.occurrence_identity is the corpus authority for the concept, and its own
scope law forbids filename, SourceSpan, authored name, structural Node equality
and content hash as identity inputs, allocating OccurrenceId inside one
graph-scoped allocator. An allocator-assigned integer is not stable across
compiles and so cannot appear as a literal in a declared row. A per-occurrence
key is not merely unimplemented here — it is unavailable from the authority that
owns the concept, which is why the count is the strongest bound the substrate
currently supports. Dissolve-on: content-addressed occurrence identity from the
namespace lane, at which point rows key on the occurrence and the count deletes.
The control is exercised at the mechanism, not through a corpus compile, so the
boundary is exact: declared occurrences pass, declared+1 refuses AND that
refusal blocks, and zero occurrences never red.
On the hand-Rust question raised in review 45469: the cli_run.rs delta is 14
lines, all of them arms of two EXISTING total matches over CompilerDiagnostic,
forced by exhaustiveness once variants are added in .dag — remove them and the
seed does not compile. Hand-written function count is unchanged at 742 before
and after. No new host transport, capability, or carrier.
Verified by execution: whole-tree compile-clean 0 blocking with 18 + 4 counted,
so declared counts equal observed exactly; two-pass bootstrap + regen_stage0
--verify (regen_divergence_count=0); compiler_tests 30 passed / 1 failed, that
one the pre-existing rust_btree_set_ord_eligibility failure byte-identical to
origin/main.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
* WIP: p0 - protect the live system
* Check every explicit return against the declared type (codex review 45472)
Verified before fixing, and the finding was exactly right:
fn f(cond: Bool) -> Int { if cond { return "wrong" } 1 } exit 0
The wall compared only the body's FINAL inferred type. The block's value is the
trailing 1, which conforms, so the wrong-typed early exit was never compared
against anything. An early return is a second exit from the same declaration and
must meet the same declared type.
The first attempt threaded the check onto the `expected` already flowing into the
ExprReturn arm, and it did NOT work — measured, not assumed: a return inside a
statement-position `if` carries no expected type, so the probe still compiled
clean. Threading a declared-return field through InferScope would have reached
it, but that is ~14 construction sites across three files including the emitter.
The check is instead a post-pass at infer_item, which is local, needs no scope
change, and reuses declared_type_conformance_diags rather than minting a second
relation — so an early exit is judged by exactly the ground-kernel-scalar and
ground-element-collection discipline the trailing expression is judged by, and
widens with that gate rather than beside it.
Verified by execution: the probe above now refuses with a located
`expected 'Primitive(Int)', got 'Primitive(String)'`; whole-tree compile-clean
still 0 blocking, so no legitimate early return in the corpus reds; two-pass
bootstrap + regen_stage0 --verify (regen_divergence_count=0).
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
* Hold the frontier-occurrence key in the diagnostic authority (codex review 45476)
The occurrence-budget fold hand-rolled a match over CompilerDiagnostic inside
v1.compiler.infer, which put a second reader of the coproduct outside the
coproduct's own authority: adding a variant could leave the budget silently
blind to it, and two places would decide what a diagnostic means.
diagnostic_frontier_occurrence_key now lives in 00_core beside diagnostic_to_span
and diagnostic_to_message, and the budget consumes it. Only two variants carry an
occurrence against a row — MethodExistenceFrontierAdmitted names its receiver
shape directly, and ReceiverTypeUnestablished always arises from a receiver with
no authored name, whose shape renders as Primitive(), which is why that literal
is the key rather than a field on the variant. A new variant that should be
budgeted is added in that one fn, next to the variants it joins.
Verified by execution: whole-tree compile-clean 0 blocking with 18 + 4 counted,
unchanged, so the routing is behaviour-preserving; two-pass bootstrap +
regen_stage0 --verify (regen_divergence_count=0); compiler_tests 30 passed /
1 failed, the pre-existing rust_btree_set_ord_eligibility failure.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
* WIP: p0 - protect the live system
* Stop the return walk at lambda boundaries, and give the seed projection its receipt
codex review 45481, finding 1 — confirmed by execution before fixing:
fn apply_it(g: fn(Int) -> String, v: Int) -> String { g(v) }
fn outer(v: Int) -> Int { apply_it(g: x => { return "inner" }, v: v) 1 }
-> expected 'Primitive(Int)', got 'Primitive(String)'
collect_explicit_return_types recursed through ExprLambda, so a return belonging
to the LAMBDA's callable return type was checked against the enclosing
declaration. That is a fabricated refusal — the mirror image of the hole the walk
was added to close, and §5 forbids one exactly as it forbids the other. Every
callable boundary is a new declaration and its returns are judged against it. The
walk now stops at ExprLambda, which also means lambda returns are not yet judged
at all; that narrowing is stated on the note rather than implied, and it
dissolves when the walk carries each callable's own declared return.
The discriminating PAIR is now witnessed, since one direction alone proves
nothing here: the early return must refuse AND the lambda return must not.
codex reviews 45469/45481/45484, hand-Rust gate — receipt added in the gate's own
form, both on the carrier (v1.compiler.core compiler_diagnostic_seed_projection_note,
beside the coproduct whose extension forces the arms) and in the changed planning
artifact. It is an explicit deferral naming lane
(compiler-static-failure-closure) and ROADMAP row (hand-MAINTAINED Rust -> zero
at v2 self-host), with the argument that an exhaustiveness arm is a different
class from the gate's usual subject: the gate's other deferrals are decision
surfaces that COULD live in .dag and therefore owe their own schedule, while an
arm cannot live anywhere but the seed's projection of the coproduct and
disappears exactly when the seed does.
Checkable receipt: hand-written fn count in cli_run.rs is 742 at origin/main and
742 here; the diff is 13 added lines with zero `fn`. The 322 lines review 45484
attributes to hand-Rust in compiler_tests.rs are not hand-written at all — that
file is GENERATED, listed in gunbc.stage0_emit_model.generated_stage0_files and
emitted by regen_stage0 from src/v1/compiler_tests_rust.dag, so its growth is
witness text authored in .dag.
Verified by execution: both probes correct in both directions; whole-tree
compile-clean 0 blocking; two-pass bootstrap + regen_stage0 --verify
(regen_divergence_count=0); compiler_tests 30 passed / 1 failed, the pre-existing
rust_btree_set_ord_eligibility failure.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
* chore: regenerate drifted generated artifacts (ci auto-heal)
* WIP: p0 - protect the live system
* Make the budget a real ratchet, fix the witness arity, and make the seam diverge
Three findings, all correct, and one of them was mine to catch before review.
cursor review 45494 finding 2 — THE WITNESS DID NOT COMPILE. I changed
frontier_occurrence_budget_diags to take a locating module_span and did not
re-run the suite, so three call sites in the witness still passed two arguments.
Reading caught what I skipped running; the run would have caught it immediately
and I did not do the run. Fixed, and the suite is green again.
codex review 45491 — the ceiling did not ratchet. `observed > declared` let
seven shrink to six while the declared seven stood, so a seventh call could
return silently: a static limit, not a ratchet, and the note claimed the ratchet
anyway. My stated justification for the ceiling — that a narrower closure sees
fewer occurrences — was simply wrong about this check, which runs per MODULE:
every occurrence of a module's rows is present whenever that module is
typechecked at all, and a closure omitting the module never runs its rows. So
there was no partial-visibility case to protect and the asymmetry bought
nothing. The comparison is now equality, which removes the headroom a
reintroduction slips into: fixing a call reds until the declared count is
lowered. Both directions are asserted in the witness, since the under-count half
is what makes it a ratchet and is the half an author is tempted to relax.
cursor review 45494 finding 1 also flagged the equality as contradicting the
note. It contradicted the note because the note was stale, not because the code
was wrong — the note has been rewritten to describe what the code does and to
record why the ceiling reasoning failed.
codex review 45493 — `1.0 / 0.0` IS NOT DIVERGENT. Under IEEE-754 it is positive
infinity, not a trap, so the Float seam RETURNED and the kernels asserted
unreachable would have produced [+inf]. A fabricated plausible output, the exact
thing §5 forbids, introduced while fixing a different fabrication. Integer
division by zero traps; float division by zero does not, however similar they
look. The Float projection now forces the Int seam to evaluate in its condition,
so divergence happens before any Float is produced. Confirmed in the emitted
Rust: `if (pure_dag_seam_unreachable() == 0)` over `pub fn
pure_dag_seam_unreachable() -> i64 { (1 / 0) }`.
Verified by execution: two-pass bootstrap + regen_stage0 --verify
(regen_divergence_count=0); whole-tree compile-clean 0 blocking; compiler_tests
30 passed / 1 failed, that one the pre-existing rust_btree_set_ord_eligibility
failure byte-identical to origin/main.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
* WIP: p0 - protect the live system
* Count the unjudged conformance residue, and author the receipt where it survives
codex review 45500 — the conformance wall's unjudged branch returned an empty
diagnostic list, so an unproven declaration was byte-for-byte indistinguishable
in the output from a proven-conforming one: the absence of a check reading as
the presence of a proof. It now emits DeclaredTypeConformanceUnjudged, counted
and non-blocking, so the wall's frontier has a SIZE — 3005 declarations
whole-tree — a number that falls as the relation widens and is therefore a
prioritizable measure of the gap rather than an invisible one.
It fires only where the declared and produced SHAPES DIFFER. Identical shapes
have nothing to prove, and counting them would bury the signal under
declarations nobody doubts; the residue that matters is exactly the set where a
mismatch could hide.
codex review 45501 finding 2 — the HAND-RUST receipt had gone stale, reading
five variants and 13 lines after a sixth variant landed. That made the receipt
itself the stale-prose defect it exists to prevent. Corrected to six variants
and 18 lines, with both figures now marked as re-derived from their two commands
on every variant addition rather than carried forward.
AND THE RECEIPT WAS IN THE WRONG FILE, which is why it vanished: I had written it
into docs/plans/compile-clean-forcecheck.md, and that .md is a GENERATED
PROJECTION of dag/gunbc/plans/compile_clean_forcecheck.dag — the CI auto-heal
commit regenerated the doc and silently reverted it. The receipt is now authored
in the .dag plan authority and survives the heal, which is verified by running
the generated-artifact gate and seeing the text reappear in the projection. The
plan carrier says so in-place, so the next author does not repeat it.
review 45499 — the count/length pair on the algebra templates is a §3 nicknaming
fork RECORDED rather than introduced, and the row now says so. The fork's
authority is the interpreter, which dispatches length, count and size to one
native arm and predates this change; the templates listed only length, so
`String |> count` resolved at runtime with no declared row, which the
method-existence wall exposed the moment it began proving absence from the
roster. Reconciling the declaration to the runtime is the honest direction —
inventing a distinct meaning for count would be the fabrication, and dropping the
row would refuse a working call. Dissolve-on: one name across the interpreter
arm, the templates, and the corpus, which is a corpus-wide rename and its own
lane.
Verified by execution: whole-tree compile-clean 0 blocking; two-pass bootstrap +
regen_stage0 --verify (regen_divergence_count=0); generated-artifact gate green
with the receipt present in the projection; compiler_tests 30 passed / 1 failed,
the pre-existing rust_btree_set_ord_eligibility failure.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
* WIP: p0 - protect the live system
* WIP: p0 - protect the live system
* Ground filesystem_read's return type; count the residue the gate was not counting
CI red on the last push was my own wall firing on a site my instrument never
reached, and chasing it found three defects underneath it.
ROOT CAUSE. filesystem_read was registered in 04_method as a bare
type_variable_node, so `filesystem_read(path: p).content` established nothing:
the field lookup had nothing to look in and the result was a fabricated
Primitive() carrying no name. A later `.split` on that value was then accepted
with no judgment behind it — #7479's exact shape one layer down, surviving
because the interpreter dispatches split on the native String regardless, so
nothing ever failed loudly. The return type was never unknown: runtime_rust.dag
already emits `pub struct FilesystemReadResult { pub content: String }`.
Declaring it makes the seed's struct and the compiler's type one fact instead of
two, via a make_kernel_record_type helper that builds the same
Conj-with-named-children shape lookup_field_type_node already walks for authored
records — so the kernel path and the authored path cannot drift.
WHY MY INSTRUMENT MISSED IT, WHICH IS THE MORE USEFUL FINDING. Whole-tree
compile-clean reported zero blocking while this site sat outside its closure;
the discovery corpus resolves entries compile-clean never opens. That is the
SECOND time this lane's instrument was narrower than the wall it was measuring —
the first was main_wet hiding twelve sites. The measurement was wrong before the
wall was, both times.
THE RESIDUE WAS NOT ACTUALLY COUNTED. compile_clean_diagnostic_is_advisory is a
CLOSED ALLOWLIST, not the complement of is_hard, so all three non-blocking
variants this lane adds matched neither predicate: they rendered to the terminal
while every count the gate reported read zero for them. I had been telling
reviewers the frontier was counted, and the population figures I quoted came
from grepping log text — no mechanism in the repository counted them. Found by
executing the gate before and after the expansion fix and seeing its advisory
total sit unchanged at 4590 while the printed population halved. The three
variants are now in the allowlist; the total moves 4590 -> 6176 and nothing
falls through either counter.
THE FRONTIER WAS REPORTED AT NEARLY TWICE ITS SIZE. Measured, 1436 of the 3005
unjudged conformance pairs were one type compared against ITSELF at two
expansion depths — a declaration naming T against a body producing T's expanded
body (203 Node, 173 Outcome, 46 Witness, 43 Optional, 38 PipelineStep, long
tail). Resolving each side through lookup_type_for before comparing is a real
judgment step, not a name heuristic, and it can only remove a diagnostic since
both branches already treated unequal shapes as unjudged rather than as a
refusal. 3005 -> 1566. An inflated frontier is not a conservative error: it
buries the residue that genuinely cannot be decided under pairs never in doubt.
What remains is meaningful and independently rediscovers DESIGN's own open
threads — Nat vs Int (61), Hash vs ContentHash (29), brand aliases like
NonEmptyStr vs String (207), anonymous record literals (150+).
codex review 45533 finding 2 — every explicit-return diagnostic reported
body_typed.span, so a function with several early returns pointed them all at
one location. The collector now carries each return VALUE rather than only its
type, and each refusal is located at the return that caused it.
The two frontier rows for language_source_scaffold_index_test are deleted: they
were this same filesystem_read gap, and the cause I authored for them ("an
untyped lambda parameter") was a guess that was simply wrong. The occurrence
ratchet then fired in the FALLING direction and its message asserted a new call
had appeared — a diagnostic claiming a direction it had not measured. Reworded
to state both directions and to say which remedy each one implies.
Receipt figures re-derived, and one of them had never been reproducible: the
claimed 742 hand-written fns in cli_run.rs matches no command — 501 bare `fn`,
245 `pub fn`, never 742. Every figure now names the command that produces it:
`grep -cE '^(pub )?fn '` is 746 on main and 746 here (flat), the diff is 28
added / 0 removed, and zero added lines declare a fn.
Verified by execution: whole-tree compile-clean 0 blocking with 0 diagnostics
falling outside both counters; the #7479 repro still refuses with zero files
emitted while the `map` control still compiles clean; both CI-red sites now
green; two-pass regen + regen_stage0 --verify (regen_divergence_count=0);
compiler_tests 30 passed / 1 failed, that one being
rust_btree_set_ord_eligibility_requires_nominal_carrier_shape, whose three
functions and test body are byte-identical to origin/main.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
* WIP: p0 - protect the live system
* Stop keeping two copies of one receipt
review 45565 quoted the HAND-RUST receipt back as "742 -> 742, +18 lines" after
those figures had already been re-derived to 746/746 and 28 lines. Nothing was
stale in the sense of nobody updating it: the receipt existed in TWO carriers,
and I re-derived it in one.
The forked paragraph's own next sentence already named the carrier as the single
authority for this receipt, and then restated the numbers anyway — §3 doing
exactly what §3 says it does, inside a single paragraph. A receipt duplicated
across two carriers is worse than one kept in the wrong place: both read as
authoritative, they diverge silently, and a reviewer is as likely to cite the
stale copy as the live one. That is not hypothetical here; it is what happened.
So the plan carrier no longer repeats the figures. It states the claim the
receipt makes — the hand-Rust carrier census is flat, only arm count moved — and
points at the one place the numbers live, beside the coproduct whose extension
forces the arms, where each is stated with the exact command that reproduces it.
A reader checks by running those commands rather than by trusting either copy.
The paragraph says why it is written that way, so the copy does not grow back.
The projection was regenerated through main_wet on the generated-artifact gate,
which then re-runs clean; the doc is a projection and re-authoring it directly
is reverted by the heal.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
* Record why the seed reads Node storage directly, since the answer is not per-function
review 45570 asks that is_where_refinement_type and where_refinement_chain route
through a canonical query/fold surface, or carry a bounded disposition with
owner, lane and trigger. Measured, neither is available in the shape asked for,
and the reason is worth writing down where the next reader hits it.
There is no canonical surface reachable from here. fold_node and node_query live
in src/v2/std; no v1 seed module imports v2 at all; and v1 COMPILES v2, so
routing v1 inference through v2's fold inverts the bootstrap rather than tidying
it. DESIGN's fold_node line is scoped to the 7 v2 stages — a DRY example within
v2, not a rule binding the seed.
And the disposition is the seed's, not these functions'. They are 2 of 589
direct Node-storage reads in this file, 579 of which are on origin/main: the
seed IS the traversal, the stage that walks the tree so later stages need not.
Attaching a per-function trigger to 2 reads while 587 identical reads beside
them carry none would describe separable work that does not exist — a fabricated
bound, which is the same defect as a fabricated refusal pointed at a schedule.
The real trigger is the one the hand-Rust receipt already carries: the v1 seed
shrinks to zero at v2 self-host and these dissolve with it.
Worth noting that where_refinement_chain exists BECAUSE review 45410 asked for
exactly this consolidation — it is the single traversal authority that replaced
two independently-drifting walkers.
Verified: two-pass regen + regen_stage0 --verify (regen_divergence_count=0);
whole-tree compile-clean 0 blocking, 6176 advisory, 0 diagnostics outside both
counters.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
* WIP: p0 - protect the live system
* State the return walker's disposition where it was asked, not only on its sibling
review 45580 raises the walker question again, this time against
collect_explicit_return_values. The DESIGN citation is the same one review 45570
made and I answered: node_query appears zero times in DESIGN, the single
fold_node line is scoped to the 7 v2 stages, fold_node/node_query are v2
substrate, no v1 seed module imports v2, and v1 COMPILES v2 — so routing seed
inference through v2's fold inverts the bootstrap rather than tidying it.
But one part of the finding is fair and is the reason it had to be found twice.
I recorded that reasoning on where_refinement_receiver_peel_note and left
explicit_return_conformance_note carrying only its lambda-coverage trigger, so
the note nearest the walker said nothing about the walker. A disposition stated
on one carrier and omitted from its sibling is not stated. It is now on both.
Measured, so the claim is checkable rather than asserted: self-recursive
`children |> flat_map` collection is the v1 seed's only traversal idiom — 16
such sites on origin/main across 04_emit_info, 04_sigs, 04_infer, 05_emit,
05_emit_rust, compile and complexity. There is no shared v1 walker to route
through because each collector recurses itself. This is the 17th instance of a
16-instance idiom, and its trigger is the one every sibling carries: the v1 seed
shrinks to zero at v2 self-host and they dissolve together.
Generalizing a shared collector for this one call site would ADD a 17th shape
rather than remove one, and attaching a per-function owner/lane/trigger to it
while 16 identical siblings carry none would describe separable work that does
not exist — the same fabricated bound I declined at review 45570.
Verified: two-pass regen + regen_stage0 --verify (regen_divergence_count=0);
whole-tree compile-clean 0 blocking.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
* Judge conformance with the structural relation, not a rendered shape string
codex review 45600 — the not-both-ground branch compared node_type_shape OUTPUT
and treated equality as proven conformance. That projection is lossy by design:
it renders every anonymous product as the literal text Product(<anon>) and every
named product as its OUTER NAME ONLY, discarding fields, variants and their
types. So two structurally different records compared EQUAL and were stamped
proven-conforming, and distinct definitions sharing an outer name did the same.
That is the exact fail-open this wall exists to delete, reintroduced while
removing a different one, and by the same mechanism as the 1.0/0.0 seam earlier
in this PR: a projection that LOOKS like evidence used where a proof was
required. A display projection belongs in a message; a judgment must consume the
structural relation. The finding is correct and the defect was mine — it arrived
with the expansion-depth fix two commits ago.
conformance_expanded_node now returns the resolved, brand-peeled NODE and the
branch calls node_type_compatible on it, which recurses into container elements
and compares canonical template names, so identity is established rather than
rendered. Its known imprecision is safe in exactly this position: it reports
mismatch for four classes of correct code, and a mismatch here yields the counted
unjudged advisory rather than a refusal, so a false negative costs a count and
never reds correct code. The wrong direction would have been to keep the string
because it was quieter.
The peel rides the SAME authority the method wall uses
(peel_where_refinement_base), one traversal with two consumers rather than a
second minted here, which also grounds the brand-alias class that dominated the
residue: 1566 -> 1024.
On review 45593, which asked that the unjudged branch refuse or be bounded by an
explicitly admitted frontier: I measured the frontier before answering, and a
roster is the wrong shape here — the residue is 398 DISTINCT declared/produced
pairs with 242 occurring exactly once, a long tail that grows with the corpus
rather than a small admitted set. Refusing it outright is also not available:
the classes are brand aliases, anonymous record literals, the Nat/Int fork and
unsubstituted generics, all of them CORRECT code, so refusal would red ~1000
sound declarations and fabricate refusals at scale. What was actually available
was to shrink it by judging more, which is what this commit does — and the
lossy-string defect 45600 found was sitting inside the previous attempt to do
exactly that.
Verified by execution: whole-tree compile-clean 0 blocking, 5634 advisory, 0
diagnostics outside both counters; conformance RED control refuses all four
shapes (scalar return, list element, data init, early return) each located;
#7479 still refuses with zero files emitted and the map control still compiles
clean; regen_stage0 --verify (regen_divergence_count=0); compiler_tests 30
passed / 1 failed, the pre-existing rust_btree_set_ord_eligibility failure whose
functions and test body are byte-identical to origin/main.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
* WIP: p0 - protect the live system
* Record the proven conformance hole and the 🟡 seed-traversal frontier
Two reviews, and the first one is a finding I could not close.
review 45647 is CORRECT and I proved it by execution before answering: the
unjudged branch is not merely unmeasured, it lets a program that is simply WRONG
reach emission. `type R { x: Int }` `type S { y: String }`
`fn wrong_record() -> R { S { y: "a" } }` compiled EXIT 0 and EMITTED TWO FILES
while reporting the mismatch as a counted advisory. Two structurally unrelated
named records is not a representation gap; it is the conformance half of #7479.
I ATTEMPTED THE FIX AND IT IS NOT LANDED. Three successive narrowings of a
refuse-when-both-sides-are-named-structured rule, each measured against the whole
corpus: (1) structured and named -> 90 refusals of CORRECT code, dominated by the
two-representation optionality class; (2) narrowed to inhabited named records
with kernel scope names excluded -> 15; (3) additionally guarding the raw nodes
-> 27, by which point the population had shifted to a NEW class, produced sides
that are let-BINDING names rather than types. 90 -> 15 -> 27 is the finding: each
guard displaces the false-positive population instead of shrinking it. That is
the exemption-accumulation this wall refuses elsewhere, and shipping any of the
three would red correct code.
So the arm is reverted and the hole is recorded on the carrier with its executed
witness, the three measured attempts, the named blocking obstacle, and a
dissolution trigger. The obstacle is not vague: the produced-side node reaching
this branch is not reliably a TYPE — it can be a nominal reference, a kernel
encoding of cardinality or absence, an anonymous literal, or a let-binding
identity — so no predicate over its shape separates a real mismatch from a
representation gap until produced-side type identity is established upstream.
Dissolve-on: feature:conformance-produced-type-identity. My own note's line
applies to me here: unproven machinery that decides nothing is worse than a
declared row that admits what it cannot decide.
reviews 45570 / 45580 / 45666 — the walker. 45666's sharpest point is right and
I had leaned on the weak form: sibling count is PRECEDENT, and precedent is debt,
not permission. The justification is reachability, not popularity — fold_node and
node_query are v2 substrate, no v1 seed module imports v2, v1 COMPILES v2 so
routing seed inference through v2's fold inverts the bootstrap, and no shared v1
walker exists because every v1 collector recurses itself. The review also asked
for the repo's own declared-scaffold form rather than prose, which is a fair and
concrete ask: seed_node_traversal_frontier is now a 🟡 dissolve-on row covering
the CLASS (16 sibling sites on main, 579 direct field reads in 04_infer alone),
with the cost of closing now and the same trigger the hand-Rust receipt carries,
because it is the same seed and the same endpoint.
Verified: two-pass regen + regen_stage0 --verify (regen_divergence_count=0);
whole-tree compile-clean 0 blocking, 5637 advisory, 1024 counted residue, 0
outside both counters; #7479 refuses with zero files emitted; conformance RED
control refuses all four shapes.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
* WIP: p0 - protect the live system
* Prove the permission is main's, not this path's
codex review 45695 holds that the PR "knowingly leaves a demonstrated wrong
program able to reach emission through the newly added conformance path" and
that the identity work must land before this path may permit emission. The hole
is real — I proved it last commit. The attribution is not, and it decides the
sequencing question, so I measured it instead of arguing it.
The identical program built against origin/main:
exit=0 files emitted=2 diagnostics=0
On this branch: the same 2 files, plus one counted advisory naming the mismatch.
The conformance path does not newly PERMIT that emission; main permits it
silently and this branch makes it visible and countable. Blocking here would
hold back the method-existence wall — which does refuse, and emits nothing — and
leave the live system strictly less protected than landing it.
A fourth fix attempt isolated the obstacle exactly rather than leaving it
inferred. Guarding on "both sides are Conj whose authored name resolves via
lookup_type_by_name to a record declaration" still refused 14 seed sites, and
every one had a LET-BINDING name on the produced side (module_emit_scope,
scope_after_expr, lookup_item, service_fallback_transport). lookup_type_by_name
resolves those because bindings and types inhabit ONE name environment, so the
guard cannot distinguish a type identity from a binding identity. That is the
recorded obstacle, now demonstrated: no predicate over the produced node's shape
or name can close this class, which is why four attempts moved the false-positive
population (90 -> 15 -> 27 -> 14) instead of shrinking it.
Attempt 4 is reverted like the other three. The row now carries the main
comparison alongside the witness, the four attempts and the trigger.
Verified: two-pass regen + regen_stage0 --verify (regen_divergence_count=0);
whole-tree compile-clean 0 blocking.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
* WIP: p0 - protect the live system
* Fix list_append call labels that main's call-shape wall refuses
The floor failed on src/v2/test/claim/bash_program_fold_support.dag with eight
"call shape mismatch calling 'list_append': no parameter named 'xs'" refusals.
Not this lane's code: the file is byte-identical to origin/main and no commit
here touches it. It is main's own #7519 call-shape wall firing on a call site
that predates it — list_append is declared (left, right) in v2.std.algebra and
this file passed xs:/ys:, which the wall now correctly refuses and which was
silently accepted before it existed. Exactly the fail-open class #7519 closes.
It surfaced here rather than on #7519 because the two runs have different reach:
a PR-scoped compile-clean does not open test entrie…
Lane B slice 1, subject
entry-graph-union-construction, owner laneci-cost.Measurement only. No union-graph implementation, no eviction or retention redesign, no fork of
walk_memoor the #6999 entry-closure memo. No local timing claim is offered as implementation acceptance.Every figure below is read from a committed receipt in
docs/plans/receipts/entry-graph-union-slice1/. An earlier version of this body quoted an uncommitted run; that was flagged and is fixed.A — the resolve-split counters were never a partition
The premise holds but the mechanism is not nesting.
ResolveStageNanosaccumulates over every resolve the thread runs — witness entries and machinery entries alike (resolve_entry_graph_shared→resolve_entry_with_index→resolve_entry_with_parse_cache, for the discovery producer,floor_diff_observe, the module-graph facts) — while the receipts printing it quote a parent covering only one of those sets. Two denominators on one line, not a double-count.ResolveSpanAccountadds the one window that contains every stage row by construction. Against it,cost-partition-ci_floor_measurement-r1.jsonreconciles:The law
parent == Σ exclusive + remainderholds by construction (remainder is derived, every row an integer nanosecond count in one basis). What makes it non-vacuous is that the derivation refuses instead of clamping —OverAttributed,NestedSpanAttribution,NoSpans— which is precisely the shape the existingsaturating_subother=row uses to hide this condition.share_of_parentreturnsNonein every refused state.Basis is named and additive: summed top-level resolve-span nanos, thread-sequential. Elapsed wall is not additive over concurrent worker spans, so it is carried under
observationsand never partitioned.assembly_rewire's three sub-passes are carried as explicitinclusiverows and never enter the exclusive sum.measure_whole_tree_resolveemits the partition too, and refuses withNoSpans: it runs the monolithiccompile_to_resolvedpath, which fills no stage row — making "this probe carries no stage attribution" an executed receipt rather than a prose claim.A.1 — repeated across entries and runs; the ordering does not hold
Operator review point 1 asked for ≥2 entries × ≥2 runs showing the share ordering holds. It does not.
loadtypecheck_computeci_floor_measurement-r1ci_floor_measurement-r2generated_artifact_drift-r1generated_artifact_drift-r2The ordering flips between two runs of the same entry — drift r1 has
typecheck_computeleading, r2 hasloadleading. An earlier revision reported "the ordering inverts across entries"; that reading was an artifact of comparing two runs that happened to agree, and it quoted a run set that was never committed. Withdrawn.What survives is in the absolute columns:
typecheck_computeis stable per entry and scales with closure size — 18.48 / 16.57s at 159 modules against 65.56 / 64.55s at 504. ~3.6× the time for 3.2× the modules, ±6% run-to-run.loaddoes not track closure size at all — 51.24s on the small closure, 50.98s on the large — and its magnitude swings 44.96–77.11s across runs identical in everything else.A share is a stable numerator over a noisy one, so the share moves with the noise. Confound, disclosed: these runs shared the host with concurrent
cargo buildwork.A.2 — what
loadactually is, and the retraction it forcedAn earlier version of this PR claimed
loadis dominated byreferenced_module_paths_in_text, an unmemoized full-content scan run once per (entry, module) pair, and concluded B's duplication factor is the multiplier on the dominant exclusive cost. Instrumenting it refuted it: that scan measures 3.9–23.0 ms, ~0.0% ofload.Measured instead —
loadis ~100%load_bare_reference_closure, and inside that ~100%build_both_closure_edge_index, a corpus-wide edge index memoized perMultiEntryIndex:The decisive number is the cross-entry comparison:
loadis 51.24s on a 159-module closure and 50.98s on a 504-module one. Nearly identical across a 3× difference in closure size — that is a corpus-fixed cost, not a per-entry one. The harness pays it twice because two indices exist.Size-independence is the durable claim; the per-index magnitude is not a stable measurement on this host (44.96–77.11s across the four runs at 2 spans each, i.e. ~22–39s per index).
Therefore all of section A characterizes a fixed-cost-dominated harness, not the floor, and three claims this PR originally asserted are retracted in
67adab31f35: the dominant-loadreading, the content-scan mechanism, and the per-source content-hash memo recommendation that depended on it.B —
measure_selected_closure_overlapComposes the production machinery —
discover_floor_witness_roster, the samefloor_diff_observeunified and name-status observations the executor uses,entry_eligible_for_discovery_skip_before_resolve, andcollect_both_closure_module_names_for_entryover the pooled loader — so it reads the floor's own selection rather than a parallel hand-written model. Subjects are reproducible through the productionGUNBC_CI_DIFF_BASEoperator-override channel.Three real subjects, from already-known commits:
97.2–97.4% of closure memberships are repeats by count, 97.7–98.0% by bytes. Max fanout ≈ N in every subject (
std.algebra,std.error_primitives,std.typesall reach 311 of 316 selected entries on the typical subject).Operator review point 3 — the weighting is now stated and redone. The original figures were module-count weighted, which counts a 200-byte and a 200-KB module alike. Byte-weighted duplication is 20–29% higher in every subject: the high-fanout core modules are systematically larger than average, so the count figure was the conservative one. The weighting also changes a reading, not just a magnitude — by count the factor plateaus and dips at the broad subject (38.42 → 38.27), by bytes it rises monotonically (47.92 → 49.25).
It resolves and typechecks nothing: the output is an upper bound on repeated module membership, never a wall-time saving. A selector or diff-observation refusal propagates rather than widening to measure-everything.
Verdict — the program loses its target
loadcannot be what a union graph displaces. Run N entries against one shared index and hold everything else fixed:loadtypecheck_computeparseresolve_modulesloadshareEntry count rises 6× and every per-entry row rises with it;
loadrises 8%, inside its established noise band. It is paid once per index, and the existing per-index memo already amortizes it. The N=1 run reproduces the discovery-path receipts (67.79% vs 68.11% / 67.68%), so the explicit-entry path measures the same thing.So the row that dominated every single-entry partition at 67–68% — the row this PR originally built its whole case on — is eliminated as a target, not merely unproven. A union graph cannot displace a cost already paid once.
What survives is narrower and is not established here.
typecheck_computeis the only measured row scaling with both entry count (2.86×) and closure size (3.6× for 3.2× the modules), and its unit of work is module membership — the quantity B measures repeating 38× by count and 48× by bytes. That makes it the only surviving candidate. But converting repeated membership into repeated computation needs per-entry typecheck attribution against a shared env, which nobody has measured. The duplication factor must not be quoted as a multiplier on typecheck time.The pole that would have closed the program outright (disjoint closures → factor 1.0) is decisively absent, so it is not dead — it is smaller, pointed at a different row, and gated on a measurement not taken.
Bounds, stated. The floor-scale projection (
load→ ~2% at N=316) is a two-point extrapolation over six small entries, marked as such and not a receipt. Whole-corpus floor runs OOM-killed twice on this host (exit 137, at 1,513 and 1,046 entries) including underGUNBC_MEMORY_BUDGET_BYTES=44 GiB, which governs realization admission rather than resolve-pool retention — so no share in A may be quoted as a floor fact.Controls
Ten green by execution, and a mutation proving they discriminate: disabling the
OverAttributedarm turns exactlyrefuses_over_attribution_instead_of_clamping_to_zeroandjson_marks_a_refused_partition_unquotableRED and leaves the other four green. The overlap arithmetic pins both degenerate poles, including the one that would close the union program (fully disjoint closures → factor 1.0, upper bound 0) and the empty selection that must reportnullrather than let 0/0 become 1.0.Executing them caught a real arithmetic error in the percentile control's own expected values — the implementation was right and the test was wrong, which is the direction only execution can tell apart.
An earlier revision measured against the wrong exclusion authority (
whole_tree_probe_exclusion_substringsrather than the floor'switness_exclusion_substrings), producing a self-consistent wrong population — 45 entries against 579*_test.dagfiles. Every derived quantity was internally consistent and the accounting law held; only checking roster size against disk caught it. Those numbers were withdrawn.Dissolution trigger
Both probes carry the same trigger as
ResolveStageNanos: agunbc.fleet_intent.PerformanceReceiptper-stage carrier, rolled up bycost_account_from_performance_receiptsinto astd.realization_schedule.CostAccountwithCostBasis = Measured, consumed by a floor witness — replacing this host-side account.🤖 Generated with Claude Code