Derive the public-input limb claims instead of transmitting them

[scaraven]

Summary

In the public-input round the prover used to send c_0, c_1, the evaluations of the two low memory limbs at (r_pi, 0, ..., 0), which the verifier checked against the public-input line. Both are lines through the public input's own limbs, so the verifier now computes them: limb i claims interp_k(pi[0].c_i, pi[1].c_i, r_pi), and nothing is transmitted. The proof stream is two scalars shorter, and the recursive guest drops two BLAKE2s compressions per verified child.

Fiat-Shamir

• r_pi is still squeezed at the same position (after the commitment and the table sumcheck, before flock), so the committed memory cannot depend on it, and the squeeze ratchets the state for every later challenge.
• The claim values are functions of the public input, which seeds the transcript, and of r_pi, so they are fixed before the opening's batching challenge. Nothing new needs absorbing.
• The verifier still rejects a public input with a nonzero top limb, so the limbs the claims use are exactly the ones the seed binds.

Changes (all three verifiers move together)

• Rust (crates/leanvm_core/src/cpu/mod.rs): bind_pi_claim computes the limb lines from the layout's public input on both sides. The prover's two add_scalar calls, the verifier's two next_scalar reads and the line check are gone.
• Python (python-verifier/verifier.py): step 5 evaluates the limb lines; the unused Y constant is removed.
• Guest (crates/rec_aggregation/guests/lean_ethereum.py): new canonical_limbs hints each public word's low limb and binds both limbs with assert_in_k (unique tower representation, top limb forced zero), replacing two fs_next absorbs and the reassembly assert.
• Spec (doc/leanvm/body/08-end-to-end-protocol.tex, sec:e2e-pi) and the comments that said every pooled claim value rode the stream.

Tests

• New vm_proofs::a_proof_binds_the_memory_to_the_public_input: a forging prover (prove_claiming, #[doc(hidden)]) runs on the real input but seeds its transcript with another, and the opening must reject it, for a low-limb and a high-limb difference. Mutation-checked: with the public-input claims removed from finish_claims this test fails, while every honest-prover test still passes.
• cargo test --release --workspace passes, including aggregate_two_to_one, public_api_end_to_end and the Python verifier test. On a 15 GB machine rec_aggregation needs --test-threads=1 to avoid an OOM kill. cargo clippyall, cargo docall, cargo fmt --check and ruff are clean.
• An adversarial review found no critical or major issues; its minor findings (stale comments, doc wording, the test gap above) are addressed.

Base branch

leanvm-main is leanEthereum/leanVM main at 248da071, pushed so this PR shows only this change; the fork's main has diverged from leanVM.