`proj_idx` truncation: `size_t` → `unsigned`

Disclaimer: this bug was found autonomously by Opus 4.6 using this setup and has not been reviewed by a Lean expert yet. Below is its (unedited) report.

Prerequisites

• 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

In src/kernel/type_checker.cpp:

infer_proj, reduce_proj, and lazy_delta_proj_reduction all store projection indices in unsigned after an is_small() check — but is_small() only guarantees < 2^63, not < 2^32.

Example: Expr.proj(S, 2^32 + 1, e) → is_small() passes (fits in 64-bit) → get_small_value() returns 4294967297 as size_t → stored in unsigned → silently becomes 1.

proj_truncation_test.lean

Context

Zulip thread

Steps to Reproduce

1. Define a structure and construct an Expr.proj with index 2^32 (or any multiple of 2^32 plus k).
2. Reduce it via Lean.Kernel.whnf — the kernel silently treats it as index k.

import Lean                                                                                                              
                                                                                                                           
  structure Pair where                                                                                                     
    fst : Nat                                                                                                              
    snd : Bool                                                                                                             
                                                                                                                           
  open Lean in                                                                                                             
  #eval show MetaM Unit from do                                                                                            
    let val := mkApp2 (mkConst ``Pair.mk) (mkNatLit 42) (mkConst ``Bool.true)                                              
    let env ← getEnv                                                                                                       
    let lctx : LocalContext := {}                                                                                          
    let proj0 := Expr.proj ``Pair 0 val                                                                                    
    let projBig := Expr.proj ``Pair (2^32) val                                                                             
    match Lean.Kernel.whnf env lctx proj0, Lean.Kernel.whnf env lctx projBig with                                          
    | .ok r0, .ok rBig =>                                                                                                  
      IO.println s!"proj(Pair, 0,    Pair.mk 42 true) = {r0}"                                                              
      IO.println s!"proj(Pair, 2^32, Pair.mk 42 true) = {rBig}"                                                            
    | _, _ => IO.println "error"                                                                                           
    match Lean.Kernel.isDefEq env lctx proj0 projBig with                                                                  
    | .ok b => IO.println s!"Kernel.isDefEq(proj idx=0, proj idx=2^32) = {b}"                                              
    | .error _ => IO.println "isDefEq error"

Expected behavior: The kernel should reject proj(Pair, 2^32, ...) since Pair only has 2 fields (indices 0 and 1). It should not be definitionally equal to proj(Pair, 0, ...).

Actual behavior:

proj(Pair, 0,    Pair.mk 42 true) = 42
proj(Pair, 2^32, Pair.mk 42 true) = 42
Kernel.isDefEq(proj idx=0, proj idx=2^32) = true

See proj_truncation_test.lean

Versions

• Lean 4.28.0 (commit 7e01a1bf5c70)
• Lean 4.29.0-rc2 (commit 83e54b65b65d)
• Linux x86-64

Additional Information

N/A

Impact

Low. Normal Lean code never produces projection indices >= the field count. The bug requires constructing raw Expr.proj nodes via metaprogramming. The Meta layer rejects these, so exploitation would require bypassing Meta (e.g.,addDeclCore(doCheck := false) or crafted .olean files).

Start with src/kernel/type_checker.cpp and inspect infer_proj, reduce_proj, and lazy_delta_proj_reduction, then run the linked proj_truncation_test.lean reproduction against the reported Lean versions. Done means an oversized projection index is not silently treated as a smaller index, and the invalid projection is rejected rather than considered definitionally equal to a valid one.