helpers.hpp File Reference

#include "barretenberg/smt_verification/circuit/ultra_circuit.hpp"
#include "barretenberg/smt_verification/solver/solver.hpp"
#include "barretenberg/smt_verification/terms/term.hpp"

Go to the source code of this file.

Functions
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	shl8 (smt_circuit::STerm v0, smt_circuit::STerm v1, smt_solver::Solver *solver)
	Left shift operation with 8-bit truncation.
smt_circuit::STerm	pow2_8 (smt_circuit::STerm v0, smt_solver::Solver *solver)
	Calculates power of 2.
smt_circuit::STerm	shr (smt_circuit::STerm v0, smt_circuit::STerm v1, smt_solver::Solver *solver)
	Right shift operation.
smt_circuit::STerm	shl (smt_circuit::STerm v0, smt_circuit::STerm v1, smt_solver::Solver *solver)
	Left shift operation without 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.
smt_circuit::STerm	add_signed (smt_circuit::STerm v0, smt_circuit::STerm v1, uint32_t bit_size)
smt_circuit::STerm	sub_signed (smt_circuit::STerm v0, smt_circuit::STerm v1, uint32_t bit_size)
	Signed subtraction operation: c = a - b + truncate to bit_size bits.
smt_circuit::STerm	mul_signed (smt_circuit::STerm v0, smt_circuit::STerm v1, uint32_t bit_size)
	Signed multiplication operation: c = a * b + truncate to bit_size bits.

Function Documentation

add_signed()

smt_circuit::STerm add_signed	(	smt_circuit::STerm	v0,
		smt_circuit::STerm	v1,
		uint32_t	bit_size
	)

Parameters

v0	Augend
v1	Addend
bit_size	Bit size to truncate to

Returns

Result of truncate(a + b, bit_size - 1)

Definition at line 68 of file helpers.cpp.

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 88 of file helpers.cpp.

mul_signed()

smt_circuit::STerm mul_signed	(	smt_circuit::STerm	v0,
		smt_circuit::STerm	v1,
		uint32_t	bit_size
	)

Signed multiplication operation: c = a * b + truncate to bit_size bits.

Parameters

v0	Multiplicand
v1	Multiplier
bit_size	Bit size to truncate to

Returns

Result of (a * b + truncate(bit_size))

Definition at line 81 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.

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.

shl8()

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

Left shift operation with 8-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 8 bits

Definition at line 61 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.

sub_signed()

smt_circuit::STerm sub_signed	(	smt_circuit::STerm	v0,
		smt_circuit::STerm	v1,
		uint32_t	bit_size
	)

Signed subtraction operation: c = a - b + truncate to bit_size bits.

Parameters

v0	Minuend
v1	Subtrahend
bit_size	Bit size to truncate to

Returns

Result of (a - b + truncate(bit_size))

Definition at line 74 of file helpers.cpp.