[dhsorens]

Stacked on #1: the WHIR fold of a queried row past level 0, dot(ext_row(row), eq_kernel(r)), is ArkLib's multilinearCombine at r of the row's lanes. With #1's level0_fold this covers the verifier's fold at every level.

What is proved

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

• Dot.lean:
  • dot_spec: the extracted dot of equal-length slices is the sum of products in Ext3.
  • ext_row_spec: ext_row regroups a row's words three to a lane (wordsE).
  • deeper_fold: given eq_kernel's output, dot(ext_row(row), weights) of a row of 3 · 2^n words is multilinearCombine (extLanes row n) r (), lane i being the extension element of words 3i, 3i + 1, 3i + 2.
• Std.lean: hax triples for Vec::new and Vec::push.

deeper_fold rests on the same axioms as level0_fold: Lean's three and the field proofs' bv_decide certificates, no opaque item's assumption.

Patch

08-dot-by-index.patch (pre-extraction only) writes dot's loop over indices instead of a zip of slice iterators. The verifier's tests and the real-proof suite (-p leanvm_core --test verifiers) pass on the patched source.

Bug hunting

No bug found on this path. Checked that a prover cannot trip the preconditions the proofs need: every row reaching ext_row and dot has the length the verifier fixes (the raw form reads exactly leaf_words, the pruned form's expand requires it), folds are at most 6, within eq_kernel_spec's bound of 8, and the pruned openings come back in query order, duplicates included. Also revisited the raw form's unchecked level-0 lanes past n_lanes (the pruned form forces them to zero): by argument, not by a test, they cannot move a claim, since evaluate_basis is a batch of the stack claims' weights, each of which should be zero outside its slot. Confirming that last step for every claim kind is an open item.

Warnings

14, as on #1.