helpers.cpp File Reference

#include "barretenberg/smt_verification/circuit/ultra_circuit.hpp"
#include "barretenberg/smt_verification/solver/solver.hpp"
#include "barretenberg/smt_verification/util/smt_util.hpp"

Go to the source code of this file.

Functions
uint32_t	pow_num (uint32_t base, uint32_t exp)
smt_circuit::STerm	pow2_8 (smt_circuit::STerm v0, smt_solver::Solver *solver)
	Calculates power of 2.
smt_circuit::STerm	shl (smt_circuit::STerm v0, smt_circuit::STerm v1, smt_solver::Solver *solver)
	Left shift operation without truncation.
smt_circuit::STerm	shr (smt_circuit::STerm v0, smt_circuit::STerm v1, smt_solver::Solver *solver)
	Right shift operation.
smt_circuit::STerm	shl64 (smt_circuit::STerm v0, smt_circuit::STerm v1, smt_solver::Solver *solver)
	Left shift operation with 64-bit truncation.
smt_circuit::STerm	shl32 (smt_circuit::STerm v0, smt_circuit::STerm v1, smt_solver::Solver *solver)
	Left shift operation with 32-bit truncation.
smt_circuit::STerm	idiv (smt_circuit::STerm v0, smt_circuit::STerm v1, uint32_t bit_size, smt_solver::Solver *solver)
	Signed division in noir-style.

Function Documentation

idiv()

smt_circuit::STerm idiv	(	smt_circuit::STerm	v0,
		smt_circuit::STerm	v1,
		uint32_t	bit_size,
		smt_solver::Solver *	solver
	)

Signed division in noir-style.

Parameters

v0	Numerator
v1	Denominator
bit_size	bit sizes of numerator and denominator
solver	SMT solver instance

Returns

Result of (v0 / v1)

Definition at line 61 of file helpers.cpp.

pow2_8()

smt_circuit::STerm pow2_8	(	smt_circuit::STerm	v0,
		smt_solver::Solver *	solver
	)

Calculates power of 2.

Parameters

v0	Exponent (8-bit value)
solver	SMT solver instance

Returns

2^v0

Definition at line 16 of file helpers.cpp.

pow_num()

uint32_t pow_num	(	uint32_t	base,
		uint32_t	exp
	)

Definition at line 6 of file helpers.cpp.

shl()

smt_circuit::STerm shl	(	smt_circuit::STerm	v0,
		smt_circuit::STerm	v1,
		smt_solver::Solver *	solver
	)

Left shift operation without truncation.

Parameters

v0	Value to shift
v1	Number of bits to shift (8-bit value)
solver	SMT solver instance

Returns

Result of (v0 << v1) without truncation

Definition at line 34 of file helpers.cpp.

shl32()

smt_circuit::STerm shl32	(	smt_circuit::STerm	v0,
		smt_circuit::STerm	v1,
		smt_solver::Solver *	solver
	)

Left shift operation with 32-bit truncation.

Parameters

v0	Value to shift
v1	Number of bits to shift (8-bit value)
solver	SMT solver instance

Returns

Result of (v0 << v1) truncated to 32 bits

Definition at line 54 of file helpers.cpp.

shl64()

smt_circuit::STerm shl64	(	smt_circuit::STerm	v0,
		smt_circuit::STerm	v1,
		smt_solver::Solver *	solver
	)

Left shift operation with 64-bit truncation.

Parameters

v0	Value to shift
v1	Number of bits to shift (8-bit value)
solver	SMT solver instance

Returns

Result of (v0 << v1) truncated to 64 bits

Definition at line 47 of file helpers.cpp.

shr()

smt_circuit::STerm shr	(	smt_circuit::STerm	v0,
		smt_circuit::STerm	v1,
		smt_solver::Solver *	solver
	)

Right shift operation.

Parameters

v0	Value to shift
v1	Number of bits to shift (8-bit value)
solver	SMT solver instance

Returns

Result of (v0 >> v1)

Definition at line 40 of file helpers.cpp.