java-topology/whitepaper/outreach/lean4.md

Lean 4 — Multi-MOAD Disclosure Brief

Project: Lean 4 (leanprover/lean4) Disclosure date: 2026-04-13 Severity: HIGH Speedup: varies by defect: 34x (lean4-0001 N=2000), 678x (lean4-0002 K=N=1000), 210x (lean4-0003 N=1000) — all confirmed by benchmark Status: patch-ready — 7 patches on unlean4 branch, benchmarks complete

---

Summary

Lean 4 contains seven confirmed defects spanning four MOAD classes. Four reach the O(N^2) threshold (MOAD-0001 — A Sedimentary Defect), two represent concurrent race conditions (MOAD-0005 — A Thundering Herd), and one is a thread-local context leak (MOAD-0003 — A Leaked Context). The highest-impact finding is in Lake, Lean's build system: cycle detection during topological dependency resolution uses a plain List for O(N) membership testing on every node visit, producing O(N^2) total cost on linear dependency chains. Large Lean projects (Mathlib4: ~2000 source files) traverse dependency subgraphs deep enough to feel this.

The Defects

lean4-0001 (MOAD-0001 — HIGH): src/lake/Lake/Util/Cycle.lean:83

Lake's guardCycle function carries a CallStack κ = List κ. On every node visit during topological build traversal, it calls List.contains to detect cycles. With a dependency chain of depth D, each call scans the entire ancestor stack: O(D) per call, O(N x D) total. Worst case (linear chain, D = N): O(N^2).

public abbrev CallStack κ := List κ        -- plain List, no hash index

@[inline] public def guardCycle ... : m α := do
  let parents <- getCallStack
  if parents.contains key then             -- O(N) scan every node visit
    throwCycle ...
  else
    withCallStack (key :: parents) act

Fix: carry a parallel Std.HashSet for O(1) .contains, keep the List for cycle path reporting only.

N modules (linear chain)	guardCycle scans	comparisons
100	100	~5,000
500	500	~125,000
1,000	1,000	~500,000

lean4-0002 (MOAD-0001 — MEDIUM): src/kernel/inductive.cpp:529

The kernel's inductive type validator checks that every type-former argument appears in the constructor return type. std::find on a plain buffer<expr> runs inside an outer loop over to_check. Cost: O(K x N) per constructor, where K = type-former arg count, N = return-type arg count.

for (expr const & arg : to_check) {                                // O(K) outer
    if (std::find(result_args.begin(), result_args.end(), arg)     // O(N) inner
            == result_args.end())
        return true;
}

Fix: expr_set result_set(result_args.begin(), result_args.end()) before the loop; replace std::find with result_set.find.

lean4-0003 (MOAD-0001 — LOW-MEDIUM): src/kernel/inductive.cpp:543, src/library/util.cpp:69

Two identical patterns: fresh name generation via std::find in a while loop scanning a growing vector<name> or names list. Each iteration scans the full list. Cost O(N^2) to find a free slot at position N.

// library/util.cpp:69
while (std::find(lp_names.begin(), lp_names.end(), l) != lp_names.end()) {
    l = name("l").append_after(i++);
}

Fix: convert to name_set before the loop for O(1) collision check.

lean4-0004 (MOAD-0005 — HIGH): src/library/ir_interpreter.cpp:828-869

The IR interpreter's lookup_symbol uses double-checked locking without memory barriers. A first read of m_symbol_cache runs without any lock. The lock is then acquired (shared), released, and re-acquired (exclusive) for the actual compute+insert. On weakly-ordered architectures (ARM, RISC-V) without explicit memory barriers, a second thread can observe partially-initialized cache entries from the unsynchronized first read.

auto e = m_symbol_cache.find(fn);          // (1) unguarded read
if (e != m_symbol_cache.end()) return e->second;
std::shared_lock lock(*g_native_symbol_cache_mutex);
// ... unlock ... re-acquire exclusive ...
// (2) second check + compute + insert under exclusive lock

Fix: guard m_symbol_cache under the shared lock for the initial read, eliminating the unsynchronized check.

lean4-0005 (MOAD-0005 — HIGH): src/lake/Lake/Build/Job/Register.lean:43, src/lake/Lake/Build/Run.lean:157

Lake spawns build jobs as async tasks (via Job.async). All concurrent tasks share a single BuildContext.registeredJobs : IO.Ref (Array OpaqueJob). Each calls .modify (·.push job) without a mutex. Lean's IO.Ref.modify is not atomic across concurrent tasks: two tasks reading the same array and both pushing will lose one registration.

-- IO.Ref (Array OpaqueJob) — shared, no mutex
(← getBuildContext).registeredJobs.modify (·.push job)

-- monitor drains the same ref concurrently:
let newJobs <- (← read).jobs.modifyGet ((·, #[]))

Fix: replace IO.Ref with IO.Mutex (or a Channel) for the job queue. Use .atomically for all register and drain operations.

lean4-0006 (MOAD-0003 — MEDIUM): src/kernel/trace.cpp:16

Trace options arrive as a thread-local pointer via LEAN_THREAD_PTR(const options, g_opts). Lean's async task system reuses a thread pool. When a thread finishes one elaboration task and picks up another, the prior task's trace options remain in g_opts. The new task inherits the old configuration: incorrect trace output, potential information leakage across elaboration contexts.

LEAN_THREAD_PTR(const options, g_opts);   // never cleared at task boundaries

bool is_trace_class_enabled(name const & n) {
    if (!g_opts) return false;
    return is_trace_class_enabled_core(*g_opts, n);
}

Fix: reset g_opts to nullptr at task start/end in the thread pool scheduler, consistent with reset_thread_local() already called elsewhere in the runtime.

lean4-0007 (MOAD-0001 — LOW-MEDIUM, Windows only): src/runtime/process.cpp:250

When spawning child processes on Windows with environment variable inheritance, the runtime iterates all inherited env var keys and calls unordered_map::count({key_begin, key_end}), constructing a temporary std::string from a char range on every iteration. With N environment variables: O(N) string constructions inside an O(N) loop. Typical Windows environments carry 50-200 variables; the waste is real but not critical.

while (*key_begin) {
    ...
    if (!new_env_vars.count({key_begin, key_end})) {   // std::string constructed per iteration
        ...
    }
}

Fix: use std::string_view for key lookup, or pre-build a key set from new_env_vars before the loop.

Impact

Lean 4 is the implementation language for Lean's entire elaborator, tactic engine, standard library, and build system (Lake). It underpins Mathlib, the largest formal mathematics library in existence, and is the primary tool for formally verified software in academic and industrial settings. Microsoft Research, CMU, and dozens of universities use Lean 4 for formal verification research.

The Lake MOAD-0001 defect (lean4-0001) hits on every build of a project with deep module dependency chains. Mathlib4 has ~2,000 Lean files with layered dependencies: any build subgraph with a linear chain of D modules traverses O(D^2) comparisons. On a cold build, this compounds across hundreds of independent traversals.

The MOAD-0005 defects (lean4-0004, lean4-0005) affect runtime stability under concurrent builds. Lean 4's async build system (-j N flag) spawns parallel jobs: the job registration race means build progress can silently drop jobs from the monitor display or lose registrations under load.

MOAD Reference

Each defect class maps to a published research post on undefect.com. These describe the abstract pattern, root cause, and canonical fix — independent of any specific project.

MOAD	Codename	Defects in Lean 4	Research
MOAD-0001	A Sedimentary Defect (CWE-407)	lean4-0001, lean4-0002, lean4-0003, lean4-0007	undefect.com/moad-2026-0001/
MOAD-0003	A Leaked Context	lean4-0006	undefect.com/moad-2026-0003/
MOAD-0005	A Thundering Herd (CWE-362)	lean4-0004, lean4-0005	undefect.com/moad-2026-0005/

What We Ask

We ask the Lean 4 maintainers to confirm the defects, review our proposed fixes, and merge patches upstream. We coordinate disclosure timing — we will hold publication of patches until upstream confirms receipt and has a reasonable window to respond.

Contact: security@undefect.com