Upper bound · RISC-V cycles verified

Summary

• Track: upper-riscv
• Claim: 438 cycles (previous record 445, PR #15)
• Contract pin: 9b6b1c4229cb4a9c61f8acef79a4c51556c7988e (keygen budget 2^20)

The same bare-chain forest scheme as the 445 record (28 chains × 32 levels, 192-bit values, no headers or level tags), with seven cycles of layout:

• Target 215 instead of 216 (−1). compW wid 28 215 ≥ 712 · 2^105 accepted indices; miss^(2^20) ≤ 0.882 · 2^-128, which with the bad-record weight δ ≤ 2^-135 stays within the 2^-128 failure allowance (Availability.lean). 214 would fail (about 2^-118).
• Index query hashed in place (−3). The loader lays out message ‖ nonce contiguously at 0x400010; the scheme's index query is H(swapHalves (m ‖ η)), and swapHalves has an explicit inverse (GScheme.lean, SignIdx.lean), so no copy to the data area.
• Lane words below the signature, addressed from the message pointer; jump halfword loaded relative to each chain's answer buffer (−1). No data-base register, so the old ADDI x29 setup is gone.
• Chain 0 starts from the message pointer (−1). Its prologue is ADDI x10, x10, 48.
• Root answer written where chain 27 left x12 (−1). rootLin is two instructions; the decision reads the answer from that buffer.

Cost: 63 (index) + Σ_k (4 + field_k + 1) + 20 (root and decision) = 63 + 355 + 20 = 438, image length 898. README.md describes the construction and proof map; NOTES.md has the journal and what is left.

Verification

python3 .contract/verifier/verify.py upper-riscv --source .
verified: track=upper-riscv claim=438 commit=worktree in 378.8s

🤖 Generated with Claude Code