From 999fcd2d95b50b1844cd783e5823a418c38fa597 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leomoura@amazon.com>
Date: Fri, 30 May 2025 13:07:26 -0400
Subject: [PATCH] fix: hash function for congruence closure in `grind` (#8549)

This PR fixes the hash function used to implement congruence closure in
`grind`. The hash of an `Expr` must not depend on whether the expression
has been internalized or not.
---
 .../Meta/Tactic/Grind/AlphaShareCommon.lean   |  2 +-
 src/Lean/Meta/Tactic/Grind/ENodeKey.lean      |  5 +++-
 src/Lean/Meta/Tactic/Grind/Types.lean         | 10 +++----
 tests/lean/run/grind_congr_hash_issue.lean    | 26 +++++++++++++++++++
 .../grind_panic_invariant.lean}               | 13 +++++-----
 5 files changed, 42 insertions(+), 14 deletions(-)
 create mode 100644 tests/lean/run/grind_congr_hash_issue.lean
 rename tests/lean/{grind/panic.lean => run/grind_panic_invariant.lean} (69%)

diff --git a/src/Lean/Meta/Tactic/Grind/AlphaShareCommon.lean b/src/Lean/Meta/Tactic/Grind/AlphaShareCommon.lean
index 2402ff7693..6a3739dcf2 100644
--- a/src/Lean/Meta/Tactic/Grind/AlphaShareCommon.lean
+++ b/src/Lean/Meta/Tactic/Grind/AlphaShareCommon.lean
@@ -13,7 +13,7 @@ private def hashChild (e : Expr) : UInt64 :=
   | .bvar .. | .mvar .. | .const .. | .fvar .. | .sort .. | .lit .. =>
     hash e
   | .app .. | .letE .. | .forallE .. | .lam .. | .mdata .. | .proj .. =>
-    (unsafe ptrAddrUnsafe e).toUInt64
+    hashPtrExpr e
 
 private def alphaHash (e : Expr) : UInt64 :=
   match e with
diff --git a/src/Lean/Meta/Tactic/Grind/ENodeKey.lean b/src/Lean/Meta/Tactic/Grind/ENodeKey.lean
index 5a8c34ba9d..7d66714ccb 100644
--- a/src/Lean/Meta/Tactic/Grind/ENodeKey.lean
+++ b/src/Lean/Meta/Tactic/Grind/ENodeKey.lean
@@ -21,8 +21,11 @@ have been hash-consed, i.e., we have applied `shareCommon`.
 structure ENodeKey where
   expr : Expr
 
+abbrev hashPtrExpr (e : Expr) : UInt64 :=
+  unsafe (ptrAddrUnsafe e >>> 3).toUInt64
+
 instance : Hashable ENodeKey where
-  hash k := unsafe (ptrAddrUnsafe k.expr).toUInt64
+  hash k := hashPtrExpr k.expr
 
 instance : BEq ENodeKey where
   beq k₁ k₂ := isSameExpr k₁.expr k₂.expr
diff --git a/src/Lean/Meta/Tactic/Grind/Types.lean b/src/Lean/Meta/Tactic/Grind/Types.lean
index 374700b453..389491488a 100644
--- a/src/Lean/Meta/Tactic/Grind/Types.lean
+++ b/src/Lean/Meta/Tactic/Grind/Types.lean
@@ -86,7 +86,7 @@ instance : BEq CongrTheoremCacheKey where
 
 -- We manually define `Hashable` because we want to use pointer equality.
 instance : Hashable CongrTheoremCacheKey where
-  hash a := mixHash (unsafe ptrAddrUnsafe a.f).toUInt64 (hash a.numArgs)
+  hash a := mixHash (hashPtrExpr a.f) (hash a.numArgs)
 
 structure EMatchTheoremTrace where
   origin : Origin
@@ -372,9 +372,9 @@ structure CongrKey (enodes : ENodeMap) where
 
 private def hashRoot (enodes : ENodeMap) (e : Expr) : UInt64 :=
   if let some node := enodes.find? { expr := e } then
-    unsafe (ptrAddrUnsafe node.root).toUInt64
+    hashPtrExpr node.root
   else
-    13
+    hashPtrExpr e
 
 private def hasSameRoot (enodes : ENodeMap) (a b : Expr) : Bool := Id.run do
   if isSameExpr a b then
@@ -461,9 +461,9 @@ structure PreInstance where
 
 instance : Hashable PreInstance where
   hash i := Id.run do
-    let mut r := unsafe (ptrAddrUnsafe i.proof >>> 3).toUInt64
+    let mut r := hashPtrExpr i.proof
     for v in i.assignment do
-      r := mixHash r (unsafe (ptrAddrUnsafe v >>> 3).toUInt64)
+      r := mixHash r (hashPtrExpr v)
     return r
 
 instance : BEq PreInstance where
diff --git a/tests/lean/run/grind_congr_hash_issue.lean b/tests/lean/run/grind_congr_hash_issue.lean
new file mode 100644
index 0000000000..75f18e6752
--- /dev/null
+++ b/tests/lean/run/grind_congr_hash_issue.lean
@@ -0,0 +1,26 @@
+set_option grind.warning false
+set_option grind.debug true
+
+opaque f : Nat → Nat
+opaque g : (Nat → Nat) → Prop
+
+example
+    : f a = x →
+      -- At this point `f` has not been internalized
+      g f →
+      -- Since `f` has now occurred as the argument of `f`, it is internalized
+      f b = y →
+      -- The congruence hash for `f a` must not depend on whether `f` has been internalized or not
+      b = a →
+      x = y := by
+  grind
+
+-- Same example with `a = b` to ensure the previous issue does not depend on how we break
+-- ties when merging equivalence classes of the same size
+example
+    : f a = x →
+      g f →
+      f b = y →
+      a = b →
+      x = y := by
+  grind
diff --git a/tests/lean/grind/panic.lean b/tests/lean/run/grind_panic_invariant.lean
similarity index 69%
rename from tests/lean/grind/panic.lean
rename to tests/lean/run/grind_panic_invariant.lean
index f5e805ca66..b995387501 100644
--- a/tests/lean/grind/panic.lean
+++ b/tests/lean/run/grind_panic_invariant.lean
@@ -16,11 +16,6 @@ inductive cexec : com → Prop where
 @[grind] inductive red : com × Nat → com × Nat → Prop where
   | red_assign: ∀ s, red (.ASSIGN, s) (.SKIP, 0)
 
-/--
-The following theorem causes assertion violation in grind.
-We obtain the following:
-_private.Lean.Meta.Tactic.Grind.Inv.0.Lean.Meta.Grind.checkEqc Lean.Meta.Tactic.Grind.Inv:29:10: assertion violation: isSameExpr e ( __do_lift._@.Lean.Meta.Tactic.Grind.Inv._hyg.31.0 )
--/
 theorem issue3 (s s' : Nat) (c : com) :
   star red (c, s) (.SKIP, s') → cexec c := by
     intro h
@@ -31,5 +26,9 @@ theorem issue3 (s s' : Nat) (c : com) :
     case star_refl =>
       sorry
     case star_step r _ a_ih =>
-      -- this is where the assertion violation happens
-      grind
+      /-
+      The following `grind` used to trigger an assertion violation:
+      _private.Lean.Meta.Tactic.Grind.Inv.0.Lean.Meta.Grind.checkEqc Lean.Meta.Tactic.Grind.Inv:29:10: assertion violation: isSameExpr e ( __do_lift._@.Lean.Meta.Tactic.Grind.Inv._hyg.31.0 )
+      -/
+      fail_if_success grind
+      sorry