fix: refuse to finalize spec when an assertion declaration failed to elaborate

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