Repository navigation
OPT — v1.2.0 - Contract-Driven Optimization Framework Expansion
#OPT - v1.2.0
This release expands OPT from its original five-record catalog into a broader contract-driven optimization framework while preserving the frozen v1 formal model.
Merged via PR #3 — Expand OPT with contract-driven optimization framework.
Highlights
OPT now treats optimization as a constrained problem rather than simply a collection of performance techniques.
A canonical optimization contract is introduced:
P = (X, F, f, d, C, B, S)
covering:
- search space;
- feasible set;
- objective;
- optimization direction;
- correctness and semantic constraints;
- evaluation budget;
- stopping rule.
The framework is designed to answer a more disciplined question:
What exactly is being optimized, under which invariants, and with what evidence?
15 new optimization records
The catalog grows from 5 to 20 records with the addition of:
OPT-INC-001— Signature-bound incremental executionOPT-COAL-001— Concurrent duplicate-work coalescingOPT-SET-001— Density-adaptive compact setsOPT-CONT-001— Partitioned coordination domainsOPT-FAN-001— Shared materialization for fan-out and replayOPT-SEARCH-001— Budget-aware adaptive parameter searchOPT-APPROX-001— Contract-bounded approximationOPT-REDUCE-001— Early working-set reductionOPT-CRIT-001— Critical-path prioritizationOPT-BUDGET-001— Performance regression budgetsOPT-PRUNE-001— Bound-driven search-space pruningOPT-SIMD-001— Evidence-gated native autovectorizationOPT-SOA-001— Worker-local SoA tilingOPT-POOL-001— Persistent topology-aware worker poolsOPT-AUTO-001— Calibrated host-aware path promotion
The SIMD, SoA, worker-pool and host-auto records are derived from merged GALAXY optimization work while preserving its evidence boundaries. Hardware-specific measurements are not promoted into universal tuning constants.
New optimization problem contract
OPTIMIZATION-PROBLEM.md establishes a common vocabulary and decision boundary for future optimization work.
Records and future implementations are expected to identify the target problem and constraints before selecting or tuning a mechanism.
The optimization-record template, catalog guidance, machine-facing documentation and roadmap have been updated accordingly.
Provenance and evidence
New bounded source notes cover:
- Psycledelics Wonderbuild
- Jazco performance-engineering material
- BayesianOptimization
- Hyperopt
- NLopt
- Awesome WPO
- mathematical and combinatorial optimization
- GALAXY CPU optimization phases
External measurements are retained as provenance and context rather than silently converted into portable performance targets.
Licensing boundaries are explicit. In particular, GPL Wonderbuild implementation code is not copied into this Apache-2.0 repository.
Catalog integrity pipeline
A dependency-free validation pipeline now protects the catalog:
scripts/check_catalog.py— stable public entrypointscripts/check_catalog_normalizer.py— normalization and execution boundaryscripts/check_catalog_core.py— schema, rendering, link and provenance validation
Validation covers:
- record identity and filenames;
- headings and section ownership;
- mandatory post-v1 sections;
- optimization contract fields;
- README and CATALOG coverage;
- visible record links and fragments;
- reference definitions;
- source-evidence identities;
- repository-relative path safety;
- provenance requirements;
- frozen-v1 integrity.
The checker is read-only with respect to repository documentation and retains symlink/write-containment protections.
Adversarial Markdown and HTML hardening
The public validator received extensive adversarial review against CommonMark and browser HTML behaviour.
Retained regression coverage now includes, among other cases:
- hidden and non-rendering ancestry;
- raw HTML block boundaries and same-line terminator suffixes;
- HTML, SVG and MathML namespace transitions;
- SVG
xlink:href; - SVG definition containers;
- table foster parenting and recovery;
- malformed and misnested formatting;
- formatting-element reconstruction;
- duplicate
htmlandbodystate; - select and form parsing behaviour;
- foreign CDATA;
- self-closing foreign elements;
- fenced and indented literal content;
- inline-code protection;
- reference links and images;
- URL/entity/path normalization;
- heading and paragraph recovery;
- visible record-ID inventory.
Public-entrypoint regressions execute against disposable repository fixtures rather than relying solely on internal helper tests.
Astra corrective audit
A supplied Astra audit was incorporated as a bounded corrective pass.
Its retained regression matrix covers:
- paragraph-bounded reference-image ownership;
- raw textarea recovery;
- HTML end-tag recovery;
- URL preprocessing;
- protected link/image spans;
- contextual reference-definition visibility.
The audit corpus remains part of the test suite.
Formalization boundary preserved
The original v1 Lean formalization remains immutable.
This release does not modify:
Lean/OPTFormal/Core.leanLean/OPTFormal/FrozenV100.leanLean/OPTFormal.lean
The original five formalized records remain frozen. New catalog records are engineering guidance and are not presented as theorem-backed merely by association with the v1 model.
Verification
Final merged PR head:
69db479245ea24bf3d1a4f0393dce648234f1c96
Merge commit:
3441c6ceacd4a6ca43ec46de758e2d5bc23d8ca7
Final verification:
- catalog integrity workflow: passed
- Lean formal workflow: passed
- Python regression suite: 61 tests passed
- bundled archive inventory: complete
- final Codex review: no major issues found
- unresolved review threads at final verification: 0
Compatibility
The public validation entrypoint remains:
python3 scripts/check_catalog.pyExisting v1 formal artifacts remain unchanged.
Validation is intentionally stricter for malformed, hidden, misleading or incorrectly attributed catalog content.
Future work
A wholesale parser rewrite was deliberately kept out of this release.
A future bounded migration may replace duplicated Markdown/HTML interpretation with a shared parsed-document representation while preserving:
- the public CLI;
- the existing regression corpus;
- catalog semantics;
- provenance requirements;
- frozen formal artifacts;
- read-only validation guarantees.
That work should be evaluated separately rather than expanding the scope of this release.
This release turns OPT from a small optimization reference catalog into a contract-first, provenance-aware optimization framework with an adversarially tested integrity boundary.