From 001c82cd9ea3b7f00d5750054b4ab6c15570590a Mon Sep 17 00:00:00 2001 From: malatrax Date: Wed, 11 Dec 2024 10:29:48 +0100 Subject: [PATCH 1/5] feat: interaction trace evaluation --- .../src/components/io/table.rs | 52 +++++++++++++++++-- 1 file changed, 49 insertions(+), 3 deletions(-) diff --git a/crates/brainfuck_prover/src/components/io/table.rs b/crates/brainfuck_prover/src/components/io/table.rs index dd4c32b..bb68e82 100644 --- a/crates/brainfuck_prover/src/components/io/table.rs +++ b/crates/brainfuck_prover/src/components/io/table.rs @@ -1,10 +1,16 @@ -use crate::components::{IoClaim, TraceColumn, TraceEval}; +use crate::components::{ + memory::component::InteractionClaim, IoClaim, TraceColumn, TraceError, TraceEval, +}; use brainfuck_vm::{instruction::InstructionType, registers::Registers}; +use num_traits::One; use stwo_prover::{ - constraint_framework::{logup::LookupElements, Relation, RelationEFTraitBound}, + constraint_framework::{ + logup::{LogupTraceGenerator, LookupElements}, + Relation, RelationEFTraitBound, + }, core::{ backend::{ - simd::{column::BaseColumn, m31::LOG_N_LANES}, + simd::{column::BaseColumn, m31::LOG_N_LANES, qm31::PackedSecureField}, Column, }, channel::Channel, @@ -248,6 +254,46 @@ impl> Relation for IoElements { } } +/// Creates the interaction trace from the main trace evaluation +/// and the interaction elements for the I/O components. +/// +/// The Processor component uses the other components: +/// The Processor component multiplicities are then positive, +/// and the I/O components' multiplicities are negative +/// in the logUp protocol. +/// +/// # Returns +/// - Interaction trace evaluation, to be committed. +/// - Interaction claim: the total sum from the logUp protocol, +/// to be mixed into the Fiat-Shamir [`Channel`]. +#[allow(clippy::similar_names)] +pub fn interaction_trace_evaluation( + main_trace_eval: &TraceEval, + lookup_elements: &IoElements, +) -> Result<(TraceEval, InteractionClaim), TraceError> { + // If the main trace of the I/O components is empty, then we claimed that it's log size is zero. + let log_size = + if main_trace_eval.is_empty() { 0 } else { main_trace_eval[0].domain.log_size() }; + + let mut logup_gen = LogupTraceGenerator::new(log_size); + let mut col_gen = logup_gen.new_col(); + + let mv_col = &main_trace_eval[IoColumn::Io.index()].data; + for (vec_row, mv) in mv_col.iter().enumerate().take(1 << (log_size - LOG_N_LANES)) { + // We want to prove that the I/O table is a sublist (ordered set inclusion) of the Processor + // table. Therefore we set the index of the row into the numerator of the fraction. + let num = -PackedSecureField::one() * PackedSecureField::broadcast(vec_row.into()); + let denom: PackedSecureField = lookup_elements.combine(&[*mv]); + col_gen.write_frac(vec_row, num, denom); + } + + col_gen.finalize_col(); + + let (trace, claimed_sum) = logup_gen.finalize_last(); + + Ok((trace, InteractionClaim { claimed_sum })) +} + #[cfg(test)] mod tests { use super::*; From c210c4e0735761070504b93b55c560ed05b02d64 Mon Sep 17 00:00:00 2001 From: malatrax Date: Fri, 13 Dec 2024 15:58:23 +0100 Subject: [PATCH 2/5] refactor: use io InteractionClaim --- crates/brainfuck_prover/src/components/io/table.rs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/crates/brainfuck_prover/src/components/io/table.rs b/crates/brainfuck_prover/src/components/io/table.rs index bb68e82..d2a2201 100644 --- a/crates/brainfuck_prover/src/components/io/table.rs +++ b/crates/brainfuck_prover/src/components/io/table.rs @@ -1,5 +1,5 @@ use crate::components::{ - memory::component::InteractionClaim, IoClaim, TraceColumn, TraceError, TraceEval, + io::component::InteractionClaim, IoClaim, TraceColumn, TraceError, TraceEval, }; use brainfuck_vm::{instruction::InstructionType, registers::Registers}; use num_traits::One; From c42fe1131bab2dd2b52e47ee18f0ebc6cce3d590 Mon Sep 17 00:00:00 2001 From: malatrax Date: Mon, 16 Dec 2024 10:29:17 +0100 Subject: [PATCH 3/5] refactor: remove row index from the IO multiplicity --- crates/brainfuck_prover/src/components/io/table.rs | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/crates/brainfuck_prover/src/components/io/table.rs b/crates/brainfuck_prover/src/components/io/table.rs index d2a2201..a937c56 100644 --- a/crates/brainfuck_prover/src/components/io/table.rs +++ b/crates/brainfuck_prover/src/components/io/table.rs @@ -281,8 +281,8 @@ pub fn interaction_trace_evaluation( let mv_col = &main_trace_eval[IoColumn::Io.index()].data; for (vec_row, mv) in mv_col.iter().enumerate().take(1 << (log_size - LOG_N_LANES)) { // We want to prove that the I/O table is a sublist (ordered set inclusion) of the Processor - // table. Therefore we set the index of the row into the numerator of the fraction. - let num = -PackedSecureField::one() * PackedSecureField::broadcast(vec_row.into()); + // table. + let num = -PackedSecureField::one(); let denom: PackedSecureField = lookup_elements.combine(&[*mv]); col_gen.write_frac(vec_row, num, denom); } From 8e586c2edd90355fb890c3f6665f3f366b397416 Mon Sep 17 00:00:00 2001 From: malatrax Date: Mon, 16 Dec 2024 11:02:44 +0100 Subject: [PATCH 4/5] feat: add IO interaction trace evaluation --- .../src/components/io/table.rs | 66 +++++++++++++++++++ 1 file changed, 66 insertions(+) diff --git a/crates/brainfuck_prover/src/components/io/table.rs b/crates/brainfuck_prover/src/components/io/table.rs index a937c56..2cb4371 100644 --- a/crates/brainfuck_prover/src/components/io/table.rs +++ b/crates/brainfuck_prover/src/components/io/table.rs @@ -298,6 +298,7 @@ pub fn interaction_trace_evaluation( mod tests { use super::*; use num_traits::{One, Zero}; + use stwo_prover::core::channel::Blake2sChannel; type TestIOTable = IOTable<10>; @@ -534,4 +535,69 @@ mod tests { ); } } + + #[test] + fn test_interaction_trace_evaluation() { + let mut io_table = TestIOTable::new(); + // Trace rows are: + // - Real row + // - Real row + // - Dummy row (padding to the power of 2) + // - Dummy row (padding to the power of 2) + let rows = vec![ + IOTableRow::new(BaseField::one()), + IOTableRow::new(BaseField::from(2)), + IOTableRow::new(BaseField::zero()), + IOTableRow::new(BaseField::zero()), + ]; + io_table.add_rows(rows); + + let (trace_eval, claim) = io_table.trace_evaluation(); + + let channel = &mut Blake2sChannel::default(); + let lookup_elements = IoElements::draw(channel); + + let (interaction_trace_eval, interaction_claim) = + interaction_trace_evaluation(&trace_eval, &lookup_elements).unwrap(); + + let log_size = trace_eval[0].domain.log_size(); + let mut logup_gen = LogupTraceGenerator::new(log_size); + let mut col_gen = logup_gen.new_col(); + + let mut denoms = [PackedSecureField::zero(); 4]; + let mv_col = &trace_eval[IoColumn::Io.index()].data; + // Construct the denominator for each row of the logUp column, from the main trace + // evaluation. + for vec_row in 0..1 << (log_size - LOG_N_LANES) { + let mv = mv_col[vec_row]; + let denom: PackedSecureField = lookup_elements.combine(&[mv]); + denoms[vec_row] = denom; + } + + let num_0 = -PackedSecureField::one(); + let num_1 = -PackedSecureField::one(); + let num_2 = -PackedSecureField::one(); + let num_3 = -PackedSecureField::one(); + + col_gen.write_frac(0, num_0, denoms[0]); + col_gen.write_frac(1, num_1, denoms[1]); + col_gen.write_frac(2, num_2, denoms[2]); + col_gen.write_frac(3, num_3, denoms[3]); + + col_gen.finalize_col(); + let (expected_interaction_trace_eval, expected_claimed_sum) = logup_gen.finalize_last(); + + assert_eq!(claim.log_size, log_size,); + for col_index in 0..expected_interaction_trace_eval.len() { + assert_eq!( + interaction_trace_eval[col_index].domain, + expected_interaction_trace_eval[col_index].domain + ); + assert_eq!( + interaction_trace_eval[col_index].to_cpu().values, + expected_interaction_trace_eval[col_index].to_cpu().values + ); + } + assert_eq!(interaction_claim.claimed_sum, expected_claimed_sum); + } } From 0e602b32d200613fa59404bf6ed4c1116d48bad9 Mon Sep 17 00:00:00 2001 From: malatrax Date: Mon, 16 Dec 2024 12:27:59 +0100 Subject: [PATCH 5/5] refactor: integrate clk and ci registers to IO interaction trace evaluation --- .../src/components/io/table.rs | 127 +++++++++++++----- 1 file changed, 97 insertions(+), 30 deletions(-) diff --git a/crates/brainfuck_prover/src/components/io/table.rs b/crates/brainfuck_prover/src/components/io/table.rs index 2cb4371..4c63533 100644 --- a/crates/brainfuck_prover/src/components/io/table.rs +++ b/crates/brainfuck_prover/src/components/io/table.rs @@ -2,7 +2,7 @@ use crate::components::{ io::component::InteractionClaim, IoClaim, TraceColumn, TraceError, TraceEval, }; use brainfuck_vm::{instruction::InstructionType, registers::Registers}; -use num_traits::One; +use num_traits::{One, Zero}; use stwo_prover::{ constraint_framework::{ logup::{LogupTraceGenerator, LookupElements}, @@ -278,12 +278,17 @@ pub fn interaction_trace_evaluation( let mut logup_gen = LogupTraceGenerator::new(log_size); let mut col_gen = logup_gen.new_col(); - let mv_col = &main_trace_eval[IoColumn::Io.index()].data; - for (vec_row, mv) in mv_col.iter().enumerate().take(1 << (log_size - LOG_N_LANES)) { - // We want to prove that the I/O table is a sublist (ordered set inclusion) of the Processor - // table. - let num = -PackedSecureField::one(); - let denom: PackedSecureField = lookup_elements.combine(&[*mv]); + let clk_col = &main_trace_eval[IoColumn::Clk.index()].data; + let ci_col = &main_trace_eval[IoColumn::Ci.index()].data; + let mv_col = &main_trace_eval[IoColumn::Mv.index()].data; + for vec_row in 0..1 << (log_size - LOG_N_LANES) { + let clk = clk_col[vec_row]; + let ci = ci_col[vec_row]; + let mv = mv_col[vec_row]; + // We want to prove that the I/O table is a sublist (ordered set inclusion) + // of the Processor table. + let num = if ci.is_zero() { PackedSecureField::zero() } else { -PackedSecureField::one() }; + let denom: PackedSecureField = lookup_elements.combine(&[clk, ci, mv]); col_gen.write_frac(vec_row, num, denom); } @@ -298,15 +303,21 @@ pub fn interaction_trace_evaluation( mod tests { use super::*; use num_traits::{One, Zero}; - use stwo_prover::core::channel::Blake2sChannel; type TestIOTable = IOTable<10>; #[test] fn test_io_row_new() { - let row = IOTableRow::new(BaseField::zero(), BaseField::from(46), BaseField::from(91)); - let expected_row = - IOTableRow { clk: BaseField::zero(), ci: BaseField::from(46), mv: BaseField::from(91) }; + let row = IOTableRow::new( + BaseField::zero(), + InstructionType::PutChar.to_base_field(), + BaseField::from(91), + ); + let expected_row = IOTableRow { + clk: BaseField::zero(), + ci: InstructionType::PutChar.to_base_field(), + mv: BaseField::from(91), + }; assert_eq!(row, expected_row); } @@ -320,9 +331,17 @@ mod tests { fn test_table_add_row_from_register() { let mut io_table = TestIOTable::new(); // Create a row to add to the table - let row = IOTableRow::new(BaseField::zero(), BaseField::from(46), BaseField::from(91)); + let row = IOTableRow::new( + BaseField::zero(), + InstructionType::PutChar.to_base_field(), + BaseField::from(91), + ); // Add the row to the table - io_table.add_row_from_register(BaseField::zero(), BaseField::from(46), BaseField::from(91)); + io_table.add_row_from_register( + BaseField::zero(), + InstructionType::PutChar.to_base_field(), + BaseField::from(91), + ); // Check that the table contains the added row assert_eq!(io_table.table, vec![row], "Added row should match the expected row."); } @@ -331,7 +350,11 @@ mod tests { fn test_table_add_row() { let mut io_table = TestIOTable::new(); // Create a row to add to the table - let row = IOTableRow::new(BaseField::zero(), BaseField::from(46), BaseField::from(91)); + let row = IOTableRow::new( + BaseField::zero(), + InstructionType::PutChar.to_base_field(), + BaseField::from(91), + ); // Add the row to the table io_table.add_row(row.clone()); // Check that the table contains the added row @@ -343,9 +366,21 @@ mod tests { let mut io_table = TestIOTable::new(); // Create a vector of rows to add to the table let rows = vec![ - IOTableRow::new(BaseField::zero(), BaseField::from(46), BaseField::from(91)), - IOTableRow::new(BaseField::one(), BaseField::from(46), BaseField::from(9)), - IOTableRow::new(BaseField::from(4), BaseField::from(46), BaseField::from(43)), + IOTableRow::new( + BaseField::zero(), + InstructionType::PutChar.to_base_field(), + BaseField::from(91), + ), + IOTableRow::new( + BaseField::one(), + InstructionType::PutChar.to_base_field(), + BaseField::from(9), + ), + IOTableRow::new( + BaseField::from(4), + InstructionType::PutChar.to_base_field(), + BaseField::from(43), + ), ]; // Add the rows to the table io_table.add_rows(rows.clone()); @@ -392,7 +427,11 @@ mod tests { }; let registers: Vec = vec![reg3, reg1, reg2]; - let row = IOTableRow::new(BaseField::zero(), BaseField::from(46), BaseField::from(5)); + let row = IOTableRow::new( + BaseField::zero(), + InstructionType::PutChar.to_base_field(), + BaseField::from(5), + ); let mut expected_io_table: OutputTable = IOTable::new(); expected_io_table.add_row(row); @@ -520,8 +559,21 @@ mod tests { fn test_trace_evaluation_circle_domain() { let mut io_table = TestIOTable::new(); io_table.add_rows(vec![ - IOTableRow::new(BaseField::zero(), BaseField::from(44), BaseField::one()), - IOTableRow::new(BaseField::one(), BaseField::from(44), BaseField::from(2)), + IOTableRow::new( + BaseField::zero(), + InstructionType::ReadChar.to_base_field(), + BaseField::one(), + ), + IOTableRow::new( + BaseField::one(), + InstructionType::ReadChar.to_base_field(), + BaseField::from(2), + ), + IOTableRow::new( + BaseField::from(3), + InstructionType::ReadChar.to_base_field(), + BaseField::from(7), + ), ]); let (trace, claim) = io_table.trace_evaluation(); @@ -542,20 +594,31 @@ mod tests { // Trace rows are: // - Real row // - Real row - // - Dummy row (padding to the power of 2) + // - Real row // - Dummy row (padding to the power of 2) let rows = vec![ - IOTableRow::new(BaseField::one()), - IOTableRow::new(BaseField::from(2)), - IOTableRow::new(BaseField::zero()), - IOTableRow::new(BaseField::zero()), + IOTableRow::new( + BaseField::zero(), + InstructionType::ReadChar.to_base_field(), + BaseField::one(), + ), + IOTableRow::new( + BaseField::one(), + InstructionType::ReadChar.to_base_field(), + BaseField::from(2), + ), + IOTableRow::new( + BaseField::from(3), + InstructionType::ReadChar.to_base_field(), + BaseField::from(7), + ), + IOTableRow::new(BaseField::zero(), BaseField::zero(), BaseField::zero()), ]; io_table.add_rows(rows); let (trace_eval, claim) = io_table.trace_evaluation(); - let channel = &mut Blake2sChannel::default(); - let lookup_elements = IoElements::draw(channel); + let lookup_elements = IoElements::dummy(); let (interaction_trace_eval, interaction_claim) = interaction_trace_evaluation(&trace_eval, &lookup_elements).unwrap(); @@ -565,19 +628,23 @@ mod tests { let mut col_gen = logup_gen.new_col(); let mut denoms = [PackedSecureField::zero(); 4]; - let mv_col = &trace_eval[IoColumn::Io.index()].data; + let clk_col = &trace_eval[IoColumn::Clk.index()].data; + let ci_col = &trace_eval[IoColumn::Ci.index()].data; + let mv_col = &trace_eval[IoColumn::Mv.index()].data; // Construct the denominator for each row of the logUp column, from the main trace // evaluation. for vec_row in 0..1 << (log_size - LOG_N_LANES) { + let clk = clk_col[vec_row]; + let ci = ci_col[vec_row]; let mv = mv_col[vec_row]; - let denom: PackedSecureField = lookup_elements.combine(&[mv]); + let denom: PackedSecureField = lookup_elements.combine(&[clk, ci, mv]); denoms[vec_row] = denom; } let num_0 = -PackedSecureField::one(); let num_1 = -PackedSecureField::one(); let num_2 = -PackedSecureField::one(); - let num_3 = -PackedSecureField::one(); + let num_3 = PackedSecureField::zero(); col_gen.write_frac(0, num_0, denoms[0]); col_gen.write_frac(1, num_1, denoms[1]);