feat: Circuit checker class (#4931)

Moves the `check_circuit` functionality to a single new class called
`CircuitChecker` that utilizes Relations instead of redefining the
constraint algebra in the circuit builders.

The initial motivation for this work was to update the check circuit
functionality to handle the new block structure. I've decided to do a
larger refactor because notions like Flavor and Relations that did not
yet exist when check_circuit was originally implemented now allow for
substantial simplification. The overall logic remains equivalent. Most
of the file changes amount to `builder.check_circuit()` -->
`CircuitChecker::check(builder)`.

Note: the `CircuitChecker::check()` method receives a const reference to
a builder, makes a copy, finalizes that copy and performs checks on the
result. It is thus guaranteed that the original circuit is unchanged so
checks to this end have been removed from some tests.

Closes AztecProtocol/barretenberg#885 (Update
check circuit to handle block structure)
Closes AztecProtocol/barretenberg#806 (Use
Relations for check circuit)

barretenberg/cpp/src/CMakeLists.txt

@@ -49,6 +49,7 @@ else()
 endif()
 
 add_subdirectory(barretenberg/bb)
+add_subdirectory(barretenberg/circuit_checker)
 add_subdirectory(barretenberg/client_ivc)
 add_subdirectory(barretenberg/commitment_schemes)
 add_subdirectory(barretenberg/common)

barretenberg/cpp/src/barretenberg/circuit_checker/CMakeLists.txt

@@ -0,0 +1 @@
+barretenberg_module(circuit_checker proof_system flavor)

barretenberg/cpp/src/barretenberg/circuit_checker/circuit_checker.cpp

@@ -0,0 +1,190 @@
+#include "circuit_checker.hpp"
+#include "barretenberg/flavor/goblin_ultra.hpp"
+#include <barretenberg/plonk/proof_system/constants.hpp>
+#include <unordered_set>
+
+namespace bb {
+
+template <> auto CircuitChecker::init_empty_values<UltraCircuitBuilder_<UltraArith<bb::fr>>>()
+{
+    return UltraFlavor::AllValues{};
+}
+
+template <> auto CircuitChecker::init_empty_values<GoblinUltraCircuitBuilder_<bb::fr>>()
+{
+    return GoblinUltraFlavor::AllValues{};
+}
+
+template <typename Builder> bool CircuitChecker::check(const Builder& builder_in)
+{
+    // Create a copy of the input circuit and finalize it
+    Builder builder{ builder_in };
+    builder.finalize_circuit();
+
+    // Construct a hash table for lookup table entries to efficiently determine if a lookup gate is valid
+    LookupHashTable lookup_hash_table;
+    for (const auto& table : builder.lookup_tables) {
+        const FF table_index(table.table_index);
+        for (size_t i = 0; i < table.size; ++i) {
+            lookup_hash_table.insert({ table.column_1[i], table.column_2[i], table.column_3[i], table_index });
+        }
+    }
+
+    // Instantiate structs used for checking tag and memory record correctness
+    TagCheckData tag_data;
+    MemoryCheckData memory_data{ builder };
+
+    // Initialize empty AllValues of the correct Flavor based on Builder type; for input to Relation::accumulate
+    auto values = init_empty_values<Builder>();
+    Params params;
+    params.eta = memory_data.eta; // used in Auxiliary relation for RAM/ROM consistency
+
+    // TODO(https://github.com/AztecProtocol/barretenberg/issues/867): Once we sort gates into their respective blocks
+    // we'll need to either naively run this on all blocks or run only the relevant checks on each block.
+    auto& block = builder.blocks.main;
+
+    // Perform checks on each gate defined in the builder
+    bool result = true;
+    for (size_t idx = 0; idx < block.size(); ++idx) {
+        populate_values(builder, block, values, tag_data, memory_data, idx);
+
+        result = result && check_relation<Arithmetic>(values, params);
+        result = result && check_relation<Elliptic>(values, params);
+        result = result && check_relation<Auxiliary>(values, params);
+        result = result && check_relation<GenPermSort>(values, params);
+        result = result && check_lookup(values, lookup_hash_table);
+        if constexpr (IsGoblinBuilder<Builder>) {
+            result = result && check_relation<PoseidonInternal>(values, params);
+            result = result && check_relation<PoseidonExternal>(values, params);
+        }
+    }
+
+    // Tag check is only expected to pass after all gates have been processed
+    result = result && check_tag_data(tag_data);
+
+    return result;
+};
+
+template <typename Relation> bool CircuitChecker::check_relation(auto& values, auto& params)
+{
+    // Define zero initialized array to store the evaluation of each sub-relation
+    using SubrelationEvaluations = typename Relation::SumcheckArrayOfValuesOverSubrelations;
+    SubrelationEvaluations subrelation_evaluations;
+    for (auto& eval : subrelation_evaluations) {
+        eval = 0;
+    }
+
+    // Evaluate each subrelation in the relation
+    Relation::accumulate(subrelation_evaluations, values, params, /*scaling_factor=*/1);
+
+    // Ensure each subrelation evaluates to zero
+    for (auto& eval : subrelation_evaluations) {
+        if (eval != 0) {
+            return false;
+        }
+    }
+    return true;
+}
+
+bool CircuitChecker::check_lookup(auto& values, auto& lookup_hash_table)
+{
+    // If this is a lookup gate, check the inputs are in the hash table containing all table entries
+    if (!values.q_lookup.is_zero()) {
+        return lookup_hash_table.contains({ values.w_l + values.q_r * values.w_l_shift,
+                                            values.w_r + values.q_m * values.w_r_shift,
+                                            values.w_o + values.q_c * values.w_o_shift,
+                                            values.q_o });
+    }
+    return true;
+};
+
+bool CircuitChecker::check_tag_data(const TagCheckData& tag_data)
+{
+    return tag_data.left_product == tag_data.right_product;
+};
+
+template <typename Builder>
+void CircuitChecker::populate_values(
+    Builder& builder, auto& block, auto& values, TagCheckData& tag_data, MemoryCheckData& memory_data, size_t idx)
+{
+    // Function to quickly update tag products and encountered variable set by index and value
+    auto update_tag_check_data = [&](const size_t variable_index, const FF& value) {
+        size_t real_index = builder.real_variable_index[variable_index];
+        // Check to ensure that we are not including a variable twice
+        if (tag_data.encountered_variables.contains(real_index)) {
+            return;
+        }
+        uint32_t tag_in = builder.real_variable_tags[real_index];
+        if (tag_in != DUMMY_TAG) {
+            uint32_t tag_out = builder.tau.at(tag_in);
+            tag_data.left_product *= value + tag_data.gamma * FF(tag_in);
+            tag_data.right_product *= value + tag_data.gamma * FF(tag_out);
+            tag_data.encountered_variables.insert(real_index);
+        }
+    };
+
+    // A lambda function for computing a memory record term of the form w3 * eta^3 + w2 * eta^2 + w1 * eta
+    auto compute_memory_record_term = [](const FF& w_1, const FF& w_2, const FF& w_3, const FF& eta) {
+        return ((w_3 * eta + w_2) * eta + w_1) * eta;
+    };
+
+    // Set wire values. Wire 4 is treated specially since it may contain memory records
+    values.w_l = builder.get_variable(block.w_l()[idx]);
+    values.w_r = builder.get_variable(block.w_r()[idx]);
+    values.w_o = builder.get_variable(block.w_o()[idx]);
+    if (memory_data.read_record_gates.contains(idx)) {
+        values.w_4 = compute_memory_record_term(values.w_l, values.w_r, values.w_o, memory_data.eta);
+    } else if (memory_data.write_record_gates.contains(idx)) {
+        values.w_4 = compute_memory_record_term(values.w_l, values.w_r, values.w_o, memory_data.eta) + FF::one();
+    } else {
+        values.w_4 = builder.get_variable(block.w_4()[idx]);
+    }
+
+    // Set shifted wire values. Again, wire 4 is treated specially. On final row, set shift values to zero
+    values.w_l_shift = idx < block.size() - 1 ? builder.get_variable(block.w_l()[idx + 1]) : 0;
+    values.w_r_shift = idx < block.size() - 1 ? builder.get_variable(block.w_r()[idx + 1]) : 0;
+    values.w_o_shift = idx < block.size() - 1 ? builder.get_variable(block.w_o()[idx + 1]) : 0;
+    if (memory_data.read_record_gates.contains(idx + 1)) {
+        values.w_4_shift =
+            compute_memory_record_term(values.w_l_shift, values.w_r_shift, values.w_o_shift, memory_data.eta);
+    } else if (memory_data.write_record_gates.contains(idx + 1)) {
+        values.w_4_shift =
+            compute_memory_record_term(values.w_l_shift, values.w_r_shift, values.w_o_shift, memory_data.eta) +
+            FF::one();
+    } else {
+        values.w_4_shift = idx < block.size() - 1 ? builder.get_variable(block.w_4()[idx + 1]) : 0;
+    }
+
+    // Update tag check data
+    update_tag_check_data(block.w_l()[idx], values.w_l);
+    update_tag_check_data(block.w_r()[idx], values.w_r);
+    update_tag_check_data(block.w_o()[idx], values.w_o);
+    update_tag_check_data(block.w_4()[idx], values.w_4);
+
+    // Set selector values
+    values.q_m = block.q_m()[idx];
+    values.q_c = block.q_c()[idx];
+    values.q_l = block.q_1()[idx];
+    values.q_r = block.q_2()[idx];
+    values.q_o = block.q_3()[idx];
+    values.q_4 = block.q_4()[idx];
+    values.q_arith = block.q_arith()[idx];
+    values.q_sort = block.q_sort()[idx];
+    values.q_elliptic = block.q_elliptic()[idx];
+    values.q_aux = block.q_aux()[idx];
+    values.q_lookup = block.q_lookup_type()[idx];
+    if constexpr (IsGoblinBuilder<Builder>) {
+        values.q_poseidon2_internal = block.q_poseidon2_internal()[idx];
+        values.q_poseidon2_external = block.q_poseidon2_external()[idx];
+    }
+}
+
+// Template method instantiations for each check method
+// template bool CircuitChecker::check<bb::fr>(const StandardCircuitBuilder_<bb::fr>& builder);
+// template bool CircuitChecker::check<bb::fq>(const StandardCircuitBuilder_<bb::fq>& builder);
+template bool CircuitChecker::check<UltraCircuitBuilder_<UltraArith<bb::fr>>>(
+    const UltraCircuitBuilder_<UltraArith<bb::fr>>& builder_in);
+template bool CircuitChecker::check<GoblinUltraCircuitBuilder_<bb::fr>>(
+    const GoblinUltraCircuitBuilder_<bb::fr>& builder_in);
+
+} // namespace bb

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

@@ -0,0 +1,169 @@
+#pragma once
+#include "barretenberg/flavor/ultra.hpp"
+#include "barretenberg/proof_system/circuit_builder/standard_circuit_builder.hpp"
+#include "barretenberg/proof_system/circuit_builder/ultra_circuit_builder.hpp"
+#include "barretenberg/relations/auxiliary_relation.hpp"
+#include "barretenberg/relations/ecc_op_queue_relation.hpp"
+#include "barretenberg/relations/elliptic_relation.hpp"
+#include "barretenberg/relations/gen_perm_sort_relation.hpp"
+#include "barretenberg/relations/poseidon2_external_relation.hpp"
+#include "barretenberg/relations/poseidon2_internal_relation.hpp"
+#include "barretenberg/relations/relation_parameters.hpp"
+#include "barretenberg/relations/ultra_arithmetic_relation.hpp"
+
+#include <optional>
+
+namespace bb {
+
+class CircuitChecker {
+  public:
+    using FF = bb::fr;
+    using Arithmetic = UltraArithmeticRelation<FF>;
+    using Elliptic = EllipticRelation<FF>;
+    using Auxiliary = AuxiliaryRelation<FF>;
+    using GenPermSort = GenPermSortRelation<FF>;
+    using PoseidonExternal = Poseidon2ExternalRelation<FF>;
+    using PoseidonInternal = Poseidon2InternalRelation<FF>;
+    using Params = RelationParameters<FF>;
+
+    /**
+     * @brief Check the correctness of a circuit witness
+     * @details Ensures that all relations for a given 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.
+     *
+     * @tparam Builder
+     * @param builder
+     */
+    template <typename Builder> static bool check(const Builder& builder);
+
+    /**
+     * @brief Specialized circuit checker for the Standard builder
+     *
+     * @tparam FF Allows for use with scalar field for bn254 or grumpkin
+     * @param builder
+     */
+    template <typename FF> static bool check(const StandardCircuitBuilder_<FF>& builder)
+    {
+        const auto& block = builder.blocks.arithmetic;
+        for (size_t i = 0; i < builder.num_gates; i++) {
+            FF left = builder.get_variable(block.w_l()[i]);
+            FF right = builder.get_variable(block.w_r()[i]);
+            FF output = builder.get_variable(block.w_o()[i]);
+            FF gate_sum = block.q_m()[i] * left * right + block.q_1()[i] * left + block.q_2()[i] * right +
+                          block.q_3()[i] * output + block.q_c()[i];
+            if (!gate_sum.is_zero()) {
+                info("gate number", i);
+                return false;
+            }
+        }
+        return true;
+    }
+
+  private:
+    struct TagCheckData;
+    struct MemoryCheckData;
+
+    /**
+     * @brief 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.
+     *
+     * @tparam Relation
+     * @param values Values of the relation inputs at a single row
+     * @param params
+     */
+    template <typename Relation> static bool check_relation(auto& values, auto& params);
+
+    /**
+     * @brief Check whether the values in a lookup gate are contained within a corresponding hash table
+     *
+     * @param values Inputs to a lookup gate
+     * @param lookup_hash_table Preconstructed hash table representing entries of all tables in circuit
+     */
+    static bool check_lookup(auto& values, auto& lookup_hash_table);
+
+    /**
+     * @brief 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
+     *
+     * @param tag_data
+     */
+    static bool check_tag_data(const TagCheckData& tag_data);
+
+    /**
+     * @brief Helper for initializing an empty AllValues container of the right Flavor based on Builder
+     * @details 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 GoblinUltraFlavor is used for the GoblinUltra
+     * builder
+     *
+     * @tparam Builder
+     */
+    template <typename Builder> static auto init_empty_values();
+
+    /**
+     * @brief Populate the values required to check the correctness of a single "row" of the circuit
+     * @details Populates all wire values (plus shifts) and selectors. Updates running tag product information.
+     * Populates 4th wire with memory records (as needed).
+     *
+     * @tparam Builder
+     * @param builder
+     * @param values
+     * @param tag_data
+     * @param idx
+     */
+    template <typename Builder>
+    static void populate_values(
+        Builder& builder, auto& block, auto& values, TagCheckData& tag_data, MemoryCheckData& memory_data, size_t idx);
+
+    /**
+     * @brief Struct for managing the running tag product data for ensuring tag correctness
+     */
+    struct TagCheckData {
+        FF left_product = FF::one();           // product of (value + γ ⋅ tag)
+        FF right_product = FF::one();          // product of (value + γ ⋅ tau[tag])
+        const FF gamma = FF::random_element(); // randomness for the tag check
+
+        // We need to include each variable only once
+        std::unordered_set<size_t> encountered_variables;
+    };
+
+    /**
+     * @brief Struct for managing memory record data for ensuring RAM/ROM correctness
+     */
+    struct MemoryCheckData {
+        FF eta = FF::random_element(); // randomness for constructing wire 4 mem records
+
+        std::unordered_set<size_t> read_record_gates;  // row indices for gates containing RAM/ROM read mem record
+        std::unordered_set<size_t> write_record_gates; // row indices for gates containing RAM/ROM write mem record
+        // Construct hash tables for memory read/write indices to efficiently determine if row is a memory record
+        MemoryCheckData(const auto& builder)
+        {
+            for (const auto& gate_idx : builder.memory_read_records) {
+                read_record_gates.insert(gate_idx);
+            }
+            for (const auto& gate_idx : builder.memory_write_records) {
+                write_record_gates.insert(gate_idx);
+            }
+        }
+    };
+
+    // Define a hash table for efficiently checking if lookups are present in the set of tables used by the circuit
+    using Key = std::array<FF, 4>; // key value is the four wire inputs for a lookup gates
+    struct HashFunction {
+        const FF mult_const = FF(uint256_t(0x1337, 0x1336, 0x1335, 0x1334));
+        const FF mc_sqr = mult_const.sqr();
+        const FF mc_cube = mult_const * mc_sqr;
+
+        size_t operator()(const Key& entry) const
+        {
+            FF result = entry[0] + mult_const * entry[1] + mc_sqr * entry[2] + mc_cube * entry[3];
+            return static_cast<size_t>(result.reduce_once().data[0]);
+        }
+    };
+    using LookupHashTable = std::unordered_set<Key, HashFunction>;
+};
+} // namespace bb