java-topology/docs/tickets/lean4-0001-lake-guardcycle-callstack-list-quadratic.md

lean4-0001: guardCycle() O(N²) — List.contains on call stack in topological build traversal

Target: leanprover/lean4 Severity: HIGH CWE: CWE-407 (Inefficient Algorithmic Complexity) MOAD: MOAD-0001 (A Sedimentary Defect) File: src/lake/Lake/Util/Cycle.lean:83, src/lake/Lake/Build/Topological.lean:98 Language: Lean 4 Status: open

Description

guardCycle uses List.contains for cycle detection inside Lake's topological dependency resolver. Every module build traversal calls guardCycle once per node, each time scanning the entire ancestor call stack linearly. For a project with N modules in a linear dependency chain, total cost reaches O(N²).

Root Cause

-- Lake/Util/Cycle.lean:14
public abbrev CallStack κ := List κ   -- plain List, no hash index

-- Lake/Util/Cycle.lean:79–86
@[inline] public def guardCycle
  [BEq κ] [Monad m] [MonadCycle κ m] (key : κ) (act : m α)
: m α := do
  let parents ← getCallStack
  if parents.contains key then          -- O(N) scan every call
    throwCycle <| key :: (parents.partition (· != key)).1 ++ [key]
  else
    withCallStack (key :: parents) act  -- prepend: stack grows to depth D

Called from recFetchAcyclic at Lake/Build/Topological.lean:98 for every node in the module dependency graph during a build.

With a linear chain A → B → C → … → Z (N modules):

• node 1: scan depth 0
• node 2: scan depth 1
• node N: scan depth N-1
• Total: O(N²/2) comparisons

Complexity

N modules (linear chain)	guardCycle calls	comparisons
100	100	~5,000
500	500	~125,000
1000	1000	~500,000

Real projects (Mathlib4: ~2000 files) hit this on dependency-heavy subgraphs.

Fix

Carry a parallel HashSet (or NameHashSet / Std.HashSet) for O(1) membership test. Keep the List only for cycle path reporting.

-- Proposed: pair (HashSet for O(1) contains, List for cycle reporting)
public abbrev CallStack κ := Std.HashSet κ × List κ

@[inline] public def guardCycle
  [BEq κ] [Hashable κ] [Monad m] [MonadCycle κ m] (key : κ) (act : m α)
: m α := do
  let (set, list) ← getCallStack
  if set.contains key then                    -- O(1)
    throwCycle <| key :: (list.partition (· != key)).1 ++ [key]
  else
    withCallStack (set.insert key, key :: list) act

Speedup Estimate

Linear chain N=1000: O(N²) → O(N). ~1000× faster at that scale. Typical projects (N=50–200 in hot subgraphs): 50–200× faster.