acir_loader.test.cpp File Reference

Tests for verifying ACIR (Arithmetic Circuit Intermediate Representation) operations. More...

#include "acir_loader.hpp"
#include "barretenberg/circuit_checker/circuit_checker.hpp"
#include "barretenberg/common/test.hpp"
#include "barretenberg/dsl/acir_format/acir_format.hpp"
#include "barretenberg/smt_verification/circuit/ultra_circuit.hpp"
#include "barretenberg/smt_verification/solver/solver.hpp"
#include "barretenberg/smt_verification/util/smt_util.hpp"
#include "barretenberg/stdlib/client_ivc_verifier/client_ivc_recursive_verifier.hpp"
#include "barretenberg/stdlib_circuit_builders/ultra_circuit_builder.hpp"
#include "formal_proofs.hpp"
#include "helpers.hpp"
#include <vector>

Go to the source code of this file.

Functions
void	save_buggy_witness (std::string instruction_name, smt_circuit::UltraCircuit circuit)
	Saves witness data when a bug is found during verification.
bool	verify_buggy_witness (std::string instruction_name)
	Verifies a previously saved witness file for correctness.
	TEST (acir_formal_proofs, uint_terms_add)
	Tests 127-bit unsigned addition Verifies that the ACIR implementation of addition is correct Execution time: ~2.8 seconds on SMTBOX.
	TEST (acir_formal_proofs, uint_terms_and)
	Tests 127-bit unsigned bitwise AND Verifies that the ACIR implementation of AND is correct.
	TEST (acir_formal_proofs, uint_terms_and32)
	Tests 32-bit unsigned bitwise AND Verifies that the ACIR implementation of AND is correct Execution time: ~6.7 seconds on SMTBOX.
	TEST (acir_formal_proofs, uint_terms_div)
	Tests 126-bit unsigned division Verifies that the ACIR implementation of division is correct.
	TEST (acir_formal_proofs, uint_terms_eq)
	Tests 127-bit unsigned equality comparison Verifies two cases:
	TEST (acir_formal_proofs, uint_terms_lt)
	Tests 127-bit unsigned less than comparison Verifies two cases:
	TEST (acir_formal_proofs, uint_terms_mod)
	Tests 126-bit unsigned modulo Verifies that the ACIR implementation of modulo is correct Execution time: ??? seconds on SMTBOX.
	TEST (acir_formal_proofs, uint_terms_mul)
	Tests 127-bit unsigned multiplication Verifies that the ACIR implementation of multiplication is correct Execution time: ~10.0 seconds on SMTBOX.
	TEST (acir_formal_proofs, uint_terms_or)
	Tests 127-bit unsigned bitwise OR Verifies that the ACIR implementation of OR is correct.
	TEST (acir_formal_proofs, uint_terms_or32)
	Tests 32-bit unsigned bitwise OR Verifies that the ACIR implementation of OR is correct Execution time: ~20.3 seconds on SMTBOX.
	TEST (acir_formal_proofs, uint_terms_shl64)
	Tests 64-bit left shift Verifies that the ACIR implementation of left shift is correct Execution time: ~4588 seconds on SMTBOX Memory usage: ~30GB RAM.
	TEST (acir_formal_proofs, uint_terms_shl32)
	Tests 32-bit left shift Verifies that the ACIR implementation of left shift is correct Execution time: ~4574 seconds on SMTBOX Memory usage: ~30GB RAM.
	TEST (acir_formal_proofs, uint_terms_shr)
	Tests right shift operation Verifies that the ACIR implementation of right shift is correct Execution time: ~3927.88 seconds on SMTBOX Memory usage: ~10GB RAM.
	TEST (acir_formal_proofs, uint_terms_sub)
	Tests 127-bit unsigned subtraction Verifies that the ACIR implementation of subtraction is correct Execution time: ~2.6 seconds on SMTBOX.
	TEST (acir_formal_proofs, uint_terms_xor)
	Tests 127-bit unsigned bitwise XOR Verifies that the ACIR implementation of XOR is correct.
	TEST (acir_formal_proofs, uint_terms_xor32)
	Tests 32-bit unsigned bitwise XOR Verifies that the ACIR implementation of XOR is correct.
	TEST (acir_formal_proofs, uint_terms_not)
	Tests 127-bit unsigned bitwise NOT Verifies that the ACIR implementation of NOT is correct Execution time: ~21.3 seconds on SMTBOX.
	TEST (acir_formal_proofs, field_terms_add)
	Tests field addition Verifies that the ACIR implementation of field addition is correct Execution time: ~0.22 seconds on SMTBOX.
	TEST (acir_formal_proofs, field_terms_div)
	Tests field division Verifies that the ACIR implementation of field division is correct Execution time: ~0.22 seconds on SMTBOX.
	TEST (acir_formal_proofs, field_terms_eq)
	Tests field equality comparison Verifies two cases:
	TEST (acir_formal_proofs, field_terms_mul)
	Tests field multiplication Verifies that the ACIR implementation of field multiplication is correct Execution time: ~0.22 seconds on SMTBOX.
	TEST (acir_formal_proofs, integer_terms_div)
	Tests 126-bit signed division Verifies that the ACIR implementation of signed division is correct Execution time: >17 DAYS on SMTBOX.
	TEST (acir_formal_proofs, non_uniqueness_for_casts_field_to_u64)
	Tests non-uniqueness for casts Verifies that the ACIR implementation of casts is correct Field -> u64.
	TEST (acir_formal_proofs, non_uniqueness_for_casts_u64_to_u8)
	Tests non-uniqueness for casts Verifies that the ACIR implementation of casts is correct u64 -> u8.
	TEST (acir_formal_proofs, non_uniqueness_for_casts_u8_to_u64)
	Tests non-uniqueness for casts Verifies that the ACIR implementation of casts is correct u8 -> u64.

Variables
const std::string	ARTIFACTS_PATH = "/tmp/"

Detailed Description

Tests for verifying ACIR (Arithmetic Circuit Intermediate Representation) operations.

This test suite verifies the correctness of various arithmetic, logical, and bitwise operations implemented in ACIR format. It uses SMT solvers to formally verify the operations.

Definition in file acir_loader.test.cpp.

Function Documentation

save_buggy_witness()

void save_buggy_witness	(	std::string	instruction_name,
		smt_circuit::UltraCircuit	circuit
	)

Saves witness data when a bug is found during verification.

Parameters

instruction_name	Name of the instruction being tested
circuit	The circuit containing the bug

Saves witness data to a file named {instruction_name}.witness in the artifacts directory

Definition at line 32 of file acir_loader.test.cpp.

TEST() [1/25]

TEST	(	acir_formal_proofs	,
		field_terms_add
	)

Tests field addition Verifies that the ACIR implementation of field addition is correct Execution time: ~0.22 seconds on SMTBOX.

Definition at line 395 of file acir_loader.test.cpp.

TEST() [2/25]

TEST	(	acir_formal_proofs	,
		field_terms_div
	)

Tests field division Verifies that the ACIR implementation of field division is correct Execution time: ~0.22 seconds on SMTBOX.

Definition at line 413 of file acir_loader.test.cpp.

TEST() [3/25]

TEST	(	acir_formal_proofs	,
		field_terms_eq
	)

Tests field equality comparison Verifies two cases:

1. When operands are equal, result must be 0
2. When operands are not equal, result must be 1 Execution time: ~19.2 seconds on SMTBOX

Definition at line 433 of file acir_loader.test.cpp.

TEST() [4/25]

TEST	(	acir_formal_proofs	,
		field_terms_mul
	)

Tests field multiplication Verifies that the ACIR implementation of field multiplication is correct Execution time: ~0.22 seconds on SMTBOX.

Definition at line 461 of file acir_loader.test.cpp.

TEST() [5/25]

TEST	(	acir_formal_proofs	,
		integer_terms_div
	)

Tests 126-bit signed division Verifies that the ACIR implementation of signed division is correct Execution time: >17 DAYS on SMTBOX.

Definition at line 479 of file acir_loader.test.cpp.

TEST() [6/25]

TEST	(	acir_formal_proofs	,
		non_uniqueness_for_casts_field_to_u64
	)

Tests non-uniqueness for casts Verifies that the ACIR implementation of casts is correct Field -> u64.

Definition at line 496 of file acir_loader.test.cpp.

TEST() [7/25]

TEST	(	acir_formal_proofs	,
		non_uniqueness_for_casts_u64_to_u8
	)

Tests non-uniqueness for casts Verifies that the ACIR implementation of casts is correct u64 -> u8.

Definition at line 509 of file acir_loader.test.cpp.

TEST() [8/25]

TEST	(	acir_formal_proofs	,
		non_uniqueness_for_casts_u8_to_u64
	)

Tests non-uniqueness for casts Verifies that the ACIR implementation of casts is correct u8 -> u64.

Definition at line 522 of file acir_loader.test.cpp.

TEST() [9/25]

TEST	(	acir_formal_proofs	,
		uint_terms_add
	)

Tests 127-bit unsigned addition Verifies that the ACIR implementation of addition is correct Execution time: ~2.8 seconds on SMTBOX.

Definition at line 65 of file acir_loader.test.cpp.

TEST() [10/25]

TEST	(	acir_formal_proofs	,
		uint_terms_and
	)

Tests 127-bit unsigned bitwise AND Verifies that the ACIR implementation of AND is correct.

Definition at line 83 of file acir_loader.test.cpp.

TEST() [11/25]

TEST	(	acir_formal_proofs	,
		uint_terms_and32
	)

Tests 32-bit unsigned bitwise AND Verifies that the ACIR implementation of AND is correct Execution time: ~6.7 seconds on SMTBOX.

Definition at line 101 of file acir_loader.test.cpp.

TEST() [12/25]

TEST	(	acir_formal_proofs	,
		uint_terms_div
	)

Tests 126-bit unsigned division Verifies that the ACIR implementation of division is correct.

Definition at line 118 of file acir_loader.test.cpp.

TEST() [13/25]

TEST	(	acir_formal_proofs	,
		uint_terms_eq
	)

Tests 127-bit unsigned equality comparison Verifies two cases:

1. When operands are equal, result must be 0
2. When operands are not equal, result must be 1 Execution time: ~22.8 seconds on SMTBOX

Definition at line 138 of file acir_loader.test.cpp.

TEST() [14/25]

TEST	(	acir_formal_proofs	,
		uint_terms_lt
	)

Tests 127-bit unsigned less than comparison Verifies two cases:

1. When a < b, result must be 0
2. When a >= b, result must be 1 Execution time: ~81.7 seconds on SMTBOX

Definition at line 168 of file acir_loader.test.cpp.

TEST() [15/25]

TEST	(	acir_formal_proofs	,
		uint_terms_mod
	)

Tests 126-bit unsigned modulo Verifies that the ACIR implementation of modulo is correct Execution time: ??? seconds on SMTBOX.

Definition at line 196 of file acir_loader.test.cpp.

TEST() [16/25]

TEST	(	acir_formal_proofs	,
		uint_terms_mul
	)

Tests 127-bit unsigned multiplication Verifies that the ACIR implementation of multiplication is correct Execution time: ~10.0 seconds on SMTBOX.

Definition at line 215 of file acir_loader.test.cpp.

TEST() [17/25]

TEST	(	acir_formal_proofs	,
		uint_terms_not
	)

Tests 127-bit unsigned bitwise NOT Verifies that the ACIR implementation of NOT is correct Execution time: ~21.3 seconds on SMTBOX.

Definition at line 377 of file acir_loader.test.cpp.

TEST() [18/25]

TEST	(	acir_formal_proofs	,
		uint_terms_or
	)

Tests 127-bit unsigned bitwise OR Verifies that the ACIR implementation of OR is correct.

Definition at line 232 of file acir_loader.test.cpp.

TEST() [19/25]

TEST	(	acir_formal_proofs	,
		uint_terms_or32
	)

Tests 32-bit unsigned bitwise OR Verifies that the ACIR implementation of OR is correct Execution time: ~20.3 seconds on SMTBOX.

Definition at line 250 of file acir_loader.test.cpp.

TEST() [20/25]

TEST	(	acir_formal_proofs	,
		uint_terms_shl32
	)

Tests 32-bit left shift Verifies that the ACIR implementation of left shift is correct Execution time: ~4574 seconds on SMTBOX Memory usage: ~30GB RAM.

Definition at line 288 of file acir_loader.test.cpp.

TEST() [21/25]

TEST	(	acir_formal_proofs	,
		uint_terms_shl64
	)

Tests 64-bit left shift Verifies that the ACIR implementation of left shift is correct Execution time: ~4588 seconds on SMTBOX Memory usage: ~30GB RAM.

Definition at line 269 of file acir_loader.test.cpp.

TEST() [22/25]

TEST	(	acir_formal_proofs	,
		uint_terms_shr
	)

Tests right shift operation Verifies that the ACIR implementation of right shift is correct Execution time: ~3927.88 seconds on SMTBOX Memory usage: ~10GB RAM.

Definition at line 307 of file acir_loader.test.cpp.

TEST() [23/25]

TEST	(	acir_formal_proofs	,
		uint_terms_sub
	)

Tests 127-bit unsigned subtraction Verifies that the ACIR implementation of subtraction is correct Execution time: ~2.6 seconds on SMTBOX.

Definition at line 325 of file acir_loader.test.cpp.

TEST() [24/25]

TEST	(	acir_formal_proofs	,
		uint_terms_xor
	)

Tests 127-bit unsigned bitwise XOR Verifies that the ACIR implementation of XOR is correct.

Definition at line 342 of file acir_loader.test.cpp.

TEST() [25/25]

TEST	(	acir_formal_proofs	,
		uint_terms_xor32
	)

Tests 32-bit unsigned bitwise XOR Verifies that the ACIR implementation of XOR is correct.

Definition at line 359 of file acir_loader.test.cpp.

verify_buggy_witness()

bool verify_buggy_witness

(

std::string

instruction_name

)

Verifies a previously saved witness file for correctness.

Parameters

instruction_name

Name of the instruction to verify

Returns

true if witness is valid, false otherwise

Loads a witness file and verifies it against the corresponding ACIR program

Definition at line 46 of file acir_loader.test.cpp.

Variable Documentation

ARTIFACTS_PATH

const std::string ARTIFACTS_PATH = "/tmp/"

Definition at line 23 of file acir_loader.test.cpp.