helpers.test.cpp File Reference

#include "helpers.hpp"
#include "barretenberg/common/test.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_circuit_builders/ultra_circuit_builder.hpp"

Go to the source code of this file.

Functions
	TEST (helpers, shl)
	Test left shift operation Tests that 5 << 1 = 10 using SMT solver.
	TEST (helpers, shr)
	Test right shift operation Tests that 5 >> 1 = 2 using SMT solver.
	TEST (helpers, buggy_shr)
	Test edge case for right shift operation Tests that 1879048194 >> 16 = 28672 using SMT solver.
	TEST (helpers, pow2)
	Test power of 2 calculation Tests that 2^11 = 2048 using SMT solver.
	TEST (helpers, signed_div)
	Test signed division with zero dividend Tests that 0 / -1 = 0 using SMT solver.
	TEST (helpers, signed_div_1)
	Test signed division with positive dividend and negative divisor Tests that 1 / -1 = -1 using SMT solver.
	TEST (helpers, signed_div_2)
	Test signed division with positive numbers Tests that 7 / 2 = 3 using SMT solver.
	TEST (helpers, shl_overflow)
	Test left shift overflow behavior Tests that 1 << 50 = 0 (due to overflow) using SMT solver.

Function Documentation

TEST() [1/8]

TEST	(	helpers	,
		buggy_shr
	)

Test edge case for right shift operation Tests that 1879048194 >> 16 = 28672 using SMT solver.

Definition at line 70 of file helpers.test.cpp.

TEST() [2/8]

TEST	(	helpers	,
		pow2
	)

Test power of 2 calculation Tests that 2^11 = 2048 using SMT solver.

Definition at line 99 of file helpers.test.cpp.

TEST() [3/8]

TEST	(	helpers	,
		shl
	)

Test left shift operation Tests that 5 << 1 = 10 using SMT solver.

Definition at line 16 of file helpers.test.cpp.

TEST() [4/8]

TEST	(	helpers	,
		shl_overflow
	)

Test left shift overflow behavior Tests that 1 << 50 = 0 (due to overflow) using SMT solver.

Definition at line 204 of file helpers.test.cpp.

TEST() [5/8]

TEST	(	helpers	,
		shr
	)

Test right shift operation Tests that 5 >> 1 = 2 using SMT solver.

Definition at line 43 of file helpers.test.cpp.

TEST() [6/8]

TEST	(	helpers	,
		signed_div
	)

Test signed division with zero dividend Tests that 0 / -1 = 0 using SMT solver.

Definition at line 123 of file helpers.test.cpp.

TEST() [7/8]

TEST	(	helpers	,
		signed_div_1
	)

Test signed division with positive dividend and negative divisor Tests that 1 / -1 = -1 using SMT solver.

Definition at line 150 of file helpers.test.cpp.

TEST() [8/8]

TEST	(	helpers	,
		signed_div_2
	)

Test signed division with positive numbers Tests that 7 / 2 = 3 using SMT solver.

Definition at line 177 of file helpers.test.cpp.