Skip to content

fix: require the trace proof term to start on the line of the closing brace#16

Closed
hwbehrens wants to merge 4 commits into
verse-lab:veil-2.0-previewfrom
hwbehrens:veil-2.0-preview
Closed

fix: require the trace proof term to start on the line of the closing brace#16
hwbehrens wants to merge 4 commits into
verse-lab:veil-2.0-previewfrom
hwbehrens:veil-2.0-preview

Conversation

@hwbehrens

Copy link
Copy Markdown

set_option ... in fails to parse when the immediately preceding command is a trace command:

sat trace [can_acquire] {
  acquire
}

set_option veil.violationIsError false in
sat trace [handoff] {
  acquire
  release
  acquire
}
error: unexpected token 'sat'; expected spec
info: ✅ Satisfying trace found

The trace command's grammar ends with a bare optional proof term:

syntax expected_smt_result "trace" ("[" ident "]")? "{" traceSpec "}" (term)? : command

set_option X in <term> is valid term syntax, so after } the parser consumes the following command as the trace's proof term, commits past in, and fails on sat ("expected spec" is the furthest-progress expectation, from the scoped spec : term rule). The consequences:

  • the preceding trace command fails to parse as a whole, so it never runs and its result message is lost (the info above is from the second trace only);
  • error recovery re-runs the inner command as a bare command, without the option applied;
  • a term-shaped line after a trace parses successfully and is silently elaborated as the trace's proof term (a stray trivial after a trace reports an unrelated "Type mismatch").

This PR requires the proof term to start on the same line as the closing brace:

withPosition("}" (lineEq term)?)

The module above then parses and both traces run, with the option applied to the second. VeilTest/Regression/TraceTermTail.lean covers the trace-then-scoped-trace pattern, and the full lake build (Veil + VeilTest) passes.

Two notes:

  1. Proof terms that started on the line after the } no longer parse. I found no in-tree usage; nothing in VeilTest or Examples passes a proof term to a trace.
  2. A bare lineEq without an enclosing withPosition is a silent no-op, since there is no saved position to compare against. pickExpression in Veil/Frontend/DSL/Action/Syntax.lean uses kw_pick (lineEq term)? without one, so its guard may be vacuous as well; happy to look at that separately if useful.

hwbehrens and others added 4 commits July 2, 2026 19:27
…elaborate

An assertion whose body fails to elaborate is reported as an error but
is not registered in the module. #gen_spec then finalized the
specification without it and #check_invariants reported all green,
silently omitting the property the user wrote.

elabAssertion now records the names of failed assertion declarations,
and Module.ensureSpecIsFinalized refuses to finalize while any exist.
Since all checking commands require a finalized spec, nothing downstream
can run against a specification that silently lost an assertion.

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
… brace

The trace command's optional proof term was a bare (term)?, so the
parser greedily tried to consume whatever followed the trace command as
its proof term. A subsequent set_option ... in <command> parses as a
term up to 'in' and then fails, taking the whole trace command down
with it: the trace never runs, its result message is lost, and error
recovery then runs the inner command without the option applied. A
term-shaped follow-up line was silently swallowed as the proof term.

Guard the tail with withPosition/lineEq so the proof term must start on
the same line as the closing brace. (A bare lineEq without withPosition
is a no-op, since there is no saved position to compare against.)

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
fix: require the trace proof term to start on the line of the closing brace
fix: refuse to finalize spec when an assertion declaration failed to elaborate
@hwbehrens hwbehrens closed this by deleting the head repository Jul 3, 2026
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant