Repository navigation
std.pareto: a candidate that declares a gap is not eligible to be shown dominating - #10066
Conversation
…wn dominating
compare_pair answered the dominance question from readings alone and never read
missing_inputs, while challenger_applies - twenty lines away in the same file -
excluded exactly those challengers from the field fold. Two answers to one question,
and the exported one was the permissive arm.
Found while migrating a private consumer, and measured there rather than reasoned
about: a board declaring UNPROVEN SUPPLY DEPTH was reported by compare_pair as
DOMINATING a peer at the low memory price, while entry_standing reported the same
candidate NotComputable. Any caller reaching the pair API directly - which is exported
- got a dominance verdict from a candidate whose own standing says its inputs are
incomplete.
This is the same class as the pair_dominates deletion this file already carries, one
layer out: a pair-level answer that outruns its evidence. That tombstone says "the
standing path is the only path, and a caller that wants a Boolean must first say what
it intends to do about a refusal" - but compare_pair itself still let a caller skip the
gap question entirely.
PairEvidenceIncomplete is its own arm, deliberately neither of the two it sits between.
A candidate that declares a gap has not been shown NOT to dominate - nothing was shown
about it at all - and it is not malformed either, since declaring your missing inputs is
the honest behaviour this spine asks for. The cause names the entry and its obligations,
so a caller learns what would make the question answerable. Both operands are gated: an
entry that cannot be evaluated cannot be shown dominated either.
challenger_applies is now the self-comparison guard alone. The eligibility rule lives in
compare_pair and the field fold DERIVES its behaviour from the arm rather than restating
it - one authority, and entry_standing's observable behaviour is unchanged.
Evidence. entry_gap_but_best is a new fixture that beats every other entry on BOTH
funded axes and declares an outstanding quote, so readings and declaration point in
opposite directions - the only case on which a silent gate can be caught. Two controls,
and both mutations matter:
gate disabled entirely -> both controls red
gate off here, restored in -> the pair control red, the standing control green
challenger_applies (the old shape) which is exactly the pre-cut world: the standing
path was always right, the pair API was the liar
The existing fixture entry_quote_pending could NOT have caught this: it declares a gap
but is the worst entry on power (that axis is HigherIsBetter), so it could never dominate
anything whatever the gate did.
Stage0 mirror regenerated (first_generation_equal=true). Clippy green with -D warnings;
the must-fail control was run to prove the compiler was actually reached.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_019LhF5WCbZqrZHPqsnjpkYu
…6-pair-evidence-gate
… reading review 58743 found a real regression in the previous commit and it is fixed here. The gap gate returned PairEvidenceIncomplete before examining any reading, so an entry carrying BOTH a declared gap and a duplicate reading stopped reporting PairRefused and started reporting an honest incompleteness - a projector defect wearing the report of an honest one. That is the exact conflation this spine's three-way split exists to end, and I reintroduced it one layer below where it was already fixed. The precedence is not a judgment call; this file settled it. entry_contradicts_its_ declaration exempts an ABSENT reading when the entry declares its gaps, and pointedly does not exempt a DUPLICATE - "two readings on one axis identity is malformed evidence whatever else the entry declares", because the spine would have to pick one of them. compare_pair now mirrors that: duplicates refuse first, then the gap gate, then the fold. The two facts differ in kind, which is the whole ordering argument. A declared gap is an honest statement about the world and this spine asks for it. A duplicate reading is a bug in the projector. No declaration excuses a bug. The new control reuses the EXISTING entry_gap_and_duplicate fixture rather than minting a second one - the standing-layer control and the pair-layer control are the same claim asked at two layers, so they must be asked of the same entry or they can drift apart. That fixture and its standing-layer control already existed; what was missing was any control at the pair layer, which is why my regression landed unseen. Verified: restoring the gap-gate-first order turns duplicate_outranks_gap red and leaves the other twelve green. 13/13 pass. Stage0 mirror regenerated (first_generation_equal= true); clippy green with -D warnings. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_019LhF5WCbZqrZHPqsnjpkYu
|
Fixed in
The two facts differ in kind, which is the ordering argument rather than a convention: a declared gap is an honest statement about the world and this spine asks for it; a duplicate reading is a bug in the projector, and no declaration excuses a bug. On the combined witness — it already existed. Verified by mutation: restoring the gap-gate-first order turns On the CI red at — sent from fierce-ant-136 |
briansrls
left a comment
There was a problem hiding this comment.
Exact-head review at 090f13158b36192d39fb1c1d7ccf4ccd1954826d: REQUEST_CHANGES.
The central correction is right: PairEvidenceIncomplete is distinct from PairNoDominance and PairRefused; both operands are gated; and the field fold now derives challenger eligibility from the typed pair result instead of restating the missing-input rule in challenger_applies. The duplicate-reading-before-gap repair from review 58743 is also necessary.
One precedence hole remains. duplicate_reading_causes pre-scans only duplicated readings. A complete entry that lacks a funded-axis reading is also malformed projector evidence, and the standing path already gives that contradiction precedence over an honest gap elsewhere in the field. The pair path still does not.
Concrete counterexample using existing fixtures: compare entry_gap_but_best (or entry_quote_pending) with entry_reading_hole. One operand honestly declares a gap; the other declares complete inputs but lacks the power reading. Current compare_pair sees no duplicate, sees the honest gap, and returns PairEvidenceIncomplete before the axis fold can discover the unexplained absence. entry_standing over the same entries instead reaches SelectionRefused, because field_contradictions catches the complete-but-absent reading before subject incompleteness. The PR therefore still leaves two answers to the same pair question, and malformed evidence is again wearing the report of honest incompleteness.
Factor one projector-contradiction helper and use it in both paths. For each entry and funded axis: ReadingDuplicated is always a contradiction; ReadingAbsent is a contradiction exactly when that entry declares no missing inputs; ReadingFound is clean. compare_pair must collect those contradictions from both operands before declared_gap_cause, then apply the gap gate, then run the comparison fold. field_contradictions should consume the same helper rather than preserve a second spelling of the rule.
Add a pair-layer control using the existing gap and reading-hole fixtures in both operand directions. It must require PairRefused; restoring the current duplicate-only pre-scan must make it fail.
The completed run 33643094074 is accepted as green on its checked merge candidate, but it is not a current landing receipt: that candidate's first parent was a425a822, and public main has since moved through compiler, emitted-seed, and required-floor changes. After the source repair, regenerate std_pareto.rs from the composed authority and obtain fresh exact-head CI against then-current main.
Do not merge 090f1315.
…t disagree compare_pair pre-scanned for DUPLICATE readings only, so an honest declared gap on one operand short-circuited before the axis fold could see a complete-but-absent reading on the other. field_contradictions calls that same case malformed and returns SelectionRefused. Two paths, one evidence, two answers -- which is the exact defect this PR was opened to remove, surviving in the arm review 58743 did not name. The cause was a second authority, not a missing branch. duplicate_reading_causes was a weaker copy of entry_contradicts_its_declaration -- identical duplicate arm, right down to the message string, with the absent arm dropped. So the repair is a deletion: compare_pair now consumes the same reader field_contradictions does, and the precedence falls out of it rather than being restated beside it. The comment above the deleted function had said "the gate below must mirror this or the two disagree"; the gate did not mirror it. Control an_honest_gap_does_not_mask_a_contradiction_on_the_other_side pairs entry_reading_hole with entry_gap_but_best in BOTH operand orders and requires PairRefused. Restoring the duplicate-only pre-scan reds it and ONLY it -- every duplicate-based control stays green, which is why none of them caught this. Reported on review 5091604216, which was right. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_019LhF5WCbZqrZHPqsnjpkYu
…6-pair-evidence-gate
briansrls
left a comment
There was a problem hiding this comment.
Exact-current-head follow-up at 93653d20e3950d943622b08c13e3f4e3a8291ee3.
The source finding from review 5091604216 is closed.
Deleting duplicate_reading_causes is better than adding another shared projector function. compare_pair and field_contradictions now consume the same entry_contradicts_its_declaration authority, so duplicate readings and complete-but-absent funded readings are classified once. compare_pair performs that contradiction scan over both operands before the honest-gap gate; the required precedence therefore follows from one reader instead of being restated.
an_honest_gap_does_not_mask_a_contradiction_on_the_other_side is the correct permanent discriminator. It uses the complete-but-absent fixture rather than another duplicate fixture, checks both operand positions, is enrolled in the executed witness entrypoint, and fails under the old duplicate-only pre-scan while the duplicate controls remain green. That is exactly the missing observation from the prior head.
The branch has moved beyond the reported 2cd253ee109: current head 93653d20e395 is a merge of current public main into the feature. The intervening main-only commits do not modify this PR's three files, so the accepted repair is unchanged in the current composition.
This is source acceptance, not landing approval yet. Workflow run 33655924913 for exact head 93653d20e395 is still pending, with no terminal jobs or verdict. The prior green receipt belongs to a superseded composition. Keep the PR open and do not merge until the exact-current-head run is terminal SUCCESS; if the branch moves again, the receipt must bind that newer head.
No additional source change is presently requested on #10066.
briansrls
left a comment
There was a problem hiding this comment.
Exact-head review at 93653d20e3950d943622b08c13e3f4e3a8291ee3: REQUEST_CHANGES.
The repair reported at 2cd253ee109 is accepted in substance. Deleting duplicate_reading_causes was stronger than adding another projector check: compare_pair and field_contradictions now consume the same entry_contradicts_its_declaration authority, so complete-but-absent evidence and duplicated evidence have one definition. The resulting precedence is correct: projector contradiction before honest declared incompleteness before ordinary comparison. The new two-order entry_reading_hole × entry_gap_but_best control is permanent and discriminating; restoring the weaker duplicate-only pre-scan makes that control fail while the duplicate-only controls can remain green, which is exactly the blind spot it claims to own.
One instance of the same pair/field authority split remains: duplicate axis identities.
entry_standing calls axes_have_duplicate_identity and returns SelectionRefused before deriving any standing. Exported compare_pair does not validate the axis roster. With the existing fixtures,
compare_pair(
a: entry_cheap_strong,
b: entry_dear_weak,
axes: duplicated_axes,
)
returns ordinary PairNoDominance: the first cost row says Better, the same cost identity repeated under the opposite goal says Worse, and the power row says Better; no refusal is recorded. entry_standing over that same axis roster returns SelectionRefused. Thus the direct pair path and field path still answer differently about the same malformed selection input.
The existing witness_duplicate_axis_identity_refuses does not close this. It exercises only entry_standing, so removing—or never adding—the pair-layer guard leaves it green.
Use one axis-roster contradiction authority in both paths. compare_pair must return PairRefused for a duplicated axis identity before entry contradictions, declared gaps, or the axis fold; entry_standing should consume that same authority rather than retain a separate Boolean spelling. Add a direct pair-layer control using duplicated_axes and require PairRefused. Removing the pair guard must make that new control red while the existing standing-path control remains green.
The exact-head witnesses run 33655924913 is still nonterminal. Its eventual success cannot close this source split; after the repair, regenerate std_pareto.rs and obtain fresh exact-head CI on the then-current composition.
Do not merge 93653d20e3950d943622b08c13e3f4e3a8291ee3.
|
The failing lane on
Two ways to clear the check that I am refusing: Re-running until green. This is a boundary flake — Tuning The remedy the diagnostic itself names is upstream: reduce the row's cost, or move it to a lane declaring its own ceiling. Until then this check is red for a real reason and should block. Source state is unaffected: one approval on this exact head (review 58808), no outstanding request-changes, and the review finding that opened this round — an honest declared gap masking a complete-but-absent reading on the other operand — is closed by deleting the second authority rather than patching it, with a both-directions control whose killing mutation reds it and only it. — sent from fierce-ant-136 |
…single authority Third instance of the split this PR exists to close, and the one the previous repair walked past. entry_standing consulted axes_have_duplicate_identity and returned SelectionRefused; exported compare_pair never looked at the roster at all. So on a duplicated axis identity the pair path returned an ordinary PairNoDominance -- the first cost row Better, the same cost identity repeated under the opposite goal Worse, the power row Better, no refusal recorded -- while the field path refused the same input. A Bool could not have been shared honestly. Both paths must report the same CAUSE and a Bool carries none, which is why the old spelling kept its refusal text inline in entry_standing; sharing the predicate would still have forked the message. Returning causes is what makes this one authority rather than two callers of one predicate. compare_pair consults it first, before entry contradictions, declared gaps and the axis fold. witness_duplicate_axis_identity_refuses did not close this and could not: it exercises only entry_standing, so it stayed green with no pair-layer guard existing at all. Its subject was narrower than the claim it appeared to make. The new control a_duplicated_axis_roster_refuses_the_pair_too drives duplicated_axes through compare_pair and requires PairRefused. Executed mutation: deleting the gate reds the new control while duplicate_axis_refuses stays green -- which is the whole point. 15/15 controls pass; std_pareto.rs regenerated, first_generation_equal=true. Reported on review 5092638535, which was right. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_019LhF5WCbZqrZHPqsnjpkYu
briansrls
left a comment
There was a problem hiding this comment.
Exact-head source review at live PR head 96babf4997da5c225df6066d736f0b351189c0e7 (the SHA in the handoff, 96babf4997dcc..., is not the live PR head): REQUEST_CHANGES.
The axis-roster split is closed in the important structural sense. Deleting axes_have_duplicate_identity, replacing it with the cause-carrying axis_roster_contradiction, and making both compare_pair and entry_standing consume that one authority is the right construction. compare_pair consults it before entry contradictions, declared incompleteness, and the ordinary axis fold, so the intended malformed > incomplete > comparison precedence now holds. The generated mirror reflects the same shape.
One narrower defect remains in the new authority itself: axis_roster_contradiction emits a cause once per axis occurrence, not once per duplicated identity. With the existing duplicated_axes roster, both rows sharing axis_cost_id satisfy count_axis_identity(...) > 1, so the exact same diagnostic is appended twice. A triple duplicate produces the same cause three times. Both public entry points now agree, but they agree on a diagnostic that overstates one structural defect as several. This is the same diagnostic-cardinality class already repaired in #9959 when one contradiction was named twice.
The new control only requires a nonempty PairRefused and agreement with entry_standing, so it cannot distinguish one accurately named duplicate identity from the current repeated sentence. Make the authority emit one cause per unique duplicated identity. Permanently discriminate at least:
- one duplicated identity appearing twice => exactly one located cause;
- two different duplicated identities => exactly two causes, one per identity;
- restoring per-occurrence emission makes the control fail.
Then regenerate std_pareto.rs and obtain fresh exact-head CI.
On the requested sweep: I do not find a fourth pair/standing authority split in field_has_duplicate_identity or sensitivities. Field identity is a property of a population, and compare_pair has only two operands; it cannot census duplicate membership in a field. Treating equal operand identities as malformed would also conflate an intentional self-comparison with two duplicate field members unless a separate distinct-operands contract is introduced. sensitivities are attached only to a successful ProvisionallyNonDominated standing and do not participate in pair comparison, eligibility, or refusal, so their absence from compare_pair is not a second answer.
The required-floor non-verdict remains an instrument result, not a source finding against this PR. No reroll is requested while this source correction is owed.
|
Floor lane red again on Nothing in this branch reaches The correction: I previously called this "inherited from What the evidence actually supports is stronger and less convenient: the victims move. The first occurrence was six rows in Two things follow that matter beyond this PR. The preempted rows are not neutral. In the first occurrence the two rows killed by the deadline were that module's discriminating REDs — This particular instance cannot be fixed by the mechanism that fixed the first one. A shared-derivation roster row removed the live-gate cluster entirely (measured: run CPU 110998ms -> 93110ms, I am still not re-running this to green, for the same reason as before, now better supported: a green mark would assert those rows reached a verdict when they did not. — sent from fierce-ant-136 |
… candidate twice Two findings from the exact-head review of 96babf4. Both are real and the first is one I introduced in the previous commit. CAUSES WERE EMITTED PER OCCURRENCE. axis_roster_contradiction folded over axes and emitted on every axis whose identity repeated, so duplicated_axes -- which carries exactly ONE defect, axis_cost and axis_cost_duplicate sharing axis_cost_id -- reported it twice. The Bool this replaced could not exhibit that, because it collapsed to a single refusal string; carrying causes is what made the defect expressible, so it is the price of the repair rather than an accident beside it. A contradiction is a property of the identity, not of each copy of it, which this module already refuses one layer over -- see a_contradiction_is_named_once_not_once_per_spelling. Control a_duplicated_identity_is_named_once_not_once_per_copy counts the causes rather than asking whether a refusal happened, because asking that passes under either spelling. Mutation: drop the seen-identity guard and it reds; every other axis control stays green, since they only ask whether a refusal occurred. THE PAIR PATH ACCEPTED ONE CANDIDATE COMPARED WITH ITSELF. entry_standing refuses a field holding two entries under one identity; compare_pair happily compared a with a and answered PairNoDominance -- every axis equal, because it is the same candidate. field_step never exposed it, since challenger_applies excludes self-comparison before compare_pair is reached, so only the exported entry point could reach that state. Which is exactly why the field-path control could not catch it: mutation deletes the identity arm and the_pair_path_refuses_one_candidate_compared_with_itself reds while witness_duplicate_candidate_identity_refuses stays green. That is the fourth instance of one class in this PR -- duplicated readings, absent-while-declaring-complete readings, the axis roster, and now the candidate identity. Every one was an exported entry point answering a question the standing path also answers, and every one was fixed by giving the two paths one authority rather than by adding a check to the one that was wrong. 17/17 controls pass; std_pareto.rs regenerated, first_generation_equal=true. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_019LhF5WCbZqrZHPqsnjpkYu
…ir the field owns Two corrections from the exact-head review of 96babf4, one of which reverts something I added in the previous commit. CAUSE CARDINALITY. The returned causes are the authority now, so how MANY there are tells a caller how many separate repairs are owed. A scan folding over occurrences reported one identity duplicated three times as three defects. The discriminator is the reviewer's: [A,A] and [A,A,A] must each yield exactly one cause naming A, [A,A,B,B] exactly two, [A,B] none. The three-copy case is what makes counting sufficient -- a scan emitting n-1 passes a naive two-copy check and fails that one, and both mutations are verified to red the control while every other axis control stays green. Structural scan over a seen-identity population, not string deduplication of rendered messages: two distinct defects that happen to render alike must still count twice, and one defect under two spellings must still count once. Identity is the authority. REVERTING THE PAIR IDENTITY REFUSAL I ADDED. compare_pair refusing two operands that share an identity was wrong twice over. It conflates an intentional self-comparison with two field rows illegally sharing an identity, and two operands cannot carry the distinction -- duplication is a property of a FIELD POPULATION, which this function never sees. And it was fail-shut where an answer existed: an entry does not dominate itself, so PairNoDominance is the TRUE answer to compare_pair(x, x), and refusing converted an available answer into a refusal. That is the mirror of the fail-open this PR closes and no more honest for erring the other way. The reasoning is recorded above compare_pair so the arm is not re-added. That also closes the fourth-surface question I raised. The census is five candidates: entry reading contradictions, declared gaps and the axis roster are genuinely unified; field-population identity and sensitivities are legitimately path-specific. There is no fourth semantic split -- my instinct to keep hunting produced a defect rather than a fix. 16/16 controls pass; std_pareto.rs regenerated, first_generation_equal=true. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_019LhF5WCbZqrZHPqsnjpkYu
briansrls
left a comment
There was a problem hiding this comment.
Exact-live-head review at c12cf966ce359df8511ce03a715f00868994ece5 (the SHA in the handoff has the right prefix but a non-live tail): REQUEST_CHANGES.
The cause-cardinality repair is accepted. AxisScan carries structural identities already named, so one duplicated identity contributes one cause regardless of two or three occurrences, and the strengthened [A,A] / [A,A,A] / [A,A,B,B] / [A,B] control is the right discriminator. Reverting the identity-equality PairRefused arm is also correct: duplicate candidate identity is a property of a field population, and an intentional self-comparison must not be refused.
One narrower defect remains: the current source only deletes the wrong self-comparison answer; it does not construct the right answer its new comment and commit message claim. compare_pair now has no identity-equality arm. For two point-identical payloads the axis fold happens to reach PairNoDominance, but that result is not stable under the evidence carrier:
- a candidate with a clean wide reading such as
[10,20], compared with itself, reachesUndecidedOnEvidencebecause identical wide intervals correctly do not establish equality between two independently-valued subjects; currentcompare_pair(x, x)therefore returnsPairPendingEvidence, notPairNoDominance; - two complete payloads carrying one candidate identity but different exact readings can return
PairDominates, so the exported pair API can still say one structural candidate dominates itself.
Identity equality is not evidence of a duplicated field, but it is proof that the relation is a self-comparison. Preserve malformed-query precedence: admit the axis roster and reject any entry projector contradiction first. Then, before the declared-gap and ordinary axis-evidence folds, short-circuit equal candidate identities to PairNoDominance. Do not restore the refusal, and keep field_has_duplicate_identity field-only.
Add one permanent control with three cases:
- one candidate with a wide interval compared with itself =>
PairNoDominance; - two complete payloads sharing one identity but carrying different readings =>
PairNoDominance; - those two rows placed together in one field =>
SelectionRefused.
Both the intermediate refusal implementation and the current fall-through implementation must fail that control. Regenerate std_pareto.rs and obtain fresh exact-head CI.
Run 33683379804 is still in progress and will be superseded by the source edit. Do not merge the current head.
briansrls
left a comment
There was a problem hiding this comment.
Follow-up on exact head c12cf966ce359df8511ce03a715f00868994ece5: one correction to my permanent-control prescription in review 5095265887.
The three self-relation cases there are necessary but not sufficient to pin the required precedence. A mutant that moves the equal-identity short-circuit to the top of compare_pair would satisfy all three while laundering malformed evidence into PairNoDominance.
The control must therefore also exercise the self relation under malformed input:
- equal candidate identity + duplicated axis roster =>
PairRefused; - equal candidate identity + projector contradiction (duplicate reading, or complete-but-absent funded reading) =>
PairRefused.
Those cases pin the intended order:
axis-roster contradiction > entry/projector contradiction > self relation > honestly declared gap > ordinary pair evidence.
Killing mutations the permanent control must reject are now four distinct shapes: (1) restore the fail-shut equal-identity PairRefused; (2) leave the current fall-through, which yields pending/dominance on wide/divergent same-identity payloads; (3) short-circuit equal identity before axis-roster admission; (4) short-circuit equal identity before projector admission.
No extra semantic surface is being added: field_has_duplicate_identity remains field-only. This only makes the exported pair relation structurally irreflexive without letting that relation mask malformed query evidence.
…cted The previous commit deleted the wrong answer to compare_pair(x, x) -- a refusal -- and left the axis fold to produce the right one. It does not, and I asserted that it did in a comment and a commit message without ever running it. Two ways the fall-through is wrong, both reachable through the exported API: A clean WIDE reading such as [10,20] compared with itself reaches UndecidedOnEvidence, so compare_pair returned PairPendingEvidence. That arm is correct between two INDEPENDENTLY-VALUED subjects -- identical wide intervals do not establish equality -- and wrong here, because this is one subject. The point-identical case happened to reach PairNoDominance, which is why the defect was invisible to the fixtures already present. Two complete payloads carrying one candidate identity but different exact readings returned PairDominates: the exported pair API reporting that a structural candidate dominates ITSELF. Identity equality is still NOT evidence that some field holds a duplicate -- that is a field-population property two operands cannot carry, so this does not refuse and field_has_duplicate_identity stays field-only. But it IS proof the relation is a self-comparison, and nothing dominates itself. Precedence: the axis roster and either operand's projector contradiction are defects in what was ASKED and still outrank the answer; identity equality then short-circuits ahead of declared gaps and the axis fold, since a gap cannot make a subject fail to tie with itself. Control a_subject_does_not_dominate_itself carries the reviewer's three cases, and case 3 is the one that keeps the other two honest: the same two rows placed together in a FIELD must still yield SelectionRefused, so answering a self-comparison at pair grain cannot be read as admitting duplicates. Both prior implementations red it, verified: the intermediate refusal, and the fall-through with no identity arm. 17/17 controls pass; std_pareto.rs regenerated, first_generation_equal=true. Reported on review 5095265887, which was right. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_019LhF5WCbZqrZHPqsnjpkYu
briansrls
left a comment
There was a problem hiding this comment.
Exact-head review at 2ed233a54da980792d831d012bc069db4e56e130: REQUEST_CHANGES, narrowly on the permanent discriminator.
The source repair itself is correct. compare_pair now admits malformed query structure first (axis-roster contradiction, then either operand's projector contradiction), constructs equal candidate identity as PairNoDominance, then consults declared gaps, then folds axis evidence. This closes both concrete self-comparison failures from the prior head without reintroducing the field-population refusal. field_has_duplicate_identity correctly remains field-only.
The new control is not yet strong enough for the invariant the source now states. a_subject_does_not_dominate_itself carries only three cases: wide self-comparison, same-identity/different-readings, and duplicate identity placed in a field. Those kill the two prior implementations, but they do not kill precedence regressions.
Two mutations currently survive all three cases:
- move the identity-equality
PairNoDominancearm ahead ofaxis_roster_contradiction/entry_contradicts_its_declaration; malformed self-comparisons are then laundered intoPairNoDominancewhile the control stays green; - move identity equality below
declared_gap_cause; a clean gapped entry compared with itself then becomesPairEvidenceIncomplete, contradicting the new source claim that a gap cannot make a subject fail to tie with itself, while all three current cases stay green.
Extend the same permanent control to pin the whole ordering it claims:
- clean wide
xvsx=>PairNoDominance; - same identity, differing complete readings =>
PairNoDominance; - same identity in two field positions =>
SelectionRefused; - clean self-comparison under
duplicated_axes=>PairRefused; - a projector-malformed row compared with itself (existing
entry_reading_holeorentry_double_reading) =>PairRefused; - a clean honestly-gapped row compared with itself (existing
entry_gap_but_best) =>PairNoDominance.
The first three prove the relation answer; the next two prove malformed-query > self; the last proves self > honest incompleteness. Each boundary in the source precedence is then executable rather than prose.
No std.pareto semantic change is requested on this head; this is a witness-strengthening change. The in-flight exact-head run 33687465230 belongs to the current weaker-control head and will be superseded by that witness edit.
Do not merge 2ed233a54da980792d831d012bc069db4e56e130.
|
Floor red on This branch now has five heads, none of which touch the affected modules:
Same tree, same modules, alternating outcomes — and across three different module sets now ( So the class is a population of rows sitting close enough to the 500ms CPU ceiling that runner load decides which ones get preempted, not a defect in any one module and not this diff. Two of the three rows above are in the module that I am not re-running this to green. Separately, review 58947 is being addressed by a source edit (the quadratic fold in — sent from fierce-ant-136 |
…mply linearity Review 58947 found a §6 cost-shape defect in axis_roster_contradiction and it was worse than reported: the fold did TWO full-list scans per element, a count_axis_identity over the whole roster plus an already-named scan, not one. §6 is explicit that a quadratic fold is always fixed regardless of realized n, so the realized roster being small is not the argument and is not offered as one. The scan now carries the prefix already traversed and emits exactly when an identity's prefix count is 1 -- its SECOND occurrence. Third and later copies see a count of 2 or more and add nothing, so one duplicated identity still yields exactly one cause without a separate already-named population to rescan. One lookup per element, one traversal. count_axis_identity and identity_already_named are both unreferenced now and are deleted rather than left as attractors. WHAT THIS IS NOT: it is not linear, and the comment says so instead of letting the improvement imply it. Exact duplicate detection needs a map, set or ordering to beat O(n*distinct), and std carries none -- so the review's suggested alternative, "consume an existing linear grouping/query surface", does not exist in this repo today. std.keyed_roster, the canonical duplicate-detection authority, documents itself as O(n^2) worst case in its own header for the same reason. Naming the floor is the honest form: a comment claiming a linear construction that the substrate cannot express would be another unexecuted assertion, which this PR has already produced three of. keyed_roster is not consumed here because it answers a different question: it locates the FIRST duplicate as evidence, where a roster scan owes one cause per duplicated identity. A linear grouping surface would dissolve both. Controls re-verified after the restructure, in both directions: emitting on every occurrence reds causes_sized_by_defects; never emitting reds it plus both axis-refusal controls. 17/17 pass; regen first_generation_equal=true. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_019LhF5WCbZqrZHPqsnjpkYu
Test-only. The source order was already right; the control was not. Three cases established the self-relation ANSWER and pinned none of its POSITION. The source states malformed axis roster > malformed projector > self relation > honest gap > fold and the comment claimed "a gap cannot make a subject fail to tie with itself" -- a sentence true of the code and asserted by nothing. Three reorderings passed every existing case: hoisting self above axis admission, above projector admission, or dropping it below declared_gap_cause, the last silently turning a self-comparison into PairEvidenceIncomplete. Six observations now, the last three each making one boundary crossable: duplicated axis roster on self -> PairRefused; projector-malformed self -> PairRefused; honestly gapped self -> PairNoDominance. All five killing mutations executed -- the intermediate refusal, the fall-through, and each reordering. The first attempt at the axis-reorder mutation did not apply cleanly and produced no red; it was redone as a minimal condition edit with the same observable effect, because a mutation that fails for the wrong reason establishes nothing. This is the same method failure this PR has produced three times, one line later and subtler: not an unexecuted claim about behaviour, but an unexecuted claim about ORDER. The rule review 5095502958 states is the sharper form -- every clause in a precedence claim needs a mutation that can cross that boundary, because running the headline is not running the order. 17/17 controls pass. No std.pareto change, so the generated mirror does not move. Reported on review 5095502958, which was right. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_019LhF5WCbZqrZHPqsnjpkYu
briansrls
left a comment
There was a problem hiding this comment.
Exact-head source/witness review at live PR head f2d5d4dff0d1ecf589af18f2d06475a3be6b5ad4: SOURCE APPROVED; LANDING HOLD pending terminal exact-head CI.
The precedence-control finding from review 5095502958 is closed. This commit is test-only: only dag/test/claim/pareto_selection_witness_test.dag moves; std.pareto and the generated mirror are unchanged.
a_subject_does_not_dominate_itself now owns the full order it describes, not just the self-relation answer. The six observations discriminate: wide self -> PairNoDominance; same identity/different readings -> PairNoDominance; duplicate identity in a field -> SelectionRefused; self under duplicated axes -> PairRefused; projector-malformed self -> PairRefused; honestly-gapped self -> PairNoDominance. Those pin malformed axis roster > malformed projector > self relation > honest gap > evidence fold.
The five named killing mutations are the right set: restore the equal-identity refusal, remove the identity arm, hoist self above axis admission, hoist self above projector admission, and move self below the declared-gap gate. The last three each cross one stated precedence boundary; none is now prose-only.
I also accept the process correction: a mutation that failed to apply and produced no red is no evidence. Recasting the axis mutation as a minimal condition edit with the same observable semantic fault is the right falsifier shape.
No further source or witness change is requested on this head.
This APPROVE clears my superseded CHANGES_REQUESTED state; it is not merge authorization yet. Workflow run 33691767100 for this exact head is still in progress. Do not merge until I issue an explicit landing approval after terminal CI and the normal forward-delta adjudication if public main moves materially.
Materiality adjudication of public
|
briansrls
left a comment
There was a problem hiding this comment.
LANDING APPROVED on exact head f2d5d4dff0d1ecf589af18f2d06475a3be6b5ad4.
The final hold is discharged.
- Workflow run
33691767100is terminal SUCCESS on this exact head. Its six jobs are all terminal:required-witnesses-build,required-witnesses-floor,rust-unit-tests,fabric-evidence, and aggregatewitnessessucceeded;emit-copy-qualification-batterywas skipped by its own condition. - The forward-composition census is complete through current public
main@7c7bfb49c0c3fdc806f6f0ddb48492a31bd40008. GitHub reports exactly 31 commits from tested baseab4e3a4ac4da8a939e5448bb90d03754c066b5fcto that current tip, matching the PR's materiality adjudication. There is no unadjudicated tail. - I accept that adjudication as non-material to #10066's semantic/import/generated-output/acceptance closure. The
std.paretoreceipt-census reader is observational only; the floor-harness changes are additive measurement / clippy-roster work with no new refusal or verdict-composition rule, and #10133 reduces rather than increases this PR's preemption exposure. - The stale Codex review is not a landing prerequisite: it is against a superseded head and is not an adverse current-head finding.
The earlier source/witness approval remains valid. No rerun for byte-currency is owed under the banked composition rule. Later neutral public movement does not revoke this approval; later material movement would.
You may merge #10066 at this exact head.
The defect
compare_pairanswered the dominance question from readings alone and never readmissing_inputs, whilechallenger_applies— twenty lines away in the same file — excluded exactly those challengers from the field fold. Two answers to one question, and the exported one was the permissive arm.Found while migrating a private consumer onto #9959's interval evidence, and measured there rather than reasoned about: a board declaring unproven supply depth was reported by
compare_pairas dominating a peer at the low memory price, whileentry_standingreported that same candidateNotComputable. Any caller reaching the pair API directly — which is exported — got a dominance verdict from a candidate whose own standing says its inputs are incomplete.This is the same class as the
pair_dominatesdeletion this file already carries, one layer out: a pair-level answer that outruns its evidence. That tombstone says "the standing path is the only path, and a caller that wants a Boolean must first say what it intends to do about a refusal" — butcompare_pairitself still let a caller skip the gap question entirely.The shape
PairEvidenceIncompleteis its own arm, deliberately neither of the two it sits between. A candidate that declares a gap has not been shown not to dominate — nothing was shown about it at all — and it is not malformed either, since declaring your missing inputs is the honest behaviour this spine asks for. The cause names the entry and its obligations, so a caller learns what would make the question answerable. Both operands are gated: an entry that cannot be evaluated cannot be shown dominated either.challenger_appliesis now the self-comparison guard alone. The eligibility rule lives incompare_pair, and the field fold derives its behaviour from the arm rather than restating it — one authority, andentry_standing's observable behaviour is unchanged.Evidence
entry_gap_but_bestis a new fixture that beats every other entry on both funded axes and declares an outstanding quote, so readings and declaration point in opposite directions — the only case on which a silent gate can be caught.challenger_applies(the old shape)That second row is exactly the pre-cut world, and it is the point: the standing path was always right; the pair API was the liar.
The existing fixture
entry_quote_pendingcould not have caught this — it declares a gap but is the worst entry on power (that axis isHigherIsBetter), so it could never dominate anything whatever the gate did. Reaching for it would have produced a control that passes in both worlds.Checks
pareto_selection_witness_test.first_generation_equal=true(verified before merging main; the two files drifting locally afterwards areNat/i64churn from Preserve authored identity on resolved type-reference leaves #10046 against a stale local binary, in files this PR does not touch — CI regenerates with a current compiler).cargo clippy --all-targets -- -D warningsgreen;cargo test --release -p v1-compiler --libgreen. Both remote, with the must-fail control run to prove the compiler was actually reached.Sequencing
Independent of private #33 and of the queued axis-scoped-gap cut. It does not change
ParetoEntry.missing_inputs' shape — it reads it — and no private consumer callscompare_pairany more, so there is no cross-repo churn. #33 remains the priority.🤖 Generated with Claude Code
https://claude.ai/code/session_019LhF5WCbZqrZHPqsnjpkYu