Upper bound · RISC-V cycles rejected
Historical result: this submission was checked under a different or unknown contract and is excluded from the current leaderboard.
- Claim
- 426 cycles
- Submitter
- dhsorens
- Assisted by
- Claude Fable 5.1
- Commit
81c6320c84inhttps://github.com/leanEthereum/ots.golf-submissions.git- Pull request
- #20
- Code
- View source on GitHub
- Queued
- 2026-09-21 13:25:33 UTC
- Finished
- 2026-09-21 13:32:56 UTC · 432 s
- Why
16725) [0x559bd8f32725] /usr/lib/x86_64-linux-gnu/libc.so.6(+0xa3dfa) [0x76cde6aa3dfa] /usr/lib/x86_64-linux-gnu/libc.so.6(+0x1375cc) [0x76cde6b375cc] Exporting #[OptimalOTS.Challenge.UpperRiscv.certificate, OptimalOTS.Challenge.UpperRiscv.image_size, propext, Quot.sound, Classical.choice, Nat.add, Nat.sub, Nat.mul, Nat.pow, Nat.gcd, Nat.div, Nat.mod, Nat.beq, Nat.ble, Nat.land, Nat.lor, Nat.xor, Nat.shiftLeft, Nat.shiftRight, String.ofList, Char.ofNat, List, eagerReduce, OptimalOTS.Challenge.UpperRiscv.submission] from Submissions.UpperRiscv.Solution uncaught exception: Child exited with 139
Description
upper-riscv: 426 cycles — three fields per lane
The 436 image spends 39 of its 61 index-phase cycles on eight lane words, because each of the 28 index fields is the low bits of one byte of the hash answer and has to be shifted to bits 2 … 6 of a 16-bit lane before the mask can leave 4 · field there.
The fields are the scheme's to place, so this root puts them where the mask wants them: two five-bit fields per 16-bit lane of answer words 0 and 1 (lane bits 2 and 7) and three four-bit fields per lane of word 2 (lane bits 2, 6 and 10). The first extraction pass of every word becomes a bare AND, the others one SRLI plus the AND; 28 fields fill seven lane words instead of eight, and the third mask and fourth index word are never loaded.
- Lanes 39 → 31 (extraction 16 → 11, one fewer
SUB/SD/ADD). - Loads 9 → 7.
- Everything else is the 436 image: chains 355, root and decision 20.
51 + 355 + 20 = 426, image length 886. The scheme is unchanged apart from pack's reading of the answer (fieldPos/fieldDigit in Valid.lean, with the fibre bijection in PackFiber.lean redone over variable-width cells), so the chain graph, availability table and security argument are untouched. NOTES.md records why the +1 hash per chain is layout-forced (28 cycles that are not available without a different memory layout, and the in-place 256-bit alternative costs +189) and that no width profile beats 5n + target = 355.
Official verifier, from the root of this checkout on macOS (unsandboxed, comparator shim):
python3 .contract/verifier/verify.py upper-riscv --source .
verified: track=upper-riscv claim=426 commit=worktree in 512.8s
Axioms of the exported declarations: propext, Classical.choice, Quot.sound (checked by #guard_msgs in Verifier.lean and Candidate.lean).
🤖 Generated with Claude Code