diff --git a/crates/prover/src/examples/wide_fibonacci/component.rs b/crates/prover/src/examples/wide_fibonacci/component.rs index cfd5d2928..70596a1d1 100644 --- a/crates/prover/src/examples/wide_fibonacci/component.rs +++ b/crates/prover/src/examples/wide_fibonacci/component.rs @@ -1,7 +1,7 @@ use itertools::Itertools; use num_traits::Zero; -use super::trace_gen::write_trace_row; +use super::trace_gen::{write_lookup_column, write_trace_row}; use crate::core::air::{Air, Component}; use crate::core::backend::CPUBackend; use crate::core::fields::m31::BaseField; @@ -9,6 +9,7 @@ use crate::core::ColumnVec; pub const LOG_N_COLUMNS: usize = 8; pub const N_COLUMNS: usize = 1 << LOG_N_COLUMNS; +pub const LOG_N_ROWS: usize = 4; /// Component that computes fibonacci numbers over [N_COLUMNS] columns. pub struct WideFibComponent { @@ -36,6 +37,21 @@ impl WideFibComponent { dst } + pub fn lookup_columns( + &self, + trace: &[Vec], + // TODO(AlonH): Change alpha and z to SecureField. + alpha: BaseField, + z: BaseField, + ) -> ColumnVec> { + let n_rows = trace[0].len(); + let zero_vec = vec![BaseField::zero(); n_rows]; + let mut dst = vec![zero_vec; 2]; + write_lookup_column(&mut dst[0], trace, 0, alpha, z); + write_lookup_column(&mut dst[1], trace, N_COLUMNS - 2, alpha, z); + dst + } + pub fn log_column_size(&self) -> u32 { self.log_n_instances + self.log_fibonacci_size - LOG_N_COLUMNS as u32 } diff --git a/crates/prover/src/examples/wide_fibonacci/mod.rs b/crates/prover/src/examples/wide_fibonacci/mod.rs index 91a0cc84a..7a3066679 100644 --- a/crates/prover/src/examples/wide_fibonacci/mod.rs +++ b/crates/prover/src/examples/wide_fibonacci/mod.rs @@ -7,9 +7,9 @@ pub mod trace_gen; #[cfg(test)] mod tests { use itertools::Itertools; - use num_traits::Zero; + use num_traits::{One, Zero}; - use super::component::{Input, WideFibAir, WideFibComponent, LOG_N_COLUMNS}; + use super::component::{Input, WideFibAir, WideFibComponent, LOG_N_COLUMNS, LOG_N_ROWS}; use crate::commitment_scheme::blake2_hash::Blake2sHasher; use crate::commitment_scheme::hasher::Hasher; use crate::core::air::accumulation::DomainEvaluationAccumulator; @@ -34,8 +34,44 @@ mod tests { } } + pub fn assert_constraints_on_lookup_column( + columns: &[Vec], + input_trace: &[Vec], + alpha: BaseField, + z: BaseField, + ) { + let n_columns = input_trace.len(); + let column_length = columns[0].len(); + let mut column_0_prev_value = BaseField::one(); + let mut column_1_prev_value = BaseField::one(); + for i in 0..column_length { + assert_eq!( + (columns[0][i] + - (input_trace[0][i] + alpha * input_trace[1][i] - z) * column_0_prev_value), + BaseField::zero() + ); + assert_eq!( + (columns[1][i] + - (input_trace[n_columns - 2][i] + alpha * input_trace[n_columns - 1][i] - z) + * column_1_prev_value), + BaseField::zero() + ); + column_0_prev_value = columns[0][i]; + column_1_prev_value = columns[1][i]; + } + + assert_eq!( + (input_trace[0][0] + alpha * input_trace[1][0] - z) * columns[1][column_length - 1] + - (input_trace[n_columns - 2][column_length - 1] + + alpha * input_trace[n_columns - 1][column_length - 1] + - z) + * columns[0][column_length - 1], + BaseField::zero() + ); + } + #[test] - fn test_wide_fib_trace() { + fn test_trace_row_constraints() { let wide_fib = WideFibComponent { log_fibonacci_size: LOG_N_COLUMNS as u32, log_n_instances: 1, @@ -53,6 +89,25 @@ mod tests { assert_constraints_on_row(&trace1); } + #[test] + fn test_lookup_column_constraints() { + let wide_fib = WideFibComponent { + log_fibonacci_size: (LOG_N_ROWS + LOG_N_COLUMNS) as u32, + log_n_instances: 0, + }; + let input = Input { + a: m31!(1), + b: m31!(1), + }; + + let alpha = m31!(1); + let z = m31!(2); + let trace = wide_fib.fill_initial_trace(vec![input]); + let lookup_trace = wide_fib.lookup_columns(&trace, alpha, z); + + assert_constraints_on_lookup_column(&lookup_trace, &trace, alpha, z) + } + #[test] fn test_composition_is_low_degree() { let wide_fib = WideFibComponent { diff --git a/crates/prover/src/examples/wide_fibonacci/trace_gen.rs b/crates/prover/src/examples/wide_fibonacci/trace_gen.rs index b82e8edfb..f9845635a 100644 --- a/crates/prover/src/examples/wide_fibonacci/trace_gen.rs +++ b/crates/prover/src/examples/wide_fibonacci/trace_gen.rs @@ -1,3 +1,5 @@ +use num_traits::One; + use super::component::{Input, N_COLUMNS}; use crate::core::fields::m31::BaseField; use crate::core::fields::FieldExpOps; @@ -18,3 +20,19 @@ pub fn write_trace_row( (dst[N_COLUMNS - 2][row_index], dst[N_COLUMNS - 1][row_index]) } + +pub fn write_lookup_column( + dst: &mut [BaseField], + input_trace: &[Vec], + column_offset: usize, + alpha: BaseField, + z: BaseField, +) { + let mut prev_value = BaseField::one(); + for (i, cell) in dst.iter_mut().enumerate() { + let row_i_0 = input_trace[column_offset][i]; + let row_i_1 = input_trace[column_offset + 1][i]; + *cell = (row_i_0 + alpha * row_i_1 - z) * prev_value; + prev_value = *cell; + } +} diff --git a/src/examples/wide_fibonacci/trace_asserts.rs b/src/examples/wide_fibonacci/trace_asserts.rs new file mode 100644 index 000000000..49bac5456 --- /dev/null +++ b/src/examples/wide_fibonacci/trace_asserts.rs @@ -0,0 +1,333 @@ +use num_traits::Zero; + +use crate::core::fields::m31::BaseField; + +pub fn assert_constraints_on_row(row: &[BaseField]) { + assert_eq!( + (row[2] - ((row[0] * row[0]) + (row[1] * row[1]))), + BaseField::zero() + ); + assert_eq!( + (row[3] - ((row[1] * row[1]) + (row[2] * row[2]))), + BaseField::zero() + ); + assert_eq!( + (row[4] - ((row[2] * row[2]) + (row[3] * row[3]))), + BaseField::zero() + ); + assert_eq!( + (row[5] - ((row[3] * row[3]) + (row[4] * row[4]))), + BaseField::zero() + ); + assert_eq!( + (row[6] - ((row[4] * row[4]) + (row[5] * row[5]))), + BaseField::zero() + ); + assert_eq!( + (row[7] - ((row[5] * row[5]) + (row[6] * row[6]))), + BaseField::zero() + ); + assert_eq!( + (row[8] - ((row[6] * row[6]) + (row[7] * row[7]))), + BaseField::zero() + ); + assert_eq!( + (row[9] - ((row[7] * row[7]) + (row[8] * row[8]))), + BaseField::zero() + ); + assert_eq!( + (row[10] - ((row[8] * row[8]) + (row[9] * row[9]))), + BaseField::zero() + ); + assert_eq!( + (row[11] - ((row[9] * row[9]) + (row[10] * row[10]))), + BaseField::zero() + ); + assert_eq!( + (row[12] - ((row[10] * row[10]) + (row[11] * row[11]))), + BaseField::zero() + ); + assert_eq!( + (row[13] - ((row[11] * row[11]) + (row[12] * row[12]))), + BaseField::zero() + ); + assert_eq!( + (row[14] - ((row[12] * row[12]) + (row[13] * row[13]))), + BaseField::zero() + ); + assert_eq!( + (row[15] - ((row[13] * row[13]) + (row[14] * row[14]))), + BaseField::zero() + ); + assert_eq!( + (row[16] - ((row[14] * row[14]) + (row[15] * row[15]))), + BaseField::zero() + ); + assert_eq!( + (row[17] - ((row[15] * row[15]) + (row[16] * row[16]))), + BaseField::zero() + ); + assert_eq!( + (row[18] - ((row[16] * row[16]) + (row[17] * row[17]))), + BaseField::zero() + ); + assert_eq!( + (row[19] - ((row[17] * row[17]) + (row[18] * row[18]))), + BaseField::zero() + ); + assert_eq!( + (row[20] - ((row[18] * row[18]) + (row[19] * row[19]))), + BaseField::zero() + ); + assert_eq!( + (row[21] - ((row[19] * row[19]) + (row[20] * row[20]))), + BaseField::zero() + ); + assert_eq!( + (row[22] - ((row[20] * row[20]) + (row[21] * row[21]))), + BaseField::zero() + ); + assert_eq!( + (row[23] - ((row[21] * row[21]) + (row[22] * row[22]))), + BaseField::zero() + ); + assert_eq!( + (row[24] - ((row[22] * row[22]) + (row[23] * row[23]))), + BaseField::zero() + ); + assert_eq!( + (row[25] - ((row[23] * row[23]) + (row[24] * row[24]))), + BaseField::zero() + ); + assert_eq!( + (row[26] - ((row[24] * row[24]) + (row[25] * row[25]))), + BaseField::zero() + ); + assert_eq!( + (row[27] - ((row[25] * row[25]) + (row[26] * row[26]))), + BaseField::zero() + ); + assert_eq!( + (row[28] - ((row[26] * row[26]) + (row[27] * row[27]))), + BaseField::zero() + ); + assert_eq!( + (row[29] - ((row[27] * row[27]) + (row[28] * row[28]))), + BaseField::zero() + ); + assert_eq!( + (row[30] - ((row[28] * row[28]) + (row[29] * row[29]))), + BaseField::zero() + ); + assert_eq!( + (row[31] - ((row[29] * row[29]) + (row[30] * row[30]))), + BaseField::zero() + ); + assert_eq!( + (row[32] - ((row[30] * row[30]) + (row[31] * row[31]))), + BaseField::zero() + ); + assert_eq!( + (row[33] - ((row[31] * row[31]) + (row[32] * row[32]))), + BaseField::zero() + ); + assert_eq!( + (row[34] - ((row[32] * row[32]) + (row[33] * row[33]))), + BaseField::zero() + ); + assert_eq!( + (row[35] - ((row[33] * row[33]) + (row[34] * row[34]))), + BaseField::zero() + ); + assert_eq!( + (row[36] - ((row[34] * row[34]) + (row[35] * row[35]))), + BaseField::zero() + ); + assert_eq!( + (row[37] - ((row[35] * row[35]) + (row[36] * row[36]))), + BaseField::zero() + ); + assert_eq!( + (row[38] - ((row[36] * row[36]) + (row[37] * row[37]))), + BaseField::zero() + ); + assert_eq!( + (row[39] - ((row[37] * row[37]) + (row[38] * row[38]))), + BaseField::zero() + ); + assert_eq!( + (row[40] - ((row[38] * row[38]) + (row[39] * row[39]))), + BaseField::zero() + ); + assert_eq!( + (row[41] - ((row[39] * row[39]) + (row[40] * row[40]))), + BaseField::zero() + ); + assert_eq!( + (row[42] - ((row[40] * row[40]) + (row[41] * row[41]))), + BaseField::zero() + ); + assert_eq!( + (row[43] - ((row[41] * row[41]) + (row[42] * row[42]))), + BaseField::zero() + ); + assert_eq!( + (row[44] - ((row[42] * row[42]) + (row[43] * row[43]))), + BaseField::zero() + ); + assert_eq!( + (row[45] - ((row[43] * row[43]) + (row[44] * row[44]))), + BaseField::zero() + ); + assert_eq!( + (row[46] - ((row[44] * row[44]) + (row[45] * row[45]))), + BaseField::zero() + ); + assert_eq!( + (row[47] - ((row[45] * row[45]) + (row[46] * row[46]))), + BaseField::zero() + ); + assert_eq!( + (row[48] - ((row[46] * row[46]) + (row[47] * row[47]))), + BaseField::zero() + ); + assert_eq!( + (row[49] - ((row[47] * row[47]) + (row[48] * row[48]))), + BaseField::zero() + ); + assert_eq!( + (row[50] - ((row[48] * row[48]) + (row[49] * row[49]))), + BaseField::zero() + ); + assert_eq!( + (row[51] - ((row[49] * row[49]) + (row[50] * row[50]))), + BaseField::zero() + ); + assert_eq!( + (row[52] - ((row[50] * row[50]) + (row[51] * row[51]))), + BaseField::zero() + ); + assert_eq!( + (row[53] - ((row[51] * row[51]) + (row[52] * row[52]))), + BaseField::zero() + ); + assert_eq!( + (row[54] - ((row[52] * row[52]) + (row[53] * row[53]))), + BaseField::zero() + ); + assert_eq!( + (row[55] - ((row[53] * row[53]) + (row[54] * row[54]))), + BaseField::zero() + ); + assert_eq!( + (row[56] - ((row[54] * row[54]) + (row[55] * row[55]))), + BaseField::zero() + ); + assert_eq!( + (row[57] - ((row[55] * row[55]) + (row[56] * row[56]))), + BaseField::zero() + ); + assert_eq!( + (row[58] - ((row[56] * row[56]) + (row[57] * row[57]))), + BaseField::zero() + ); + assert_eq!( + (row[59] - ((row[57] * row[57]) + (row[58] * row[58]))), + BaseField::zero() + ); + assert_eq!( + (row[60] - ((row[58] * row[58]) + (row[59] * row[59]))), + BaseField::zero() + ); + assert_eq!( + (row[61] - ((row[59] * row[59]) + (row[60] * row[60]))), + BaseField::zero() + ); + assert_eq!( + (row[62] - ((row[60] * row[60]) + (row[61] * row[61]))), + BaseField::zero() + ); + assert_eq!( + (row[63] - ((row[61] * row[61]) + (row[62] * row[62]))), + BaseField::zero() + ); +} + +pub fn assert_constraints_on_lookup_column( + columns: &[Vec], + input_trace: &[Vec], + alpha: BaseField, + z: BaseField, +) { + assert_eq!( + (columns[0][0] - (input_trace[0][0] + alpha * input_trace[1][0] - z)), + BaseField::zero() + ); + assert_eq!( + (columns[0][1] - ((input_trace[0][1] + alpha * input_trace[1][1] - z) * columns[0][0])), + BaseField::zero() + ); + assert_eq!( + (columns[0][2] - ((input_trace[0][2] + alpha * input_trace[1][2] - z) * columns[0][1])), + BaseField::zero() + ); + assert_eq!( + (columns[0][3] - ((input_trace[0][3] + alpha * input_trace[1][3] - z) * columns[0][2])), + BaseField::zero() + ); + assert_eq!( + (columns[0][4] - ((input_trace[0][4] + alpha * input_trace[1][4] - z) * columns[0][3])), + BaseField::zero() + ); + assert_eq!( + (columns[0][5] - ((input_trace[0][5] + alpha * input_trace[1][5] - z) * columns[0][4])), + BaseField::zero() + ); + assert_eq!( + (columns[0][6] - ((input_trace[0][6] + alpha * input_trace[1][6] - z) * columns[0][5])), + BaseField::zero() + ); + assert_eq!( + (columns[0][7] - ((input_trace[0][7] + alpha * input_trace[1][7] - z) * columns[0][6])), + BaseField::zero() + ); + assert_eq!( + (columns[1][0] - (input_trace[62][0] + alpha * input_trace[63][0] - z)), + BaseField::zero() + ); + assert_eq!( + (columns[1][1] - ((input_trace[62][1] + alpha * input_trace[63][1] - z) * columns[1][0])), + BaseField::zero() + ); + assert_eq!( + (columns[1][2] - ((input_trace[62][2] + alpha * input_trace[63][2] - z) * columns[1][1])), + BaseField::zero() + ); + assert_eq!( + (columns[1][3] - ((input_trace[62][3] + alpha * input_trace[63][3] - z) * columns[1][2])), + BaseField::zero() + ); + assert_eq!( + (columns[1][4] - ((input_trace[62][4] + alpha * input_trace[63][4] - z) * columns[1][3])), + BaseField::zero() + ); + assert_eq!( + (columns[1][5] - ((input_trace[62][5] + alpha * input_trace[63][5] - z) * columns[1][4])), + BaseField::zero() + ); + assert_eq!( + (columns[1][6] - ((input_trace[62][6] + alpha * input_trace[63][6] - z) * columns[1][5])), + BaseField::zero() + ); + assert_eq!( + (columns[1][7] - ((input_trace[62][7] + alpha * input_trace[63][7] - z) * columns[1][6])), + BaseField::zero() + ); + + assert_eq!( + (input_trace[0][0] + alpha * input_trace[1][0] - z) * columns[1][7] + - (input_trace[62][7] + alpha * input_trace[63][7] - z) * columns[0][7], + BaseField::zero() + ); + +} diff --git a/src/examples/wide_fibonacci/trace_gen.rs b/src/examples/wide_fibonacci/trace_gen.rs index b9ed616a7..78a96fdbe 100644 --- a/src/examples/wide_fibonacci/trace_gen.rs +++ b/src/examples/wide_fibonacci/trace_gen.rs @@ -142,3 +142,36 @@ pub fn write_trace_row( (dst[62][row_offset], dst[63][row_offset]) } + +pub fn write_lookup_column( + dst: &mut [BaseField], + input_trace: &[Vec], + column_offset: usize, + alpha: BaseField, + z: BaseField, +) { + let row_0_a = input_trace[column_offset][0]; + let row_0_b = input_trace[column_offset + 1][0]; + dst[0] = row_0_a + alpha * row_0_b - z; + let row_1_a = input_trace[column_offset][1]; + let row_1_b = input_trace[column_offset + 1][1]; + dst[1] = (row_1_a + alpha * row_1_b - z) * dst[0]; + let row_2_a = input_trace[column_offset][2]; + let row_2_b = input_trace[column_offset + 1][2]; + dst[2] = (row_2_a + alpha * row_2_b - z) * dst[1]; + let row_3_a = input_trace[column_offset][3]; + let row_3_b = input_trace[column_offset + 1][3]; + dst[3] = (row_3_a + alpha * row_3_b - z) * dst[2]; + let row_4_a = input_trace[column_offset][4]; + let row_4_b = input_trace[column_offset + 1][4]; + dst[4] = (row_4_a + alpha * row_4_b - z) * dst[3]; + let row_5_a = input_trace[column_offset][5]; + let row_5_b = input_trace[column_offset + 1][5]; + dst[5] = (row_5_a + alpha * row_5_b - z) * dst[4]; + let row_6_a = input_trace[column_offset][6]; + let row_6_b = input_trace[column_offset + 1][6]; + dst[6] = (row_6_a + alpha * row_6_b - z) * dst[5]; + let row_7_a = input_trace[column_offset][7]; + let row_7_b = input_trace[column_offset + 1][7]; + dst[7] = (row_7_a + alpha * row_7_b - z) * dst[6]; +}