[dhsorens]

Stacked on #2: Scaled, the table the verifier multiplies a fixed factor through, computes the product, so eq_kernel's theorems now cover points of up to 31 coordinates (they stopped at 8, below which eq_kernel multiplies without the table). The folds of #1 and #2 inherit the wider bound.

What is proved

In crates/verifier/proofs/verifier/lean/Verifier/Verification/:

• Field/Window.lean, on bits:
  • ofBitVec_timesX: Scaled::new's times_x multiplies by x.
  • ofBitVec_eq_sum: a word is the sum of the powers of x its bits stand for.
  • sum_win: a word is the sum of its eleven six-bit windows, each window's bits weighed by their powers of x.
• Scaled.lean:
  • new_spec: entry idx of Scaled::new(r) is window idx % 704 / 64's value idx % 64 times r y^(idx / 704), proved loop by loop (bits, windows, limbs).
  • mul_spec and scaled_mul: Scaled::new(r) then mul(a) is a * r.
• EqKernel.lean: scaler_new_spec (a Scaler multiplies by its factor, through the table or not); eq_kernel_spec, level0_fold, deeper_fold now take point.length ≤ 31, the most for which 1 << len fits a 32-bit usize.
• Std.lean: loop_range_spec_result, hax's range-loop rule for a loop whose result is not its state.

Axioms: Lean's three, the field proofs' bv_decide certificates, and one more of the same kind for timesX_eq.

Patch

09-scaled-limbs-by-index.patch (pre-extraction only) indexes Scaled::mul's three limbs over a range instead of iterating the array. The verifier's tests and the real-proof suite pass on the patched source.

Bug hunting

No bug found. Scaled's last window tabulates multiples by x^64 and x^65 it never reads (a limb's top window holds four bits); scaled_mul confirms the lookups land only on the rest. Checked that no prover-announced length reaches eq_kernel unbounded: the Keccak shape's depth is the constant KECCAK_DEPTH in execution proofs and is required to divide ROUNDS in verify_keccak_batch, so segments() neither divides by zero nor underflows; the other call sites take fixed lengths or ones the announced-size checks bound.

Warnings

14, as on #1.