Symbolic Circuit class for Standard Circuit Builder. More...

#include <ultra_circuit.hpp>

Inheritance diagram for smt_circuit::UltraCircuit:

Public Member Functions
	UltraCircuit (CircuitSchema &circuit_info, Solver *solver, TermType type=TermType::FFTerm, const std::string &tag="", bool enable_optimizations=true, bool rom_ram_relaxed=false)
	Construct a new UltraCircuit object.

	UltraCircuit (const UltraCircuit &other)=default

	UltraCircuit (UltraCircuit &&other)=default

UltraCircuit &	operator= (const UltraCircuit &other)=default

UltraCircuit &	operator= (UltraCircuit &&other)=default

	~UltraCircuit () override=default

size_t	get_num_gates () const
	Get the num gates object.

bool	simulate_circuit_eval (std::vector< bb::fr > &witness) const override
	Similar functionality to old .check_circuit() method in standard circuit builder.

void	process_new_table (uint32_t table_idx)

size_t	handle_arithmetic_relation (size_t cursor)
	Adds all the arithmetic gate constraints to the solver. Relaxes constraint system for non-ff solver engines via removing subcircuits that were already proved being correct.

size_t	handle_lookup_relation (size_t cursor)
	Adds all the lookup gate constraints to the solver. Relaxes constraint system for non-ff solver engines via removing subcircuits that were already proved being correct.

size_t	handle_elliptic_relation (size_t cursor)
	Adds all the elliptic gate constraints to the solver.

size_t	handle_delta_range_relation (size_t cursor)
	Adds all the delta_range gate constraints to the solver.

size_t	handle_nnf_relation (size_t cursor)
	Adds all the nnf constraints to the solver.

void	handle_range_constraints ()
	Adds all the range constraints to the solver.

void	rom_table_read (uint32_t rom_array_idx, uint32_t index_idx, uint32_t value1_idx, uint32_t value2_idx)
	Perform read from ROM table.

void	ram_table_read (uint32_t ram_array_idx, uint32_t index_idx, uint32_t value_idx)
	Perform read from RAM table.

void	ram_table_write (uint32_t ram_array_idx, uint32_t ram_index_idx, uint32_t read_from_value_idx)
	Perform write to RAM table.

void	handle_rom_tables ()
	Adds all the ROM related constraints into the solver.

void	handle_ram_tables ()
	Adds all the RAM related constraints into the solver.

Public Member Functions inherited from smt_circuit::CircuitBase
	CircuitBase (std::unordered_map< uint32_t, std::string > &variable_names, std::vector< bb::fr > &variables, std::vector< uint32_t > &public_inps, std::vector< uint32_t > &real_variable_index, std::vector< uint32_t > &real_variable_tags, Solver *solver, TermType type, const std::string &tag="", bool enable_optimizations=true)

STerm	operator[] (const std::string &name)
	Returns a previously named symbolic variable.

STerm	operator[] (const uint32_t &idx)

size_t	get_num_real_vars () const

size_t	get_num_vars () const

void	init ()

	CircuitBase (const CircuitBase &other)=default

	CircuitBase (CircuitBase &&other) noexcept=default

CircuitBase &	operator= (const CircuitBase &other)=default

CircuitBase &	operator= (CircuitBase &&other) noexcept=default

virtual	~CircuitBase ()=default

Static Public Member Functions
static std::pair< UltraCircuit, UltraCircuit >	unique_witness_ext (CircuitSchema &circuit_info, Solver *s, TermType type, const std::vector< std::string > &equal={}, const std::vector< std::string > &not_equal={}, const std::vector< std::string > &equal_at_the_same_time={}, const std::vector< std::string > &not_equal_at_the_same_time={}, bool enable_optimizations=false)
	Check your circuit for witness uniqueness.

static std::pair< UltraCircuit, UltraCircuit >	unique_witness (CircuitSchema &circuit_info, Solver *s, TermType type, const std::vector< std::string > &equal={}, bool enable_optimizations=false)
	Check your circuit for witness uniqueness.

Public Attributes
std::vector< std::vector< std::vector< bb::fr > > >	selectors

std::vector< std::vector< std::vector< uint32_t > > >	wires_idxs

std::vector< std::vector< std::vector< bb::fr > > >	lookup_tables

std::unordered_map< uint32_t, SymSet< STuple > >	cached_symbolic_tables

std::unordered_map< uint32_t, TableType >	tables_types

std::unordered_map< uint32_t, size_t >	tables_sizes

std::unordered_map< uint64_t, SymSet< STerm > >	cached_range_tables

std::unordered_map< uint32_t, uint64_t >	range_tags

std::vector< std::vector< std::vector< uint32_t > > >	rom_records

std::vector< std::vector< std::array< uint32_t, 2 > > >	rom_states

std::vector< std::vector< std::vector< uint32_t > > >	ram_records

std::vector< std::vector< uint32_t > >	ram_states

std::unordered_map< uint32_t, SymArray< STerm, STuple > >	cached_rom_tables

std::unordered_map< uint32_t, SymArray< STerm, STerm > >	cached_ram_tables

bool	rom_ram_relaxed

Public Attributes inherited from smt_circuit::CircuitBase
std::vector< bb::fr >	variables

std::unordered_set< uint32_t >	public_inps

std::unordered_map< uint32_t, std::string >	variable_names

std::unordered_map< std::string, uint32_t >	variable_names_inverse

std::unordered_map< uint32_t, STerm >	symbolic_vars

std::vector< uint32_t >	real_variable_index

std::vector< uint32_t >	real_variable_tags

std::unordered_map< uint32_t, bool >	optimized

bool	enable_optimizations

std::unordered_map< uint32_t, std::vector< bb::fr > >	post_process

Solver *	solver

TermType	type

std::string	tag

Detailed Description

Symbolic Circuit class for Standard Circuit Builder.

Contains all the information about the circuit: gates, variables, symbolic variables, specified names and global solver.

Definition at line 53 of file ultra_circuit.hpp.

Constructor & Destructor Documentation

◆ UltraCircuit() [1/3]

smt_circuit::UltraCircuit::UltraCircuit	(	CircuitSchema &	circuit_info,
		Solver *	solver,
		TermType	type = `TermType::FFTerm`,
		const std::string &	tag = `""`,
		bool	optimizations = `true`,
		bool	rom_ram_relaxed = `false`
	)

explicit

Construct a new UltraCircuit object.

Parameters

circuit_info	CircuitShema object
solver	pointer to the global solver
tag	tag of the circuit. Empty by default.

Definition at line 13 of file ultra_circuit.cpp.

◆ UltraCircuit() [2/3]

smt_circuit::UltraCircuit::UltraCircuit ( const UltraCircuit & other )

default

◆ UltraCircuit() [3/3]

smt_circuit::UltraCircuit::UltraCircuit ( UltraCircuit && other )

default

◆ ~UltraCircuit()

smt_circuit::UltraCircuit::~UltraCircuit ( )

overridedefault

Member Function Documentation

◆ get_num_gates()

size_t smt_circuit::UltraCircuit::get_num_gates ( ) const

inline

Get the num gates object.

Note: DO NOT RELY ON THIS FUNCTION

Returns: size_t

Definition at line 101 of file ultra_circuit.hpp.

◆ handle_arithmetic_relation()

size_t smt_circuit::UltraCircuit::handle_arithmetic_relation ( size_t cursor )

Adds all the arithmetic gate constraints to the solver. Relaxes constraint system for non-ff solver engines via removing subcircuits that were already proved being correct.

Parameters

cusor current selector

Returns: new cursor value

Definition at line 80 of file ultra_circuit.cpp.

◆ handle_delta_range_relation()

size_t smt_circuit::UltraCircuit::handle_delta_range_relation ( size_t cursor )

Adds all the delta_range gate constraints to the solver.

Parameters

cusor current selector

Returns: new cursor value

Todo:: Useless?

Definition at line 375 of file ultra_circuit.cpp.

◆ handle_elliptic_relation()

size_t smt_circuit::UltraCircuit::handle_elliptic_relation ( size_t cursor )

Adds all the elliptic gate constraints to the solver.

Parameters

cusor current selector

Returns: new cursor value

Definition at line 306 of file ultra_circuit.cpp.

◆ handle_lookup_relation()

size_t smt_circuit::UltraCircuit::handle_lookup_relation ( size_t cursor )

Adds all the lookup gate constraints to the solver. Relaxes constraint system for non-ff solver engines via removing subcircuits that were already proved being correct.

Parameters

cusor current selector

Returns: new cursor value

Definition at line 212 of file ultra_circuit.cpp.

◆ handle_nnf_relation()

size_t smt_circuit::UltraCircuit::handle_nnf_relation ( size_t cursor )

Adds all the nnf constraints to the solver.

Parameters

cursor current selector

Returns: new cursor value

Definition at line 458 of file ultra_circuit.cpp.

◆ handle_ram_tables()

void smt_circuit::UltraCircuit::handle_ram_tables ( )

Adds all the RAM related constraints into the solver.

Definition at line 684 of file ultra_circuit.cpp.

◆ handle_range_constraints()

void smt_circuit::UltraCircuit::handle_range_constraints ( )

Adds all the range constraints to the solver.

Definition at line 421 of file ultra_circuit.cpp.

◆ handle_rom_tables()

void smt_circuit::UltraCircuit::handle_rom_tables ( )

Adds all the ROM related constraints into the solver.

Definition at line 642 of file ultra_circuit.cpp.

◆ operator=() [1/2]

UltraCircuit & smt_circuit::UltraCircuit::operator= ( const UltraCircuit & other )

default

◆ operator=() [2/2]

UltraCircuit & smt_circuit::UltraCircuit::operator= ( UltraCircuit && other )

default

◆ process_new_table()

void smt_circuit::UltraCircuit::process_new_table ( uint32_t table_idx )

Definition at line 166 of file ultra_circuit.cpp.

◆ ram_table_read()

void smt_circuit::UltraCircuit::ram_table_read	(	uint32_t	ram_array_idx,
		uint32_t	ram_index_idx,
		uint32_t	read_to_value_idx
	)

Perform read from RAM table.

Parameters

ram_array_idx	index of the RAM table
ram_index_idx	witness index of the (index) in table
read_to_value_idx	witness index of the value to store

Definition at line 601 of file ultra_circuit.cpp.

◆ ram_table_write()

void smt_circuit::UltraCircuit::ram_table_write	(	uint32_t	ram_array_idx,
		uint32_t	ram_index_idx,
		uint32_t	read_from_value_idx
	)

Perform write to RAM table.

Parameters

ram_array_idx	index of the RAM table
ram_index_idx	witness index of the (index) in table
read_to_value_idx	witness index of the value to store

Definition at line 624 of file ultra_circuit.cpp.

◆ rom_table_read()

void smt_circuit::UltraCircuit::rom_table_read	(	uint32_t	rom_array_idx,
		uint32_t	rom_index_idx,
		uint32_t	read_to_value1_idx,
		uint32_t	read_to_value2_idx
	)

Perform read from ROM table.

Parameters

rom_array_idx	index of the ROM table
rom_index_idx	witness index of the (index) in table
read_to_value1_idx	witness index of the first value to store
read_to_value2_idx	witness index of the second value to store

Definition at line 573 of file ultra_circuit.cpp.

◆ simulate_circuit_eval()

bool smt_circuit::UltraCircuit::simulate_circuit_eval ( std::vector< bb::fr > & witness ) const

overridevirtual

Similar functionality to old .check_circuit() method in standard circuit builder.

Parameters

witness

Returns: true; false

Todo:: Do we actually need this here?

Implements smt_circuit::CircuitBase.

Definition at line 727 of file ultra_circuit.cpp.

◆ unique_witness()

std::pair< UltraCircuit, UltraCircuit > smt_circuit::UltraCircuit::unique_witness	(	CircuitSchema &	circuit_info,
		Solver *	s,
		TermType	type,
		const std::vector< std::string > &	equal = `{}`,
		bool	enable_optimizations = `false`
	)

static

Check your circuit for witness uniqueness.

Creates two Circuit objects that represent the same circuit, however you can choose which variables should be equal in both cases, other witness members will be marked as not equal at the same time or basically they will have to differ by at least one element.

Parameters

circuit_info
s	pointer to the global solver
equal	The list of names of variables which should be equal in both circuits(each is equal)

Returns: std::pair<Circuit, Circuit>

Definition at line 811 of file ultra_circuit.cpp.

◆ unique_witness_ext()

std::pair< UltraCircuit, UltraCircuit > smt_circuit::UltraCircuit::unique_witness_ext	(	CircuitSchema &	circuit_info,
		Solver *	s,
		TermType	type,
		const std::vector< std::string > &	equal = `{}`,
		const std::vector< std::string > &	not_equal = `{}`,
		const std::vector< std::string > &	equal_at_the_same_time = `{}`,
		const std::vector< std::string > &	not_equal_at_the_same_time = `{}`,
		bool	enable_optimizations = `false`
	)

static

Check your circuit for witness uniqueness.

Creates two Circuit objects that represent the same circuit, however you can choose which variables should be (not) equal in both cases, and also the variables that should (not) be equal at the same time.

Parameters

circuit_info
s	pointer to the global solver
equal	The list of names of variables which should be equal in both circuits(each is equal)
not_equal	The list of names of variables which should not be equal in both circuits(each is not equal)
equal_at_the_same_time	The list of variables, where at least one pair has to be equal
not_equal_at_the_same_time	The list of variables, where at least one pair has to be distinct

Returns: std::pair<Circuit, Circuit>

Definition at line 752 of file ultra_circuit.cpp.

Member Data Documentation

◆ cached_ram_tables

std::unordered_map<uint32_t, SymArray<STerm, STerm> > smt_circuit::UltraCircuit::cached_ram_tables

Definition at line 80 of file ultra_circuit.hpp.

◆ cached_range_tables

std::unordered_map<uint64_t, SymSet<STerm> > smt_circuit::UltraCircuit::cached_range_tables

Definition at line 68 of file ultra_circuit.hpp.

◆ cached_rom_tables

std::unordered_map<uint32_t, SymArray<STerm, STuple> > smt_circuit::UltraCircuit::cached_rom_tables

Definition at line 78 of file ultra_circuit.hpp.

◆ cached_symbolic_tables

std::unordered_map<uint32_t, SymSet<STuple> > smt_circuit::UltraCircuit::cached_symbolic_tables

Definition at line 65 of file ultra_circuit.hpp.

◆ lookup_tables

std::vector<std::vector<std::vector<bb::fr> > > smt_circuit::UltraCircuit::lookup_tables

Definition at line 64 of file ultra_circuit.hpp.

◆ ram_records

std::vector<std::vector<std::vector<uint32_t> > > smt_circuit::UltraCircuit::ram_records

Definition at line 75 of file ultra_circuit.hpp.

◆ ram_states

std::vector<std::vector<uint32_t> > smt_circuit::UltraCircuit::ram_states

Definition at line 76 of file ultra_circuit.hpp.

◆ range_tags

std::unordered_map<uint32_t, uint64_t> smt_circuit::UltraCircuit::range_tags

Definition at line 70 of file ultra_circuit.hpp.

◆ rom_ram_relaxed

bool smt_circuit::UltraCircuit::rom_ram_relaxed

Definition at line 81 of file ultra_circuit.hpp.

◆ rom_records

std::vector<std::vector<std::vector<uint32_t> > > smt_circuit::UltraCircuit::rom_records

Definition at line 72 of file ultra_circuit.hpp.

◆ rom_states

std::vector<std::vector<std::array<uint32_t, 2> > > smt_circuit::UltraCircuit::rom_states

Definition at line 73 of file ultra_circuit.hpp.

◆ selectors

std::vector<std::vector<std::vector<bb::fr> > > smt_circuit::UltraCircuit::selectors

Definition at line 55 of file ultra_circuit.hpp.

◆ tables_sizes

std::unordered_map<uint32_t, size_t> smt_circuit::UltraCircuit::tables_sizes

Definition at line 67 of file ultra_circuit.hpp.

◆ tables_types

std::unordered_map<uint32_t, TableType> smt_circuit::UltraCircuit::tables_types

Definition at line 66 of file ultra_circuit.hpp.

◆ wires_idxs

std::vector<std::vector<std::vector<uint32_t> > > smt_circuit::UltraCircuit::wires_idxs

Definition at line 62 of file ultra_circuit.hpp.

The documentation for this class was generated from the following files:

src/barretenberg/smt_verification/circuit/ultra_circuit.hpp
src/barretenberg/smt_verification/circuit/ultra_circuit.cpp

Public Member Functions

Static Public Member Functions

Public Attributes

Detailed Description

Constructor & Destructor Documentation

◆ UltraCircuit() [1/3]

◆ UltraCircuit() [2/3]

◆ UltraCircuit() [3/3]

◆ ~UltraCircuit()

Member Function Documentation

◆ get_num_gates()

◆ handle_arithmetic_relation()

◆ handle_delta_range_relation()

◆ handle_elliptic_relation()

◆ handle_lookup_relation()

◆ handle_nnf_relation()

◆ handle_ram_tables()

◆ handle_range_constraints()

◆ handle_rom_tables()

◆ operator=() [1/2]

◆ operator=() [2/2]

◆ process_new_table()

◆ ram_table_read()

◆ ram_table_write()

◆ rom_table_read()

◆ simulate_circuit_eval()

◆ unique_witness()

◆ unique_witness_ext()

Member Data Documentation

◆ cached_ram_tables

◆ cached_range_tables

◆ cached_rom_tables

◆ cached_symbolic_tables

◆ lookup_tables

◆ ram_records

◆ ram_states

◆ range_tags

◆ rom_ram_relaxed

◆ rom_records

◆ rom_states

◆ selectors

◆ tables_sizes

◆ tables_types

◆ wires_idxs