java-topology/docs/tickets/lean4-0003-library-util-fresh-name-std-find-while.md

lean4-0003: library/util.cpp + kernel/inductive.cpp — O(N²) fresh name generation via std::find in while loop

Target: leanprover/lean4 Severity: LOW-MEDIUM CWE: CWE-407 (Inefficient Algorithmic Complexity) MOAD: MOAD-0001 (A Sedimentary Defect) Files: src/library/util.cpp:69–72, src/kernel/inductive.cpp:543–546 Language: C++ Status: open

Description

Two identical patterns: a while loop generates fresh names by appending an incrementing index, checking for collisions via std::find on a plain vector each iteration. Cost is O(N²) if N existing names must be checked before a fresh one is found.

Root Cause

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

// kernel/inductive.cpp:543–546
while (std::find(m_lparams.begin(), m_lparams.end(), u) != m_lparams.end()) {
    u = name("u").append_after(i);
    i++;
}

Both scan the full list per attempt. With N existing names: O(N²) to find a free slot at position N.

Fix

Convert to std::unordered_set<name> (or name_set) before the loop:

name_set existing(lp_names.begin(), lp_names.end());
while (existing.count(l)) {
    l = name("l").append_after(i++);
}

Severity Note

Universe parameter counts are typically < 10 in practice. Performance impact is negligible today but the pattern is structurally a sedimentary defect and will bite as Lean handles larger polymorphic libraries.