From f5ad365427a4eda28a10c14e7337c95f9227c204 Mon Sep 17 00:00:00 2001 From: jewelofchaos9 Date: Mon, 6 Jan 2025 10:06:51 +0000 Subject: [PATCH 1/4] init for acir_formal_proofs --- .../src/acir_instruction_builder.rs | 287 ++++++++++++++++++ compiler/noirc_evaluator/src/lib.rs | 4 + compiler/noirc_evaluator/src/ssa/ir/map.rs | 2 +- compiler/noirc_evaluator/ssa_test/.gitignore | 1 + compiler/noirc_evaluator/ssa_test/Cargo.toml | 12 + compiler/noirc_evaluator/ssa_test/README.md | 27 ++ compiler/noirc_evaluator/ssa_test/src/main.rs | 111 +++++++ 7 files changed, 443 insertions(+), 1 deletion(-) create mode 100644 compiler/noirc_evaluator/src/acir_instruction_builder.rs create mode 100644 compiler/noirc_evaluator/ssa_test/.gitignore create mode 100644 compiler/noirc_evaluator/ssa_test/Cargo.toml create mode 100644 compiler/noirc_evaluator/ssa_test/README.md create mode 100644 compiler/noirc_evaluator/ssa_test/src/main.rs diff --git a/compiler/noirc_evaluator/src/acir_instruction_builder.rs b/compiler/noirc_evaluator/src/acir_instruction_builder.rs new file mode 100644 index 00000000000..af0337e2e0d --- /dev/null +++ b/compiler/noirc_evaluator/src/acir_instruction_builder.rs @@ -0,0 +1,287 @@ +use std::collections::BTreeSet; +use acvm::{ + acir::{ + circuit::{ + Circuit, ExpressionWidth, + Program as AcirProgram + }, + native_types::Witness, + }, + FieldElement, +}; + +use crate::ssa::ssa_gen::Ssa; +use crate::ssa::ir::map::Id; +use crate::ssa::ir::function::Function; + +use crate::ssa::{ + function_builder::FunctionBuilder, + ir::{instruction::BinaryOp, types::Type}, +}; +use crate::brillig::Brillig; +use serde::{Deserialize, Serialize}; + +/// Represents artifacts generated from compiling an instruction +#[derive(Serialize, Deserialize)] +pub struct InstructionArtifacts { + /// Name of the instruction + pub instruction_name: String, + + /// SSA representation formatted as "acir(inline) {...}" + pub formatted_ssa: String, + + /// JSON serialized SSA + pub serialized_ssa: String, + + /// Gzipped bytes of ACIR program + pub serialized_acir: Vec, +} + +/// Represents the type of a variable in the instruction +#[derive(Debug)] +pub enum VariableType { + /// Field element type + Field, + /// Unsigned integer type + Unsigned, + /// Signed integer type + Signed +} + +/// Represents a variable with its type and size information +pub struct Variable { + /// Type of the variable (Field, Unsigned, or Signed) + pub variable_type: VariableType, + /// Bit size of the variable (ignored for Field type) + pub variable_size: u32, +} + +impl Variable { + /// Gets a string representation of the variable's type and size + pub fn get_name(&self) -> String { + return format!("{:?}_{}", self.variable_type, self.variable_size) + } +} + +impl InstructionArtifacts { + /// Converts a Variable into its corresponding SSA Type + fn get_type(variable: &Variable) -> Type { + match variable.variable_type { + VariableType::Field => Type::field(), + VariableType::Signed => Type::signed(variable.variable_size), + VariableType::Unsigned => Type::unsigned(variable.variable_size) + } + } + + /// Creates a new binary operation instruction artifact + fn new_binary(op: BinaryOp, instruction_name: String, first_variable: &Variable, second_variable: &Variable) -> Self { + let first_variable_type = Self::get_type(first_variable); + let second_variable_type = Self::get_type(second_variable); + let ssa = binary_function(op, first_variable_type, second_variable_type); + let serialized_ssa = &serde_json::to_string(&ssa).unwrap(); + let formatted_ssa = format!("{}", ssa); + + let program = ssa_to_acir_program(ssa); + let serialized_program = AcirProgram::serialize_program(&program); + let name = format!("{}_{}_{}", instruction_name, first_variable.get_name(), second_variable.get_name()); + + Self { + instruction_name: name, + formatted_ssa: formatted_ssa, + serialized_ssa: serialized_ssa.to_string(), + serialized_acir: serialized_program + } + } + + /// Creates a new instruction artifact using a provided SSA generation function + fn new_by_func(ssa_generate_function: fn(Type) -> Ssa, instruction_name: String, variable: &Variable) -> Self { + let variable_type = Self::get_type(variable); + let ssa = ssa_generate_function(variable_type); + let serialized_ssa = &serde_json::to_string(&ssa).unwrap(); + let formatted_ssa = format!("{}", ssa); + + let program = ssa_to_acir_program(ssa); + let serialized_program = AcirProgram::serialize_program(&program); + let name = format!("{}_{}", instruction_name, variable.get_name()); + + Self { + instruction_name: name, + formatted_ssa: formatted_ssa, + serialized_ssa: serialized_ssa.to_string(), + serialized_acir: serialized_program + } + } + + /// Creates a new constrain instruction artifact + pub fn new_constrain(variable: &Variable) -> Self { + return Self::new_by_func(constrain_function, "Constrain".into(), variable) + } + + /// Creates a new NOT operation instruction artifact + pub fn new_not(variable: &Variable) -> Self { + return Self::new_by_func(not_function, "Not".into(), variable) + } + + /// Creates a new range check instruction artifact + pub fn new_range_check(variable: &Variable) -> Self { + return Self::new_by_func(range_check_function, "RangeCheck".into(), variable) + } + + /// Creates a new truncate instruction artifact + pub fn new_truncate(variable: &Variable) -> Self { + return Self::new_by_func(truncate_function, "Truncate".into(), variable) + } + + /// Creates a new ADD operation instruction artifact + pub fn new_add(first_variable: &Variable, second_variable: &Variable) -> Self { + return Self::new_binary(BinaryOp::Add, "Binary::Add".into(), first_variable, second_variable); + } + + /// Creates a new SUB operation instruction artifact + pub fn new_sub(first_variable: &Variable, second_variable: &Variable) -> Self { + return Self::new_binary(BinaryOp::Sub, "Binary::Sub".into(), first_variable, second_variable); + } + + /// Creates a new XOR operation instruction artifact + pub fn new_xor(first_variable: &Variable, second_variable: &Variable) -> Self { + return Self::new_binary(BinaryOp::Xor, "Binary::Xor".into(), first_variable, second_variable); + } + + /// Creates a new AND operation instruction artifact + pub fn new_and(first_variable: &Variable, second_variable: &Variable) -> Self { + return Self::new_binary(BinaryOp::And, "Binary::And".into(), first_variable, second_variable); + } + + /// Creates a new OR operation instruction artifact + pub fn new_or(first_variable: &Variable, second_variable: &Variable) -> Self { + return Self::new_binary(BinaryOp::Or, "Binary::Or".into(), first_variable, second_variable); + } + + /// Creates a new less than operation instruction artifact + pub fn new_lt(first_variable: &Variable, second_variable: &Variable) -> Self { + return Self::new_binary(BinaryOp::Lt, "Binary::Lt".into(), first_variable, second_variable); + } + + /// Creates a new equals operation instruction artifact + pub fn new_eq(first_variable: &Variable, second_variable: &Variable) -> Self { + return Self::new_binary(BinaryOp::Eq, "Binary::Eq".into(), first_variable, second_variable); + } + + /// Creates a new modulo operation instruction artifact + pub fn new_mod(first_variable: &Variable, second_variable: &Variable) -> Self { + return Self::new_binary(BinaryOp::Mod, "Binary::Mod".into(), first_variable, second_variable); + } + + /// Creates a new multiply operation instruction artifact + pub fn new_mul(first_variable: &Variable, second_variable: &Variable) -> Self { + return Self::new_binary(BinaryOp::Mul, "Binary::Mul".into(), first_variable, second_variable); + } + + /// Creates a new divide operation instruction artifact + pub fn new_div(first_variable: &Variable, second_variable: &Variable) -> Self { + return Self::new_binary(BinaryOp::Div, "Binary::Div".into(), first_variable, second_variable); + } + + /// Creates a new shift left operation instruction artifact + pub fn new_shl(first_variable: &Variable, second_variable: &Variable) -> Self { + return Self::new_binary(BinaryOp::Shl, "Binary::Shl".into(), first_variable, second_variable); + } + + /// Creates a new shift right operation instruction artifact + pub fn new_shr(first_variable: &Variable, second_variable: &Variable) -> Self { + return Self::new_binary(BinaryOp::Shr, "Binary::Shr".into(), first_variable, second_variable); + } +} + +/// Converts SSA to ACIR program +fn ssa_to_acir_program(ssa: Ssa) -> AcirProgram { + // third brillig names, fourth errors + let (acir_functions, brillig, _, _) = ssa + .into_acir(&Brillig::default(), ExpressionWidth::default()) + .expect("Should compile manually written SSA into ACIR"); + + let mut functions: Vec> = Vec::new(); + + for acir_func in acir_functions.iter() { + let mut private_params: BTreeSet = acir_func.input_witnesses.clone().into_iter().collect(); + let ret_values: BTreeSet = acir_func.return_witnesses.clone().into_iter().collect(); + let circuit: Circuit; + private_params.extend(ret_values.iter().cloned()); + circuit = Circuit { + current_witness_index: acir_func.current_witness_index().witness_index(), + opcodes: acir_func.opcodes().to_vec(), + private_parameters: private_params.clone(), + ..Circuit::::default() + }; + functions.push(circuit); + } + return AcirProgram { functions: functions, unconstrained_functions: brillig }; +} + +/// Creates an SSA function for binary operations +fn binary_function(op: BinaryOp, first_variable_type: Type, second_variable_type: Type) -> Ssa { + // returns v0 op v1 + let main_id: Id = Id::new(0); + let mut builder = FunctionBuilder::new("main".into(), main_id); + let v0 = builder.add_parameter(first_variable_type); + let v1 = builder.add_parameter(second_variable_type); + let v2 = builder.insert_binary(v0, op, v1); + builder.terminate_with_return(vec![v2]); + + let func = builder.finish(); + // remove_bit_shifts replaces bit shifts with equivalent arithmetic operations + let cleared_func = func.remove_bit_shifts(); + return cleared_func; +} + +/// Creates an SSA function for constraint operations +fn constrain_function(variable_type: Type) -> Ssa { + // constrains v0 == v1, returns v1 + let main_id: Id = Id::new(0); + let mut builder = FunctionBuilder::new("main".into(), main_id); + + let v0 = builder.add_parameter(variable_type.clone()); + let v1 = builder.add_parameter(variable_type); + builder.insert_constrain(v0, v1, None); + builder.terminate_with_return(vec![v1]); + + return builder.finish(); +} + +/// Creates an SSA function for range check operations +fn range_check_function(variable_type: Type) -> Ssa { + let main_id: Id = Id::new(0); + let mut builder = FunctionBuilder::new("main".into(), main_id); + + let v0 = builder.add_parameter(variable_type); + builder.insert_range_check(v0, 64, Some("Range Check failed".to_string())); + builder.terminate_with_return(vec![v0]); + + return builder.finish() +} + +/// Creates an SSA function for truncate operations +fn truncate_function(variable_type: Type) -> Ssa { + // truncate v0: field 10, 20?.. + let main_id: Id = Id::new(0); + let mut builder = FunctionBuilder::new("main".into(), main_id); + + let v0 = builder.add_parameter(variable_type); + let v1 = builder.insert_truncate(v0, 10, 20); + builder.terminate_with_return(vec![v1]); + + return builder.finish(); +} + +/// Creates an SSA function for NOT operations +fn not_function(variable_type: Type) -> Ssa { + // returns not v0 + let main_id: Id = Id::new(0); + let mut builder = FunctionBuilder::new("main".into(), main_id); + + let v0 = builder.add_parameter(variable_type); + let v1 = builder.insert_not(v0); + builder.terminate_with_return(vec![v1]); + + return builder.finish() +} diff --git a/compiler/noirc_evaluator/src/lib.rs b/compiler/noirc_evaluator/src/lib.rs index 75ea557d3de..886ac1ece77 100644 --- a/compiler/noirc_evaluator/src/lib.rs +++ b/compiler/noirc_evaluator/src/lib.rs @@ -11,6 +11,10 @@ pub mod ssa; pub use ssa::create_program; pub use ssa::ir::instruction::ErrorType; +pub mod acir_instruction_builder; +pub use acir_instruction_builder::{ + InstructionArtifacts, VariableType, Variable +}; /// Trims leading whitespace from each line of the input string #[cfg(test)] diff --git a/compiler/noirc_evaluator/src/ssa/ir/map.rs b/compiler/noirc_evaluator/src/ssa/ir/map.rs index 1d637309191..088b1832610 100644 --- a/compiler/noirc_evaluator/src/ssa/ir/map.rs +++ b/compiler/noirc_evaluator/src/ssa/ir/map.rs @@ -28,7 +28,7 @@ impl Id { /// /// This is private so that we can guarantee ids created from this function /// point to valid T values in their external maps. - fn new(index: u32) -> Self { + pub(crate) fn new(index: u32) -> Self { Self { index, _marker: std::marker::PhantomData } } diff --git a/compiler/noirc_evaluator/ssa_test/.gitignore b/compiler/noirc_evaluator/ssa_test/.gitignore new file mode 100644 index 00000000000..03314f77b5a --- /dev/null +++ b/compiler/noirc_evaluator/ssa_test/.gitignore @@ -0,0 +1 @@ +Cargo.lock diff --git a/compiler/noirc_evaluator/ssa_test/Cargo.toml b/compiler/noirc_evaluator/ssa_test/Cargo.toml new file mode 100644 index 00000000000..497f1baeab2 --- /dev/null +++ b/compiler/noirc_evaluator/ssa_test/Cargo.toml @@ -0,0 +1,12 @@ +[package] +name = "ssa_test" +version = "0.1.0" +edition = "2021" + +[dependencies] +noirc_evaluator = {path = "../"} +serde = "1.0.214" +serde_json = "1.0.120" +flate2 = "1.0.35" +clap = { version = "4.4.11", features = ["derive"] } +[workspace] diff --git a/compiler/noirc_evaluator/ssa_test/README.md b/compiler/noirc_evaluator/ssa_test/README.md new file mode 100644 index 00000000000..a2e3b47af72 --- /dev/null +++ b/compiler/noirc_evaluator/ssa_test/README.md @@ -0,0 +1,27 @@ +# SSA Test Generator + +This tool generates test artifacts for formally verifying SSA instructions and their conversion to ACIR. + +## Purpose + +The test generator creates test cases for: + +- Bitvector operations (up to 127 bits): add, sub, mul, mod, xor, and, div, eq, lt, not, etc. +- Shift operations (tested with smaller bit sizes 32 and 64): shl, shr +- Binary operations (32-bit): xor, and, or +- Field operations: add, mul, div +- Signed integer operations: div (126-bit) + +Each test case generates: +- Formatted SSA representation +- Serialized ACIR output + +## Usage + +Run the generator with the desired output directory. The directory can be specified using the `-d` or `--dir` flag: + +```bash +cargo run -- -d /path/to/output/directory/ +``` + +DON'T FORGET TO CHANGE ARTIFACTS_PATH IN barretenberg/cpp/src/barretenberg/acir_formal_proofs/acir_loader.test.cpp TO THE NEW OUTPUT DIRECTORY. \ No newline at end of file diff --git a/compiler/noirc_evaluator/ssa_test/src/main.rs b/compiler/noirc_evaluator/ssa_test/src/main.rs new file mode 100644 index 00000000000..dc02e9b3aa6 --- /dev/null +++ b/compiler/noirc_evaluator/ssa_test/src/main.rs @@ -0,0 +1,111 @@ +use std::fs::File; +use std::io::Write; +use std::io::Read; +use std::path::Path; +use flate2::read::GzDecoder; +use::noirc_evaluator::acir_instruction_builder::{ + InstructionArtifacts, VariableType, Variable +}; +use clap::Parser; + +#[derive(Parser)] +#[command(author, version, about, long_about = None)] +struct Args { + #[arg(short, long, default_value = "../../../../../barretenberg/cpp/src/barretenberg/acir_formal_proofs/artifacts/")] + dir: String, +} + +/// Decompresses gzipped data into a byte vector +fn ungzip(compressed_data: Vec) -> Vec { + let mut decompressed_data: Vec = Vec::new(); + let mut decoder = GzDecoder::new(&compressed_data[..]); + decoder.read_to_end(&mut decompressed_data).unwrap(); + return decompressed_data; +} + +/// Saves byte data to a file at the specified path +fn save_to_file(data: &[u8], filename: &str) -> Result<(), std::io::Error> { + let path = Path::new(filename); + let mut file = File::create(path)?; + file.write_all(data)?; + Ok(()) +} + +/// Saves instruction artifacts to files in the artifacts directory +/// Prints the formatted SSA for each artifact and saves the decompressed ACIR +fn save_artifacts(all_artifacts: Vec, dir: &str) { + for artifacts in all_artifacts.iter() { + println!("{}", artifacts.formatted_ssa); + let filename = format!("{}{}{}", dir, artifacts.instruction_name, ".acir"); + let acir = &artifacts.serialized_acir; + match save_to_file(&ungzip(acir.clone()), &filename) { + Ok(_) => (), + Err(error) => println!("Error saving data: {}", error), + } + } +} + +/// Main function that generates test artifacts for SSA instructions +/// Creates test cases for various operations with different variable types and bit sizes +fn main() { + let args = Args::parse(); + + let mut all_artifacts: Vec = Vec::new(); + + // Define test variables with different types and sizes + let field_var = Variable{ variable_type: VariableType::Field, variable_size: 0}; + // max bit size for signed and unsigned + let u127_var = Variable{ variable_type: VariableType::Unsigned, variable_size: 127}; + let i127_var = Variable{ variable_type: VariableType::Signed, variable_size: 127}; + // max bit size allowed by mod and div + let u126_var = Variable{ variable_type: VariableType::Unsigned, variable_size: 126}; + let i126_var = Variable{ variable_type: VariableType::Signed, variable_size: 126}; + // 64 bit unsigned + let u64_var = Variable{ variable_type: VariableType::Unsigned, variable_size: 64}; + // 32 bit unsigned + let u32_var = Variable{ variable_type: VariableType::Unsigned, variable_size: 32}; + // 8 bit unsigned + let u8_var = Variable{ variable_type: VariableType::Unsigned, variable_size: 8}; + + // Test bitvector operations with max bit size (127 bits) + all_artifacts.push(InstructionArtifacts::new_add(&u127_var, &u127_var)); + all_artifacts.push(InstructionArtifacts::new_sub(&u127_var, &u127_var)); + all_artifacts.push(InstructionArtifacts::new_mul(&u127_var, &u127_var)); + all_artifacts.push(InstructionArtifacts::new_mod(&u126_var, &u126_var)); + all_artifacts.push(InstructionArtifacts::new_xor(&u127_var, &u127_var)); + all_artifacts.push(InstructionArtifacts::new_and(&u127_var, &u127_var)); + all_artifacts.push(InstructionArtifacts::new_div(&u126_var, &u126_var)); + all_artifacts.push(InstructionArtifacts::new_eq(&u127_var, &u127_var)); + all_artifacts.push(InstructionArtifacts::new_lt(&u127_var, &u127_var)); + all_artifacts.push(InstructionArtifacts::new_xor(&u127_var, &u127_var)); + all_artifacts.push(InstructionArtifacts::new_or(&u127_var, &u127_var)); + all_artifacts.push(InstructionArtifacts::new_not(&u127_var)); + all_artifacts.push(InstructionArtifacts::new_constrain(&u127_var)); + all_artifacts.push(InstructionArtifacts::new_truncate(&u127_var)); + all_artifacts.push(InstructionArtifacts::new_range_check(&u127_var)); + + // Test shift operations with smaller bit sizes + // shl truncates variable, so test different sizes + // Too heavy to test 127 bits, but it just multiplies or divides by 2^rhs + // Should work the same if div and mul are verified + all_artifacts.push(InstructionArtifacts::new_shl(&u64_var, &u8_var)); + all_artifacts.push(InstructionArtifacts::new_shr(&u64_var, &u8_var)); + all_artifacts.push(InstructionArtifacts::new_shl(&u32_var, &u8_var)); + + // Test binary operations with 32 bits + all_artifacts.push(InstructionArtifacts::new_xor(&u32_var, &u32_var)); + all_artifacts.push(InstructionArtifacts::new_and(&u32_var, &u32_var)); + all_artifacts.push(InstructionArtifacts::new_or(&u32_var, &u32_var)); + + // Test field operations + all_artifacts.push(InstructionArtifacts::new_add(&field_var, &field_var)); + all_artifacts.push(InstructionArtifacts::new_mul(&field_var, &field_var)); + all_artifacts.push(InstructionArtifacts::new_div(&field_var, &field_var)); + all_artifacts.push(InstructionArtifacts::new_eq(&field_var, &field_var)); + + // Test signed division (only operation that differs for signed integers) + all_artifacts.push(InstructionArtifacts::new_div(&i126_var, &i126_var)); + all_artifacts.push(InstructionArtifacts::new_lt(&i127_var, &i127_var)); + + save_artifacts(all_artifacts, &args.dir); +} From 71bcdf3fd10db1bf7ff6ed3a03b7a6d976638f84 Mon Sep 17 00:00:00 2001 From: jewelofchaos9 Date: Mon, 6 Jan 2025 12:18:24 +0000 Subject: [PATCH 2/4] cargo.toml + deleted gitignore --- Cargo.lock | 11 +++++++++++ Cargo.toml | 1 + compiler/noirc_evaluator/ssa_test/.gitignore | 1 - compiler/noirc_evaluator/ssa_test/Cargo.toml | 18 ++++++++++-------- 4 files changed, 22 insertions(+), 9 deletions(-) delete mode 100644 compiler/noirc_evaluator/ssa_test/.gitignore diff --git a/Cargo.lock b/Cargo.lock index eb6d4327faf..12581e53a33 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -4794,6 +4794,17 @@ dependencies = [ "der", ] +[[package]] +name = "ssa_test" +version = "1.0.0-beta.1" +dependencies = [ + "clap", + "flate2", + "noirc_evaluator", + "serde", + "serde_json", +] + [[package]] name = "stable_deref_trait" version = "1.2.0" diff --git a/Cargo.toml b/Cargo.toml index 73937667c14..8a0845e7bb6 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -10,6 +10,7 @@ members = [ "compiler/noirc_printable_type", "compiler/fm", "compiler/wasm", + "compiler/noirc_evaluator/ssa_test", # Crates related to tooling built on top of the Noir compiler "tooling/lsp", "tooling/debugger", diff --git a/compiler/noirc_evaluator/ssa_test/.gitignore b/compiler/noirc_evaluator/ssa_test/.gitignore deleted file mode 100644 index 03314f77b5a..00000000000 --- a/compiler/noirc_evaluator/ssa_test/.gitignore +++ /dev/null @@ -1 +0,0 @@ -Cargo.lock diff --git a/compiler/noirc_evaluator/ssa_test/Cargo.toml b/compiler/noirc_evaluator/ssa_test/Cargo.toml index 497f1baeab2..87f94063d2e 100644 --- a/compiler/noirc_evaluator/ssa_test/Cargo.toml +++ b/compiler/noirc_evaluator/ssa_test/Cargo.toml @@ -1,12 +1,14 @@ [package] name = "ssa_test" -version = "0.1.0" -edition = "2021" +version.workspace = true +authors.workspace = true +edition.workspace = true +rust-version.workspace = true +license.workspace = true [dependencies] -noirc_evaluator = {path = "../"} -serde = "1.0.214" -serde_json = "1.0.120" -flate2 = "1.0.35" -clap = { version = "4.4.11", features = ["derive"] } -[workspace] +noirc_evaluator.workspace = true +serde.workspace = true +serde_json.workspace = true +clap.workspace = true +flate2.workspace = true \ No newline at end of file From beb25dc83c429710f5b928fe0fa99f8847949046 Mon Sep 17 00:00:00 2001 From: jewelofchaos9 Date: Mon, 6 Jan 2025 12:29:30 +0000 Subject: [PATCH 3/4] delete question mark --- compiler/noirc_evaluator/src/acir_instruction_builder.rs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/compiler/noirc_evaluator/src/acir_instruction_builder.rs b/compiler/noirc_evaluator/src/acir_instruction_builder.rs index af0337e2e0d..e7759ec1698 100644 --- a/compiler/noirc_evaluator/src/acir_instruction_builder.rs +++ b/compiler/noirc_evaluator/src/acir_instruction_builder.rs @@ -262,7 +262,7 @@ fn range_check_function(variable_type: Type) -> Ssa { /// Creates an SSA function for truncate operations fn truncate_function(variable_type: Type) -> Ssa { - // truncate v0: field 10, 20?.. + // truncate v0: field to bit size 10 with max bit size 20. let main_id: Id = Id::new(0); let mut builder = FunctionBuilder::new("main".into(), main_id); From 99efe836ab2e06672252411b14ffb8553531e823 Mon Sep 17 00:00:00 2001 From: jewelofchaos9 Date: Mon, 6 Jan 2025 17:12:12 +0000 Subject: [PATCH 4/4] resloving --- Cargo.lock | 2 +- Cargo.toml | 2 +- .../{ssa_test => ssa_verification}/Cargo.toml | 2 +- .../{ssa_test => ssa_verification}/README.md | 0 .../src/main.rs | 33 +++++++++++++++---- 5 files changed, 30 insertions(+), 9 deletions(-) rename compiler/noirc_evaluator/{ssa_test => ssa_verification}/Cargo.toml (91%) rename compiler/noirc_evaluator/{ssa_test => ssa_verification}/README.md (100%) rename compiler/noirc_evaluator/{ssa_test => ssa_verification}/src/main.rs (79%) diff --git a/Cargo.lock b/Cargo.lock index 12581e53a33..7b5553b6e9b 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -4795,7 +4795,7 @@ dependencies = [ ] [[package]] -name = "ssa_test" +name = "ssa_verification" version = "1.0.0-beta.1" dependencies = [ "clap", diff --git a/Cargo.toml b/Cargo.toml index 8a0845e7bb6..904ace59e4f 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -10,7 +10,7 @@ members = [ "compiler/noirc_printable_type", "compiler/fm", "compiler/wasm", - "compiler/noirc_evaluator/ssa_test", + "compiler/noirc_evaluator/ssa_verification", # Crates related to tooling built on top of the Noir compiler "tooling/lsp", "tooling/debugger", diff --git a/compiler/noirc_evaluator/ssa_test/Cargo.toml b/compiler/noirc_evaluator/ssa_verification/Cargo.toml similarity index 91% rename from compiler/noirc_evaluator/ssa_test/Cargo.toml rename to compiler/noirc_evaluator/ssa_verification/Cargo.toml index 87f94063d2e..053134ce3d1 100644 --- a/compiler/noirc_evaluator/ssa_test/Cargo.toml +++ b/compiler/noirc_evaluator/ssa_verification/Cargo.toml @@ -1,5 +1,5 @@ [package] -name = "ssa_test" +name = "ssa_verification" version.workspace = true authors.workspace = true edition.workspace = true diff --git a/compiler/noirc_evaluator/ssa_test/README.md b/compiler/noirc_evaluator/ssa_verification/README.md similarity index 100% rename from compiler/noirc_evaluator/ssa_test/README.md rename to compiler/noirc_evaluator/ssa_verification/README.md diff --git a/compiler/noirc_evaluator/ssa_test/src/main.rs b/compiler/noirc_evaluator/ssa_verification/src/main.rs similarity index 79% rename from compiler/noirc_evaluator/ssa_test/src/main.rs rename to compiler/noirc_evaluator/ssa_verification/src/main.rs index dc02e9b3aa6..53a5954473a 100644 --- a/compiler/noirc_evaluator/ssa_test/src/main.rs +++ b/compiler/noirc_evaluator/ssa_verification/src/main.rs @@ -8,17 +8,35 @@ use::noirc_evaluator::acir_instruction_builder::{ }; use clap::Parser; +/// Command line arguments for the SSA test generator #[derive(Parser)] -#[command(author, version, about, long_about = None)] +#[command( + author, + version, + about = "Generates test artifacts for formally verifying SSA instructions and their conversion to ACIR", + long_about = "This tool generates test cases for various operations including: +- Bitvector operations (up to 127 bits): add, sub, mul, mod, xor, and, div, eq, lt, not +- Shift operations (32 and 64 bits): shl, shr +- Binary operations (32-bit): xor, and, or +- Field operations: add, mul, div +- Signed integer operations: div (126-bit) + +Each test case generates formatted SSA representation and serialized ACIR output. + +FLAGS: + -d, --dir Output directory for test artifacts [default: ../../../../../barretenberg/cpp/src/barretenberg/acir_formal_proofs/artifacts/]" +)] struct Args { + /// Output directory path for the generated test artifacts + /// Defaults to the barretenberg acir formal proofs artifacts directory #[arg(short, long, default_value = "../../../../../barretenberg/cpp/src/barretenberg/acir_formal_proofs/artifacts/")] dir: String, } /// Decompresses gzipped data into a byte vector -fn ungzip(compressed_data: Vec) -> Vec { +fn ungzip(compressed_data: &[u8]) -> Vec { let mut decompressed_data: Vec = Vec::new(); - let mut decoder = GzDecoder::new(&compressed_data[..]); + let mut decoder = GzDecoder::new(compressed_data); decoder.read_to_end(&mut decompressed_data).unwrap(); return decompressed_data; } @@ -35,12 +53,15 @@ fn save_to_file(data: &[u8], filename: &str) -> Result<(), std::io::Error> { /// Prints the formatted SSA for each artifact and saves the decompressed ACIR fn save_artifacts(all_artifacts: Vec, dir: &str) { for artifacts in all_artifacts.iter() { - println!("{}", artifacts.formatted_ssa); + println!("{}\n{}", artifacts.instruction_name, artifacts.formatted_ssa); let filename = format!("{}{}{}", dir, artifacts.instruction_name, ".acir"); let acir = &artifacts.serialized_acir; - match save_to_file(&ungzip(acir.clone()), &filename) { + match save_to_file(&ungzip(&acir), &filename) { Ok(_) => (), - Err(error) => println!("Error saving data: {}", error), + Err(error) => { + eprintln!("Error saving data: {}", error); + std::process::exit(1); + }, } } }