Upper bound · RISC-V cycles verified

Current head: 694 cycles. The first head (696) lowered the nibble-sum target; the second head takes two more instructions out of the root and decision phases with the scheme unchanged: the root length is one ADDI x11, x13, 1856 from the checked signature length still in x13, and the decision branches on each mismatching word (BNE) to a reject stub after the accepting HALT (7 cycles on every path instead of 8). verified: track=upper-riscv claim=694 locally.

---

First head: 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 an audit of every remaining instruction block. (Correction to an earlier revision of these notes: the chain prologue is not reducible by rebasing on one pointer — the HASH ABI reads at x10 and writes 32 bytes at x12, so both pointers are forced. The one large lever left is removing the per-step level tag, worth 157 cycles, which requires restructuring the tagNat query→node map in Names.lean.)

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