Beta-cache re-entry can create cyclic metavariable assignments

betaLambdaEnv can overwrite a cached parameter with an expression containing that same parameter. Re-entering the identity lambda with 0 :: previousResult changes the assignment from ?xs := [] to ?xs := 0 :: ?xs.

The following bounded check detects the cycle without attempting to expand it. It fails on f5172bf69dc3015592788c4b9aba896e0bea54c4 (PR #241, before the specialization prototype):

import Tests.Utils
open Lean Meta Elab Command Blaster.Optimize
run_cmd liftTermElabM do
  let lam ← Tests.parseTerm (← `(fun xs : List Nat => xs))
  let empty := mkApp (mkConst ``List.nil [levelZero]) (mkConst ``Nat)
  let check : TranslateEnvT Unit := do
    let first ← betaLambdaEnv (← hashcons lam) #[← hashcons empty]
    let argument ← mkApp3Expr (mkConst ``List.cons [levelZero]) (mkConst ``Nat)
      (mkNatLit 0) first.betaReduced
    let second ← betaLambdaEnv (← hashcons lam) #[argument]
    let value ← getMVarValue second.betaReduced
    if (value.find? (fun e => exprEq e second.betaReduced)).isSome then
      throwError "beta-cache reuse created a cyclic metavariable assignment"
  check.run' (default : TranslateEnv)

Run with lake build Tests.Benchmarks.BetaCacheReentrant after saving the file at that module path. The reported error is beta-cache reuse created a cyclic metavariable assignment.

Expected: the nested invocation denotes [0], and restoring its saved assignments recovers the outer invocation's [].

Actual: the cached metavariable occurs in its own assigned value. Following that assignment can grow the instantiation stack without bound. The new demand-driven CEK experiment exposed this during a seven-transition identity application; the small direct API reproducer does not require that experiment.

The usual eager argument normalization masks many instances. Cache reuse must snapshot arguments under the old assignment environment before rebinding cached metavariables, including over-application arguments and simultaneous substitutions. This report establishes a cyclic assignment and nontermination risk; it does not claim a demonstrated false Valid verdict.

Checked existing issues/PRs for beta-cache/metavariable fixes; none found covering this collision.

Save the reproducer as Tests.Benchmarks.BetaCacheReentrant and run lake build Tests.Benchmarks.BetaCacheReentrant to observe the cyclic assignment. Start by tracing betaLambdaEnv, TranslateEnvT, and the cached metavariable restoration path. Done means the nested invocation yields [0], restores the outer [], and no cyclic assignment is detected.