From 013861948247539332a1810c5ae6b8e4e14d2072 Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Thu, 7 May 2026 11:38:24 +0000 Subject: [PATCH 1/4] fix: codegen should not inspect private ctor of public type --- src/Lean/Compiler/LCNF/Irrelevant.lean | 5 +++++ src/Lean/Compiler/LCNF/ToImpureType.lean | 4 ++++ tests/pkg/module/Module/Basic.lean | 4 ++++ tests/pkg/module/Module/ImportedPrivateImported.lean | 3 +++ tests/pkg/module/Module/PrivateImported.lean | 4 ++++ 5 files changed, 20 insertions(+) diff --git a/src/Lean/Compiler/LCNF/Irrelevant.lean b/src/Lean/Compiler/LCNF/Irrelevant.lean index 79baa4a0a4f4..ca77af069b85 100644 --- a/src/Lean/Compiler/LCNF/Irrelevant.lean +++ b/src/Lean/Compiler/LCNF/Irrelevant.lean @@ -41,6 +41,10 @@ public structure TrivialStructureInfo where Return `some fieldIdx` if `declName` is the name of an inductive datatype s.t. - It does not have builtin support in the runtime. - It has only one constructor. + - The constructor must be as visible as the type, otherwise the compiler may attempt to access + not-imported data. + (It would be sufficient to check the visibility of the type's used constants (and their bodies?) + but we do not currently know of a type where this optimization would be relevant) - This constructor has only one computationally relevant field. -/ public def Irrelevant.hasTrivialStructure? @@ -57,6 +61,7 @@ where fillCache : CoreM (Option TrivialStructureInfo) := do let .inductInfo info ← getConstInfo declName | return none if info.isUnsafe || info.isRec then return none let [ctorName] := info.ctors | return none + if isPrivateName ctorName && !isPrivateName declName then return none let ctorType ← getOtherDeclBaseType ctorName [] if ctorType.isErased then return none let mask ← getRelevantCtorFields ctorName trivialType diff --git a/src/Lean/Compiler/LCNF/ToImpureType.lean b/src/Lean/Compiler/LCNF/ToImpureType.lean index d259110b7dce..684d34b90a14 100644 --- a/src/Lean/Compiler/LCNF/ToImpureType.lean +++ b/src/Lean/Compiler/LCNF/ToImpureType.lean @@ -72,6 +72,10 @@ where fillCache : CoreM Expr := do let numCtors := ctorNames.length let mut numScalarCtors := 0 for ctorName in ctorNames do + if isPrivateName ctorName && !isPrivateName name then + -- If the constructor is private but the type is not, we cannot access the constructor's + -- fields and thus must assume it has a non-scalar layout. + return ImpureType.tobject let some (.ctorInfo ctorInfo) := env.find? ctorName | unreachable! let hasRelevantField ← Meta.MetaM.run' <| Meta.forallTelescope ctorInfo.type fun params _ => do diff --git a/tests/pkg/module/Module/Basic.lean b/tests/pkg/module/Module/Basic.lean index 1af071c62311..835b564132ed 100644 --- a/tests/pkg/module/Module/Basic.lean +++ b/tests/pkg/module/Module/Basic.lean @@ -52,6 +52,10 @@ This is a current compiler limitation for `module`s that may be lifted in the fu #guard_msgs in public def Fun.mk (f : Nat → Nat) : Fun := f +public structure Struct where + x : Nat +deriving Inhabited + #guard_msgs(drop warning) in /-- A theorem. -/ public theorem t : f = 1 := testSorry diff --git a/tests/pkg/module/Module/ImportedPrivateImported.lean b/tests/pkg/module/Module/ImportedPrivateImported.lean index d907685ce65c..8814e36485e1 100644 --- a/tests/pkg/module/Module/ImportedPrivateImported.lean +++ b/tests/pkg/module/Module/ImportedPrivateImported.lean @@ -15,3 +15,6 @@ public import Module.PrivateImported /-! #12833: namespaces privately imported but publicly used must be re-exported. -/ open Namespaced + +/-! Codegen should not fail on attempted trivial structure/enum optimization revealing private data. -/ +def f : StructWithPrivImportedFieldType := default diff --git a/tests/pkg/module/Module/PrivateImported.lean b/tests/pkg/module/Module/PrivateImported.lean index a6f89267db01..04583da43943 100644 --- a/tests/pkg/module/Module/PrivateImported.lean +++ b/tests/pkg/module/Module/PrivateImported.lean @@ -41,3 +41,7 @@ fail with `Unknown constant` in this public theorem signature. -/ public theorem hmulDefaultPrivacy (m : Nat) : ∀ n, m * n = m * n := by intro n rfl + +public structure StructWithPrivImportedFieldType where + private field : Struct +deriving Inhabited From f8b164e6a88e4892edc5d39b3be3982bddf7e47e Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Wed, 13 May 2026 08:28:01 +0000 Subject: [PATCH 2/4] build stage2 --- stage0/src/stdlib_flags.h | 2 ++ 1 file changed, 2 insertions(+) diff --git a/stage0/src/stdlib_flags.h b/stage0/src/stdlib_flags.h index e44444704908..60b1b4acd319 100644 --- a/stage0/src/stdlib_flags.h +++ b/stage0/src/stdlib_flags.h @@ -1,5 +1,7 @@ #include "util/options.h" +// Dear CI, please build stage2 + namespace lean { options get_default_options() { options opts; From 99996f174b8442dc8d9b74666047134cf07209dd Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Wed, 13 May 2026 09:19:43 +0000 Subject: [PATCH 3/4] add missing --plugin to stdlib.make.in --- src/stdlib.make.in | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/stdlib.make.in b/src/stdlib.make.in index 45feac318313..efcf063d290f 100644 --- a/src/stdlib.make.in +++ b/src/stdlib.make.in @@ -80,7 +80,7 @@ endif Lake: Lean # lake is in its own subdirectory, so must adjust relative paths... - +"${LEAN_BIN}/leanmake" -C lake lib lib.export ../${LIB}/temp/LakeMain.o.export PKG=Lake $(LEANMAKE_OPTS) OUT="../${LIB}" LIB_OUT="../${LIB}/lean" TEMP_OUT="../${LIB}/temp" OLEAN_OUT="../${LIB}/lean" EXTRA_SRC_ROOTS=LakeMain.lean + +"${LEAN_BIN}/leanmake" -C lake lib lib.export ../${LIB}/temp/LakeMain.o.export PKG=Lake $(LEANMAKE_OPTS) LEAN_OPTS+="--plugin ${PREV_STAGE}/${CMAKE_RELATIVE_LIBRARY_OUTPUT_DIRECTORY}/libLake_shared${CMAKE_SHARED_LIBRARY_SUFFIX}" OUT="../${LIB}" LIB_OUT="../${LIB}/lean" TEMP_OUT="../${LIB}/temp" OLEAN_OUT="../${LIB}/lean" EXTRA_SRC_ROOTS=LakeMain.lean LeanChecker: Lake +"${LEAN_BIN}/leanmake" lib PKG=LeanChecker $(LEANMAKE_OPTS) OUT="$(OUTARC)" LIB_OUT="$(OUTARC)" TEMP_OUT="${LIB}/temp" OLEAN_OUT="$(OUTARC)" From a225bc6d7ffb934b206a8526161da8ab31bdbf3f Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Wed, 13 May 2026 15:16:39 +0000 Subject: [PATCH 4/4] try opt --- src/Init/System/Promise.lean | 11 ++++++++--- 1 file changed, 8 insertions(+), 3 deletions(-) diff --git a/src/Init/System/Promise.lean b/src/Init/System/Promise.lean index c257b2946130..053941308877 100644 --- a/src/Init/System/Promise.lean +++ b/src/Init/System/Promise.lean @@ -14,7 +14,8 @@ set_option linter.missingDocs true namespace IO -private opaque PromisePointed : NonemptyType.{0} +/-- Internal use. -/ +opaque PromisePointed : NonemptyType.{0} /-- `Promise α` allows you to create a `Task α` whose value is provided later by calling `resolve`. @@ -30,8 +31,12 @@ If the promise is dropped without ever being resolved, `promise.result?.get` wil See `Promise.result!/resultD` for other ways to handle this case. -/ structure Promise (α : Type) : Type where - private prom : PromisePointed.type - private h : Nonempty α + -- HACK: These fields used to be private but that currently prevents trivial structure + -- optimization from happening. The information leak from this is quite mild here. + /-- Internal use. -/ + prom : PromisePointed.type + /-- Internal use. -/ + h : Nonempty α instance [s : Nonempty α] : Nonempty (Promise α) := by exact Nonempty.intro { prom := Classical.choice PromisePointed.property, h := s }