Use original parameter names in symbolic evaluation output (#983)

## Use original parameter names in symbolic evaluation output

### Problem
Generated variable names in verification condition output used opaque
`$__` prefixed names (e.g., `$__top5`, `$__i3`, `$__S4`), making VCs
hard to read. The name disambiguation logic was duplicated between the
SMT encoder and the symbolic evaluator.

### Solution
- Extract shared `@N` suffix disambiguation utilities into `Strata.Name`
(`Strata/Util/Name.lean`)
- Change `genSym` to prefer bare names and add `@N` suffixes only when
the name is already in use, tracked via a `usedNames` set in
`EvalConfig`
- When a name already contains an `@N` suffix (e.g. a Strata parameter
named `g@1`), `genSym` decomposes it and increments the suffix instead
of appending a second `@` — producing `g@2` rather than `g@1@1`
- Remove the now-dead `gen` and `varPrefix` fields from `EvalConfig`
- `findUnique` uses `Std.HashSet String` for O(1) membership checks,
with a fast counter-based search (`findUniqueFast`, 1M attempts) and a
provably-terminating list-erasure fallback (`findUniqueSlow`)
- Formal correctness proofs in `NameProofs.lean`:
  - `findUniqueFast_not_mem`: fast path result is not in `usedNames`
- `findUniqueSlow_not_mem`: slow path result (when `some`) is not in
`usedNames`, proved by strong induction on `remaining.length`
- `findUniqueSlow_ne_none`: slow path never returns `none` when
`remaining` covers `usedSet`, given `DisambiguateInjective` (a named
proposition for suffix injectivity)
- `findUnique_not_mem`: combined correctness for `findUnique`, fully
proved assuming `DisambiguateInjective` (no `sorry`)
- Add `@` to the DDM parser's `strataIsIdRest` so that SMT model
responses with `@N`-suffixed variable names are parsed correctly
- Sanitize SMT-LIB names starting with `@` or `.` (reserved in SMT-LIB)
by prefixing with `$`
- Pipe-quote variable names in SMT `get-value` commands so names
containing `@` are valid

### Testing
All existing tests pass with updated expectations. No simplification
regressions — all obligations that simplified to `true` on main still
simplify to `true`. Added a dedicated test (`AtSignDisambiguationTest`)
verifying that a parameter named `g@1` (containing `@`) does not collide
with the `@N` disambiguation suffix of another parameter `g`.

Author: MikaelMayer

Strata.lean

@@ -17,6 +17,7 @@ import Strata.DL.Lambda.Lambda
 import Strata.DL.Imperative.Imperative
 
 /- Utilities -/
+import Strata.Util.NameProofs
 import Strata.Util.Sarif
 
 /- Strata Languages -/

Strata/DDM/Parser.lean

@@ -123,7 +123,7 @@ private def strataIsIdFirst (c : Char) : Bool :=
   c.isAlpha || c == '_' || c == '$'
 
 private def strataIsIdRest (c : Char) : Bool :=
-  c.isAlphanum || c == '_' || c == '\'' || c == '.' || c == '?' || c == '!' || c == '$'
+  c.isAlphanum || c == '_' || c == '\'' || c == '.' || c == '?' || c == '!' || c == '$' || c == '@'
 
 private def isIdFirstOrBeginEscape (c : Char) : Bool :=
   strataIsIdFirst c || isIdBeginEscape c

Strata/DL/Lambda/LState.lean

@@ -7,6 +7,7 @@ module
 
 public import Strata.DL.Lambda.Factory
 public import Strata.DL.Lambda.Scopes
+public import Strata.Util.Name
 
 /-! ## State for (Partial) Evaluation of Lambda Expressions
 
@@ -23,40 +24,30 @@ variable {T : LExprParams} [Inhabited T.Metadata] [BEq T.Metadata] [DecidableEq
 ---------------------------------------------------------------------
 
 /-
-Configuration for symbolic execution, where we have `gen` for keeping track of
-fresh `fvar`'s numbering. We also have a `fuel` argument for the evaluation
-function, and support for factory functions.
-
-We rely on the parser disallowing Lambda variables to begin with `$__`, which is
-reserved for internal use. Also see `TEnv.genExprVar` used during type inference
-and `LState.genVar` used during evaluation.
+Configuration for symbolic execution, where we have `usedNames` for tracking
+which variable names have been generated. We also have a `fuel` argument for
+the evaluation function, and support for factory functions.
 -/
 structure EvalConfig (T : LExprParams) where
   factory : @Factory T
   fuel : Nat := 200
-  varPrefix : String := "$__"
-  gen : Nat := 0
+  usedNames : Std.HashSet String := {}
 
 instance : ToFormat (EvalConfig T) where
   format c :=
     f!"Eval Depth: {(repr c.fuel)}" ++ Format.line ++
-    f!"Variable Prefix: {c.varPrefix}" ++ Format.line ++
-    f!"Variable gen count: {c.gen}" ++ Format.line ++
     f!"Factory Functions:" ++ Format.line ++
     Std.Format.joinSep c.factory.toArray.toList f!"{Format.line}"
 
 def EvalConfig.init : EvalConfig T :=
   { factory := @Factory.default T,
     fuel := 200,
-    gen := 0 }
-
-def EvalConfig.incGen (c : EvalConfig T) : EvalConfig T :=
-    { c with gen := c.gen + 1 }
+    usedNames := {} }
 
 def EvalConfig.genSym (x : String) (c : EvalConfig T) : String × EvalConfig T :=
-  let new_idx := c.gen
-  let c := c.incGen
-  let new_var := c.varPrefix ++ x ++ toString new_idx
+  let (base, startSuffix) := Strata.Name.breakDisambiguated x
+  let new_var := Strata.Name.findUnique base startSuffix c.usedNames
+  let c := { c with usedNames := c.usedNames.insert new_var }
   (new_var, c)
 
 ---------------------------------------------------------------------
@@ -122,7 +113,8 @@ def LState.knownVars (σ : LState T) : List T.Identifier :=
 
 /--
 Generate a fresh (internal) identifier with the base name
-`x`; i.e., `σ.config.varPrefix ++ x`.
+`x`, reusing the bare name when possible and adding `@N` suffixes
+only when disambiguation is needed.
 -/
 def LState.genVar {IDMeta} [Inhabited IDMeta] [DecidableEq IDMeta] (x : String) (σ : LState ⟨Unit, IDMeta⟩) : String × LState ⟨Unit, IDMeta⟩ :=
   let (new_var, config) := σ.config.genSym x
@@ -151,7 +143,6 @@ def LState.genVars (xs : List String) (σ : (LState ⟨Unit, Unit⟩)) : (List S
 instance : ToFormat (T.Identifier × LState T) where
   format im :=
     f!"New Variable: {im.fst}{Format.line}\
-       Gen in EvalConfig: {im.snd.config.gen}{Format.line}\
        {im.snd}"
 
 ---------------------------------------------------------------------

Strata/DL/SMT/Encoder.lean

@@ -8,6 +8,7 @@ module
 public import Strata.DL.SMT.DDMTransform.Translate
 public import Strata.DL.SMT.Factory
 public import Strata.DL.SMT.Op
+public import Strata.Util.Name
 public import Strata.DL.SMT.Solver
 public import Strata.DL.SMT.Term
 public import Strata.DL.SMT.TermType
@@ -102,6 +103,8 @@ def smtReservedKeywords : List String :=
    "abs", "and", "distinct", "/", "=", ">", ">=", "ite", "=>",
    "div", "is_int", "<", "<=", "-", "mod", "*", "not", "or", "+",
    "to_int", "to_real", "xor",
+   -- Nonlinear arithmetic theory symbols
+   "exp", "sin", "cos", "tan", "sqrt", "pi",
    -- String theory symbols
    "str.at", "str.++", "str.contains", "str.from_code", "str.from_int",
    "str.in_re", "str.indexof", "str.is_digit", "str.<=", "str.len",
@@ -114,44 +117,18 @@ def smtReservedKeywords : List String :=
    -- Array theory symbols
    "select", "store"]
 
-/-- Generate a disambiguated name by appending @suffix -/
-def disambiguateName (baseName : String) (suffix : Nat) : String :=
-  s!"{baseName}@{suffix}"
-
-/-- Parse a list of digit characters as a natural number. -/
-def digitsToNat (cs : List Char) : Nat :=
-  cs.foldl (fun n c => n * 10 + (c.toNat - '0'.toNat)) 0
-
-/-- Break a potentially disambiguated name into its base name and next suffix.
-    If the name has an `@N` suffix, returns `(base, N + 1)`.
-    Otherwise returns `(name, 1)`. -/
-def breakDisambiguatedName (name : String) : String × Nat :=
-  let cs := name.toList
-  let digitSuffix := cs.reverse.takeWhile Char.isDigit |>.reverse
-  let rest := cs.reverse.dropWhile Char.isDigit |>.reverse
-  match rest.reverse, digitSuffix with
-  | '@' :: _, _ :: _ => (String.ofList rest.dropLast, digitsToNat digitSuffix + 1)
-  | _, _ => (name, 1)
-
-/-- Find a unique name by trying candidates with increasing suffixes.
-    The `isUsed` predicate checks if a candidate name is already taken. -/
-def findUniqueName (baseName : String) (startSuffix : Nat) (isUsed : String → Bool) (limit : Nat := 1000) : String :=
-  let rec loop (candidate : String) (suffix : Nat) (remaining : Nat) : String :=
-    if h : remaining == 0 then candidate  -- Fallback after limit attempts
-    else if isUsed candidate then
-      loop (disambiguateName baseName suffix) (suffix + 1) (remaining - 1)
-    else
-      candidate
-  termination_by remaining
-  decreasing_by
-    have : remaining ≠ 0 := by intro h'; simp [h'] at h
-    omega
-  loop (if startSuffix == 1 then baseName else disambiguateName baseName (startSuffix - 1)) startSuffix limit
+/-- Sanitize a name for use in SMT-LIB. Symbols starting with `@` or `.` are
+    reserved in SMT-LIB and rejected by z3 even when pipe-quoted. Prefix such
+    names with `$` to make them valid simple symbols. -/
+def sanitizeSmtName (name : String) : String :=
+  if name.isEmpty then name
+  else
+    let first := name.front
+    if first == '@' || first == '.' then "$" ++ name else name
 
 /-- The `$__` prefix is reserved for internal use and cannot appear in user
-    identifiers (see `Strata.DL.Lambda.LState.EvalConfig.varPrefix`).
-    The `.` after `t`/`f` prevents collision with Lambda-generated names
-    like `$__t0` (variable `t`, index 0). -/
+    identifiers. The `.` after `t`/`f` prevents collision with
+    evaluation-generated names (which use `@N` suffixes). -/
 def termId (n : Nat)                    : String := s!"$__t.{n}"
 def ufId (n : Nat)                      : String := s!"$__f.{n}"
 
@@ -189,10 +166,10 @@ def defineRecord (ty : TermType) (tEncs : List Term) : EncoderM Term := do
 def encodeUF (uf : UF) : EncoderM String := do
   if let (.some enc) := (← get).ufs.get? uf then return enc
   -- Check for name clashes with already-encoded UFs and reserved keywords, disambiguate
-  let baseName := uf.id
-  let existingNames := (← get).ufs.toList.map (·.2) |>.toArray
-  let isUsed := fun candidate => existingNames.contains candidate || smtReservedKeywords.contains candidate
-  let id := findUniqueName baseName 1 isUsed (existingNames.size + smtReservedKeywords.length)
+  let baseName := sanitizeSmtName uf.id
+  let existingNames := (← get).ufs.toList.map (·.2)
+  let usedNames := Std.HashSet.ofList (existingNames ++ smtReservedKeywords)
+  let id := Strata.Name.findUnique baseName 1 usedNames
   comment uf.id
   let argTys := uf.args.map (fun vt => vt.ty)
   Solver.declareFun id argTys uf.out

Strata/DL/SMT/Solver.lean

@@ -160,7 +160,7 @@ def comment (comment : String) : SolverM Unit :=
   emitln s!"; {inline}"
 
 def getValue (ids : List String) : SolverM Unit :=
-  let ids := Std.Format.joinSep ids " "
+  let ids := Std.Format.joinSep (ids.map quoteIdent) " "
   emitln s!"(get-value ({ids}))"
 
 def declareSort (id : String) (arity : Nat) : SolverM Unit :=

Strata/Languages/Core/Env.lean

@@ -7,6 +7,7 @@ module
 
 public import Strata.Languages.Core.Program
 public import Strata.DL.Imperative.EvalContext
+public import Strata.Util.Name
 
 public section
 
@@ -244,23 +245,21 @@ def Env.addToContext
     : Env :=
   List.foldl (fun E (x, v) => E.insertInContext x v) E xs
 
--- TODO: prove uniqueness, add different prefix
+-- TODO: prove uniqueness
 def Env.genSym (x : String) (c : Lambda.EvalConfig CoreLParams) : CoreIdent × Lambda.EvalConfig CoreLParams :=
-  let new_idx := c.gen
-  let c := c.incGen
-  let new_var := c.varPrefix ++ x ++ toString new_idx
+  let (new_var, c) := c.genSym x
   (⟨new_var, ()⟩, c)
 
 def Env.genVar' (x : String) (σ : (Lambda.LState CoreLParams)) :
     (CoreIdent × (Lambda.LState CoreLParams)) :=
-  let (new_var, config) := Env.genSym x σ.config
+  -- If `x` is already bound in the state, mark it used so that findUnique
+  -- skips the bare name and avoids self-referential substitutions
+  -- (e.g. havoc x generating fvar "x" when x is in scope).
+  let config := if σ.state.find? (⟨x, ()⟩ : CoreIdent) |>.isSome
+    then { σ.config with usedNames := σ.config.usedNames.insert x }
+    else σ.config
+  let (new_var, config) := Env.genSym x config
   let σ : Lambda.LState CoreLParams := { σ with config := config }
-  -- let known_vars := Lambda.LState.knownVars σ
-  -- if new_var ∈ known_vars then
-  --   panic s!"[LState.genVar] Generated variable {Std.format new_var} is not fresh!\n\
-  --            Known variables: {Std.format σ.knownVars}"
-  -- else
-  --   (new_var, σ)
   (new_var, σ)
 
 def Env.genVar (x : Expression.Ident) (E : Env) : Expression.Ident × Env :=

Strata/Languages/Core/ProcedureEval.lean

@@ -39,9 +39,9 @@ The differences across paths are:
   clears `deferred` on the false branch, so pre-split obligations appear only
   in the first (true) path; post-split obligations appear in each path under
   distinct path conditions.
-- `exprEnv.config.gen`: may diverge when branches execute different numbers of
-  `genFVar` calls (e.g. procedure calls only in one branch). We take the max to
-  prevent fresh-variable name collisions in subsequent evaluation.
+- `exprEnv.config.usedNames`: may diverge when branches generate different
+  variables. We union the sets to prevent fresh-variable name collisions in
+  subsequent evaluation.
 
 The `fallback` Env is returned when `results` is empty (which should not occur
 in practice, since `Statement.eval` always produces at least one result).
@@ -52,18 +52,32 @@ private def mergeResults (fallback : Env) (results : List Env) : Env :=
   | [E] => E
   | E :: rest =>
     let allDeferred := rest.foldl (fun acc e => acc ++ e.deferred) E.deferred
-    let maxGen      := rest.foldl (fun acc e => max acc e.exprEnv.config.gen) E.exprEnv.config.gen
+    let mergedNames := rest.foldl (fun acc e =>
+      acc.union e.exprEnv.config.usedNames) E.exprEnv.config.usedNames
     { E with
       deferred := allDeferred,
-      exprEnv  := { E.exprEnv with config := { E.exprEnv.config with gen := maxGen } } }
+      exprEnv  := { E.exprEnv with config := { E.exprEnv.config with usedNames := mergedNames } } }
+
+/--
+Evaluate a single procedure: generate fresh variables for parameters,
+execute the body, check postconditions, and collect proof obligations.
+-/
 
 def eval (E : Env) (p : Procedure) : Env × Statistics :=
   -- Create a new scope with the formals and return variables. We will pop this
   -- scope at the end of this procedure.
+  -- Parameters go through genFVars for globally unique names.
+  -- Mark original parameter names as used so that fvar names always differ
+  -- from the scope keys. Without this, a bare fvar "x" would be captured
+  -- by the scope entry for "x" after reassignment, causing old(x) to
+  -- resolve to the post-assignment value instead of the initial value.
   let vars := p.header.inputs.keys ++ p.header.outputs.keys
+  let E := vars.foldl (fun E (v : CoreIdent) =>
+    { E with exprEnv.config.usedNames := E.exprEnv.config.usedNames.insert v.name }) E
   let var_tys := p.header.inputs.values ++ p.header.outputs.values
   let var_tys := var_tys.map (fun ty => some ty)
-  let (vals, E) := E.genFVars (vars.zip var_tys)
+  let vars_typed := vars.zip var_tys
+  let (vals, E) := E.genFVars vars_typed
   let pVarMap := List.zip vars (var_tys.zip vals)
   let E := E.pushScope pVarMap
   let E := { E with pathConditions := E.pathConditions.push [] }

Strata/Languages/Core/SMTEncoder.lean

@@ -277,20 +277,17 @@ partial def toSMTTerm (E : Env) (bvs : BoundVars) (e : LExpr CoreLParams.mono) (
     let fvarNames := (e.collectFvarNames.map (·.name)).toArray
     -- Generate base name using global counter to ensure uniqueness across terms.
     -- The `$__` prefix is reserved for internal use and cannot appear in user
-    -- identifiers (see `Strata.DL.Lambda.LState.EvalConfig.varPrefix`).
+    -- identifiers.
     let (baseName, startSuffix) :=
       if ctx.uniqueBoundNames || name.isEmpty then
         (s!"$__bv{ctx.bvCounter}", 1)
       else
-        Encoder.breakDisambiguatedName name
+        let (b, s) := Strata.Name.breakDisambiguated name
+        (Encoder.sanitizeSmtName b, s)
     let ctx := { ctx with bvCounter := ctx.bvCounter + 1 }
     -- Check for clashes with existing bvars, fvars in ctx, and fvars in body
-    let isUsed := fun candidate =>
-      bvs.any (fun (n, _) => n == candidate) ||
-      ctx.ufs.any (fun uf => uf.id == candidate) ||
-      fvarNames.contains candidate
-    let limit := bvs.length + ctx.ufs.size + fvarNames.size
-    let x := Encoder.findUniqueName baseName startSuffix isUsed limit
+    let usedNames := Std.HashSet.ofList (bvs.map (·.1) ++ ctx.ufs.toList.map (·.id) ++ fvarNames.toList)
+    let x := Strata.Name.findUnique baseName startSuffix usedNames
     let (ety, ctx) ← LMonoTy.toSMTType E ty ctx useArrayTheory
     let (trt, ctx) ← appToSMTTerm E ((x, ety) :: bvs) tr [] ctx useArrayTheory
     let (et, ctx) ← toSMTTerm E ((x, ety) :: bvs) e ctx useArrayTheory

Strata/Util/Name.lean

@@ -0,0 +1,85 @@
+/-
+  Copyright Strata Contributors
+
+  SPDX-License-Identifier: Apache-2.0 OR MIT
+-/
+module
+public import Std.Data.HashSet.Basic
+
+/-! # Name disambiguation utilities
+
+Shared helpers for generating unique names. Bare names are preferred;
+`@N` suffixes are added only when disambiguation is needed.
+Used by the SMT encoder (for UF/bound-variable disambiguation) and
+the symbolic evaluator (for readable generated variable names).
+-/
+
+public section
+
+namespace Strata.Name
+
+/-- Generate a disambiguated name by appending `@suffix`. -/
+def disambiguate (baseName : String) (suffix : Nat) : String :=
+  s!"{baseName}@{suffix}"
+
+/-- Parse a list of digit characters as a natural number. -/
+def digitsToNat (cs : List Char) : Nat :=
+  cs.foldl (fun n c => n * 10 + (c.toNat - '0'.toNat)) 0
+
+/-- Break a potentially disambiguated name into its base name and next suffix.
+    If the name has an `@N` suffix, returns `(base, N + 1)`.
+    Otherwise returns `(name, 1)`. -/
+def breakDisambiguated (name : String) : String × Nat :=
+  let cs := name.toList
+  let digitSuffix := cs.reverse.takeWhile Char.isDigit |>.reverse
+  let rest := cs.reverse.dropWhile Char.isDigit |>.reverse
+  match rest.reverse, digitSuffix with
+  | '@' :: _, _ :: _ => (String.ofList rest.dropLast, digitsToNat digitSuffix + 1)
+  | _, _ => (name, 1)
+
+/-- Fast candidate search with a fuel counter. Returns `none` if fuel is exhausted. -/
+def findUniqueFast (baseName : String) (candidate : String) (suffix : Nat)
+    (usedNames : Std.HashSet String) (fuel : Nat) : Option String :=
+  if !usedNames.contains candidate then some candidate
+  else match fuel with
+    | 0 => none
+    | fuel + 1 =>
+      findUniqueFast baseName (disambiguate baseName suffix) (suffix + 1) usedNames fuel
+
+/-- Provably-terminating fallback via list erasure.
+    Uses `usedSet` (a `HashSet`) for O(1) membership checks and `remaining`
+    (a list that shrinks via erasure) for termination.
+    Returns `none` only if `remaining` is exhausted before finding a
+    candidate outside `usedSet` — unreachable when `remaining` covers
+    `usedSet` and candidates are distinct. -/
+def findUniqueSlow (baseName : String) (candidate : String) (suffix : Nat)
+    (usedSet : Std.HashSet String) (remaining : List String) : Option String :=
+  if !usedSet.contains candidate then some candidate
+  else if h : remaining.contains candidate then
+    have : (remaining.erase candidate).length < remaining.length := by grind
+    findUniqueSlow baseName (disambiguate baseName suffix) (suffix + 1)
+                   usedSet (remaining.erase candidate)
+  else none
+termination_by remaining.length
+
+/-- Find a unique name by trying candidates with increasing `@N` suffixes.
+    Uses a fast counter-based loop, falling back to a provably-terminating
+    list-erasure search if the counter is exhausted (so we never panic). -/
+def findUnique (baseName : String) (startSuffix : Nat)
+    (usedNames : Std.HashSet String) : String :=
+  let firstCandidate :=
+    if startSuffix == 1 then baseName
+    else disambiguate baseName (startSuffix - 1)
+  match findUniqueFast baseName firstCandidate startSuffix usedNames 1000000 with
+  | some name => name
+  | none =>
+    let slowSuffix := startSuffix + 1000000
+    let usedList := usedNames.toList
+    match findUniqueSlow baseName (disambiguate baseName slowSuffix)
+                         (slowSuffix + 1) usedNames usedList with
+    | some name => name
+    | none => disambiguate baseName (slowSuffix + usedList.length + 1)
+
+end Strata.Name
+
+end -- public section