fix: widen transparency field to 3 bits in Meta.Config cache key (#13768)

This PR fixes a long-standing bug in `Meta.Config.toKey` and
`Context.setTransparency` where `TransparencyMode` was packed into only
2 bits of the cache key, even though it has 5 constructors (`.all`,
`.default`, `.reducible`, `.instances`, `.none`). The `.none` case
(value `4`, i.e. `0b100`) overlapped with the `foApprox` bit, so
configurations differing only in transparency vs. `foApprox` could
collide in the `isDefEq`/`WHNF` cache, and `Context.setTransparency`
corrupted the neighbouring bit when switching to/from `.none`.

The fix widens the transparency field to 3 bits and shifts every
subsequent flag up by one. Split out from
https://github.com/leanprover/lean4/pull/13637 where the same fix was
needed anyway to accommodate a 6th transparency constructor.

🤖 Prepared with Claude Code

---------

Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

src/Lean/Meta/Basic.lean

@@ -197,23 +197,23 @@ structure Config where
 /-- Convert `isDefEq` and `WHNF` relevant parts into a key for caching results -/
 private def Config.toKey (c : Config) : UInt64 :=
   c.transparency.toUInt64 |||
-  (c.foApprox.toUInt64 <<< 2) |||
-  (c.ctxApprox.toUInt64 <<< 3) |||
-  (c.quasiPatternApprox.toUInt64 <<< 4) |||
-  (c.constApprox.toUInt64 <<< 5) |||
-  (c.isDefEqStuckEx.toUInt64 <<< 6) |||
-  (c.unificationHints.toUInt64 <<< 7) |||
-  (c.proofIrrelevance.toUInt64 <<< 8) |||
-  (c.assignSyntheticOpaque.toUInt64 <<< 9) |||
-  (c.offsetCnstrs.toUInt64 <<< 10) |||
-  (c.iota.toUInt64 <<< 11) |||
-  (c.beta.toUInt64 <<< 12) |||
-  (c.zeta.toUInt64 <<< 13) |||
-  (c.zetaDelta.toUInt64 <<< 14) |||
-  (c.univApprox.toUInt64 <<< 15) |||
-  (c.etaStruct.toUInt64 <<< 16) |||
-  (c.proj.toUInt64 <<< 18) |||
-  (c.zetaHave.toUInt64 <<< 20)
+  (c.foApprox.toUInt64 <<< 3) |||
+  (c.ctxApprox.toUInt64 <<< 4) |||
+  (c.quasiPatternApprox.toUInt64 <<< 5) |||
+  (c.constApprox.toUInt64 <<< 6) |||
+  (c.isDefEqStuckEx.toUInt64 <<< 7) |||
+  (c.unificationHints.toUInt64 <<< 8) |||
+  (c.proofIrrelevance.toUInt64 <<< 9) |||
+  (c.assignSyntheticOpaque.toUInt64 <<< 10) |||
+  (c.offsetCnstrs.toUInt64 <<< 11) |||
+  (c.iota.toUInt64 <<< 12) |||
+  (c.beta.toUInt64 <<< 13) |||
+  (c.zeta.toUInt64 <<< 14) |||
+  (c.zetaDelta.toUInt64 <<< 15) |||
+  (c.univApprox.toUInt64 <<< 16) |||
+  (c.etaStruct.toUInt64 <<< 17) |||
+  (c.proj.toUInt64 <<< 19) |||
+  (c.zetaHave.toUInt64 <<< 21)
 
 /-- Configuration with key produced by `Config.toKey`. -/
 structure ConfigWithKey where
@@ -1263,8 +1263,8 @@ def withTrackingZetaDeltaSet (s : FVarIdSet) : n α → n α :=
 
 @[inline] private def Context.setTransparency (ctx : Context) (transparency : TransparencyMode) : Context :=
   let config := { ctx.config with transparency }
-  -- Recall that `transparency` is stored in the first 2 bits
-  let key : UInt64 := ((ctx.configKey >>> (2 : UInt64)) <<< 2) ||| transparency.toUInt64
+  -- Recall that `transparency` is stored in the first 3 bits (it has 5 values).
+  let key : UInt64 := ((ctx.configKey >>> (3 : UInt64)) <<< 3) ||| transparency.toUInt64
   { ctx with keyedConfig := { config, key } }
 
 @[inline] def withTransparency (mode : TransparencyMode) : n α → n α :=

tests/elab/13768.lean

@@ -0,0 +1,18 @@
+module
+
+import Lean
+
+/-!
+Regression test for https://github.com/leanprover/lean4/pull/13768.
+
+`TransparencyMode` has five constructors (`.all`, `.default`, `.reducible`, `.instances`,
+`.none`), so it needs 3 bits in the `Meta.Config` cache key. Previously only 2 bits were
+allocated, so the high bit of `.none` (value `4`) overlapped with the `foApprox` bit, and
+configurations differing only in `foApprox` produced the same key when `transparency = .none`.
+-/
+
+open Lean Meta
+
+#guard
+  ({ transparency := .none, foApprox := false } : Meta.Config).toConfigWithKey.key !=
+  ({ transparency := .none, foApprox := true  } : Meta.Config).toConfigWithKey.key