graph, verification: attest a clean verify pass (#32) - #150
Merged
Conversation
verified.type_check/.spec_check/.test are written automatically by lex-llm's dispatcher whenever lex_check/lex_spec_check/lex_test reports a pass. lex_run isn't in that list, and shouldn't be added there generically -- an ordinary build-mode lex_run passing proves nothing, only a VERIFY-mode one that found no FAIL does, and the dispatcher has no notion of agent mode. So a clean verify pass -- the strongest evidence in the system, an independent re-derivation that never trusted the implementation -- left no durable trace: a review agent or task_spec.lex criterion in a later session had no way to check "was this independently verified," only "did it type-check." Added a fourth kind, verified.independent_check, written directly by the fix-loop's verify gate (attest_verify_pass_if_clean, called from run_agent_with_events/run_agent_persistent_with_events right after verify_found_failure comes back false) via trail_log.append, then promoted into .lex/verified.jsonl the same way harvest/append_all already promotes the other three -- since the turn's own harvest already ran before this code gets a chance to write anything, this harvests+appends just the one new event rather than waiting for a later turn to pick it up. Validated two ways: a live end-to-end run isolating the gate (empty setup, a genuinely correct src/abi.lex this time -- which needed two MORE real bugs fixed beyond the accumulator overwrite this session already knew about: u_word never zero-padded to 32 bytes at all, and ABool's encoding wrongly concatenated an extra byte) confirmed the tool-call/event shape works, though the run itself was slow and error-prone enough on this local model that it wasn't worth waiting out to completion; a fast deterministic unit-level check (hand-built event lists, both branches) confirmed the write-on-clean-pass and no-write-on-FAIL paths precisely. Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>
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.
Summary
verified.type_check/.spec_check/.testare written automatically by lex-llm's dispatcher wheneverlex_check/lex_spec_check/lex_testreports a pass.lex_runisn't in that list, and shouldn't be added there generically — an ordinary build-modelex_runpassing proves nothing, only a VERIFY-mode one that found no FAIL does, and the dispatcher has no notion of agent mode. So a clean verify pass — the strongest evidence in the system, an independent re-derivation that never trusted the implementation — left no durable trace: areviewagent ortask_spec.lexcriterion in a later session had no way to check "was this independently verified," only "did it type-check."verified.independent_check, written directly by the fix-loop's verify gate (attest_verify_pass_if_clean, called fromrun_agent_with_events/run_agent_persistent_with_eventsright afterverify_found_failurecomes back false) viatrail_log.append, then promoted into.lex/verified.jsonlthe same wayharvest/append_allalready promotes the other three.verified = ["verified.independent_check"].Test plan
lex check/lex fmt --check/lex doc-sync --check— cleanlex test tests— 4/4 existing tests still pass.lex/verified.jsonlwith the right shape; a FAIL present writes nothingsrc/abi.lex— confirmed the tool-call/event shape works (found and fixed two more real bugs in the fixture along the way:u_wordnever zero-padded to 32 bytes, andABool's encoding wrongly concatenated an extra byte), though the run was slow/error-prone enough on the local model that the deterministic check is what actually pins the behavior🤖 Generated with Claude Code