Skip to content

doc: point the packed-matrix prototype report at its implementation - #9163

Open
kim-em wants to merge 1 commit into
mainfrom
packed-kernel-doc-followup
Open

doc: point the packed-matrix prototype report at its implementation#9163
kim-em wants to merge 1 commit into
mainfrom
packed-kernel-doc-followup

Conversation

@kim-em

@kim-em kim-em commented Aug 4, 2026

Copy link
Copy Markdown
Owner

This PR adds a forward pointer from the packed-matrix prototype report to the report that measures the landed implementation, and updates the benchmark module's description of what its packed variants are for now that the implementation exists.

reports/hexbz-packed-fp-matrix.md prices a benchmark prototype. Its factors were the input to a decision, not a description of shipped code, and the specialization they justified landed in #9158 "perf: pack the Berlekamp fixed-space matrix into UInt32 words". A reader arriving at the prototype page had nothing telling them that, and its 17.0x is not the implementation's 6.06x.

bench/HexBench/BerlekampKernel.lean described its packed variants as prototyped "before any production specialization is written". One is written. The variants are still doing two jobs, and the docstring now names them: they remain the entry-for-entry oracle Hex.Berlekamp.Packed's output is checked against on every phase-profile run, and they are the floor the implementation's own cost is read against, which is where the measured 2.62x gap on cyclo_phi385 comes from.

Documentation only. No Lean declaration changes; check_factor_sweep_freshness.py still passes, so no re-measurement is implied.

🤖 Prepared with Claude Code

The prototype report's factors price a benchmark, and the specialization they
justified has since landed, so a reader arriving there could take them for the
shipped implementation's. Add the forward pointer, and say what the benchmark
module's packed variants are for now that the implementation exists.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant