OPT v1.4.0 — Exact Pair Streams, Modular Filtering and Mathematical Evidence

OPT v1.4.0 adds OPT-STREAM-001 — Bounded replayable pair streams, extending the catalog to 22 optimization records. This release covers exact integer enumeration, complete equal-sum joins, modular filtering, and reproducible measurements of their memory–latency tradeoffs.

Exact pair streams and bounded replay

• Adds PairSums, which enumerates indexed pair sums through a heap instead of materializing the entire Cartesian product.
• Adds an exact equal-sum join with bounded tie buffering and suffix replay.
• Preserves duplicate occurrences, original indices and deterministic ordering.
• Supports immutable input snapshots and independent replay clones.
• Treats interrupted enumeration as an incomplete prefix.

The mechanism is independently adapted from the inspected OpenAI math manuscripts, retaining attribution to the classical Schroeppel–Shamir pair-sum method.

Modular pair filtering

Adds a separate FilteredPairSums API that generates only pairs satisfying a declared residue condition.

• Preserves actual-sum and original-index ordering.
• Supports positive composite moduli and modulus one.
• Normalizes signed residues.
• Allocates no table proportional to the modulus.
• Preserves duplicate identities and replay independence.

Congruence remains distinct from exact equality. The existing unfiltered pair stream and exact join retain their established behavior.

Reproducible performance evidence

Three benchmark procedures retain raw samples, environment details, source identities, counts and ordered output digests.

• Pair enumeration: the local 128×128 fixture reduces median traced allocation from 1,871,552 bytes to 23,641 bytes, approximately 79× lower.
• Full joins: 350 verified samples characterize seven fixture shapes and four buffer capacities. Small buffers save memory but can increase replay latency; larger buffers trade additional storage for lower replay cost.
• Modular filtering: 180 verified samples characterize nine fixtures. Sparse balanced fixtures run approximately 24–28× faster locally, while temporary bucket construction raises traced allocation peaks to approximately 2.2× baseline. Dense fixtures show no established latency advantage.

Full-join and modular benchmarks measure timing separately from allocation tracing. These synthetic observations establish neither portable defaults nor target-application speedups.

Mathematical evidence scope

Adds EVIDENCE-SCOPE.md and expands the record template and donor assessment to distinguish:

• file integrity;
• numerical certificate replay;
• manuscript arguments;
• selected formal theorem coverage;
• independent implementation tests;
• target performance measurements.

The OpenAI math assessment is pinned to commit fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb. No donor proofs are imported or reported as independently replayed.

Validation

• 91 tests passing, including exhaustive and adversarial oracle comparisons.
• Catalog integrity verified: 22 records, including five frozen v1 records.
• PR CI passes for tests/archive inventory, catalog integrity, and Lean formalization.
• Lean trust audit verifies 354 declarations.
• Frozen formal model files and the pinned toolchain remain unchanged.

Included pull requests

• #5 — Add bounded pair streams and scoped mathematical evidence
• #6 — Characterize full equal-sum join memory and latency tradeoffs
• #7 — Add exact modular pair filtering with scoped performance evidence

Full changelog: v1.3.0...v1.4.0

Upgrade

No migration is required. The new references are optional additions, and the frozen v1 formalization retains its existing scope.

OPT v1.3.0 — Working-Set-Aware Cache Capacity

OPT v1.3.0 expands the QSOL Optimization Catalog with OPT-CACHE-001 — Working-set-aware cache capacity, a reusable pattern for preventing bounded reuse caches from turning intended reuse into repeated reconstruction, recapture, recompilation, or reload work.

The pattern was motivated by independently reported evidence from Unsloth issue #12468, where a multi-GPU CUDA graph cache regression was isolated to a fixed cache-capacity bound. OPT generalizes the lesson without promoting the donor's cache constants as universal settings.

Highlights

• Adds OPT-CACHE-001 — Working-set-aware cache capacity.
• Adds a provenance-linked source note for the Unsloth CUDA graph cache regression.
• Expands the OPT catalog to 21 optimization records, while preserving the five frozen v1 records.
• Adds cache-capacity guidance to the human and machine-oriented decision maps.
• Strengthens safeguards against cargo-culting cache sizes, worker counts, thresholds, or other source-environment constants.
• Updates catalog regression tests so future record additions do not require hard-coded total-record-count changes.

OPT-CACHE-001

The new pattern addresses a common performance failure:

A bounded reuse cache can become slower when useful states are evicted before their next reuse, forcing expensive work to be reconstructed repeatedly.

Rather than treating cache size as a universal constant, OPT-CACHE-001 requires targets to reason about:

• overlapping live reusable-state cardinality;
• reuse and stack-distance distributions;
• reconstruction or recapture cost;
• eviction and premature-eviction frequency;
• retained-state memory and resource cost;
• cache admission, retention and partitioning policy;
• end-to-end performance rather than raw cache hit rate.

The objective is minimum total workload cost inside an explicit resource envelope, not maximum cache size or maximum hit rate.

Stronger correctness boundaries

The final record incorporates several safeguards identified during review.

Cache-key equivalence

Reducing key cardinality now requires a named equivalence invariant.

Targets must directly test representative distinct source states that intentionally collide under the merged cache key rather than relying only on generic cached-versus-reconstructed parity.

Atomic cache publication

New cache entries must remain private until computation and required validation complete successfully.

Failure or cancellation must not expose partial reusable state or replace an existing authoritative entry.

Correct working-set measurement

The record no longer defines required capacity as every distinct state appearing within a time horizon.

Instead, targets should measure overlapping live retention intervals and reuse/stack-distance distributions.

This avoids oversizing cases such as:

A, A, B, B, C, C

where three distinct states appear overall but a cache capacity of one can preserve every immediate reuse.

Finite tuning budgets

Cache-policy tuning now requires a finite, predeclared evaluation budget with an explicit accounting unit such as:

• candidate evaluations;
• benchmark samples;
• wall-clock time;
• GPU-seconds; or
• another bounded resource.

Targets must also define an operational stopping rule before tuning begins.

Noise-aware performance margins

Performance promotion and rollback margins must be derived from characterized benchmark and environment variability.

A single noisy measurement is not sufficient evidence to promote or reject a cache policy.

External evidence

The new source record documents:

unslothai/unsloth issue #12468

The report isolated a tensor-split decode regression across Windows, WSL2 and bare-metal Linux.

In the reporter's exact-source WSL2 reproduction:

• the released bounded-cache configuration operated at roughly 32–33 tokens/s;
• changing only the cache-capacity bound to a deliberately oversized diagnostic value restored roughly 94–101 tokens/s.

The oversized value was explicitly used as an isolation experiment, not as a proposed production setting.

OPT therefore promotes the mechanism:

measure the reuse working set and manage cache capacity accordingly

—not:

replace one magic number with another.

Catalog integration

OPT-CACHE-001 is now integrated into:

• README.md
• README4AI.md
• CATALOG.md

The pattern composes with existing OPT records including:

• OPT-INV-001 — invariant-driven reuse;
• OPT-BUDGET-001 — performance regression budgets;
• OPT-AUTO-001 — calibrated host-aware path promotion;
• OPT-CONT-001 — partitioned coordination domains;
• OPT-REDUCE-001 — early working-set reduction.

Test maintenance

Catalog regression tests no longer assume a fixed total record count.

Successful integrity output is validated structurally while the immutable v1 boundary remains explicitly checked:

frozen_v1=5

This allows the post-v1 catalog to continue expanding without turning each new optimization record into an unrelated test-maintenance failure.

Provenance

Implemented in:

PR #4 — Add OPT-CACHE-001 working-set-aware cache capacity

#4

External evidence:

Unsloth issue #12468 — Tensor split decode regression

unslothai/unsloth#12468

Upgrade

No migration is required.

Existing OPT records and the frozen v1 formalization remain unchanged. OPT-CACHE-001 is a new post-v1 catalog record and does not extend or alter the immutable v1 Lean proof boundary.

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 execution
• OPT-COAL-001 — Concurrent duplicate-work coalescing
• OPT-SET-001 — Density-adaptive compact sets
• OPT-CONT-001 — Partitioned coordination domains
• OPT-FAN-001 — Shared materialization for fan-out and replay
• OPT-SEARCH-001 — Budget-aware adaptive parameter search
• OPT-APPROX-001 — Contract-bounded approximation
• OPT-REDUCE-001 — Early working-set reduction
• OPT-CRIT-001 — Critical-path prioritization
• OPT-BUDGET-001 — Performance regression budgets
• OPT-PRUNE-001 — Bound-driven search-space pruning
• OPT-SIMD-001 — Evidence-gated native autovectorization
• OPT-SOA-001 — Worker-local SoA tiling
• OPT-POOL-001 — Persistent topology-aware worker pools
• OPT-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 entrypoint
• scripts/check_catalog_normalizer.py — normalization and execution boundary
• scripts/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 html and body state;
• 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.lean
• Lean/OPTFormal/FrozenV100.lean
• Lean/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.py

Existing 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.

OPT v1.1.0 — Lean 4 Formal Verification Layer

#RELEASE NOTES#

OPT v1.1.0 adds a dependency-free Lean 4 formal verification layer for the immutable OPT v1.0.0 optimization catalog.

This release does not rewrite the frozen optimization records. Instead, it adds machine-checkable contracts for their core invariants, evidence boundaries, trust assumptions, and admissibility rules.

Highlights

Lean 4 formalization

The release formalizes key OPT principles including:

• Correctness outranks speed

  • A faster implementation that changes required semantics is not an optimization.

• Adaptation boundaries

  • Admissible optimizations must preserve:

    • semantics
    • named invariants
    • determinism
    • validation
    • provenance
    • evidence boundaries
    • public API behaviour

• OPT-INV-001

  • Cached or reused computation is valid only under an explicit equivalence witness.

• OPT-PAR-001

  • Parallel execution must preserve the scalar/reference result when the deterministic equivalence contract applies.

• OPT-LEAN-001

  • Verified dependency reuse does not constitute evidence of a cold reconstruction.

• DSP approximation contracts

  • Approximate implementations require an explicit error bound, validated tolerance, and reference comparison.

• Resource composition

  • Composed optimizations are modeled against combined CPU, memory, and I/O requirements.

Evidence and benchmark semantics

v1.1.0 formally separates:

• historical observations;
• environment-specific measurements;
• transferable performance targets.

No evidence status, including verified, is sufficient by itself to authorize a transferable benchmark target.

Promotion to a transferable target requires explicit target-context evidence covering:

• target-environment measurement;
• correctness validation;
• provenance binding.

This prevents source-project benchmark numbers from silently becoming universal performance claims.

Frozen v1.0.0 catalog model

The formal model represents the five records frozen in OPT v1.0.0:

• OPT-PY-001
• OPT-INV-001
• OPT-LEAN-001
• OPT-PAR-001
• OPT-DSP-001

Lean proves that the formal catalog contains exactly five distinct records.

suxen.zip remains explicitly classified as source-candidate material. Keyword inventory results are not promoted into measured-performance evidence.

Trust boundary hardening

The Lean layer was subjected to repeated adversarial review and hardened against multiple proof-surface and CI escape paths.

Source-purity gate

Lean source scanning rejects executable uses of:

• sorry
• sorryAx
• admit
• axiom
• constant
• unsafe

The scanner distinguishes executable syntax from inert content including:

• line and nested block comments;
• ordinary strings;
• hash-delimited raw strings;
• interpolated strings;
• nested interpolation;
• character literals;
• guillemet-quoted identifiers.

Regression cases cover bypass attempts involving comment markers, interpolation braces, raw strings, quoted identifiers, and direct sorryAx use.

Full declaration-level axiom audit

The trust audit is no longer limited to a hand-maintained theorem list or even proposition-valued declarations.

Every declaration originating from the formal module set is inspected.

The audited module boundary includes:

• OPTFormal
• every OPTFormal.* module
• OPTFormalAll

The audit:

1. identifies declarations by their originating module rather than namespace;
2. rejects project-originating primitive .axiomInfo declarations;
3. runs Lean.collectAxioms across every formal declaration;
4. permits only Lean core propext;
5. classifies proposition-valued declarations only after the complete declaration audit succeeds.

On the final reviewed PR head, the audit covered:

• 354 formal declarations
• 101 logical exports

This also prevents generated or data-valued declarations from creating an unaudited proof channel.

Multi-version formal audit root

Lean/OPTFormalAll.lean provides an unpinned audit root for current and future formal modules.

CI recursively enumerates every module under:

Lean/OPTFormal/

and requires the audit root to import the complete set.

Future modules such as a hypothetical OPTFormal.FrozenV200 therefore cannot silently exist outside the formal audit graph.

Declarations are tracked by originating module, so placing a theorem in the root namespace or an unrelated namespace does not evade the trust boundary.

Frozen v1 formal-model integrity

The constructed v1 formal model is permanently bound to Git history.

Protected files include:

• Lean/OPTFormal/Core.lean
• Lean/OPTFormal/FrozenV100.lean
• Lean/OPTFormal.lean

Rather than storing editable expected blob hashes beside the CI check, the workflow derives the baseline from the historical commit that established the three-file blob gate on the canonical first-parent lineage.

For the merged PR #2 history, that anchor is:

a6fc797ef5759a5f0005b18630748ba68b5c7631

First-parent traversal prevents merged side history from substituting an alternative earlier baseline.

Future releases may add separately versioned formal modules, but the v1 formal model cannot be silently rewritten.

Reproducible Lean environment

The formal package intentionally has no mathlib or third-party Lean dependencies.

CI pins:

• Lean 4.33.1
• the exact lean-toolchain declaration
• the official Lean Linux distribution SHA-256
• the checkout action by commit SHA

The Lean archive is downloaded from the official release and authenticated before extraction.

Validation

The final PR #2 head passed both required validation lanes:

Lean formalization

• frozen v1.0.0 identity verified
• canonical first-parent model anchor verified
• source scanner self-tests passed
• source-purity scan passed
• complete formal-module coverage verified
• OPTFormal built successfully
• OPTFormalAll built successfully
• 354 formal declarations audited
• 101 logical exports classified
• axiom allowlist verified
• only core propext permitted

Existing OPT regression suite

• ZIP inventory regression tests passed
• bundled SUXEN archive audit passed
• existing OPT behavior remained green

Provenance

Frozen OPT v1.0.0 release commit:

41e2fc3677469839fb298dedefd0ce72caebcc68

Final reviewed PR #2 head:

530287344756f0a3444bcf419d81fe3e6339e7e2

PR #2 merge commit:

10c2e27075b9174ef2f2d586c281dc1da45588b5

Pull request:

QSOLKCB/OPT#2

Release principle

Correctness outranks speed.

OPT v1.1.0 turns that principle from repository doctrine into an executable formal contract.

Optimization remains optimization only when the required semantics, evidence boundaries, determinism, provenance, and validation survive the transformation.

OPT v1.0.0 — QSOL Optimization Catalog

#RELEASE NOTES#

OPT v1.0.0 establishes the first stable release of the QSOL optimization catalog: a provenance-aware repository of reusable performance patterns, implementation guidance, validation contracts, and evidence boundaries for future QSOL development.

This release turns OPT from a minimal repository into a reusable optimization vault covering deterministic testing, invariant-driven reuse, trust-preserving Lean CI, bounded parallel execution, and control-rate/sparse/vectorized DSP.

Highlights

Reusable optimization catalog

The initial catalog contains five optimization records:

• OPT-PY-001 — Deterministic Test Execution

  • minimal deterministic fixtures
  • vectorized assertions
  • bounded deterministic caches
  • convergence and cycle early exits
  • sweep reduction
  • repeated-work elimination

• OPT-INV-001 — Invariant-Driven Computation Reuse

  • reuse only where equivalence is established
  • preserve reference-path validation
  • avoid cargo-cult caching and unsafe memoization

• OPT-LEAN-001 — Trust-Preserving Lean CI

  • verified dependency reuse
  • isolated cold-trust reconstruction
  • source and artifact integrity checks
  • explicit distinction between cache acceleration and proof trust

• OPT-PAR-001 — Bounded Deterministic Parallel Execution

  • scalar/parallel equivalence
  • bounded worker pools
  • deterministic ordering
  • requested-versus-observed worker accounting
  • environment-scoped performance evidence

• OPT-DSP-001 — Control-Rate, Sparse and Vectorized DSP

  • control-rate separation
  • sparse coupling
  • shared intermediate computation
  • vectorized block synthesis
  • explicit separation between implemented reference mechanisms and unverified native-performance claims

Repository Interface

v1.0.0 introduces the repository structure used by both humans and implementation agents:

• expanded README.md
• README4AI.md
• AGENTS.md
• CATALOG.md
• reusable optimization-record template
• provenance and source documentation

The catalog is designed around a simple rule:

Correctness outranks speed.

Optimization records must preserve the relevant scientific, deterministic, formal, numerical, or evidentiary contract. A faster result that changes the meaning of the computation is not an optimization.

Evidence and Provenance Model

OPT now distinguishes between:

• verified mechanisms
• environment-specific measurements
• implemented references
• proposed techniques
• source candidates

Benchmark numbers are not treated as universal constants. Historical measurements remain attached to their source context, and adaptations are expected to be re-measured on the target environment.

The release also corrects the QEC optimization lineage by separating the v68.x deterministic-test work from the later v170.x multicore benchmark evidence.

Safe Source-Archive Auditing

v1.0.0 includes a bounded, non-extracting recursive ZIP inventory system developed to inspect the preserved suxen.zip source candidate without promoting unsupported claims.

The scanner supports:

• recursive nested ZIP inspection
• ordinary and self-extracting ZIPs
• rebased and non-rebased SFX offsets
• text/source detection
• UTF-8, BOM-marked UTF-16 and UTF-32 handling
• Windows and POSIX path traversal rejection
• terminal-safe diagnostic output
• bounded recursive labels
• nested ZIP, general-member, text, compressed-data and total-output budgets
• bounded DEFLATE, BZIP2 and LZMA decompression
• LZMA dictionary workspace limits
• local/central filename and flag validation
• CRC and actual-size verification
• overlapping-entry rejection
• unsupported ZIP64 and multi-disk rejection
• central-directory and member-count preflight
• bounded keyword-hit reporting
• fail-closed incomplete-inventory semantics

The archive remains a source candidate. Inventory hits are not automatically promoted into optimization records.

Validation

The final v1.0.0 implementation passed the complete ZIP inventory regression suite and the bundled suxen.zip audit before merge.

The final validation state included:

• 43 tests passing
• 14 archives scanned
• 13 nested archives
• 607 members inspected
• 501 text/source members scanned
• 28,935,445 bytes of actual decompressed content validated
• 1,370 optimization-related hits
• inventory_complete=true

Stability Boundary

v1.0.0 establishes the baseline contract for future OPT development:

1. correctness before speed;
2. measured and proposed techniques remain distinct;
3. deterministic, reference, or conformance paths are retained where required;
4. environment-specific constants are not copied blindly;
5. provenance remains attached to optimization claims;
6. safety or trust boundaries may not be weakened merely to improve performance.

Future releases can extend the catalog with additional optimization families while preserving these invariants.

Release Provenance

Initial catalog implementation completed through PR #1.

Final reviewed source head:

9fa4164cf1ce8d4be6568db28e33c5242391278b

Merge commit:

41e2fc3677469839fb298dedefd0ce72caebcc68

---

OPT v1.0.0

Reusable speed without reusable mistakes.