fix: kernel: move level parameter count and thm-is-prop checks for robustness

src/kernel/environment.cpp

@@ -197,9 +197,9 @@ environment environment::add_theorem(declaration const & d, bool check) const {
         sharecommon_persistent_fn share;
         expr val(share(v.get_value().raw()));
         expr type(share(v.get_type().raw()));
+        check_constant_val(*this, v.to_constant_val(), checker);
         if (!checker.is_prop(type))
             throw theorem_type_is_not_prop(*this, v.get_name(), type);
-        check_constant_val(*this, v.to_constant_val(), checker);
         check_no_metavar_no_fvar(*this, v.get_name(), val);
         expr val_type = checker.check(val, v.get_lparams());
         if (!checker.is_def_eq(val_type, type))

src/kernel/type_checker.cpp

@@ -483,12 +483,12 @@ expr type_checker::whnf_core(expr const & e, bool cheap_rec, bool cheap_proj) {
 }
 
 /** \brief Return some definition \c d iff \c e is a target for delta-reduction, and the given definition is the one
-    to be expanded. */
+    to be expanded. If \c is_delta succeeds, then \c unfold_definition will also succeed. */
 optional<constant_info> type_checker::is_delta(expr const & e) const {
     expr const & f = get_app_fn(e);
     if (is_constant(f)) {
         if (optional<constant_info> info = env().find(const_name(f)))
-            if (info->has_value())
+            if (info->has_value() && length(const_levels(f)) == info->get_num_lparams())
                 return info;
     }
     return none_constant_info();
@@ -499,20 +499,18 @@ optional<expr> type_checker::unfold_definition_core(expr const & e) {
         if (auto d = is_delta(e)) {
             levels const & us = const_levels(e);
             unsigned len = length(us);
-            if (len == d->get_num_lparams()) {
-                if (m_diag) {
-                    m_diag->record_unfold(d->get_name());
-                }
-                if (len > 0) {
-                    auto it = m_st->m_unfold.find(e);
-                    if (it != m_st->m_unfold.end())
-                        return some_expr(it->second);
-                    expr result = instantiate_value_lparams(*d, us);
-                    m_st->m_unfold.insert(mk_pair(e, result));
-                    return some_expr(result);
-                } else {
-                    return some_expr(instantiate_value_lparams(*d, us));
-                }
+            if (m_diag) {
+                m_diag->record_unfold(d->get_name());
+            }
+            if (len > 0) {
+                auto it = m_st->m_unfold.find(e);
+                if (it != m_st->m_unfold.end())
+                    return some_expr(it->second);
+                expr result = instantiate_value_lparams(*d, us);
+                m_st->m_unfold.insert(mk_pair(e, result));
+                return some_expr(result);
+            } else {
+                return some_expr(instantiate_value_lparams(*d, us));
             }
         }
     }

tests/elab/10577.lean

@@ -0,0 +1,48 @@
+import Lean
+
+/-!
+Regression test for https://github.com/leanprover/lean4/issues/10577
+
+Before the fix, the kernel would crash (access uninitialized memory) when a constant was applied
+to the wrong number of universe levels.  The root cause was that `is_delta` could succeed for a
+constant even when the supplied universe-level count did not match the declaration's level-parameter
+count, but `unfold_definition` would subsequently return `none` for that same constant (because it
+did contain the level-count check).  The call site in `lazy_delta_reduction_step` unconditionally
+dereferenced the `unfold_definition` result, causing undefined behaviour.
+
+The fix moves the level-parameter-count check into `is_delta`, establishing the invariant:
+  **If `is_delta` succeeds then `unfold_definition` will also succeed.**
+-/
+
+-- Discovered via fuzzing; the important feature is that `false_of_true_eq_false`
+-- (which has 0 universe-level parameters) is applied with 1 universe level in some
+-- sub-expressions, while the surrounding declaration has `levelParams := []`.
+def name_0 : Lean.Name := .anonymous
+def level_0 : Lean.Level := .zero
+def name_1 : Lean.Name := .str name_0 "false_of_true_eq_false"
+def expr_0 : Lean.Expr := .lit (.natVal 0)
+def expr_1 : Lean.Expr := .const name_1 [level_0]
+def name_2 : Lean.Name := .str name_0 "Eq"
+def expr_18 : Lean.Expr := .const name_2 [level_0]
+def expr_8 : Lean.Expr := .letE `d (.bvar 0) (.bvar 0) (.bvar 0) false
+def expr_10 : Lean.Expr := .const name_1 []
+def expr_11 : Lean.Expr := .app expr_10 expr_8
+def expr_13 : Lean.Expr := .app expr_18 expr_0
+def expr_16 : Lean.Expr := .letE `c expr_11 (.bvar 0) (.bvar 0) false
+def expr_27 : Lean.Expr := .app (.app expr_13 expr_1) expr_0
+def expr_30 : Lean.Expr := .letE `b (.bvar 0) expr_27 expr_16 false
+def expr_36 : Lean.Expr := .letE `a (.sort level_0) expr_10 expr_30 false
+def decl_0 : Lean.Declaration :=
+  .thmDecl {
+    name := `foo42
+    levelParams := []
+    type := expr_36
+    value := expr_10
+  }
+
+open Lean
+
+/-- error: (kernel) let-declaration type mismatch 'a' -/
+#guard_msgs in
+run_meta
+  setEnv (← ofExceptKernelException <| (← getEnv).addDeclCore 0 decl_0 none)

tests/elab/bvarcrash.lean

@@ -636,9 +636,8 @@ open Lean
 run_meta do
   for decl in [decl_0, decl_1, decl_2, decl_3, decl_4, decl_5, decl_6, decl_7, decl_8] do
     setEnv (← ofExceptKernelException <| (← getEnv).addDeclCore 0 decl none)
-/--
-error: (kernel) type checker does not support loose bound variables, replace them with free variables before invoking it
--/
+
+/-- error: (kernel) constant has already been declared '«term_+_»' -/
 #guard_msgs in
 run_meta
     setEnv (← ofExceptKernelException <| (← getEnv).addDeclCore 0 decl_9 none)