Fix Statement.renameLhs to compare identifier names

Strata/Languages/Core/Statement.lean

@@ -387,22 +387,22 @@ def Statement.renameLhs (s : Core.Statement)
     : Statement :=
   match s with
   | .init lhs ty rhs metadata =>
-    .init (if lhs.name == fr then to else lhs) ty rhs metadata
+    .init (if lhs.name == fr.name then to else lhs) ty rhs metadata
   | .set lhs rhs metadata =>
-    .set (if lhs.name == fr then to else lhs) rhs metadata
+    .set (if lhs.name == fr.name then to else lhs) rhs metadata
   | .call lhs pname args metadata =>
     .call (lhs.map (fun l =>
-      if l.name == fr  then to else l)) pname args metadata
+      if l.name == fr.name then to else l)) pname args metadata
   | .block lbl b metadata =>
     .block lbl (Block.renameLhs b fr to) metadata
   | .ite x thenb elseb m =>
     .ite x (Block.renameLhs thenb fr to) (Block.renameLhs elseb fr to) m
   | .loop m g i b md =>
     .loop m g i (Block.renameLhs b fr to) md
-  | .havoc l md => .havoc (if l.name == fr then to else l) md
+  | .havoc l md => .havoc (if l.name == fr.name then to else l) md
   | .funcDecl decl md =>
-    -- Rename function name if it matches
-    let decl' := if decl.name == fr then { decl with name := to } else decl
+    -- Rename function name if it matches (compare .name strings to avoid metadata mismatch)
+    let decl' := if decl.name.name == fr.name then { decl with name := to } else decl
     .funcDecl decl' md
   | .assert _ _ _ | .assume _ _ _ | .cover _ _ _ | .goto _ _ => s
   termination_by s.sizeOf

StrataTest/Languages/Core/RenameLhsTests.lean

@@ -0,0 +1,49 @@
+/-
+  Copyright Strata Contributors
+
+  SPDX-License-Identifier: Apache-2.0 OR MIT
+-/
+
+import Strata.Languages.Core.Statement
+
+namespace Core
+
+open Lambda Lambda.LTy.Syntax Core.Syntax
+open Imperative (PureFunc)
+
+section RenameLhsTests
+
+/-! ## Tests for Statement.renameLhs on funcDecl -/
+
+private def mkFunc (name : CoreIdent) : PureFunc Expression :=
+  { name := name, inputs := [], output := t[int] }
+
+-- renameLhs on funcDecl should match by name even when metadata differs.
+-- The function has `glob` metadata, but `fr` has `locl` metadata — they share
+-- the same name string "f", so the rename should succeed.
+/-- info: true -/
+#guard_msgs in
+#eval
+  let fr  : CoreIdent := ⟨"f", Visibility.locl⟩
+  let to  : CoreIdent := ⟨"g", Visibility.locl⟩
+  let decl := mkFunc ⟨"f", Visibility.glob⟩
+  let s := Statement.renameLhs (.funcDecl decl) fr to
+  match s with
+  | .funcDecl decl' _ => decl'.name == to
+  | _ => false
+
+-- renameLhs on funcDecl should not rename when names differ.
+/-- info: true -/
+#guard_msgs in
+#eval
+  let fr  : CoreIdent := ⟨"h", Visibility.locl⟩
+  let to  : CoreIdent := ⟨"g", Visibility.locl⟩
+  let decl := mkFunc (CoreIdent.glob "f")
+  let s := Statement.renameLhs (.funcDecl decl) fr to
+  match s with
+  | .funcDecl decl' _ => decl'.name == CoreIdent.glob "f"
+  | _ => false
+
+end RenameLhsTests
+
+end Core