formal_proofs.hpp File Reference

#include "acir_loader.hpp"
#include "barretenberg/smt_verification/circuit/ultra_circuit.hpp"
#include "barretenberg/smt_verification/solver/solver.hpp"
#include "cvc5/cvc5.h"
#include <string>
#include <unordered_map>

Go to the source code of this file.

Functions
void	debug_solution (smt_solver::Solver *solver, std::unordered_map< std::string, cvc5::Term > terms)
	Debug helper to print solver assertions and model values.
bool	verify_add (smt_solver::Solver *solver, smt_circuit::UltraCircuit circuit)
	Verify addition operation: c = a + b.
bool	verify_sub (smt_solver::Solver *solver, smt_circuit::UltraCircuit circuit)
	Verify subtraction operation: c = a - b.
bool	verify_mul (smt_solver::Solver *solver, smt_circuit::UltraCircuit circuit)
	Verify multiplication operation: c = a * b.
bool	verify_div (smt_solver::Solver *solver, smt_circuit::UltraCircuit circuit)
	Verify integer division operation: c = a / b.
bool	verify_div_field (smt_solver::Solver *solver, smt_circuit::UltraCircuit circuit)
	Verify field division operation: c = a / b (in field)
bool	verify_mod (smt_solver::Solver *solver, smt_circuit::UltraCircuit circuit)
	Verify modulo operation: c = a mod b.
bool	verify_or (smt_solver::Solver *solver, smt_circuit::UltraCircuit circuit)
	Verify bitwise OR operation: c = a | b.
bool	verify_and (smt_solver::Solver *solver, smt_circuit::UltraCircuit circuit)
	Verify bitwise AND operation: c = a & b.
bool	verify_xor (smt_solver::Solver *solver, smt_circuit::UltraCircuit circuit)
	Verify bitwise XOR operation: c = a ^ b.
bool	verify_not_127 (smt_solver::Solver *solver, smt_circuit::UltraCircuit circuit)
	Verify NOT operation on 127 bits: b = ~a.
bool	verify_shl32 (smt_solver::Solver *solver, smt_circuit::UltraCircuit circuit)
	Verify 32-bit left shift operation: c = a << b.
bool	verify_shl64 (smt_solver::Solver *solver, smt_circuit::UltraCircuit circuit)
	Verify 64-bit left shift operation: c = a << b.
bool	verify_shr (smt_solver::Solver *solver, smt_circuit::UltraCircuit circuit)
	Verify right shift operation: c = a >> b.
bool	verify_eq_on_equlaity (smt_solver::Solver *solver, smt_circuit::UltraCircuit circuit)
	Verify equality comparison when values are equal.
bool	verify_eq_on_inequlaity (smt_solver::Solver *solver, smt_circuit::UltraCircuit circuit)
	Verify equality comparison when values are not equal.
bool	verify_lt (smt_solver::Solver *solver, smt_circuit::UltraCircuit circuit)
	Verify less than comparison: a < b.
bool	verify_gt (smt_solver::Solver *solver, smt_circuit::UltraCircuit circuit)
	Verify greater than comparison: a > b.
bool	verify_non_uniqueness_for_casts (smt_solver::Solver *solver, AcirToSmtLoader *loader, smt_circuit::TermType type)
	Verify non-uniqueness for casts.

Function Documentation

debug_solution()

void debug_solution	(	smt_solver::Solver *	solver,
		std::unordered_map< std::string, cvc5::Term >	terms
	)

Debug helper to print solver assertions and model values.

Parameters

solver	SMT solver instance
terms	Map of term names to CVC5 terms to evaluate

Definition at line 7 of file formal_proofs.cpp.

verify_add()

bool verify_add	(	smt_solver::Solver *	solver,
		smt_circuit::UltraCircuit	circuit
	)

Verify addition operation: c = a + b.

Parameters

solver	SMT solver instance
circuit	Circuit containing variables a, b, c

Returns

true if a counterexample is found (verification fails)

Definition at line 16 of file formal_proofs.cpp.

verify_and()

bool verify_and	(	smt_solver::Solver *	solver,
		smt_circuit::UltraCircuit	circuit
	)

Verify bitwise AND operation: c = a & b.

Parameters

solver	SMT solver instance
circuit	Circuit containing variables a, b, c

Returns

true if a counterexample is found (verification fails)

Definition at line 123 of file formal_proofs.cpp.

verify_div()

bool verify_div	(	smt_solver::Solver *	solver,
		smt_circuit::UltraCircuit	circuit
	)

Verify integer division operation: c = a / b.

Parameters

solver	SMT solver instance
circuit	Circuit containing variables a, b, c

Returns

true if a counterexample is found (verification fails)

Definition at line 61 of file formal_proofs.cpp.

verify_div_field()

bool verify_div_field	(	smt_solver::Solver *	solver,
		smt_circuit::UltraCircuit	circuit
	)

Verify field division operation: c = a / b (in field)

Parameters

solver	SMT solver instance
circuit	Circuit containing variables a, b, c

Returns

true if a counterexample is found (verification fails)

Definition at line 76 of file formal_proofs.cpp.

verify_eq_on_equlaity()

bool verify_eq_on_equlaity	(	smt_solver::Solver *	solver,
		smt_circuit::UltraCircuit	circuit
	)

Verify equality comparison when values are equal.

Parameters

solver	SMT solver instance
circuit	Circuit containing variables a, b, c

Returns

true if a counterexample is found (verification fails)

Definition at line 215 of file formal_proofs.cpp.

verify_eq_on_inequlaity()

bool verify_eq_on_inequlaity	(	smt_solver::Solver *	solver,
		smt_circuit::UltraCircuit	circuit
	)

Verify equality comparison when values are not equal.

Parameters

solver	SMT solver instance
circuit	Circuit containing variables a, b, c

Returns

true if a counterexample is found (verification fails)

Definition at line 230 of file formal_proofs.cpp.

verify_gt()

bool verify_gt	(	smt_solver::Solver *	solver,
		smt_circuit::UltraCircuit	circuit
	)

Verify greater than comparison: a > b.

Parameters

solver	SMT solver instance
circuit	Circuit containing variables a, b, c

Returns

true if a counterexample is found (verification fails)

Definition at line 260 of file formal_proofs.cpp.

verify_lt()

bool verify_lt	(	smt_solver::Solver *	solver,
		smt_circuit::UltraCircuit	circuit
	)

Verify less than comparison: a < b.

Parameters

solver	SMT solver instance
circuit	Circuit containing variables a, b, c

Returns

true if a counterexample is found (verification fails)

Definition at line 245 of file formal_proofs.cpp.

verify_mod()

bool verify_mod	(	smt_solver::Solver *	solver,
		smt_circuit::UltraCircuit	circuit
	)

Verify modulo operation: c = a mod b.

Parameters

solver	SMT solver instance
circuit	Circuit containing variables a, b, c

Returns

true if a counterexample is found (verification fails)

Definition at line 93 of file formal_proofs.cpp.

verify_mul()

bool verify_mul	(	smt_solver::Solver *	solver,
		smt_circuit::UltraCircuit	circuit
	)

Verify multiplication operation: c = a * b.

Parameters

solver	SMT solver instance
circuit	Circuit containing variables a, b, c

Returns

true if a counterexample is found (verification fails)

Definition at line 46 of file formal_proofs.cpp.

verify_non_uniqueness_for_casts()

bool verify_non_uniqueness_for_casts	(	smt_solver::Solver *	solver,
		AcirToSmtLoader *	loader,
		smt_circuit::TermType	type
	)

Verify non-uniqueness for casts.

Parameters

solver	SMT solver instance
loader	ACIR loader instance
type	Type of term to verify non-uniqueness for

Returns

true if a counterexample is found (verification fails)

Definition at line 290 of file formal_proofs.cpp.

verify_not_127()

bool verify_not_127	(	smt_solver::Solver *	solver,
		smt_circuit::UltraCircuit	circuit
	)

Verify NOT operation on 127 bits: b = ~a.

Parameters

solver	SMT solver instance
circuit	Circuit containing variables a, b

Returns

true if a counterexample is found (verification fails)

Definition at line 154 of file formal_proofs.cpp.

verify_or()

bool verify_or	(	smt_solver::Solver *	solver,
		smt_circuit::UltraCircuit	circuit
	)

Verify bitwise OR operation: c = a | b.

Parameters

solver	SMT solver instance
circuit	Circuit containing variables a, b, c

Returns

true if a counterexample is found (verification fails)

Definition at line 108 of file formal_proofs.cpp.

verify_shl32()

bool verify_shl32	(	smt_solver::Solver *	solver,
		smt_circuit::UltraCircuit	circuit
	)

Verify 32-bit left shift operation: c = a << b.

Parameters

solver	SMT solver instance
circuit	Circuit containing variables a, b, c

Returns

true if a counterexample is found (verification fails)

Definition at line 170 of file formal_proofs.cpp.

verify_shl64()

bool verify_shl64	(	smt_solver::Solver *	solver,
		smt_circuit::UltraCircuit	circuit
	)

Verify 64-bit left shift operation: c = a << b.

Parameters

solver	SMT solver instance
circuit	Circuit containing variables a, b, c

Returns

true if a counterexample is found (verification fails)

Definition at line 185 of file formal_proofs.cpp.

verify_shr()

bool verify_shr	(	smt_solver::Solver *	solver,
		smt_circuit::UltraCircuit	circuit
	)

Verify right shift operation: c = a >> b.

Parameters

solver	SMT solver instance
circuit	Circuit containing variables a, b, c

Returns

true if a counterexample is found (verification fails)

Definition at line 200 of file formal_proofs.cpp.

verify_sub()

bool verify_sub	(	smt_solver::Solver *	solver,
		smt_circuit::UltraCircuit	circuit
	)

Verify subtraction operation: c = a - b.

Parameters

solver	SMT solver instance
circuit	Circuit containing variables a, b, c

Returns

true if a counterexample is found (verification fails)

Definition at line 31 of file formal_proofs.cpp.

verify_xor()

bool verify_xor	(	smt_solver::Solver *	solver,
		smt_circuit::UltraCircuit	circuit
	)

Verify bitwise XOR operation: c = a ^ b.

Parameters

solver	SMT solver instance
circuit	Circuit containing variables a, b, c

Returns

true if a counterexample is found (verification fails)

Definition at line 138 of file formal_proofs.cpp.