Contributor: @jurajselep, with Codex
Date: 2026-09-15
Problem: 16×16 matrix multiplication
Cost: 63,639, improving 63,819 by 180 (0.2820%)
This builds on the 63,819 program by @SecurityQQ. All 4,096 multiplications and 3,840 additions retain their arithmetic dependencies and order. Input homes and copy chains change, followed by whole-program address allocation.
The search accounts for every other live value when optimizing one input’s
replicas. Alternating restaging and global allocation reached 63,645.
Allowing a wider 1 → 10 → 4 → 1 relay for B[0,7] then replaced a tier-17
reread with source reads costing 1 + 10 + 4 = 15, reaching 63,643.
The final improvement comes from an equal-cost restaging of A[0,0].
Its local read cost remains 90 and the immediate program score remains
63,643. The changed copy lifetimes free capacity that whole-program
allocation uses to reach 63,639. A strict local-improvement rule misses
this interaction. The final program has 1,947 copies and maximum address 626.
| Read site | 63,819 | 63,639 | Change |
|---|---|---|---|
| Copy sources | 20,639 | 20,558 | -81 |
| Multiplication operands | 18,477 | 18,471 | -6 |
| Addition operands | 20,256 | 20,271 | +15 |
| Output exit reads | 4,447 | 4,339 | -108 |
| Total | 63,819 | 63,639 | -180 |
These are abstract read costs under the unchanged scorer.
The verifier derives fresh SSA values, lifetimes, and read counts directly
from the submitted IR. Value v occupies gaps birth(v) < g <= end(v).
Tier t has capacity 2t-1 and read price t. For nonnegative rational
capacity prices p[t,g], the following is a lower bound on any allocation
of that trace:
sum_v min_t (reads(v)*t + sum_{birth(v)<g<=end(v)} p[t,g])
- sum_{t,g} (2*t-1)*p[t,g]
The certificate stores 4,908 prices as [tier, gap, numerator, denominator].
Exact rational arithmetic gives capacity supply 27,390 and lower bound
63,639. Tiers above 26 have zero rent; the minimum over that entire
unbounded tail occurs at tier 27. The checker includes this alternative.
The submitted physical program is the feasible integral witness and has the same cost. Thus 63,639 is optimal for this fixed SSA trace. The certificate does not cover different copy graphs, arithmetic orders, reduction trees, or arithmetic circuits.
Only Python’s standard library and existing repository code are needed:
python3 -S matmul/submissions/best_63639.py
python3 -S -m unittest matmul.test_record_63639 -v
The verifier pins the IR and certificate hashes, runs the official scorer
and the independent polynomial prover from best_66178.py, checks operation
counts and the read-cost ledger, compares the copy-erased arithmetic DAG
and order against best_63819.ir, and replays the exact dual bound.
All 256 outputs are proved correct for arbitrary inputs. Verification works
from any directory and does not rerun the search or require an optimizer.
IR SHA-256:
4f1ce0c343cc0dd3d78b56be6907fd8a9bb59e93af0e9b3293028788fa5f61d0.