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.

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

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

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

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

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