missions: a pre-#632 PASS line is a PASS, and its unstated kernel stays unstated - #643
Open
DrMurphyIsIn wants to merge 3 commits into
Open
DrMurphyIsIn wants to merge 3 commits into
DrMurphyIsIn wants to merge 3 commits into
Conversation
…ys unstated Backfilling the records written before the new checks, a different session hit a refusal that was both wrong and misleadingly worded: all five pre-#632 records came back "no job in this run printed a COMPARATOR PASS for <node>", although the logs plainly contain PASS lines for them. `kernel=` was added to the judge's PASS line by #632. Before that the line ended at `run=`, and the parser required the field, so every legacy line failed to match and the node looked unjudged. The field is now optional. What the record says about such a run matters more than the parse. A pre-#632 log states no kernel mode, so the tool does not invent one: `kernel_mode` is recorded as "unstated", `provenance-report` and `mission verify` surface it ("the judge log predates the kernel field, so the recorded second kernel is the recorder's reading, not the log's word"), and `--strict-provenance` makes it an error. That is the same rule as the rest of this tooling: a check that could not be made leaves a mark in the record, not only in a terminal. One case is refused outright rather than merely marked: `--lean-kernel-only` against a legacy log. `heavy_certificates` did not exist when those runs judged their nodes, so nanoda DID replay the export; a record claiming otherwise would be false, not merely unconfirmed. Verified against the real pre-#632 dbn log (job 107864773418 of run 36059451077): its four nodes now parse with `legacy = True`, a record with no kernel claim is accepted, and a Lean-kernel-only claim is refused with that reason. 9 new tests, 74 across the provenance files, 422 in the broad suite. conjecture1_proved = False (unchanged; provenance tooling only). Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_017icTazCuXLgRx61VNRAZWU
…marker means it Two problems behind the reviewer's messaging nit, one of them a latent trap. The console printed "second kernel: nanoda" and the report spoke of "the recorded second kernel" while the record contained no such field: `second_kernel` defaulted to "nanoda" and is only serialised when it differs, so a legacy record silently ASSERTED that nanoda replayed the export -- which is precisely what its log does not say. A legacy record now carries `second_kernel = "unstated (pre-#632 log)"`, written out, and the report says the log "does not state which second kernel ran" rather than implying someone read it. The trap: `lean_kernel_only` was computed as `second_kernel != "nanoda"`, so ANY other value read as the strong claim that the second kernel was skipped. Writing "unstated" would therefore have made all five legacy records announce themselves as "Lean kernel only (heavy_certificates: nanoda not run)" -- an overstatement of what was checked, in the exact direction this tooling exists to prevent. It now tests the heavy marker itself. Caught by looking at who consumes the field before changing it, not by a test; the new tests pin both halves so it cannot come back. conjecture1_proved = False (unchanged; provenance tooling only). Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_017icTazCuXLgRx61VNRAZWU
Three conflicts, all where #645's compositional judge and this branch's legacy reading touch the same code. judge_log._PASS: both sides made a tail optional. #645 added `judge=/parts=`, this branch made `kernel=` optional. The combined form is kernel optional THEN the judge tail optional, so all four shapes the judge has ever printed parse: a pre-#632 line ending at `run=`, an ordinary modern line ending at `kernel=`, a heavy `kernel=lean-kernel-only` line, and a compositional line with `judge=compositional parts=9`. Verified on one real example of each. `Verdict` keeps both sides' fields and the `legacy` property. cli.comparator_record: kept main's compositional branch and this branch's reading of an absent kernel field, so `kernel_mode` is `verdict.kernel or "unstated"` and the compose path is untouched. provenance.ProvenanceRow: kept every field from both sides (kernel_mode, judge_via, judge_mode, parts) and all four assignments. 460 tests pass across the judge, compose, provenance, mission, schema, verify and CI suites, including test_compose.py's compositional parse tests. conjecture1_proved = False (unchanged; provenance tooling only). Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_017icTazCuXLgRx61VNRAZWU
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
1 participant
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.
Follow-up to #641, found by a different session backfilling the records written before those checks existed.
The bug
All five pre-#632 records were refused with "no job in this run printed a COMPARATOR PASS for
<node>" — while the logs plainly contain PASS lines for them.kernel=was added to the judge's PASS line by #632; before that the line ended atrun=:The parser required the field, so every legacy line failed to match and the node looked unjudged. That is wrong, and the message was misleading about a log that did contain a pass.
What changes
kernel=is optional. But what the record then says about such a run matters more than the parse:kernel_mode = "unstated", never inferred from the caller's switchprovenance-reportandmission verifysurface it;--strict-provenancemakes it an error--lean-kernel-onlyon a legacy logThat last one is not pedantry.
heavy_certificatesdid not exist when those runs judged their nodes, so nanoda did replay the export. A record claiming Lean-kernel-only would be false, not merely unconfirmed.Everything else follows the rule the rest of this tooling uses: a check that could not be made leaves a mark in the record, not only in a terminal.
Verification
Against the real pre-#632 dbn log (job 107864773418 of run 36059451077):
legacy = Trueand an empty kernel field;second_kernelreads as unknown rather than asnanoda;9 new tests (including that modern and legacy lines coexist in one log), 74 across the provenance files, 422 in the broad suite.
conjecture1_proved = False(unchanged; provenance tooling only).🤖 Generated with Claude Code
https://claude.ai/code/session_017icTazCuXLgRx61VNRAZWU