From f6ac255a4105138e6adebe814fb7208f4634950d Mon Sep 17 00:00:00 2001 From: "russell@unturf.com" Date: Mon, 13 Apr 2026 09:08:56 -0400 Subject: [PATCH] scan-todo: add lean4 wave 35, add Priority 4c formal methods section --- SCAN-TODO.md | 9 ++++++++- 1 file changed, 8 insertions(+), 1 deletion(-) diff --git a/SCAN-TODO.md b/SCAN-TODO.md index 0299fb2eb..4cf5d6527 100644 --- a/SCAN-TODO.md +++ b/SCAN-TODO.md @@ -1,6 +1,6 @@ # Scan TODO — Unscanned High-Value Targets -Status: 865 UNDF, 420+ defect dirs, 34 waves complete. +Status: 865 UNDF, 420+ defect dirs, 35 waves complete. Rule: clone, scan, delete clone after. Keep disk under 90%. ## Priority 1 — Major infrastructure not yet scanned @@ -43,6 +43,13 @@ Rule: clone, scan, delete clone after. Keep disk under 90%. - [ ] Solvespace (C++, parametric CAD) - [x] Cura / PrusaSlicer (C++/Python, 3D printing slicers) — cura-0001 MOAD-0001 CompatibleMachineModel list rebuild O(P^2) LOW-MEDIUM; cura-0002 MOAD-0001 SettingInheritanceManager List[str] membership O(S) per property change HIGH 109x; prusaslicer-0001/0002/0003 MOAD-0001 (pre-existing); prusaslicer-0004 MOAD-0001 FillRectilinear queue O(R^2) std::find 64x; MOADs 0002/0003/0004/0005 CLEAN both targets +## Priority 4c — Formal Methods / Theorem Provers + +- [x] Lean 4 (Lean+C++, theorem prover + build system) — lean4-0001 MOAD-0001 Lake guardCycle List.contains O(N^2) in topological build (Cycle.lean:83); lean4-0002 MOAD-0001 kernel/inductive.cpp std::find nested loop O(K*N); lean4-0003 MOAD-0001 fresh name generation std::find while loop (inductive.cpp:543, util.cpp:69); lean4-0004 MOAD-0005 ir_interpreter.cpp double-checked locking race in symbol cache (828-869); lean4-0005 MOAD-0005 Lake job registration IO.Ref race (Run.lean:157); lean4-0006 MOAD-0003 trace.cpp LEAN_THREAD_PTR(g_opts) leaks across thread pool; lean4-0007 MOAD-0001 runtime/process.cpp Windows env var O(N^2); MOAD-0004/0011 CLEAN; MOAD-0007 CLEAN +- [ ] Coq (OCaml, theorem prover) +- [ ] Isabelle/HOL (ML, theorem prover) +- [ ] Agda (Haskell, dependently typed) + ## Priority 5 — AI/ML new wave - [x] Ollama (Go, local LLM runtime) — ollama-0001 MOAD-0001 CWE-407 kvcache buildMask slices.Contains O(B*E) Gemma3 multi-image HIGH 250x; MOADs 0002/0003/0004/0005 CLEAN