fix: exempt bootstrap-path extensions from the resolution access tripwire

Compiling `Init.Prelude` for stage 2 panicked on the extension access tripwire: `Environment.find?` consults the reserved-name predicates on lookup misses, also inside a resolution search, and the predicates (and their realization-action preludes) read their registering module's extensions. These paths are only exercised during bootstrapping, so the stage 1 test suite never reached them; CI builds stage 2 for this branch because `stage0/src/stdlib_flags.h` differs.

Register the involved extensions as `.exempt`, each of which is monotone and keyed by declarations that must exist before any query can observe them: `reservedNamePredicatesExt` (fixed at initialization), `defHeightOverrideExt`, `methodSpecsAttr` (threading `tcResolutionAccess` through `ParametricAttributeImpl`), `eqnsExt`/`eqnOptionsExt`, `matchEqnsExt`, `sparseCasesOnInfoExt`/`sparseCasesOnCacheExt`, and the partial-fixpoint `eqnInfoExt`. Realization bodies themselves run on the realization context's environment, which is never armed, so no further classification is needed there. Verified by a full local stage 2 build (previously failing at `Init.Prelude`, now clean).

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>

Author: Kha

src/Lean/Elab/PreDefinition/PartialFixpoint/Eqns.lean

@@ -26,7 +26,9 @@ public structure EqnInfo where
   deriving Inhabited
 
 public builtin_initialize eqnInfoExt : MapDeclarationExtension EqnInfo ←
-  mkMapDeclarationExtension (exportEntriesFn := fun env s =>
+  -- consulted by the reserved-name predicates for fixpoint induction names, so also on
+  -- resolution search paths; populated only when the declaration is created (monotone)
+  mkMapDeclarationExtension (tcResolutionAccess := .exempt) (exportEntriesFn := fun env s =>
     let all := s.toArray
     -- Do not export for non-exposed defs at exported/server levels
     let exported := s.filter (fun n _ => env.hasExposedBody n) |>.toArray

src/Lean/Environment.lean

@@ -3055,7 +3055,9 @@ This is consulted for all definitions regardless of their reducibility hints. Cu
 structural recursion to ensure that parent definitions get the correct height even though the
 `_f` helper definitions are marked as `.abbrev` (which `getMaxHeight` would otherwise ignore). -/
 builtin_initialize defHeightOverrideExt : EnvExtension (NameMap UInt32) ←
-  registerEnvExtension (pure {}) (asyncMode := .local)
+  -- read when auxiliary declarations are created during realization, which can happen inside a
+  -- resolution search; overrides are set only for declarations being created (monotone)
+  registerEnvExtension (pure {}) (asyncMode := .local) (tcResolutionAccess := .exempt)
 
 /-- Register a height override for a definition so that `getMaxHeight` uses it. -/
 def setDefHeightOverride (env : Environment) (declName : Name) (height : UInt32) : Environment :=

src/Lean/Meta/Constructions/SparseCasesOn.lean

@@ -24,7 +24,9 @@ structure SparseCasesOnKey where
 deriving BEq, Hashable
 
 builtin_initialize sparseCasesOnCacheExt : EnvExtension (PHashMap SparseCasesOnKey Name) ←
-  registerEnvExtension (pure {}) (asyncMode := .local)  -- mere cache, keep it local
+  -- mere cache, keep it local; may be consulted on resolution search paths via the reserved-name
+  -- machinery (monotone realization cache)
+  registerEnvExtension (pure {}) (asyncMode := .local) (tcResolutionAccess := .exempt)
 
 /-- Information necessary to recognize and split on sparse casesOn (in particular in MatchEqs) -/
 public structure SparseCasesOnInfo where
@@ -35,7 +37,9 @@ public structure SparseCasesOnInfo where
 deriving Inhabited
 
 builtin_initialize sparseCasesOnInfoExt : MapDeclarationExtension SparseCasesOnInfo ←
-  mkMapDeclarationExtension (exportEntriesFn := fun env s =>
+  -- consulted by the reserved-name predicate for `else_eq` names, so also on resolution search
+  -- paths; populated only when the declaration is created (monotone)
+  mkMapDeclarationExtension (tcResolutionAccess := .exempt) (exportEntriesFn := fun env s =>
     let all := s.toArray
     -- Do not export for non-exposed defs at exported/server levels
     let exported := s.filter (fun n _ => env.hasExposedBody n) |>.toArray

src/Lean/Meta/Eqns.lean

@@ -47,7 +47,9 @@ def eqnAffectingOptions : Array (Lean.Option Bool) :=
 keyed by declaration name. Only populated when at least one option has a non-default value.
 Stores an association list of (option name, value) pairs for options that differ from defaults. -/
 builtin_initialize eqnOptionsExt : MapDeclarationExtension (Array (Name × DataValue)) ←
-  mkMapDeclarationExtension (asyncMode := .local)
+  -- consulted during equation realization, which can happen inside a resolution search;
+  -- populated only when the declaration is created (monotone)
+  mkMapDeclarationExtension (asyncMode := .local) (tcResolutionAccess := .exempt)
 
 def eqnThmSuffixBase := "eq"
 def eqnThmSuffixBasePrefix := eqnThmSuffixBase ++ "_"
@@ -157,7 +159,9 @@ structure EqnsExtState where
 
 /-- A mapping from equational theorem to the declaration it was derived from.  -/
 builtin_initialize eqnsExt : EnvExtension EqnsExtState ←
-  registerEnvExtension (pure {}) (asyncMode := .local)
+  -- consulted during equation realization, which can happen inside a resolution search;
+  -- a mere name mapping for realized equation theorems (monotone)
+  registerEnvExtension (pure {}) (asyncMode := .local) (tcResolutionAccess := .exempt)
 
 /--
 Runs `act` with the equation-affecting options restored to the values stored for `declName`

src/Lean/Meta/Match/MatchEqsExt.lean

@@ -30,10 +30,12 @@ structure MatchEqnsExtState where
 
 /- We generate the equations and splitter on demand, and do not save them on .olean files. -/
 builtin_initialize matchEqnsExt : EnvExtension MatchEqnsExtState ←
+  -- consulted during match-equation realization, which can happen inside a resolution search;
+  -- a mere name mapping for realized equation theorems (monotone)
   -- Using `local` allows us to use the extension in `realizeConst` without specifying `replay?`.
   -- The resulting state can still be accessed on the generated declarations using `.asyncEnv`;
   -- see below
-  registerEnvExtension (pure {}) (asyncMode := .local)
+  registerEnvExtension (pure {}) (asyncMode := .local) (tcResolutionAccess := .exempt)
 
 def registerMatchEqns (matchDeclName : Name) (matchEqns : MatchEqns) : CoreM Unit := do
   modifyEnv fun env => matchEqnsExt.modifyState env fun { map, eqns } => {

src/Lean/Meta/MethodSpecs.lean

@@ -112,12 +112,41 @@ overloaded `Cls.op` operation, and similarly `instClsT.op_spec_<n>` based on the
 `opImpl.eq_<n>`.
 -/
 @[builtin_doc]
-builtin_initialize methodSpecsAttr : ParametricAttribute MethodSpecsAttrData ←
-  registerParametricAttribute {
+builtin_initialize methodSpecsAttr : ParametricAttribute MethodSpecsAttrData ← do
+  -- `registerParametricAttribute` inlined so that the extension can be registered with
+  -- `tcResolutionAccess := .exempt`: it is consulted (via the reserved-name machinery) when
+  -- specification theorems are realized, which can happen inside a resolution search, and the
+  -- attribute is applied when the method implementation is declared (monotone).
+  let impl : ParametricAttributeImpl MethodSpecsAttrData := {
     name := `method_specs
     descr := "generate method specification theorems"
     getParam
   }
+  let ext : PersistentEnvExtension (Name × MethodSpecsAttrData) (Name × MethodSpecsAttrData) (List Name × NameMap MethodSpecsAttrData) ← registerPersistentEnvExtension {
+    name            := impl.ref
+    tcResolutionAccess := .exempt
+    mkInitial       := pure ([], {})
+    addImportedFn   := fun _ => pure ([], {})
+    addEntryFn      := fun (decls, m) p => (p.1 :: decls, m.insert p.1 p.2)
+    exportEntriesFnEx := fun env (decls, m) => Id.run do
+      let all := (m.foldl (fun a n p => a.push (n, p)) #[]).qsort (fun a b => Name.quickLt a.1 b.1)
+      let exported := all.filter fun (n, a) => impl.filterExport env n a
+      { exported, server := exported, «private» := all }
+    statsFn         := fun (_, m) => "parametric attribute" ++ Format.line ++ "number of local entries: " ++ format m.size
+  }
+  let attrImpl : AttributeImpl := {
+    impl.toAttributeImplCore with
+    add := fun decl stx kind => do
+      unless kind == AttributeKind.global do throwAttrMustBeGlobal impl.name kind
+      let env ← getEnv
+      unless (env.getModuleIdxFor? decl).isNone do
+        throwAttrDeclInImportedModule impl.name decl
+      let val ← impl.getParam decl stx
+      modifyEnv fun env => ext.addEntry (asyncDecl := decl) env (decl, val)
+      try impl.afterSet decl val catch _ => setEnv env
+  }
+  registerBuiltinAttribute attrImpl
+  pure { attr := attrImpl, ext, preserveOrder := impl.preserveOrder }
 
 builtin_initialize methodSpecsSimpExtension : SimpExtension ←
   registerSimpAttr `method_specs_simp

src/Lean/ResolveName.lean

@@ -43,7 +43,9 @@ def registerReservedNamePredicate (p : Environment → Name → Bool) : IO Unit
   reservedNamePredicatesRef.modify fun ps => ps.push p
 
 builtin_initialize reservedNamePredicatesExt : EnvExtension (Array (Environment → Name → Bool)) ←
-  registerEnvExtension reservedNamePredicatesRef.get
+  -- consulted by `Environment.find?` (via `isReservedName`), so also on resolution search paths;
+  -- the predicate set is fixed at initialization
+  registerEnvExtension reservedNamePredicatesRef.get (tcResolutionAccess := .exempt)
 
 /--
 Returns `true` if `name` is a reserved name.