diff --git a/miden-air/src/air.rs b/miden-air/src/air.rs index fb87e77a3..df562e988 100644 --- a/miden-air/src/air.rs +++ b/miden-air/src/air.rs @@ -1,5 +1,12 @@ use crate::{MidenAirBuilder, RowMajorMatrix}; +pub enum BusType { + /// A multiset bus + Multiset, + /// A logup bus + Logup, +} + /// Super trait for all AIR definitions in the Miden VM ecosystem. /// /// This trait contains all methods from `BaseAir`, `BaseAirWithPublicValues`, @@ -59,6 +66,11 @@ pub trait MidenAir: Sync { 0 } + /// Types of buses + fn bus_types(&self) -> Vec { + vec![] + } + /// Build an aux trace (EF-based) given the main trace and EF challenges. /// Return None to indicate no aux or to fall back to legacy behavior. /// The output is a matrix of EF elements, flattened to a matrix of F elements. diff --git a/miden-air/src/lib.rs b/miden-air/src/lib.rs index 0f7eea882..181a20097 100644 --- a/miden-air/src/lib.rs +++ b/miden-air/src/lib.rs @@ -42,7 +42,7 @@ mod air; mod builder; mod filtered_builder; -pub use air::MidenAir; +pub use air::{BusType, MidenAir}; pub use builder::MidenAirBuilder; pub use filtered_builder::FilteredMidenAirBuilder; // Re-export for convenience diff --git a/miden-prover/src/air_wrapper_bus_boundary.rs b/miden-prover/src/air_wrapper_bus_boundary.rs new file mode 100644 index 000000000..c84e3765f --- /dev/null +++ b/miden-prover/src/air_wrapper_bus_boundary.rs @@ -0,0 +1,93 @@ +use std::marker::PhantomData; + +use miden_air::{BusType, MidenAir, MidenAirBuilder}; +use p3_field::{PrimeCharacteristicRing, TwoAdicField}; +use p3_matrix::Matrix; +use p3_matrix::dense::RowMajorMatrix; +use p3_maybe_rayon::prelude::*; + +use crate::{StarkGenericConfig, Val}; + +pub struct AirWithBoundaryConstraints<'a, SC, A> +where + SC: StarkGenericConfig + std::marker::Sync, + A: MidenAir, SC::Challenge>, + Val: TwoAdicField, +{ + pub inner: &'a A, + pub phantom: PhantomData, +} + +impl<'a, SC, A> MidenAir, SC::Challenge> for AirWithBoundaryConstraints<'a, SC, A> +where + SC: StarkGenericConfig + std::marker::Sync, + A: MidenAir, SC::Challenge>, + Val: TwoAdicField, +{ + fn width(&self) -> usize { + self.inner.width() + } + + fn preprocessed_trace(&self) -> Option>> { + self.inner.preprocessed_trace() + } + + fn num_public_values(&self) -> usize { + self.inner.num_public_values() + } + + fn periodic_table(&self) -> Vec>> { + self.inner.periodic_table() + } + + fn num_randomness(&self) -> usize { + self.inner.num_randomness() + } + + fn aux_width(&self) -> usize { + self.inner.aux_width() + } + + /// Types of buses + fn bus_types(&self) -> Vec { + self.inner.bus_types() + } + + fn build_aux_trace( + &self, + _main: &RowMajorMatrix>, + _challenges: &[SC::Challenge], + ) -> Option>> { + self.inner.build_aux_trace(_main, _challenges) + } + + fn eval>>(&self, builder: &mut AB) { + // First, apply the inner AIR's constraints + self.inner.eval(builder); + + if self.inner.num_randomness() > 0 { + // Then, apply any additional boundary constraints as needed + let aux = builder.permutation(); + let aux_current = aux.row_slice(0).unwrap(); + let aux_bus_boundary_values = builder.aux_bus_boundary_values().to_vec(); + + for (idx, bus_type) in self.inner.bus_types().into_iter().enumerate() { + match bus_type { + BusType::Multiset => { + builder + .when_first_row() + .assert_zero_ext(aux_current[idx].into() - AB::ExprEF::ONE); + } + BusType::Logup => { + builder + .when_first_row() + .assert_zero_ext(aux_current[idx].into()); + } + } + builder + .when_last_row() + .assert_zero_ext(aux_current[idx].into() - aux_bus_boundary_values[idx].into()); + } + } + } +} diff --git a/miden-prover/src/check_constraints.rs b/miden-prover/src/check_constraints.rs index e63f2c611..06357a015 100644 --- a/miden-prover/src/check_constraints.rs +++ b/miden-prover/src/check_constraints.rs @@ -72,6 +72,15 @@ pub(crate) fn check_constraints( ) }; + let aux_bus_boundary_values; + if let Some(aux_matrix) = aux_trace.as_ref() { + let aux_bus_boundary_values_base = + unsafe { aux_matrix.row_slice_unchecked(height - 1) }; + aux_bus_boundary_values = prover_row_to_ext::(&aux_bus_boundary_values_base); + } else { + aux_bus_boundary_values = vec![]; + }; + let preprocessed_pair = preprocessed.as_ref().map(|preprocessed_matrix| { let preprocessed_local = preprocessed_matrix .values @@ -109,6 +118,7 @@ pub(crate) fn check_constraints( main, aux, aux_randomness, + aux_bus_boundary_values: &aux_bus_boundary_values, preprocessed: preprocessed_pair, public_values, periodic_values, @@ -135,6 +145,8 @@ pub struct DebugConstraintBuilder<'a, F: Field, EF: ExtensionField> { aux: ViewPair<'a, EF>, /// randomness that is used to compute aux trace aux_randomness: &'a [EF], + /// Aux bus boundary values (against the last row) + aux_bus_boundary_values: &'a [EF], /// A view of the preprocessed current and next row as a vertical pair (if present). preprocessed: Option>, /// The public values provided for constraint validation (e.g. inputs or outputs). @@ -233,7 +245,7 @@ where } fn aux_bus_boundary_values(&self) -> &[Self::VarEF] { - unimplemented!() + self.aux_bus_boundary_values } fn periodic_evals(&self) -> &[Self::PeriodicVal] { diff --git a/miden-prover/src/folder.rs b/miden-prover/src/folder.rs index 1b741f790..0375d8572 100644 --- a/miden-prover/src/folder.rs +++ b/miden-prover/src/folder.rs @@ -18,6 +18,8 @@ pub struct ProverConstraintFolder<'a, SC: StarkGenericConfig> { /// The randomness used to compute the aux trace; can be zero width. /// Cached EF randomness packed from base randomness to avoid temporary leaks pub packed_randomness: Vec>, + /// Aux trace bus boundary values packed from base field to extension field + pub aux_bus_boundary_values: &'a [PackedChallenge], /// The preprocessed columns (if any) pub preprocessed: Option>>, /// Public inputs to the AIR @@ -117,7 +119,7 @@ impl<'a, SC: StarkGenericConfig> MidenAirBuilder for ProverConstraintFolder<'a, } fn aux_bus_boundary_values(&self) -> &[Self::VarEF] { - unimplemented!() + self.aux_bus_boundary_values } fn periodic_evals(&self) -> &[Self::PeriodicVal] { @@ -137,6 +139,8 @@ pub struct VerifierConstraintFolder<'a, SC: StarkGenericConfig> { pub aux: ViewPair<'a, SC::Challenge>, /// The randomness used to compute the aux tract; can be zero width. pub randomness: &'a [SC::Challenge], + /// Aux trace bus boundary values; can be zero width. + pub aux_bus_boundary_values: &'a [SC::Challenge], /// The preprocessed columns (if any) pub preprocessed: Option>, /// Public values that are inputs to the computation @@ -227,7 +231,7 @@ impl<'a, SC: StarkGenericConfig> MidenAirBuilder for VerifierConstraintFolder<'a } fn aux_bus_boundary_values(&self) -> &[Self::VarEF] { - unimplemented!() + self.aux_bus_boundary_values } fn periodic_evals(&self) -> &[Self::PeriodicVal] { diff --git a/miden-prover/src/lib.rs b/miden-prover/src/lib.rs index 7cc4c6fff..1fe8c61ff 100644 --- a/miden-prover/src/lib.rs +++ b/miden-prover/src/lib.rs @@ -1,3 +1,4 @@ +mod air_wrapper_bus_boundary; #[cfg(debug_assertions)] mod check_constraints; mod config; @@ -12,6 +13,7 @@ mod symbolic_variable; mod util; mod verifier; +pub use air_wrapper_bus_boundary::*; #[cfg(debug_assertions)] pub use check_constraints::*; pub use config::*; diff --git a/miden-prover/src/prover.rs b/miden-prover/src/prover.rs index 2d5b5bed0..7ba134263 100644 --- a/miden-prover/src/prover.rs +++ b/miden-prover/src/prover.rs @@ -1,3 +1,5 @@ +use std::marker::PhantomData; + use itertools::Itertools; use miden_air::MidenAir; use p3_challenger::{CanObserve, FieldChallenger}; @@ -12,9 +14,11 @@ use p3_util::log2_strict_usize; use tracing::{debug_span, info_span, instrument}; use crate::periodic_tables::compute_periodic_on_quotient_eval_domain; +use crate::util::prover_row_to_ext; use crate::{ - Commitments, Domain, OpenedValues, PackedChallenge, PackedVal, Proof, ProverConstraintFolder, - StarkGenericConfig, Val, get_log_quotient_degree, get_symbolic_constraints, + AirWithBoundaryConstraints, Commitments, Domain, OpenedValues, PackedChallenge, PackedVal, + Proof, ProverConstraintFolder, StarkGenericConfig, Val, get_log_quotient_degree, + get_symbolic_constraints, }; /// Commits the preprocessed trace if present. @@ -44,10 +48,15 @@ pub fn prove( public_values: &[Val], ) -> Proof where - SC: StarkGenericConfig, + SC: StarkGenericConfig + Sync, A: MidenAir, SC::Challenge>, Val: TwoAdicField, { + let air = &AirWithBoundaryConstraints { + inner: air, + phantom: PhantomData::, + }; + // Compute the height `N = 2^n` and `log_2(height)`, `n`, of the trace. let degree = trace.height(); let log_degree = log2_strict_usize(degree); @@ -104,7 +113,7 @@ where // From the degree of the constraint polynomial, compute the number // of quotient polynomials we will split Q(x) into. This is chosen to // always be a power of 2. - let log_quotient_degree = get_log_quotient_degree::, SC::Challenge, A>( + let log_quotient_degree = get_log_quotient_degree::, SC::Challenge, _>( air, preprocessed_width, public_values.len(), @@ -170,7 +179,7 @@ where // begin aux trace generation (optional) let num_randomness = air.num_randomness(); - let (aux_trace_commit_opt, _aux_trace_opt, aux_trace_data_opt, randomness) = + let (aux_trace_commit_opt, _aux_trace_opt, aux_trace_data_opt, randomness, aux_finals) = if num_randomness > 0 { let randomness: Vec = (0..num_randomness) .map(|_| challenger.sample_algebra_element()) @@ -184,19 +193,30 @@ where let aux_trace = aux_trace_opt .expect("aux_challenges > 0 but no aux trace was provided or generated"); + let aux_finals_base = aux_trace + .last_row() + .expect("aux_challenges > 0 but aux trace was empty") + .into_iter() + .collect_vec(); + let aux_finals = prover_row_to_ext(&aux_finals_base); + let (aux_trace_commit, aux_trace_data) = info_span!("commit to aux trace data") .in_scope(|| pcs.commit([(ext_trace_domain, aux_trace.clone().flatten_to_base())])); challenger.observe(aux_trace_commit.clone()); + for aux_final in &aux_finals { + challenger.observe_algebra_element(*aux_final); + } ( Some(aux_trace_commit), Some(aux_trace), Some(aux_trace_data), randomness, + aux_finals, ) } else { - (None, None, None, vec![]) + (None, None, None, vec![], vec![]) }; #[cfg(debug_assertions)] @@ -254,7 +274,7 @@ where // `C(T_1(x), ..., T_w(x), T_1(hx), ..., T_w(hx), selectors(x)) / Z_H(x)` // at every point in the quotient domain. The degree of `Q(x)` is `<= deg(C(x)) - N = 2N - 2` in the case // where `deg(C) = 3`. (See the discussion above constraint_degree for more details.) - let quotient_values: Vec = quotient_values::( + let quotient_values: Vec = quotient_values::( air, public_values, trace_domain, @@ -262,6 +282,7 @@ where &trace_on_quotient_domain, aux_trace_on_quotient_domain.as_ref(), &randomness, + &aux_finals, preprocessed_on_quotient_domain.as_ref(), alpha, constraint_count, @@ -396,6 +417,12 @@ where } else { (None, None) }; + let aux_finals = if aux_trace_data_opt.is_some() { + Some(aux_finals) + } else { + None + }; + let opened_values = OpenedValues { trace_local, trace_next, @@ -410,6 +437,7 @@ where commitments, opened_values, opening_proof, + aux_finals, degree_bits: log_ext_degree, } } @@ -425,12 +453,13 @@ pub fn quotient_values( trace_on_quotient_domain: &Mat, aux_trace_on_quotient_domain: Option<&Mat>, randomness: &[SC::Challenge], + aux_bus_boundary_values: &[SC::Challenge], preprocessed_on_quotient_domain: Option<&Mat>, alpha: SC::Challenge, constraint_count: usize, ) -> Vec where - SC: StarkGenericConfig, + SC: StarkGenericConfig + Sync, A: MidenAir, SC::Challenge>, Mat: Matrix> + Sync, Val: TwoAdicField, @@ -547,6 +576,13 @@ where let packed_randomness: Vec> = randomness.iter().copied().map(Into::into).collect(); + // Pack aux bus boundary values + let packed_aux_bus_boundary_values: Vec> = aux_bus_boundary_values + .iter() + .copied() + .map(Into::into) + .collect(); + // Grab precomputed periodic evaluations for this packed chunk. let periodic_values: Vec> = periodic_on_quotient .as_ref() @@ -575,7 +611,9 @@ where accumulator, constraint_index: 0, packed_randomness, + aux_bus_boundary_values: &packed_aux_bus_boundary_values, }; + air.eval(&mut folder); // quotient(x) = constraints(x) / Z_H(x) diff --git a/miden-prover/src/symbolic_builder.rs b/miden-prover/src/symbolic_builder.rs index a1db3599c..210fef7cc 100644 --- a/miden-prover/src/symbolic_builder.rs +++ b/miden-prover/src/symbolic_builder.rs @@ -95,6 +95,7 @@ pub struct SymbolicAirBuilder { main: RowMajorMatrix>, aux: Option>>, aux_randomness: Vec>, + aux_bus_boundary_values: Vec>, public_values: Vec>, periodic_values: Vec>, constraints: Vec>, @@ -152,6 +153,9 @@ impl SymbolicAirBuilder { None }; let randomness = Self::sample_randomness(num_randomness); + let aux_bus_boundary_values = (0..aux_width) + .map(move |index| SymbolicVariable::new(Entry::AuxBusBoundary, index)) + .collect(); let public_values = (0..num_public_values) .map(move |index| SymbolicVariable::new(Entry::Public, index)) .collect(); @@ -163,6 +167,7 @@ impl SymbolicAirBuilder { main: RowMajorMatrix::new(main_values, width), aux, aux_randomness: randomness, + aux_bus_boundary_values, public_values, periodic_values, constraints: vec![], @@ -230,7 +235,7 @@ impl MidenAirBuilder for SymbolicAirBuilder { } fn aux_bus_boundary_values(&self) -> &[Self::VarEF] { - unimplemented!() + &self.aux_bus_boundary_values } fn public_values(&self) -> &[Self::PublicVar] { diff --git a/miden-prover/src/verifier.rs b/miden-prover/src/verifier.rs index 92c207f42..8568c758e 100644 --- a/miden-prover/src/verifier.rs +++ b/miden-prover/src/verifier.rs @@ -1,7 +1,9 @@ //! See `prover.rs` for an overview of the protocol and a more detailed soundness analysis. +use std::marker::PhantomData; + use itertools::Itertools; -use miden_air::MidenAir; +use miden_air::{BusType, MidenAir}; use p3_challenger::{CanObserve, FieldChallenger}; use p3_commit::{Pcs, PolynomialSpace}; use p3_field::{BasedVectorSpace, Field, PrimeCharacteristicRing, TwoAdicField}; @@ -13,7 +15,10 @@ use tracing::{debug_span, instrument}; use crate::periodic_tables::evaluate_periodic_at_point; use crate::symbolic_builder::get_log_quotient_degree; use crate::util::verifier_row_to_ext; -use crate::{Domain, PcsError, Proof, StarkGenericConfig, Val, VerifierConstraintFolder}; +use crate::{ + AirWithBoundaryConstraints, Domain, PcsError, Proof, StarkGenericConfig, Val, + VerifierConstraintFolder, +}; /// Recomposes the quotient polynomial from its chunks evaluated at a point. /// @@ -75,6 +80,7 @@ pub fn verify_constraints( aux_local: Option<&[SC::Challenge]>, aux_next: Option<&[SC::Challenge]>, randomness: &[SC::Challenge], + aux_bus_boundary_values: &[SC::Challenge], public_values: &[Val], trace_domain: Domain, zeta: SC::Challenge, @@ -82,7 +88,7 @@ pub fn verify_constraints( quotient: SC::Challenge, ) -> Result<(), VerificationError> where - SC: StarkGenericConfig, + SC: StarkGenericConfig + Sync, A: MidenAir, SC::Challenge>, Val: TwoAdicField, { @@ -147,6 +153,7 @@ where main, aux, randomness, + aux_bus_boundary_values, preprocessed, public_values, periodic_values: &periodic_values, @@ -226,16 +233,23 @@ pub fn verify( air: &A, proof: &Proof, public_values: &[Val], + var_length_public_inputs: &[&[&[Val]]], ) -> Result<(), VerificationError>> where - SC: StarkGenericConfig, + SC: StarkGenericConfig + Sync, A: MidenAir, SC::Challenge>, Val: TwoAdicField, { + let air = &AirWithBoundaryConstraints { + inner: air, + phantom: PhantomData::, + }; + let Proof { commitments, opened_values, opening_proof, + aux_finals, degree_bits, } = proof; @@ -247,9 +261,9 @@ where let trace_domain = pcs.natural_domain_for_degree(degree); // TODO: allow moving preprocessed commitment to preprocess time, if known in advance let (preprocessed_width, preprocessed_commit) = - process_preprocessed_trace::(air, opened_values, pcs, trace_domain, config.is_zk())?; + process_preprocessed_trace::(air, opened_values, pcs, trace_domain, config.is_zk())?; - let log_quotient_degree = get_log_quotient_degree::, SC::Challenge, A>( + let log_quotient_degree = get_log_quotient_degree::, SC::Challenge, _>( air, preprocessed_width, public_values.len(), @@ -297,7 +311,8 @@ where // begin processing aux trace (optional) let num_randomness = air.num_randomness(); - let air_width = A::width(air); + let air_width = air.width(); + let bus_types = air.bus_types(); let valid_shape = opened_values.trace_local.len() == air_width && opened_values.trace_next.len() == air_width && opened_values.quotient_chunks.len() == quotient_degree @@ -310,12 +325,15 @@ where // Check aux trace shape && if num_randomness > 0 { let aux_width_base = aux_width * SC::Challenge::DIMENSION; - match (&opened_values.aux_trace_local, &opened_values.aux_trace_next) { - (Some(l), Some(n)) => l.len() == aux_width_base && n.len() == aux_width_base, + // Note: bus_types length is not matched against aux_width, to allow for more generic aux traces. + match (&opened_values.aux_trace_local, &opened_values.aux_trace_next, aux_finals) { + (Some(l), Some(n), Some(f)) => l.len() == aux_width_base + && n.len() == aux_width_base + && f.len() == aux_width, _ => false, } } else { - opened_values.aux_trace_local.is_none() && opened_values.aux_trace_next.is_none() + opened_values.aux_trace_local.is_none() && opened_values.aux_trace_next.is_none() && aux_finals.is_none() }; if !valid_shape { return Err(VerificationError::InvalidProofShape); @@ -330,6 +348,14 @@ where } else { return Err(VerificationError::InvalidProofShape); } + if let Some(aux_finals) = &aux_finals { + for aux_final in aux_finals { + challenger.observe_algebra_element(*aux_final); + } + } else { + return Err(VerificationError::InvalidProofShape); + } + randomness } else { // No aux trace expected @@ -449,7 +475,33 @@ where zeta, ); - verify_constraints::>( + // Verify the aux trace final values match the expected values if the aux trace contains buses (one bus per aux column) + // Note: if no buses are defined (bus_types.is_empty), the boundary values of the aux_trace are not checked against the provided variable-length public inputs. + for (idx, (bus_type, aux_final)) in bus_types + .iter() + .zip(aux_finals.as_ref().unwrap_or(&vec![])) + .enumerate() + { + let public_inputs_for_bus = *var_length_public_inputs + .get(idx) + .ok_or(VerificationError::InvalidProofShape)?; + let expected_final = match bus_type { + BusType::Multiset => bus_multiset_boundary_varlen::<_, SC>( + &randomness, + public_inputs_for_bus.iter().copied(), + ), + BusType::Logup => bus_logup_boundary_varlen::<_, SC>( + &randomness, + public_inputs_for_bus.iter().copied(), + ), + }; + + if *aux_final != expected_final { + return Err(VerificationError::InvalidBusBoundaryValues); + } + } + + verify_constraints::>( air, &opened_values.trace_local, &opened_values.trace_next, @@ -458,6 +510,7 @@ where opened_values.aux_trace_local.as_deref(), opened_values.aux_trace_next.as_deref(), &randomness, + aux_finals.as_ref().unwrap_or(&vec![]), public_values, init_trace_domain, zeta, @@ -468,6 +521,49 @@ where Ok(()) } +/// Computes the final value for a multiset bus given variable-length public inputs. +pub fn bus_multiset_boundary_varlen< + 'a, + I: IntoIterator]>, + SC: StarkGenericConfig, +>( + randomness: &[SC::Challenge], + public_inputs: I, +) -> SC::Challenge { + let mut bus_p_last = SC::Challenge::ONE; + let rand = randomness; + for row in public_inputs { + let mut p_last = rand[0]; + for (c, p_i) in row.iter().enumerate() { + p_last += SC::Challenge::from(*p_i) * rand[c + 1]; + } + bus_p_last *= p_last; + } + bus_p_last +} + +/// Computes the final value for a logup bus boundary constraint given variable-length public inputs. +pub fn bus_logup_boundary_varlen< + 'a, + I: IntoIterator]>, + SC: StarkGenericConfig, +>( + randomness: &[SC::Challenge], + public_inputs: I, +) -> SC::Challenge { + let mut bus_q_last = SC::Challenge::ZERO; + let rand = randomness; + for row in public_inputs { + let mut q_last = rand[0]; + for (c, p_i) in row.iter().enumerate() { + let p_i = *p_i; + q_last += SC::Challenge::from(p_i) * rand[c + 1]; + } + bus_q_last += q_last.inverse(); + } + bus_q_last +} + #[derive(Debug)] pub enum VerificationError { InvalidProofShape, @@ -482,4 +578,6 @@ pub enum VerificationError { RandomizationError, /// The domain does not support computing the next point algebraically. NextPointUnavailable, + /// The expected bus boundary final values do not match the opened values. + InvalidBusBoundaryValues, } diff --git a/miden-prover/tests/fibonacci_air.rs b/miden-prover/tests/fibonacci_air.rs index 2aa8cfd95..b1649d0c9 100644 --- a/miden-prover/tests/fibonacci_air.rs +++ b/miden-prover/tests/fibonacci_air.rs @@ -146,11 +146,12 @@ fn test_fibonacci_impl(a: u64, b: u64, n: usize, x: u64, log_final_poly_len: usi Goldilocks::from_u64(b), Goldilocks::from_u64(x), ]; + let var_len_pis = vec![]; let air = FibonacciAir::new(); let proof = prove(&config, &air, &trace, &pis); - verify(&config, &air, &proof, &pis).expect("verification failed"); + verify(&config, &air, &proof, &pis, &var_len_pis).expect("verification failed"); } #[test] @@ -202,8 +203,9 @@ fn test_incorrect_fibonacci_value() { Goldilocks::ONE, Goldilocks::from_u64(999), // incorrect result ]; + let var_len_pis = vec![]; let air = FibonacciAir::new(); let proof = prove(&config, &air, &trace, &pis); - verify(&config, &air, &proof, &pis).expect("verification failed"); + verify(&config, &air, &proof, &pis, &var_len_pis).expect("verification failed"); } diff --git a/miden-prover/tests/periodic_air.rs b/miden-prover/tests/periodic_air.rs index 04fe2b7d8..ce7c4c483 100644 --- a/miden-prover/tests/periodic_air.rs +++ b/miden-prover/tests/periodic_air.rs @@ -186,11 +186,12 @@ fn test_fibonacci_periodic_impl(a: u64, b: u64, n: usize, x: u64, log_final_poly Goldilocks::from_u64(b), Goldilocks::from_u64(x), ]; + let var_len_pis = vec![]; let air = FibonacciPeriodicAir::new(); let proof = prove(&config, &air, &trace, &pis); - verify(&config, &air, &proof, &pis).expect("verification failed"); + verify(&config, &air, &proof, &pis, &var_len_pis).expect("verification failed"); } #[test] @@ -252,10 +253,11 @@ fn test_fibonacci_periodic_wrong_selector() { let challenger = Challenger::new(perm); let config = MyConfig::new(pcs, challenger); let pis = vec![Goldilocks::ZERO, Goldilocks::ONE, Goldilocks::from_u32(21)]; + let var_len_pis = vec![]; let air = FibonacciPeriodicAir::new(); // This should fail because selector[1] = 0, but periodic[1] = 1 let proof = prove(&config, &air, &trace, &pis); - verify(&config, &air, &proof, &pis).expect("verification failed"); + verify(&config, &air, &proof, &pis, &var_len_pis).expect("verification failed"); } diff --git a/miden-prover/tests/perm_air.rs b/miden-prover/tests/perm_air.rs index 5d366851d..3aba6bef5 100644 --- a/miden-prover/tests/perm_air.rs +++ b/miden-prover/tests/perm_air.rs @@ -227,6 +227,7 @@ fn test_public_value_impl(n: usize, x: u64, log_final_poly_len: usize) { let config = MyConfig::new(pcs, challenger); let pis = vec![Goldilocks::ZERO, Goldilocks::ONE, Goldilocks::from_u64(x)]; + let var_len_pis = vec![]; let mut air = FibPermAir::new(); air.with_aux_builder(|main: &RowMajorMatrix, challenges: &[Challenge]| { @@ -234,7 +235,7 @@ fn test_public_value_impl(n: usize, x: u64, log_final_poly_len: usize) { }); let proof = prove(&config, &air, &trace, &pis); - verify(&config, &air, &proof, &pis).expect("verification failed"); + verify(&config, &air, &proof, &pis, &var_len_pis).expect("verification failed"); } #[test] @@ -279,6 +280,7 @@ fn test_public_value_impl_deg5(n: usize, x: u64, log_final_poly_len: usize) { let config = MyConfig5::new(pcs, challenger); let pis = vec![Goldilocks::ZERO, Goldilocks::ONE, Goldilocks::from_u64(x)]; + let var_len_pis = vec![]; let mut air = FibPermAir::>::new(); air.with_aux_builder(|main: &RowMajorMatrix, challenges: &[Challenge5]| { @@ -286,7 +288,7 @@ fn test_public_value_impl_deg5(n: usize, x: u64, log_final_poly_len: usize) { }); let proof = prove(&config, &air, &trace, &pis); - verify(&config, &air, &proof, &pis).expect("verification failed"); + verify(&config, &air, &proof, &pis, &var_len_pis).expect("verification failed"); } #[cfg(debug_assertions)] @@ -311,11 +313,12 @@ fn test_incorrect_public_value() { Goldilocks::ONE, Goldilocks::from_u32(123_123), // incorrect result ]; + let var_len_pis = vec![]; let mut air = FibPermAir::new(); air.with_aux_builder(|main: &RowMajorMatrix, challenges: &[Challenge]| { miden_prover::generate_logup_trace::(main, &challenges[0]) }); let proof = prove(&config, &air, &trace, &pis); - verify(&config, &air, &proof, &pis).expect("verification failed"); + verify(&config, &air, &proof, &pis, &var_len_pis).expect("verification failed"); } diff --git a/uni-stark/src/proof.rs b/uni-stark/src/proof.rs index 625df5cb5..f0c080a61 100644 --- a/uni-stark/src/proof.rs +++ b/uni-stark/src/proof.rs @@ -20,6 +20,7 @@ pub struct Proof { pub commitments: Commitments>, pub opened_values: OpenedValues, pub opening_proof: PcsProof, + pub aux_finals: Option>, pub degree_bits: usize, } diff --git a/uni-stark/src/prover.rs b/uni-stark/src/prover.rs index 7d0a24a56..ce1c95658 100644 --- a/uni-stark/src/prover.rs +++ b/uni-stark/src/prover.rs @@ -417,6 +417,7 @@ where commitments, opened_values, opening_proof, + aux_finals: None, degree_bits: log_ext_degree, } } diff --git a/uni-stark/src/symbolic_variable.rs b/uni-stark/src/symbolic_variable.rs index 01ded99b1..579d7d642 100644 --- a/uni-stark/src/symbolic_variable.rs +++ b/uni-stark/src/symbolic_variable.rs @@ -13,6 +13,7 @@ pub enum Entry { Permutation { offset: usize }, Public, Periodic, + AuxBusBoundary, Challenge, } @@ -37,7 +38,7 @@ impl SymbolicVariable { match self.entry { Entry::Preprocessed { .. } | Entry::Main { .. } | Entry::Permutation { .. } => 1, Entry::Aux { .. } => 1, - Entry::Public | Entry::Periodic | Entry::Challenge => 0, + Entry::Public | Entry::Periodic | Entry::Challenge | Entry::AuxBusBoundary => 0, } } } diff --git a/uni-stark/src/verifier.rs b/uni-stark/src/verifier.rs index 201c4a761..956b1fab2 100644 --- a/uni-stark/src/verifier.rs +++ b/uni-stark/src/verifier.rs @@ -238,6 +238,7 @@ where commitments, opened_values, opening_proof, + aux_finals: _aux_finals, degree_bits, } = proof;