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

Veil/Core/Tools/ModelChecker/Symbolic/TraceLang.lean

@@ -62,9 +62,14 @@ syntax (name := traceAssertion) "assert " term:max : trace_line
 syntax traceLine := (traceAction <|> traceAssertion)
 syntax traceSpec := (traceLine colEq)*
 
+/-- The optional proof term must start on the same line as the closing brace.
+Without the `lineEq` guard, the parser greedily tries to consume whatever
+follows the trace command as its proof term; e.g. a subsequent
+`set_option ... in <command>` parses as a term up to `in` and then fails,
+taking the whole trace command down with it. -/
 syntax expected_smt_result "trace" ("[" ident "]")? "{"
   traceSpec
-"}" (term)? : command
+withPosition("}" (lineEq term)?) : command
 
 
 namespace Veil

Veil/Frontend/DSL/Module/Elaborators.lean

@@ -268,6 +268,8 @@ generating compiled model source. -/
 def Module.ensureSpecIsFinalized (mod : Module) (stx : Syntax) : CommandElabM Module := do
   if mod.isSpecFinalized then
     return mod
+  unless mod._failedAssertions.isEmpty do
+    throwError "cannot finalize the specification: the following assertion declaration(s) failed to elaborate: {mod._failedAssertions.toList}"
   let mod ← mod.ensureStateIsDefined
   throwIfNoInitializerDefined mod
   warnIfNoInvariantsDefined mod
@@ -590,9 +592,17 @@ def elabAssertion : CommandElab := fun stx => do
     | .stateConstraint => "state_constraint"
   withTraceNode (`veil.perf.elaborator.assertion ++ assertion.name) (fun _ => return s!"{kindStr} {assertion.name}") do
     -- Elaborate the assertion in the Lean environment
-    let mod' ← mod.defineAssertion assertion
+    try
+      let mod' ← mod.defineAssertion assertion
   --   dbg_trace s!"Elaborated assertion: {← liftTermElabM <|Lean.PrettyPrinter.formatTactic stx}"
-    localEnv.modifyModule (fun _ => mod')
+      localEnv.modifyModule (fun _ => mod')
+    catch ex =>
+      -- A failed assertion is not registered in the module. Record its name so
+      -- that `#gen_spec` refuses to finalize a specification that would
+      -- silently omit it (`#check_invariants` would then report all-green
+      -- without it).
+      localEnv.modifyModule (fun _ => { mod with _failedAssertions := mod._failedAssertions.push assertion.name })
+      throw ex
 
 @[command_elab Veil.genSpec]
 def elabGenSpec : CommandElab := fun stx => do

Veil/Frontend/DSL/Module/Representation.lean

@@ -374,6 +374,12 @@ structure Module where
   can still be added after this. -/
   protected _specFinalizedAt : Option Syntax := none
 
+  /-- Implementation detail. Names of assertion declarations that failed to
+  elaborate. Such assertions are not registered in `assertions`, so the
+  specification must not be finalized while any exist; otherwise the failed
+  assertion would be silently omitted from all subsequent checks. -/
+  protected _failedAssertions : Array Name := #[]
+
   /-- Assertions can be grouped into "sets", which are checked
   independently of each other. Sets are per-module. By default, all
   assertions are added to the same set. -/

VeilTest/Regression/DroppedAssertion.lean

@@ -0,0 +1,34 @@
+import Veil
+
+-- An assertion whose body fails to elaborate is not registered in the module.
+-- Previously, `#gen_spec` would then finalize the specification without it and
+-- `#check_invariants` would report all-green, silently omitting the property.
+-- Now `#gen_spec` refuses to finalize while failed assertion declarations exist.
+
+veil module DroppedAssertion
+
+type node
+
+relation r : node → Bool
+
+#gen_state
+
+after_init {
+  r N := false
+}
+
+action flip (n : node) {
+  r n := true
+}
+
+/-- error: Unbound uncapitalized variable: N' -/
+#guard_msgs in
+invariant [uniqueness] r N ∧ r N' → N = N'
+
+/--
+error: cannot finalize the specification: the following assertion declaration(s) failed to elaborate: [uniqueness]
+-/
+#guard_msgs in
+#gen_spec
+
+end DroppedAssertion

VeilTest/Regression/TraceTermTail.lean

@@ -0,0 +1,40 @@
+import Veil
+
+-- The trace command's optional proof term must start on the same line as the
+-- closing brace. Previously the parser greedily tried to consume whatever
+-- followed the trace command as its proof term: a subsequent
+-- `set_option ... in <command>` parsed as a term up to `in` and then failed
+-- ("unexpected token ...; expected spec"), taking the whole trace command down
+-- with it; error recovery then ran the inner command without the option.
+
+veil module TraceTermTail
+
+individual flag : Bool
+
+#gen_state
+
+after_init {
+  flag := false
+}
+
+action set_flag {
+  flag := true
+}
+
+invariant [flag_unset] ¬ flag
+
+#gen_spec
+
+#guard_msgs(drop warning, drop info) in
+sat trace [first] {
+  set_flag
+}
+
+#guard_msgs(drop warning, drop info) in
+set_option veil.violationIsError false in
+sat trace [second] {
+  set_flag
+  set_flag
+}
+
+end TraceTermTail