lex_spec_check: a spec parse error is not a falsification - #104
Merged
Conversation
…he DSL's no-literal limitation Found in a full-pipeline retest (LEX_PERSIST_TRACE=1) of #99-#103's fixes: spec mode wrote 5 properties comparing word_frequencies' List[(Str,Int)] result against literal lists/tuples (`== [("the", 4)]`), which the spec DSL cannot express — it has no list or tuple literal syntax at all (confirmed against crates/spec-checker/src/ast.rs's SpecExpr enum: no ETuple/EList node). Every one of those 5 calls hit "spec parse: spec parse error at byte N: expected primary expression, got Some(LBracket)" — and every one came back to the model as "spec falsified", because verdict() treated any non-zero exit that wasn't a recognised CLI-usage error as a falsification. A spec that never parsed never reached a verdict at all; reporting it as one is exactly the "broken tool that testifies" problem this same file's header comment already describes for a different case (#83). The model, told its property was disproven rather than malformed, kept "fixing" specs that were correct but unparseable, burning 4 of its 20 steps on retries of the same unsupported construct before running out of budget. Fixed by recognising the "spec parse:" prefix lex-cli wraps every parse failure in (crates/lex-cli/src/main.rs's `anyhow!("spec parse: {e}")`, confirmed stable across all three of its call sites) as an error, before the falsified fallback ever runs. Also documented the actual limitation in spec_agent.lex's prompt — assert length/an indexed element instead of whole-value equality against a literal. Verified both work against a real function: `length(words(x)) >= 1` and `words(x)[0] != ""` both genuinely Proved (1000 trials each) against a real List[Str]-returning function. 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.
Found in a full-pipeline retest of #99-#103's fixes: spec mode wrote 5
properties comparing a
List[(Str,Int)]result against literallists/tuples (
== [("the", 4)]), which the spec DSL genuinely cannotexpress — no list/tuple literal syntax exists in it at all (confirmed
against
spec-checker's ownSpecExprAST).Every one of those 5 calls hit a real parse error, and every one came
back to the model as
"spec falsified"— becauseverdict()onlyrecognized CLI-usage errors as non-falsifications, not spec-content
parse errors. A spec that never parsed never reached a verdict; this
tool's own header comment already describes exactly this failure mode
for a different case (#83: "a broken tool that testifies"). The model,
told a correct property was disproven, kept retrying the same
unsupported construct instead of fixing the actual problem, burning 4
of its 20 steps before running out of budget.
Fixed by recognizing the
"spec parse:"prefixlex-cliwraps everyparse failure in (confirmed stable across all three of its call
sites) as an error, ahead of the falsified fallback.
Also documented the real limitation in
spec_agent.lex's prompt —assert
length(...)/an indexed element instead of whole-valueequality against a literal. Both verified working against a real
List[Str]-returning function (genuinely Proved, 1000 trials each).Co-Authored-By: Claude Sonnet 5 noreply@anthropic.com