fix(soundness): bound untrusted num_instances in recursion verifier

Companion to the native-verifier bound. The native verifier rejects any
num_instances entry (and their sum) exceeding 2^MAX_NUM_VARIABLES and derives
log2_num_instances from those bounded counts. The recursion verifier reads
sum_num_instances and log2_num_instances as untrusted hints without bounding
them, so a crafted proof could drive pow_2(log2_num_instances) past the field
size and wrap the next_pow2 - sum offset, verifying a different statement than
the native verifier.

verify_chip_proof_pre_main now bounds log2_num_instances <= MAX_NUM_VARIABLES and
sum_num_instances / each num_instances[i] <= 2^MAX_NUM_VARIABLES before they are
used. Valid proofs are always within this bound, so only malformed proofs are
rejected; native and recursion stay in lockstep.

Validated: cargo check / clippy clean; aggregation e2e over multi-shard
keccak_syscall verifies (leaf proofs run the asserts for every chip, valid
proofs are not rejected).

Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>

Author: spherel

ceno_recursion/src/zkvm_verifier/verifier.rs

@@ -29,7 +29,10 @@ use crate::{
         SepticExtensionVariable, SepticPointVariable, SumcheckLayerProofVariable,
     },
 };
-use ceno_zkvm::structs::{ComposedConstrainSystem, VerifyingKey, ZKVMVerifyingKey};
+use ceno_zkvm::{
+    scheme::constants::MAX_NUM_VARIABLES,
+    structs::{ComposedConstrainSystem, VerifyingKey, ZKVMVerifyingKey},
+};
 use ff_ext::BabyBearExt4;
 
 use crate::transcript::{challenger_add_forked_index, clone_challenger_state};
@@ -613,6 +616,28 @@ pub fn verify_chip_proof_pre_main<C: Config>(
     let lk_counts_per_instance: Usize<C::N> = Usize::from(lk_len);
     let num_batched: Usize<C::N> = Usize::from(num_batched);
 
+    // Bound the untrusted instance-count hints before they feed
+    // `pow_2(log2_num_instances)` and the `next_pow2 - sum` offset, so a crafted
+    // proof cannot overflow the field. Valid proofs are always within
+    // `2^MAX_NUM_VARIABLES`.
+    builder.assert_less_than_slow_small_rhs(
+        chip_proof.log2_num_instances.get_var(),
+        RVar::from(MAX_NUM_VARIABLES + 1),
+    );
+    let max_instances_plus_one: Var<C::N> = builder.eval(C::N::from_canonical_usize(
+        (1usize << MAX_NUM_VARIABLES) + 1,
+    ));
+    builder.assert_less_than_slow_bit_decomp(
+        chip_proof.sum_num_instances.get_var(),
+        max_instances_plus_one,
+    );
+    builder
+        .range(0, chip_proof.num_instances.len())
+        .for_each(|idx_vec, builder| {
+            let n = builder.get(&chip_proof.num_instances, idx_vec[0]);
+            builder.assert_less_than_slow_bit_decomp(n, max_instances_plus_one);
+        });
+
     let log2_num_instances = chip_proof.log2_num_instances.clone();
     if composed_cs.has_ecc_ops() {
         builder.assign(