perf: GPT-6.1 Sol says compiler optimization speeds up SHA-256 by 2.36×
Maintainers usually reply within 1 day
Nobody has claimed this yet.
Assessment
- Difficulty
- 5/5
- Estimated time
- Over a week
- Newbie friendliness
- 35/100
- Issue type
- Feature
- Clarity
- Mostly clear
- Activity status
- Active
- Domain
- compilers
Research direction
Start with the prototype in src/Lean/Compiler/LCNF/ScalarArgs.lean, then read its integration in src/Lean/Compiler/LCNF/Passes.lean and the benchmark in tests/bench/sha256/Sha256ProbeBaseline.lean. Review how the pass handles scalar type selection, recursive calls, and wrappers, and run the SHA-256 benchmark and relevant compiler tests. Done means the prototype has received review and testing sufficient to establish correctness and performance.
Written by the indexing model from the issue text.
Description
I don't fully understand the details, but the improvement seems significant, so I am submitting this issue. I hope it would help your development. Feel free to close this issue if it not so helpful.
GPT-6.1 Sol (Medium) + Codex App
Title: Compiler optimization speeds up SHA-256 by 2.36×
I (GPT-6.1 Sol) implemented a prototype compiler optimization that speeds up a SHA-256 benchmark by 2.36×, without changing the original Lean SHA-256 code.
The implementation is on the opt_sha256 branch. The relevant files are:
- ScalarArgs.lean: the new optimization pass, including scalar-type selection, argument splitting, recursive-call rewriting, and wrapper generation.
- Passes.lean: integration into the monomorphic optimization pipeline.
- Sha256ProbeBaseline.lean: the SHA-256 block-processing code, including the loop with eight mutable
UInt32variables.
The SHA-256 block-processing loop maintains eight mutable UInt32 variables representing its working state. Lean carries this state through recursive calls as nested products. Even after specialization and tail-recursion lowering, the generated C retains tuple projections, field updates, and reference-counting/reuse checks on each iteration. Object reuse reduces allocations, but the remaining operations still introduce substantial overhead.
In my local benchmark, runtime decreased from 42.69 ms to 18.05 ms, approximately 58% less time. The difference persists when the generated C is compiled with -O3.
The transformation replaces recursive product arguments with separate scalar arguments.
The following pseudocode illustrates the transformation after simplification; it is not actual Lean code or a literal dump of the generated C.
Before:
loop(i, state):
(a, (b, (c, d))) = state
...
return loop(i + 1, (a', (b', (c', d'))))
After:
worker(i, a, b, c, d):
...
return worker(i + 1, a', b', c', d')
This example shows four variables for readability; the SHA-256 loop carries eight. The worker passes updated scalar values directly to the next iteration, eliminating nested tuple packing and unpacking inside the loop.
A wrapper preserves the original function interface. Tuple construction and projection become local to the worker, allowing the existing simplifier to eliminate them before reference-counting insertion. In the optimized SHA-256 loop, the generated C carries eight uint32_t values between iterations and constructs the result tuple at termination.
The prototype restricts eligible field types to known scalar types supported by existing code generation. It also limits product size and expanded argument count. It does not attempt to solve general structure-layout optimization.
Similar loop-state overhead was discussed in the 2023 Zulip thread “two RBMaps”. This prototype automates an execution shape similar to the suggested handwritten tail-recursion workaround.
This implementation is a prototype and needs further review and testing.
- Dominant language
- Lean
- Stars
- 9.7k
- Forks
- 1.1k
- Avg merge
- 1d 17m
- Merged PRs (30d)
- 296
Getting set up
- No Dockerfile or Docker Compose file
- Has a pull request template
- Read the contributing guide
First steps
- Read the whole issue, then the project's contributing guide.
- Comment on the issue to say you are picking it up — it saves two people doing the same work.
- Fork the repository and make your change on a branch.
- Open a pull request that references the issue number.
More from leanprover/lean4
-
bug
Difficulty 1/5 Under an hour Newbie friendliness 85/100
leanprover/lean4#15925 ·
Maintainers usually reply within 1 day
-
`IO.appPath` fails when `/proc` belongs to another PID namespacePossibly taken @treiher claimed this 6 days ago. Openbug
Difficulty 2/5 1-3 hours Newbie friendliness 72/100
leanprover/lean4#15692 · 3 reactions ·
Maintainers usually reply within 1 day
-
`IO.FS.realPath` reports every failure as `noFileOrDirectory` instead of classifying by `errno`Openbug
Difficulty 2/5 1-3 hours Newbie friendliness 66/100
leanprover/lean4#15683 ·
Maintainers usually reply within 1 day
-
`Child.pid` leaks the `Child` and its pipe file descriptors (owned argument treated as borrowed)Openbug
Difficulty 2/5 1-3 hours Newbie friendliness 70/100
leanprover/lean4#15681 ·
Maintainers usually reply within 1 day
-
bug
Difficulty 2/5 1-3 hours Newbie friendliness 76/100
leanprover/lean4#15677 ·
Maintainers usually reply within 1 day
All issues in leanprover/lean4
Similar issues
-
enhancement scope:diagnostics scope:syntax
Difficulty 2/5 1-3 hours Newbie friendliness 77/100
-
code: refactoring good first issue
Difficulty 2/5 1-3 hours Newbie friendliness 68/100
idris-lang/Idris2#3887 ·
Maintainers usually reply within 1 day
-
severity: low
Difficulty 2/5 1-3 hours Newbie friendliness 72/100
luainkernel/lunatik#2207 ·
Maintainers usually reply within 1 day
-
backend:X86 generated by fuzzer llvm:globalisel miscompilation
Difficulty 2/5 1-3 hours Newbie friendliness 72/100
llvm/llvm-project#235468 · 1 comment ·
Maintainers usually reply within 1 day
-
area:codegen backend:cuda backend:hip bug direction:input
Difficulty 2/5 1-3 hours Newbie friendliness 78/100
CrossGL/crosstl#3061 · 1 comment ·
Maintainers usually reply within 1 day