From bfc45aac53666fc928e0bbe6361c39133defb45b Mon Sep 17 00:00:00 2001 From: Thomas Coratger Date: Thu, 7 Nov 2024 18:41:25 +0100 Subject: [PATCH 1/7] add InstructionTable struct --- crates/brainfuck_vm/src/lib.rs | 1 + crates/brainfuck_vm/src/tables/instruction.rs | 179 ++++++++++++++++++ crates/brainfuck_vm/src/tables/mod.rs | 1 + 3 files changed, 181 insertions(+) create mode 100644 crates/brainfuck_vm/src/tables/instruction.rs create mode 100644 crates/brainfuck_vm/src/tables/mod.rs diff --git a/crates/brainfuck_vm/src/lib.rs b/crates/brainfuck_vm/src/lib.rs index 461a445..e333483 100644 --- a/crates/brainfuck_vm/src/lib.rs +++ b/crates/brainfuck_vm/src/lib.rs @@ -2,4 +2,5 @@ pub mod compiler; pub mod instruction; pub mod machine; pub mod registers; +pub mod tables; pub mod test_helper; diff --git a/crates/brainfuck_vm/src/tables/instruction.rs b/crates/brainfuck_vm/src/tables/instruction.rs new file mode 100644 index 0000000..bc6909e --- /dev/null +++ b/crates/brainfuck_vm/src/tables/instruction.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 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.clone() }); + } + + #[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.clone()); + // 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_vm/src/tables/mod.rs b/crates/brainfuck_vm/src/tables/mod.rs new file mode 100644 index 0000000..ca4b15f --- /dev/null +++ b/crates/brainfuck_vm/src/tables/mod.rs @@ -0,0 +1 @@ +pub mod instruction; From 04455c896277cb7370292deb72425e41d02ed823 Mon Sep 17 00:00:00 2001 From: Thomas Coratger Date: Thu, 7 Nov 2024 18:45:10 +0100 Subject: [PATCH 2/7] clippy --- crates/brainfuck_vm/src/tables/instruction.rs | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) diff --git a/crates/brainfuck_vm/src/tables/instruction.rs b/crates/brainfuck_vm/src/tables/instruction.rs index bc6909e..44fc2c2 100644 --- a/crates/brainfuck_vm/src/tables/instruction.rs +++ b/crates/brainfuck_vm/src/tables/instruction.rs @@ -36,7 +36,7 @@ impl InstructionTable { /// /// # Returns /// A new instance of [`InstructionTable`] with an empty table. - pub fn new() -> Self { + pub const fn new() -> Self { Self { table: Vec::new() } } @@ -80,8 +80,8 @@ impl InstructionTable { /// # 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) + pub fn get_row(&self, row: &InstructionTableRow) -> Option<&InstructionTableRow> { + self.table.iter().find(|r| *r == row) } } @@ -142,7 +142,7 @@ mod tests { // 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.clone() }); + assert_eq!(instruction_table, InstructionTable { table: rows }); } #[test] @@ -157,7 +157,7 @@ mod tests { // 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.clone()); + 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."); } @@ -172,7 +172,7 @@ mod tests { ni: BaseField::from(91), }; // Try to retrieve the non-existing row from the table - let retrieved = instruction_table.get_row(row); + 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."); } From 2ee12826d3e563f18cc85fcebeb0203801c30554 Mon Sep 17 00:00:00 2001 From: Thomas Coratger Date: Thu, 7 Nov 2024 20:45:07 +0100 Subject: [PATCH 3/7] mv tables --- crates/brainfuck_prover/src/lib.rs | 1 + .../{brainfuck_vm => brainfuck_prover}/src/tables/instruction.rs | 0 crates/{brainfuck_vm => brainfuck_prover}/src/tables/mod.rs | 0 crates/brainfuck_vm/src/lib.rs | 1 - 4 files changed, 1 insertion(+), 1 deletion(-) rename crates/{brainfuck_vm => brainfuck_prover}/src/tables/instruction.rs (100%) rename crates/{brainfuck_vm => brainfuck_prover}/src/tables/mod.rs (100%) diff --git a/crates/brainfuck_prover/src/lib.rs b/crates/brainfuck_prover/src/lib.rs index 8913003..bf65d8a 100644 --- a/crates/brainfuck_prover/src/lib.rs +++ b/crates/brainfuck_prover/src/lib.rs @@ -1,2 +1,3 @@ pub mod brainfuck_air; pub mod components; +pub mod tables; diff --git a/crates/brainfuck_vm/src/tables/instruction.rs b/crates/brainfuck_prover/src/tables/instruction.rs similarity index 100% rename from crates/brainfuck_vm/src/tables/instruction.rs rename to crates/brainfuck_prover/src/tables/instruction.rs diff --git a/crates/brainfuck_vm/src/tables/mod.rs b/crates/brainfuck_prover/src/tables/mod.rs similarity index 100% rename from crates/brainfuck_vm/src/tables/mod.rs rename to crates/brainfuck_prover/src/tables/mod.rs diff --git a/crates/brainfuck_vm/src/lib.rs b/crates/brainfuck_vm/src/lib.rs index e333483..461a445 100644 --- a/crates/brainfuck_vm/src/lib.rs +++ b/crates/brainfuck_vm/src/lib.rs @@ -2,5 +2,4 @@ pub mod compiler; pub mod instruction; pub mod machine; pub mod registers; -pub mod tables; pub mod test_helper; From b2e67ec46efaaaed110fde3180a1ef9a8d387dca Mon Sep 17 00:00:00 2001 From: Thomas Coratger Date: Thu, 7 Nov 2024 20:46:18 +0100 Subject: [PATCH 4/7] mv --- .../brainfuck_prover/src/{tables => components}/instruction.rs | 0 crates/brainfuck_prover/src/components/mod.rs | 2 +- crates/brainfuck_prover/src/lib.rs | 1 - crates/brainfuck_prover/src/tables/mod.rs | 1 - 4 files changed, 1 insertion(+), 3 deletions(-) rename crates/brainfuck_prover/src/{tables => components}/instruction.rs (100%) delete mode 100644 crates/brainfuck_prover/src/tables/mod.rs diff --git a/crates/brainfuck_prover/src/tables/instruction.rs b/crates/brainfuck_prover/src/components/instruction.rs similarity index 100% rename from crates/brainfuck_prover/src/tables/instruction.rs rename to crates/brainfuck_prover/src/components/instruction.rs 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_prover/src/lib.rs b/crates/brainfuck_prover/src/lib.rs index bf65d8a..8913003 100644 --- a/crates/brainfuck_prover/src/lib.rs +++ b/crates/brainfuck_prover/src/lib.rs @@ -1,3 +1,2 @@ pub mod brainfuck_air; pub mod components; -pub mod tables; diff --git a/crates/brainfuck_prover/src/tables/mod.rs b/crates/brainfuck_prover/src/tables/mod.rs deleted file mode 100644 index ca4b15f..0000000 --- a/crates/brainfuck_prover/src/tables/mod.rs +++ /dev/null @@ -1 +0,0 @@ -pub mod instruction; From 3cd05bddcbcc4a724f22e698d8418b8e876859bf Mon Sep 17 00:00:00 2001 From: Thomas Coratger Date: Fri, 8 Nov 2024 10:39:19 +0100 Subject: [PATCH 5/7] num traits --- Cargo.lock | 1 + Cargo.toml | 1 + crates/brainfuck_prover/Cargo.toml | 1 + crates/brainfuck_vm/Cargo.toml | 2 +- 4 files changed, 4 insertions(+), 1 deletion(-) diff --git a/Cargo.lock b/Cargo.lock index 4809964..117ab4a 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 a752d96..d6046b6 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -40,3 +40,4 @@ 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" 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_vm/Cargo.toml b/crates/brainfuck_vm/Cargo.toml index fbe450f..926237c 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"] } From 773276f7ad68f94f7605cb2859533fbcd6a00906 Mon Sep 17 00:00:00 2001 From: Thomas Coratger Date: Fri, 8 Nov 2024 10:49:13 +0100 Subject: [PATCH 6/7] fix comment --- .../src/components/{ => instruction}/instruction.rs | 0 crates/brainfuck_prover/src/components/instruction/mod.rs | 1 + 2 files changed, 1 insertion(+) rename crates/brainfuck_prover/src/components/{ => instruction}/instruction.rs (100%) create mode 100644 crates/brainfuck_prover/src/components/instruction/mod.rs diff --git a/crates/brainfuck_prover/src/components/instruction.rs b/crates/brainfuck_prover/src/components/instruction/instruction.rs similarity index 100% rename from crates/brainfuck_prover/src/components/instruction.rs rename to crates/brainfuck_prover/src/components/instruction/instruction.rs 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..ca4b15f --- /dev/null +++ b/crates/brainfuck_prover/src/components/instruction/mod.rs @@ -0,0 +1 @@ +pub mod instruction; From d126ee81be97641158c0f847e8210b61e9e1c3fb Mon Sep 17 00:00:00 2001 From: Thomas Coratger Date: Fri, 8 Nov 2024 10:54:25 +0100 Subject: [PATCH 7/7] fix naming --- crates/brainfuck_prover/src/components/instruction/mod.rs | 2 +- .../src/components/instruction/{instruction.rs => table.rs} | 0 2 files changed, 1 insertion(+), 1 deletion(-) rename crates/brainfuck_prover/src/components/instruction/{instruction.rs => table.rs} (100%) diff --git a/crates/brainfuck_prover/src/components/instruction/mod.rs b/crates/brainfuck_prover/src/components/instruction/mod.rs index ca4b15f..13971b0 100644 --- a/crates/brainfuck_prover/src/components/instruction/mod.rs +++ b/crates/brainfuck_prover/src/components/instruction/mod.rs @@ -1 +1 @@ -pub mod instruction; +pub mod table; diff --git a/crates/brainfuck_prover/src/components/instruction/instruction.rs b/crates/brainfuck_prover/src/components/instruction/table.rs similarity index 100% rename from crates/brainfuck_prover/src/components/instruction/instruction.rs rename to crates/brainfuck_prover/src/components/instruction/table.rs