fix(tri): walk every last N, not the first -- and an anchor pins the population, not the instrument - #3037
Merged
Merged
Conversation
…e population, not the instrument
`window_markers` asked `low.find("last ")` -- the FIRST occurrence and no
other -- then whether a digit followed. Section 439 says "reads the last
COMMIT message" on its line 18, where no digit follows, and "Over the
last 20 commit messages on master" on line 27. The rule stopped at the
first and returned nothing.
So section 439 was absent from its own population, and it is the section
that produced the 4-against-33 row of section 457's own table. The
one-variable probe is the whole proof: same tree, same command, `find`
against `match_indices`, 19 against 20.
`find` answers "does the FIRST occurrence satisfy this" and the question
is "does ANY". On one line the two agree; on a page of prose they do not,
and a page of prose is the only text this rule reads.
Then the sharper half. Section 457 published `12 of 420` anchored to
c039ebe, and that number reproduces exactly at that commit -- an audit
re-took every anchored figure, twelve of twelve, and none failed. But
re-run at the same anchor with the FIXED tool it is 13 of 420.
The anchor was right and the instrument was not. A figure over a fixed
population is re-takeable only by someone holding the same binary, and
nothing in "over the 20 commits ending at <sha>" says which binary. The
data anchor and the tool version are two different anchors, and section
457 named one of them. That does not weaken anchoring, it completes it:
an unanchored figure cannot be re-taken at all, while an anchored one can
be re-taken and disagreed with, which is what happened here.
Section 457 is corrected in place.
Two process notes. The probe was not mine -- a read-only fan-out
instructed to attack the previous pass's own numbers wrote it, and its
refuter narrowed the charge correctly: 457 never claimed 439 was among
the twelve, so the membership complaint falls and the matcher defect
stands. And the first mutant written to prove this fix did not compile
(`break` outside a loop, left over from the loop it removed); it was
reported as never built rather than scored as a kill.
Skill section 465.
Refs #2994
Contributor
Contributor
|
📓 NotebookLM Notebook linked to this PR
This notebook contains session context, decisions, and artifacts for this work. |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
findanswers a different question than the rule askedwindow_markersaskedlow.find("last ")— the first occurrence and no other — then whether a digit followed. §439 says "reads the last COMMIT message" on its line 18, where no digit follows, and "Over the last 20 commit messages on master" on line 27. The rule stopped at the first and returned nothing.So §439 was absent from its own population — and it is the section that produced the 4-against-33 row of §457's own table.
The one-variable probe is the whole proof. Same tree, same command:
find("last ")match_indices("last ")findanswers "does the FIRST occurrence satisfy this?" and the question is "does ANY?". On one line the two agree; on a page of prose they do not, and a page of prose is the only kind of text this rule reads.The same anchor, a different instrument, a different number
§457 published
12 of 420anchored toc039ebebe, and that number reproduces exactly at that commit — an audit re-took every anchored figure this loop published, twelve of twelve, and none failed.Re-run at the same anchor with the fixed tool it is 13 of 420.
The anchor was right and the instrument was not. A figure over a fixed population is re-takeable only by someone holding the same binary, and nothing in "over the 20 commits ending at
<sha>" says which binary. The data anchor and the tool version are two different anchors, and §457 named one of them.This does not weaken anchoring — it completes it. An unanchored figure cannot be re-taken at all. An anchored one can be re-taken and disagreed with, which is what happened here, and the disagreement is the finding. §457 is corrected in place.
Two process notes
The probe was not mine. A read-only fan-out instructed to attack the previous pass's own numbers wrote it. Its refuter then narrowed the charge correctly: §457 never claimed §439 was among the twelve, so the membership complaint falls and the matcher defect stands.
The first mutant did not compile —
breakoutside a loop, left over from the loop it removed — and was reported as never built rather than scored as a kill. §455's fourth arm arriving in a new place. The corrected mutant, a faithful revert tofind, kills the probe test.cargo test -p tri— 517 passed, 0 failedRefs #2994