#include <ultra_circuit_checker.hpp>

Classes
struct	HashFunction

struct	MemoryCheckData
	Struct for managing memory record data for ensuring RAM/ROM correctness. More...

struct	TagCheckData
	Struct for managing the running tag product data for ensuring tag correctness. More...

Public Types
using	FF = bb::fr

using	Arithmetic = UltraArithmeticRelation< FF >

using	Elliptic = EllipticRelation< FF >

using	Memory = MemoryRelation< FF >

using	NonNativeField = NonNativeFieldRelation< FF >

using	DeltaRangeConstraint = DeltaRangeConstraintRelation< FF >

using	PoseidonExternal = Poseidon2ExternalRelation< FF >

using	PoseidonInternal = Poseidon2InternalRelation< FF >

using	Params = RelationParameters< FF >

Static Public Member Functions
template<typename Builder >
static bool	check (const Builder &builder_in)
	Check the correctness of a circuit witness.

Private Types
using	Key = std::array< FF, 4 >

using	LookupHashTable = std::unordered_set< Key, HashFunction >

Static Private Member Functions
template<typename Builder >
static Builder	prepare_circuit (const Builder &builder_in)
	Copy the builder and finalize it before checking its validity.

template<typename Builder >
static bool	check_block (Builder &builder, auto &block, TagCheckData &tag_data, MemoryCheckData &memory_data, LookupHashTable &lookup_hash_table)
	Checks that the provided witness satisfies all gates contained in a single execution trace block.

template<typename Relation >
static bool	check_relation (auto &values, auto &params)
	Check that a given relation is satisfied for the provided inputs corresponding to a single row.

static bool	check_lookup (auto &values, auto &lookup_hash_table)
	Check whether the values in a lookup gate are contained within a corresponding hash table.

template<typename Builder >
static bool	check_databus_read (auto &values, Builder &builder)
	Check that the {index, value} pair contained in a databus read gate reflects the actual value present in the corresponding databus column at the given index.

static bool	check_tag_data (const TagCheckData &tag_data)
	Check whether the left and right running tag products are equal.

template<typename Builder >
static auto	init_empty_values ()
	Helper for initializing an empty AllValues container of the right Flavor based on Builder.

template<typename Builder >
static void	populate_values (Builder &builder, auto &block, auto &values, TagCheckData &tag_data, MemoryCheckData &memory_data, size_t idx)
	Populate the values required to check the correctness of a single "row" of the circuit.

template<>
auto	init_empty_values ()

template<>
UltraCircuitBuilder_< UltraExecutionTraceBlocks >	prepare_circuit (const UltraCircuitBuilder_< UltraExecutionTraceBlocks > &builder_in)

Detailed Description

Definition at line 18 of file ultra_circuit_checker.hpp.

Member Typedef Documentation

◆ Arithmetic

using bb::UltraCircuitChecker::Arithmetic = UltraArithmeticRelation<FF>

Definition at line 21 of file ultra_circuit_checker.hpp.

◆ DeltaRangeConstraint

using bb::UltraCircuitChecker::DeltaRangeConstraint = DeltaRangeConstraintRelation<FF>

Definition at line 25 of file ultra_circuit_checker.hpp.

◆ Elliptic

using bb::UltraCircuitChecker::Elliptic = EllipticRelation<FF>

Definition at line 22 of file ultra_circuit_checker.hpp.

◆ FF

using bb::UltraCircuitChecker::FF = bb::fr

Definition at line 20 of file ultra_circuit_checker.hpp.

◆ Key

using bb::UltraCircuitChecker::Key = std::array<FF, 4>

private

Definition at line 47 of file ultra_circuit_checker.hpp.

◆ LookupHashTable

using bb::UltraCircuitChecker::LookupHashTable = std::unordered_set<Key, HashFunction>

private

Definition at line 49 of file ultra_circuit_checker.hpp.

◆ Memory

using bb::UltraCircuitChecker::Memory = MemoryRelation<FF>

Definition at line 23 of file ultra_circuit_checker.hpp.

◆ NonNativeField

using bb::UltraCircuitChecker::NonNativeField = NonNativeFieldRelation<FF>

Definition at line 24 of file ultra_circuit_checker.hpp.

◆ Params

using bb::UltraCircuitChecker::Params = RelationParameters<FF>

Definition at line 28 of file ultra_circuit_checker.hpp.

◆ PoseidonExternal

using bb::UltraCircuitChecker::PoseidonExternal = Poseidon2ExternalRelation<FF>

Definition at line 26 of file ultra_circuit_checker.hpp.

◆ PoseidonInternal

using bb::UltraCircuitChecker::PoseidonInternal = Poseidon2InternalRelation<FF>

Definition at line 27 of file ultra_circuit_checker.hpp.

Member Function Documentation

◆ check()

template<typename Builder >

template bool bb::UltraCircuitChecker::check< UltraCircuitBuilder_< UltraExecutionTraceBlocks > > ( const Builder & builder_in )

static

Check the correctness of a circuit witness.

Ensures that all relations for a given Ultra arithmetization are satisfied by the witness for each gate in the circuit.

Note: : This method does not check the permutation relation since this fundamentally depends on grand product polynomials created by the prover. The lookup relation is also not checked for the same reason, however, we do check the correctness of lookup gates by simply ensuring that the inputs to those gates are present in the lookup tables attached to the circuit.

Template Parameters

Builder

Parameters

builder

Definition at line 46 of file ultra_circuit_checker.cpp.

◆ check_block()

template<typename Builder >

bool bb::UltraCircuitChecker::check_block	(	Builder &	builder,
		auto &	block,
		TagCheckData &	tag_data,
		MemoryCheckData &	memory_data,
		LookupHashTable &	lookup_hash_table
	)

staticprivate

Checks that the provided witness satisfies all gates contained in a single execution trace block.

Template Parameters

Builder

Parameters

builder
block
tag_data
memory_data
lookup_hash_table

Definition at line 101 of file ultra_circuit_checker.cpp.

◆ check_databus_read()

template<typename Builder >

bool bb::UltraCircuitChecker::check_databus_read	(	auto &	values,
		Builder &	builder
	)

staticprivate

Check that the {index, value} pair contained in a databus read gate reflects the actual value present in the corresponding databus column at the given index.

Parameters

values Inputs to a databus read gate

Definition at line 227 of file ultra_circuit_checker.cpp.

◆ check_lookup()

bool bb::UltraCircuitChecker::check_lookup	(	auto &	values,
		auto &	lookup_hash_table
	)

staticprivate

Check whether the values in a lookup gate are contained within a corresponding hash table.

Parameters

values	Inputs to a lookup gate
lookup_hash_table	Preconstructed hash table representing entries of all tables in circuit

Definition at line 215 of file ultra_circuit_checker.cpp.

◆ check_relation()

template<typename Relation >

bool bb::UltraCircuitChecker::check_relation	(	auto &	values,
		auto &	params
	)

staticprivate

Check that a given relation is satisfied for the provided inputs corresponding to a single row.

Note: Assumes the relation constraints should evaluate to zero on each row and thus does not apply to linearly dependent relations like the log derivative lookup argument.

Template Parameters

Relation

Parameters

values	Values of the relation inputs at a single row
params

Definition at line 194 of file ultra_circuit_checker.cpp.

◆ check_tag_data()

bool bb::UltraCircuitChecker::check_tag_data ( const TagCheckData & tag_data )

staticprivate

Check whether the left and right running tag products are equal.

Note: By construction, this is in general only true after the last gate has been processed

Parameters

tag_data

Definition at line 259 of file ultra_circuit_checker.cpp.

◆ init_empty_values() [1/2]

template<>

auto bb::UltraCircuitChecker::init_empty_values ( )

staticprivate

Definition at line 9 of file ultra_circuit_checker.cpp.

◆ init_empty_values() [2/2]

template<typename Builder >

static auto bb::UltraCircuitChecker::init_empty_values ( )

staticprivate

Helper for initializing an empty AllValues container of the right Flavor based on Builder.

We construct a Flavor::AllValues object from each row of circuit data so that we can use the Relations to check correctness. UltraFlavor is used for the Ultra builder and MegaFlavor is used for the Mega builder

Template Parameters

Builder

◆ populate_values()

template<typename Builder >

void bb::UltraCircuitChecker::populate_values	(	Builder &	builder,
		auto &	block,
		auto &	values,
		TagCheckData &	tag_data,
		MemoryCheckData &	memory_data,
		size_t	idx
	)

staticprivate

Populate the values required to check the correctness of a single "row" of the circuit.

Populates all wire values (plus shifts) and selectors. Updates running tag product information. Populates 4th wire with memory records (as needed).

Template Parameters

Builder

Parameters

builder
values
tag_data
idx

Definition at line 265 of file ultra_circuit_checker.cpp.

◆ prepare_circuit() [1/2]

template<typename Builder >

static Builder bb::UltraCircuitChecker::prepare_circuit ( const Builder & builder_in )

staticprivate

Copy the builder and finalize it before checking its validity.

◆ prepare_circuit() [2/2]

template<>

UltraCircuitBuilder_< UltraExecutionTraceBlocks > bb::UltraCircuitChecker::prepare_circuit ( const UltraCircuitBuilder_< UltraExecutionTraceBlocks > & builder_in )

staticprivate

Definition at line 14 of file ultra_circuit_checker.cpp.

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

src/barretenberg/circuit_checker/ultra_circuit_checker.hpp
src/barretenberg/circuit_checker/ultra_circuit_checker.cpp

Classes

Public Types

Static Public Member Functions

Private Types

Static Private Member Functions

Detailed Description

Member Typedef Documentation

◆ Arithmetic

◆ DeltaRangeConstraint

◆ Elliptic

◆ FF

◆ Key

◆ LookupHashTable

◆ Memory

◆ NonNativeField

◆ Params

◆ PoseidonExternal

◆ PoseidonInternal

Member Function Documentation

◆ check()

◆ check_block()

◆ check_databus_read()

◆ check_lookup()

◆ check_relation()

◆ check_tag_data()

◆ init_empty_values() [1/2]

◆ init_empty_values() [2/2]

◆ populate_values()

◆ prepare_circuit() [1/2]

◆ prepare_circuit() [2/2]