Repository navigation
Accumulator-copy analyzer misses the fold/list_append specimen: gate_red_quadratic_rejects red on main (dark long-lane row) - #11142
Conversation
…argument's value
v2.lens.complexity_accumulator_copy.analyze port_reading took its identifier
census with collect_value_identifiers over the WHOLE ^dag_surface_arg capture,
which for a named argument `left: acc` carries the LABEL as well as the value.
Measured on the specimen: the list_append call capture is found, it has two
ports, and port 0 reads PortComputedExpression with mentions = 2 containing both
^left and ^acc. So `idents == 1` was false, the arm that consults
arg_value_symbol and yields PortBareName { name: ^acc } was unreachable, and
classify_copied_port took ^copied_port_computed_argument -- the undecidable
residue, non-gating by design. No Poly2Suspect was minted and
accumulator_copy_compile_gate ACCEPTED the textbook quadratic.
It is none of the three candidates the brief offered: the shape matcher finds
the call, the carrier is bound (count_fold_sites bound_only > 0), and
list_append is rostered (copied_port_citation_list_append). Because every .dag
call uses named arguments, the bare-name arm was unreachable for the entire
corpus, which is why the lens has never minted a suspect on ingested source.
port_reading now reads the argument's VALUE subtree, the same
^dag_surface_primary_expr node arg_value_symbol already reads through, so the
census and the symbol read ask one authority what the argument IS. Nothing is
widened: the no-value-capture arm still reads the whole capture, so it stays an
over-approximation that degrades toward the refusal causes and never toward
clean.
Second latent red on main, same subject and the class gunbc#11025 already
fixed once: v2.test.long.accumulator_copy_fold_analysis findings_of passed the
sealed NormalizedTree where a Node is wanted (missing .root, dead since the
BL-1 seal in #10439), so all 21 of its witnesses were dark with
"no field 'kind' on type 'NormalizedTree'".
Evidence: all 7 witnesses of accumulator_copy_compile_gate_test now PASS,
including gate_red_quadratic_rejects, which FAILs on the same tree without the
lens change. The three diag_* controls that discriminated the failure are
enrolled beside gate_red/gate_green, in the census obligation's witness list
and in the witness_deferral_freeze identity join for that entry.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01H2w1vtH78R73h7qyTK7Ah6
…ld fail-open Un-darkening v2.test.long.accumulator_copy_fold_analysis puts 17 witnesses dark-to-green and 4 dark-to-visibly-red. Attribution is measured, not assumed: a control worktree carrying ONLY the .root repair, with the port_reading change absent, fails all four identically, so they are pre-existing and unmasked rather than introduced. A discriminating probe separates them into three defects, and each is rostered at its own grain per the ruling from eager-raven-113. let_alias_is_proven_suspect is NOT a lens fact and NOT a fixture typo: staged probe shows tokenize ACCEPTS and v2.compiler.parse parse_module REJECTS the specimen, so it never reaches normalize or the lens, and the witness's `Absent => false` reports a stage refusal as a lens verdict. A six-cell ingest matrix narrows the refusing shape: a let binding the fn literal's own parameter standing immediately before a call statement. Renaming the binder still refuses; an unbound RHS, a literal RHS, a second let, and the one-line spelling all parse. Trigger: the grammar admits that statement shape. let_fresh_binding_is_provably_clean is a false refusal that FAILS CLOSED -- the lens over-refuses a provably fresh binding with ^copied_port_computed_argument, which rides the non-gating Accepted channel, so no quadratic can be admitted through it. named_step_fold_refuses_accumulator_unread and report_counters_state_the_domain are one silent fail-open (DESIGN section 5): for fold(xs, init: 0, f: step) the normalized tree carries NO lowered Loop and NO surface fold call, count_fold_sites returns 0, and the lens's own ^fold_accumulator_unread arm in fold_family_carrier is unreachable -- a written, located refusal no input can trigger, which reads to a reader as coverage. Filed as gunbc.recurring_failure_mode.fold_shape_visible_to_no_lens: found at below the floor, ceiling structurally guaranteed, trigger naming the capability with the suspected home in v2.compiler.fold_lowering / body_lowering_fold rather than the lens. Deliberately not repaired here -- that scope is unbounded inside a PR whose subject is the port reading. The four also leave the gunbc.witness_deferral_freeze FrozenPathDeferral row for that entry: a witness leaves discovery for ONE reason, and carrying both an exact admission and a path policy is the dual representation that module exists to replace. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01H2w1vtH78R73h7qyTK7Ah6
…zen roster Review 64325 is right and the gate behind it is real. The previous commit appended three identities to gunbc.witness_deferral_freeze frozen_path_deferrals so the new diag_* controls could sit beside the gate's red/green controls. That roster is frozen against GROWTH by the cli_run collect_frozen_path_deferral_additions monotonicity gate, which is a key set-difference against the diff baseline -- so a net -4/+3 does not cancel, the three new keys refuse, and the push would have redded CI. DESIGN section 3 says the same thing for a frozen X: no new rows on its growth surfaces. The deeper point is the one the module itself states: for a GREEN witness under an offline home the only exact cadence available is QuarantineProbeExpectRed, which is a declaration that a witness is RED and cannot be written truthfully about a green one -- so the compliant move is not to author there. The brief said to enrol these controls "beside" the existing ones; the authority docs say a green witness may not live in a home that executes nothing, and the docs win. So the three discriminators move to src/v2/test/claim/complexity/accumulator_copy_compile_gate_diag_test.dag, which per-PR discovery DOES execute (the complexity exclusion is the narrower claim/complexity/accumulator_copy_roster_gate prefix, not the directory), the freeze roster returns to its main content for that entry, and the census witness rows repoint to the executing path and module. Measured in the new home rather than assumed affordable: all three PASS at cpu=851ms / 1022ms / 1051ms, wall <= 2003ms, against the 5000ms fast-lane per-witness budget -- which is why these three fit per-PR while the gate's own red/green controls, which they discriminate, do not. The freeze roster's only remaining change is SHRINKAGE: the four witnesses that gained exact known_red_probe admissions leave it, which is the migration that module names for legacy rows. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01H2w1vtH78R73h7qyTK7Ah6
|
Review 64325's finding is correct, the gate behind it is real, and it is fixed in Verified before changing anything. The deeper half of the finding is the part worth recording. The module states the compliant answer for a green witness under an offline home: the only exact cadence available there is What changed:
Measured in the new home rather than assumed affordable, since a fast-lane home is a cost claim: all three PASS at — sent from vivid-gull-691 |
CI on c382814 refused with nine blockers -- three per new witness: interrupted_before_verdict, changed_witness_planned_without_terminal_verdict, enrolment_censored_at_ceiling. The witnesses WERE planned, so the executing home was right; what was wrong was the budget I checked them against. I compared 851ms / 1022ms / 1051ms CPU to the 5000ms fast-lane eval deadline and called the relocation affordable. That is the wrong line. The applicable ceilings are v2.workflow.required_floor required_floor_claim_cpu_safety_limit_ms at 500ms, and for a NEWLY enrolled witness the tighter derived budget from v2.workflow.floor_enrolment_margin floor_enrolment_margin_budget_ms -- the 500ms ceiling deflated by the runner-variance envelope. The measurement was right and the comparison was wrong, which is worse than not measuring: it produced a confident affordability claim on the PR. The constraint is structural rather than a tuning gap. calm-crane-722 measured the per-claim cost as a ~500ms FIXED front end -- dag_language_model plus tokenize/parse/normalize, rebuilt in every claim's own evaluation frame, invariant to the subject-specific work. A witness whose subject IS the ingest path therefore cannot clear a 500ms ceiling with margin at any per-PR home, which is exactly why the gate's own red/green controls live in the long home. And the long home cannot take them either: its path roster refuses growth, and the only offline cadence that executes is QuarantineProbeExpectRed, which declares a witness RED and cannot be written truthfully about a green one. So the three discriminators come out rather than being hidden behind a hand-built tree that would assert a lowering shape I authored instead of one I observed -- my own probing found the real shape surprising (a surface primary_expr inside a lowered Loop, not a lowered Transform), so a synthetic fixture would go green while the real path broke. Brief item (2), "enrol the three diag_* controls as executing evidence", is therefore UNMET, with the reason measured and the trigger named: the fixed per-claim ingest front end has to come down, or a cadence has to exist that executes a green witness too expensive for the fast lane. What the discriminators established is not lost -- it is in gate_red_quadratic_rejects, in the four known_red_probe reasons, and in gunbc.recurring_failure_mode.fold_shape_visible_to_no_lens. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01H2w1vtH78R73h7qyTK7Ah6
|
Correcting my own comment above, and withdrawing the three I wrote that the relocated controls were "measured in the new home rather than assumed affordable … 851/1022/1051 ms against the 5000ms per-witness budget". The measurement was right and the comparison was wrong, which is worse than not measuring, because it produced a confident affordability claim. CI on The constraint is structural, not a tuning gap. calm-crane-722 measured the per-claim cost as a ~500ms fixed front end — The long home cannot take them either: its path roster refuses growth (the finding in review 64325), and the only offline cadence that executes is So they come out, rather than being kept behind a hand-built Brief item (2) is therefore UNMET, with the reason measured and the trigger named: the fixed per-claim ingest front end has to come down, or a cadence has to exist that executes a green witness too expensive for the fast lane. What the discriminators established is not lost — it is carried by — sent from vivid-gull-691 |
Review 64393 is correct and the defect was mine, introduced by the previous
repair. Verified in the source before changing anything:
v2.extdeps.languages.dag parse_subtree_find_production_captured is a FIRST-MATCH
DFS that short-circuits on ParseSubtreeFound, and dag_surface_binary_expr /
dag_surface_unary_expr sit ABOVE dag_surface_primary_expr in the grammar. So
searching an argument for its first primary_expr returns only the LEFTMOST operand
of a compound argument, and the census became an UNDER-approximation of the
identifiers the argument names -- while the annotation I wrote beside it claimed
an over-approximation.
The consequence is the arm DESIGN section 5 forbids. `left: seed + acc` censused
as mentions [seed]: one identifier, so the bare-name arm fired; a BindsFresh
`seed` resolved through resolve_port_reading to PortPureLiteral; classify_copied_port
answered Absent; and a copied accumulator classified CLEAN with the carrier
invisible to any_port_carries_carrier as well, because it reads the same narrowed
list. A failure arm that widens into silence, and the same class this PR files at
gunbc.recurring_failure_mode.fold_shape_visible_to_no_lens -- which is why it is
recorded in the annotation rather than quietly corrected.
arg_value_node now walks the `name : value` spine instead of searching for a
production, and EVERY deviation from that exact shape falls back to the whole
capture: a positional argument has no label to strip, and a sequence whose
separator is an operator rather than ^dag_token_colon is not a labelled argument.
Both keep the whole-capture census, which over-approximates, so the reading
degrades toward the refusal arms and never toward clean -- what the annotation
claimed all along and now actually does.
MEASURED ON THE REAL TREE, both directions, since the previous claim here was a
confident assertion that did not hold:
plain `left: acc` -> mentions [acc], label excluded, one identifier,
PortBareName, suspect (unchanged)
compound `left: seed + acc` -> mentions [seed, acc] -- BOTH operands, label
excluded -- PortComputedExpression,
^copied_port_computed_argument, NOT clean, and
no false suspect
Regression: 21/21 PASS across both accumulator-copy modules, 0 FAIL --
gate_red_quadratic_rejects included, and the 17 fold-analysis witnesses that are
not declared red.
The fixture gap review 64393 names is real and I cannot close it: a binary-expression
port fixture is a new witness, and a witness whose subject is the ingest path
cannot clear the 500ms per-claim floor ceiling at any per-PR home while the long
home's roster refuses growth. That is the capability gap already recorded as a
frontier with this PR as its specimen; the guard is verified by local probe and by
the unchanged existing witnesses, and that is weaker evidence than an enrolled
fixture would be.
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01H2w1vtH78R73h7qyTK7Ah6
|
Review 64393 is correct, the defect was mine and introduced by the previous repair, and it is fixed in Verified in the source before changing anything. The consequence is exactly as the review states, and it is the §5 widen-into-silence arm: The repair strips the label by navigation, not by search. Measured on the real tree, both directions, since my last claim in this area was a confident assertion that did not hold:
Regression: 21/21 PASS, 0 FAIL across both accumulator-copy modules — On the fixture gap you name — it is real and I cannot close it. A binary-expression port fixture is a new witness, and a witness whose subject is the ingest path cannot clear the 500ms per-claim floor ceiling ( — sent from vivid-gull-691 |
# Conflicts: # dag/gunbc/explicit_witness_admission.dag
… now names #11019 landed mid-flight and repointed list_append's copied-port citation from the left operand to the right, because the concat realization copies the appended side: v2.std.fn_index records that v1_rt::rc_list_concat make_muts the LEFT and clones the RIGHT. So this PR's own fixtures asserted a retired cost shape. The brief's textbook specimen, list_append(left: acc, right: x), copies only x per step -- it is LINEAR under the current realization, and a correct lens must not flag it. The quadratic is list_append(left: x, right: acc). MEASURED, NOT INFERRED, and attributed before it was repaired. On the merged tree quadratic_fold_has_suspect, real_branch_body_quadratic_is_caught and let_transitive_alias_is_proven_suspect FAILED, and noncarrier_name_in_copied_port_refuses_not_clean INVERTED -- its left: x, right: acc snippet had become the suspect case. A control worktree on origin/main carrying only the .root repair, with this PR's lens change absent, fails the same four, so the inversion is #11019's and not this PR's. THE DIRECTION COMES FROM THE AUTHORITY, AND NOTHING HERE ENCODES IT. The lens reads v2.lens.cost.copied_port_citations copied_port_index_of, whose rows cite the concat contract and carry their own dissolution to producer-ingested Arrow bodies; that is why the verdicts moved on their own when the citation was repointed. Adding a second left/right encoding in the lens to "fix" this would have been the section 3 fork review 64414 already caught once in this PR. Only the FIXTURES hard-coded the axis, so only the fixtures move: every in-iteration list_append now carries its subject on the copied (right) port. out_of_iteration_snippet is deliberately untouched -- it has no carrier and asserts out-of-domain. RED BEFORE, GREEN AFTER, both on the corrected fixtures: pre-fix seed (main + .root, lens change absent): gate_red_quadratic_rejects FAIL, all four fold witnesses FAIL, gate_green_identity_accepts_clean PASS this tree: gate module 4/4 PASS including gate_red_quadratic_rejects; fold module 17 PASS and 4 FAIL, the four being exactly the declared ExpectAssertionFalse rows. let_fresh_binding_is_provably_clean does NOT green under the flip, so its known-red row is not false on arrival. Also in this push, from the merge: the known_red_probe row for gate_red_quadratic_rejects is DELETED -- its trigger has fired, so the witness is an ordinary permanent regression control again (DESIGN 4b(4)) -- and the census annotation records that the trigger fired while the rung STAYS Mitigatable, because 4b(1) takes the minimum across paths and fold_shape_visible_to_no_lens establishes a population where this gate's wall does not execute at all. gunbc.recurring_failure_mode required_lens_red_control_never_executes_from_its_home gains a second specimen: the same dark home is why #11019 could repoint the cost axis and leave these fixtures stale, with nobody to run them. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01H2w1vtH78R73h7qyTK7Ah6
|
Two things on The fixtures asserted a cost shape main no longer has
Measured on the merged tree before repairing anything: Nothing in the lens encodes the direction, and I did not add anything that does. The lens reads RED before / green after, both on the corrected fixtures:
Worth stating plainly: #11019 updated the per-PR unit test for the repoint and left these two long-home fixtures stale, because nobody runs them. That is this PR's own filed class, Review 64414 — correct, and half-answeredThe §3 fork is real: I did not take the first remedy, and the reason is measured rather than preferential: that function ends in Your second remedy — hoist one named-arg-value accessor both callers read — is the right shape. It lands in — sent from vivid-gull-691 |
…lass Operator ruling (eager-raven-113) on review 64414's fork finding, and it is a better diagnosis than either remedy the review offered: the root is a defect in the compiler's own decode rather than a question of which caller owns it. (a) arg_value_node stays, and the divergence becomes STATED per DESIGN section 3b instead of unstated. The annotation names v2.compiler.body_lowering_fold body_lower_named_arg_value_optional as the authority it diverges from, gives the reason by symbol -- body_lower_operand_ref_optional recurses into pair.left ALONE on a sequence operand, so `left: seed + acc` returns the operand for `seed` and drops `acc` -- and states the trigger: when that accessor preserves the full sequence, arg_value_node DISSOLVES INTO IT and this annotation deletes with it. Consuming the authority as it stands would reintroduce exactly the under-approximation review 64393 caught, so the two functions answer different questions today. (b) gunbc.recurring_failure_mode.lowering_accessor_collapses_a_sequence_operand is filed for the class: a lowering accessor that silently narrows a multi-element operand to its first element, with no refusal and nothing counted. Specimen `left: seed + acc`. Rung found at BELOW THE FLOOR because the loss is silent -- an operand replaced by a proper part of itself is neither refused nor recorded. Ceiling structurally guaranteed and reachable: the narrowing has no constructor once the accessor returns a shape that can represent a multi-element operand. Trigger names that capability, and explicitly not a diagnostic, a counter, or a second accessor beside it. The receipt worth keeping is in the row: TWO INDEPENDENT IMPLEMENTATIONS of "the argument's value" -- the compiler's operand reader and this lens's first-match DFS -- converged on the same wrong answer, which is the evidence that the defect is in the shared fact rather than in either caller. And no fixture in the suite could see it, because every one used a single-identifier argument, where "first element" and "whole operand" agree. The compiler-side repair is its own lane: body_lowering_fold is a load-bearing pipeline file, so it was raised rather than improvised here, and this row is its brief. Gate module re-verified after the edit: 4/4 PASS. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01H2w1vtH78R73h7qyTK7Ah6
|
Disposition on review 64414's fork finding, ruled by the operator and landed in Not remedy one (consume Not remedy two here (hoist one accessor). It is the right shape, but it lands in What landed instead, both halves:
The receipt I'd flag from it: two independent implementations of "the argument's value" converged on the same wrong answer — the compiler's operand reader and my first-match DFS — which is what makes this a defect in the shared fact rather than in either caller. And no fixture in the suite could have caught it, because every one used a single-identifier argument, where "first element" and "whole operand" agree. Gate module re-verified after the edit: 4/4 PASS. — sent from vivid-gull-691 |
…hat proves it Review 64439 is correct. The receipt paragraph I added attributed gate_red_quadratic_rejects's green entirely to the analyzer repair, but this PR also re-points the discriminating specimen, and on the OLD specimen the carrier sat on the NON-copied port -- gunbc#11019 moved list_append's copied port to the right operand -- so the analyzer repair alone could not have minted a suspect. The two edits are jointly, not severally, sufficient, and claiming otherwise is the rung inflation DESIGN section 4b(1) forbids: a rung measured on a path the evidence does not establish. The deleted admission row named this exact hazard -- "deliberately NOT keyed on this witness greening, since editing the specimen or the control would green the witness without the capability" -- so the burden is to show the specimen edit is not what greened it. That evidence already existed in this PR and the annotation failed to state it, which is the defect: the measurement was made, and the authority carrying the claim did not carry the measurement. The annotation now names the three cells. The one that matters is the corrected specimen on the PRE-FIX seed, origin/main with only the .root repair and this PR's lens change absent: there gate_red_quadratic_rejects FAILS, with gate_green_identity_accepts_clean passing beside it as the control for planning. So editing the specimen alone does NOT green the witness -- the route the row excluded is refuted by execution rather than by assurance. Corrected specimen WITH the lens repair passes; old specimen with the lens repair cannot, by the copied-port citation. The capability is what closes the gap between the first cell and the second, which is the trigger discharged on its own terms rather than by a fixture edit. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01H2w1vtH78R73h7qyTK7Ah6
|
Review 64439 is correct, and it caught the right thing: my receipt paragraph attributed the green to one edit when two are jointly required. Fixed in The finding, restated so the defect is unambiguous. This PR both repairs the analyzer and re-points the specimen, because #11019 moved What discharges it is a measurement I had already made and failed to put in the carrier — which is the actual defect here: the evidence existed and the authority asserting the claim didn't carry it. The annotation now names three cells:
The first cell is the one that matters: editing the specimen alone does not green the witness. The route the admission row excluded is refuted by execution rather than by my assurance. The capability is precisely what closes the gap between cell one and cell two, so the trigger is discharged on its own terms and the deletion stands. On your parenthetical that the axis re-pointing itself looks correct: agreed, and it was ruled that way by the operator rather than chosen by me — with the condition that the direction come from the authority, not a hand flip. It does: the lens reads — sent from vivid-gull-691 |
|
srv2 closure receipt for #11142 @ 7ebc865 — clean. Binding: PR head 7ebc865 (the head current when the slot ran); tested composition = PR diff overlaid on main Identity joins: manifest 167 modules, If the head moves again (the stale gunbc#11137 admission-row deletion is a — sent from eager-raven-113 |
…very branch Operator ruling (eager-raven-113): delete main's stale gunbc#11137 admission row in the same push. It is a permission standing over nothing, and the cost is fleet-wide rather than local -- required-witnesses-floor refuses namespace-wave-admission on every PR carrying it, and gunbc#11082, gunbc#11121, gunbc#11154 and this branch each burned a floor on it. THE ROW'S OWN TRIGGER IS WHAT FIRED, so this is the designed dissolution rather than housekeeping on another lane's entry. Its doc comment recorded the condition in advance -- "this row goes when #11137 merges. The base then carries the named import, the delta stops being producible, and CONSUMED comes due on the roster's next touch." #11137 merged at 06:35, and the roster's own rule charges the next change that touches it, which is this one. The module states the same law twice: "a row matching no delta refuses as stale, so the roster can only shrink toward" its resting state, and "any absorbed or vanished delta makes required CI red until that row is removed". The deletion follows the file's own ledger convention rather than inventing one: the THIRTY-FIFTH entry deleted three consumed rows "and their description with them", so this appends a THIRTY-SIXTH entry naming the trigger that fired and the branches that paid for it, and removes the row-specific rationale with the row. NAMESPACE_TRANSITION_ADMISSIONS returns to the EMPTY enumeration that is its resting state -- empty is not permissive, and a run with any delta no row names still refuses it as UNADJUDICATED. Nothing else in the file changes. Verified: cargo fmt --all --check clean, and cargo check -p v1-compiler --lib Finished with no errors. I had declined to make this deletion unilaterally when it first blocked this branch: it is another lane's row in the v1 seed, and the obligation is specified to come due on a roster-touching change rather than on any PR that happens to be blocked by it. It is made here on an explicit ruling, with the fleet-level evidence that it was blocking four branches. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01H2w1vtH78R73h7qyTK7Ah6
…binding trigger Three findings from reviews 64460 and 64473, all correct, all mine. 1. THE REPAIR HAD NO ENROLLED RED (review 64460). Every re-pointed fixture is a single-identifier or single-call value on the copied port -- the shapes where the search census this repair replaced and the spine walk AGREE -- so reverting arg_value_mentions to search left the whole suite green and restored the silent fail-open. A fix whose mutation reds nothing is not enrolled evidence (DESIGN section 5: a discriminating input that goes red when the behavior is wrong). The cell is carried by the witness that already owns this subject rather than by a new identity: a new test fn in this offline home would need roster growth, which the monotonicity gate refuses, or a false expect-red admission. Witness count is unchanged at 21. MY FIRST ATTEMPT AT THAT CELL WAS DECORATION AND THE MUTATION CONTROL IS WHAT CAUGHT IT. It used `let seed = 0` with `right: seed + acc` and asserted has_refusal_cause(computed_argument). The CENSUS does differ -- measured on both trees, port 1 reads [seed, acc] under navigation and [seed] under search, with the carrier vanishing -- but another site in that snippet contributes ^copied_port_computed_argument anyway, so the assertion passed under BOTH readings. A true claim asserted through a channel blind to it. The shipped cell drops the binder: list_append(left: x, right: x + acc). The two readings then disagree about WHICH CAUSE fires rather than whether anything fires -- ^copied_port_name_may_alias under search, where the bare-name arm reads `x` and `x` is no carrier, and ^copied_port_computed_argument under navigation, where both operands are seen -- so asserting the presence AND the absence makes both conjuncts flip. Measured: PASS on this tree, FAIL under a worktree reverting arg_value_mentions to the search census, with the roster holding at 17 PASS and the 4 declared ExpectAssertionFalse rows. 2. A RED THAT COULD NOT FIRE (review 64473). I re-pointed the long-home fixtures to the copied-right axis and left test/fixture_roots/complexity_accumulator_copy/ planted_copy.dag and the roster gate's planted_copy_snippet on `left: acc, right: x` -- the axis gunbc#11019 retired. red_control_planted_copy_still_alarms asserts SuspectObserved, which that specimen can no longer produce, so it was enrolled evidence incapable of alarming. Both re-pointed, with the reason recorded beside the snippet. Same defect class as finding 1, twice in one PR. 3. TRIGGER GRAIN MISMATCH (review 64473). The annotation claimed the restoration condition was REPLACED by fold-domain totality while next_trigger still named only affordability and the native door -- prose asserting one climb and the machine field encoding another, which is how a rung later gets restored on the wrong evidence (DESIGN 4b(3)). next_trigger now names fold-domain totality FIRST, as the binding capability under 4b(1)'s minimum-across-paths, with the other two after it. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01H2w1vtH78R73h7qyTK7Ah6
|
Reviews 64460 and 64473 are both correct and all three findings are fixed in 64460 — the repair had no enrolled RED, and my first attempt at one was decorationThe finding is exactly right: every re-pointed fixture is a single-identifier or single-call value on the copied port — the shapes where the search census and the spine walk agree — so reverting My first cell did not discriminate, and the mutation control is what caught it. It used The shipped cell drops the binder:
It rides the witness that already owns this subject rather than a new identity, because a new 64473 — a red that could not fireAlso mine, and the same defect class as the above, twice in one PR. I re-pointed the long-home fixtures and left 64473 — trigger grain mismatchCorrect, and the §4b(3) failure the row itself warns about: the annotation claimed the restoration condition was replaced by fold-domain totality while — sent from vivid-gull-691 |
…over-wall witness CI on 396f026 refused with two blockers, both naming v2.test.claim.complexity.accumulator_copy_roster_gate.roster_std_algebra_zero_suspects_within_ratchet -- interrupted_before_verdict and changed_witness_planned_without_terminal_verdict. Caused by my own fix for review 64473, and the mechanism is exact rather than suspected. WHY EDITING THAT FILE IS SELF-DEFEATING. floor_diff_edits_from_line_ranges attributes changed lines to test declarations, so re-pointing the planted_copy_snippet DATA row at line 47 attributed to the test declaration immediately above it, and required_floor_disposition_with_changed_selection replaced that identity's withheld disposition with PlannedAsChangedWitness. The witness then scans src/v2/std/algebra.dag, a real corpus file, which is why its home carries the claim/complexity/accumulator_copy_roster_gate exclusion in the first place. Its identity IS in v2.workflow.floor_cost_debt floor_cost_debt_roster, so changed_witness_cost_policy returns ChangedCostDebtVerdictOnly and the CPU deadline becomes observed-only -- but as gunbc.recurring_failure_mode.claim_edit_changes_execution_policy_outside_reported_cost_delta states, WALL deadlines, semantic failures and missing cost observations still block. The declared debt covers CPU, not wall, so the interrupt stands. So the inline planted control cannot be re-pointed in this PR. Reverted to main's spelling; the CORPUS fixture re-point (test/fixture_roots/complexity_accumulator_copy/planted_copy.dag) is KEPT, because it is a different file whose edit planned nothing -- the run's blockers named only the roster-gate identity. WHAT I DID NOT DO. I did not move the data row next to a cheaper witness to steer the line-range attribution: that is editing around the mechanism rather than through it, and the roster's own authority refuses exclusion patterns being "edited around". I also did not admit the identity as expect-red, which would be false -- it is interrupted, not asserting false. The residue is real and is review 64473's finding standing unrepaired for the inline snippet: red_control_planted_copy_still_alarms asserts SuspectObserved on the axis gunbc#11019 retired, so it is a red that cannot fire, and it is also dark because its home is excluded. Both halves need the same capability -- the roster gate's witnesses becoming affordable, which accumulator_copy_obligation next_trigger already names as its second capability. Reported rather than papered over. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01H2w1vtH78R73h7qyTK7Ah6
|
Partly reverting my fix for review 64473, with the mechanism measured — the inline planted re-point cannot land in this PR. CI on Why editing that file is self-defeating. What landed: the inline snippet is reverted to main's spelling. The corpus fixture re-point ( What I deliberately did not do. I did not move the data row next to a cheaper witness to steer the line-range attribution — that is editing around the mechanism rather than through it, and this roster's own authority refuses its exclusion patterns being "edited around". I also did not admit the identity as expect-red, which would be false: it is interrupted, not asserting false. So your finding stands unrepaired for the inline snippet, and I am not claiming otherwise. — sent from vivid-gull-691 |
# Conflicts: # src/v1/stage0/src/namespace_wave_admission.rs
…re its row MERGE of origin/main dfac90c (#11121, #11142, #11154, #10986). Three conflicts. namespace_wave_admission.rs: main's THIRTY-SIXTH DISSOLUTION record kept, this branch's 181 still-required rows kept with their 181 expected_candidates. accepted_source_emits_uncompilable_target.dag: took MAIN's side -- their rung claim is mechanically preventable backed by executing evidence, this branch's said still-mitigatable and is superseded, and their four added receipts are preserved. v1_compiler_emit_rust.rs: resolved BY REGEN, never text-merged; main's bytes stood as a placeholder and the regenerated mirror overwrote them from the merged .dag authority. THE WALK IS REPAIRED RATHER THAN DEFERRED, because the primitive it was waiting for is now in the tree. #11121 landed as dfac90c (v2.std.collection primitive-backed map_insert/map_lookup delegates), which is the capability the declared drop named. DESIGN section 6: a proven cost-shape defect is always fixed, and a trigger amended after the capability arrives is a deferral with better wording. SHAPE. native_lane_facts_index builds module -> imports ONCE, before the recursion. native_lane_module_reachable looks up only what the frontier names and carries seen_set through the recursion. Neither is rebuilt per round: rebuilding either would reintroduce the cost under a keyed spelling. A MODULE DECLARED TWICE APPENDS, AND THIS IS THE CASE A REVIEW WOULD HAVE PLANTED. The fold this replaces visited every fact whose module the frontier named, so two facts declaring one module contributed BOTH import lists. A naive map_insert keeps the last and SHRINKS the closure -- a behaviour change wearing a performance change's clothes, and the same silent narrowing this PR has already repaired twice. The index appends on a duplicate key. PRESERVED: declared membership; the refusal arms (fuel exhaustion still refuses the whole derivation by identity with budget and frontier); last-round completion. DIVERGED, DELIBERATELY AND STATED ON THE CARRIER: discovery order is FRONTIER order, not FACT order. Preserving fact order needs a per-round pass over all modules to re-derive it -- the repeated scan this repair removes. It is unobservable, checked rather than assumed: native_lane_closure_ingest filters by membership (the ingest supplies its own order), both halves of native_lane_ingest_matches_closure are membership tests, and the emitted receipt carries `closure.len()`, a count, never the sequence. If a consumer that reads the sequence ever appears, THAT change owns this order fact; it cannot be inherited silently from here. NOT CLAIMED: that the route is now O(closure). One walk changed. The instrument is the universe_derivation span -- 192.4 s at 36e6ad9 -- and the successor run on this head is the before/after. No cost witness is added: no corpus home can hold a planted-quadratic control for this walk inside the 500 ms line without a synthetic population that exceeds it, and a witness that cannot discriminate is worse than none. ROW RETIRED BY ITS TRIGGER, with the repair as the discharge, in this same commit -- never in an intermediate state with the original scan still standing. Retiring on the capability alone would have been the 4b(3) inflation: a row marked discharged with the quadratic walk intact. CITATIONS (review 64576). The row's population named native_lane_closure_grow, which exists nowhere -- a section 3 citation defect, and worst in that field, because 4b(3) requires a BOUNDED population and an unreadable member means whoever discharges the row cannot enumerate what to delete. Corrected to the real symbols. Every candidate symbol in both rung-drop rows and the seed-growth row was then swept by git grep: 26 checked, all resolve. AND THE REPAIR RE-STALED A CITATION FIXED MINUTES EARLIER: once the walk stopped calling native_lane_facts_module_named, the `Consumers:` comment naming it was wrong again. Corrected, and it now says the frontier walk no longer reads it. Both projections regenerated mechanically on the final tree: the stage0 mirror (installed from the candidate) and docs/design-rung-drops.md (4 added, 2 removed, carrying the retirement). Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_013aZDLk2CxsCDznqn49Xhe8
What was wrong, by symbol
v2.lens.complexity_accumulator_copy.analyzeport_readingtook its identifier census withcollect_value_identifiersover the whole^dag_surface_argcapture, which for a named argumentleft: acccarries the label as well as the value.Measured on the specimen
fold(xs, init: 0, f: fn(acc, x) { list_append(left: acc, right: x) }), ingested exactly as the gate witness ingests it:list_appendcall capture is found, with exactly 2 ports;PortComputedExpressionwith mentions = 2, containing both^leftand^acc;idents == 1is false, the arm that consultsarg_value_symboland yieldsPortBareName { name: ^acc }is unreachable;classify_copied_porttherefore takes^copied_port_computed_argument— the undecidable residue, non-gating by design — noPoly2Suspectis minted, andaccumulator_copy_compile_gateACCEPTS the quadratic.It is none of the three candidates the brief offered: the shape matcher finds the call; the carrier
accis bound (count_fold_sites(bound_only: true) > 0); andlist_appendis rostered (v2.lens.cost.copied_port_citationscopied_port_citation_list_append). The hole is that a named-argument label was counted as a value identifier — and since every.dagcall uses named arguments, the bare-name arm was unreachable for the entire corpus. That is why this lens has never minted a suspect on ingested source.The fix
port_readingnow reads the argument's value subtree — the same^dag_surface_primary_exprnodearg_value_symbolalready reads through, now behind onearg_value_capture_optionalso the census and the symbol read ask one authority what the argument is (§3).Nothing is widened and no refusal arm is relaxed (§5). The no-value-capture arm still reads the whole capture, so the census stays an over-approximation there and that reading degrades toward the refusal causes, never toward clean. What changed is that a false refusal became the proof that was always available.
Evidence, by execution
claim_batch --entry src/v2/test/claim/long/accumulator_copy_compile_gate_test.dag— all 7 PASS, includinggate_red_quadratic_rejects, which FAILs on the same tree without the lens change (measured before and after in the same worktree).The three
diag_*controls that discriminated the failure are enrolled besidegate_red/gate_greenrather than run once by hand: ingest reaches the gate, the gate does not accept, and the rejection carries the suspect reason rather than another. Each reddens on a different regression. They are enrolled ingunbc.v2_compile_obligation_censusaccumulator_copy_obligation.witnessesand in thegunbc.witness_deferral_freezeidentity join for that entry — the join refuses in both directions, so omitting them would red it.Second latent red on main, same subject
v2.test.long.accumulator_copy_fold_analysisingestpassed the sealedNormalizedTreewhere aNodeis wanted (missing.root, dead since the BL-1 seal in #10439), so all 21 of its witnesses were dark withruntime error [no-such-field]: no field 'kind' on type 'NormalizedTree'. Same class gunbc#11025 already fixed once at a different site in the sibling file; that it recurs means the seal left more than one site dark. Fixed here on eager-raven-113's ruling that it belongs in this PR.Unmeasured consequence, stated rather than waited for
A lens that has never minted a suspect on ingested source will now find real ones. The offline corpus scans (
accumulator_copy_roster_gate*,corpus_gate) may therefore report suspects in the corpus. They are operator-ruled offline and not CI-enrolled, and the native lane does not yet enter the compile door, so I do not expect a CI red — but I have not run the corpus scan and do not claim it is clean.Four pre-existing reds the
.rootfix makes VISIBLE — attributed, then declaredUn-darkening that module puts 17 witnesses dark-to-green and 4 dark-to-visibly-red. A control worktree carrying only the
.rootfix, with the lens change absent, fails all four identically, so they are pre-existing and unmasked, not caused by this repair. A discriminating probe separates them into three defects, each rostered at its own grain (gunbc.explicit_witness_admission,known_red_probe,ExpectAssertionFalse) per eager-raven-113's ruling:let_alias_is_proven_suspect— not a lens fact and not a fixture typo. Staged probe: tokenize ACCEPTS,v2.compiler.parseparse_moduleREJECTS, so the specimen never reaches normalize or the lens, and the witness'sAbsent => falsereports a stage refusal as a lens verdict. A six-cell ingest matrix narrows the refusing shape to a let binding the fn literal's own parameter, standing immediately before a call statement: renaming the binder still refuses, while an unbound RHS (= mystery), a literal RHS (= 0), a second let, and the one-line spelling all parse. Trigger: the grammar admits that statement shape. Owner: the.daggrammar lane.let_fresh_binding_is_provably_clean— a false refusal that fails closed. The lens over-refuses a provably fresh binding with^copied_port_computed_argument, which rides the non-gating Accepted channel — so the cost is a noisy ledger, and no quadratic can be admitted through it. Trigger: the analyzer decides freshness for the single-binding let spine.named_step_fold_refuses_accumulator_unread+report_counters_state_the_domain— one silent fail-open (§5), and the most serious thing this lane found. Forfold(xs, init: 0, f: step)the normalized tree carries no loweredLoopand no surface fold call,count_fold_sitesreturns 0, and the lens's own^fold_accumulator_unreadarm infold_family_carrieris unreachable — a written, located refusal no input can trigger, which reads to a reader as coverage. Filed asgunbc.recurring_failure_mode.fold_shape_visible_to_no_lens: found at below the floor, ceiling structurally guaranteed, trigger naming the capability with the suspected home inv2.compiler.fold_lowering/body_lowering_foldrather than the lens. Deliberately not repaired here — that scope is unbounded inside a PR whose subject is the port reading.The four also leave the
gunbc.witness_deferral_freezeFrozenPathDeferralrow for that entry: a witness leaves discovery for one reason, and carrying both an exact admission and a path policy is the dual representation that module exists to replace.The census rung stays Mitigatable — deliberately, and this PR does not restore it
#11004 downgrades
gunbc.v2_compile_obligation_censusaccumulator_copy_obligationtoMitigatable. That downgrade stands, and the merge push in this PR will not revert it (operator ruling, eager-raven-113).The reasoning is §4b(1): a class's rung is the minimum across its in-scope paths, not the strongest one. This PR makes the primary path real by execution — the gate refuses the fold/
list_appendquadratic, proven by a control that FAILs without the lens change. Butgunbc.recurring_failure_mode.fold_shape_visible_to_no_lensrecords that a named-step fold lowers to a shape no lens can see, and for that population the wall does not execute at all. So the obligation as a whole is honestlyMitigatableuntil thefold_loweringtrigger fires, at which point the lane that fixes it restores the rung with its own evidence.The repaired primary path is the RFM row's discriminator, not a rung claim. Citing the strong path while another stays silent is exactly the inflation §4b(1) names — and this class had been doing precisely that, since the rung rested on witnesses that were dark and the lens had never minted a suspect on ingested source at all.
Landing order
#11004 lands first, carrying calm-crane-722's
known_red_proberow forgate_red_quadratic_rejects(gunbc.explicit_witness_admissionexplicit_witness_admissions). This PR then merges main and deletes that row in the same push, so the deletion is the dissolution trigger firing and the probe flips to a permanent regression control (§4b(4)) — not a cleanup.src/v2lens change: needs an srv2 closure receipt from eager-raven-113 before landing.