From 99d35312bf21420a7a0840b0e408e08198a0279d Mon Sep 17 00:00:00 2001
From: Hans Behrens <hwbehrens@users.noreply.github.com>
Date: Thu, 2 Jul 2026 18:31:02 -0700
Subject: [PATCH] fix: refuse to finalize spec when an assertion declaration
 failed to 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>
---
 Veil/Frontend/DSL/Module/Elaborators.lean    | 14 ++++++--
 Veil/Frontend/DSL/Module/Representation.lean |  6 ++++
 VeilTest/Regression/DroppedAssertion.lean    | 34 ++++++++++++++++++++
 3 files changed, 52 insertions(+), 2 deletions(-)
 create mode 100644 VeilTest/Regression/DroppedAssertion.lean

diff --git a/Veil/Frontend/DSL/Module/Elaborators.lean b/Veil/Frontend/DSL/Module/Elaborators.lean
index 2a322f56..d2f743d3 100644
--- a/Veil/Frontend/DSL/Module/Elaborators.lean
+++ b/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
diff --git a/Veil/Frontend/DSL/Module/Representation.lean b/Veil/Frontend/DSL/Module/Representation.lean
index cd2bb312..7dab973a 100644
--- a/Veil/Frontend/DSL/Module/Representation.lean
+++ b/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. -/
diff --git a/VeilTest/Regression/DroppedAssertion.lean b/VeilTest/Regression/DroppedAssertion.lean
new file mode 100644
index 00000000..10e3c3ca
--- /dev/null
+++ b/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