Lean kernel replay rejects any theorem whose proof reduces a string literal #93

Title: runBuiltinKernel rejects proofs that reduce a string literal (unknown constant 'Char.ofNat', or a spurious type mismatch)

Comparator's final step, the replay through the Lean kernel, rejects solutions that
the Lean compiler, lean4checker and nanoda all accept, whenever the proof has to
reduce a string literal. A match on a string literal and a decide on string
equality both trigger it; the same shapes over Nat literals pass.

Versions: comparator, lean4export and the toolchain all at v4.34.0; also
reproduced at v4.35.0-rc1. nanoda_lib at 4c544ed. Linux (WSL2, Ubuntu 24.04).

Reproduction

An empty package, no dependencies. lakefile.toml:

name = "repro"

[[lean_lib]]
name = "Repro"
globs = ["Repro.+"]

Repro/StrC.lean (challenge):

def strTag (s : String) : Nat :=
  match s with
  | "live" => 1
  | _ => 0

theorem strTag_live : strTag "live" = 1 := by sorry

Repro/StrS.lean (solution): the same file with := rfl in place of := by sorry.

str.json:

{
    "challenge_module": "Repro.StrC",
    "solution_module": "Repro.StrS",
    "theorem_names": ["strTag_live"],
    "permitted_axioms": ["propext", "Quot.sound"],
    "external_kernels": { "nanoda": ["nanoda_bin"] }
}

lake env comparator str.json:

Running nanoda kernel on solution
nanoda kernel accepts the solution
Running Lean default kernel on solution.
Lean default kernel rejects the solution
uncaught exception: while replaying declaration 'strTag_live':
(kernel) declaration type mismatch, 'strTag_live' has type
  @Eq Nat (strTag "live") (strTag "live")
but it is expected to have type
  @Eq Nat (strTag "live") 1

Second shape, clearer error

Repro/EqC.lean: theorem str_ne : ("live" = "dead") = False := by sorry,
solution with := by decide. Same config with "theorem_names": ["str_ne"]:

nanoda kernel accepts the solution
Lean default kernel rejects the solution
uncaught exception: while replaying declaration 'str_ne':
(kernel) unknown constant 'Char.ofNat'

Control: the same shape over Nat passes

def natTag (n : Nat) : Nat :=
  match n with
  | 5 => 1
  | _ => 0

theorem natTag_five : natTag 5 = 1 := rfl

nanoda kernel accepts the solution
Lean default kernel accepts the solution
Your solution is okay!

Only the literal differs.

What rules out the obvious explanations

• The solution files compile normally, so the elaborator and the kernel accept
  these proofs in an ordinary environment.
• lake env leanchecker Repro.StrS replays the compiled module through the kernel
  and accepts it. The kernel is fine; the export/parse/replay path is not.
• nanoda accepts the very same export, so the export carries what a kernel needs.
• Char.ofNat is in the export. Parsing the NDJSON of the str_ne case gives
  365 declaration records, among them Char.ofNat, Char.ofNatAux,
  Char.ofNat._proof_1, String.ofList and String.decEq — yet replay reports
  unknown constant 'Char.ofNat'.

Cause

Lean/Replay.lean:74 decides what a declaration needs before adding it:

partial def replayConstant (name : Name) : M Unit := do
  if ← isTodo name then
    let some ci := (← read).newConstants[name]? | unreachable!
    replayConstants ci.getUsedConstantsAsSet

The dependencies are the constants the declaration mentions. A string literal
mentions nothing: Expr.lit (.strVal "live") is an atom. Char.ofNat and
String.ofList are needed not to read it but to reduce it, and by then they are
not in the environment. Hence the two symptoms: unknown constant where the
expansion is forced, and a failure to reduce — reported as a type mismatch — where
it is not. Nat literals are reduced by the kernel's own arithmetic and need no
constants, which is why the control passes.

lean4checker does not hit this because it replays into an environment whose
imports are already loaded, so those constants happen to be present. Comparator
replays into Lean.mkEmptyEnvironment, by design, and so meets the gap first.

A fix could sit on either side: comparator seeding the kernel environment with the
constants literal expansion needs, or Lean.Replay treating them as implicit
dependencies of every declaration.

Impact

Any development that distinguishes cases by string literals, which is normal in
modelling work, cannot use comparator's Lean-kernel step at all. The other five
steps, including statement comparison and the external kernel, work.