47 lines
2 KiB
Diff
47 lines
2 KiB
Diff
# UNDF: UNDF-2026-000001260
|
|
# CWE-407: Algorithmic Complexity -- O(K*N) -> O(K+N) in inductive type validation
|
|
#
|
|
# Defect: std::find(result_args...) inside for(arg : to_check) -- O(K*N) where
|
|
# K = to_check.size(), N = result_args.size(). Kernel inductive type checker.
|
|
#
|
|
# Fix: build expr_set from result_args before loop -- O(N) build, O(1) lookup.
|
|
# Total: O(K+N).
|
|
#
|
|
# Also fixes init_elim_level(): std::find(m_lparams...) in while loop for fresh
|
|
# name generation. m_lparams is a names list of length L. Scanning O(L) per
|
|
# iteration gives O(L^2) to find a free slot at position L. Fix: build
|
|
# name_set before loop for O(1) collision check.
|
|
#
|
|
# Complexity gate:
|
|
# K=N=500: must complete in <0.1s (vs ~0.5s defective)
|
|
--- a/src/kernel/inductive.cpp
|
|
+++ b/src/kernel/inductive.cpp
|
|
@@ -7,6 +7,7 @@
|
|
#include "runtime/sstream.h"
|
|
#include "runtime/utf8.h"
|
|
#include "util/name_generator.h"
|
|
+#include "kernel/expr_sets.h"
|
|
#include "kernel/environment.h"
|
|
#include "kernel/type_checker.h"
|
|
#include "kernel/instantiate.h"
|
|
@@ -526,9 +526,11 @@ namespace lean {
|
|
buffer<expr> result_args;
|
|
get_app_args(type, result_args);
|
|
/* Check condition 2: every argument in to_check must occur in result_args */
|
|
+ expr_set result_args_set(result_args.begin(), result_args.end());
|
|
for (expr const & arg : to_check) {
|
|
- if (std::find(result_args.begin(), result_args.end(), arg) == result_args.end())
|
|
+ if (result_args_set.find(arg) == result_args_set.end())
|
|
return true; /* Condition 2 failed */
|
|
}
|
|
return false;
|
|
@@ -540,8 +542,10 @@ namespace lean {
|
|
} else {
|
|
name u("u");
|
|
int i = 1;
|
|
- while (std::find(m_lparams.begin(), m_lparams.end(), u) != m_lparams.end()) {
|
|
+ name_set lparams_set = to_name_set(m_lparams);
|
|
+ while (lparams_set.contains(u)) {
|
|
u = name("u").append_after(i);
|
|
i++;
|
|
}
|