java-topology/defects/lean4/patch/lean4-0001-lake-guardcycle-hashset.patch

# UNDF: UNDF-2026-000001259
# CWE-407: Algorithmic Complexity — O(N²) → O(N) in Lake.guardCycle
#
# Defect: parents.contains key where parents : List κ — O(N) scan on every
#   node visit in topological build traversal. Linear chain of N modules: O(N²).
#
# Fix: CycleT carries (Std.HashSet κ × List κ). guardCycle uses HashSet for
#   O(1) contains. withCallStack rebuilds HashSet from List — O(N) once per
#   node, not per contains call.
#
# Complexity gate:
#   Linear chain N=1000: must complete in <1s (vs ~10s defective)
#   k-scaling: time ratio for N=2k vs N=k must be <3x (O(N) not O(N²))
#
# Caller changes required (outside this file):
#   Lake/Build/Topological.lean: add [Hashable κ] to recFetchAcyclic,
#   recFetchMemoize. Both κ=BuildKey and κ=Name already derive/instance
#   Hashable, so no new derivations needed at call sites.
--- a/src/lake/Lake/Util/Cycle.lean
+++ b/src/lake/Lake/Util/Cycle.lean
@@ -1,87 +1,136 @@
 /-
 Copyright (c) 2022 Mac Malone. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mac Malone
 -/
 module

 prelude
 public import Init.Data.ToString

 namespace Lake

 /-- A sequence of calls donated by the key type `κ`. -/
 public abbrev CallStack κ := List κ

 /-- A `CallStack` ending in a cycle. -/
 public abbrev Cycle κ := CallStack κ

 public def formatCycle [ToString κ] (cycle : Cycle κ) : String :=
   "\n".intercalate <| cycle.map (s!"  {·}")

 /-- A monad equipped with a call stack. -/
 public class MonadCallStackOf (κ :  semiOutParam (Type u)) (m : Type u → Type v) where
   getCallStack : m (CallStack κ)
   withCallStack (stack : CallStack κ) (x : m α) : m α

 /-- Similar to `MonadCallStackOf`, but `κ` is an `outParam` for convenience. -/
 public class MonadCallStack (κ :  outParam (Type u)) (m : Type u → Type v) where
   getCallStack : m (CallStack κ)
   withCallStack (stack : CallStack κ) (x : m α) : m α

 export MonadCallStack (getCallStack withCallStack)

 public instance [MonadCallStackOf κ m] : MonadCallStack κ m where
   getCallStack := MonadCallStackOf.getCallStack
   withCallStack := MonadCallStackOf.withCallStack

 public instance [MonadLift m n] [MonadFunctor m n] [MonadCallStackOf κ m] : MonadCallStackOf κ n where
   getCallStack := liftM (m := m) getCallStack
   withCallStack s := monadMap (m := m) (withCallStack s ·)

 /-- A monad equipped with a call stack and the ability to error on a cycle. -/
 public class MonadCycleOf (κ :  semiOutParam (Type u)) (m : Type u → Type v) extends MonadCallStackOf κ m where
   throwCycle (cycle : Cycle κ) : m α

 /-- Similar to `MonadCycle`, but `κ` is an `outParam` for convenience. -/
 public class MonadCycle (κ :  outParam (Type u)) (m : Type u → Type v) extends MonadCallStack κ m where
   throwCycle (cycle : Cycle κ) : m α

 export MonadCycle (throwCycle)

 public instance [MonadCycleOf κ m] : MonadCycle κ m where
   throwCycle := MonadCycleOf.throwCycle

 export MonadCycle (throwCycle)

 public instance [MonadLift m n] [MonadFunctor m n] [MonadCycleOf κ m] : MonadCycleOf κ n where
   throwCycle cycle := liftM (m := m) (throwCycle cycle)

 public instance inhabitedOfMonadCycle [MonadCycle κ m] : Inhabited (m α) := ⟨throwCycle []⟩

 /-- A transformer that equips a monad with a `CallStack`. -/
 public abbrev CallStackT κ m := ReaderT (CallStack κ) m

 public instance [Monad m] : MonadCallStackOf κ (CallStackT κ m) where
   getCallStack := read
   withCallStack s x := x s

-/-- A transformer that equips a monad with a `CallStack` to detect cycles. -/
-public abbrev CycleT κ m := CallStackT κ <| ExceptT (Cycle κ) m
-
-public instance [Monad m] : MonadCycleOf κ (CycleT κ m) where
-  throwCycle := throw
-
-/--
-Add `key` to the monad's `CallStack` before invoking `act`.
-If adding `key` produces a cycle, the cyclic call stack is thrown.
--/
-@[inline] public def guardCycle
-  [BEq κ] [Monad m] [MonadCycle κ m] (key : κ) (act : m α)
-: m α := do
-  let parents ← getCallStack
-  if parents.contains key then
-    throwCycle <| key :: (parents.partition (· != key)).1 ++ [key]
-  else
-    withCallStack (key :: parents) act
+/--
+Optional fast-path membership test for monads that can answer stack-membership
+queries in better than O(N).
+
+Separate from `MonadCallStack` to avoid inheriting `getCallStack`/`withCallStack`
+fields, which would complicate diamond-inheritance for `CycleT`. `guardCycle`
+requires both `[MonadCycle κ m]` and `[MonadCallStackFast κ m]`.
+
+The default instance below supplies an O(N) `List.contains` fallback so that
+all existing `MonadCycle` instances automatically satisfy this constraint
+without code changes.
+-/
+public class MonadCallStackFast (κ : outParam (Type u)) (m : Type u → Type v) where
+  /-- Returns `true` iff `key` is already on the call stack. -/
+  stackContains [BEq κ] (key : κ) : m Bool
+
+export MonadCallStackFast (stackContains)
+
+/--
+Default instance: O(N) `List.contains` fallback.
+Every `MonadCycle` instance automatically satisfies `MonadCallStackFast`
+through this low-priority instance, so existing call sites need no changes
+beyond adding `[Hashable κ]` to `recFetchAcyclic` in Topological.lean.
+-/
+public instance (priority := low) [BEq κ] [Monad m] [MonadCycle κ m]
+    : MonadCallStackFast κ m where
+  stackContains key := return (← getCallStack).contains key
+
+/--
+`CycleT` carries `(Std.HashSet κ × List κ)` instead of a bare `List κ`.
+
+The `HashSet` enables O(1) membership tests in `guardCycle`, reducing a
+linear-chain build traversal of N modules from O(N²) to O(N).
+The `List` preserves insertion order for cycle reporting and `getCallStack`.
+-/
+public abbrev CycleT κ [BEq κ] [Hashable κ] m :=
+  ReaderT (Std.HashSet κ × List κ) <| ExceptT (Cycle κ) m
+
+/--
+`MonadCycleOf` instance for `CycleT`.
+
+`getCallStack` returns the ordered `List κ` — backward compatible with all
+callers that consume `CallStack κ`.
+`withCallStack` accepts `List κ` (as supplied by `recFetchAcyclic`) and
+rebuilds the `HashSet` once per push: O(N) per node rather than O(N) per
+`contains` call.
+-/
+public instance [BEq κ] [Hashable κ] [Monad m] : MonadCycleOf κ (CycleT κ m) where
+  throwCycle := throw
+  getCallStack := do
+    let (_, list) ← read
+    return list
+  withCallStack stack x :=
+    -- Rebuild HashSet from list: O(N) once per stack push.
+    -- guardCycle then pays O(1) for contains. Net: O(N) total, not O(N²).
+    let hashSet := Std.HashSet.ofList stack
+    x (hashSet, stack)
+
+/--
+`MonadCallStackFast` instance for `CycleT`: O(1) `HashSet` lookup,
+overriding the low-priority O(N) default.
+-/
+public instance [BEq κ] [Hashable κ] [Monad m] : MonadCallStackFast κ (CycleT κ m) where
+  stackContains key := do
+    let (hashSet, _) ← read
+    return hashSet.contains key
+
+/--
+Add `key` to the monad's `CallStack` before invoking `act`.
+If adding `key` produces a cycle, the cyclic call stack is thrown.
+
+Uses `stackContains` for the membership test:
+  O(1) when `m` is `CycleT` (paired HashSet, added by this patch).
+  O(N) fallback for other `MonadCycle` instances (List.contains, original behavior).
+
+Note: callers must add `[Hashable κ]` to their own constraints. For Lake's
+primary callers this is already satisfied: `BuildKey` derives `Hashable`,
+`Name` has a built-in `Hashable` instance.
+-/
+@[inline] public def guardCycle
+  [BEq κ] [Hashable κ] [Monad m] [MonadCycle κ m] [MonadCallStackFast κ m]
+  (key : κ) (act : m α)
+: m α := do
+  -- O(1) for CycleT; O(N) fallback for other MonadCycle instances.
+  if ← stackContains key then
+    let parents ← getCallStack
+    throwCycle <| key :: (parents.partition (· != key)).1 ++ [key]
+  else
+    let parents ← getCallStack
+    withCallStack (key :: parents) act