perf: pick cache size coprime to pointer alignment

src/Lean/Util/FindExpr.lean

@@ -10,7 +10,7 @@ namespace Expr
 
 namespace FindImpl
 
-abbrev cacheSize : USize := 8192
+abbrev cacheSize : USize := 8192 - 1
 
 structure State where
   keys : Array Expr -- Remark: our "unsafe" implementation relies on the fact that `()` is not a valid Expr

src/Lean/Util/FoldConsts.lean

@@ -10,7 +10,7 @@ namespace Lean
 namespace Expr
 namespace FoldConstsImpl
 
-abbrev cacheSize : USize := 8192
+abbrev cacheSize : USize := 8192 - 1
 
 structure State where
   visitedTerms  : Array Expr  -- Remark: cache based on pointer address. Our "unsafe" implementation relies on the fact that `()` is not a valid Expr

src/Lean/Util/ReplaceExpr.lean

@@ -10,7 +10,7 @@ namespace Expr
 
 namespace ReplaceImpl
 
-@[inline] def cacheSize : USize := 8192
+@[inline] def cacheSize : USize := 8192 - 1
 
 structure Cache where
   -- First cacheSize elements are the keys.
@@ -23,7 +23,7 @@ unsafe def Cache.new : Cache :=
 
 @[inline]
 unsafe def Cache.keyIdx (key : Expr) : USize :=
-  (ptrAddrUnsafe key >>> 4) % cacheSize
+  ptrAddrUnsafe key % cacheSize
 
 @[inline]
 unsafe def Cache.resultIdx (key : Expr) : USize :=

src/Lean/Util/ReplaceLevel.lean

@@ -23,7 +23,7 @@ namespace Expr
 
 namespace ReplaceLevelImpl
 
-abbrev cacheSize : USize := 8192
+abbrev cacheSize : USize := 8192 - 1
 
 structure State where
   keys    : Array Expr -- Remark: our "unsafe" implementation relies on the fact that `()` is not a valid Expr