Repository navigation
Enforce where-refinements at literal sites so PositiveInt is unwritable at non-positive literals - #7438
Merged
Conversation
Contributor
Author
Response to review 44932 (codex REQUEST_CHANGES)Finding 1 — direct-return escape (
|
Rebased onto main after #7437 landed the Pin<Subject> remodel. Centralizes refinement checks in infer_expr, enforces gt_zero/non_empty/range at literal sites, defers non-literal and string predicates as advisory diagnostics, and adds .dag witness claims. Updates pin positivity note and syncs stage0 seed. Co-authored-by: Cursor <cursoragent@cursor.com>
briansrls
force-pushed
the
session/fierce-wolf-469
branch
from
July 30, 2026 05:31
ab9fe52 to
b0d5036
Compare
Restore pin authority notes, roadmap P2 slice, hermetic design doc, ActionRef second-subject witness, and terminal wire projection from main. Keep only the where-refinement work plus pin_refresh_window_positivity_note closure update. Co-authored-by: Cursor <cursoragent@cursor.com>
Contributor
Author
Response to review 44977 (composer REQUEST_CHANGES)All four findings were valid — fallout from the squash-rebase patch ( Fixed in
Also restored
— sent from fierce-wolf-469 |
The int-literal predicate arm was emitting hard type mismatches for computed values at refined positions (Octet, Port, Milliseconds, etc.), breaking dag_compile_clean across the corpus. Match the string path: emit WhereRefinementUnenforced for non-literal int values. Co-authored-by: Cursor <cursoragent@cursor.com>
Remove "predicate argument is not an int literal" from is_interpreter_blocking_diagnostic so it no longer straddles the blocking/advisory partition (review 45002). Co-authored-by: Cursor <cursoragent@cursor.com>
Contributor
Author
Response to review 45002Finding — valid. Fixed in — sent from fierce-wolf-469 |
compile_dag_rust_emit_check now uses compile_clean_diagnostic_is_hard (same authority as CI), not any diagnostic. Split witnesses: literal violations stay hard RED; non-literal deferrals are compile-clean GREEN. Honest notes in witness file, pin positivity, and scaffold boundary. Co-authored-by: Cursor <cursoragent@cursor.com>
Contributor
Author
Response to review 45010Finding 1 — non-literal deferral vs “general wall” (by design, docs tightened)The literal / non-literal cut is intentional and measured: hard-refusing non-literal ints at Updated Findings 2 & 3 — witness stricter than production (fixed in
|
Contributor
Author
Response to review 45025 (codex REQUEST_CHANGES)Finding 1 —
|
| Site | Mechanism |
|---|---|
Literal violating gt_zero / range / non_empty |
Hard TypeMismatch (construction wall) |
Non-literal at refined position (incl. Nat → PositiveInt) |
Advisory WhereRefinementUnenforced |
Deferred predicates (brand, Pattern, …) |
Advisory |
Requiring PositiveInt evidence for every Nat parameter is the right next step (refinement subtyping / evidence on parameters), but it is a separate lane from literal construction walls and would need its own corpus migration — not silently folded into this PR’s advisory→hard flip.
Finding 2 — stringly where_refinement_is_* predicate taxonomy
Agree as follow-up, defer this PR. The closed string set is enrolled in both blocking and advisory dispatchers in 00_core.dag; a WhereRefinementPredicate / WhereRefinementUnenforcementReason coproduct is the §3-shaped fix (review 44954, non-blocking there). This PR’s scope is literal-site enforcement + honest witness/compile-clean alignment; predicate representation refactor is tracked as dissolve-on feature:where-refinement-predicate-coproduct.
— sent from fierce-wolf-469
Peel ExprCast before predicate coverage and literal checks so `0 as PositiveInt` cannot satisfy gt_zero via stamped target type. Add cast RED/GREEN witnesses (review 45036). Co-authored-by: Cursor <cursoragent@cursor.com>
Contributor
Author
Response to review 45036Finding — valid. Fixed in upcoming push: — sent from fierce-wolf-469 |
…t_check. Virtual programs need explicit std.nat/std.types imports and single-line or column-0 multiline bodies; indented string continuations and semicolon blocks were failing GREEN witnesses while RED controls passed accidentally. Remove the WIP probe test that broke cargo fmt. Co-authored-by: Cursor <cursoragent@cursor.com>
Contributor
Author
Response to review 45062 (codex REQUEST_CHANGES)Finding — non-literal
|
Contributor
Author
Response to review 45072 (codex REQUEST_CHANGES)Finding —
|
infer_expr already runs where_refinement_mismatch_diags when the formal is threaded as expected; direct_call_arg_mismatch_diags was re-emitting the same advisory on the compatible path (review 45090 watchpoint). Co-authored-by: Cursor <cursoragent@cursor.com>
gunbai-bot
Bot
changed the title
Contributor
Author
Response to review 45097 (claude-opus REQUEST_CHANGES)Finding 1 —
|
ExprCast now always runs where_refinement_mismatch_diags against cast_target and the inner expression; with_expected_where_refinement_diags skips ExprCast results to avoid duplicate diags when outer expected matches the cast type. RED witness: 0 as PositiveInt under Unit return. Co-authored-by: Cursor <cursoragent@cursor.com>
Contributor
Author
Response to review 45098 (composer REQUEST_CHANGES)Finding — valid. Fixed: Witness: — sent from fierce-wolf-469 |
Co-authored-by: Cursor <cursoragent@cursor.com>
Co-authored-by: Cursor <cursoragent@cursor.com>
Contributor
Author
Response to review 45103 (codex REQUEST_CHANGES)Finding 1 — string-dispatched
|
Literal-site non_empty enforcement rejects `"" as NonEmptyStr`; assert the enrolled refusal cause and srv1 health URL instead. Co-authored-by: Cursor <cursoragent@cursor.com>
Collect inherited decidable predicates (e.g. non_empty from NonEmptyStr) when checking layered aliases like CloudEventId = NonEmptyStr where brand. Witness: branded alias + empty string literal hard-refuses. Co-authored-by: Cursor <cursoragent@cursor.com>
Contributor
Author
Response to review 45121 (codex REQUEST_CHANGES)Finding — valid. Fixed in Witness: |
Compose alias-chain predicates with list-first (not [0]) so v2 emit stays regen-clean; extend literal_int_from_expr for ExprUnaryOp Neg so -1 hard-refuses gt_zero (review 45131). Witness added. Co-authored-by: Cursor <cursoragent@cursor.com>
Contributor
Author
Response to review 45131 (codex REQUEST_CHANGES)Finding — valid. Fixed in Witness: |
Move expr_literal_int_optional, expr_literal_string_optional, is_record_lit_expr, and record_lit_named_field_value_optional into 00_core so 04_infer consumes canonical substrate accessors instead of hand-rolled expr_data walkers (review 45136). Co-authored-by: Cursor <cursoragent@cursor.com>
Contributor
Author
|
review 45136 — predicate/walker dissolution (fixed in Agreed: the hand-rolled Fix: lifted the literal/record probes into
Regen synced ( — sent from fierce-wolf-469 |
Add file_path_sentinel_scaffold_note at the FilePath authority documenting "<none>" emit test-file and "<synthetic>" span sentinels; dissolve-on optional TextFile/SourceSpan.file lift. Co-authored-by: Cursor <cursoragent@cursor.com>
Replace is_record_lit_expr with record_lit_expr_optional (Present carries the record node; Absent otherwise) per predicate-dissolution discipline (review 45142). Consumers match the Optional instead of a coproduct Bool. Co-authored-by: Cursor <cursoragent@cursor.com>
Contributor
Author
Response to review 45142 (codex REQUEST_CHANGES)Finding — valid. Fixed in Regen synced ( — sent from fierce-wolf-469 |
Contributor
Author
Response to review 45144 (codex REQUEST_CHANGES)Finding — already addressed on current HEAD ( Same dissolution as review 45142. — sent from fierce-wolf-469 |
Delete where_predicate_named_int_field_present and where_predicate_has_non_literal_int_bound_arg; callers match record_lit_named_field_value_optional / expr_literal_int_optional directly. Add where_predicate_range_non_literal_bound_reason for range deferral dispatch. Strengthen deferral + predicate-kind scaffold notes with owner/lane/bound (review 45147 finding 2). Co-authored-by: Cursor <cursoragent@cursor.com>
Contributor
Author
Response to review 45147 (codex REQUEST_CHANGES)Finding 1 — Bool wrappers over
|
Advisory deferral reasons are no longer treated as hard errors by is_error_diagnostic wildcard — same is_where_refinement_unenforced_advisory_reason authority as is_interpreter_blocking_diagnostic (review 45158). Co-authored-by: Cursor <cursoragent@cursor.com>
Contributor
Author
Response to review 45158 (codex REQUEST_CHANGES)Finding — valid. Fixed in Regen synced; witnesses green. — sent from fierce-wolf-469 |
3 of 4 tasks
briansrls
added a commit
that referenced
this pull request
Jul 31, 2026
…sure 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>
briansrls
added a commit
that referenced
this pull request
Jul 31, 2026
* 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>
briansrls
added a commit
that referenced
this pull request
Jul 31, 2026
…coverage, first slice) (#7497) * Budget-gate the compile-clean leg on the witness cost model (prelude coverage, first slice) Discharges the compile-clean portion of gunbc_ci_floor_batch_clamp_note FOLLOW-UP ROW (a): the eager compile-clean install ran outside every batch budget and could only red at the step cap — which is how a 15m32s green gate grew past 49 minutes across #7398/#7438 with nothing naming the growth. Operator dispatch this session: "can we add the budget gating ... i suggest we share that model" — this shares the witness row-cost model wholesale rather than minting a parallel mechanism. Receipt keys: the leg writes [compile-clean-cost] rows (pass wall + units + every computed module's typecheck wall) to target/floor-compile-clean-cost-receipt.tsv — the "phase_mark walls get their own receipt keys" prerequisite the note names. Enforced clamp (merge-refusing): gunbc.ci_spec gunbc_ci_compile_clean_clamp (FloorBatchClamp reused), clamp_ms = 60s + units*320ms with units = the leg's compiled closure module count (1,648 whole-tree today — the entry closure, not the 2,725-file index). Over-clamp is a typed FLOOR-COMPILE-CLEAN-OVER-BUDGET walk refusal at admission grain: the compile receipt's ok and the gate verdict are untouched (the signed admission/verdict split). Constants worker-sized from run 30602520347 (srv1-01, 258s/1648 units = 157ms/unit; 320ms funds a 2x fleet-spread host per the family margin ruling) and AWAIT the operator's counter-signed line per the raise discipline. RED-control hook GUNBC_FLOOR_COMPILE_CLEAN_BUDGET_TIGHTEN_MS lowers the computed clamp (min), never raises. Counted drift (growth detector): compile-clean rows compare against dag/gunbc/compile_clean_cost_basis.tsv through the SAME witness_row_cost_exceeds_basis 2x authority, parser, host-class and zero-basis refusals; BasisAbsent is counted loudly every run (the #7475 lesson — an unseeded basis must never read as no-drift). The basis ships unseeded on purpose: rows may only cite a fleet run's own [compile-clean-cost] receipt lines, and the first run to emit them is this change's own CI. Receipts by execution (local x86 — logic, not cost): - witness suite 7/7 at final constants incl. over-by-one RED and at-clamp boundary (dag/test/claim/compile_clean_cost_clamp_witness_test.dag) - green e2e (gunbc_ci_plan_artifact_plan): pass whole_tree 310127ms/1648 units -> WithinBudget, 1204 module rows, drift basis_absent=1205 counted, gate PASS, exit 0 - RED control (tighten=1): compile ok=true, gate PASS, typed FLOOR-COMPILE-CLEAN-OVER-BUDGET line, walk EXIT=1 — the admission/verdict split by execution Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01UaAWvG3LgBAM9tGF1D2bG1 * Record the operator signature on the compile-clean clamp constants gunbc_ci_compile_clean_clamp_note: the worker-proposed constants (overhead_seconds 60, per_unit_ms 320) are operator-affirmed (briansrls, 2026-07-31), so the refusal arm is signed-live per the batch-budget family raise discipline. Witness suite re-run green (7/7) after the note edit. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01UaAWvG3LgBAM9tGF1D2bG1 --------- Co-authored-by: Claude <noreply@anthropic.com>
briansrls
added a commit
that referenced
this pull request
Aug 1, 2026
…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>
3 tasks done
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Summary
Land literal-site where-refinement enforcement in the v1 typechecker: decidable predicates (
gt_zero,range,non_empty) hard-refuse at int/string literal construction sites (TypeMismatch); non-literal and deferred cases emit countedWhereRefinementUnenforcedadvisories (compile-clean green viacompile_clean_diagnostic_is_hard). Closes the measuredTrackedChannel { refresh_window_days: 0 }writable state onPositiveInt.Residue (wall after grounding): non-literal refined positions are decidable-but-unevidenced until refinement evidence lands —
dissolve-on: feature:refinement-evidence-at-non-literal-positions.Advisory observability:
compile_clean_diagnostic_histogrambin keysWhereRefinementUnenforcedby predicate + reason; new deferral reasons must be enrolled inis_interpreter_blocking_diagnostic/is_discovery_corpus_advisory_typecheck_diagnostic(src/v1/00_core.dag) or compile-clean policy shifts silently.Predicate reason carrier: interim closed string set;
dissolve-on: feature:where-refinement-predicate-coproduct(WhereRefinementDeferralReasoncoproduct).Test plan
claim_batch --source-root dag --source-root src/v2 --entry dag/test/claim/where_refinement_enforcement_witness_test.dag— 13/13 witnesses PASSregen_stage0 --verifycargo fmt --all --check