Skip to content

Commit

Permalink
Added comments and state checks
Browse files Browse the repository at this point in the history
  • Loading branch information
@Rumata888
Rumata888 committed Apr 21, 2023
1 parent d13eab4 commit ae7f89b
Show file tree
Hide file tree
Showing 3 changed files with 255 additions and 29 deletions.
64 changes: 38 additions & 26 deletions cpp/src/barretenberg/proof_system/circuit_constructors/ultra_circuit_constructor.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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());
Expand Down Expand Up @@ -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,
Expand Down Expand Up @@ -2935,46 +2936,46 @@ 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
*/
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();
const fr auxillary_base = fr::random_element();
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<size_t> 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<barretenberg::fr, barretenberg::fr, barretenberg::fr, barretenberg::fr>& entry) const
{
Expand All @@ -2985,23 +2986,22 @@ 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<barretenberg::fr, barretenberg::fr, barretenberg::fr, barretenberg::fr>& entry1,
const std::tuple<barretenberg::fr, barretenberg::fr, barretenberg::fr, barretenberg::fr>& entry2) const
{
return entry1 == entry2;
}
};
// The set of all lookup tuples that are in the tables
std::unordered_set<std::tuple<barretenberg::fr, barretenberg::fr, barretenberg::fr, barretenberg::fr>,
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) {
Expand All @@ -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<size_t> 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;
}
Expand All @@ -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;
Expand All @@ -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;
Expand All @@ -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];
Expand All @@ -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];
Expand All @@ -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;
}
Expand Down Expand Up @@ -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;
Expand Down Expand Up @@ -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
Loading

0 comments on commit ae7f89b

Please sign in to comment.