Kernel accesses uninitialized memory

[TwoFX]

Prerequisites

Please put an X between the brackets as you perform the following steps:

• Check that your issue is not already filed:
  https://github.com/leanprover/lean4/issues
• Reduce the issue to a minimal, self-contained, reproducible test case.
  Avoid dependencies to Mathlib or Batteries.
• Test your test case against the latest nightly release, for example on
  https://live.lean-lang.org/#project=lean-nightly
  (You can also use the settings there to switch to “Lean nightly”)

Description

Here is some code (discovered via fuzzing)

import Lean
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
  }
run_meta Lean.addDecl decl_0

It realiably crashes live.lean-lang.org. On my computer, it prints (kernel) unknown constant '__expr_for_default_constructor__'. In both cases, the problem appears to be the following line, where unfold_definition returns none_expr, but the code tries to extract the expression:

lean4/src/kernel/type_checker.cpp

Line 899 in 646f2fa

s_n = whnf_core(*unfold_definition(s_n), false, true);

It seems unlikely that this can be developed into an exploit.

Expected behavior: No crash on live.lean-lang.org

Actual behavior: Crashes live.lean-lang.org

Versions

Lean 4.25.0-nightly-2025-09-26

Impact

Add 👍 to issues you consider important. If others are impacted by this issue, please ask them to add 👍 to it.

[nomeata]

@copilot please prepare a draft PR for fixing this. The proper fix is to move the level parameter length check into is_delta. The invariant should be that if is_delta succeeds, then unfold_definition does.

[nomeata]

There are two issues playing together here:

1. For theorems, we check whether the type is a proposition before checking whether the type is type correct. This means that we evaluate and expression that can be type incorrect.
2. When defeq'ing we assume type correct input and stumble over this.

At some point in the past I have tried to exploit this behavior, but couldn't: I could not make the reduction of I'll typed terms have side effects that somehow make the kernel skip the later type check.

But it may still be prudent to make the kernel a bit more robust this way, and at least fix number 2.