Lane A C1: evaluate CostExpr at concrete SizeVariable bindings, with the CostSum binder lexically scoped by gunbai-bot[bot] · Pull Request #7932 · gunb-ai/gunbc

gunbai-bot · 2026-08-06T19:07:49Z

What this is

Exact valuation for v2.lens.cost: a CostExpr together with a complete valuation of its size variables, evaluated to exact semantic work or a typed refusal. Not hardware time — no duration, rate, or calibration constant enters v2.lens.cost.valuation.

Recut to the exact core by operator ruling. Partial evaluation and bounded evaluation are held on session/deep-owl-215-partial-bounded-hold — sequenced, not rejected. The program is converging on one end-to-end result (exact work and span as literal numbers for a real DAG section) and the exact core is all that milestone needs. Two constraints ride with the held work, recorded on cost_valuation_exact_core_scope_note so returning it cannot quietly undo decisions already taken:

complete and partial stay two entry points over one fold — a caller who swaps one for the other to silence a refusal is running the author-side absorbing fallback, and a single entry point would make that invisible;
the unresolved state must carry the residual CostExpr, not just free-variable names. The held revision carried names only, so 3 + x lost the 3, the addition, and the shape — a result no consumer could complete, lower-bound, render, or check for conservation of work. It must be the rich CostExpr rather than a normalized SymbolicCost, because normalization is exactly the step that discards the CostSum binder.

CostEvaluation is therefore two states: at the exact core there are exactly two honest answers, the work is this number or here is why it cannot be. Declaring an arm with no producer is rung inflation — and the bounded arm in particular was carried through an earlier revision of this PR while its arithmetic silently collapsed a two-endpoint envelope to its own ceiling.

The load-bearing part: binder scoping

v2.lens.cost.expr normalize_cost_expr_to_symbolic matches CostSum with the binder discarded, so a binder-dependent body projects a SymbolicCost naming a variable bound inside the sum. The magnitude may survive; the variable identity does not. This evaluator does not inherit that: env_bind prepends, lookup_bindings answers the head-most match, so a binder shadows an outer binding of the same identity for the extent of its body and only there. Removal on exit is structural — the extended environment is a local value — rather than an unbind step someone must remember. A CostSum is iterated, never multiplied by its bound.

The projection defect is carried as tracked debt (projection_path_binder_discard_debt_note) with its trigger and the reason the existing bounded_summation fixture cannot see it (same variable for binder and bound).

The log arm reported the wrong cause

It matched CostLog { base: _, .. }, ignored the base, and answered UngroundedLogArgument for every non-refusing case — so base 0 read as an argument problem, and a fully grounded argument was called ungrounded, while the normalizer right beside it already checked the base against its own InvalidLogBase. Two paths disagreeing about one fact. Now three causes for three unrelated failures:

failure	cause
base 0 or 1	`ExpressionRefused` carrying the authority's `InvalidLogBase` — cited, not re-minted
unbound argument	`MissingSizeBinding`, like any other unbound size
valid base, exact argument, no integer-log authority	`IntegerLogarithmUnavailable`, naming the real gap

Evidence, by execution

All 16 witnesses pass, every one enrolled in the Tier1 claim conjunction. Four mutations show they discriminate:

mutation	reds	stays green
binder pinned to `Zero`	binder-dependent, shadowing	invariant-body, zero-iteration
unbound variable → `ExactCost 0`	missing-binding	zero-iteration
log arm ignores the base	both invalid-base	grounded-argument, unbound-argument
summation short-circuit removed	one-cause	the rest

The first row is why the existing C1 fixture cannot see the binder class. The second is the point of pairing the earned zero and the fabricated zero. The third is why base-zero and grounded-argument must both be asserted: under the old arm they returned the same cause, so either alone would have passed.

Existing cost-lens witnesses re-run green: atom_zero, bounded_summation (including existing_cost_lens_kernel_unchanged), copied_port_derivation, disj_alternative_floor, expr_refusal, loop_iteration_floor. The Blocking cost wall is untouched.

Nonempty carrier

std.algebra FreeSemigroup<T> — the free semigroup over T exactly as FreeMonoid is the free monoid over T. Its head field is the construction wall: a refusal carrying no cause has no representation.

Deliberately not the Refined<List<T>> spelling of v2.test.claim.manual.refinement_nonempty_list: a refinement predicate concedes the empty state is writable. The NonEmptyList alias is withheld until that fixture retires, so one name never resolves to two declarations. Five carriers in the tree are this shape monomorphised; exactly two carry a dissolution trigger, and both are retargeted onto FreeSemigroup here because they named an event ("promote the manual refinement to std") this PR decided is not the mechanism. The other three are named as untracked stalls owed a row.

Also in

Refusal accumulation was quadratic and reachable today — non_empty_append is linear in its left argument and CostEffect refuses unconditionally, so a refusing body under upper = u built u left-nested causes, all identical because the body expression is fixed and only the binder value changes. evaluate_summation now stops once the accumulator has refused; the soundness argument (a refusal is a property of the body expression, not the binder's value) and its dissolve-on are on the carrier.
nat_max on v2.std.nat is not a duplicate of std.nat nat_max — the two Nats are different types, the same reason nat_add/nat_mul are already forked. Call sites qualify.

Scope guards honoured

No CostSubject, no speculative ValueIdentity, no call graphs / SCC summaries / parser progress / interprocedural memoization. Bindings attach directly to the landed SizeVariable.

CI note

The pull_request trigger has not produced Actions runs for this branch (nor for 7927 and 7893) — cause unknown, surfaced to the operator. This head carries a dispatched ci run, which is the same workflow on the same SHA through a different trigger.

🤖 Generated with Claude Code

…the CostSum binder lexically scoped The subject is semantic work, not hardware time: a CostExpr plus concrete bindings yields exact, unresolved, or refused modelled work. No duration, rate, or calibration constant enters this module. The load-bearing part is binder handling. v2.lens.cost.expr normalize_cost_expr_to_symbolic matches CostSum with the binder discarded, so a binder-dependent body projects a SymbolicCost naming a variable that is bound inside the sum - the magnitude may survive, the variable identity does not. This evaluator does not inherit that: env_bind prepends and lookup_bindings answers the head-most match, so a binder shadows an outer binding of the same identity for the extent of its body and only for that extent, with removal on exit structural rather than an unbind step. Proven by execution against a binder-discarding mutation: pinning the binder to Zero reds binder_dependent_body_is_summed_not_treated_as_invariant and binder_shadowing_is_scoped_and_removed_on_exit while leaving the invariant-body and zero-iteration witnesses green - which is the exact signature of the defect, and is why the existing C1 fixture (same variable for binder and bound) cannot see it. A second mutation answering zero for an unbound variable reds both missing-binding witnesses while zero_iterations_produce_exact_zero stays green: that pairing is what keeps a zero in a cost report unambiguous between nothing to do and nothing modelled. Carriers: v2.lens.cost.valuation CostEvaluation, CostValuationBinding, evaluate_cost_expr, evaluate_cost_expr_partially; std.algebra FreeSemigroup with v2.std.algebra non_empty_singleton / non_empty_append. The nonempty arms are carried by std.algebra FreeSemigroup - the free semigroup over T exactly as FreeMonoid is the free monoid over T, one algebraic axis at two identities. Its head field is the construction wall: an UnresolvedCost naming no free variable and a refusal carrying no cause have no representation, rather than being validated against. It is deliberately not the Refined<List<T>> spelling of the manual fixture, whose refinement predicate concedes the empty state is writable, and the NonEmptyList alias is withheld until that fixture retires so one name never resolves to two declarations. NonEmptyDiagnostics, FiniteSet, NonEmptySymbolChain and NonEmptyGrammarChoiceAmbiguityRows are the same shape monomorphised and dissolve onto it at their own already-declared triggers; that corpus-wide de-fork is not carried here. Stated gaps rather than silent ones: BoundedCost is declared-not-produced because its seed is a ceiling-valued binding, which is the sibling discrete-cost note's envelope scope; CostLog refuses its magnitude through the expression authority's own vocabulary until a cited integer-logarithm authority exists on std.nat. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>

… claim totality, quadratic accumulation, and a false citation Bounded-upper CostSum answered an EXACT value. combine_evaluation of ExactCost 3 and ExactCost 7 under nat_max reaches combine_known with both endpoints at 3, so bounded_or_exact collapses to ExactCost 7 — an exactness claim manufactured from an inexact input, sitting exactly where the envelope lane plugs its seed in. Replaced with evaluation_interval, which pairs the LOWER of one evaluation with the UPPER of a different one; an inverted interval refuses with InvertedCostInterval rather than being normalised by swapping the endpoints. Witnessed at its own seam because the arm has no producer yet; restoring the max spelling reds three of the four new witnesses. The PR body claim that the envelope lane adds a seed and no arithmetic was therefore false and is retracted. The Tier1 claim conjunction ran three of thirteen witnesses while its label asserted the refusal and scoping behaviour the other ten established, so CI could go green with the label false. every_valuation_witness_holds now enumerates every test fn in the file. Refusal accumulation was quadratic and reachable today: non_empty_append is linear in its left argument, so a body refusing under upper = u built u causes left-nested — and CostEffect refuses unconditionally in this slice. The causes were also IDENTICAL, because the body expression is fixed and only the binder value changes, so this amplified one deficit u times rather than counting u deficits. evaluate_summation now stops evaluating the body once the accumulator has settled; the soundness argument (a refusal here is a property of the body expression, not the binder's value) and its dissolve-on are on the carrier, and the new one-cause witness reds when the skip is removed. The FreeSemigroup grounding note carried a false citation, in the note arguing for single authority. Of the four carriers it named as each already carrying a migrate_when_nonempty_list_refinement_promoted trigger, grep says only two do, and a fifth instance was omitted. Corrected to five carriers, two triggered. Both surviving triggers are RETARGETED onto FreeSemigroup: they named the event as promoting the manual refinement to std, and this change decided that promotion is not the mechanism, so they would have been left waiting on an event that cannot occur as spelled. Also: the partial evaluation mode is stated as not being an escape from a refusal (swapping entry points to silence one is the author-side absorbing fallback); the order note now says causes accumulate WITHIN an arm and the dominated side's payload is dropped ACROSS arms; and the projection-path binder discard in normalize_cost_expr_to_symbolic is named as tracked debt with its trigger and the reason the existing fixture cannot see it. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>

gunbai-bot · 2026-08-06T19:45:58Z

Both findings from review 49620 verified against the code and fixed in the pushed commit.

Finding 2 (bounded-upper summation) — confirmed, and worse than "wrong for the envelope lane". Traced: combine_evaluation(ExactCost 3, ExactCost 7, nat_max) reaches combine_known with lower/upper both 3, so bounded_or_exact(nat_max(3,7), nat_max(3,7)) collapses equal endpoints to ExactCost 7. That is an exactness claim manufactured from an inexact input — the fabricated-plausible-output class, narrowing in the direction that reads as harmless because the number is still a legitimate upper bound.

Fixed by building the pairing rather than by refusing the arm: evaluation_interval takes the lower of one evaluation against the upper of a different one — which is precisely what combine_evaluation does not do, since it pairs lower-with-lower and upper-with-upper. An inverted interval refuses with a typed InvertedCostInterval cause rather than being normalised by swapping endpoints, because answering the swapped question is the same fabrication one level up.

On your point that the arm is declared unwitnessed: agreed that does not excuse the arithmetic, and the arm's producer-status note now says so. evaluation_interval is witnessed directly at its own seam rather than through a producer that does not exist — five witnesses covering both endpoints retained, the no-collapse control, the degenerate equal-endpoint case, the inverted refusal, and refusal propagation. Restoring the max spelling reds three of the four interval witnesses, so this is a regression control on a defect that actually occurred.

Finding 1 (claim conjunction) — confirmed. One clarification on mechanism, which does not change the verdict: the sibling test fns are not orphans — claim_batch discovers and executes each one, and all 19 pass. But your point stands at the claim seam: the Tier1 label asserted refusal and scoping behaviour that only three of the enrolled functions established, so the claim row could have gone green with its own label false. every_valuation_witness_holds() now enumerates every test fn in the file, and claim_conjunction_totality_note states the rule the file follows: a claim label may assert only what its conjunction executes, so adding a test fn without adding it there is the defect to watch for.

Two further fixes landed alongside, from the lane review: refusal accumulation inside evaluate_summation was quadratic and reachable today (non_empty_append is linear in its left argument, CostEffect refuses unconditionally, and the accumulated causes were identical because the body expression is fixed across iterations), and the FreeSemigroup grounding note carried a false citation about which carriers already declare a dissolution trigger — corrected to what grep decides, with the two real triggers retargeted since this PR invalidated the event they named.

— sent from deep-owl-215

Zero GitHub Actions runs were created for either pushed SHA over roughly an hour, while sibling branches got ci runs throughout that window; the run was not awaiting approval either. main protection requires the ci check, so an empty synchronize is the only way to get one. Two approvals on the previous head are re-earned rather than assumed. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>

Operator ruling: scope to complete exact valuation. Kept — exact valuation at a complete binding set, CostSum binder scoping and shadowing, duplicate refusal, effect refusal, log refusal, and the earned-zero versus fabricated-zero distinction. Held on session/deep-owl-215-partial-bounded-hold — partial evaluation and bounded evaluation, sequenced rather than rejected, with both constraints that ride with them recorded on the carrier so they cannot be quietly undone: complete and partial stay TWO ENTRY POINTS over one fold, and the unresolved state must carry the residual CostExpr, not just free-variable names. CostEvaluation is two states here because at the exact core there are exactly two honest answers: the work is this number, or here is why it cannot be. Declaring an arm with no producer is rung inflation — and the bounded arm in particular was carried through an earlier revision while its arithmetic silently collapsed a two-endpoint envelope to its own ceiling. The log arm reported the wrong cause. It matched CostLog { base: _, .. }, ignored the base entirely, and answered UngroundedLogArgument for every non-refusing case — so base 0 read as an ARGUMENT problem, and a fully grounded argument was called UNGROUNDED, while v2.lens.cost.expr's normalizer right beside it already checked the base against its own InvalidLogBase. Two paths disagreeing about one fact. Now three distinct causes for three unrelated failures: an invalid base refuses through the expression authority's InvalidLogBase (cited, not re-minted), an unbound argument refuses as MissingSizeBinding like any other unbound size, and a valid base with an exact argument refuses as IntegerLogarithmUnavailable, which names the real gap and is countable against it. Restoring the base-ignoring arm reds both invalid-base witnesses; the base-zero and grounded-argument pair is the discriminating one, since the old arm gave both the same cause. All 16 witnesses green by execution, all 16 enrolled in the claim conjunction. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>

…naming-hygiene gate found The enroll-or-refuse pre-plan walk refused v2.test.lens_cost.valuation every_valuation_witness_holds as a plain fn unreachable from every test fn and test data — silent de-enrollment. It is the single root of the run: the ci job's failure was FloorUpstreamAlreadyRed with build=success and heal=success, which adds no verdict of its own. Note the remedy that does NOT work, since it is the obvious one: the claim data already referenced the helper by name — that is what it exists for — and a plain `data` does not count as reachability for this gate. Promotion to `test fn` is what satisfies it. Worth naming the shape rather than just fixing it: the conjunction was factored out to close review 49620's finding that the claim enumerated three of thirteen witnesses, and the helper that fixed a specification-without-execution defect was itself not executed by anything the gate recognises. Same class, one level out. The totality note now says so, so the next reader sees why the enrollment is deliberate rather than incidental. 17 witnesses green by execution; the local pre-plan walk that produced the CI refusal now completes clean. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>

…rifted the self-host fixed-point regen_verify_gate_passes returned false because src/v1/stage0/src/std_algebra.rs did not contain the FreeSemigroup the emitter now produces from dag/std/algebra.dag. Adding a type to a std authority without regenerating the committed emitter output is exactly what the fixed-point gate exists to catch. Regenerated with regen_stage0 rather than hand-edited — the file is emitter output, and a hand-added struct would pass the diff while making the seed diverge from its authority. The diff is 7 lines, additive, only the struct. Order mattered: regenerate, rebuild the seed binaries from the regenerated sources, then verify with those binaries — regen_divergence_count=0, and 17 witnesses green against the rebuilt seed. The ci job's failure was again FloorUpstreamAlreadyRed with build and heal green, so regen was the only real signal. Note on the emitted shape, since it is visible in the diff: FreeSemigroup carries a _phantom: PhantomData<T> beside an already-inhabited T. That is the emitter's established convention for generic structs here, not something this type triggered — 25 of 39 structs in this one file carry it, including Magma<T> and the FieldOfFractions<R> pair DESIGN names as correctly grounded. There are zero construction sites for it in emitted Rust, so it imposes nothing on call sites. Whether the convention is a defect is a corpus-wide emitter question, not this PR's. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>

gunbai-bot · 2026-08-07T00:02:08Z

On the _phantom nit from review 49751 — accurate observation, but declining it, and the reason is the same discipline the rest of this PR is built on.

src/v1/stage0/src/std_algebra.rs is emitter output, not source. The change that regenerated it exists precisely because the self-host fixed-point gate caught the committed seed drifting from what dag/std/algebra.dag now produces. Hand-editing the struct to drop the field would pass the drift diff while making the seed diverge from its authority — the file would no longer be what the emitter emits, which is the one property the gate exists to hold. So the phantom cannot be dropped here; it can only be dropped in the emitter.

And it is not specific to FreeSemigroup. Measured in that same file: 25 of 39 structs carry _phantom, including

Magma<T> { op: Rc<dyn Fn(T, T) -> T>, _phantom } — T inhabited by op
FieldOfFractions<R> { num: R, denom: R, _phantom } — R inhabited by both fields, and this is the pair DESIGN names as the correctly grounded construction

So the emitter adds the marker to generic structs whose parameter is genuinely inhabited, as a matter of course. That may well be worth fixing, but the denominator is the corpus and the subject is the emitter's generic handling — not this PR, which would be cementing a hand-edit into generated output to make one instance look tidy.

Practically it costs nothing today: there are zero construction sites for FreeSemigroup in emitted Rust (grep -c 'FreeSemigroup *{' src/v1/stage0/src/ → 0), so no call site is burdened, and none of the held partial/bounded work adds any either.

— sent from deep-owl-215

…ether CostMul routed both sides through the generic refusal-dominates combiner, so CostMul of zero and CostEffect refused while the symbolic authority answered zero for the same expression — two paths disagreeing about one CostExpr, and the exact evaluator was the wrong one: a zero multiplicity means the body is never executed, so refusing because an unexecuted factor lacks an effect model is the did-no-work versus could-not-model conflation the earned-zero controls exist to prevent. Fixing only that would have traded one divergence for a narrower one, because the reference was itself ASYMMETRIC: symbolic_product matched a's arms first, including UnknownCost, and only then inspected b — so zero times unknown absorbed while unknown times ZERO returned unknown. Multiplication is commutative, so an operand order that changes the answer is a defect, not a style. Both paths are fixed in one motion and now agree in both orders. The annihilator lives in a multiplication-specific function and beats refusal-dominance, which governs every other combination here. That ordering is load-bearing and the carrier says so: checking refusals first reads like tightening a fail-closed path and would silently restore the defect, with only the two zero-times-effect witnesses reding. Controls, both directions on both properties, because an asymmetry defect cannot be caught by an asymmetric test: zero times unknown and unknown times zero both absorb; one times unknown and unknown times one both stay unknown; zero times CostEffect and CostEffect times zero are both ExactCost zero; one times CostEffect still refuses. Mutations discriminate — reverting multiply_evaluations reds both zero-order witnesses while one-times-effect still refuses; restoring the old arm order reds only the right-operand case. 24 witnesses green. The Blocking cost-wall baseline was re-run because this touches an authority feeding it: loop_iteration_floor (incl. its independent linear-times-zero control), disj_alternative_floor, bounded_summation (incl. existing_cost_lens_kernel_unchanged), atom_zero, expr_refusal and copied_port_derivation — 19 witnesses, all green. Witness accounting corrected: the claim label and note now say every LEAF witness, which the aggregating conjunction obviously cannot include itself in. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>

Adding v2.std.nat.nat_max (the Peano Nat, needed by evaluate_size_expr's SizeMax and evaluate_cost_expr_in_env's CostMax) gave the name two declarations. test.claim.realization_schedule_critical_path is the single module whose import closure carries both authorities, so its bare call site stopped resolving and reddened the compile-clean gate. Qualified as std.nat.nat_max, matching the std.nat.nat_compare already qualified on the line above it inside the same witness. The four other bare nat_max call sites were checked by scoped compile rather than assumed safe -- dag/std/realization_width, dag/std/realization_measurement, dag/gunbc/econ/free_tier_serving and dag/gunbc/econ/scm_serving_model each compile with zero errors, so their closures do not carry both authorities and they need no qualification. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>

…ered residue The floor reported three reds. Two roots, one of them not mine. NON-FOLD RESIDUE. Three wildcard arms landed with the exact evaluator. Two were avoidable and are now gone rather than declared: combine_evaluation and evaluate_summation match over CostEvaluation, which has exactly two variants, so `_ =>` became `ExactCost { value: .. } =>`. DESIGN section 5 puts construction above declaring a residue, and it buys what a roster row cannot -- a third CostEvaluation variant would now make both matches non-exhaustive and compile-clean would refuse, instead of the new variant being swept into a wildcard silently. multiply_evaluations is rostered, not "fixed". Its arms discriminate a nested VALUE (an ExactCost carrying Zero) rather than a variant, so enumerating would write the residual combine_evaluation call twice, underneath the arm order that multiply_evaluations_zero_note declares load-bearing. Duplicating that expression to satisfy a counter would make the function more fragile. Its reason says so, rather than reusing the generic nfr_reason_mint_era its neighbours carry. INERT CARRIER. Not from this change. Probing inert_carrier_names_live returned eleven live names against twelve rostered; the extra is ProcMeminfo, whose consumer landed in #7891 -- already an ancestor of this branch -- while the roster row stayed. origin/main carries both files byte-identically, so this witness is red on main too. The row is deleted here because it blocks merge and deletion is exactly what its own dissolve trigger prescribes; reported upstream so another lane does not duplicate it. Also records, in symbolic_product_zero_absorption_note, that the symmetry the annihilator fix established is CLASSIFICATION and not provenance: unknown times unknown still returns the left operand's diagnostic. That is pre-existing and module-wide (symbolic_sequential drops the same way), and closing it means widening UnknownCost to carry several diagnostics, which is its own change with its own witnesses. Green by execution: non_fold_residue_clean_holds, non_fold_residue_no_unrostered_or_stale, inert_carrier_no_unrostered_or_stale, and every_valuation_witness_holds over all 23 leaf witnesses -- the last because the exhaustive-arm edits rewrote live evaluation paths, not just roster data. Seed receipt reports unrostered=0 stale=0 live=149. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>

# Conflicts: # dag/gunbc/non_fold_residue.dag

gunbai-bot · 2026-08-07T21:48:42Z

Closing as folded into #8027 (cost-analysis lane consolidation, tree wind-down). The branch is kept — nothing here is lost, and this PR can be reopened.

Why folded rather than re-run. This PR was 2/2 on head and mergeable=true, so the only thing standing between it and a merge was ci, red on cross_module_qualified_reference_emits_call_from_correct_module (killed at 5481.9ms against the 5000ms fast-lane budget). Those approvals were unspendable, and nothing on this branch would have made them spendable:

Move cross-module qualified-declaration emit witness to substrate long lane #8010 retired that witness to the substrate long lane at 21:13:21Z — but on main. A PR runs its own corpus, so a re-run here reproduces the failure exactly. Checked on this branch: dag/test/claim/qualified_declaration_reference_emit_witness_test.dag still contains the function, so the fast lane still discovers it.
Its merge ref 1bcb64ff437 does not carry Move cross-module qualified-declaration emit witness to substrate long lane #8010 either — merge refs recompute lazily, not on every base movement — so even a fresh trigger would have tested a tree without the retirement.

Merging main in would have fixed it and cost the approvals. #8027 is cut from current main, so it carries the retirement by construction (0 occurrences in the fast-lane file, long-lane file present) and gets a clean read on the same content.

Content preserved verbatim — #8027 merges this branch, it does not rebase or re-author it. All 12 files, +916/-10.

Stage0 obligation checked at content grain on the folded tree, not by filename: FreeSemigroup is dag=1 / seed=1; the other introduced symbols (non_empty_append, non_empty_singleton, non_empty_to_list, free_semigroup_grounding_note) live entirely under src/v2/**, outside the seed projection. No dag>0 / seed=0 symbol. The regen job settles it by execution.

— sent from proud-bear-834

…ries #8010's witness retirement) (#8027) * WIP: cost analysis * Execute the name-key precondition C0(b2)'s join was assuming classification_matches_fact joins a roster row to a DeclFact on BARE NAME, while DeclFact carries qualified_name and kind and could key exactly. That is sound only while every top-level declaration of v1.compiler.complexity has a distinct name, and nothing in the carrier makes that true -- it is a property of the subject module, not a wall this carrier erects. Measured over src/v1/complexity.dag: 201 top-level declarations (171 fn, 26 type, 4 data, 0 let), zero duplicate names. So the join is correct today. But a measurement of the current tree is not an oracle (DESIGN section 5), so the precondition is now EXECUTED rather than assumed. The gap this closes is real and none of the four existing totality witnesses covers it: a duplicate name in the DERIVED population still classifies, still matches a roster row, and leaves no stale row, so one roster row can silently answer for two declarations while every count agrees. roster_names_distinct does not cover it either -- it constrains the AUTHORED side only, and the duplicate here would be on the derived side. Added population_names_distinct beside the existing roster_names_distinct, reusing name_already_seen rather than minting a second distinctness fold. Green by execution, all three run through claim_batch against the real tree: PASS w_population_decl_names_are_distinct (live population) PASS w_distinctness_fold_reds_on_a_planted_duplicate (discriminating RED) PASS w_distinctness_fold_accepts_a_distinct_control (positive control) The RED matters: a distinctness fold that cannot fail proves nothing, so a planted same-name pair must come back false or the live green is empty. Dissolve-on is named on the carrier: the roster carrying exact DeclFact identity (qualified_name, or name plus kind) makes the join exact by construction and retires the precondition. That is a 201-row re-authoring and is deliberately not bundled here. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Sweep the stale-status class across the whole plan, not the one line I fixed (review 49289) Review 49289 caught three more instances of exactly the defect this PR exists to remove, and it was right: I corrected one occurrence and did not sweep for the class -- the same shortcut I would send back on someone else's diff. Fixed, all verified against main rather than recalled: section 7 C0(c) bullet still called the split "the next implementation slice" while the C0 summary said DELIVERED section 9 operator ruling same, so a reader of section 9 could still treat C0(c) as open section 2 table still listed a single lens_contract_complexity row carrying RatchetForever. That row does not exist on main. Replaced with the two rows that do -- derived_kernel (WallAfterGrounding) and optimality (RatchetForever, the genuinely undecidable residue) Two the review did not name, found by sweeping for the class instead of the reported lines: section 4 asserted in the present tense that lens_contract_complexity carries RatchetForever. Marked RESOLVED by #7841 and kept as the argument the split rests on, rather than deleted -- the reasoning is why the split has the shape it has section 8 a discriminating control named the deleted contract. Re-pointed at both split rows, where the mode/consumer disagreement is actually checkable status blockquote said one carrier "currently" declares it permanent Remaining bare mentions at lines 119, 143 and 147 are deliberate historical references ("the mixed row", "as written then") describing the pre-split state in explicitly past tense, not live claims about the tree. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Fix the dissolution trigger: it named a deleted row and set an unsatisfiable condition (review 49307) Third catch of the same class, and this one was more than a stale name -- the retirement criteria were unsatisfiable as written. Clause 1 required that "lens_contract_complexity's boundary class distinguishes the genuinely undecidable residue from the decidable capability". That is precisely what #7841 delivered, so the clause is SATISFIED and now says so, naming the two rows that replaced the mixed one. Clause 2 required that "lens_contract_complexity has a live consumer witness and has flipped off AuditOnly". Read onto the split, that can never be true. lens_contract_complexity_optimality is RatchetForever and stays permanently AuditOnly by the plan's own section 7 C0(c) ruling -- so a retirement condition demanding it flip would make this doc unretirable BY CONSTRUCTION. Re-scoped to lens_contract_complexity_derived_kernel, which is the half that can legitimately flip, and the clause now states explicitly why optimality is excluded so nobody re-adds it later. That second half is the part worth noticing: a dissolution trigger that cannot fire is a scaffold with no exit, which is the failure DESIGN section 6 asks a named trigger to prevent. The stale name would have been cosmetic; the unsatisfiable condition was not. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * WIP: cost analysis * Remove merge-event status prose from the plan; cite carrier symbols instead Reviews caught this plan stale in four separate places, each claim true when written and false a day later. The common shape was a merge-event assertion -- "DELIVERED ON MERGE of #7841", "both rows are on main" -- which rots without anyone touching it, because nothing in the tree can decide it. Replace the class, not the four lines. Every delivery claim now names the carrier SYMBOL a reader can resolve (DESIGN section 3, cite-the-symbol), so it is decidable by grep rather than by remembering which PR merged when. Verified: all seven cited symbols resolve; zero PR numbers and zero merge-event phrases remain in the carrier. Also fixes a real dangling reference the C0(c) split created: the census note in gunbc.v1_complexity_capability_census cited lens_contract_complexity, a row that no longer exists. Re-pointed at lens_contract_complexity_derived_kernel, which is the one a consumer surface would actually move -- optimality is AuditOnly permanently. * chore: regenerate drifted generated artifacts (ci auto-heal) * WIP: cost analysis * Stop the witness-admission row scan slicing UTF-8 prose mid-character The floor worker died exit 101 with no terminal receipt on witness_admission_entry_function_keys_from_source: WINDOW is a 400-BYTE budget applied to UTF-8 prose via after.len().min(WINDOW), so whenever byte 400 lands inside a multi-byte char the slice panics and takes the whole run down. The row that exposed it simply happened to put an em dash across that offset. Every other slice in that function takes its offset from find/split_once, which return char boundaries; this fixed offset was the only unguarded one. It now walks down to the nearest boundary, so an over-long row is truncated rather than fatal. Note the comment directly above already recorded an earlier panic in this same function, so the failure mode has form. Fixing the string instead of the scanner was the tempting move and it is the unmarked workaround DESIGN section 5 forbids: it would leave the defect armed for the next author who writes prose with an em dash in it. So the em dash stays in the row, and the scanner is what changed. PROVEN DISCRIMINATING BY EXECUTION, both directions: - unfixed: panics "byte index 400 is not a char boundary; it is inside em dash (bytes 398..401)" -- the production failure reproduced exactly - fixed: passes The fixture puts entry: and function: FIRST, mirroring real rows, because the scanner deliberately panics when entry: falls outside the window and that refusal is correct behaviour rather than the bug under test -- an earlier draft of this fixture tripped that arm and would have tested the wrong thing. The prose is a run of em dashes shifted by 0/1/2 ASCII bytes, covering every residue class mod 3, so at least one iteration is GUARANTEED to put the window edge strictly inside a character. The test deliberately does not model where the scanner sets search_from; pinning that offset would make the fixture fail for the wrong reason the moment the scanner moves. * Lane A C1: evaluate CostExpr at concrete SizeVariable bindings, with the CostSum binder lexically scoped The subject is semantic work, not hardware time: a CostExpr plus concrete bindings yields exact, unresolved, or refused modelled work. No duration, rate, or calibration constant enters this module. The load-bearing part is binder handling. v2.lens.cost.expr normalize_cost_expr_to_symbolic matches CostSum with the binder discarded, so a binder-dependent body projects a SymbolicCost naming a variable that is bound inside the sum - the magnitude may survive, the variable identity does not. This evaluator does not inherit that: env_bind prepends and lookup_bindings answers the head-most match, so a binder shadows an outer binding of the same identity for the extent of its body and only for that extent, with removal on exit structural rather than an unbind step. Proven by execution against a binder-discarding mutation: pinning the binder to Zero reds binder_dependent_body_is_summed_not_treated_as_invariant and binder_shadowing_is_scoped_and_removed_on_exit while leaving the invariant-body and zero-iteration witnesses green - which is the exact signature of the defect, and is why the existing C1 fixture (same variable for binder and bound) cannot see it. A second mutation answering zero for an unbound variable reds both missing-binding witnesses while zero_iterations_produce_exact_zero stays green: that pairing is what keeps a zero in a cost report unambiguous between nothing to do and nothing modelled. Carriers: v2.lens.cost.valuation CostEvaluation, CostValuationBinding, evaluate_cost_expr, evaluate_cost_expr_partially; std.algebra FreeSemigroup with v2.std.algebra non_empty_singleton / non_empty_append. The nonempty arms are carried by std.algebra FreeSemigroup - the free semigroup over T exactly as FreeMonoid is the free monoid over T, one algebraic axis at two identities. Its head field is the construction wall: an UnresolvedCost naming no free variable and a refusal carrying no cause have no representation, rather than being validated against. It is deliberately not the Refined<List<T>> spelling of the manual fixture, whose refinement predicate concedes the empty state is writable, and the NonEmptyList alias is withheld until that fixture retires so one name never resolves to two declarations. NonEmptyDiagnostics, FiniteSet, NonEmptySymbolChain and NonEmptyGrammarChoiceAmbiguityRows are the same shape monomorphised and dissolve onto it at their own already-declared triggers; that corpus-wide de-fork is not carried here. Stated gaps rather than silent ones: BoundedCost is declared-not-produced because its seed is a ceiling-valued binding, which is the sibling discrete-cost note's envelope scope; CostLog refuses its magnitude through the expression authority's own vocabulary until a cited integer-logarithm authority exists on std.nat. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Address review 49620 and the parent lane review: interval arithmetic, claim totality, quadratic accumulation, and a false citation Bounded-upper CostSum answered an EXACT value. combine_evaluation of ExactCost 3 and ExactCost 7 under nat_max reaches combine_known with both endpoints at 3, so bounded_or_exact collapses to ExactCost 7 — an exactness claim manufactured from an inexact input, sitting exactly where the envelope lane plugs its seed in. Replaced with evaluation_interval, which pairs the LOWER of one evaluation with the UPPER of a different one; an inverted interval refuses with InvertedCostInterval rather than being normalised by swapping the endpoints. Witnessed at its own seam because the arm has no producer yet; restoring the max spelling reds three of the four new witnesses. The PR body claim that the envelope lane adds a seed and no arithmetic was therefore false and is retracted. The Tier1 claim conjunction ran three of thirteen witnesses while its label asserted the refusal and scoping behaviour the other ten established, so CI could go green with the label false. every_valuation_witness_holds now enumerates every test fn in the file. Refusal accumulation was quadratic and reachable today: non_empty_append is linear in its left argument, so a body refusing under upper = u built u causes left-nested — and CostEffect refuses unconditionally in this slice. The causes were also IDENTICAL, because the body expression is fixed and only the binder value changes, so this amplified one deficit u times rather than counting u deficits. evaluate_summation now stops evaluating the body once the accumulator has settled; the soundness argument (a refusal here is a property of the body expression, not the binder's value) and its dissolve-on are on the carrier, and the new one-cause witness reds when the skip is removed. The FreeSemigroup grounding note carried a false citation, in the note arguing for single authority. Of the four carriers it named as each already carrying a migrate_when_nonempty_list_refinement_promoted trigger, grep says only two do, and a fifth instance was omitted. Corrected to five carriers, two triggered. Both surviving triggers are RETARGETED onto FreeSemigroup: they named the event as promoting the manual refinement to std, and this change decided that promotion is not the mechanism, so they would have been left waiting on an event that cannot occur as spelled. Also: the partial evaluation mode is stated as not being an escape from a refusal (swapping entry points to silence one is the author-side absorbing fallback); the order note now says causes accumulate WITHIN an arm and the dominated side's payload is dropped ACROSS arms; and the projection-path binder discard in normalize_cost_expr_to_symbolic is named as tracked debt with its trigger and the reason the existing fixture cannot see it. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Trigger the pull_request ci workflow, which never fired for this branch Zero GitHub Actions runs were created for either pushed SHA over roughly an hour, while sibling branches got ci runs throughout that window; the run was not awaiting approval either. main protection requires the ci check, so an empty synchronize is the only way to get one. Two approvals on the previous head are re-earned rather than assumed. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Recut to the exact core; fix the log arm reporting the wrong cause Operator ruling: scope to complete exact valuation. Kept — exact valuation at a complete binding set, CostSum binder scoping and shadowing, duplicate refusal, effect refusal, log refusal, and the earned-zero versus fabricated-zero distinction. Held on session/deep-owl-215-partial-bounded-hold — partial evaluation and bounded evaluation, sequenced rather than rejected, with both constraints that ride with them recorded on the carrier so they cannot be quietly undone: complete and partial stay TWO ENTRY POINTS over one fold, and the unresolved state must carry the residual CostExpr, not just free-variable names. CostEvaluation is two states here because at the exact core there are exactly two honest answers: the work is this number, or here is why it cannot be. Declaring an arm with no producer is rung inflation — and the bounded arm in particular was carried through an earlier revision while its arithmetic silently collapsed a two-endpoint envelope to its own ceiling. The log arm reported the wrong cause. It matched CostLog { base: _, .. }, ignored the base entirely, and answered UngroundedLogArgument for every non-refusing case — so base 0 read as an ARGUMENT problem, and a fully grounded argument was called UNGROUNDED, while v2.lens.cost.expr's normalizer right beside it already checked the base against its own InvalidLogBase. Two paths disagreeing about one fact. Now three distinct causes for three unrelated failures: an invalid base refuses through the expression authority's InvalidLogBase (cited, not re-minted), an unbound argument refuses as MissingSizeBinding like any other unbound size, and a valid base with an exact argument refuses as IntegerLogarithmUnavailable, which names the real gap and is countable against it. Restoring the base-ignoring arm reds both invalid-base witnesses; the base-zero and grounded-argument pair is the discriminating one, since the old arm gave both the same cause. All 16 witnesses green by execution, all 16 enrolled in the claim conjunction. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Enroll the claim conjunction as a test fn: it was the one orphan the naming-hygiene gate found The enroll-or-refuse pre-plan walk refused v2.test.lens_cost.valuation every_valuation_witness_holds as a plain fn unreachable from every test fn and test data — silent de-enrollment. It is the single root of the run: the ci job's failure was FloorUpstreamAlreadyRed with build=success and heal=success, which adds no verdict of its own. Note the remedy that does NOT work, since it is the obvious one: the claim data already referenced the helper by name — that is what it exists for — and a plain `data` does not count as reachability for this gate. Promotion to `test fn` is what satisfies it. Worth naming the shape rather than just fixing it: the conjunction was factored out to close review 49620's finding that the claim enumerated three of thirteen witnesses, and the helper that fixed a specification-without-execution defect was itself not executed by anything the gate recognises. Same class, one level out. The totality note now says so, so the next reader sees why the enrollment is deliberate rather than incidental. 17 witnesses green by execution; the local pre-plan walk that produced the CI refusal now completes clean. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Regenerate the stage0 seed: adding FreeSemigroup to a std authority drifted the self-host fixed-point regen_verify_gate_passes returned false because src/v1/stage0/src/std_algebra.rs did not contain the FreeSemigroup the emitter now produces from dag/std/algebra.dag. Adding a type to a std authority without regenerating the committed emitter output is exactly what the fixed-point gate exists to catch. Regenerated with regen_stage0 rather than hand-edited — the file is emitter output, and a hand-added struct would pass the diff while making the seed diverge from its authority. The diff is 7 lines, additive, only the struct. Order mattered: regenerate, rebuild the seed binaries from the regenerated sources, then verify with those binaries — regen_divergence_count=0, and 17 witnesses green against the rebuilt seed. The ci job's failure was again FloorUpstreamAlreadyRed with build and heal green, so regen was the only real signal. Note on the emitted shape, since it is visible in the diff: FreeSemigroup carries a _phantom: PhantomData<T> beside an already-inhabited T. That is the emitter's established convention for generic structs here, not something this type triggered — 25 of 39 structs in this one file carry it, including Magma<T> and the FieldOfFractions<R> pair DESIGN names as correctly grounded. There are zero construction sites for it in emitted Rust, so it imposes nothing on call sites. Whether the convention is a defect is a corpus-wide emitter question, not this PR's. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Zero is a two-sided annihilator: fix CostMul and symbolic_product together CostMul routed both sides through the generic refusal-dominates combiner, so CostMul of zero and CostEffect refused while the symbolic authority answered zero for the same expression — two paths disagreeing about one CostExpr, and the exact evaluator was the wrong one: a zero multiplicity means the body is never executed, so refusing because an unexecuted factor lacks an effect model is the did-no-work versus could-not-model conflation the earned-zero controls exist to prevent. Fixing only that would have traded one divergence for a narrower one, because the reference was itself ASYMMETRIC: symbolic_product matched a's arms first, including UnknownCost, and only then inspected b — so zero times unknown absorbed while unknown times ZERO returned unknown. Multiplication is commutative, so an operand order that changes the answer is a defect, not a style. Both paths are fixed in one motion and now agree in both orders. The annihilator lives in a multiplication-specific function and beats refusal-dominance, which governs every other combination here. That ordering is load-bearing and the carrier says so: checking refusals first reads like tightening a fail-closed path and would silently restore the defect, with only the two zero-times-effect witnesses reding. Controls, both directions on both properties, because an asymmetry defect cannot be caught by an asymmetric test: zero times unknown and unknown times zero both absorb; one times unknown and unknown times one both stay unknown; zero times CostEffect and CostEffect times zero are both ExactCost zero; one times CostEffect still refuses. Mutations discriminate — reverting multiply_evaluations reds both zero-order witnesses while one-times-effect still refuses; restoring the old arm order reds only the right-operand case. 24 witnesses green. The Blocking cost-wall baseline was re-run because this touches an authority feeding it: loop_iteration_floor (incl. its independent linear-times-zero control), disj_alternative_floor, bounded_summation (incl. existing_cost_lens_kernel_unchanged), atom_zero, expr_refusal and copied_port_derivation — 19 witnesses, all green. Witness accounting corrected: the claim label and note now say every LEAF witness, which the aggregating conjunction obviously cannot include itself in. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Qualify the one bare nat_max the second Nat authority made ambiguous Adding v2.std.nat.nat_max (the Peano Nat, needed by evaluate_size_expr's SizeMax and evaluate_cost_expr_in_env's CostMax) gave the name two declarations. test.claim.realization_schedule_critical_path is the single module whose import closure carries both authorities, so its bare call site stopped resolving and reddened the compile-clean gate. Qualified as std.nat.nat_max, matching the std.nat.nat_compare already qualified on the line above it inside the same witness. The four other bare nat_max call sites were checked by scoped compile rather than assumed safe -- dag/std/realization_width, dag/std/realization_measurement, dag/gunbc/econ/free_tier_serving and dag/gunbc/econ/scm_serving_model each compile with zero errors, so their closures do not carry both authorities and they need no qualification. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Close the two hygiene gates: exhaustive arms where possible, one rostered residue The floor reported three reds. Two roots, one of them not mine. NON-FOLD RESIDUE. Three wildcard arms landed with the exact evaluator. Two were avoidable and are now gone rather than declared: combine_evaluation and evaluate_summation match over CostEvaluation, which has exactly two variants, so `_ =>` became `ExactCost { value: .. } =>`. DESIGN section 5 puts construction above declaring a residue, and it buys what a roster row cannot -- a third CostEvaluation variant would now make both matches non-exhaustive and compile-clean would refuse, instead of the new variant being swept into a wildcard silently. multiply_evaluations is rostered, not "fixed". Its arms discriminate a nested VALUE (an ExactCost carrying Zero) rather than a variant, so enumerating would write the residual combine_evaluation call twice, underneath the arm order that multiply_evaluations_zero_note declares load-bearing. Duplicating that expression to satisfy a counter would make the function more fragile. Its reason says so, rather than reusing the generic nfr_reason_mint_era its neighbours carry. INERT CARRIER. Not from this change. Probing inert_carrier_names_live returned eleven live names against twelve rostered; the extra is ProcMeminfo, whose consumer landed in #7891 -- already an ancestor of this branch -- while the roster row stayed. origin/main carries both files byte-identically, so this witness is red on main too. The row is deleted here because it blocks merge and deletion is exactly what its own dissolve trigger prescribes; reported upstream so another lane does not duplicate it. Also records, in symbolic_product_zero_absorption_note, that the symmetry the annihilator fix established is CLASSIFICATION and not provenance: unknown times unknown still returns the left operand's diagnostic. That is pre-existing and module-wide (symbolic_sequential drops the same way), and closing it means widening UnknownCost to carry several diagnostics, which is its own change with its own witnesses. Green by execution: non_fold_residue_clean_holds, non_fold_residue_no_unrostered_or_stale, inert_carrier_no_unrostered_or_stale, and every_valuation_witness_holds over all 23 leaf witnesses -- the last because the exhaustive-arm edits rewrote live evaluation paths, not just roster data. Seed receipt reports unrostered=0 stale=0 live=149. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Roster #7965's two carriers and handle #7909's two git mock cases Both failing witnesses on this PR are MAIN-SIDE DEBT landed today, not this branch's. Neither constituent introduced them and neither of main's own runs executed the witnesses that catch them. inert_carrier_no_unrostered_or_stale. TerminatingOneShotFrontier and WitnessPurpose (dag/std/witness_purpose.dag, #7965) are a taxonomy landed ahead of its consumer: nothing outside their own module and their own test file references them, which is precisely the seed's inert predicate (declared once, referenced by a test, zero non-test references outside the declaration block). They get roster rows in the established shape, carrying the shared dissolve trigger -- a live consumer reads the carrier and the stale-roster check then forces the row's deletion. git_mock_consumer_is_total_holds. #7909 added git.Inspect.WorkingTreeStatus and git.Inspect.IgnoredFiles to git_published_mock_corpus without arms in materialize_git_mock, so both fell to mock_unhandled_rejection and totality failed. main publishes 20 cases against 18 arms; this adds the two arms. HOW THE OWNER WAS ESTABLISHED, because my first attribution was wrong. I found seven type carriers new versus main and inferred they were the inert ones -- true premise, unsupported conclusion, since none of the seven can satisfy the predicate (five are referenced by no test file at all; the other two are consumed in non-test fn signatures). The primitive is not directly invocable (no unique runtime declaration identity) and a second-worktree run is invalid because the corpus scan anchors to the compile-time-baked workspace root. So the rule was read out of the seed and reimplemented, and THE REPLICA IS VALIDATED AGAINST THE EXECUTED ORACLE: on this head it reproduces 13 inert against 11 rostered, exactly the unrostered=2 stale=0 the real run measured. Run over three trees it gives main 2 unrostered + 1 stale, pr-7932 clean, this branch main's 2 with main's stale already fixed -- so this branch was strictly better than main before this commit. GREEN BY EXECUTION, with the discriminating red on the real consumer: inert_carrier_no_unrostered_or_stale FAILED on this head before this commit and PASSES after; git_mock_consumer_is_total_holds likewise, alongside both omission RED controls (git_mock_omitted_member_is_red_holds, git_mock_omitted_show_tree_is_red_holds) still passing, so the added arms did not disarm the controls. No regen: neither module projects to a stage0 seed file and no seed .rs references the roster units, verified against a positive control (dag/std/algebra.dag does project, to std_algebra.rs). 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> Co-authored-by: gunbai-bot[bot] <289086189+gunbai-bot[bot]@users.noreply.github.com>

gunbc.ci_process_end_to_end already legislated this class — "no check present means not yet observed and never counts as satisfied; cancelled, timed out, refused by the infrastructure, and genuinely failed stay four different things" — but its displaced_cost was written as a PREDICTION ("an absent check currently reads the same as one that passed elsewhere"), so nothing made it rank. It now carries measurement, supplied by calm-ram-435 who had recorded the class before tonight: #7932 @ 493de34 (2026-08-07) a CANCELLED required ci folded into PASS; the tally reported MERGE CRITERIA MET while GitHub held mergeStateStatus=BLOCKED #8051 @ b4a8d5d two runs on one head; the concurrency-cancelled one pinned checks_state at PENDING beside a SUCCESS row #8059 (2026-08-10) merged on a cancelled run → 99 sites, two files THE SKEW RUNS BOTH WAYS. One cancelled row reads as pass in one direction and as pending in the other, so no single sign-correction closes it — which is why red_control now demands an executed control for EACH direction, and says the verdict derives from the authoritative merge state rather than from aggregating rollup rows. It also names the adjacent trap: mergeable: MERGEABLE is GitHub's conflict-freedom field, not a checks verdict, so it is never a second confirmation of anything. What #8059 cost is stated as the receipt rather than as a story: main could not derive its own generated artifacts, every PR adding an emitted module was blocked, three sessions each found it believing their own branch was broken, and two independently wrote the same 81-row repair within a minute. None of the 99 is a review gap and none is a review fix — each is a type error the compiler decides in milliseconds. The only thing that had to happen was for the checks to run. Verified: main_wet EXIT=0 with drift confined to this authority edit and its regenerated ROADMAP.md projection; lead-budget lens returns []. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_018gTJKsR5YdkaEc2SUGN9ff

…map onto the 2026-08-10 stop (#8116) * Roadmap: declare the infrastructure lanes, and make main the fleet's desired state The roadmap carried no node for most of what is now the priority. Verified against the authority before writing anything: zero hits for TasksMax, sccache, compile pool, build cache, Spark, ctrl-build, or the generated-file merge driver; one incidental hit for GitHub Actions ownership. The three "watchdog" hits are observation-collapse-watchdog-restatement, a display concept that happens to share the word with the runner recovery timer. The fleet lane's six rows all say the same shape - given a stated setting, apply it and read it back. None binds MAIN as where that stated setting comes from, which is exactly the gap: the mechanism half was modelled and the authority half never was. Meanwhile the work exists in design documents nothing on the roadmap points at. generated-file-conflict-policy.md is operator-ruled with four chartered lanes and no nodes. fleet-self-converge-enforcement-design.md names the self-converge timer as missing on every host and calls it the highest-risk gap. It also cited roadmap node 2-periodic-actuation, deleted in the 2026-07-27 refresh - repointed here to its successor fleet-anti-entropy-hygiene rather than left dangling. Sixteen nodes across five lanes, three of them new: fleet +5 main-revision-authority, atomic-convergence-verdict, runner-host-convergence, runner-broker-recovery, spark-inference-serving ci-placement +1 compile-pool-envelope ci-control (new) 4 owned-execution, executed-coverage-receipt, check-projection, actions-runner-retirement, remote-build-containment generated-artifact 2 projection-registry-containment, commit-policy-census ci-cost +2 arc-reconciliation, build-once-per-subject judgment (new) 1 mechanical-review-service Focus moves from the v1 exit and guarantee-ladder lanes to the infrastructure lanes. Nothing is deleted or parked: 98 hidden rows are counted on the page and one row restores the full view. The judgment lane is deliberately off the page while its prerequisite is on it. One witness repair, and it is not cosmetic. witness_projection_is_active_only rendered through roadmap_authority(), which applies the focus, while both its negative controls name ACCEPTED nodes. Any focus that stops selecting the namespace and P-derive lanes therefore makes them absent because HIDDEN, and the claim greens while proving nothing about acceptance. It now reads the focus-independent view, where absence can only mean accepted - the same reason witness_rendered_nodes_are_declared_or_derived already reads both documents. Proven discriminating by planting an active node's headline as a negative control (FAIL) and restoring it (PASS). Executed: generated-artifact drift gate green after regeneration; 44/44 roadmap_authority witnesses; 39/39 roadmap_page; 13/13 roadmap_frontier; 7/7 roadmap_emit. No acceptance receipts recorded. 123 nodes are active and only 9 carry a bound closing check; merged is not accepted, and manufacturing receipts for 51 merges would be the rung inflation this authority spends paragraphs forbidding. roadmap-receipt-continuity is the one mechanically decidable candidate and is left for the operator. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_018gTJKsR5YdkaEc2SUGN9ff * Compute fabric above CI, and the two nodes the wind-down inventory named Two corrections to the previous commit. ONE: the compute fabric was missing, and owning CI was standing where it should have been. Building, checking, regenerating, changing machines, serving models and eventually judging changes are four consumers of one fabric, not four execution systems, and the previous cut put the build story underneath ci-control - which makes owned CI the definition of a build rather than one caller of it. compute-exact-work-contract exact subject in, one of five typed endings out. A branch name or a working directory is not a subject. A provider that cannot serve the requested operation class refuses BEFORE running rather than answering a smaller question. compute-artifact-return-and-materialization a write-producing computation cannot report success while its declared outputs are unreachable. That is the exact live defect: a remote run finished successfully, produced nothing locally, and the stale binary left behind was compared against itself. It grounds on docs/plans/execution-spine-design.md rather than minting a parallel concept. That document is operator-SIGNED (FLAGS A-E, 2026-07-09) and its thesis is already that realization and materialization are the only downstream readers of the dependency view - which is the fabric being asked for. Minting a second scheduler beside it would have been the nicknaming DESIGN section 3 forbids, in the place it costs most. ci-owned-execution, ci-remote-build-containment, fleet-runner-host-convergence and fleet-spark-inference-serving now depend on it. ci-remote-build-containment is restated as what it actually is: a MIGRATION, whose only permitted additions are refusals, and which is deleted once its useful behaviour is a provider behind the contract. Remote execution does not live there. TWO: two nodes the inventory named that genuinely had no home. ci-floor-discovery-snapshot the ordinary and scoped workers each walk the corpus in separate processes; the second walk measures around 284 seconds. It carries the complete typed result, never a pass-or-fail flag, and a consumer that finds it absent, damaged or wrong-subject refuses instead of recomputing. Distinct from phased-single-process-ci, which removes the cross-PHASE duplicate; this removes the cross-WORKER one. compiler-declaration-floor a value was observed flowing through a field declared as the wrong type while all fifty-two behaviour witnesses over it stayed green. Five planted defects refused separately, plus an unchanged-behaviour control so the wall cannot be satisfied by refusing more of the language. No rung asserted - the claims carrier says where it stands. Focus adds compute. 100 hidden rows counted on the page. The focus note now states plainly what a focus is NOT. Off the page sits real retained work with real remaining boundaries, and nothing currently records why a hidden lane is paused or what restarts it - a lane frozen behind infrastructure, one draining to merge, and one parked because its hypothesis was falsified are three states that all read identically as absent. That is a missing dimension on the node, and it is named as landing next rather than papered over here. Executed: drift gate green after regeneration; roadmap_authority 44/44. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_018gTJKsR5YdkaEc2SUGN9ff * Deduplication before consumers, and the mechanism chain that removes preparation The compute contract as landed said exact subject in, typed ending out. It did not say identical computations collapse to one producer, and it did not say the fabric owns admission. Without both, handing agents a compute interface is a tidier way for ten callers to launch ten cold builds of one tree - the exact failure the lane exists to prevent. compute-deduplication-and-admission two requests naming the same computation are one piece of work: one producer, everyone else a consumer of its result. The fabric decides how many cold builds a machine carries, what the pool's total demand may be, which host serves a request, and what order competing work is served in - and tells a caller which of those it waits on. Requests differing anywhere in the identity must NOT collapse, and a capacity refusal is counted rather than becoming an invisible queue. It stands IN FRONT OF ci-owned-execution in the graph rather than beside it. Owning CI adds a consumer, and a consumer added before the duplication is removed multiplies the load instead of sharing it. The mechanism staircase, each removing a DIFFERENT duplicate: ci-scoped-worker-shared-substrate the second initialised world. Isolation keeps meaning separate mutable scratch and lifetime, never recomputing facts already fixed and immutable. ci-selection-before-preparation preparation that precedes selection. Selection is sharp about meaning and blunt about cost: it concludes the corpus is irrelevant after discovering, naming, rostering and indexing it. ci-streaming-realization the barrier between preparing and executing. Its acceptance property is that the first witness executes before the last selected entry is prepared. Chained by dependency edges rather than declared as a set, so at most the next one is startable and the limit on concurrent performance mechanisms falls out of the graph instead of being prose nothing enforces. phased-single-process-ci now sits behind the scoped-substrate row for the same reason. Width two is deliberately absent from the chain and stays parked: the tested implementation shared typed bytes while each worker still built its own world. compute_consumer_admission_sequencing_note records the ruling and, separately, that native realization and shared preparation are ONE programme. Emitting a native bundle is the right destination and the miniature is decisive at its scale, but the cited production enrolment delivered zero of three native and three of three fallback, so the required path took no benefit - and native bodies surrounded by duplicated preparation would still be bad CI. Executed: drift gate green after regeneration; roadmap_authority 44/44. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_018gTJKsR5YdkaEc2SUGN9ff * Review response: native cutover unblocked, thresholds out of RED controls, dedup bound to a real build Four review findings acted on. The lifecycle finding is answered by sequencing rather than by content and is stated at the end. NATIVE CUTOVER WAS STALE AND ORDERED BACKWARDS. native-selected-witness-bundle read "merge #7599 once controls clear" and "fallback counts trending to zero". #7599 is MERGED, and the cited production enrolment ran none of its three selected members natively and fell back on all three. So the mechanism exists, the required path takes no benefit, and the node was still describing the mechanism as the work. It is now a REPLACEMENT: emit the bundle, execute the selected population by direct call, and DELETE that population's interpreter scheduling in the same change. Interpretation survives only as a named differential control on a cadence, never as a success arm the production path falls through to. Fallback, interpreted and unavailable all at zero is the bar, not a residue to trend. Its two parent edges are removed and one is REVERSED: five-minute-ci-gate now depends on the cutover. The gate is an aggregate outcome, so making the cutover wait for it meant the one step that removes the interpreter from the required path could not start until the programme it contributes to had succeeded. The warm-merge edge went with it - no input dependency was ever shown; the bundle needs a selected population, an emitter and a toolchain, none of which merge admission supplies. The node now has no parents and is startable. witness_five_minute_ci_gate_program_chain_is_explicit CAUGHT THIS, which is what it is for. It pinned the old edge shape, so the reordering had to be deliberate rather than incidental. Updated to require the reversed edge and to assert BOTH old edges absent, so the previous direction cannot return silently. TIME THRESHOLD REMOVED FROM A SEMANTIC RED CONTROL. ci-scoped-worker-shared- substrate required "the scoped segment falls by at least three minutes". That is a tree-measured number standing in for a structural claim - the same shape DESIGN section 5 rejects for census pins. Replaced with what the row actually means: no second source loading, no second index construction, no second initialised world, same population, same outcomes, bounded scratch, no path back to cold construction. Wall, CPU and memory sit beside it as observations. A timer moving cannot claim a duplicate was removed, and a duplicate genuinely removed is not disqualified by a noisy host. DEDUPLICATION IS BOUND TO A REAL ARTEFACT BUILD. Its first slice was open to being demonstrated on two read-only checks collapsing into one verdict - the one case where duplicate work costs nothing, while the case that swamps the fleet is two cold builds. It now names two agent sessions requesting the same artefact-producing build, one producer, one compilation, one returned output, two attached consumers - and it depends on artifact return rather than standing beside it. LIFECYCLE: not in this PR, by agreement with the review. ProgramDisposition and the work-item agreement land first as their own change and this stacks behind them; RoadmapNode is constructed in 19 files and that shape change deserves an isolated review rather than riding a 24-node expansion. Executed: drift gate green after regeneration; roadmap_authority 44/44 with the chain witness green on the new direction. CI failure on b47d383 was infrastructure, established two ways: the regen job died at "Setup Rust" with rustup ETXTBSY (exit 126, 10s in, before any content ran) because runner slots share one home directory; and gunbc.roadmap_authority is absent from the 112-module regen input closure, so this change cannot alter regen output. regen_stage0 --verify run locally reports divergence count 0. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_018gTJKsR5YdkaEc2SUGN9ff * Lane 1 gets its node: commit-writer admission is scheduled first, not implied Review response (PR #8034 review, finding 1): the conflict-policy charter's four lanes were covered two-of-four, and the uncovered pair included lane 1 — the one the charter titles "FIRST: the live safety hole" and the one gunbc.repo_local_git_config's authority note names as the boundary a writer cannot pass. A generated-artifact lane whose first row is the population and whose absent row is the writer reads, on the page, as if the safety hole is scheduled. Now it is scheduled, as the parent of the lane-2/3 chain, matching the charter's own transaction ("prove no unmerged index entries — lane 1 predicate"). The node transcribes the charter's two refusal arms (unmerged-stage refusal; staged-blob conflict-marker-grammar refusal) and the operator's second-pass acceptance wall (complete staged-index observation, observed-not-declared classification, provenance-receipt fixture exemption, writer bindings as countable carriers). ROADMAP.md regenerated via generated_artifact_gate main_wet; all 44 roadmap witnesses green by execution with the node in place. Deferred per the same review's recommendation, recorded here: lane 4 (keyed rosters get set/map construction semantics) and the execution-spine-design.md doc-graph binding (needs a typed HandAuthoredDocBind anchor or a plan registration) stack behind the sequenced work-item PR. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_018gTJKsR5YdkaEc2SUGN9ff * Consolidation: quarry #8033, add the deterministic confidence lane, reframe owned CI Operator consolidation ruling (2026-08-08): #8034 is the sole roadmap authority branch; #8033's parallel edits port here rather than merging beside it. Ported from #8033, at their exact homes rather than as new identities: - placement-compile-pool-envelope absorbs the task-vs-outer-budget distinction as typed acceptance classes (ProcessAdmissionExhausted, OuterResourceEnvelopeKilled, EffectiveLimitMismatch, CompilePoolPlacementRefused) plus the 8.8%-of-visible-limit receipt. No second placement identity. - The five false-verification incident classes map to their existing exact homes in false_verification_incident_mapping_note; the proposed umbrella node does not port (a coarse identity over mechanisms this graph already decomposes is the §3 second authority). - ci-gate-contention-independent-verdict lands as the one genuine gap, recut qualitatively: host load cannot decide a semantic merge verdict; timeout is a typed execution outcome, never assertion failure; the cutoff is never widened. New lane: confidence-semantic-impact-query (owner confidence, on the focused page) — the deterministic repository-inspection product, explicitly independent of LLM/Spark; judgment-mechanical-review-service now depends on it as its grounding packet. First consumer is one real corpus query usable by a person, not a fixture suite. Reframed: ci-owned-execution's old floor is quarry + shadow oracle, not the template — obligations port only on a proven disagreement; first slice is the exact-subject → bounded population → emitted bundle → owned execution → typed receipt chain with the old path shadowing. Updated: the focus note's namespace standing now carries the 2026-08-08 exact-subject re-observation (A–D established, E/F unavailable under P2a triggers, frontier 2), superseding the stale none-of-six wording. Structure: 151 unique ids, acyclic, no dangling edges, all cited paths resolve. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_018gTJKsR5YdkaEc2SUGN9ff * chore: regenerate drifted generated artifacts (ci auto-heal) * Spark enrollment as fleet membership, and abstraction formation on the confidence chain Two operator directions (2026-08-08), landed as four graph changes. fleet-spark-host-enrollment: srv5/srv6 stop being hand-managed boxes. The endpoint rows are DERIVED as a downstream projection joining procurement identity and network allocation — re-typing the reserved address literal refuses (§3 fork), a reverse import into the network intent refuses (the measured cycle: procurement already imports it), and a second host-identity authority refuses. Enrollment carries a GB10 inference envelope, never runner-style thread capacity. Identity converge + reach ride the installed fleet key. fleet-spark-inference-serving now depends on it; runtime, model revision, auth and the collector bundle stay in the serving row, sequenced separately per the operator's "1 and 2 now". abstraction-candidate-discovery (owner confidence): descriptive grouping of subjects observationally equivalent under a NAMED lens, carrying the distinctions the quotient would erase, nearest existing authorities, and over-collapse/demand standing. Descriptive evidence only — the normative "these should share a layer" is an explicit bridge in the judgment row, per the abstraction-calculus mode-crossing rule. Deterministic: no Spark, no LLM. First slice hard-stops on an APPLIED acceptance (consumer migrated, duplicate deleted, receipts equal) so discovery cannot become an inert analysis service. REDs plant the three negative classes: keep-distinct on a load-bearing distinction, projection-missing on a downstream-join pair (the Spark endpoint session is the live receipt), demand-absent on a consumer-less candidate. judgment-mechanical-review-service broadens to the abstraction/modeling ruling vocabulary (existing-authority, likely-duplicate, candidate-new-abstraction, projection-missing, reprime-candidate, keep-distinct, over-collapse-risk, missing-consumer/actuator/readback, unknown) and gains the discovery dependency. Chain: confidence → discovery → judgment ← spark-serving; the Spark ranks and explains over exact packets, it never becomes the repository index. Structure: 153 unique ids, acyclic, no dangling edges; ROADMAP.md regenerated via main_wet; 44/44 roadmap witnesses green by execution. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_018gTJKsR5YdkaEc2SUGN9ff * Regenerate ROADMAP.md from the merged authorities Post-merge projection: the conflict on the generated file was taken provisionally and the bytes here are main_wet's output over the merged authority state, per the generated-file policy (regenerate, never hand-resolve). Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_018gTJKsR5YdkaEc2SUGN9ff * Bind the Spark standup accounting doc: main's floor has been red since #7972 landed it orphaned docs/plans/spark-standup-program-accounting.md landed in the #7972 omega with no HandAuthoredDocBind and no inbound link, so doc_graph_has_no_orphan_docs (and doc_graph_is_clean) have correctly refused every main push since the last green at 4cdcd57 — the doc-reachability wall working as designed, fleet-wide. Attribution receipt: replaying the doc-graph reachability rule (ROADMAP.md/DESIGN.md/runbook roots + registered plans + hand binds, markdown links as edges) over last-green main, current main, and a candidate branch shows exactly one orphan appearing in the window, this doc. The bind anchors on the physical facts the doc records — gunbc.dgx_spark_procurement spark_a3ee_reservation / spark_3bd5_reservation — and its dissolution names the follow-up the doc itself declares: the Spark standup program landing as roadmap rows, findings migrating to typed carriers, then the doc registers as a plan or deletes and the bind deletes with it. Verified by execution: doc_graph_has_no_orphan_docs and doc_graph_is_clean both PASS on this tree; both FAIL on its parent. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_018gTJKsR5YdkaEc2SUGN9ff * Floor fixes: four boundaries back inside the brief budget; ROADMAP reprojected The floor's brief-budget witness (100 words of authored boundary per ticket, gunbc.roadmap_page ticket_brief_word_budget) redded on four nodes this branch authored or lengthened: ci-owned-execution (104), commit-writer-admission (106), abstraction-candidate-discovery (114), judgment-mechanical-review- service (114). Each boundary is trimmed to <=100 tokens with no clause of the bar dropped — overflow either compressed or already carried by the node's other fields (abstraction discovery's no-model-server fact lives in its out_of_scope). Max boundary is now 99. The sibling doc-graph reds are main's breakage (the #7972 omega landed docs/plans/spark-standup-program-accounting.md orphaned; every push since last-green 4cdcd57 refused): fixed for the fleet in PR #8053 and carried here by cherry-pick so this branch's floor does not wait on that merge. Verified by execution on this tree: witness_ticket_brief_budget_holds_and_reds PASS, doc_graph_has_no_orphan_docs PASS, doc_graph_is_clean PASS, roadmap suite 44/44, regen ExitSuccess. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_018gTJKsR5YdkaEc2SUGN9ff * Final Spark/convergence recut per executive verdict Narrow Spark enrollment to membership/profile/endpoint with honestly Unobserved cells; join lifecycle cells into the fleet convergence verdict and name the one-producer defect; spell the inference-serving internal path; make the fleet participation migration the first abstraction-candidate-discovery specimen. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_018gTJKsR5YdkaEc2SUGN9ff * Add ci2-complete-native-cost-receipt: whole-corpus native shadow experiment as the bounded cutover's immediate successor Operator direction 2026-08-08: keep CI2-0's bounded acceptance attainable; measure emission/compilation/execution walls separately over the complete roster, then decide from the measured warm wall whether per-PR selection remains load-bearing or is deleted. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_018gTJKsR5YdkaEc2SUGN9ff * CI-0 recut: one row, one PR — fallback deleted, whole corpus classified, emitted, executed, authoritative (operator 2026-08-08) Collapses diagnosis-precursor / bounded-cutover / whole-corpus-receipt into a single state transition on native-selected-witness-bundle; deletes the ci2-complete-native-cost-receipt row added earlier today. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_018gTJKsR5YdkaEc2SUGN9ff * chore: regenerate drifted generated artifacts (ci auto-heal) * Add roadmap-serve-emitted-realization: dissolve the interpreted serve scaffold via emit-on-demand (srv1 outage 2026-08-08) Interpreted concat clones its accumulator (quadratic); emitted concat moves (linear). Order: emit wiring first, content-hashed bodies second, concurrency last; request deadline regardless; belt GcpProjectId fix folded in. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_018gTJKsR5YdkaEc2SUGN9ff * Reconcile #8034 per operator review: record #8054 failed acceptance on confidence-semantic-impact-query; collapse five-minute-gate parent onto the CI-0 one-PR child (cursor review 50559 §3 finding) Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_018gTJKsR5YdkaEc2SUGN9ff * Wire compiler-declaration-floor into guarantee_ladder_edges (cursor review 50566) Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_018gTJKsR5YdkaEc2SUGN9ff * Catch #8034 up to the day's rulings: CI-0 staged (3-member merge, producer successor, v2-only terminal), general-witness-body-producer row with construct census, CONFIDENCE post-rework standing, structural fork detector as abstraction-discovery first slice Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_018gTJKsR5YdkaEc2SUGN9ff * Operator amendment: two judgment modes over one evidence substrate, semantic judgment receipt, model-selection successor, serving infra acceptance, participation-criterion detector, forward-intent refusals Incorporates worker corrections: participation over shape as the mechanical criterion; consumer-verb stringly-enum class moved into the deterministic detector; runner-vs-inference capacity control marked not-yet-built. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_018gTJKsR5YdkaEc2SUGN9ff * Wire fleet-runner-broker-recovery into the fleet graph (cursor review 50583) Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_018gTJKsR5YdkaEc2SUGN9ff * Wire ci-executed-coverage-receipt and ci-gate-contention-independent-verdict as prerequisites of ci-check-projection (cursor review 50587) Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_018gTJKsR5YdkaEc2SUGN9ff * De-number the gate program prose: dispatch order follows graph edges (cursor review 50595 non-blocking finding) Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_018gTJKsR5YdkaEc2SUGN9ff * CI2-0 mandate recut: one node, complete v2 witness-execution cutover in #8043 — producer successor row deleted (operator mandate 2026-08-08) The census's 3-of-9,353 was circular (restated enrollment, never attempted realization); the fixture route's limits were mistaken for compiler limits. No successor PRs; canonical-pipeline wiring, per-identity semantic-kind x realization-standing from actual attempts, predecessor deletion, and the whole-population receipt all land in #8043. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_018gTJKsR5YdkaEc2SUGN9ff * Dirty-worktree verification as compute's first daily consumer (operator verdict 2026-08-08) Amends compute-exact-work-contract first_slice: exact dirty-tree snapshot runs all affected (or explicitly conservatively complete) v2 tests, exact receipt at most 5s warm, BaseUnstable a distinct answer; confidence optional for narrowing, never correctness. No new node. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_018gTJKsR5YdkaEc2SUGN9ff * V2-LENS-0 node and the two-command product interface (operator convergence mandate 2026-08-09) Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_018gTJKsR5YdkaEc2SUGN9ff * Heal main: link the #8062 probe receipt, admit its specimen module to the debt ceiling, read trim's input in its seam Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_018gTJKsR5YdkaEc2SUGN9ff * chore: regenerate drifted generated artifacts (ci auto-heal) * Move the probe-receipt link to the emitting plan authority (review 50763) Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_018gTJKsR5YdkaEc2SUGN9ff * Regenerate model-realization-fork.md from the amended authority Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_018gTJKsR5YdkaEc2SUGN9ff * Hoist in-body annotations to module grain in two witness files (12 §4c refusals) Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_018gTJKsR5YdkaEc2SUGN9ff * V2-LENS-0: dispatch trigger, checkpoint structure, permanence laws (operator ruling 2026-08-09) Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_018gTJKsR5YdkaEc2SUGN9ff * Record the four-lane closeout and the root it identified Four lanes (CONVERGE, CI RESET, CI2-0, DEVBOOT-0) closed 2026-08-10 with zero displacement between them. Each was asked for the root with evidence and explicitly invited to reject the manager's hypothesis; all four declined to confirm it. The re-cut that matters: of 11 rejecting members in one real std closure, 5 are normalize contradicting its OWN declared contract (retaining wrapper declarations, then rejecting the tree those retentions live in via its own module-grain well_formed gate) and only 3 are genuine frontend gaps. A broken contract is a bounded repair; a missing capability is a program. Synthesis across the four: nothing could be verified incrementally — the acceptance contract demanded the whole corpus and moved between measurements, the mechanism demanded 60-75 minutes and gated deploys as well as merges, and the instruments built to escape both were themselves unverified. Written to git rather than left in message threads because five sessions were archived today holding measurements, one leaving a PR whose premise had been reverted underneath it. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_018gTJKsR5YdkaEc2SUGN9ff * Heal main's SubstrateLongLaneRow schema break, and reconcile the roadmap onto the 2026-08-10 stop Two things, the first a live main repair found while validating the second. MAIN IS RED AND NOTHING WAS GOING TO CATCH IT. #8114 (24ff2da) added 18 SubstrateLongLaneRow literals carrying `dissolve_on:`; #8059 (45e7024) merged after it and renamed that field to `dissolution: DissolutionCondition`. Each PR was green alone and the pair is red — the merge race a merge queue exists to prevent, landing during the runner outage, so no run has reported it. All 18 now carry `unbound_dissolution(description: ...)` and name their sibling row explicitly rather than saying "same as sibling row", which is the vague prose #8059 was eliminating. Verified: compiling ci_layer_roots' closure emits zero SubstrateLongLaneRow diagnostics (the residual exit=1 is the pre-existing 25-row §4c population in host_phase_status_witness_test.dag, untouched here). ROADMAP RECONCILIATION. ROADMAP.md is a generated artifact; the authority is dag/gunbc/roadmap_authority.dag. Baseline control first: the unedited authority reproduces the committed ROADMAP.md exactly, modulo one trailing newline the CLI adds — so the instrument was validated before it was trusted. The structural fix: edge(five-minute-ci-gate -> native-selected-witness-bundle) is DELETED. The entire CI-cost chain — discovery snapshot, scoped substrate, early selection, streaming — hung beneath a node that is now stopped and can never be accepted, so every floor row was unschedulable. It was also backwards on the merits: a 3,290s floor carries 97s of witness evaluation, so an infinitely fast evaluator leaves ~97% of the floor standing and native execution was never the CI-cost lever. Four rows follow from that: - native-selected-witness-bundle re-cut from "complete cutover in one PR" to the self-host frontier it always was (operator root 3). The frontier is stated as measured: of 11 rejecting members in one real 15-file std closure, 5 are normalize contract violations, 2 the graft guard working, 3 genuine LEX/PARSE gaps, 1 uncaptured. A broken contract is a bounded repair; a missing capability is a program — they do not schedule together. The sugar chain is deferred WITH its SHAs (6888b97 -> f62e838 -> c84842c): cherry-picked clean onto main it is 5/5 FAIL, because separability was asserted from a description and refuted by execution. - five-minute-ci-gate carries the measured decomposition rather than a narrative: 1,422s discovery/setup, 690s scoped worker, 97s evaluation; duplicate discovery 295.7s + 284.3s; selection paid after preparation; one missing typed key costing 82-96% of a cold symbol-index build. - five_minute_ci_gate_program_note updated, because DESIGN cites it as the single authority for sub-lane scope and dispatch order and must not carry a second copy. - v2-lens-suite-execution's trigger ("after CI2-0 terminal acceptance") is unreachable and now says so. It KEEPS its dependency deliberately: its own handback demands zero v1 lens-body executions, so relaxing the trigger would only move the frontier into the handback. Regenerated ROADMAP.md from the edited authority; the lead-budget lens returns [] (no violations). Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_018gTJKsR5YdkaEc2SUGN9ff * Heal the second half of the #8059 schema break: HasTrigger is not a constructor wise-boar-328 hit a symptom my first commit did not cover, reproducing it independently while merging main into #8109. Checked rather than assumed, and it is real: dag/gunbc/doc_graph_roots.dag calls `HasTrigger { text: ... }` in 81 places and HasTrigger is DEFINED NOWHERE IN THE TREE. All 81 were introduced by #8059 (45e7024) itself — the same PR that renamed SubstrateLongLaneRow.dissolve_on. So that PR shipped a nonexistent constructor 81 times and merged during the runner outage, where nothing executed it. The intended form is not a guess. The field is typed: HandAuthoredDocBind.dissolution: PlanRetirement PlanRetirement = PlanRetiresWhen { condition: DissolutionCondition } | PlanHasNoRetirement and the file ALREADY IMPORTS both `PlanRetiresWhen` and `unbound_dissolution` while using neither — the imports were written for the correct form and the constructor call was wrong. Each payload is free text describing when the plan retires, which is UnboundDissolution by construction (BoundDissolution carries a DeclarationRef, not prose), so every row becomes: dissolution: PlanRetiresWhen { condition: unbound_dissolution(description: ...) } Verified by execution: compiling doc_graph_roots' closure emits zero errors and zero HasTrigger/PlanRetirement/dissolution diagnostics. The residual 25 hard diagnostics are the pre-existing §4c annotation population in host_phase_status_witness_test.dag, untouched and unrelated. Main needed both halves; the first commit alone would have left it red. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_018gTJKsR5YdkaEc2SUGN9ff * The cancelled-check row stops predicting and carries its three receipts gunbc.ci_process_end_to_end already legislated this class — "no check present means not yet observed and never counts as satisfied; cancelled, timed out, refused by the infrastructure, and genuinely failed stay four different things" — but its displaced_cost was written as a PREDICTION ("an absent check currently reads the same as one that passed elsewhere"), so nothing made it rank. It now carries measurement, supplied by calm-ram-435 who had recorded the class before tonight: #7932 @ 493de34 (2026-08-07) a CANCELLED required ci folded into PASS; the tally reported MERGE CRITERIA MET while GitHub held mergeStateStatus=BLOCKED #8051 @ b4a8d5d two runs on one head; the concurrency-cancelled one pinned checks_state at PENDING beside a SUCCESS row #8059 (2026-08-10) merged on a cancelled run → 99 sites, two files THE SKEW RUNS BOTH WAYS. One cancelled row reads as pass in one direction and as pending in the other, so no single sign-correction closes it — which is why red_control now demands an executed control for EACH direction, and says the verdict derives from the authoritative merge state rather than from aggregating rollup rows. It also names the adjacent trap: mergeable: MERGEABLE is GitHub's conflict-freedom field, not a checks verdict, so it is never a second confirmation of anything. What #8059 cost is stated as the receipt rather than as a story: main could not derive its own generated artifacts, every PR adding an emitted module was blocked, three sessions each found it believing their own branch was broken, and two independently wrote the same 81-row repair within a minute. None of the 99 is a review gap and none is a review fix — each is a type error the compiler decides in milliseconds. The only thing that had to happen was for the checks to run. Verified: main_wet EXIT=0 with drift confined to this authority edit and its regenerated ROADMAP.md projection; lead-budget lens returns []. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_018gTJKsR5YdkaEc2SUGN9ff --------- Co-authored-by: Brian Searls <briansearls1@gmail.com> 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>

gunbc-ci-auto-heal and others added 2 commits August 6, 2026 19:07

gunbc-ci-auto-heal and others added 5 commits August 6, 2026 20:00

Merge remote-tracking branch 'origin/main' into session/deep-owl-215

8b86900

gunbc-ci-auto-heal and others added 2 commits August 7, 2026 03:31

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

Witness purpose taxonomy, derived envelope compare, and placement projection #7893

Closed

2 of 3 tasks

gunbc-ci-auto-heal and others added 2 commits August 7, 2026 06:12

Merge remote-tracking branch 'origin/main' into session/deep-owl-215

94cdca4

# Conflicts: # dag/gunbc/non_fold_residue.dag

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

Consolidate the cost-analysis lane: fold #7932 onto current main (carries #8010's witness retirement) #8027

Merged

gunbai-bot Bot closed this Aug 7, 2026

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

Lane A cost valuation #8028

Closed

6 tasks

Navigation Menu

Repository navigation

Lane A C1: evaluate CostExpr at concrete SizeVariable bindings, with the CostSum binder lexically scoped - #7932

Lane A C1: evaluate CostExpr at concrete SizeVariable bindings, with the CostSum binder lexically scoped#7932
gunbai-bot[bot] wants to merge 11 commits into
mainfrom
session/deep-owl-215

gunbai-bot Bot commented Aug 6, 2026 •

edited

Loading

Uh oh!

gunbai-bot Bot commented Aug 6, 2026

Uh oh!

gunbai-bot Bot commented Aug 7, 2026

Uh oh!

gunbai-bot Bot commented Aug 7, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

0 participants

Conversation

gunbai-bot Bot commented Aug 6, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

What this is

The load-bearing part: binder scoping

The log arm reported the wrong cause

Evidence, by execution

Nonempty carrier

Also in

Scope guards honoured

CI note

Uh oh!

gunbai-bot Bot commented Aug 6, 2026

Uh oh!

gunbai-bot Bot commented Aug 7, 2026

Uh oh!

gunbai-bot Bot commented Aug 7, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

0 participants

gunbai-bot Bot commented Aug 6, 2026 •

edited

Loading