diff --git a/defects/lean4/bench/__pycache__/bench-lean4-0001.cpython-312.pyc b/defects/lean4/bench/__pycache__/bench-lean4-0001.cpython-312.pyc new file mode 100644 index 000000000..69629f35f Binary files /dev/null and b/defects/lean4/bench/__pycache__/bench-lean4-0001.cpython-312.pyc differ diff --git a/defects/lean4/bench/__pycache__/bench-lean4-0002.cpython-312.pyc b/defects/lean4/bench/__pycache__/bench-lean4-0002.cpython-312.pyc new file mode 100644 index 000000000..df54cffef Binary files /dev/null and b/defects/lean4/bench/__pycache__/bench-lean4-0002.cpython-312.pyc differ diff --git a/defects/lean4/bench/__pycache__/bench-lean4-0003.cpython-312.pyc b/defects/lean4/bench/__pycache__/bench-lean4-0003.cpython-312.pyc new file mode 100644 index 000000000..e843fef53 Binary files /dev/null and b/defects/lean4/bench/__pycache__/bench-lean4-0003.cpython-312.pyc differ diff --git a/defects/lean4/bench/bench-lean4-0001.py b/defects/lean4/bench/bench-lean4-0001.py new file mode 100644 index 000000000..9eea18b7f --- /dev/null +++ b/defects/lean4/bench/bench-lean4-0001.py @@ -0,0 +1,55 @@ +#!/usr/bin/env python3 +# bench-lean4-0001.py +# lean4-0001: guardCycle List.contains vs HashSet +# +# Models the Lean4 Environment.guardCycle defect where ancestor cycle +# detection uses List.contains (O(N) per call) inside an O(N) traversal, +# giving O(N^2) total. Fixed version uses a HashSet/set for O(1) contains. + +import sys +import time + +def bench_defective(n): + """Model guardCycle with list.contains, O(N^2) total.""" + t0 = time.perf_counter() + parents = [] + for i in range(n): + _ = i in parents # O(len(parents)) linear scan + parents.insert(0, i) # prepend like withCallStack + return time.perf_counter() - t0 + +def bench_fixed(n): + """Model guardCycle with set.contains, O(N) total.""" + t0 = time.perf_counter() + parents_set = set() + parents_list = [] + for i in range(n): + _ = i in parents_set # O(1) + parents_set.add(i) + parents_list.insert(0, i) + return time.perf_counter() - t0 + +TRIALS = 3 +SIZES = [100, 500, 1000, 2000] + +def run(): + lines = [] + header = "=== lean4-0001: guardCycle List vs HashSet ===" + print(header) + lines.append(header) + + for n in SIZES: + def_times = [bench_defective(n) for _ in range(TRIALS)] + fix_times = [bench_fixed(n) for _ in range(TRIALS)] + d_ms = min(def_times) * 1000 + f_ms = min(fix_times) * 1000 + speedup = d_ms / f_ms if f_ms > 0 else float('inf') + line = f"N={n:<5}: defective={d_ms:.3f}ms fixed={f_ms:.3f}ms speedup={speedup:.1f}x" + print(line) + lines.append(line) + sys.stdout.flush() + + return lines + +if __name__ == "__main__": + run() diff --git a/defects/lean4/bench/bench-lean4-0002.py b/defects/lean4/bench/bench-lean4-0002.py new file mode 100644 index 000000000..82bed7d2e --- /dev/null +++ b/defects/lean4/bench/bench-lean4-0002.py @@ -0,0 +1,56 @@ +#!/usr/bin/env python3 +# bench-lean4-0002.py +# lean4-0002: expr_set inductive type check std::find vs set +# +# Models the Lean4 isInductiveApp / inductive type-check defect where +# result argument deduplication uses std::find (O(N) per call) inside +# an O(K) outer loop, giving O(K*N) total. Fixed version builds a set +# once (O(N)) and queries it O(1) per item. + +import sys +import time + +def bench_defective(k, n): + """Model std::find pattern: O(K*N) total.""" + to_check = list(range(k)) + result_args = list(range(n, 2 * n)) # disjoint so scan goes full length + t0 = time.perf_counter() + for arg in to_check: + _ = arg in result_args # O(N) linear scan + return time.perf_counter() - t0 + +def bench_fixed(k, n): + """Model set lookup pattern: O(N) build + O(K) queries = O(N+K).""" + to_check = list(range(k)) + result_args = list(range(n, 2 * n)) + result_set = set(result_args) # O(N) build -- done once + t0 = time.perf_counter() + for arg in to_check: + _ = arg in result_set # O(1) + return time.perf_counter() - t0 + +TRIALS = 3 +SIZES = [100, 500, 1000] + +def run(): + lines = [] + header = "=== lean4-0002: inductive type check std::find vs set ===" + print(header) + lines.append(header) + + for sz in SIZES: + k, n = sz, sz + def_times = [bench_defective(k, n) for _ in range(TRIALS)] + fix_times = [bench_fixed(k, n) for _ in range(TRIALS)] + d_ms = min(def_times) * 1000 + f_ms = min(fix_times) * 1000 + speedup = d_ms / f_ms if f_ms > 0 else float('inf') + line = f"K=N={sz:<4}: defective={d_ms:.3f}ms fixed={f_ms:.3f}ms speedup={speedup:.1f}x" + print(line) + lines.append(line) + sys.stdout.flush() + + return lines + +if __name__ == "__main__": + run() diff --git a/defects/lean4/bench/bench-lean4-0003.py b/defects/lean4/bench/bench-lean4-0003.py new file mode 100644 index 000000000..9d9794eab --- /dev/null +++ b/defects/lean4/bench/bench-lean4-0003.py @@ -0,0 +1,55 @@ +#!/usr/bin/env python3 +# bench-lean4-0003.py +# lean4-0003: fresh name generation while loop +# +# Models the Lean4 Name.mkFresh / getUnusedName defect where the while +# loop calls List.contains (O(N)) to check for collisions with N existing +# names. For each of M candidates checked, cost is O(M*N). Fixed version +# builds a HashSet once and checks O(1) per candidate. + +import sys +import time + +def bench_defective(n): + """Model while loop with list membership check: O(N) per iteration.""" + existing = list(range(n)) + t0 = time.perf_counter() + candidate = n # will not be found -- simulates worst-case scan + for _ in range(n): + _ = candidate in existing # O(N) each time + return time.perf_counter() - t0 + +def bench_fixed(n): + """Model while loop with set membership check: O(1) per iteration.""" + existing = list(range(n)) + existing_set = set(existing) # O(N) build once + t0 = time.perf_counter() + candidate = n + for _ in range(n): + _ = candidate in existing_set # O(1) + return time.perf_counter() - t0 + +TRIALS = 3 +SIZES = [100, 500, 1000] + +def run(): + lines = [] + header = "=== lean4-0003: fresh name generation ===" + print(header) + lines.append(header) + + for n in SIZES: + def_times = [bench_defective(n) for _ in range(TRIALS)] + fix_times = [bench_fixed(n) for _ in range(TRIALS)] + d_ms = min(def_times) * 1000 + f_ms = min(fix_times) * 1000 + speedup = d_ms / f_ms if f_ms > 0 else float('inf') + line = f"N={n:<5}: defective={d_ms:.3f}ms fixed={f_ms:.3f}ms speedup={speedup:.1f}x" + print(line) + lines.append(line) + sys.stdout.flush() + + return lines + +if __name__ == "__main__": + run() diff --git a/defects/lean4/bench/results.txt b/defects/lean4/bench/results.txt new file mode 100644 index 000000000..d4ef233e2 --- /dev/null +++ b/defects/lean4/bench/results.txt @@ -0,0 +1,16 @@ +=== lean4-0001: guardCycle List vs HashSet === +N=100 : defective=0.206ms fixed=0.027ms speedup=7.7x +N=500 : defective=3.366ms fixed=0.086ms speedup=39.1x +N=1000 : defective=7.688ms fixed=0.292ms speedup=26.3x +N=2000 : defective=38.064ms fixed=1.101ms speedup=34.6x + +=== lean4-0002: inductive type check std::find vs set === +K=N=100 : defective=0.319ms fixed=0.002ms speedup=146.7x +K=N=500 : defective=2.772ms fixed=0.011ms speedup=259.5x +K=N=1000: defective=14.088ms fixed=0.021ms speedup=678.3x + +=== lean4-0003: fresh name generation === +N=100 : defective=0.105ms fixed=0.004ms speedup=29.7x +N=500 : defective=3.317ms fixed=0.016ms speedup=205.6x +N=1000 : defective=19.888ms fixed=0.095ms speedup=209.7x + diff --git a/defects/lean4/bench/run_all.py b/defects/lean4/bench/run_all.py new file mode 100644 index 000000000..1dfbd1401 --- /dev/null +++ b/defects/lean4/bench/run_all.py @@ -0,0 +1,33 @@ +#!/usr/bin/env python3 +# run_all.py -- run all lean4 bench scripts and write results.txt + +import sys +import os +import importlib.util +import time + +BENCH_DIR = os.path.dirname(os.path.abspath(__file__)) + +def load_module(filename): + path = os.path.join(BENCH_DIR, filename) + spec = importlib.util.spec_from_file_location("mod", path) + mod = importlib.util.module_from_spec(spec) + spec.loader.exec_module(mod) + return mod + +all_lines = [] + +for fname in ["bench-lean4-0001.py", "bench-lean4-0002.py", "bench-lean4-0003.py"]: + mod = load_module(fname) + lines = mod.run() + all_lines.extend(lines) + all_lines.append("") + print() + sys.stdout.flush() + +out_path = os.path.join(BENCH_DIR, "results.txt") +with open(out_path, "w") as f: + f.write("\n".join(all_lines) + "\n") + +print(f"results written to {out_path}") +sys.stdout.flush()