Upper bound · RISC-V cycles verified

Lowers the RISC-V cycle claim from 702 to 696 by reducing the accepted-index nibble sum target from 160 to 157. The scheme, graph, machine image layout, signature format and the entire security development are unchanged.

Why 160 was not minimal

Verification hashes nibble k times in chain k, and an index is accepted iff its 32 nibbles sum to target, so every unit of target costs exactly two cycles. The only constraint on target is signing availability: (1 - comp(32,target)/2^128)^(2^20) <= 2^-128.

Availability.lean bounded that with the rational Bernoulli inequality (1-p)^k <= 1/(1+k*p), applied once to a block of 8192 trials to get miss^8192 <= 1/2 and then 2^-128 from 128 blocks. Used that way it needs 2^20 * p >= 128, i.e. comp(32,target) >= 2^115, whose least solution is exactly 160. The one-shot application throws away a factor ln 2 ≈ 1.4427, because (1-p)^(1/p) <= e^-1 rather than 1/2.

The fix

Keep the compounding inside ℚ instead of recovering e: apply the same lemma to 128 trials, then raise to the 64th power.

miss^8192 = (miss^128)^64 <= (1/(1 + 128p))^64 = (8388608/8481920)^64 <= 1/2

the last step because (8481920/8388608)^64 ≈ 2.0298 > 2 (a 260-digit norm_num check). This needs only p >= 729/2^23.

comp 32 157 = 30465700825049557482282408820464096 ≈ 2^114.55, kernel-checked through the existing compTable dynamic program, clearing the 729*2^105 threshold by about 3%. 157 is exactly minimal: comp 32 156 gives failure about 2^-119, above the allowance. True failure at 157 is about 2^-135.

Reducing the count only helps security — RowHyp asks for 2 <= numValid and 2*numValid <= 2^128 — so Potentials.lean needed one literal changed and no new argument.

Diff

target, its kernel-computed count, the two availability lemmas, the machine's sum-check immediate (XORI x27, x27, 1280 → 1256, since the lane sum carries 8·Σ), and the cost bookkeeping: chain cycles 608 → 602, compressions 172 → 169 and 173 → 170, cycleBound 702 → 696.

NOTES.md records the full cycle decomposition (382 instruction cycles vs 314 hash cycles), the (C, w, N) parameter optimisation showing C = 32, N = 157 is the optimum of that family, and the next lever I costed but did not take: rebasing the chain prologue on x10 with header tweak slotAddr k - 8 removes one instruction from each of the 32 prologues, worth 32 more cycles.

Verification

$ python3 .contract/verifier/verify.py upper-riscv --source .
verified: track=upper-riscv claim=696

(248 s; exported certificate : submission.Certificate 696 depends only on propext, Classical.choice, Quot.sound.)

🤖 Generated with Claude Code