fix: Validate length of proof.commit_phase_commits (#1468)

The length of `proof.commit_phase_commits` is not validated and
[here](https://github.com/openvm-org/openvm/blob/18096f4194b76b743463c0fb39955f24d010e9bf/extensions/native/recursion/src/fri/two_adic_pcs.rs#L125)
we directly use it as the maximum log trace height.

close INT-3646

Author: nyunyunyunyu

extensions/native/recursion/src/commit.rs

@@ -54,6 +54,7 @@ pub trait PcsVariable<C: Config> {
         builder: &mut Builder<C>,
         rounds: Array<C, TwoAdicPcsRoundVariable<C>>,
         proof: Self::Proof,
+        log_max_height: RVar<C::N>,
         challenger: &mut impl ChallengerVariable<C>,
     );
 }

extensions/native/recursion/src/fri/mod.rs

@@ -39,22 +39,23 @@ pub fn verify_query<C: Config>(
     proof: &FriQueryProofVariable<C>,
     betas: &Array<C, Ext<C::F, C::EF>>,
     reduced_openings: &Array<C, Ext<C::F, C::EF>>,
-    log_max_height: RVar<C::N>,
+    log_max_lde_height: RVar<C::N>,
 ) -> Ext<C::F, C::EF>
 where
     C::F: TwoAdicField,
     C::EF: TwoAdicField,
 {
     builder.cycle_tracker_start("verify-query");
     let folded_eval: Ext<C::F, C::EF> = builder.eval(C::F::ZERO);
-    let two_adic_generator_f = config.get_two_adic_generator(builder, log_max_height);
+    let two_adic_generator_f = config.get_two_adic_generator(builder, log_max_lde_height);
 
     let two_adic_gen_ext = two_adic_generator_f.to_operand().symbolic();
     let two_adic_generator_ef: Ext<_, _> = builder.eval(two_adic_gen_ext);
 
-    let index_bits_truncated = index_bits.slice(builder, 0, log_max_height);
+    let index_bits_truncated = index_bits.slice(builder, 0, log_max_lde_height);
     let x = builder.exp_bits_big_endian(two_adic_generator_ef, &index_bits_truncated);
 
+    // proof.commit_phase_openings.len() == log_max_lde_height - log_blowup
     builder.assert_usize_eq(
         proof.commit_phase_openings.len(),
         commit_phase_commits.len(),
@@ -63,12 +64,13 @@ where
         .range(0, commit_phase_commits.len())
         .for_each(|i_vec, builder| {
             let i = i_vec[0];
-            let log_folded_height = builder.eval_expr(log_max_height - i - C::N::ONE);
+            let log_folded_height = builder.eval_expr(log_max_lde_height - i - C::N::ONE);
             let log_folded_height_plus_one = builder.eval_expr(log_folded_height + C::N::ONE);
             let commit = builder.get(commit_phase_commits, i);
             let step = builder.get(&proof.commit_phase_openings, i);
             let beta = builder.get(betas, i);
 
+            // reduced_openings.len() == MAX_TWO_ADICITY >= log_max_lde_height >= log_folded_height_plus_one
             let reduced_opening = builder.get(reduced_openings, log_folded_height_plus_one);
             builder.assign(&folded_eval, folded_eval + reduced_opening);
 

extensions/native/recursion/src/fri/two_adic_pcs.rs

@@ -25,6 +25,7 @@ pub const MAX_TWO_ADICITY: usize = 27;
 /// 1. FieldMerkleTreeMMCS sorts traces by height in descending order when committing data.
 /// 2. **Required** that `C::F` has two-adicity <= [MAX_TWO_ADICITY]. In particular this implies that all LDE matrices have
 ///    `log2(lde_height) <= MAX_TWO_ADICITY`.
+/// 3. **Required** that the maximum trace height is `2^log_max_height - 1`.
 ///
 /// Reference:
 /// <https://github.com/Plonky3/Plonky3/blob/27b3127dab047e07145c38143379edec2960b3e1/merkle-tree/src/merkle_tree.rs#L53>
@@ -41,6 +42,7 @@ pub fn verify_two_adic_pcs<C: Config>(
     config: &FriConfigVariable<C>,
     rounds: Array<C, TwoAdicPcsRoundVariable<C>>,
     proof: FriProofVariable<C>,
+    log_max_height: RVar<C::N>,
     challenger: &mut impl ChallengerVariable<C>,
 ) where
     C::F: TwoAdicField,
@@ -101,7 +103,10 @@ pub fn verify_two_adic_pcs<C: Config>(
     }
 
     builder.cycle_tracker_start("stage-d-verifier-verify");
-    let betas: Array<C, Ext<C::F, C::EF>> = builder.array(proof.commit_phase_commits.len());
+    // **ATTENTION**: always check shape of user inputs.
+    builder.assert_usize_eq(proof.query_proofs.len(), RVar::from(config.num_queries));
+    builder.assert_usize_eq(proof.commit_phase_commits.len(), log_max_height);
+    let betas: Array<C, Ext<C::F, C::EF>> = builder.array(log_max_height);
     iter_zip!(builder, proof.commit_phase_commits, betas).for_each(|ptr_vec, builder| {
         let comm_ptr = ptr_vec[0];
         let beta_ptr = ptr_vec[1];
@@ -117,16 +122,12 @@ pub fn verify_two_adic_pcs<C: Config>(
         challenger.observe_slice(builder, final_poly_elem_felts);
     });
 
-    // **ATTENTION**: always check shape of user inputs.
-    builder.assert_usize_eq(proof.query_proofs.len(), RVar::from(config.num_queries));
-
     challenger.check_witness(builder, config.proof_of_work_bits, proof.pow_witness);
 
-    let log_max_height =
-        builder.eval_expr(proof.commit_phase_commits.len() + RVar::from(log_blowup));
+    let log_max_lde_height = builder.eval_expr(log_max_height + RVar::from(log_blowup));
     // tag_exp is a shared buffer.
-    let tag_exp: Array<C, Felt<C::F>> = builder.array(log_max_height);
-    let w = config.get_two_adic_generator(builder, log_max_height);
+    let tag_exp: Array<C, Felt<C::F>> = builder.array(log_max_lde_height);
+    let w = config.get_two_adic_generator(builder, log_max_lde_height);
     let max_gen_pow = config.get_two_adic_generator(builder, 1);
     let one_var: Felt<C::F> = builder.eval(C::F::ONE);
 
@@ -154,7 +155,7 @@ pub fn verify_two_adic_pcs<C: Config>(
 
     iter_zip!(builder, proof.query_proofs).for_each(|ptr_vec, builder| {
         let query_proof = builder.iter_ptr_get(&proof.query_proofs, ptr_vec[0]);
-        let index_bits = challenger.sample_bits(builder, log_max_height);
+        let index_bits = challenger.sample_bits(builder, log_max_lde_height);
 
         // We reset the reduced opening accumulators at the start of each query.
         // We describe what `ro[log_height]` computes per query in pseduo-code, where `log_height` is log2 of the size of the LDE domain:
@@ -199,7 +200,7 @@ pub fn verify_two_adic_pcs<C: Config>(
         builder.cycle_tracker_start("cache-generator-powers");
         {
             // truncate index_bits to log_max_height
-            let index_bits_truncated = index_bits.slice(builder, 0, log_max_height);
+            let index_bits_truncated = index_bits.slice(builder, 0, log_max_lde_height);
 
             // b = index_bits
             // w = generator of order 2^log_max_height
@@ -262,7 +263,7 @@ pub fn verify_two_adic_pcs<C: Config>(
                     let cur_alpha_pow = builder.get(&alpha_pow, log_height);
 
                     builder.cycle_tracker_start("exp-reverse-bits-len");
-                    let height_idx = builder.eval_expr(log_max_height - log_height);
+                    let height_idx = builder.eval_expr(log_max_lde_height - log_height);
                     let x = builder.get(&tag_exp, height_idx);
                     builder.cycle_tracker_end("exp-reverse-bits-len");
 
@@ -317,7 +318,8 @@ pub fn verify_two_adic_pcs<C: Config>(
                 });
                 builder.cycle_tracker_end("compute-reduced-opening");
 
-                let bits_reduced: Usize<_> = builder.eval(log_max_height - log_batch_max_height);
+                let bits_reduced: Usize<_> =
+                    builder.eval(log_max_lde_height - log_batch_max_height);
                 let index_bits_shifted_v1 = index_bits.shift(builder, bits_reduced);
 
                 builder.cycle_tracker_start("verify-batch");
@@ -341,7 +343,7 @@ pub fn verify_two_adic_pcs<C: Config>(
             &query_proof,
             &betas,
             &ro,
-            log_max_height,
+            log_max_lde_height,
         );
 
         builder.assert_ext_eq(folded_eval, final_poly_ct);
@@ -435,9 +437,17 @@ where
         builder: &mut Builder<C>,
         rounds: Array<C, TwoAdicPcsRoundVariable<C>>,
         proof: Self::Proof,
+        log_max_height: RVar<C::N>,
         challenger: &mut impl ChallengerVariable<C>,
     ) {
-        verify_two_adic_pcs(builder, &self.config, rounds, proof, challenger)
+        verify_two_adic_pcs(
+            builder,
+            &self.config,
+            rounds,
+            proof,
+            log_max_height,
+            challenger,
+        )
     }
 }
 
@@ -691,7 +701,13 @@ pub mod tests {
         let commit = DigestVariable::Felt(builder.constant::<Array<_, _>>(commit));
         challenger.observe_digest(&mut builder, commit);
         challenger.sample_ext(&mut builder);
-        pcs_var.verify(&mut builder, rounds, proofvar, &mut challenger);
+        pcs_var.verify(
+            &mut builder,
+            rounds,
+            proofvar,
+            RVar::from(nb_log2_rows),
+            &mut challenger,
+        );
         builder.halt();
 
         let program = builder.compile_isa();

extensions/native/recursion/src/stark/mod.rs

@@ -200,6 +200,12 @@ where
         };
         // (T02a): `air_perm_by_height` is a valid permutation of `0..num_airs`.
         // (T02b): For all `i`, `air_proofs[i].log_degree <= MAX_TWO_ADICITY - log_blowup`.
+        // (T02c): For all `0<=i<num_air-1`, `air_proofs[air_perm_by_height[i]].log_degree >= air_proofs[air_perm_by_height[i+1]].log_degree`.
+        let log_max_height = {
+            let index = builder.get(air_perm_by_height, RVar::zero());
+            let air_proof = builder.get(air_proofs, index);
+            RVar::from(air_proof.log_degree.clone())
+        };
 
         // OK: trace_height_constraint_system comes from vkey so requirements of
         // `check_trace_height_constraints` are met.
@@ -375,7 +381,7 @@ where
                 RVar::from(builder.sll::<Usize<_>>(RVar::one(), log_quotient_degree));
             let log_quotient_size = builder.eval_expr(log_degree + log_quotient_degree);
             // Assumption: (T02b) `log_degree <= MAX_TWO_ADICITY - low_blowup`
-            // Because the VK ensures `log_quotient_degree < log_blowup`, this won't access an out
+            // Because the VK ensures `log_quotient_degree <= log_blowup`, this won't access an out
             // of bound index.
             let quotient_domain =
                 domain.create_disjoint_domain(builder, log_quotient_size, Some(pcs.config.clone()));
@@ -683,7 +689,13 @@ where
 
         // Verify the pcs proof
         builder.cycle_tracker_start("stage-d-verify-pcs");
-        pcs.verify(builder, rounds, opening.proof.clone(), challenger);
+        pcs.verify(
+            builder,
+            rounds,
+            opening.proof.clone(),
+            log_max_height,
+            challenger,
+        );
         builder.cycle_tracker_end("stage-d-verify-pcs");
 
         builder.cycle_tracker_start("stage-e-verify-constraints");