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 715.7s

The root also exports the new image_size : submission.image.byteSize < 1048576 required by core b38f3c5 (4 · 886 + 80 = 3624 bytes); the first push of this PR predated that requirement and was rejected at the export step. 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