engineering/java-topology
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

scan-todo: add lean4 wave 35, add Priority 4c formal methods section

Browse source
This commit is contained in:
russell@unturf.com 2026-04-13 09:08:56 -04:00
parent 67012b350c
commit f6ac255a41
1 changed files with 8 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

9
SCAN-TODO.md
View file

@ -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