upper-riscv: 364 cycles — ascending cell grid

Follows the 372 root of PR #27 (now on main).

The 372 image expands 24 of its 32 chains — one ADDI x10, x12, 8 after the first hash of every chain whose wire value is not already in its 24-byte working cell — because only the eight 192-bit chains at the bottom of the payload sit on the cell grid: the wide chains run upwards from the payload base, the narrow ones are relocated downwards from the top, and the two families meet at a 16-byte junction that also costs two full 256-bit root slices.

Here all 32 cells are 0x3FFFE0 + 24k in execution order and every chain runs upwards. A chain is free of the expansion exactly when its wire block starts at its own cell, and a wire block survives until it is read exactly when it lies at or above its own cell (wireSlot k ≥ slot k), since the earlier writes cover only the cells below. That leaves the wire order free, and the 672-byte budget — 28 cells — fits sixteen on-grid chains: twelve 192-bit chains stored in place plus four 96-byte blocks, each holding one 152-bit chain on the grid followed by one 160-bit and three 152-bit chains that are relocated to the cells below it. Payload.index/coindex are the two directions of this permutation (no longer an involution), checked inverse by kernel decision.

• Chains 310 → 303: 16 redirects instead of 24, two width changes (160 → 152 at pair 2, 152 → 192 at pair 10) instead of one; 189 hashes, 64 pointer instructions and 32 dispatch instructions unchanged.
• Root and decision 22 → 21: the root reads the low 192 bits of every cell as one 768-byte region, 6144 bits = 12 compression blocks instead of the 6272-bit / 13-block input with two boundary tops.
• Index phase 40, unchanged; the dispatch halfwords move from 0x3FFFE0 to 0x4002E0, just above the signature buffer.

40 + 303 + 21 = 364, image length 12340 (49464 bytes). Rows are [12,1,8] / [13,9,4] / [14,10,6] / [11,0,15] / [3,5,2] / [7]; the four pairs with an on-grid left chain and a relocated right chain (41 instructions) and the final pair (47) take the 48-instruction slots, and pairs 12–15 again reuse the third dispatch word's base constants.

The scheme changes are the state widths (four 160-bit, sixteen 152-bit, twelve 192-bit; still 5376 bits), the 6144-bit root and the wire permutation. At 152 bits the bad-record weight is δ = 2·1025²·2⁻¹⁵² ≈ 0.125·2⁻¹²⁸, which the previous availability bound (numValid ≥ 712·2¹⁰⁵, spending 0.882·2⁻¹²⁸ of the signing-failure allowance) could not accommodate; the true accepted-index count at sum 157 is 751.03·2¹⁰⁵, so Valid.numValid_avail now certifies 750·2¹⁰⁵ and the miss term drops below 0.74·2⁻¹²⁸. Strong unforgeability keeps 2δ < 1036κ (keygen 1036 with the 12-block root) and verification costs 202 compressions. NOTES.md records the accounting and the dead ends: 144-bit states fail the signing-failure budget, a 12-block root is impossible with the two-directional layout, and the wire in execution order caps the on-grid chains at twelve (368 cycles).

Official verifier, from the root of this checkout on macOS (unsandboxed, comparator shim), against the trusted core da1418b:

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

The branch is based on main (9fe2362); the PR changes only formal/Submissions/UpperRiscv/. Axioms of the exported declarations: propext, Classical.choice, Quot.sound (checked by #guard_msgs in Wire.lean and Candidate.lean).

🤖 Generated with Claude Code