Machine-facing rules for agents using this repository.
- Read
README4AI.md,OPTIMIZATION-PROBLEM.md, andCATALOG.mdbefore applying an optimization elsewhere. - Define the target optimization contract before selecting a mechanism: search space, feasible set, objective/direction, correctness constraints, evaluation budget and stopping rule.
- Treat optimization records as patterns, not universal parameter sets.
- Preserve reference semantics and add/retain conformance tests for optimized paths.
- Prefer deterministic, bounded reuse over opaque caches.
- If equivalence enables reuse, encode the equivalence as a named invariant and test it directly.
- For incremental reuse, bind the complete effective input identity and persist a new reusable state only after successful completion.
- For coalescing, merge only semantically equivalent in-flight work; define cancellation/error semantics explicitly.
- For Lean caches, distinguish verified reuse from cold reconstruction in implementation and claims.
- For parallel work, retain deterministic output ordering where required and verify scalar/parallel equivalence. Measure effective concurrency rather than assuming requested workers ran concurrently.
- For adaptive search, preserve the trial ledger and evaluation budget. Remember that excessive parallel batch width can reduce information efficiency.
- For approximation, state an explicit error/degradation contract and keep an exact/reference path where practical. Never silently weaken exact semantics.
- For pruning, test bound soundness independently; never prune on a heuristic presented as proof.
- For critical-path/speculative work, ensure speculation cannot expose side effects before commitment and does not starve the actual critical path.
- For performance budgets, characterize benchmark noise/environment before enforcing a threshold.
- For real-time/DSP work, separate slow control work from hot sample/block work when semantics allow it; avoid allocations and synchronization on the hot path.
- For SIMD/native specialization, require reference parity plus actual code-generation evidence and repeated target-host measurement. Never infer end-to-end speedup merely from wider instructions or an isolated probe.
- For SoA/tiling, bound temporary storage per worker, prove packed-field and reduction equivalence, and re-profile tile sizes on the target cache/memory hierarchy rather than copying donor values.
- For persistent worker pools, test repeated-dispatch state isolation and account for startup/teardown amortization. Physical/logical worker selection is not evidence of CPU affinity or NUMA placement.
- For automatic execution-path promotion, calibrate only already-correct candidates on workload-shaped samples, include lifecycle/tuning costs, require a material promotion margin, preserve canonical/manual control, and fail closed against an independent oracle on parity mismatch.
power_module.mdcontains both implemented ideas and aspirational performance language. Check corresponding code/evidence before promoting a claim.suxen.zipis a source candidate, not validated evidence. Inventory and read relevant source before extracting optimization claims.- The three pinned v1 Lean model files are immutable historical formalization. New records do not become formally proved by association; version future formal modules separately.
- New post-v1 records must state status, source identity, optimization problem contract, preserved contract, validation, limitations and rollback conditions.
- Run
python3 scripts/check_catalog.pyafter catalog changes. - Treat
scripts/check_catalog.pyas the public integrity entrypoint;scripts/check_catalog_normalizer.pyis its internal CommonMark-normalization helper and must not be invoked as a substitute gate. - For mathematical/formal donors, read
EVIDENCE-SCOPE.md; distinguish integrity checks, numerical replay, manuscript arguments, selected theorem coverage and target performance. Published replay instructions are not evidence of an executed replay. - For streamed products and joins, preserve indexed multiplicity, exact ordering and complete tie enumeration; account for replay/snapshot work and consumer output storage. A stopped prefix is incomplete, not a negative decision.
- Keep external Lean replay separate from the pinned v1 model unless a separately reviewed integration satisfies its toolchain, dependency and axiom gates. Challenge placeholders are not solution proofs.