From 923c52147938f0769d202a7de323fbf2d78abc6d Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Mon, 23 Feb 2026 14:13:50 +0100 Subject: [PATCH 1/3] Fix Statement.renameLhs to compare identifier names renameLhs was comparing lhs.name against the full Identifier 'fr' instead of 'fr.name', causing renames to never match when the metadata differed. --- Strata/Languages/Core/Statement.lean | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/Strata/Languages/Core/Statement.lean b/Strata/Languages/Core/Statement.lean index 4429a6ab5..02ce3b7b4 100644 --- a/Strata/Languages/Core/Statement.lean +++ b/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 + let decl' := if decl.name == fr.name then { decl with name := to } else decl .funcDecl decl' md | .assert _ _ _ | .assume _ _ _ | .cover _ _ _ | .goto _ _ => s termination_by s.sizeOf From e1c713019e9cc441b192b065ecb28bb68e824ca7 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Mon, 23 Feb 2026 14:47:31 +0000 Subject: [PATCH 2/3] fix: compare identifier names in funcDecl branch of renameLhs MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit In Statement.renameLhs, the funcDecl branch compared decl.name (a CoreIdent) with fr.name (a String). Due to Coe String CoreIdent, fr.name was coerced to CoreIdent.unres fr.name, so the comparison failed whenever decl.name.metadata ≠ Visibility.unres. Fix by comparing decl.name.name (String) with fr.name (String), consistent with all other branches (init, set, call, havoc). --- Strata/Languages/Core/Statement.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/Strata/Languages/Core/Statement.lean b/Strata/Languages/Core/Statement.lean index 02ce3b7b4..c4a80b230 100644 --- a/Strata/Languages/Core/Statement.lean +++ b/Strata/Languages/Core/Statement.lean @@ -401,8 +401,8 @@ def Statement.renameLhs (s : Core.Statement) .loop m g i (Block.renameLhs b fr to) 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.name 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 From 12f4fd2dd07b85dbcdcb69e8d6af46c449261c96 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Mon, 23 Feb 2026 14:47:37 +0000 Subject: [PATCH 3/3] test: add tests for renameLhs funcDecl metadata-mismatch fix Verify that Statement.renameLhs correctly renames a funcDecl when the function name has different metadata (e.g., glob) than the fr identifier (e.g., locl), and that it correctly skips renaming when names differ. --- StrataTest/Languages/Core/RenameLhsTests.lean | 49 +++++++++++++++++++ 1 file changed, 49 insertions(+) create mode 100644 StrataTest/Languages/Core/RenameLhsTests.lean diff --git a/StrataTest/Languages/Core/RenameLhsTests.lean b/StrataTest/Languages/Core/RenameLhsTests.lean new file mode 100644 index 000000000..e1332b65c --- /dev/null +++ b/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