7#include <unordered_set>
11template <>
auto UltraCircuitChecker::init_empty_values<UltraCircuitBuilder_<UltraExecutionTraceBlocks>>()
16template <>
auto UltraCircuitChecker::init_empty_values<MegaCircuitBuilder_<bb::fr>>()
27 if (!
builder.circuit_finalized) {
35MegaCircuitBuilder_<bb::fr> UltraCircuitChecker::prepare_circuit<MegaCircuitBuilder_<bb::fr>>(
36 const MegaCircuitBuilder_<bb::fr>& builder_in)
39 MegaCircuitBuilder_<bb::fr>
builder{ builder_in };
44 if (!
builder.circuit_finalized) {
53 if (builder_in.failed()) {
54 info(
"CircuitChecker: circuit contains invalid witnesses: ", builder_in.err());
61 for (
const auto& table :
builder.get_lookup_tables()) {
62 const FF table_index(table.table_index);
63 for (
size_t i = 0; i < table.size(); ++i) {
64 lookup_hash_table.insert({ table.column_1[i], table.column_2[i], table.column_3[i], table_index });
74 for (
auto& block :
builder.blocks.get()) {
77#ifndef FUZZING_DISABLE_WARNINGS
78 info(
"Failed at block idx = ", block_idx);
101 info(
"Failed tag check.");
107 if (memory_data.rom_logup_sum != 0) {
108 info(
"Failed ROM-LogUp sum identity.");
116template <
typename Builder>
124 auto values = init_empty_values<Builder>();
126 params.
eta = memory_data.
eta;
131 auto report_fail = [&](
const char* message,
size_t row_idx) {
132#ifndef FUZZING_DISABLE_WARNINGS
133 info(message, row_idx);
138#ifdef CHECK_CIRCUIT_STACKTRACES
139 block.stack_traces.print(row_idx);
146 for (
size_t idx = 0; idx < block.size(); ++idx) {
150 result =
result && check_relation<Arithmetic>(values, params);
152 return report_fail(
"Failed Arithmetic relation at row idx = ", idx);
155 result =
result && check_relation<BilinearBatchedEq>(values, params);
157 return report_fail(
"Failed BilinearBatchedEq relation at row idx = ", idx);
160 result =
result && check_relation<Elliptic>(values, params);
162 return report_fail(
"Failed Elliptic relation at row idx = ", idx);
165 result =
result && check_memory_relation_with_logup<Memory>(values, params, memory_data);
167 return report_fail(
"Failed Memory relation at row idx = ", idx);
169 result =
result && check_relation<NonNativeField>(values, params);
171 return report_fail(
"Failed NonNativeField relation at row idx = ", idx);
173 result =
result && check_relation<DeltaRangeConstraint>(values, params);
175 return report_fail(
"Failed DeltaRangeConstraint relation at row idx = ", idx);
179 if (values.q_nnf() == 1) {
180 bool f0 = values.q_o() == 1 && (values.q_4() == 1 || values.q_m() == 1);
181 bool f1 = values.q_r() == 1 && (values.q_o() == 1 || values.q_4() == 1 || values.q_m() == 1);
183 result =
result && check_relation<NonNativeField>(values, params);
185 return report_fail(
"Failed NonNativeField relation at row idx = ", idx);
192 return report_fail(
"Failed Lookup check relation at row idx = ", idx);
194 result =
result && check_relation<PoseidonExternal>(values, params);
196 return report_fail(
"Failed PoseidonExternal relation at row idx = ", idx);
200 result =
result && check_relation<PoseidonInternal>(values, params);
202 return report_fail(
"Failed PoseidonInternal relation at row idx = ", idx);
206 result =
result && check_relation<PoseidonInitialExternal>(values, params);
208 return report_fail(
"Failed PoseidonInitialExternal relation at row idx = ", idx);
210 result =
result && check_relation<PoseidonQuadInternal>(values, params);
212 return report_fail(
"Failed PoseidonQuadInternal relation at row idx = ", idx);
214 result =
result && check_relation<PoseidonQuadInternalTerminal>(values, params);
216 return report_fail(
"Failed PoseidonQuadInternalTerminal relation at row idx = ", idx);
218 result =
result && check_relation<PoseidonTransitionEntry>(values, params);
220 return report_fail(
"Failed PoseidonTransitionEntry relation at row idx = ", idx);
224 return report_fail(
"Failed databus read at row idx = ", idx);
231 return report_fail(
"Failed at row idx = ", idx);
238template <
typename Relation,
typename Builder,
typename Block>
241 auto values = init_empty_values<Builder>();
247 params.
eta = memory_data.
eta;
250 return check_relation<Relation>(values, params);
257 SubrelationEvaluations subrelation_evaluations;
258 for (
auto& eval : subrelation_evaluations) {
263 Relation::accumulate(subrelation_evaluations, values, params, 1);
269 constexpr_for<0, std::tuple_size_v<SubrelationEvaluations>, 1>([&]<
size_t I>() {
270 if constexpr (subrelation_is_linearly_independent<Relation, I>()) {
283template <
typename Memory>
287 SubrelationEvaluations subrelation_evaluations;
288 for (
auto& eval : subrelation_evaluations) {
291 Memory::accumulate(subrelation_evaluations, values, params, 1);
294 constexpr_for<0, std::tuple_size_v<SubrelationEvaluations>, 1>([&]<
size_t I>() {
295 if constexpr (subrelation_is_linearly_independent<Memory, I>()) {
311 if (!values.q_lookup().is_zero()) {
312 return lookup_hash_table.contains({ values.w_l() + values.q_r() * values.w_l_shift(),
313 values.w_r() + values.q_m() * values.w_r_shift(),
314 values.w_o() + values.q_c() * values.w_o_shift(),
322 if (!values.q_busread().is_zero()) {
324 auto raw_read_idx =
static_cast<size_t>(
uint256_t(values.w_r()));
325 auto value = values.w_l();
329 auto bus_selectors = values.get_databus_selectors();
331 bool read_matched =
false;
332 for (
size_t bus_idx = 0; bus_idx < bus_selectors.size(); ++bus_idx) {
333 if (bus_selectors[bus_idx] == 1) {
334 const auto& bus_vec =
builder.get_bus_vector(bus_idx);
335 bus_value =
builder.get_variable(bus_vec[raw_read_idx]);
340 return (
value == bus_value);
350template <
typename Builder>
355 auto update_tag_check_data = [&](
const size_t variable_index,
const FF&
value) {
356 size_t real_index =
builder.real_variable_index[variable_index];
361 uint32_t tag_in =
builder.real_variable_tags[real_index];
362 if (tag_in != DEFAULT_TAG) {
363 uint32_t tag_out =
builder.tau().at(tag_in);
371 auto compute_memory_record_term =
372 [](
const FF& w_1,
const FF& w_2,
const FF& w_3,
const FF& eta,
const FF& eta_two,
FF& eta_three) {
373 return (w_3 * eta_three + w_2 * eta_two + w_1 * eta);
379 auto compute_rom_logup_inverse =
380 [](
const FF& w_1,
const FF& w_2,
const FF& q_c,
const FF& eta,
const FF& eta_two,
const FF& rom_logup_gamma)
382 const FF denom = rom_logup_gamma + w_1 + eta * w_2 + eta_two * q_c;
387 values.w_l() =
builder.get_variable(block.w_l()[idx]);
388 values.w_r() =
builder.get_variable(block.w_r()[idx]);
389 values.w_o() =
builder.get_variable(block.w_o()[idx]);
392 const bool is_ram_rom_block = (&block == &
builder.blocks.memory);
394 values.w_4() = compute_memory_record_term(
395 values.w_l(), values.w_r(), values.w_o(), memory_data.
eta, memory_data.
eta_two, memory_data.
eta_three);
398 compute_memory_record_term(
399 values.w_l(), values.w_r(), values.w_o(), memory_data.
eta, memory_data.
eta_two, memory_data.
eta_three) +
401 }
else if (is_ram_rom_block && memory_data.
rom_logup_gates.contains(idx)) {
403 compute_rom_logup_inverse(values.w_l(),
410 values.w_4() =
builder.get_variable(block.w_4()[idx]);
414 if (idx < block.size() - 1) {
415 values.w_l_shift() =
builder.get_variable(block.w_l()[idx + 1]);
416 values.w_r_shift() =
builder.get_variable(block.w_r()[idx + 1]);
417 values.w_o_shift() =
builder.get_variable(block.w_o()[idx + 1]);
419 values.w_4_shift() = compute_memory_record_term(values.w_l_shift(),
426 values.w_4_shift() = compute_memory_record_term(values.w_l_shift(),
433 }
else if (is_ram_rom_block && memory_data.
rom_logup_gates.contains(idx + 1)) {
434 values.w_4_shift() = compute_rom_logup_inverse(values.w_l_shift(),
436 block.q_c()[idx + 1],
441 values.w_4_shift() =
builder.get_variable(block.w_4()[idx + 1]);
444 values.w_l_shift() = 0;
445 values.w_r_shift() = 0;
446 values.w_o_shift() = 0;
447 values.w_4_shift() = 0;
451 update_tag_check_data(block.w_l()[idx], values.w_l());
452 update_tag_check_data(block.w_r()[idx], values.w_r());
453 update_tag_check_data(block.w_o()[idx], values.w_o());
454 update_tag_check_data(block.w_4()[idx], values.w_4());
457 values.q_m() = block.q_m()[idx];
458 values.q_c() = block.q_c()[idx];
459 values.q_l() = block.q_1()[idx];
460 values.q_r() = block.q_2()[idx];
461 values.q_o() = block.q_3()[idx];
462 values.q_4() = block.q_4()[idx];
471 values.q_5() = block.q_5()[idx];
476 values.q_poseidon2_quad_internal_terminal() =
497template <
typename Builder>
bool UltraCircuitChecker::relaxed_check_delta_range_relation(
Builder&
builder)
499 std::unordered_map<uint32_t, uint64_t> range_tags;
500 for (
const auto& list :
builder.range_lists) {
501 range_tags[list.second.range_tag] = list.first;
505 for (uint32_t i = 0; i <
builder.real_variable_tags.size(); i++) {
507 if (
tag != 0 && range_tags.contains(
tag)) {
511#ifndef FUZZING_DISABLE_WARNINGS
512 info(
"Failed range constraint on variable with index = ", i,
": ",
value,
" > ", range);
520 auto block =
builder.blocks.delta_range;
521 for (
size_t idx = 0; idx < block.size(); idx++) {
529 bb::fr w5 = idx == block.size() - 1 ?
builder.get_variable(0) :
builder.get_variable(block.w_l()[idx + 1]);
533#ifndef FUZZING_DISABLE_WARNINGS
534 info(
"Failed sort constraint relation at row idx = ", idx,
" with delta1 = ", delta);
541#ifndef FUZZING_DISABLE_WARNINGS
542 info(
"Failed sort constraint relation at row idx = ", idx,
" with delta2 = ", delta);
548#ifndef FUZZING_DISABLE_WARNINGS
549 info(
"Failed sort constraint at row idx = ", idx,
" with delta3 = ", delta);
555#ifndef FUZZING_DISABLE_WARNINGS
556 info(
"Failed sort constraint at row idx = ", idx,
" with delta4 = ", delta);
577template <
typename Builder>
bool UltraCircuitChecker::relaxed_check_memory_relation(
Builder&
builder)
579 for (
size_t i = 0; i <
builder.rom_ram_logic.rom_arrays.size(); i++) {
580 auto rom_array =
builder.rom_ram_logic.rom_arrays[i];
583 for (
auto& rr : rom_array.records) {
584 uint32_t value_witness_1 = rr.value_column1_witness;
585 uint32_t value_witness_2 = rr.value_column2_witness;
586 uint32_t
index =
static_cast<uint32_t
>(
builder.get_variable(rr.index_witness));
588 uint32_t table_witness_1 = rom_array.state[
index][0];
589 uint32_t table_witness_2 = rom_array.state[
index][1];
591 if (
builder.get_variable(value_witness_1) !=
builder.get_variable(table_witness_1)) {
592#ifndef FUZZING_DISABLE_WARNINGS
593 info(
"Failed SET/Read ROM[0] in table = ", i,
" at idx = ",
index);
597 if (
builder.get_variable(value_witness_2) !=
builder.get_variable(table_witness_2)) {
598#ifndef FUZZING_DISABLE_WARNINGS
599 info(
"Failed SET/Read ROM[1] in table = ", i,
" at idx = ",
index);
606 for (
size_t i = 0; i <
builder.rom_ram_logic.ram_arrays.size(); i++) {
607 auto ram_array =
builder.rom_ram_logic.ram_arrays[i];
609 std::vector<uint32_t> tmp_state(ram_array.state.size());
612 for (
auto& rr : ram_array.records) {
613 uint32_t
index =
static_cast<uint32_t
>(
builder.get_variable(rr.index_witness));
614 uint32_t value_witness = rr.value_witness;
615 auto access_type = rr.access_type;
617 uint32_t table_witness = tmp_state[
index];
619 switch (access_type) {
621 if (
builder.get_variable(value_witness) !=
builder.get_variable(table_witness)) {
622#ifndef FUZZING_DISABLE_WARNINGS
623 info(
"Failed RAM read in table = ", i,
" at idx = ",
index);
629 tmp_state[
index] = value_witness;
636 if (tmp_state != ram_array.state) {
637#ifndef FUZZING_DISABLE_WARNINGS
638 info(
"Failed RAM final state check at table = ", i);
648template bool UltraCircuitChecker::check<UltraCircuitBuilder_<UltraExecutionTraceBlocks>>(
649 const UltraCircuitBuilder_<UltraExecutionTraceBlocks>& builder_in);
654template bool UltraCircuitChecker::check_relation_at_row<Poseidon2ExternalRelation<bb::fr>>(
656template bool UltraCircuitChecker::check_relation_at_row<Poseidon2TransitionEntryRelation<bb::fr>>(
658template bool UltraCircuitChecker::check_relation_at_row<Poseidon2QuadInternalRelation<bb::fr>>(
660template bool UltraCircuitChecker::check_relation_at_row<Poseidon2QuadInternalTerminalRelation<bb::fr>>(
#define BB_ASSERT(expression,...)
ArrayOfValues< FF, RelationImpl::SUBRELATION_PARTIAL_LENGTHS > SumcheckArrayOfValuesOverSubrelations
std::unordered_set< Key, HashFunction > LookupHashTable
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 ...
static bool check_memory_relation_with_logup(auto &values, auto ¶ms, MemoryCheckData &memory_data)
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...
static bool check_relation(auto &values, auto ¶ms)
Check that a given relation is satisfied for the provided inputs corresponding to a single row.
static bool check_tag_data(const TagCheckData &tag_data)
Check whether the left and right running tag products are equal.
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.
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.
static bool check(const Builder &builder_in)
Check the correctness of a circuit witness.
static Builder prepare_circuit(const Builder &builder_in)
Copy the builder and finalize it before checking its validity.
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.
A field element for each entity of the flavor. These entities represent the prover polynomials evalua...
Entry point for Barretenberg command-line interface.
FF read_gate_selector(const ExecutionTraceBlock< FF, NUM_WIRES > &block, GateKind kind, size_t idx)
Gate-selector value at (block, idx) for kind, returning zero if the block does not own this kind or t...
@ Poseidon2QuadIntTerminal
@ Poseidon2TransitionEntry
constexpr decltype(auto) get(::tuplet::tuple< T... > &&t) noexcept
Struct for managing memory record data for ensuring RAM/ROM correctness.
std::unordered_set< size_t > read_record_gates
std::unordered_set< size_t > write_record_gates
std::unordered_set< size_t > rom_logup_gates
Struct for managing the running tag product data for ensuring tag correctness.
std::unordered_set< size_t > encountered_variables
static constexpr field one()
constexpr field invert() const noexcept