diff --git a/Cargo.lock b/Cargo.lock index 0c45e955d36..4c197dc148b 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -5502,6 +5502,18 @@ dependencies = [ "noirc_evaluator", ] +[[package]] +name = "ssa_verification" +version = "1.0.0-beta.6" +dependencies = [ + "acvm", + "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 66cbc34fb72..b420962d006 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -43,6 +43,7 @@ members = [ "tooling/ssa_fuzzer", "tooling/ssa_fuzzer/fuzzer", + "tooling/ssa_verification", "tooling/ssa_executor", "utils/protobuf", ] diff --git a/tooling/ssa_verification/Cargo.toml b/tooling/ssa_verification/Cargo.toml new file mode 100644 index 00000000000..9f27b523e50 --- /dev/null +++ b/tooling/ssa_verification/Cargo.toml @@ -0,0 +1,17 @@ + +[package] +name = "ssa_verification" +description = "CLI tool to generate input for SSA formal verification" +version.workspace = true +authors.workspace = true +edition.workspace = true +rust-version.workspace = true +license.workspace = true + +[dependencies] +noirc_evaluator.workspace = true +acvm.workspace = true +serde.workspace = true +serde_json.workspace = true +clap.workspace = true +flate2.workspace = true \ No newline at end of file diff --git a/tooling/ssa_verification/src/acir_instruction_builder.rs b/tooling/ssa_verification/src/acir_instruction_builder.rs new file mode 100644 index 00000000000..7ac61aed509 --- /dev/null +++ b/tooling/ssa_verification/src/acir_instruction_builder.rs @@ -0,0 +1,348 @@ +use acvm::{ + FieldElement, + acir::{ + circuit::{Circuit, ExpressionWidth, Program as AcirProgram}, + native_types::Witness, + }, +}; +use std::collections::BTreeSet; + +use noirc_evaluator::ssa::ssa_gen::Ssa; +use noirc_evaluator::ssa::{ + SsaEvaluatorOptions, ir::map::Id, optimize_ssa_builder_into_acir, primary_passes, + secondary_passes, +}; +use noirc_evaluator::ssa::{SsaLogging, ir::function::Function}; +use std::collections::HashMap; + +use noirc_evaluator::brillig::BrilligOptions; +use noirc_evaluator::ssa::{ + SsaBuilder, + function_builder::FunctionBuilder, + ir::{instruction::BinaryOp, types::Type}, +}; +use serde::{Deserialize, Serialize}; + +/// Represents artifacts generated from compiling an instruction +#[derive(Serialize, Deserialize)] +pub(crate) struct InstructionArtifacts { + /// Name of the instruction + pub(crate) instruction_name: String, + + /// SSA representation formatted as "acir(inline) {...}" + pub(crate) formatted_ssa: String, + + /// JSON serialized SSA + pub(crate) serialized_ssa: String, + + /// Gzipped bytes of ACIR program + pub(crate) serialized_acir: Vec, +} + +/// Represents the type of a variable in the instruction +#[derive(Debug)] +pub(crate) enum VariableType { + /// Field element type + Field, + /// Unsigned integer type + Unsigned, + /// Signed integer type + Signed, +} + +/// Represents a variable with its type and size information +pub(crate) struct Variable { + /// Type of the variable (Field, Unsigned, or Signed) + pub(crate) variable_type: VariableType, + /// Bit size of the variable (ignored for Field type) + pub(crate) variable_size: u32, +} + +impl Variable { + /// Gets a string representation of the variable's type and size + pub(crate) fn get_name(&self) -> String { + 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, + 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); + Self::new_by_ssa(ssa, instruction_name, variable) + } + + fn new_by_ssa(ssa: Ssa, instruction_name: String, variable: &Variable) -> Self { + 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, + serialized_ssa: serialized_ssa.to_string(), + serialized_acir: serialized_program, + } + } + + /// Creates a new constrain instruction artifact + pub(crate) fn new_constrain(variable: &Variable) -> Self { + Self::new_by_func(constrain_function, "Constrain".into(), variable) + } + + /// Creates a new NOT operation instruction artifact + pub(crate) fn new_not(variable: &Variable) -> Self { + Self::new_by_func(not_function, "Not".into(), variable) + } + + /// Creates a new range check instruction artifact + pub(crate) fn new_range_check(variable: &Variable, bit_size: u32) -> Self { + let ssa = range_check_function(Self::get_type(variable), bit_size); + Self::new_by_ssa(ssa, "RangeCheck".into(), variable) + } + + /// Creates a new truncate instruction artifact + pub(crate) fn new_truncate(variable: &Variable, bit_size: u32, max_bit_size: u32) -> Self { + let ssa = truncate_function(Self::get_type(variable), bit_size, max_bit_size); + Self::new_by_ssa(ssa, "Truncate".into(), variable) + } + + /// Creates a new ADD operation instruction artifact + pub(crate) fn new_add(first_variable: &Variable, second_variable: &Variable) -> Self { + Self::new_binary( + BinaryOp::Add { unchecked: false }, + "Binary::Add".into(), + first_variable, + second_variable, + ) + } + + /// Creates a new SUB operation instruction artifact + pub(crate) fn new_sub(first_variable: &Variable, second_variable: &Variable) -> Self { + Self::new_binary( + BinaryOp::Sub { unchecked: false }, + "Binary::Sub".into(), + first_variable, + second_variable, + ) + } + + /// Creates a new XOR operation instruction artifact + pub(crate) fn new_xor(first_variable: &Variable, second_variable: &Variable) -> Self { + Self::new_binary(BinaryOp::Xor, "Binary::Xor".into(), first_variable, second_variable) + } + + /// Creates a new AND operation instruction artifact + pub(crate) fn new_and(first_variable: &Variable, second_variable: &Variable) -> Self { + Self::new_binary(BinaryOp::And, "Binary::And".into(), first_variable, second_variable) + } + + /// Creates a new OR operation instruction artifact + pub(crate) fn new_or(first_variable: &Variable, second_variable: &Variable) -> Self { + Self::new_binary(BinaryOp::Or, "Binary::Or".into(), first_variable, second_variable) + } + + /// Creates a new less than operation instruction artifact + pub(crate) fn new_lt(first_variable: &Variable, second_variable: &Variable) -> Self { + Self::new_binary(BinaryOp::Lt, "Binary::Lt".into(), first_variable, second_variable) + } + + /// Creates a new equals operation instruction artifact + pub(crate) fn new_eq(first_variable: &Variable, second_variable: &Variable) -> Self { + Self::new_binary(BinaryOp::Eq, "Binary::Eq".into(), first_variable, second_variable) + } + + /// Creates a new modulo operation instruction artifact + pub(crate) fn new_mod(first_variable: &Variable, second_variable: &Variable) -> Self { + Self::new_binary(BinaryOp::Mod, "Binary::Mod".into(), first_variable, second_variable) + } + + /// Creates a new multiply operation instruction artifact + pub(crate) fn new_mul(first_variable: &Variable, second_variable: &Variable) -> Self { + Self::new_binary( + BinaryOp::Mul { unchecked: false }, + "Binary::Mul".into(), + first_variable, + second_variable, + ) + } + + /// Creates a new divide operation instruction artifact + pub(crate) fn new_div(first_variable: &Variable, second_variable: &Variable) -> Self { + Self::new_binary(BinaryOp::Div, "Binary::Div".into(), first_variable, second_variable) + } + + /// Creates a new shift left operation instruction artifact + pub(crate) fn new_shl(first_variable: &Variable, second_variable: &Variable) -> Self { + Self::new_binary(BinaryOp::Shl, "Binary::Shl".into(), first_variable, second_variable) + } + + /// Creates a new shift right operation instruction artifact + pub(crate) fn new_shr(first_variable: &Variable, second_variable: &Variable) -> Self { + 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 builder = SsaBuilder { + ssa, + ssa_logging: SsaLogging::None, + print_codegen_timings: false, + passed: HashMap::default(), + skip_passes: vec![], + }; + let ssa_evaluator_options = SsaEvaluatorOptions { + ssa_logging: SsaLogging::None, + print_codegen_timings: false, + expression_width: ExpressionWidth::default(), + emit_ssa: { None }, + skip_underconstrained_check: true, + skip_brillig_constraints_check: true, + inliner_aggressiveness: 0, + max_bytecode_increase_percent: None, + brillig_options: BrilligOptions::default(), + enable_brillig_constraints_check_lookback: false, + skip_passes: vec![], + }; + let (acir_functions, brillig, _, _) = match optimize_ssa_builder_into_acir( + builder, + &ssa_evaluator_options, + &primary_passes(&ssa_evaluator_options), + secondary_passes, + ) { + Ok(artifacts_and_warnings) => artifacts_and_warnings.0, + Err(_) => panic!("Should compile manually generated 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(); + + private_params.extend(ret_values.iter().cloned()); + let circuit: Circuit = Circuit { + current_witness_index: acir_func.current_witness_index().witness_index(), + opcodes: acir_func.opcodes.clone(), + private_parameters: private_params.clone(), + ..Circuit::::default() + }; + functions.push(circuit); + } + AcirProgram { 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]); + + builder.finish() +} + +/// 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]); + + builder.finish() +} + +/// Creates an SSA function for range check operations +fn range_check_function(variable_type: Type, bit_size: u32) -> 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, bit_size, Some("Range Check failed".to_string())); + builder.terminate_with_return(vec![v0]); + + builder.finish() +} + +/// Creates an SSA function for truncate operations +fn truncate_function(variable_type: Type, bit_size: u32, max_bit_size: u32) -> Ssa { + 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, bit_size, max_bit_size); + builder.terminate_with_return(vec![v1]); + + 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]); + + builder.finish() +} diff --git a/tooling/ssa_verification/src/main.rs b/tooling/ssa_verification/src/main.rs new file mode 100644 index 00000000000..7605de4c063 --- /dev/null +++ b/tooling/ssa_verification/src/main.rs @@ -0,0 +1,142 @@ +mod acir_instruction_builder; +use crate::acir_instruction_builder::{InstructionArtifacts, Variable, VariableType}; +use clap::Parser; +use flate2::read::GzDecoder; +use std::fs::File; +use std::io::Read; +use std::io::Write; +use std::path::Path; + +/// 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." +)] +struct Args { + /// Output directory path for the generated test artifacts + /// Defaults to the barretenberg acir formal proofs artifacts directory + #[arg(short, long, default_value = "/tmp/")] + 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(); + 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 u128_var = Variable { variable_type: VariableType::Unsigned, variable_size: 128 }; + let i128_var = Variable { variable_type: VariableType::Signed, variable_size: 128 }; + let i127_var = Variable { variable_type: VariableType::Signed, variable_size: 127 }; + // 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 }; + + // Tests for bitvector operations with max bit size (128 bits) + all_artifacts.push(InstructionArtifacts::new_add(&u128_var, &u128_var)); + all_artifacts.push(InstructionArtifacts::new_sub(&u128_var, &u128_var)); + all_artifacts.push(InstructionArtifacts::new_mul(&u128_var, &u128_var)); + all_artifacts.push(InstructionArtifacts::new_mod(&u128_var, &u128_var)); + all_artifacts.push(InstructionArtifacts::new_xor(&u128_var, &u128_var)); + all_artifacts.push(InstructionArtifacts::new_and(&u128_var, &u128_var)); + all_artifacts.push(InstructionArtifacts::new_div(&u128_var, &u128_var)); + all_artifacts.push(InstructionArtifacts::new_eq(&u128_var, &u128_var)); + all_artifacts.push(InstructionArtifacts::new_lt(&u128_var, &u128_var)); + all_artifacts.push(InstructionArtifacts::new_xor(&u128_var, &u128_var)); + all_artifacts.push(InstructionArtifacts::new_or(&u128_var, &u128_var)); + all_artifacts.push(InstructionArtifacts::new_not(&u128_var)); + all_artifacts.push(InstructionArtifacts::new_constrain(&u128_var)); + all_artifacts.push(InstructionArtifacts::new_truncate(&u128_var, 10, 20)); + all_artifacts.push(InstructionArtifacts::new_range_check(&u128_var, 64)); + // Tests for signed operations with max bit size (128 bits) + all_artifacts.push(InstructionArtifacts::new_add(&i128_var, &i128_var)); + all_artifacts.push(InstructionArtifacts::new_sub(&i128_var, &i128_var)); + all_artifacts.push(InstructionArtifacts::new_mul(&i128_var, &i128_var)); + all_artifacts.push(InstructionArtifacts::new_mod(&i127_var, &i127_var)); + all_artifacts.push(InstructionArtifacts::new_xor(&i128_var, &i128_var)); + all_artifacts.push(InstructionArtifacts::new_and(&i128_var, &i128_var)); + all_artifacts.push(InstructionArtifacts::new_div(&i127_var, &i127_var)); + all_artifacts.push(InstructionArtifacts::new_eq(&i128_var, &i128_var)); + all_artifacts.push(InstructionArtifacts::new_lt(&i127_var, &i127_var)); + all_artifacts.push(InstructionArtifacts::new_xor(&i128_var, &i128_var)); + all_artifacts.push(InstructionArtifacts::new_or(&i128_var, &i128_var)); + all_artifacts.push(InstructionArtifacts::new_not(&i128_var)); + all_artifacts.push(InstructionArtifacts::new_constrain(&i128_var)); + all_artifacts.push(InstructionArtifacts::new_truncate(&i128_var, 10, 20)); + all_artifacts.push(InstructionArtifacts::new_range_check(&i128_var, 64)); + + // 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(&i127_var, &i127_var)); + all_artifacts.push(InstructionArtifacts::new_lt(&i127_var, &i127_var)); + + save_artifacts(all_artifacts, &args.dir); +}