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

[hwbehrens]

If an assertion's body fails to elaborate (say, a typo like a primed variable C', or a capitalized variable that happens to resolve to an existing global), the declaration errors but the assertion is simply not registered in the module. #gen_spec then finalizes the specification without it, and #check_invariants reports all green. The property the user wrote is silently gone; if the model has a bug that property would catch, the report still looks like a clean pass. On a small mutex model with safety [mutual_exclusion] holds C ∧ holds C' → C = C':

error: Unbound uncapitalized variable: C'
info: Initialization must establish the invariant:
  doesNotThrow ... ✅
  lock_consistency ... ✅
The following set of actions must preserve the invariant and successfully terminate:
  acquire
    doesNotThrow ... ✅
    lock_consistency ... ✅
  ...

mutual_exclusion appears nowhere in the roster, and in a 40+ minute build log the lone error line is easy to lose while the wall of green reads as verified, which nearly bit me.

This PR makes the failure impossible to miss. elabAssertion records the names of assertion declarations that fail to elaborate, and Module.ensureSpecIsFinalized refuses to finalize the specification while any exist. Since #check_invariants, #check_action, trace commands, and #model_check all require a finalized spec, nothing downstream can run against a specification that silently lost an assertion. Same model, after:

error: Unbound uncapitalized variable: C'
error: cannot finalize the specification: the following assertion declaration(s) failed to elaborate: [mutual_exclusion]
error: The specification of module Mutex has not been finalized. Please call #gen_spec first!

The change is pretty small: a _failedAssertions : Array Name field on Module, a try/catch in elabAssertion that records the name and rethrows, and the finalization gate. VeilTest/Regression/DroppedAssertion.lean guards both the declaration error and the new #gen_spec error. Full lake build (Veil + VeilTest) passes.

One design choice though: a recorded failure is not scrubbed if a later declaration with the same name succeeds; the broken declaration still has to be fixed or removed. Scrubbing would reopen the silent-omission path, since a later unrelated assertion reusing the name could mask the failed one.

Happy to adjust if needed, for instance a warning instead of a hard error, or reporting the dropped names in the #check_invariants output as well.