49 lines
1.6 KiB
Markdown
49 lines
1.6 KiB
Markdown
# 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
|
||
|
||
```cpp
|
||
// 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`:
|
||
|
||
```cpp
|
||
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.
|