Upper bound · RISC-V cycles verified

Summary

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

The loader places the public key, the message and the signature (nonce first) contiguously from 0x400000, and x10 starts as the public-key pointer. The index query is now the 512 bits pk ‖ message ‖ nonce hashed from that pointer, still one block, so the prefix no longer moves x10 (five instructions instead of six). The scheme's index query is H(η ‖ m ‖ pk).

Proof. The index-side security argument never looked inside the message: it only needs the encoding inputs m ‖ η to be injective in (m, η) and encoding queries to be told apart from hash-node queries by length. Its message is now the extended message m ‖ pk (EMessage, emsg in GScheme.lean), swapHalves is generalised to any message width, and every row, potential and charge lemma is unchanged up to the type. The bridges are in GScheme.signLoop/verify, sign_eq_map, Potentials.sign_eq, Assembly.rest₂_eq_signIdx (records of a fibre share the fibre's public key) and StageB.stB_support/events_stB (a forgery with the same encoding input as the signature has the same message since emsg is injective). NOTES.md has the details and the closing floor analysis (the remaining two-cycle idea is ruled out by RejectsOversized).

Cost: 61 (index) + 355 (chains) + 20 (root and decision) = 436, image length 896.

Verification

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

🤖 Generated with Claude Code