java-topology/defects/lean4/patch/lean4-0003-library-util-fresh-name-set.patch

25 lines
998 B
Diff

# UNDF: UNDF-2026-000001261
# CWE-407: Algorithmic Complexity -- O(N^2) -> O(N) in fresh level param name generation
#
# Defect: std::find(lp_names...) in while loop -- O(N) scan per iteration.
# Generates O(N^2) total work to find a free slot at position N.
# lp_names is a names list iterated fresh each probe.
#
# Fix: convert lp_names to name_set before loop -- O(1) collision check.
# name_set already available via kernel/environment.h -> util/name_set.h.
# No new includes required.
#
# Complexity gate:
# N=1000 existing names: must complete in <0.01s
--- a/src/library/util.cpp
+++ b/src/library/util.cpp
@@ -66,8 +66,9 @@ optional<expr_pair> is_auto_param(expr const & e) {
name mk_fresh_lp_name(names const & lp_names) {
name l("l");
int i = 1;
- while (std::find(lp_names.begin(), lp_names.end(), l) != lp_names.end()) {
+ name_set lp_set = to_name_set(lp_names);
+ while (lp_set.contains(l)) {
l = name("l").append_after(i);
i++;
}