Venus v0.3.2

Venus v0.3.2

Summary

Venus v0.3.2 is a security release. It binds the public inputs of every recursion layer to the proven trace, closes a null-slot gap in the final aggregation circuit, completes the ArithEq result range checks, anchors in-guest proof verification to a trusted verification key, and ports a broad set of prover, emulator and loader hardening fixes. It also fixes the Arith planner panic reported in #1.

Proving keys must be regenerated, and proofs produced by earlier versions are not accepted by the new verifiers.

Security Fixes

Recursion publics binding

The recursion AIRs (compressor, recursive1, recursive2 and vadcop_final) did not constrain their public inputs to any trace cell, so a prover could claim arbitrary aggregated public values, including the final outputs. Each public is now placed in a dedicated trace row that copy constraints tie to the verifier circuit's public signal, and one constraint per connection column binds that cell to publics[k]. The public rows are selected through a binary-encoded row index held in fixed columns, so 18 public rows cost 5 fixed columns.

To keep recursive2 within 2^17 rows, recursion grinding increases from 20 to 23 bits (73 to 71 FRI queries) at the same 128-bit security target.

Null slot in vadcop_final

A null child (circuit type 0) skipped its STARK verification while its stage-1 hash and airgroup values still fed the global constraints, and the count of aggregated proofs was discarded, so a final proof could aggregate no proof at all. Null slots are now masked to zero, and at least one aggregated proof is required.

ArithEq range checks

• The x3/y3 less-than-prime chains must end at 1 on the last clock, so a non-reduced result is rejected. Upstream ZisK v0.18.0 closes the same gap.
• In arith256_mod and arith384_mod, the high part of q1 * y2 could carry into the next operation's equation. It is now constrained to zero.
• The ArithEq384 operation selector now latches for the whole cycle.

Other constraint fixes

• The global enable_* flags lacked === 0 and were therefore not constrained to be boolean.
• DMA: the last 64-bit aligned segment must close its sequence, and the extended count selector is bound.
• Signed DIV quotient sign, BLAKE2b high limbs, and MemAlign timestamps and zero extension are constrained.

Native verifiers

The native verifiers for recursive2, vadcop_final and vadcop_final_compressed are now derived by the proving-key setup (make generate-rust-verifiers; check-rust-verifiers runs in setup and verify) and reject proofs with an unexpected number of publics. make generate-key-js is removed, because the upstream JavaScript recursion templates leave publics unbound.

In-guest proof verification

ziskos::io::verify_zisk_proof took the vadcop_final verification key from the trailing bytes of the proof itself, so a guest accepted proofs made with any self-built setup. It now requires a trusted final verification key and parses the publics exactly before running the STARK verifier. The new verify_zisk_proof_with_publics and verify_zisk_proof_for_program return the authenticated program key and public outputs, and the aggregation example checks both keys.

Recursive witness runtime

The native recursive witness runtime rejects Circom main inputs that the compiler replaced with constants or non-direct expressions, and it checks inputs that were equated, instead of silently overwriting witness words. The runtime descriptor (.dat) moves to format version 5 with bounded parsing. Loading a legacy <setup>.so witness library, which executes host code, now requires PROOFMAN_ALLOW_UNSAFE_RECURSIVE_SO=1.

Prover, loader and emulator hardening

• Proof-shape metadata (starkinfo, expressions bins, global info and exec files) is validated when a setup is loaded, and global constraint operands and hint lookups are bounds-checked.
• Untrusted inputs are bounded: proof files (512 MiB), ELF files (512 MiB, with at most 1 GiB of loaded sections), hint streams (64 MiB, 4 MiB per hint) and stdin (the input region size). Assembly emulator shared-memory accesses are bounds-checked.
• Unsafe vector and trace buffer ownership conversions, FFI buffer sizes, and BN254/BLS12-381 hint pair counts are checked.
• The ProofMan reset lifecycle and ready-stream reuse are fixed. Stream selection no longer reads past the per-GPU array, and direct-stream proof collection is now locked. The RecursiveF GPU buffer was 8x too small.

Bug Fixes

• #1: an Arith instance planned only for frequent operations no longer panics with chunk_size must not be zero.
• DIVW(INT_MIN, -1) now returns the sign-extended result that the Arith AIR expects, so such programs can be proven, and the assembly emulator no longer raises SIGFPE on it.
• The MemModule collector compared word addresses against a byte bound.

Performance

Proof time on the same RTX 5090 machine, v0.3.1 against v0.3.2:

Ethereum mainnet block	v0.3.1	v0.3.2	Change
24628607 (66 txs, ~7 Mgas)	17.715s	18.051s	+0.336s (1.9%)
24628590 (478 txs, ~49 Mgas)	77.115s	78.650s	+1.535s (2.0%)

The difference is the cost of the soundness fixes. Binding 473 publics adds about 1,200 operations to the recursion constraint polynomial, and recursion grinding rises to 23 bits. The generated GPU evaluators for the changed recursion expressions are regenerated as single kernels, which recovers most of the remaining cost.

Compatibility

• Proving keys must be regenerated; make setup does this automatically. Proofs from earlier versions are rejected.
• API change: ziskos::io::verify_zisk_proof(proof, expected_vadcop_final_vk) now takes the trusted final verification key.
• Removed: make generate-key-js, the proofman-cli gen-witness command and the Circom WASM witness path.
• New input size limits, as listed above.