From f9634a7d05c062e20ff33098fe5751c43495c0ab Mon Sep 17 00:00:00 2001 From: Rumata888 Date: Fri, 21 Apr 2023 14:38:59 +0000 Subject: [PATCH] Added comments and state checks --- .../ultra_circuit_constructor.cpp | 64 ++--- .../ultra_circuit_constructor.hpp | 218 +++++++++++++++++- .../ultra_circuit_constructor.test.cpp | 2 + 3 files changed, 255 insertions(+), 29 deletions(-) diff --git a/cpp/src/barretenberg/proof_system/circuit_constructors/ultra_circuit_constructor.cpp b/cpp/src/barretenberg/proof_system/circuit_constructors/ultra_circuit_constructor.cpp index fe88c65827..5cded3381e 100644 --- a/cpp/src/barretenberg/proof_system/circuit_constructors/ultra_circuit_constructor.cpp +++ b/cpp/src/barretenberg/proof_system/circuit_constructors/ultra_circuit_constructor.cpp @@ -44,7 +44,7 @@ void UltraCircuitConstructor::finalize_circuit() * our circuit is finalised, and we must not to execute these functions again. */ bool switched_circuit_finalised = - (in_the_head && circuit_in_the_head.circuit_finalized) | (!in_the_head && circuit_finalised); + (in_the_head && circuit_in_the_head.circuit_finalised) | (!in_the_head && circuit_finalised); if (!switched_circuit_finalised) { process_ROM_arrays(public_inputs.size()); process_RAM_arrays(public_inputs.size()); @@ -1856,8 +1856,9 @@ void UltraCircuitConstructor::create_sorted_RAM_gate(RamRecord& record) */ void UltraCircuitConstructor::create_final_sorted_RAM_gate(RamRecord& record, const size_t ram_array_size) { + ENABLE_ALL_IN_THE_HEAD_SWITCHES record.record_witness = add_variable(0); - record.gate_index = num_gates; + record.gate_index = switched_num_gates; create_big_add_gate({ record.index_witness, @@ -2935,7 +2936,10 @@ inline fr UltraCircuitConstructor::compute_auxilary_identity(fr q_aux_value, } /** - * @brief + * @brief Check that the circuit is correct in its current state + * + * @details The method switches the circuit to the "in-the-head" version, finalizes it, checks gates, lookups and + * permutations and then switches it back from the in-the-head version, discarding the updates * * @return true * @return false @@ -2943,9 +2947,12 @@ inline fr UltraCircuitConstructor::compute_auxilary_identity(fr q_aux_value, bool UltraCircuitConstructor::check_circuit() { bool result = true; - reset_circuit_in_the_head(); + // Put the circuit in the head + update_circuit_in_the_head(); in_the_head = true; + // Finalize circuit-in-the-head finalize_circuit(); + // Sample randomness const fr arithmetic_base = fr::random_element(); const fr elliptic_base = fr::random_element(); const fr genperm_sort_base = fr::random_element(); @@ -2953,28 +2960,22 @@ bool UltraCircuitConstructor::check_circuit() const fr alpha = fr::random_element(); const fr eta = fr::random_element(); const fr eta_sqr = eta.sqr(); - // We need to update memory records + + // We need to get all memory std::unordered_set memory_record_gates; for (const auto& gate_idx : circuit_in_the_head.memory_read_records) { memory_record_gates.insert(gate_idx); - circuit_in_the_head.variables[circuit_in_the_head.real_variable_index[w_4[gate_idx]]] = - circuit_in_the_head.variables[real_variable_index[w_l[gate_idx]]] + - circuit_in_the_head.variables[circuit_in_the_head.real_variable_index[w_r[gate_idx]]] * eta + - circuit_in_the_head.variables[circuit_in_the_head.real_variable_index[w_o[gate_idx]]] * eta_sqr; } for (const auto& gate_idx : circuit_in_the_head.memory_write_records) { memory_record_gates.insert(gate_idx); - variables[real_variable_index[w_4[gate_idx]]] = variables[real_variable_index[w_l[gate_idx]]] + - variables[real_variable_index[w_r[gate_idx]]] * eta + - variables[real_variable_index[w_o[gate_idx]]] * eta_sqr; } + // A hashing implementation for quick simulation lookups struct HashFrTuple { const barretenberg::fr mult_const = barretenberg::fr(uint256_t(0x1337, 0x1336, 0x1335, 0x1334)); const barretenberg::fr mc_sqr = mult_const.sqr(); const barretenberg::fr mc_cube = mult_const * mc_sqr; - public: size_t operator()( const std::tuple& entry) const { @@ -2985,12 +2986,9 @@ bool UltraCircuitConstructor::check_circuit() } }; + // Equality checks for lookup tuples struct EqualFrTuple { - const barretenberg::fr mult_const = barretenberg::fr(uint256_t(0xdead, 0xbeef, 0xc0ff, 0xffee)); - const barretenberg::fr mc_sqr = mult_const.sqr(); - const barretenberg::fr mc_cube = mult_const * mc_sqr; - public: bool operator()( const std::tuple& entry1, const std::tuple& entry2) const @@ -2998,10 +2996,12 @@ bool UltraCircuitConstructor::check_circuit() return entry1 == entry2; } }; + // The set of all lookup tuples that are in the tables std::unordered_set, HashFrTuple, EqualFrTuple> table_hash; + // Prepare the lookup set for use in the circuit for (auto& table : lookup_tables) { const fr table_index(table.table_index); for (size_t i = 0; i < table.size; ++i) { @@ -3010,13 +3010,21 @@ bool UltraCircuitConstructor::check_circuit() table_hash.insert(components); } } + + // We use a running tag product mechanism to ensure tag correctness + // This is the product of (value + γ ⋅ tag) fr left_tag_product = fr::one(); + // This is the product of (value + γ ⋅ tau[tag]) fr right_tag_product = fr::one(); + // Randomness for the tag check const fr tag_gamma = fr::random_element(); + // We need to include each variable only once std::unordered_set encountered_variables; + // Function to quickly update tag products and encountered variable set by index and value auto update_tag_check_information = [&](size_t variable_index, fr value) { size_t real_index = circuit_in_the_head.real_variable_index[variable_index]; + // Check to ensure that we are not including a variable twice if (encountered_variables.contains(real_index)) { return; } @@ -3028,6 +3036,7 @@ bool UltraCircuitConstructor::check_circuit() encountered_variables.insert(real_index); } }; + // For each gate for (size_t i = 0; i < circuit_in_the_head.num_gates; i++) { fr q_arith_value; fr q_aux_value; @@ -3040,7 +3049,6 @@ bool UltraCircuitConstructor::check_circuit() fr q_4_value; fr q_m_value; fr q_c_value; - fr w_1_value; fr w_2_value; fr w_3_value; @@ -3049,6 +3057,7 @@ bool UltraCircuitConstructor::check_circuit() fr w_2_real_index; fr w_3_real_index; fr w_4_real_index; + // Get the values of selectors and wires and update tag products along the way if (i < num_gates) { q_arith_value = q_arith[i]; q_aux_value = q_aux[i]; @@ -3071,12 +3080,13 @@ bool UltraCircuitConstructor::check_circuit() update_tag_check_information(w_4[i], w_4_value); } else { + // The in-the-head selector and wire variable indices are not copies of the circuit values, but rather the + // continuation of them, so we need to access them at an offset size_t offset = i - num_gates; q_arith_value = circuit_in_the_head.q_arith[offset]; q_aux_value = circuit_in_the_head.q_aux[offset]; q_elliptic_value = circuit_in_the_head.q_elliptic[offset]; q_sort_value = circuit_in_the_head.q_sort[offset]; - q_lookup_type_value = circuit_in_the_head.q_lookup_type[i]; q_1_value = circuit_in_the_head.q_1[offset]; q_2_value = circuit_in_the_head.q_2[offset]; @@ -3093,6 +3103,7 @@ bool UltraCircuitConstructor::check_circuit() w_4_value = get_variable(circuit_in_the_head.w_4[offset]); update_tag_check_information(circuit_in_the_head.w_4[offset], w_4_value); } + // If we are touching a gate with memory access, we need to update the value of the 4th witness if (memory_record_gates.contains(i)) { w_4_value = w_1_value + eta * w_2_value + eta_sqr * w_3_value; } @@ -3200,13 +3211,14 @@ bool UltraCircuitConstructor::check_circuit() } in_the_head = false; return result; -} // namespace proof_system +} /** - * @brief Reset the circuit-in-the-head construction that we use for checking the correctness of the circuit + * @brief Reset the circuit-in-the-head construction that we use for checking the correctness of the circuit to the + * values in the circuit * */ -void UltraCircuitConstructor::reset_circuit_in_the_head() +void UltraCircuitConstructor::update_circuit_in_the_head() { // Unfortunately we have to copy all variable structures circuit_in_the_head.public_inputs = public_inputs; @@ -3234,18 +3246,18 @@ void UltraCircuitConstructor::reset_circuit_in_the_head() // Update current tag in the head to be the same as current real tag circuit_in_the_head.current_tag = current_tag; // Reset tau - circuit_in_the_head.tau.clear(); + circuit_in_the_head.tau = tau; // Copy rom and ram arrays circuit_in_the_head.rom_arrays = rom_arrays; circuit_in_the_head.ram_arrays = ram_arrays; - circuit_in_the_head.memory_read_records.clear(); - circuit_in_the_head.memory_write_records.clear(); + circuit_in_the_head.memory_read_records = memory_read_records; + circuit_in_the_head.memory_write_records = memory_write_records; circuit_in_the_head.ram_arrays = ram_arrays; circuit_in_the_head.rom_arrays = rom_arrays; circuit_in_the_head.range_lists = range_lists; circuit_in_the_head.num_gates = num_gates; - circuit_finalised = false; + circuit_in_the_head.circuit_finalised = circuit_finalised; } } // namespace proof_system \ No newline at end of file diff --git a/cpp/src/barretenberg/proof_system/circuit_constructors/ultra_circuit_constructor.hpp b/cpp/src/barretenberg/proof_system/circuit_constructors/ultra_circuit_constructor.hpp index 2c40c12659..100caa8b20 100644 --- a/cpp/src/barretenberg/proof_system/circuit_constructors/ultra_circuit_constructor.hpp +++ b/cpp/src/barretenberg/proof_system/circuit_constructors/ultra_circuit_constructor.hpp @@ -12,7 +12,6 @@ #include namespace proof_system { - static constexpr ComposerType type = ComposerType::PLOOKUP; static constexpr merkle::HashType merkle_hash_type = merkle::HashType::LOOKUP_PEDERSEN; static constexpr size_t NUM_RESERVED_GATES = 4; // This must be >= num_roots_cut_out_of_vanishing_polynomial @@ -61,6 +60,11 @@ struct RangeList { uint32_t range_tag; uint32_t tau_tag; std::vector variable_indices; + bool operator==(const RangeList& other) const noexcept + { + return target_range == other.target_range && range_tag == other.range_tag && tau_tag == other.tau_tag && + variable_indices == other.variable_indices; + } }; /** @@ -76,6 +80,12 @@ struct RomRecord { uint32_t record_witness = 0; size_t gate_index = 0; bool operator<(const RomRecord& other) const { return index < other.index; } + bool operator==(const RomRecord& other) const noexcept + { + return index_witness == other.index_witness && value_column1_witness == other.value_column1_witness && + value_column2_witness == other.value_column2_witness && index == other.index && + record_witness == other.record_witness && gate_index == other.gate_index; + } }; /** @@ -101,6 +111,13 @@ struct RamRecord { bool index_test = (index) < (other.index); return index_test || (index == other.index && timestamp < other.timestamp); } + bool operator==(const RamRecord& other) const noexcept + { + return index_witness == other.index_witness && timestamp_witness == other.timestamp_witness && + value_witness == other.value_witness && index == other.index && timestamp == other.timestamp && + access_type == other.access_type && record_witness == other.record_witness && + gate_index == other.gate_index; + } }; /** @@ -121,6 +138,11 @@ struct RamTranscript { // used for RAM records, to compute the timestamp when performing a read/write size_t access_count = 0; + // Used to check that the state hasn't changed in tests + bool operator==(const RamTranscript& other) const noexcept + { + return (state == other.state && records == other.records && access_count == other.access_count); + } }; /** @@ -138,6 +160,12 @@ struct RomTranscript { // + The value in the memory slot // + The actual index value std::vector records; + + // Used to check that the state hasn't changed in tests + bool operator==(const RomTranscript& other) const noexcept + { + return (state == other.state && records == other.records); + } }; inline std::vector ultra_selector_names() @@ -147,6 +175,14 @@ inline std::vector ultra_selector_names() return result; } +/** + * @brief Circuit-in-the-head is a structure we use to store all the information about the circuit which should be used + * during check_circuit method call, but needs to be discarded later + * + * @details In check_circuit method in UltraCircuitConstructor we want to check that the whole circuit works, but ultra + * circuits need to have ram, rom and range gates added in the end for the check to be complete as well as the set + * permutation check. + */ struct CircuitInTheHead { std::vector public_inputs; std::vector variables; @@ -183,10 +219,167 @@ struct CircuitInTheHead { std::vector memory_write_records; std::map range_lists; size_t num_gates; - bool circuit_finalized = false; + bool circuit_finalised = false; + /** + * @brief Stores the state of everything logic-related in the constructor. + * + * @details We need this function for tests. Specifically, to ensure that we are not changing anything in + * check_circuit + * + * @param circuit_constructor + * @return CircuitInTheHead + */ + template + static CircuitInTheHead store_state(const CircuitConstructor& circuit_constructor) + { + CircuitInTheHead stored_state; + stored_state.public_inputs = circuit_constructor.public_inputs; + stored_state.variables = circuit_constructor.variables; + + stored_state.next_var_index = circuit_constructor.next_var_index; + + stored_state.prev_var_index = circuit_constructor.prev_var_index; + + stored_state.real_variable_index = circuit_constructor.real_variable_index; + stored_state.real_variable_tags = circuit_constructor.real_variable_tags; + stored_state.constant_variable_indices = circuit_constructor.constant_variable_indices; + stored_state.w_l = circuit_constructor.w_l; + stored_state.w_r = circuit_constructor.w_r; + stored_state.w_o = circuit_constructor.w_o; + stored_state.w_4 = circuit_constructor.w_4; + stored_state.q_m = circuit_constructor.q_m; + stored_state.q_c = circuit_constructor.q_c; + stored_state.q_1 = circuit_constructor.q_1; + stored_state.q_2 = circuit_constructor.q_2; + stored_state.q_3 = circuit_constructor.q_3; + stored_state.q_4 = circuit_constructor.q_4; + stored_state.q_arith = circuit_constructor.q_arith; + stored_state.q_sort = circuit_constructor.q_sort; + stored_state.q_elliptic = circuit_constructor.q_elliptic; + stored_state.q_aux = circuit_constructor.q_aux; + stored_state.q_lookup_type = circuit_constructor.q_lookup_type; + stored_state.current_tag = circuit_constructor.current_tag; + stored_state.tau = circuit_constructor.tau; + + stored_state.ram_arrays = circuit_constructor.ram_arrays; + stored_state.rom_arrays = circuit_constructor.rom_arrays; + + stored_state.memory_read_records = circuit_constructor.memory_read_records; + stored_state.memory_write_records = circuit_constructor.memory_write_records; + stored_state.range_lists = circuit_constructor.range_lists; + stored_state.circuit_finalised = circuit_constructor.circuit_finalised; + stored_state.num_gates = circuit_constructor.num_gates; + return stored_state; + } + /** + * @brief CHecks that the circuit states is the same as the stored circuit's one + * + * @param circuit_constructor + * @return true + * @return false + */ + template bool is_same_state(const CircuitConstructor& circuit_constructor) + { + if (!(public_inputs == circuit_constructor.public_inputs)) { + return false; + } + if (!(variables == circuit_constructor.variables)) { + return false; + } + if (!(next_var_index == circuit_constructor.next_var_index)) { + return false; + } + if (!(prev_var_index == circuit_constructor.prev_var_index)) { + return false; + } + if (!(real_variable_index == circuit_constructor.real_variable_index)) { + return false; + } + if (!(real_variable_tags == circuit_constructor.real_variable_tags)) { + return false; + } + if (!(constant_variable_indices == circuit_constructor.constant_variable_indices)) { + return false; + } + if (!(w_l == circuit_constructor.w_l)) { + return false; + } + if (!(w_r == circuit_constructor.w_r)) { + return false; + } + if (!(w_o == circuit_constructor.w_o)) { + return false; + } + if (!(w_4 == circuit_constructor.w_4)) { + return false; + } + if (!(q_m == circuit_constructor.q_m)) { + return false; + } + if (!(q_c == circuit_constructor.q_c)) { + return false; + } + if (!(q_1 == circuit_constructor.q_1)) { + return false; + } + if (!(q_2 == circuit_constructor.q_2)) { + return false; + } + if (!(q_3 == circuit_constructor.q_3)) { + return false; + } + if (!(q_4 == circuit_constructor.q_4)) { + return false; + } + if (!(q_arith == circuit_constructor.q_arith)) { + return false; + } + if (!(q_sort == circuit_constructor.q_sort)) { + return false; + } + if (!(q_elliptic == circuit_constructor.q_elliptic)) { + return false; + } + if (!(q_aux == circuit_constructor.q_aux)) { + return false; + } + if (!(q_lookup_type == circuit_constructor.q_lookup_type)) { + return false; + } + if (!(current_tag == circuit_constructor.current_tag)) { + return false; + } + if (!(tau == circuit_constructor.tau)) { + return false; + } + if (!(ram_arrays == circuit_constructor.ram_arrays)) { + return false; + } + if (!(rom_arrays == circuit_constructor.rom_arrays)) { + return false; + } + if (!(memory_read_records == circuit_constructor.memory_read_records)) { + return false; + } + if (!(memory_write_records == circuit_constructor.memory_write_records)) { + return false; + } + if (!(range_lists == circuit_constructor.range_lists)) { + return false; + } + if (!(num_gates == circuit_constructor.num_gates)) { + return false; + } + if (!(circuit_finalised == circuit_constructor.circuit_finalised)) { + return false; + } + return true; + } }; class UltraCircuitConstructor : public CircuitConstructorBase { public: + // We use the concept of "Circuit-in-the-head" for the check_circuit method. We have to finalize the circuit to + // check it, so we put all the updates in this structure, instead of messing with the circuit itself CircuitInTheHead circuit_in_the_head; // Switch, forcing gates to interact with circuit_in_the_head instead of the regular members bool in_the_head = false; @@ -286,6 +479,12 @@ class UltraCircuitConstructor : public CircuitConstructorBase index); return circuit_in_the_head.variables[circuit_in_the_head.real_variable_index[index]]; } + + /** + * @brief Check that variable indices are valid + * + * @param variable_indices + */ void assert_valid_variables(const std::vector& variable_indices) { for (const auto& variable_index : variable_indices) { ASSERT(is_valid_variable(variable_index)); } } + /** + * @brief Checks that the variable index is valid (in the circuit or in the in-the-head circuit) + * + * @param variable_index + * @return true + * @return false + */ bool is_valid_variable(uint32_t variable_index) { if (in_the_head) { @@ -772,7 +984,7 @@ class UltraCircuitConstructor : public CircuitConstructorBase