chore: bump certified verifier to lean4:v4.34.0 and latest

[stephenh-axiom-xyz]

Resolves INT-9471.

Summary

Update the certified verifier to the finalized recursion statement on ws-fv's main branch. Refresh the generated C and Rust integration together so certified verification uses the split executable baseline and updated upstream wire format.

openvm-certified-verifier

• Re-extract csrc/ from the vm_verify and vm_dump_proof link closures using leanprover/lean4:v4.34.0.
• Update build.rs and the C adapter for the new Lean toolchain and generated symbol names.
• Encode VerificationBaseline.program_commit, initial_state, and initial_pc individually instead of recomputing app_exe_commit().
• Encode WHIR proximity strategies and symbolic degree_multiple metadata as required by the new decoder, and support Entry::Challenge.
• Remove the obsolete afterChallenge placeholder and duplicated symbolic layout fields.
• Update wire round-trip tests, covering all proximity strategies and noncanonical values in each split baseline field.

CI

• Update WS_FV_REV and the shared Lean toolchain action.
• Adapt check_certified_verifier_c.sh to Lake's nested build-trace inputs.

Validation

The following checks passed with the temporary v4.34.0-rc2 toolchain and must be rerun after updating to v4.34.0:

• Built upstream vm_verify and vm_dump_proof; verified that vendored C matches their generated link closures byte-for-byte.
• Passed all 30 certified-verifier tests and both SDK certified-verifier tests with CUDA.
• Built cargo-openvm with cuda,certified-verifier and passed test_cli_stark_e2e_certified.
• Passed targeted Clippy checks with -D warnings and cargo +nightly fmt --all -- --check.

[github-actions]

Code review

No issues found. Checked for bugs and CLAUDE.md compliance.

[jonathanpwang]

is this new for some reason?

[stephenh-axiom-xyz]

We made the Lean vk match the Rust one at some point, which included removing some Lean fields and adding some Rust fields (like Whir proximity strategy)

[jonathanpwang]

LGTM except not sure why there was a change in the WHIR test

[github-actions]

group	app.proof_time_ms	app.cycles	leaf.proof_time_ms
fibonacci	(-19 [-1.1%]) 1,669	12,000,265	(-3 [-0.8%]) 369
keccak	(-190 [-1.9%]) 9,563	18,655,329	(-20 [-1.3%]) 1,536
sha2_bench	(+13 [+0.2%]) 5,259	14,793,960	(-2 [-0.3%]) 588
regex	(-16 [-2.3%]) 683	4,137,067	(+6 [+2.8%]) 221
ecrecover	(-5 [-1.1%]) 439	123,583	(-4 [-2.1%]) 189
pairing	(-17 [-2.9%]) 563	1,745,757	196
kitchen_sink	(+32 [+1.4%]) 2,315	2,579,903	(+9 [+1.8%]) 499

Note: cells_used metrics omitted because CUDA tracegen does not expose unpadded trace heights.

Commit: 2a94f29

Benchmark Workflow