diff --git a/Cargo.lock b/Cargo.lock index eb6d4327faf..7b5553b6e9b 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -4794,6 +4794,17 @@ dependencies = [ "der", ] +[[package]] +name = "ssa_verification" +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..904ace59e4f 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -10,6 +10,7 @@ members = [ "compiler/noirc_printable_type", "compiler/fm", "compiler/wasm", + "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/src/acir_instruction_builder.rs b/compiler/noirc_evaluator/src/acir_instruction_builder.rs new file mode 100644 index 00000000000..e7759ec1698 --- /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 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); + + 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_verification/Cargo.toml b/compiler/noirc_evaluator/ssa_verification/Cargo.toml new file mode 100644 index 00000000000..053134ce3d1 --- /dev/null +++ b/compiler/noirc_evaluator/ssa_verification/Cargo.toml @@ -0,0 +1,14 @@ +[package] +name = "ssa_verification" +version.workspace = true +authors.workspace = true +edition.workspace = true +rust-version.workspace = true +license.workspace = true + +[dependencies] +noirc_evaluator.workspace = true +serde.workspace = true +serde_json.workspace = true +clap.workspace = true +flate2.workspace = true \ No newline at end of file diff --git a/compiler/noirc_evaluator/ssa_verification/README.md b/compiler/noirc_evaluator/ssa_verification/README.md new file mode 100644 index 00000000000..a2e3b47af72 --- /dev/null +++ b/compiler/noirc_evaluator/ssa_verification/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_verification/src/main.rs b/compiler/noirc_evaluator/ssa_verification/src/main.rs new file mode 100644 index 00000000000..53a5954473a --- /dev/null +++ b/compiler/noirc_evaluator/ssa_verification/src/main.rs @@ -0,0 +1,132 @@ +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; + +/// Command line arguments for the SSA test generator +#[derive(Parser)] +#[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: &[u8]) -> 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!("{}\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), &filename) { + Ok(_) => (), + Err(error) => { + eprintln!("Error saving data: {}", error); + std::process::exit(1); + }, + } + } +} + +/// 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); +}