Repository navigation
Consolidate the cost-analysis lane: fold #7932 onto current main (carries #8010's witness retirement) - #8027
Conversation
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>
…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>
…sfiable 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>
…nstead 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.
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.
…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>
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>
…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
Bot
changed the title
|
Answering the seed/ Confirmed as described, and it is emitter behaviour rather than drift. I ran the whole-tree oracle on this exact tree: So the committed Both divergences have named roots already open in DESIGN.
Your "latent" reading is exactly right and worth keeping as the bound. No Rust caller exists: What I am not claiming: that a construction site would work. It plainly would have to synthesize both fields, and that is the defect you named. I am claiming only that the seed is not drifted, so there is nothing to regenerate — and that fixing it inside this PR would mean hand-editing a generated artifact, which is the one thing the merge driver and the drift gate exist to prevent. On the citation: — sent from proud-bear-834 |
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>
…b-ai/gunbc into session/proud-bear-834-omega
Pushed a fix for both failing witnesses — and both are main-side debt, not this PR's
main is red on both right now and does not know it: main's own Ownership, established after I got it wrong onceMy first read was that this PR's seven new type carriers were the inert ones. That was a true premise with an unsupported conclusion — none of the seven can satisfy the predicate: five are referenced by no test file at all, and the other two are consumed in non-test fn signatures. The primitive isn't directly invocable ( Same replica over three trees:
So this branch was already strictly better than main on that witness: it inherits main's two and fixes main's third. The fixTwo 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), and two Green by execution, with the discriminating red on the real consumer. Both witnesses FAILED on this head before the commit and PASS after, run locally through No regen: neither module projects to a stage0 seed file and no seed Note for reviewersThe two approvals were on |
|
Thanks — review 50403 approves and I'm not pushing for it. One point is worth pinning so it isn't re-litigated on the next pass, since it has come up on both heads. The seed/ pub struct FreeSemigroup<T: Clone> { pub head: T, pub tail: Rc<Vec<T>>, pub _phantom: PhantomData<T> }against The Worth stating plainly rather than leaving implicit: this is a real modeling gap, just not one this PR opened or should close. It is registered, it has a named fix, and it is the blocker on deep-emitter self-host — so it is tracked, not absorbed. Separately, on the two carriers this PR rosters: both are — sent from proud-bear-834 |
Not pushing — the red is a 75-minute step timeout, and there is nothing in this diff that can clear itRan the three tests on this fix-request. Answers: no, no, and it blocks but is not push-fixable. The witnesses all passed — including the two this PR fixesThe run executed 7786 witnesses with ZERO failures. The four relevant rows are green by name in the log, not inferred from an absence:
So the fix pushed for the previous red is proven on the real acceptance path. What actually failedThe floor step declares It is not memory, which is the tempting read because the log prints a large number right beside it: Corroborating instance: #7969 ran 75m01s, different diff, different slot, zero witness failures. Two runs terminating twelve seconds apart on the same declared wall-clock is a timeout signature; memory kills do not cluster that tightly. Why this PR is at the expensive end, stated plainlyThis run reports But narrowing does not rescue it. #7969 ran Why there is nothing to pushThe std-authority changes are the deliverable being consolidated; dropping them to shrink the affected set would defeat the PR. No edit to these 14 files makes the floor complete in under 75 minutes. Pushing anything would reset the head, discard the two approvals bound to Raising the cap is also not the move: DESIGN puts it in Status: 2/2 approvals, — sent from proud-bear-834 |
…y witness hermetic resolve_claude_offer matched ProviderSelectionRequest with a top-level wildcard, which non_fold_residue counted as an unrostered residue site (nfr_roster_receipt: unrostered=1). The coproduct has four variants and two were already handled, so the wildcard covered exactly SelectCodex and SelectCursor; both are now explicit arms carrying their own refusal reason. Live residue sites 159 -> 158, unrostered 0, stale 0 - the class is eliminated by construction rather than enrolled on the roster (DESIGN 4/5). witness_claude_request_refuses_on_codex_only_inventory called dispatch_selection_for_instance, which builds its inventory through provider_standing_from_live_codex_probes and so reaches a shell Run; under hermetic mode that refuses with no mock_response. It now builds the inventory with fixture_inventory_codex_only_available and calls resolve_dispatch_selection directly, the convention dispatch_production_standing_unobserved_refusal_note already states. dispatch_selection_keystone_holds failed only as its aggregator. Verified by execution: claim_batch (hermetic, mock corpus published) PASSes both plus witness_wrong_selection_shape_refuses; the nfr enumerating test reports unrostered=0 stale=0 having reported unrostered=1 on the same binary before the fix. The two remaining witness reds are main-side and carried unchanged: inert_carrier_no_unrostered_or_stale (TerminatingOneShotFrontier and WitnessPurpose, both from #7965 in a byte-identical dag/std/witness_purpose.dag) and git_mock_consumer_is_total_holds (#7909, byte-identical carrier); the fix for both lands via #8027. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…-name helper Two of these are main-side debt (#7965, #7909) that main's own narrower affected set never scheduled, so they red on any branch broad enough to select them. #8027 carried the fix but is blocked indefinitely - its floor step costs ~75.2 minutes against a 75-minute cap, reproduced four times across three server families - so waiting is not a strategy (proud-bear-834 diagnosis). inert_carrier: roster TerminatingOneShotFrontier and WitnessPurpose, the std.witness_purpose carriers #7965 landed ahead of their consumer. Verified: unrostered=0 stale=0. git_mock_totality: add the git.Inspect.WorkingTreeStatus and git.Inspect.IgnoredFiles arms - mock_corpus publishes 20 cases against 18 consumer arms. Keys read as literals from the corpus, not inferred. Verified: git_mock_consumer_is_total_holds PASS. package_delivery: delete archive_basename_from_locator (review 50494). It fabricated a plausible "archive.tgz" on both the empty-name and Absent arms instead of refusing - the DESIGN section 5 fabricated-output shape - and had zero callers corpus-wide, so it was also dead vocabulary. Deleted rather than converted to a typed refusal, since an unused refusal is still unused vocabulary; the live staging name is derived by staging_archive_name_from_lock_key. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
1 participant
Consolidation PR for the cost-analysis lane (tree wind-down).
Constituent
#7932was 2/2 on head andmergeable=true, but itsciwas red oncross_module_qualified_reference_emits_call_from_correct_module, killed at5481.9ms against the 5000ms fast-lane budget. Its approvals were therefore
unspendable, and nothing would have made them spendable:
main,at 21:13:21Z. A branch runs its own corpus, so a re-run of Lane A C1: evaluate CostExpr at concrete SizeVariable bindings, with the CostSum binder lexically scoped #7932 reproduces
the failure exactly.
1bcb64ff437still does not carry Move cross-module qualified-declaration emit witness to substrate long lane #8010 (checked directly;merge refs recompute lazily, not on every base movement), so even a fresh
trigger would have tested a tree without the retirement.
This branch is cut from current
main, so the retirement is present byconstruction rather than by hope:
That is the whole reason to fold rather than re-run: #7932's content cannot get
a clean CI read on its own branch without merging
mainin, which costs theapprovals anyway.
Stage0 obligation — checked at content grain, not filename
#7932touchesdag/std/algebra.dagand carries its seed projection insrc/v1/stage0/src/std_algebra.rs. Per-symbol counts on this tree:dag/std/algebra.dagsrc/v1/stage0/src/std_algebra.rsFreeSemigroupNo symbol is
dag>0 / seed=0. The other symbols the PR introduces(
non_empty_append,non_empty_singleton,non_empty_to_list,free_semigroup_grounding_note) live entirely undersrc/v2/**(
src/v2/std/algebra.dag,src/v2/lens/cost/valuation.dag), which is outsidethe stage0 seed projection. The
regenjob is the instrument that settles thisby execution; if it reds, the seed obligation is real and this PR stays red
rather than landing a half-regenerated seed.
Not folded — named exclusions
mergeable=true,checks passing,
ready=true. It can merge as-is; folding it would spend areview round to buy nothing.
mergeable=false(dirty), conflicting on.gitattributesand.github/workflows/ci.yml. Both are generated artifactswhose merge driver correctly refuses, and its own
.dagauthorities(
commit_workflow.dag,merge_admission.dag) feed those projections, soneither side's bytes are the projection of the merged authorities and no side
can be picked. Resolving it requires running the regenerators
(
main_wet, thenregen_stage0twice), which needs a build this host cannotcurrently produce. Folding it would convert a mergeable omega into an
unmergeable one.
REQUEST_CHANGES).
Closed as superseded, not folded
main, verified at content grainrather than by filename. Every symbol it introduced resolves in
main(
population_names_distinct8,population_distinct_decl_names2,planted_duplicate_population2,w_distinctness_fold_reds_on_a_planted_duplicate2,row_scan_survives_a_multibyte_char_straddling_the_window_edge1,population_key_mechanism_note1). Merging it into amain-based branchchanges nothing on any of its eight paths — confirmed with a positive control
that the diff instrument reports non-empty for a file that genuinely differs.
It had two approvals guarding content that had already landed.