diff --git a/Cargo.lock b/Cargo.lock index 9d1566d..6d445da 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -189,6 +189,7 @@ dependencies = [ name = "brainfuck_prover" version = "0.1.0" dependencies = [ + "num-traits", "stwo-prover", ] diff --git a/Cargo.toml b/Cargo.toml index 1f0d225..0d671bf 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -40,4 +40,5 @@ clap = { version = "4.3.10", features = ["derive"] } stwo-prover = { git = "https://github.com/starkware-libs/stwo", rev = "f6214d1" } tracing = "0.1" tracing-subscriber = "0.3" +num-traits = "0.2.19" thiserror = "2.0" diff --git a/crates/brainfuck_prover/Cargo.toml b/crates/brainfuck_prover/Cargo.toml index ce63d6a..f28a0e6 100644 --- a/crates/brainfuck_prover/Cargo.toml +++ b/crates/brainfuck_prover/Cargo.toml @@ -10,3 +10,4 @@ workspace = true [dependencies] stwo-prover.workspace = true +num-traits.workspace = true diff --git a/crates/brainfuck_prover/src/components/instruction/mod.rs b/crates/brainfuck_prover/src/components/instruction/mod.rs new file mode 100644 index 0000000..13971b0 --- /dev/null +++ b/crates/brainfuck_prover/src/components/instruction/mod.rs @@ -0,0 +1 @@ +pub mod table; diff --git a/crates/brainfuck_prover/src/components/instruction/table.rs b/crates/brainfuck_prover/src/components/instruction/table.rs new file mode 100644 index 0000000..44fc2c2 --- /dev/null +++ b/crates/brainfuck_prover/src/components/instruction/table.rs @@ -0,0 +1,179 @@ +use stwo_prover::core::fields::m31::BaseField; + +/// Represents a single row in the Instruction Table. +/// +/// The Instruction Table stores: +/// - The instruction pointer (`ip`), +/// - The current instruction (`ci`), +/// - The next instruction (`ni`). +#[derive(Debug, Default, PartialEq, Eq, Clone)] +pub struct InstructionTableRow { + /// Instruction pointer: points to the current instruction in the program. + pub ip: BaseField, + /// Current instruction: the instruction at the current instruction pointer. + pub ci: BaseField, + /// Next instruction: + /// - The instruction that follows `ci` in the program, + /// - 0 if out of bounds. + pub ni: BaseField, +} + +/// Represents the Instruction Table, which holds the instruction sequence +/// for the Brainfuck virtual machine. +/// +/// The Instruction Table is constructed by concatenating the program's list of +/// instructions with the execution trace, and then sorting by instruction +/// pointer and cycle. It is used to verify that the program being executed +/// matches the correct instruction sequence. +#[derive(Debug, Default, PartialEq, Eq, Clone)] +pub struct InstructionTable { + /// A vector of [`InstructionTableRow`] representing the table rows. + pub table: Vec, +} + +impl InstructionTable { + /// Creates a new, empty [`InstructionTable`]. + /// + /// # Returns + /// A new instance of [`InstructionTable`] with an empty table. + pub const fn new() -> Self { + Self { table: Vec::new() } + } + + /// Adds a new row to the Instruction Table from the provided registers. + /// + /// # Arguments + /// * `ip` - The instruction pointer for the new row. + /// * `ci` - The current instruction for the new row. + /// * `ni` - The next instruction for the new row. + /// + /// This method pushes a new [`InstructionTableRow`] onto the `table` vector. + pub fn add_row_from_registers(&mut self, ip: BaseField, ci: BaseField, ni: BaseField) { + self.table.push(InstructionTableRow { ip, ci, ni }); + } + + /// Adds a new row to the Instruction Table. + /// + /// # Arguments + /// * `row` - The [`InstructionTableRow`] to add to the table. + /// + /// This method pushes a new [`InstructionTableRow`] onto the `table` vector. + pub fn add_row(&mut self, row: InstructionTableRow) { + self.table.push(row); + } + + /// Adds multiple rows to the Instruction Table. + /// + /// # Arguments + /// * `rows` - A vector of [`InstructionTableRow`] to add to the table. + /// + /// This method extends the `table` vector with the provided rows. + pub fn add_rows(&mut self, rows: Vec) { + self.table.extend(rows); + } + + /// Retrieves a reference to a specific row in the Instruction Table. + /// + /// # Arguments + /// * `row` - The [`InstructionTableRow`] to search for in the table. + /// + /// # Returns + /// An `Option` containing a reference to the matching row if found, + /// or `None` if the row does not exist in the table. + pub fn get_row(&self, row: &InstructionTableRow) -> Option<&InstructionTableRow> { + self.table.iter().find(|r| *r == row) + } +} + +#[cfg(test)] +mod tests { + use super::*; + use num_traits::Zero; + + #[test] + fn test_instruction_table_new() { + let instruction_table = InstructionTable::new(); + assert!( + instruction_table.table.is_empty(), + "Instruction table should be empty upon initialization." + ); + } + + #[test] + fn test_add_row() { + let mut instruction_table = InstructionTable::new(); + // Create a row to add to the table + let row = InstructionTableRow { + ip: BaseField::zero(), + ci: BaseField::from(43), + ni: BaseField::from(91), + }; + // Add the row to the table + instruction_table.add_row_from_registers( + BaseField::zero(), + BaseField::from(43), + BaseField::from(91), + ); + // Check that the table contains the added row + assert_eq!(instruction_table.table, vec![row], "Added row should match the expected row."); + } + + #[test] + fn test_add_multiple_rows() { + let mut instruction_table = InstructionTable::new(); + // Create a vector of rows to add to the table + let rows = vec![ + InstructionTableRow { + ip: BaseField::from(0), + ci: BaseField::from(43), + ni: BaseField::from(91), + }, + InstructionTableRow { + ip: BaseField::from(1), + ci: BaseField::from(91), + ni: BaseField::from(9), + }, + InstructionTableRow { + ip: BaseField::from(2), + ci: BaseField::from(62), + ni: BaseField::from(43), + }, + ]; + // Add the rows to the table + instruction_table.add_rows(rows.clone()); + // Check that the table contains the added rows + assert_eq!(instruction_table, InstructionTable { table: rows }); + } + + #[test] + fn test_get_existing_row() { + let mut instruction_table = InstructionTable::new(); + // Create a row to add to the table + let row = InstructionTableRow { + ip: BaseField::from(0), + ci: BaseField::from(43), + ni: BaseField::from(91), + }; + // Add the row to the table + instruction_table.add_row(row.clone()); + // Retrieve the row from the table + let retrieved = instruction_table.get_row(&row); + // Check that the retrieved row matches the added row + assert_eq!(retrieved.unwrap(), &row, "Retrieved row should match the added row."); + } + + #[test] + fn test_get_non_existing_row() { + let instruction_table = InstructionTable::new(); + // Create a row to search for in the table + let row = InstructionTableRow { + ip: BaseField::from(0), + ci: BaseField::from(43), + ni: BaseField::from(91), + }; + // Try to retrieve the non-existing row from the table + let retrieved = instruction_table.get_row(&row); + // Check that the retrieved row is None + assert!(retrieved.is_none(), "Should return None for a non-existing row."); + } +} diff --git a/crates/brainfuck_prover/src/components/mod.rs b/crates/brainfuck_prover/src/components/mod.rs index 8b13789..ca4b15f 100644 --- a/crates/brainfuck_prover/src/components/mod.rs +++ b/crates/brainfuck_prover/src/components/mod.rs @@ -1 +1 @@ - +pub mod instruction; diff --git a/crates/brainfuck_vm/Cargo.toml b/crates/brainfuck_vm/Cargo.toml index c73304a..699803f 100644 --- a/crates/brainfuck_vm/Cargo.toml +++ b/crates/brainfuck_vm/Cargo.toml @@ -10,7 +10,7 @@ workspace = true [dependencies] clap = { workspace = true, features = ["derive"] } -num-traits = "0.2.19" +num-traits.workspace = true stwo-prover.workspace = true tracing.workspace = true tracing-subscriber = { workspace = true, features = ["env-filter"] }