upper-riscv: 394 cycles — paired dispatch

Follows the 426 root of PR #20 (now on main).

The 426 image pays a four-instruction prologue per chain: advance the input pointer, point the answer buffer, load the dispatch halfword, jump. Two chains can share one jump if the code the jump lands in already knows both disclosed positions — which it does if the block is replicated, one copy per value of the second chain's digit.

Block q < 12 serves chains 2q (five-bit digit dA) and 2q + 1 (four-bit digit dB). Both digits sit in one 16-bit lane of the index answer (lane bits 2 … 6 and 10 … 13), so one mask leaves 4 · dA + 1024 · dB in the lane and the stored halfword base − 4 dA − 1024 dB is a complete dispatch address: 1024 dB picks one of sixteen 64-instruction copies of the pair's block, 4 dA picks the hash step in the copy's 32-step table for chain 2q. A copy runs dA + 1 hashes of chain 2q, two pointer moves, dB + 1 hashes of chain 2q + 1, then the next block's prologue — 8 + dA + dB cycles against 10 + dA + dB for two single blocks. The twelve four-bit digits of the 16 × 5 + 12 × 4 profile are exactly the twelve coarse digits; chains 24–27 keep single tables.

• Chains 355 → 331 (twelve pairs at 6 fixed cycles, four singles at 4, 243 hashes).
• Index 51 → 43 (four lane words instead of seven, plus a four-instruction fold that adds the coarse sums onto the fine ones before the one-MUL sum check).
• Root and decision 20, unchanged.

43 + 331 + 20 = 394, image length 12494 (50080 bytes: 12288 instructions are the copies). The scheme changes only in where pack reads the 28 digits (wid/jw in Valid.lean); the chain graph, availability count and security argument are untouched. NOTES.md records the design and the dead ends: 5 + 5 pairs need 32 copies × 14 pairs and overflow the 16-bit dispatch halfword's reach, fourteen 5 + 4 pairs fail the availability count, and the switch's two cycles are forced by the hash call reading its pointers from x10/x12.

Official verifier, from the root of this checkout on macOS (unsandboxed, comparator shim), core 20c5b5d:

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

The branch is rebased on main so .contract matches the submissions repository's pin; the PR changes only formal/Submissions/UpperRiscv/. Axioms of the exported declarations: propext, Classical.choice, Quot.sound (checked by #guard_msgs in Verifier.lean and Candidate.lean).

🤖 Generated with Claude Code