From ddfeca1b1b58dfa9cc3a25f200f2ccb42e6c861a Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Thu, 14 Aug 2025 16:34:54 +0100 Subject: [PATCH] fix: do not allow access to private primitives in public scope (#9890) This PR addresses a missing check in the module system where private names that remain in the public environment map for technical reasons (e.g. inductive constructors generated by the kernel and relied on by the code generator) accidentally were accessible in the public scope. --- src/Lean/Compiler/IR/Format.lean | 2 +- src/Lean/Compiler/LCNF/Basic.lean | 2 +- src/Lean/Data/Json/Basic.lean | 4 +- src/Lean/Data/Trie.lean | 4 +- src/Lean/Data/Xml/Basic.lean | 4 +- src/Lean/Elab/MutualInductive.lean | 4 +- src/Lean/Elab/StructInst.lean | 2 +- src/Lean/Elab/Tactic/Config.lean | 4 +- src/Lean/LoadDynlib.lean | 4 +- src/Lean/Meta/ReduceEval.lean | 2 +- src/Lean/Meta/Tactic/Grind/Canon.lean | 4 +- src/Lean/Meta/Tactic/Grind/EMatchTheorem.lean | 6 +-- src/Lean/ResolveName.lean | 4 ++ src/Lean/Server/Rpc/RequestHandling.lean | 6 +-- src/Lean/Structure.lean | 2 +- src/Lean/Widget/TaggedText.lean | 12 +++--- src/Std/Internal/UV/TCP.lean | 2 +- src/Std/Internal/UV/Timer.lean | 4 +- src/Std/Internal/UV/UDP.lean | 4 +- src/Std/Sync/Channel.lean | 4 +- stage0/src/stdlib_flags.h | 2 + tests/pkg/module/Module/Basic.lean | 37 +++++++++++++++++++ 22 files changed, 81 insertions(+), 38 deletions(-) diff --git a/src/Lean/Compiler/IR/Format.lean b/src/Lean/Compiler/IR/Format.lean index ba84eb5904..9588ca6bcf 100644 --- a/src/Lean/Compiler/IR/Format.lean +++ b/src/Lean/Compiler/IR/Format.lean @@ -76,7 +76,7 @@ private partial def formatIRType : IRType → Format let _ : ToFormat IRType := ⟨formatIRType⟩ "union " ++ Format.bracket "{" (Format.joinSep tys.toList ", ") "}" -instance : ToFormat IRType := ⟨formatIRType⟩ +instance : ToFormat IRType := ⟨private_decl% formatIRType⟩ instance : ToString IRType := ⟨toString ∘ format⟩ private def formatParam : Param → Format diff --git a/src/Lean/Compiler/LCNF/Basic.lean b/src/Lean/Compiler/LCNF/Basic.lean index 6e0299985a..7accd18a20 100644 --- a/src/Lean/Compiler/LCNF/Basic.lean +++ b/src/Lean/Compiler/LCNF/Basic.lean @@ -715,7 +715,7 @@ partial def Code.collectUsed (code : Code) (s : FVarIdHashSet := {}) : FVarIdHas | .jmp fvarId args => collectArgs args <| s.insert fvarId end -abbrev collectUsedAtExpr (s : FVarIdHashSet) (e : Expr) : FVarIdHashSet := +@[inline] def collectUsedAtExpr (s : FVarIdHashSet) (e : Expr) : FVarIdHashSet := collectType e s /-- diff --git a/src/Lean/Data/Json/Basic.lean b/src/Lean/Data/Json/Basic.lean index 9a89bbdd4d..46c84485b3 100644 --- a/src/Lean/Data/Json/Basic.lean +++ b/src/Lean/Data/Json/Basic.lean @@ -203,7 +203,7 @@ private partial def beq' : Json → Json → Bool | _, _ => false instance : BEq Json where - beq := beq' + beq := private beq' private partial def hash' : Json → UInt64 | null => 11 @@ -216,7 +216,7 @@ private partial def hash' : Json → UInt64 mixHash 29 <| kvPairs.foldl (init := 7) fun r k v => mixHash r <| mixHash (hash k) (hash' v) instance : Hashable Json where - hash := hash' + hash := private hash' def mkObj (o : List (String × Json)) : Json := obj <| Std.TreeMap.Raw.ofList o diff --git a/src/Lean/Data/Trie.lean b/src/Lean/Data/Trie.lean index 9118d4dbc5..7680c07f14 100644 --- a/src/Lean/Data/Trie.lean +++ b/src/Lean/Data/Trie.lean @@ -199,8 +199,8 @@ private partial def toStringAux {α : Type} : Trie α → List Format [ format (repr c), (Format.group $ Format.nest 4 $ flip Format.joinSep Format.line $ toStringAux t) ] ) cs.toList ts.toList -instance {α : Type} : ToString (Trie α) := - ⟨fun t => (flip Format.joinSep Format.line $ toStringAux t).pretty⟩ +instance {α : Type} : ToString (Trie α) where + toString t := private (flip Format.joinSep Format.line $ toStringAux t).pretty end Trie diff --git a/src/Lean/Data/Xml/Basic.lean b/src/Lean/Data/Xml/Basic.lean index 21b254e915..71d8d13e3e 100644 --- a/src/Lean/Data/Xml/Basic.lean +++ b/src/Lean/Data/Xml/Basic.lean @@ -41,5 +41,5 @@ private partial def cToString : Content → String | Content.Character c => c end -instance : ToString Element := ⟨eToString⟩ -instance : ToString Content := ⟨cToString⟩ +instance : ToString Element := ⟨private_decl% eToString⟩ +instance : ToString Content := ⟨private_decl% cToString⟩ diff --git a/src/Lean/Elab/MutualInductive.lean b/src/Lean/Elab/MutualInductive.lean index 43e10702f5..89b96e952d 100644 --- a/src/Lean/Elab/MutualInductive.lean +++ b/src/Lean/Elab/MutualInductive.lean @@ -558,7 +558,7 @@ This is likely a mistake. The correct solution would be `Type (max u 1)` rather but by this point it is impossible to rectify. So, for `u ≤ ?r + 1` we record the pair of `u` and `1` so that we can inform the user what they should have probably used instead. -/ -def accLevel (u : Level) (r : Level) (rOffset : Nat) : ExceptT MessageData (StateT AccLevelState Id) Unit := do +private def accLevel (u : Level) (r : Level) (rOffset : Nat) : ExceptT MessageData (StateT AccLevelState Id) Unit := do go u rOffset where go (u : Level) (rOffset : Nat) : ExceptT MessageData (StateT AccLevelState Id) Unit := do @@ -579,7 +579,7 @@ where /-- Auxiliary function for `updateResultingUniverse`. Applies `accLevel` to the given constructor parameter. -/ -def accLevelAtCtor (ctorParam : Expr) (r : Level) (rOffset : Nat) : StateT AccLevelState TermElabM Unit := do +private def accLevelAtCtor (ctorParam : Expr) (r : Level) (rOffset : Nat) : StateT AccLevelState TermElabM Unit := do let type ← inferType ctorParam let u ← instantiateLevelMVars (← getLevel type) match (← modifyGet fun s => accLevel u r rOffset |>.run |>.run s) with diff --git a/src/Lean/Elab/StructInst.lean b/src/Lean/Elab/StructInst.lean index b6b3a1de95..3c2a86ae6f 100644 --- a/src/Lean/Elab/StructInst.lean +++ b/src/Lean/Elab/StructInst.lean @@ -502,7 +502,7 @@ private instance : ToMessageData ExpandedFieldVal where private instance : ToMessageData ExpandedField where toMessageData field := m!"field '{field.name}' is {field.val}" -abbrev ExpandedFields := NameMap ExpandedField +private abbrev ExpandedFields := NameMap ExpandedField /-- Normalizes and expands the field views. diff --git a/src/Lean/Elab/Tactic/Config.lean b/src/Lean/Elab/Tactic/Config.lean index b21f222642..2ed5d6200d 100644 --- a/src/Lean/Elab/Tactic/Config.lean +++ b/src/Lean/Elab/Tactic/Config.lean @@ -17,12 +17,12 @@ public section namespace Lean.Elab.Tactic open Meta Parser.Tactic Command -private structure ConfigItemView where +structure ConfigItemView where ref : Syntax option : Ident value : Term /-- Whether this was using `+`/`-`, to be able to give a better error message on type mismatch. -/ - (bool : Bool := false) + bool : Bool := false /-- Interprets the `config` as an array of option/value pairs. -/ def mkConfigItemViews (c : TSyntaxArray ``configItem) : Array ConfigItemView := diff --git a/src/Lean/LoadDynlib.lean b/src/Lean/LoadDynlib.lean index 66f88b447f..93e88dbf6c 100644 --- a/src/Lean/LoadDynlib.lean +++ b/src/Lean/LoadDynlib.lean @@ -14,8 +14,8 @@ namespace Lean private opaque DynlibImpl : NonemptyType.{0} /-- A dynamic library handle. -/ -@[expose] def Dynlib := DynlibImpl.type -instance : Nonempty Dynlib := DynlibImpl.property +def Dynlib := DynlibImpl.type +instance : Nonempty Dynlib := by exact DynlibImpl.property private opaque Dynlib.SymbolImpl (dynlib : Dynlib) : NonemptyType.{0} /-- A reference to a symbol within a dynamic library. -/ diff --git a/src/Lean/Meta/ReduceEval.lean b/src/Lean/Meta/ReduceEval.lean index a52d3bda02..bc74d73d46 100644 --- a/src/Lean/Meta/ReduceEval.lean +++ b/src/Lean/Meta/ReduceEval.lean @@ -61,6 +61,6 @@ private partial def evalName (e : Expr) : MetaM Name := do throwFailedToEval e instance : ReduceEval Name where - reduceEval := evalName + reduceEval := private evalName end Lean.Meta diff --git a/src/Lean/Meta/Tactic/Grind/Canon.lean b/src/Lean/Meta/Tactic/Grind/Canon.lean index 0768fed795..039882089e 100644 --- a/src/Lean/Meta/Tactic/Grind/Canon.lean +++ b/src/Lean/Meta/Tactic/Grind/Canon.lean @@ -132,7 +132,7 @@ private inductive ShouldCanonResult where visit deriving Inhabited -instance : Repr ShouldCanonResult where +private instance : Repr ShouldCanonResult where reprPrec r _ := private match r with | .canonType => "canonType" | .canonInst => "canonInst" @@ -142,7 +142,7 @@ instance : Repr ShouldCanonResult where /-- See comments at `ShouldCanonResult`. -/ -def shouldCanon (pinfos : Array ParamInfo) (i : Nat) (arg : Expr) : MetaM ShouldCanonResult := do +private def shouldCanon (pinfos : Array ParamInfo) (i : Nat) (arg : Expr) : MetaM ShouldCanonResult := do if h : i < pinfos.size then let pinfo := pinfos[i] if pinfo.isInstImplicit then diff --git a/src/Lean/Meta/Tactic/Grind/EMatchTheorem.lean b/src/Lean/Meta/Tactic/Grind/EMatchTheorem.lean index 958ea2a1df..960569e5a4 100644 --- a/src/Lean/Meta/Tactic/Grind/EMatchTheorem.lean +++ b/src/Lean/Meta/Tactic/Grind/EMatchTheorem.lean @@ -581,12 +581,12 @@ private structure Context where /-- Only symbols with priority `>= minPrio` are considered in patterns. -/ minPrio : Nat -abbrev M := ReaderT Context StateRefT State MetaM +private abbrev M := ReaderT Context StateRefT State MetaM /-- Helper declaration for finding bootstrapping issues. See `isCandidateSymbol`. -/ private abbrev badForPatterns := [``Eq, ``HEq, ``Iff, ``And, ``Or, ``Not] -def isCandidateSymbol (declName : Name) (root : Bool) : M Bool := do +private def isCandidateSymbol (declName : Name) (root : Bool) : M Bool := do let ctx ← read let prio := ctx.symPrios.getPrio declName -- Priority 0 are never considered, they are treated as forbidden @@ -741,7 +741,7 @@ def main (patterns : List Expr) (symPrios : SymbolPriorities) (minPrio : Nat) : let (patterns, s) ← patterns.mapM (go (inSupport := false) (root := true)) { symPrios, minPrio } |>.run {} return (patterns, s.symbols.toList, s.bvarsFound) -def normalizePattern (e : Expr) : M Expr := do +private def normalizePattern (e : Expr) : M Expr := do go e (inSupport := false) (root := true) end NormalizePattern diff --git a/src/Lean/ResolveName.lean b/src/Lean/ResolveName.lean index bfa03a192f..f03224002f 100644 --- a/src/Lean/ResolveName.lean +++ b/src/Lean/ResolveName.lean @@ -104,6 +104,10 @@ private def containsDeclOrReserved (env : Environment) (declName : Name) : Bool env.containsOnBranch declName || isReservedName env declName || env.contains declName private partial def resolvePrivateName (env : Environment) (declName : Name) : Option Name := do + -- No point in checking private names when exporting. This is an optimization but also necessary + -- for correct visibility checking while we still carry some private names (e.g. kernel-generated + -- from `inductive`) in the public env. + guard !env.isExporting if containsDeclOrReserved env (mkPrivateName env declName) then return mkPrivateName env declName -- Under the module system, we assume there are at most a few `import all`s and we can just test diff --git a/src/Lean/Server/Rpc/RequestHandling.lean b/src/Lean/Server/Rpc/RequestHandling.lean index 47c9d22923..c9705c0294 100644 --- a/src/Lean/Server/Rpc/RequestHandling.lean +++ b/src/Lean/Server/Rpc/RequestHandling.lean @@ -23,7 +23,7 @@ private structure RpcProcedure where /- We store the builtin RPC handlers in a Ref and users' handlers in an extension. This ensures that users don't need to import core Lean modules to make builtin handlers work, but also that they *can* easily create custom handlers and use them in the same file. -/ -builtin_initialize builtinRpcProcedures : IO.Ref (PHashMap Name RpcProcedure) ← +private builtin_initialize builtinRpcProcedures : IO.Ref (PHashMap Name RpcProcedure) ← IO.mkRef {} builtin_initialize userRpcProcedures : MapDeclarationExtension Name ← mkMapDeclarationExtension @@ -33,7 +33,7 @@ private unsafe def evalRpcProcedureUnsafe (env : Environment) (opts : Options) ( env.evalConstCheck RpcProcedure opts ``RpcProcedure procName @[implemented_by evalRpcProcedureUnsafe] -opaque evalRpcProcedure (env : Environment) (opts : Options) (procName : Name) : +private opaque evalRpcProcedure (env : Environment) (opts : Options) (procName : Name) : Except String RpcProcedure open RequestM in @@ -71,7 +71,7 @@ def handleRpcCall (p : Lsp.RpcCallParams) : RequestM (RequestTask Json) := do builtin_initialize registerLspRequestHandler "$/lean/rpc/call" Lsp.RpcCallParams Json handleRpcCall -def wrapRpcProcedure (method : Name) paramType respType +private def wrapRpcProcedure (method : Name) paramType respType [RpcEncodable paramType] [RpcEncodable respType] (handler : paramType → RequestM (RequestTask respType)) : RpcProcedure where wrapper seshId j := do diff --git a/src/Lean/Structure.lean b/src/Lean/Structure.lean index 01bef37500..db3118e369 100644 --- a/src/Lean/Structure.lean +++ b/src/Lean/Structure.lean @@ -84,7 +84,7 @@ private structure StructureState where map : PersistentHashMap Name StructureInfo := {} deriving Inhabited -builtin_initialize structureExt : PersistentEnvExtension StructureInfo StructureInfo (Unit × StructureState) ← registerPersistentEnvExtension { +private builtin_initialize structureExt : PersistentEnvExtension StructureInfo StructureInfo (Unit × StructureState) ← registerPersistentEnvExtension { mkInitial := pure ((), {}) addImportedFn := fun _ => pure ((), {}) addEntryFn := fun (_, s) e => ((), { s with map := s.map.insert e.structName e }) diff --git a/src/Lean/Widget/TaggedText.lean b/src/Lean/Widget/TaggedText.lean index 0e1960be64..738b3a8ffa 100644 --- a/src/Lean/Widget/TaggedText.lean +++ b/src/Lean/Widget/TaggedText.lean @@ -78,12 +78,12 @@ private structure TaggedState where column : Nat := 0 deriving Inhabited -instance : Std.Format.MonadPrettyFormat (StateM TaggedState) where - pushOutput s := private modify fun ⟨out, ts, col⟩ => ⟨out.appendText s, ts, col + s.length⟩ - pushNewline indent := private modify fun ⟨out, ts, _⟩ => ⟨out.appendText ("\n".pushn ' ' indent), ts, indent⟩ - currColumn := private return (←get).column - startTag n := private modify fun ⟨out, ts, col⟩ => ⟨TaggedText.text "", (n, col, out) :: ts, col⟩ - endTags n := private modify fun ⟨out, ts, col⟩ => +private instance : Std.Format.MonadPrettyFormat (StateM TaggedState) where + pushOutput s := modify fun ⟨out, ts, col⟩ => ⟨out.appendText s, ts, col + s.length⟩ + pushNewline indent := modify fun ⟨out, ts, _⟩ => ⟨out.appendText ("\n".pushn ' ' indent), ts, indent⟩ + currColumn := return (←get).column + startTag n := modify fun ⟨out, ts, col⟩ => ⟨TaggedText.text "", (n, col, out) :: ts, col⟩ + endTags n := modify fun ⟨out, ts, col⟩ => let (ended, left) := (ts.take n, ts.drop n) let out' := ended.foldl (init := out) fun acc (n, col', top) => top.appendTag (n, col') acc ⟨out', left, col⟩ diff --git a/src/Std/Internal/UV/TCP.lean b/src/Std/Internal/UV/TCP.lean index 3f4ed27239..7e7dae5e07 100644 --- a/src/Std/Internal/UV/TCP.lean +++ b/src/Std/Internal/UV/TCP.lean @@ -11,7 +11,7 @@ public import Init.System.Promise public import Init.Data.SInt public import Std.Net -@[expose] public section +public section namespace Std namespace Internal diff --git a/src/Std/Internal/UV/Timer.lean b/src/Std/Internal/UV/Timer.lean index dc1e5f7603..852e37cece 100644 --- a/src/Std/Internal/UV/Timer.lean +++ b/src/Std/Internal/UV/Timer.lean @@ -9,7 +9,7 @@ prelude public import Init.System.IO public import Init.System.Promise -@[expose] public section +public section namespace Std namespace Internal @@ -30,7 +30,7 @@ of all functions on `Timer`s. -/ def Timer : Type := TimerImpl.type -instance : Nonempty Timer := TimerImpl.property +instance : Nonempty Timer := by exact TimerImpl.property namespace Timer diff --git a/src/Std/Internal/UV/UDP.lean b/src/Std/Internal/UV/UDP.lean index e3f79bfa56..163a679899 100644 --- a/src/Std/Internal/UV/UDP.lean +++ b/src/Std/Internal/UV/UDP.lean @@ -10,7 +10,7 @@ public import Init.System.IO public import Init.System.Promise public import Std.Net -@[expose] public section +public section namespace Std namespace Internal @@ -26,7 +26,7 @@ Represents a UDP socket. -/ def Socket : Type := SocketImpl.type -instance : Nonempty Socket := SocketImpl.property +instance : Nonempty Socket := by exact SocketImpl.property namespace Socket diff --git a/src/Std/Sync/Channel.lean b/src/Std/Sync/Channel.lean index abb3d655cf..a5e66bc5ab 100644 --- a/src/Std/Sync/Channel.lean +++ b/src/Std/Sync/Channel.lean @@ -800,7 +800,7 @@ private partial def forIn [Monad m] [MonadLiftT BaseIO m] /-- `for msg in ch.sync do ...` receives all messages in the channel until it is closed. -/ instance [MonadLiftT BaseIO m] : ForIn m (Sync α) α where - forIn ch b f := ch.forIn f b + forIn ch b f := private ch.forIn f b end Sync @@ -927,7 +927,7 @@ private partial def forIn [Inhabited α] [Monad m] [MonadLiftT BaseIO m] /-- `for msg in ch.sync do ...` receives all messages in the channel until it is closed. -/ instance [Inhabited α] [MonadLiftT BaseIO m] : ForIn m (Sync α) α where - forIn ch b f := ch.forIn f b + forIn ch b f := private ch.forIn f b end Sync diff --git a/stage0/src/stdlib_flags.h b/stage0/src/stdlib_flags.h index 79a0e58edd..b3911deb05 100644 --- a/stage0/src/stdlib_flags.h +++ b/stage0/src/stdlib_flags.h @@ -1,5 +1,7 @@ #include "util/options.h" +// Dear CI, please update stage 0 + namespace lean { options get_default_options() { options opts; diff --git a/tests/pkg/module/Module/Basic.lean b/tests/pkg/module/Module/Basic.lean index dd113f27c7..e10351a21e 100644 --- a/tests/pkg/module/Module/Basic.lean +++ b/tests/pkg/module/Module/Basic.lean @@ -260,6 +260,43 @@ constructor: #with_exporting #check { x := 1 : StructWithPrivateField } +#check StructWithPrivateField.x + +/-- error: Unknown constant `StructWithPrivateField.x` -/ +#guard_msgs in +#with_exporting +#check StructWithPrivateField.x + +/-! Private constructors should be compatible with public fields. -/ + +public structure StructWithPrivateCtor where private mk :: + x : Nat + +/-- +info: structure StructWithPrivateCtor : Type +number of parameters: 0 +fields: + StructWithPrivateCtor.x : Nat +constructor: + private StructWithPrivateCtor.mk (x : Nat) : StructWithPrivateCtor +-/ +#guard_msgs in +#print StructWithPrivateCtor + +/-- error: invalid {...} notation, constructor for 'StructWithPrivateCtor' is marked as private -/ +#guard_msgs in +#with_exporting +#check { x := 1 : StructWithPrivateCtor } + +#with_exporting +#check StructWithPrivateCtor.x + +#check StructWithPrivateCtor.mk + +/-- error: Unknown constant `StructWithPrivateCtor.mk` -/ +#guard_msgs in +#with_exporting +#check StructWithPrivateCtor.mk /-! Private duplicate in public section should not panic. -/