java-topology/docs/tickets/lean4-0002-kernel-inductive-std-find-nested-loop.md

lean4-0002: kernel/inductive.cpp O(K×N) — std::find in nested loop for inductive type validation

Target: leanprover/lean4 Severity: MEDIUM CWE: CWE-407 (Inefficient Algorithmic Complexity) MOAD: MOAD-0001 (A Sedimentary Defect) File: src/kernel/inductive.cpp:529–532 Language: C++ Status: open

Description

Inside the kernel's inductive type validator, std::find on a plain buffer<expr> runs inside a for loop over another buffer. For a constructor with K type-former arguments and N result arguments, cost reaches O(K×N).

Root Cause

// inductive.cpp:526–532
buffer<expr> result_args;
get_app_args(type, result_args);
/* Check condition 2: every argument in to_check must occur in result_args */
for (expr const & arg : to_check) {                                        // O(K) outer
    if (std::find(result_args.begin(), result_args.end(), arg) == result_args.end())  // O(N) inner
        return true; /* Condition 2 failed */
}

to_check holds type-former arguments; result_args holds application arguments from the return type. Both grow with constructor arity.

Fix

Use std::unordered_set<expr> (or Lean's expr_set) for result_args:

expr_set result_set(result_args.begin(), result_args.end());  // O(N) build
for (expr const & arg : to_check) {
    if (result_set.find(arg) == result_set.end())             // O(1) lookup
        return true;
}

Related

inductive.cpp:543 — same std::find pattern for fresh universe param name generation (while loop scanning m_lparams). Low severity in practice since universe parameter counts stay small, but structurally identical defect.