fix: missing file

src/Lean/Meta.lean

@@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 module
-
 prelude
 public import Lean.Meta.Basic
 public import Lean.Meta.LevelDefEq
@@ -59,3 +58,4 @@ public import Lean.Meta.TryThis
 public import Lean.Meta.Hint
 public import Lean.Meta.MethodSpecs
 public import Lean.Meta.CtorIdxHInj
+public import Lean.Meta.Sym

src/Lean/Meta/Sym.lean

@@ -0,0 +1,86 @@
+/-
+Copyright (c) 2025 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+module
+prelude
+public import Lean.Meta.Sym.SymM
+public import Lean.Meta.Sym.Main
+public import Lean.Meta.Sym.Util
+
+/-!
+# Symbolic simulation support.
+
+This module provides `SymM`, a monad for implementing symbolic simulators (e.g., verification condition generators)
+using Lean. The monad addresses performance issues found in symbolic simulators built on top of user-facing
+tactics (e.g., `apply` and `intros`).
+
+## Overview
+
+The `SymM` monad provides an alternative to tactics built using the `MetaM` monad. Goals are still represented
+by metavariables, but with restrictions that enable more efficient implementations. For example, we cannot
+revert or clear local declarations. This simpler metavariable management reduces the complexity of key
+operations from O(n log n) to O(1). The definitional equality test is more syntactic and cheaper than
+the one available in `MetaM`. `SymM` also provides functions for efficiently discharging goals using `GrindM`.
+
+## Design decisions
+
+### No `revert` or `clear`
+
+In `SymM`, you cannot revert or clear local declarations, so local contexts grow monotonically.
+Each goal is represented by a `Grind.Goal` object which includes a metavariable.
+
+**Why this restriction?** In standard `MetaM`, validating a metavariable assignment `?m := e` requires
+traversing `e`, checking free variables occurring in `e`, and checking that every nested metavariable
+`?n` in `e` has a local context compatible with `?m`'s local context. This uses `LocalContext.isSubPrefixOf`,
+which traverses two `PersistentArray`s with O(log n) lookups per element, expensive when called frequently.
+
+**The key insight:** Since free variable indices increase monotonically and are never reused, a local
+context can be identified by its maximal free variable index. To check whether `lctx₁` is a sub-prefix
+of `lctx₂`, we only need to verify that `lctx₂` contains the maximal free variable declared in `lctx₁`.
+
+**Implementation:** We maintain a mapping `maxFVar` from expressions to free variables, where `maxFVar[e] = x`
+means `x` is the free variable with maximal index occurring in `e`. When assigning `?m := e`, we check
+whether `maxFVar[e]` is in `?m.lctx` — a single hash lookup, O(1).
+
+**Maintaining `maxFVar`:** The mapping is updated during `intro`. The default `intro` in `MetaM` uses
+`instantiate` to replace `Expr.bvar` with `Expr.fvar`, using `looseBVarRange` to skip subexpressions
+without relevant bound variables. The `SymM` version piggybacks on this traversal to update `maxFVar`.
+
+### Skipping type checks on assignment
+
+**The problem:** In `MetaM`, assigning `?m := v` requires checking that `typeof(?m)` is definitionally
+equal to `typeof(v)`. This is necessary when metavariable types contain unassigned universe or expression
+metavariables that must be constrained. For example, applying `Exists.intro.{?u} ?α ...` requires the
+type check to constrain `?u`.
+
+**The optimization:** When both types are ground (no unassigned metavariables), the check is redundant,
+well-typed terms have unique types up to definitional equality, and the types were already checked when
+the terms were constructed. `SymM` tracks whether types are ground and skips the check when possible.
+Checks are also skipped when nothing new can be learned from them assuming terms are all well-typed.
+For domain-specific constructors (e.g., `Exec.seq` in symbolic execution), types are typically ground,
+so the check is almost always skipped.
+
+### A syntactic definitional equality test
+
+**The problem:** The `isDefEq` predicate in `MetaM` is optimized for elaboration and user-facing tactics.
+It supports reduction, type-class resolution, and many other features that can be expensive or have
+unpredictable running time. For symbolic simulation, where `isDefEq` is called frequently, this can
+cause unexpected slowdowns.
+
+**The solution:** In `SymM`, the definitional equality test is optimized for the syntactic case. It avoids
+expensive steps such as lazy-delta reduction. Reduction rules such as `beta` are implemented with term
+size and algorithmic complexity in mind, ensuring predictable performance.
+
+### `GrindM` state
+
+**The problem:** In symbolic simulation, we often want to discharge many goals using proof automation such
+as `grind`. Many of these goals share very similar local contexts. If we invoke `grind` on each goal
+independently, we repeatedly reprocess the same hypotheses.
+
+**The solution:** In `SymM`, we carry the `GrindM` state across goals and use `Grind.Goal` instead of
+bare metavariables. We also provide APIs for incrementally processing local declarations, so hypotheses
+are only processed once.
+
+-/

src/Lean/Meta/Sym/Main.lean

@@ -0,0 +1,34 @@
+/-
+Copyright (c) 2025 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+module
+prelude
+public import Lean.Meta.Sym.SymM
+public import Lean.Meta.Sym.Util
+public import Lean.Meta.Tactic.Grind.Main
+namespace Lean.Meta.Sym
+open Grind (Params)
+
+def SymM.run (x : SymM α) (params : Params) : MetaM α := do
+  x.run' {} |>.run params
+
+def SymM.run' (x : SymM α) (config : Grind.Config := {}) : MetaM α := do
+  let params ← Grind.mkDefaultParams config
+  x.run params
+
+/-- Creates a new goal using the given metavariable -/
+def mkGoal (mvarId : MVarId) : SymM Goal := do
+  let mvarId ← preprocessMVar mvarId
+  Grind.mkGoal mvarId
+
+/-- Internalizes the next `num` hypotheses into `grind`. -/
+def internalizeNumHypotheses (goal : Goal) (num : Nat) : SymM Goal := do
+  Grind.processHypotheses goal (some num)
+
+/-- Internalizes all pending hypotheses into `grind`. -/
+def internalizeAllHypotheses (goal : Goal) : SymM Goal := do
+  Grind.processHypotheses goal none
+
+end Lean.Meta.Sym

src/Lean/Meta/Sym/SymM.lean

@@ -0,0 +1,17 @@
+/-
+Copyright (c) 2025 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+module
+prelude
+public import Lean.Meta.Tactic.Grind.Types
+namespace Lean.Meta.Sym
+export Grind (ExprPtr Goal)
+
+structure State where
+  maxFVar : PHashMap ExprPtr Expr := {}
+
+public abbrev SymM := StateRefT State Grind.GrindM
+
+end Lean.Meta.Sym

src/Lean/Meta/Sym/Util.lean

@@ -0,0 +1,52 @@
+/-
+Copyright (c) 2025 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+module
+prelude
+public import Lean.Meta.Tactic.Grind.Types
+namespace Lean.Meta.Sym
+open Grind
+
+/--
+Instantiates metavariables and applies `shareCommon`.
+-/
+def preprocessExpr (e : Expr) : GrindM Expr := do
+  shareCommon (← instantiateMVars e)
+
+/--
+Helper function that removes gaps, instantiate metavariables, and applies `shareCommon`.
+Gaps are `none` cells at `lctx.decls`. In `SymM`, we assume these cells don't exist.
+-/
+def preprocessLCtx (lctx : LocalContext) : GrindM LocalContext := do
+  let auxDeclToFullName := lctx.auxDeclToFullName
+  let mut fvarIdToDecl := {}
+  let mut decls := {}
+  let mut index := 0
+  for decl in lctx do
+    let decl ← match decl with
+      | .cdecl _ fvarId userName type bi kind =>
+        let type ← preprocessExpr type
+        pure <| LocalDecl.cdecl index fvarId userName type bi kind
+      | .ldecl _ fvarId userName type value nondep kind =>
+        let type ← preprocessExpr type
+        let value ← preprocessExpr value
+        pure <| LocalDecl.ldecl index fvarId userName type value nondep kind
+    decls := decls.push (some decl)
+    fvarIdToDecl := fvarIdToDecl.insert decl.fvarId decl
+  return { fvarIdToDecl, decls, auxDeclToFullName }
+
+/--
+Instantiates assigned metavariables, applies `shareCommon`, and eliminates holes (aka `none` cells)
+in the local context.
+-/
+public def preprocessMVar (mvarId : MVarId) : GrindM MVarId := do
+  let mvarDecl ← mvarId.getDecl
+  let lctx ← preprocessLCtx mvarDecl.lctx
+  let type ← preprocessExpr mvarDecl.type
+  let mvarNew ← mkFreshExprMVarAt lctx mvarDecl.localInstances type .syntheticOpaque mvarDecl.userName
+  mvarId.assign mvarNew
+  return mvarNew.mvarId!
+
+end Lean.Meta.Sym

src/Lean/Meta/Tactic/Grind/Main.lean

@@ -124,8 +124,9 @@ def GrindM.run (x : GrindM α) (params : Params) (evalTactic? : Option EvalTacti
       trueExpr, falseExpr, natZExpr, btrueExpr, bfalseExpr, ordEqExpr, intExpr }
     |>.run' { scState }
 
-private def mkCleanState (mvarId : MVarId) (params : Params) : MetaM Clean.State := mvarId.withContext do
-  unless params.config.clean do return {}
+private def mkCleanState (mvarId : MVarId) : GrindM Clean.State := mvarId.withContext do
+  let config ← getConfig
+  unless config.clean do return {}
   let mut used : PHashSet Name := {}
   for localDecl in (← getLCtx) do
     used := used.insert localDecl.userName
@@ -148,17 +149,20 @@ private def initENodeCore (e : Expr) (interpreted ctor : Bool) : GoalM Unit := d
     updateIndicesFound (.const declName)
   mkENodeCore e interpreted ctor (generation := 0) (funCC := false)
 
-private def mkGoal (mvarId : MVarId) (params : Params) : GrindM Goal := do
-  let mvarId ← if params.config.clean then mvarId.exposeNames else pure mvarId
+/-- Returns a new goal for the given metavariable. -/
+public def mkGoal (mvarId : MVarId) : GrindM Goal := do
+  let config ← getConfig
+  let mvarId ← if config.clean then mvarId.exposeNames else pure mvarId
   let trueExpr ← getTrueExpr
   let falseExpr ← getFalseExpr
   let btrueExpr ← getBoolTrueExpr
   let bfalseExpr ← getBoolFalseExpr
   let natZeroExpr ← getNatZeroExpr
   let ordEqExpr ← getOrderingEqExpr
-  let thmEMatch := params.extensions.map fun ext => ext.ematch
-  let thmInj := params.extensions.map fun ext => ext.inj
-  let clean ← mkCleanState mvarId params
+  let extensions ← getExtensions
+  let thmEMatch := extensions.map fun ext => ext.ematch
+  let thmInj := extensions.map fun ext => ext.inj
+  let clean ← mkCleanState mvarId
   let sstates ← Solvers.mkInitialStates
   GoalM.run' { mvarId, ematch.thmMap := thmEMatch, inj.thms := thmInj, clean, sstates } do
     initENodeCore falseExpr (interpreted := true) (ctor := false)
@@ -167,7 +171,6 @@ private def mkGoal (mvarId : MVarId) (params : Params) : GrindM Goal := do
     initENodeCore bfalseExpr (interpreted := false) (ctor := true)
     initENodeCore natZeroExpr (interpreted := true) (ctor := false)
     initENodeCore ordEqExpr (interpreted := false) (ctor := true)
-    assertExtra params
 
 structure Result where
   failure?   : Option Goal
@@ -249,7 +252,7 @@ Otherwise, all remaining local declarations are processed.
 
 Remark: this function assumes the local context does not contains holes with `none` in `decls`.
 -/
-private def addHypotheses (goal : Goal) (num? : Option Nat := none) : GrindM Goal := GoalM.run' goal do
+def processHypotheses (goal : Goal) (num? : Option Nat := none) : GrindM Goal := GoalM.run' goal do
   discard <| go.run
 where
   go : ExceptT Unit GoalM Unit := do
@@ -273,23 +276,18 @@ where
           internalizeLocalDecl localDecl
     setNextDeclToEnd -- Processed all local decls
 
-private def initCore (mvarId : MVarId) (params : Params) : GrindM Goal := do
-  /-
-  **Note**: We used to use `abstractMVars` and `clearImpDetails` here.
-  These operations are now performed at `withProtectedMCtx`
-  -/
-  -- let mvarId ← mvarId.abstractMVars
-  -- let mvarId ← mvarId.clearImplDetails
-  let mvarId ← if params.config.clean || !params.config.revert then pure mvarId else mvarId.markAccessible
-  let mvarId ← if params.config.revert then mvarId.revertAll else pure mvarId
+private def initCore (mvarId : MVarId) : GrindM Goal := do
+  let config ← getConfig
+  let mvarId ← if config.clean || !config.revert then pure mvarId else mvarId.markAccessible
+  let mvarId ← if config.revert then mvarId.revertAll else pure mvarId
   let mvarId ← mvarId.unfoldReducible
   let mvarId ← mvarId.betaReduce
   appendTagSuffix mvarId `grind
-  let goal ← mkGoal mvarId params
-  if params.config.revert then
+  let goal ← mkGoal mvarId
+  if config.revert then
     return goal
   else
-    addHypotheses goal
+    processHypotheses goal
 
 def mkResult (params : Params) (failure? : Option Goal) : GrindM Result := do
   let issues     := (← get).issues
@@ -305,7 +303,8 @@ def mkResult (params : Params) (failure? : Option Goal) : GrindM Result := do
 
 def GrindM.runAtGoal (mvarId : MVarId) (params : Params) (k : Goal → GrindM α) (evalTactic? : Option EvalTactic := none) : MetaM α := do
   let go : GrindM α := withGTransparency do
-    let goal ← initCore mvarId params
+    let goal ← initCore mvarId
+    let goal ← GoalM.run' goal <| assertExtra params
     k goal
   go.run params (evalTactic? := evalTactic?)
 

src/Lean/Meta/Tactic/Grind/Types.lean

@@ -290,6 +290,10 @@ def withSplitSource [MonadControlT GrindM m] [Monad m] (splitSource : SplitSourc
 def getConfig : GrindM Grind.Config :=
   return (← readThe Context).config
 
+/-- Returns extension states associate with `grind` attributes in use -/
+def getExtensions : GrindM Grind.ExtensionStateArray :=
+  return (← readThe Context).extensions
+
 /--
 Runs `k` with the transparency setting specified by `Config.reducible`.
 Uses reducible transparency if `reducible` is `true`, otherwise default transparency.