feat: Circuit checker class

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