#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 = ArithmeticRelation< FF >

using	BilinearBatchedEq = BilinearOrBatchedEqCheckRelation< FF >

using	Elliptic = EllipticRelation< FF >

using	Memory = MemoryRelation< FF >

using	NonNativeField = NonNativeFieldRelation< FF >

using	DeltaRangeConstraint = DeltaRangeConstraintRelation< FF >

using	PoseidonExternal = Poseidon2ExternalRelation< FF >

using	PoseidonInitialExternal = Poseidon2InitialExternalRelation< FF >

using	PoseidonInternal = Poseidon2InternalRelation< FF >

using	PoseidonQuadInternal = Poseidon2QuadInternalRelation< FF >

using	PoseidonQuadInternalTerminal = Poseidon2QuadInternalTerminalRelation< FF >

using	PoseidonTransitionEntry = Poseidon2TransitionEntryRelation< 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.

template<typename Relation , typename Builder , typename Block >
static bool	check_relation_at_row (Builder &builder, Block &block, size_t row_idx)
	Evaluate a single `Relation` at `block`'s row `row_idx` in isolation, returning true iff every subrelation vanishes. Unlike `check`, which short-circuits on the first failing relation, this attributes a constraint to a specific (relation, row) pair. The builder's gates must already be emitted (no finalization).

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.

template<typename Memory >
static bool	check_memory_relation_with_logup (auto &values, auto &params, MemoryCheckData &memory_data)

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 23 of file ultra_circuit_checker.hpp.

Member Typedef Documentation

◆ Arithmetic

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

Definition at line 26 of file ultra_circuit_checker.hpp.

◆ BilinearBatchedEq

using bb::UltraCircuitChecker::BilinearBatchedEq = BilinearOrBatchedEqCheckRelation<FF>

Definition at line 27 of file ultra_circuit_checker.hpp.

◆ DeltaRangeConstraint

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

Definition at line 31 of file ultra_circuit_checker.hpp.

◆ Elliptic

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

Definition at line 28 of file ultra_circuit_checker.hpp.

◆ FF

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

Definition at line 25 of file ultra_circuit_checker.hpp.

◆ Key

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

private

Definition at line 65 of file ultra_circuit_checker.hpp.

◆ LookupHashTable

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

private

Definition at line 67 of file ultra_circuit_checker.hpp.

◆ Memory

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

Definition at line 29 of file ultra_circuit_checker.hpp.

◆ NonNativeField

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

Definition at line 30 of file ultra_circuit_checker.hpp.

◆ Params

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

Definition at line 38 of file ultra_circuit_checker.hpp.

◆ PoseidonExternal

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

Definition at line 32 of file ultra_circuit_checker.hpp.

◆ PoseidonInitialExternal

using bb::UltraCircuitChecker::PoseidonInitialExternal = Poseidon2InitialExternalRelation<FF>

Definition at line 33 of file ultra_circuit_checker.hpp.

◆ PoseidonInternal

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

Definition at line 34 of file ultra_circuit_checker.hpp.

◆ PoseidonQuadInternal

using bb::UltraCircuitChecker::PoseidonQuadInternal = Poseidon2QuadInternalRelation<FF>

Definition at line 35 of file ultra_circuit_checker.hpp.

◆ PoseidonQuadInternalTerminal

using bb::UltraCircuitChecker::PoseidonQuadInternalTerminal = Poseidon2QuadInternalTerminalRelation<FF>

Definition at line 36 of file ultra_circuit_checker.hpp.

◆ PoseidonTransitionEntry

using bb::UltraCircuitChecker::PoseidonTransitionEntry = Poseidon2TransitionEntryRelation<FF>

Definition at line 37 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 51 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 117 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 320 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 308 of file ultra_circuit_checker.cpp.

◆ check_memory_relation_with_logup()

template<typename Memory >

bool bb::UltraCircuitChecker::check_memory_relation_with_logup	(	auto &	values,
		auto &	params,
		MemoryCheckData &	memory_data
	)

staticprivate

Definition at line 284 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 253 of file ultra_circuit_checker.cpp.

◆ check_relation_at_row()

template<typename Relation , typename Builder , typename Block >

bool bb::UltraCircuitChecker::check_relation_at_row	(	Builder &	builder,
		Block &	block,
		size_t	row_idx
	)

static

Evaluate a single Relation at block's row row_idx in isolation, returning true iff every subrelation vanishes. Unlike check, which short-circuits on the first failing relation, this attributes a constraint to a specific (relation, row) pair. The builder's gates must already be emitted (no finalization).

Definition at line 239 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 345 of file ultra_circuit_checker.cpp.

◆ init_empty_values() [1/2]

template<>

auto bb::UltraCircuitChecker::init_empty_values ( )

staticprivate

Definition at line 11 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 351 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 16 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

◆ BilinearBatchedEq

◆ DeltaRangeConstraint

◆ Elliptic

◆ FF

◆ Key

◆ LookupHashTable

◆ Memory

◆ NonNativeField

◆ Params

◆ PoseidonExternal

◆ PoseidonInitialExternal

◆ PoseidonInternal

◆ PoseidonQuadInternal

◆ PoseidonQuadInternalTerminal

◆ PoseidonTransitionEntry

Member Function Documentation

◆ check()

◆ check_block()

◆ check_databus_read()

◆ check_lookup()

◆ check_memory_relation_with_logup()

◆ check_relation()

◆ check_relation_at_row()

◆ check_tag_data()

◆ init_empty_values() [1/2]

◆ init_empty_values() [2/2]

◆ populate_values()

◆ prepare_circuit() [1/2]

◆ prepare_circuit() [2/2]