From 378a2a39d9a38f0deccfdcb91df37555b36df126 Mon Sep 17 00:00:00 2001 From: adr1anh Date: Fri, 3 Mar 2023 09:35:32 +0000 Subject: [PATCH] implemented ram abstraction --- .../aztec/plonk/composer/composer_base.cpp | 2 + .../aztec/plonk/composer/ultra_composer.cpp | 547 ++++++++++++++++-- .../aztec/plonk/composer/ultra_composer.hpp | 228 ++++++-- .../plonk/composer/ultra_composer.test.cpp | 92 +++ .../plonk/proof_system/prover/prover.cpp | 22 +- .../plookup_auxiliary_widget.hpp | 224 +++++-- .../proof_system/proving_key/proving_key.cpp | 3 +- .../proof_system/proving_key/proving_key.hpp | 7 +- .../proof_system/proving_key/serialize.hpp | 12 +- 9 files changed, 958 insertions(+), 179 deletions(-) diff --git a/cpp/src/aztec/plonk/composer/composer_base.cpp b/cpp/src/aztec/plonk/composer/composer_base.cpp index d8e70aa16b..a9acf02141 100644 --- a/cpp/src/aztec/plonk/composer/composer_base.cpp +++ b/cpp/src/aztec/plonk/composer/composer_base.cpp @@ -154,6 +154,8 @@ template void ComposerBase::compute_sigma } if (last_node) { sigma_mappings[current_column][current_row].is_tag = true; + + // TODO: yikes, std::maps are expensive. Can we find a way to get rid of this? sigma_mappings[current_column][current_row].subgroup_index = tau.at(real_variable_tags[i]); } } diff --git a/cpp/src/aztec/plonk/composer/ultra_composer.cpp b/cpp/src/aztec/plonk/composer/ultra_composer.cpp index 5cb997b1ef..df6aa5b10c 100644 --- a/cpp/src/aztec/plonk/composer/ultra_composer.cpp +++ b/cpp/src/aztec/plonk/composer/ultra_composer.cpp @@ -266,6 +266,16 @@ void UltraComposer::create_balanced_add_gate(const add_quad& in) q_aux.emplace_back(0); ++num_gates; // Why 3? TODO: return to this + // The purpose of this gate is to do enable lazy 32-bit addition. + // Consider a + b = c mod 2^32 + // We want the 4th wire to represent the quotient: + // w1 + w2 = w4 * 2^32 + w3 + // If we allow this overflow 'flag' to range from 0 to 3, instead of 0 to 1, + // we can get away with chaining a few addition operations together with basic add gates, + // before having to use this gate. + // (N.B. a larger value would be better, the value '3' is for TurboPlonk backwards compatibility. + // In TurboPlonk this method uses a custom gate, + // where we were limited to a 2-bit range check by the degree of the custom gate identity. create_new_range_constraint(in.d, 3); } /** @@ -586,6 +596,7 @@ std::shared_ptr UltraComposer::compute_proving_key() */ if (!circuit_finalised) { process_ROM_arrays(public_inputs.size()); + process_RAM_arrays(public_inputs.size()); process_range_lists(); circuit_finalised = true; } @@ -697,7 +708,16 @@ std::shared_ptr UltraComposer::compute_proving_key() // TODO: composer-level constant variable needed for the program width compute_sigma_permutations<4, true>(circuit_proving_key.get()); - std::copy(memory_records.begin(), memory_records.end(), std::back_inserter(circuit_proving_key->memory_records)); + // Copy memory read/write record data into proving key. Prover needs to know which gates contain a read/write + // 'record' witness on the 4th wire. This wire value can only be fully computed once the first 3 wire polynomials + // have been committed to. The 4th wire on these gates will be a random linear combination of the first 3 wires, + // using the plookup challenge `eta` + std::copy(memory_read_records.begin(), + memory_read_records.end(), + std::back_inserter(circuit_proving_key->memory_read_records)); + std::copy(memory_write_records.begin(), + memory_write_records.end(), + std::back_inserter(circuit_proving_key->memory_write_records)); circuit_proving_key->recursive_proof_public_input_indices = std::vector(recursive_proof_public_input_indices.begin(), recursive_proof_public_input_indices.end()); @@ -1523,15 +1543,28 @@ std::vector UltraComposer::decompose_into_default_range_better_for_odd * values. So you can do: * q_aux * (q_1 * q_2 * statement_1 + q_3 * q_4 * statement_2). q_1=q_2=1 would activate statement_1, while q_3=q_4=1 * would activate statement_2 + * + * * Multiple selectors are used to 'switch' aux gates on/off according to the following pattern: + * + * | gate type | q_aux | q_1 | q_2 | q_3 | q_4 | q_m | q_c | q_arith | + * | ---------------------------- | ----- | --- | --- | --- | --- | --- | --- | ------ | + * | Bigfield Limb Accumulation 1 | 1 | 0 | 0 | 1 | 1 | 0 | --- | 0 | + * | Bigfield Limb Accumulation 2 | 1 | 0 | 0 | 1 | 0 | 1 | --- | 0 | + * | Bigfield Product 1 | 1 | 0 | 1 | 1 | 0 | 0 | --- | 0 | + * | Bigfield Product 2 | 1 | 0 | 1 | 0 | 1 | 0 | --- | 0 | + * | Bigfield Product 3 | 1 | 0 | 1 | 0 | 0 | 1 | --- | 0 | + * | RAM/ROM access gate | 1 | 1 | 0 | 0 | 0 | 1 | --- | 0 | + * | RAM timestamp check | 1 | 1 | 0 | 0 | 1 | 0 | --- | 0 | + * | ROM consistency check | 1 | 1 | 1 | 0 | 0 | 0 | --- | 0 | + * | RAM consistency check | 1 | 0 | 0 | 0 | 0 | 0 | 0 | 1 | + * * @param type */ void UltraComposer::apply_aux_selectors(const AUX_SELECTORS type) { ULTRA_SELECTOR_REFS; - q_arith.emplace_back(0); q_fixed_base.emplace_back(0); q_aux.emplace_back(type == AUX_SELECTORS::NONE ? 0 : 1); - q_c.emplace_back(0); q_sort.emplace_back(0); q_lookup_type.emplace_back(0); q_elliptic.emplace_back(0); @@ -1542,6 +1575,8 @@ void UltraComposer::apply_aux_selectors(const AUX_SELECTORS type) q_3.emplace_back(1); q_4.emplace_back(1); q_m.emplace_back(0); + q_c.emplace_back(0); + q_arith.emplace_back(0); break; } case AUX_SELECTORS::LIMB_ACCUMULATE_2: { @@ -1550,6 +1585,8 @@ void UltraComposer::apply_aux_selectors(const AUX_SELECTORS type) q_3.emplace_back(1); q_4.emplace_back(0); q_m.emplace_back(1); + q_c.emplace_back(0); + q_arith.emplace_back(0); break; } case AUX_SELECTORS::NON_NATIVE_FIELD_1: { @@ -1558,6 +1595,8 @@ void UltraComposer::apply_aux_selectors(const AUX_SELECTORS type) q_3.emplace_back(1); q_4.emplace_back(0); q_m.emplace_back(0); + q_c.emplace_back(0); + q_arith.emplace_back(0); break; } case AUX_SELECTORS::NON_NATIVE_FIELD_2: { @@ -1566,6 +1605,8 @@ void UltraComposer::apply_aux_selectors(const AUX_SELECTORS type) q_3.emplace_back(0); q_4.emplace_back(1); q_m.emplace_back(0); + q_c.emplace_back(0); + q_arith.emplace_back(0); break; } case AUX_SELECTORS::NON_NATIVE_FIELD_3: { @@ -1574,9 +1615,11 @@ void UltraComposer::apply_aux_selectors(const AUX_SELECTORS type) q_3.emplace_back(0); q_4.emplace_back(0); q_m.emplace_back(1); + q_c.emplace_back(0); + q_arith.emplace_back(0); break; } - case AUX_SELECTORS::CONSISTENT_SORTED_MEMORY_READ: { + case AUX_SELECTORS::ROM_CONSISTENCY_CHECK: { // Memory read gate used with the sorted list of memory reads. // Apply sorted memory read checks with the following additional check: // 1. Assert that if index field across two gates does not change, the value field does not change. @@ -1586,36 +1629,74 @@ void UltraComposer::apply_aux_selectors(const AUX_SELECTORS type) q_3.emplace_back(0); q_4.emplace_back(0); q_m.emplace_back(0); + q_c.emplace_back(0); + q_arith.emplace_back(0); break; } - case AUX_SELECTORS::SORTED_MEMORY_READ: { + case AUX_SELECTORS::RAM_CONSISTENCY_CHECK: { // Memory read gate used with the sorted list of memory reads. // 1. Validate adjacent index values across 2 gates increases by 0 or 1 - // 2. Validate record witness computation (r = index + \kappa timestamp * \kappa^2 * value) - // Used for ROM reads and RAM reads across read/write boundaries - q_1.emplace_back(1); + // 2. Validate record computation (r = read_write_flag + index * \eta + \timestamp * \eta^2 + value * \eta^3) + // 3. If adjacent index values across 2 gates does not change, and the next gate's read_write_flag is set to + // 'read', validate adjacent values do not change Used for ROM reads and RAM reads across read/write boundaries + q_1.emplace_back(0); q_2.emplace_back(0); - q_3.emplace_back(1); + q_3.emplace_back(0); q_4.emplace_back(0); q_m.emplace_back(0); + q_c.emplace_back(0); + q_arith.emplace_back(1); break; } - case AUX_SELECTORS::MEMORY_TIMESTAMP_CORRECTNESS: { + case AUX_SELECTORS::RAM_TIMESTAMP_CHECK: { + // For two adjacent RAM entries that share the same index, validate the timestamp value is monotonically + // increasing q_1.emplace_back(1); q_2.emplace_back(0); q_3.emplace_back(0); q_4.emplace_back(1); q_m.emplace_back(0); + q_c.emplace_back(0); + q_arith.emplace_back(0); break; } - case AUX_SELECTORS::MEMORY_READ: { - // Memory read gate for reading/writing memory cells. - // Validates record witness computation (r = index + \kappa timestamp * \kappa^2 * value) + case AUX_SELECTORS::ROM_READ: { + // Memory read gate for reading memory cells. + // Validates record witness computation (r = read_write_flag + index * \eta + timestamp * \eta^2 + value * + // \eta^3) q_1.emplace_back(1); q_2.emplace_back(0); q_3.emplace_back(0); q_4.emplace_back(0); q_m.emplace_back(1); // validate record witness is correctly computed + q_c.emplace_back(0); // read/write flag stored in q_c + q_arith.emplace_back(0); + break; + } + case AUX_SELECTORS::RAM_READ: { + // Memory read gate for reading memory cells. + // Validates record witness computation (r = read_write_flag + index * \eta + timestamp * \eta^2 + value * + // \eta^3) + q_1.emplace_back(1); + q_2.emplace_back(0); + q_3.emplace_back(0); + q_4.emplace_back(0); + q_m.emplace_back(1); // validate record witness is correctly computed + q_c.emplace_back(0); // read/write flag stored in q_c + q_arith.emplace_back(0); + break; + } + case AUX_SELECTORS::RAM_WRITE: { + // Memory read gate for writing memory cells. + // Validates record witness computation (r = read_write_flag + index * \eta + timestamp * \eta^2 + value * + // \eta^3) + q_1.emplace_back(1); + q_2.emplace_back(0); + q_3.emplace_back(0); + q_4.emplace_back(0); + q_m.emplace_back(1); // validate record witness is correctly computed + q_c.emplace_back(1); // read/write flag stored in q_c + q_arith.emplace_back(0); break; } default: { @@ -1624,6 +1705,8 @@ void UltraComposer::apply_aux_selectors(const AUX_SELECTORS type) q_3.emplace_back(0); q_4.emplace_back(0); q_m.emplace_back(0); + q_c.emplace_back(0); + q_arith.emplace_back(0); break; } } @@ -2239,27 +2322,39 @@ std::array UltraComposer::evaluate_non_native_field_subtraction( }; } -void UltraComposer::create_memory_gate(MemoryRecord& record) +/** + * @brief Gate that 'reads' from a ROM table. + * i.e. table index is a witness not precomputed + * + * @param record Stores details of this read operation. Mutated by this fn! + */ +void UltraComposer::create_ROM_gate(RomRecord& record) { // Record wire value can't yet be computed record.record_witness = add_variable(0); - apply_aux_selectors(AUX_SELECTORS::MEMORY_READ); + apply_aux_selectors(AUX_SELECTORS::ROM_READ); w_l.emplace_back(record.index_witness); - w_r.emplace_back(record.timestamp_witness); - w_o.emplace_back(record.value_witness); + w_r.emplace_back(record.value_column1_witness); + w_o.emplace_back(record.value_column2_witness); w_4.emplace_back(record.record_witness); record.gate_index = num_gates; ++num_gates; } -void UltraComposer::create_sorted_memory_gate(MemoryRecord& record, const bool is_ram_transition_or_rom) +/** + * @brief Gate that performs consistency checks to validate that a claimed ROM read value is correct + * + * @details sorted ROM gates are generated sequentially, each ROM record is sorted by index + * + * @param record Stores details of this read operation. Mutated by this fn! + */ +void UltraComposer::create_sorted_ROM_gate(RomRecord& record) { record.record_witness = add_variable(0); - apply_aux_selectors(is_ram_transition_or_rom ? AUX_SELECTORS::CONSISTENT_SORTED_MEMORY_READ - : AUX_SELECTORS::SORTED_MEMORY_READ); + apply_aux_selectors(AUX_SELECTORS::ROM_CONSISTENCY_CHECK); w_l.emplace_back(record.index_witness); - w_r.emplace_back(record.timestamp_witness); - w_o.emplace_back(record.value_witness); + w_r.emplace_back(record.value_column1_witness); + w_o.emplace_back(record.value_column2_witness); w_4.emplace_back(record.record_witness); record.gate_index = num_gates; @@ -2267,7 +2362,7 @@ void UltraComposer::create_sorted_memory_gate(MemoryRecord& record, const bool i } /** - * @brief Create a new memory region + * @brief Create a new read-only memory region * * @details Creates a transcript object, where the inside memory state array is filled with "uninitialized memory" and * and empty memory record array. Puts this object into the vector of ROM arrays. @@ -2277,7 +2372,7 @@ void UltraComposer::create_sorted_memory_gate(MemoryRecord& record, const bool i */ size_t UltraComposer::create_ROM_array(const size_t array_size) { - MemoryTranscript new_transcript; + RomTranscript new_transcript; for (size_t i = 0; i < array_size; ++i) { new_transcript.state.emplace_back( std::array{ UNINITIALIZED_MEMORY_RECORD, UNINITIALIZED_MEMORY_RECORD }); @@ -2286,6 +2381,173 @@ size_t UltraComposer::create_ROM_array(const size_t array_size) return rom_arrays.size() - 1; } +/** + * @brief Gate that performs a read/write operation into a RAM table. + * i.e. table index is a witness not precomputed + * + * @param record Stores details of this read operation. Mutated by this fn! + */ +void UltraComposer::create_RAM_gate(RamRecord& record) +{ + // Record wire value can't yet be computed (uses randomnes generated during proof construction). + // However it needs a distinct witness index, + // we will be applying copy constraints + set membership constraints. + // Later on during proof construction we will compute the record wire value + assign it + record.record_witness = add_variable(0); + apply_aux_selectors(record.access_type == RamRecord::AccessType::READ ? AUX_SELECTORS::RAM_READ + : AUX_SELECTORS::RAM_WRITE); + w_l.emplace_back(record.index_witness); + w_r.emplace_back(record.timestamp_witness); + w_o.emplace_back(record.value_witness); + w_4.emplace_back(record.record_witness); + record.gate_index = num_gates; + ++num_gates; +} + +/** + * @brief Gate that performs consistency checks to validate that a claimed RAM read/write value is correct + * + * @details sorted RAM gates are generated sequentially, each RAM record is sorted first by index then by timestamp + * + * @param record Stores details of this read operation. Mutated by this fn! + */ +void UltraComposer::create_sorted_RAM_gate(RamRecord& record) +{ + record.record_witness = add_variable(0); + apply_aux_selectors(AUX_SELECTORS::RAM_CONSISTENCY_CHECK); + w_l.emplace_back(record.index_witness); + w_r.emplace_back(record.timestamp_witness); + w_o.emplace_back(record.value_witness); + w_4.emplace_back(record.record_witness); + record.gate_index = num_gates; + ++num_gates; +} + +/** + * @brief Performs consistency checks to validate that a claimed RAM read/write value is correct. + * Used for the final gate in a list of sorted RAM records + * + * @param record Stores details of this read operation. Mutated by this fn! + */ +void UltraComposer::create_final_sorted_RAM_gate(RamRecord& record, const size_t ram_array_size) +{ + record.record_witness = add_variable(0); + record.gate_index = num_gates; + + create_big_add_gate({ + record.index_witness, + record.timestamp_witness, + record.value_witness, + record.record_witness, + 1, + 0, + 0, + 0, + -fr((uint64_t)ram_array_size - 1), + }); +} + +/** + * @brief Create a new updateable memory region + * + * @details Creates a transcript object, where the inside memory state array is filled with "uninitialized memory" and + * and empty memory record array. Puts this object into the vector of ROM arrays. + * + * @param array_size The size of region in elements + * @return size_t The index of the element + */ +size_t UltraComposer::create_RAM_array(const size_t array_size) +{ + RamTranscript new_transcript; + for (size_t i = 0; i < array_size; ++i) { + new_transcript.state.emplace_back(UNINITIALIZED_MEMORY_RECORD); + } + ram_arrays.emplace_back(new_transcript); + return ram_arrays.size() - 1; +} + +/** + * @brief Initialize a RAM cell to equal `value_witness` + * + * @param ram_id The index of the ROM array, which cell we are initializing + * @param index_value The index of the cell within the array (an actual index, not a witness index) + * @param value_witness The index of the witness with the value that should be in the + */ +void UltraComposer::init_RAM_element(const size_t ram_id, const size_t index_value, const uint32_t value_witness) +{ + ASSERT(ram_arrays.size() > ram_id); + RamTranscript& ram_array = ram_arrays[ram_id]; + const uint32_t index_witness = (index_value == 0) ? zero_idx : put_constant_variable((uint64_t)index_value); + ASSERT(ram_array.state.size() > index_value); + ASSERT(ram_array.state[index_value] == UNINITIALIZED_MEMORY_RECORD); + RamRecord new_record{ .index_witness = index_witness, + .timestamp_witness = put_constant_variable((uint64_t)ram_array.access_count), + .value_witness = value_witness, + .index = static_cast(index_value), // TODO: size_t? + .timestamp = static_cast(ram_array.access_count), + .access_type = RamRecord::AccessType::WRITE, + .record_witness = 0, + .gate_index = 0 }; + ram_array.state[index_value] = value_witness; + ram_array.access_count++; + create_RAM_gate(new_record); + ram_array.records.emplace_back(new_record); +} + +uint32_t UltraComposer::read_RAM_array(const size_t ram_id, const uint32_t index_witness) +{ + ASSERT(ram_arrays.size() > ram_id); + RamTranscript& ram_array = ram_arrays[ram_id]; + const uint32_t index = static_cast(uint256_t(get_variable(index_witness))); + ASSERT(ram_array.state.size() > index); + ASSERT(ram_array.state[index] != UNINITIALIZED_MEMORY_RECORD); + const auto value = get_variable(ram_array.state[index]); + const uint32_t value_witness = add_variable(value); + + RamRecord new_record{ .index_witness = index_witness, + .timestamp_witness = put_constant_variable((uint64_t)ram_array.access_count), + .value_witness = value_witness, + .index = index, + .timestamp = static_cast(ram_array.access_count), + .access_type = RamRecord::AccessType::READ, + .record_witness = 0, + .gate_index = 0 }; + create_RAM_gate(new_record); + ram_array.records.emplace_back(new_record); + + // increment ram array's access count + ram_array.access_count++; + + // return witness index of the value in the array + return value_witness; +} + +void UltraComposer::write_RAM_array(const size_t ram_id, const uint32_t index_witness, const uint32_t value_witness) +{ + ASSERT(ram_arrays.size() > ram_id); + RamTranscript& ram_array = ram_arrays[ram_id]; + const uint32_t index = static_cast(uint256_t(get_variable(index_witness))); + ASSERT(ram_array.state.size() > index); + ASSERT(ram_array.state[index] != UNINITIALIZED_MEMORY_RECORD); + + RamRecord new_record{ .index_witness = index_witness, + .timestamp_witness = put_constant_variable((uint64_t)ram_array.access_count), + .value_witness = value_witness, + .index = index, + .timestamp = static_cast(ram_array.access_count), + .access_type = RamRecord::AccessType::WRITE, + .record_witness = 0, + .gate_index = 0 }; + create_RAM_gate(new_record); + ram_array.records.emplace_back(new_record); + + // increment ram array's access count + ram_array.access_count++; + + // update Composer's current state of RAM array + ram_array.state[index] = value_witness; +} + /** * Initialize a ROM cell to equal `value_witness` * `index_value` is a RAW VALUE that describes the cell index. It is NOT a witness @@ -2303,7 +2565,7 @@ size_t UltraComposer::create_ROM_array(const size_t array_size) void UltraComposer::set_ROM_element(const size_t rom_id, const size_t index_value, const uint32_t value_witness) { ASSERT(rom_arrays.size() > rom_id); - auto& rom_array = rom_arrays[rom_id]; + RomTranscript& rom_array = rom_arrays[rom_id]; const uint32_t index_witness = (index_value == 0) ? zero_idx : put_constant_variable((uint64_t)index_value); ASSERT(rom_array.state.size() > index_value); ASSERT(rom_array.state[index_value][0] == UNINITIALIZED_MEMORY_RECORD); @@ -2319,12 +2581,17 @@ void UltraComposer::set_ROM_element(const size_t rom_id, const size_t index_valu * The second initialization value here is the witness, because in ROM it doesn't matter. We will decouple this * logic later. */ - MemoryRecord new_record{ - index_witness, value_witness, zero_idx, static_cast(index_value), 0, 0, 0, + RomRecord new_record{ + .index_witness = index_witness, + .value_column1_witness = value_witness, + .value_column2_witness = zero_idx, + .index = static_cast(index_value), + .record_witness = 0, + .gate_index = 0, }; rom_array.state[index_value][0] = value_witness; rom_array.state[index_value][1] = zero_idx; - create_memory_gate(new_record); + create_ROM_gate(new_record); rom_array.records.emplace_back(new_record); } @@ -2333,32 +2600,42 @@ void UltraComposer::set_ROM_element_pair(const size_t rom_id, const std::array& value_witnesses) { ASSERT(rom_arrays.size() > rom_id); - auto& rom_array = rom_arrays[rom_id]; + RomTranscript& rom_array = rom_arrays[rom_id]; const uint32_t index_witness = (index_value == 0) ? zero_idx : put_constant_variable((uint64_t)index_value); ASSERT(rom_array.state.size() > index_value); ASSERT(rom_array.state[index_value][0] == UNINITIALIZED_MEMORY_RECORD); - MemoryRecord new_record{ - index_witness, value_witnesses[0], value_witnesses[1], static_cast(index_value), 0, 0, 0, + RomRecord new_record{ + .index_witness = index_witness, + .value_column1_witness = value_witnesses[0], + .value_column2_witness = value_witnesses[1], + .index = static_cast(index_value), + .record_witness = 0, + .gate_index = 0, }; rom_array.state[index_value][0] = value_witnesses[0]; rom_array.state[index_value][1] = value_witnesses[1]; - create_memory_gate(new_record); + create_ROM_gate(new_record); rom_array.records.emplace_back(new_record); } uint32_t UltraComposer::read_ROM_array(const size_t rom_id, const uint32_t index_witness) { ASSERT(rom_arrays.size() > rom_id); - auto& rom_array = rom_arrays[rom_id]; + RomTranscript& rom_array = rom_arrays[rom_id]; const uint32_t index = static_cast(uint256_t(get_variable(index_witness))); ASSERT(rom_array.state.size() > index); ASSERT(rom_array.state[index][0] != UNINITIALIZED_MEMORY_RECORD); const auto value = get_variable(rom_array.state[index][0]); const uint32_t value_witness = add_variable(value); - MemoryRecord new_record{ - index_witness, value_witness, zero_idx, index, 0, 0, 0, + RomRecord new_record{ + .index_witness = index_witness, + .value_column1_witness = value_witness, + .value_column2_witness = zero_idx, + .index = index, + .record_witness = 0, + .gate_index = 0, }; - create_memory_gate(new_record); + create_ROM_gate(new_record); rom_array.records.emplace_back(new_record); // create_read_gate @@ -2371,7 +2648,7 @@ std::array UltraComposer::read_ROM_array_pair(const size_t rom_id, const uint32_t index = static_cast(uint256_t(get_variable(index_witness))); ASSERT(rom_arrays.size() > rom_id); - auto& rom_array = rom_arrays[rom_id]; + RomTranscript& rom_array = rom_arrays[rom_id]; ASSERT(rom_array.state.size() > index); ASSERT(rom_array.state[index][0] != UNINITIALIZED_MEMORY_RECORD); ASSERT(rom_array.state[index][1] != UNINITIALIZED_MEMORY_RECORD); @@ -2379,17 +2656,27 @@ std::array UltraComposer::read_ROM_array_pair(const size_t rom_id, const auto value2 = get_variable(rom_array.state[index][1]); value_witnesses[0] = add_variable(value1); value_witnesses[1] = add_variable(value2); - MemoryRecord new_record{ - index_witness, value_witnesses[0], value_witnesses[1], index, 0, 0, 0, + RomRecord new_record{ + .index_witness = index_witness, + .value_column1_witness = value_witnesses[0], + .value_column2_witness = value_witnesses[1], + .index = index, + .record_witness = 0, + .gate_index = 0, }; - - create_memory_gate(new_record); + create_ROM_gate(new_record); rom_array.records.emplace_back(new_record); // create_read_gate return value_witnesses; } +/** + * @brief Compute additional gates required to validate ROM reads. Called when generating the proving key + * + * @param rom_id The id of the ROM table + * @param gate_offset_from_public_inputs Required to track the gate position of where we're adding extra gates + */ void UltraComposer::process_ROM_array(const size_t rom_id, const size_t gate_offset_from_public_inputs) { auto& rom_array = rom_arrays[rom_id]; @@ -2411,22 +2698,37 @@ void UltraComposer::process_ROM_array(const size_t rom_id, const size_t gate_off std::sort(std::execution::par_unseq, rom_array.records.begin(), rom_array.records.end()); #endif - for (const auto& record : rom_array.records) { + for (const RomRecord& record : rom_array.records) { const auto index = record.index; - const auto value1 = get_variable(record.timestamp_witness); - const auto value2 = get_variable(record.value_witness); + const auto value1 = get_variable(record.value_column1_witness); + const auto value2 = get_variable(record.value_column2_witness); const auto index_witness = add_variable(fr((uint64_t)index)); const auto value1_witness = add_variable(value1); const auto value2_witness = add_variable(value2); - MemoryRecord sorted_record{ - index_witness, value1_witness, value2_witness, index, 0, 0, 0, + RomRecord sorted_record{ + .index_witness = index_witness, + .value_column1_witness = value1_witness, + .value_column2_witness = value2_witness, + .index = index, + .record_witness = 0, + .gate_index = 0, }; - create_sorted_memory_gate(sorted_record, true); + create_sorted_ROM_gate(sorted_record); + assign_tag(record.record_witness, read_tag); assign_tag(sorted_record.record_witness, sorted_list_tag); - memory_records.push_back(static_cast(sorted_record.gate_index + gate_offset_from_public_inputs)); - memory_records.push_back(static_cast(record.gate_index + gate_offset_from_public_inputs)); + // For ROM/RAM gates, the 'record' wire value (wire column 4) is a linear combination of the first 3 wire + // values. However...the record value uses the random challenge 'eta', generated after the first 3 wires are + // committed to. i.e. we can't compute the record witness here because we don't know what `eta` is! Take the + // gate indices of the two rom gates (original read gate + sorted gate) and store in `memory_records`. Once we + // generate the `eta` challenge, we'll use `memory_records` to figure out which gates need a record wire value + // to be computed. + // record (w4) = w3 * eta^3 + w2 * eta^2 + w1 * eta + read_write_flag (0 for reads, 1 for writes) + // Separate containers used to store gate indices of reads and writes. Need to differentiate because of + // `read_write_flag` (N.B. all ROM accesses are considered reads. Writes are for RAM operations) + memory_read_records.push_back(static_cast(sorted_record.gate_index + gate_offset_from_public_inputs)); + memory_read_records.push_back(static_cast(record.gate_index + gate_offset_from_public_inputs)); } // One of the checks we run on the sorted list, is to validate the difference between // the index field across two gates is either 0 or 1. @@ -2450,10 +2752,157 @@ void UltraComposer::process_ROM_array(const size_t rom_id, const size_t gate_off // because the first cell is explicitly initialized using zero_idx as the index field. } +/** + * @brief Compute additional gates required to validate RAM read/writes. Called when generating the proving key + * + * @param ram_id The id of the RAM table + * @param gate_offset_from_public_inputs Required to track the gate position of where we're adding extra gates + */ +void UltraComposer::process_RAM_array(const size_t ram_id, const size_t gate_offset_from_public_inputs) +{ + RamTranscript& ram_array = ram_arrays[ram_id]; + const auto access_tag = get_new_tag(); // current_tag + 1; + const auto sorted_list_tag = get_new_tag(); // current_tag + 2; + create_tag(access_tag, sorted_list_tag); + create_tag(sorted_list_tag, access_tag); + + // Make sure that every cell has been initialized + // TODO: throw some kind of error here? Circuit should initialize all RAM elements to prevent errors. + // e.g. if a RAM record is uninitialized but the index of that record is a function of public/private inputs, + // different public iputs will produce different circuit constraints. + for (size_t i = 0; i < ram_array.state.size(); ++i) { + if (ram_array.state[i] == UNINITIALIZED_MEMORY_RECORD) { + init_RAM_element(ram_id, static_cast(i), zero_idx); + } + } + +#ifdef NO_TBB + std::sort(ram_array.records.begin(), ram_array.records.end()); +#else + std::sort(std::execution::par_unseq, ram_array.records.begin(), ram_array.records.end()); +#endif + + // Iterate over all but final RAM record. + for (size_t i = 0; i < ram_array.records.size(); ++i) { + const RamRecord& record = ram_array.records[i]; + + const auto index = record.index; + const auto value = get_variable(record.value_witness); + const auto index_witness = add_variable(fr((uint64_t)index)); + const auto timestamp_witess = add_variable(record.timestamp); + const auto value_witness = add_variable(value); + RamRecord sorted_record{ + .index_witness = index_witness, + .timestamp_witness = timestamp_witess, + .value_witness = value_witness, + .index = index, + .timestamp = record.timestamp, + .access_type = record.access_type, + .record_witness = 0, + .gate_index = 0, + }; + + // We don't apply the RAM consistency check gate to the final record, + // as this gate expects a RAM record to be present at the next gate + if (i < ram_array.records.size() - 1) { + create_sorted_RAM_gate(sorted_record); + } else { + // For the final record in the sorted list, we do not apply the full consistency check gate. + // Only need to check the index value = RAM array size - 1. + create_final_sorted_RAM_gate(sorted_record, ram_array.state.size()); + } + + // Assign record/sorted records to tags that we will perform set equivalence checks on + assign_tag(record.record_witness, access_tag); + assign_tag(sorted_record.record_witness, sorted_list_tag); + + // For ROM/RAM gates, the 'record' wire value (wire column 4) is a linear combination of the first 3 wire + // values. However...the record value uses the random challenge 'eta', generated after the first 3 wires are + // committed to. i.e. we can't compute the record witness here because we don't know what `eta` is! Take the + // gate indices of the two rom gates (original read gate + sorted gate) and store in `memory_records`. Once we + // generate the `eta` challenge, we'll use `memory_records` to figure out which gates need a record wire value + // to be computed. + + switch (record.access_type) { + case RamRecord::AccessType::READ: { + memory_read_records.push_back( + static_cast(sorted_record.gate_index + gate_offset_from_public_inputs)); + memory_read_records.push_back(static_cast(record.gate_index + gate_offset_from_public_inputs)); + break; + } + case RamRecord::AccessType::WRITE: { + memory_write_records.push_back( + static_cast(sorted_record.gate_index + gate_offset_from_public_inputs)); + memory_write_records.push_back(static_cast(record.gate_index + gate_offset_from_public_inputs)); + break; + } + default: { + ASSERT(false); // shouldn't get here! + } + } + } + + // Step 2: Create gates that validate correctness of RAM timestamps + + std::vector timestamp_deltas; + for (size_t i = 0; i < ram_array.records.size() - 1; ++i) { + const auto& current = ram_array.records[i]; + const auto& next = ram_array.records[i + 1]; + + const bool share_index = current.index == next.index; + + fr timestamp_delta = 0; + if (share_index) { + ASSERT(next.timestamp > current.timestamp); + timestamp_delta = fr(next.timestamp - current.timestamp); + } + + uint32_t timestamp_delta_witness = add_variable(timestamp_delta); + + apply_aux_selectors(AUX_SELECTORS::RAM_TIMESTAMP_CHECK); + w_l.emplace_back(current.index_witness); + w_r.emplace_back(current.timestamp_witness); + w_o.emplace_back(timestamp_delta_witness); + w_4.emplace_back(zero_idx); + ++num_gates; + + // store timestamp offsets for later. Need to apply range checks to them, but calling + // `create_new_range_constraint` can add gates. Would ruin the structure of our sorted timestamp list. + timestamp_deltas.push_back(timestamp_delta_witness); + } + + // add the index/timestamp values of the last sorted record in an empty add gate. + // (the previous gate will access the wires on this gate and requires them to be those of the last record) + const auto& last = ram_array.records[ram_array.records.size() - 1]; + create_big_add_gate({ + last.index_witness, + last.timestamp_witness, + zero_idx, + zero_idx, + 0, + 0, + 0, + 0, + 0, + }); + + // Step 3: validate difference in timestamps is monotonically increasing. i.e. is <= maximum timestamp + const size_t max_timestamp = ram_array.access_count - 1; + for (auto& w : timestamp_deltas) { + create_new_range_constraint(w, max_timestamp); + } +} + void UltraComposer::process_ROM_arrays(const size_t gate_offset_from_public_inputs) { for (size_t i = 0; i < rom_arrays.size(); ++i) { process_ROM_array(i, gate_offset_from_public_inputs); } } +void UltraComposer::process_RAM_arrays(const size_t gate_offset_from_public_inputs) +{ + for (size_t i = 0; i < ram_arrays.size(); ++i) { + process_RAM_array(i, gate_offset_from_public_inputs); + } +} } // namespace plonk diff --git a/cpp/src/aztec/plonk/composer/ultra_composer.hpp b/cpp/src/aztec/plonk/composer/ultra_composer.hpp index c5880d04db..967a351bc5 100644 --- a/cpp/src/aztec/plonk/composer/ultra_composer.hpp +++ b/cpp/src/aztec/plonk/composer/ultra_composer.hpp @@ -43,10 +43,12 @@ class UltraComposer : public ComposerBase { NON_NATIVE_FIELD_1, NON_NATIVE_FIELD_2, NON_NATIVE_FIELD_3, - CONSISTENT_SORTED_MEMORY_READ, - SORTED_MEMORY_READ, - MEMORY_TIMESTAMP_CORRECTNESS, - MEMORY_READ, + RAM_CONSISTENCY_CHECK, + ROM_CONSISTENCY_CHECK, + RAM_TIMESTAMP_CHECK, + ROM_READ, + RAM_READ, + RAM_WRITE, }; struct RangeList { @@ -57,32 +59,76 @@ class UltraComposer : public ComposerBase { }; /** - * @brief A memory record that can be ordered + * @brief A ROM memory record that can be ordered * * */ - struct MemoryRecord { - uint32_t index_witness; - uint32_t timestamp_witness; - uint32_t value_witness; - uint32_t index; - uint32_t timestamp; - uint32_t record_witness; - size_t gate_index; - bool operator<(const MemoryRecord& other) const + struct RomRecord { + uint32_t index_witness = 0; + uint32_t value_column1_witness = 0; + uint32_t value_column2_witness = 0; + uint32_t index = 0; + uint32_t record_witness = 0; + size_t gate_index = 0; + bool operator<(const RomRecord& other) const { return index < other.index; } + }; + + /** + * @brief A RAM memory record that can be ordered + * + * + */ + struct RamRecord { + enum AccessType { + READ, + WRITE, + }; + uint32_t index_witness = 0; + uint32_t timestamp_witness = 0; + uint32_t value_witness = 0; + uint32_t index = 0; + uint32_t timestamp = 0; + AccessType access_type = AccessType::READ; // read or write? + uint32_t record_witness = 0; + size_t gate_index = 0; + bool operator<(const RamRecord& other) const { bool index_test = (index) < (other.index); return index_test || (index == other.index && timestamp < other.timestamp); } }; + /** + * @brief Each ram array is an instance of memory transcript. It saves values and indexes for a particular memory + * array + * + * + */ + struct RamTranscript { + // Represents the current state of the array. Elements are variable indices. + // Every update requires a new entry in the `records` vector below. + std::vector state; + + // A vector of records, each of which contains: + // - Witnesses for [index, timestamp, value, record] + // (record is initialized during the proof creation, and points to 0 until then) + // - Index of the element in the `state` vector + // - READ/WRITE flag + // - Real timestamp value, initialized to the current `access_count` + std::vector records; + + // used for RAM records, to compute the timestamp when performing a read/write + // Incremented at every init/read/write operation. + size_t access_count = 0; + }; + /** * @brief Each rom array is an instance of memory transcript. It saves values and indexes for a particular memory * array * * */ - struct MemoryTranscript { + struct RomTranscript { // Contains the value of each index of the array std::vector> state; @@ -90,7 +136,7 @@ class UltraComposer : public ComposerBase { // + The constant witness with the index // + The value in the memory slot // + The actual index value - std::vector records; + std::vector records; }; enum UltraSelectors { QM, QC, Q1, Q2, Q3, Q4, QARITH, QFIXED, QSORT, QELLIPTIC, QAUX, QLOOKUPTYPE, NUM }; @@ -183,17 +229,22 @@ class UltraComposer : public ComposerBase { * 3) Number of Rom array-associated gates * 4) NUmber of range-list associated gates * - * @return size_t + * + * @param count return arument, number of existing gates + * @param rangecount return argument, extra gates due to range checks + * @param romcount return argument, extra gates due to rom reads + * @param ramcount return argument, extra gates due to ram read/writes */ - virtual size_t get_num_gates() const override + void get_num_gates_split_into_components(size_t& count, + size_t& rangecount, + size_t& romcount, + size_t& ramcount) const { - // if circuit finalised already added extra gates - if (circuit_finalised) { - return num_gates; - } - size_t count = num_gates; - size_t rangecount = 0; - size_t romcount = 0; + count = num_gates; + rangecount = 0; + romcount = 0; + ramcount = 0; + // each ROM gate adds +1 extra gate due to the rom reads being copied to a sorted list set for (size_t i = 0; i < rom_arrays.size(); ++i) { for (size_t j = 0; j < rom_arrays[i].state.size(); ++j) { if (rom_arrays[i].state[j][0] == UNINITIALIZED_MEMORY_RECORD) { @@ -205,6 +256,32 @@ class UltraComposer : public ComposerBase { } constexpr size_t gate_width = ultra_settings::program_width; + // each RAM gate adds +2 extra gates due to the ram reads being copied to a sorted list set, + // as well as an extra gate to validate timestamps + for (size_t i = 0; i < ram_arrays.size(); ++i) { + for (size_t j = 0; j < ram_arrays[i].state.size(); ++j) { + if (ram_arrays[i].state[j] == UNINITIALIZED_MEMORY_RECORD) { + ramcount += 2; + } + } + ramcount += (ram_arrays[i].records.size() * 2); + ramcount += 1; // we add an addition gate after procesing a ram array + + // there will be 'max_timestamp' number of range checks, need to calculate. + const auto max_timestamp = ram_arrays[i].access_count - 1; + + // TODO: if a range check of length `max_timestamp` already exists, this will be innacurate! + // TODO: fix this + size_t padding = (gate_width - (max_timestamp % gate_width)) % gate_width; + if (max_timestamp == gate_width) + padding += gate_width; + const size_t ram_range_check_list_size = max_timestamp + padding; + + size_t ram_range_check_gate_count = (ram_range_check_list_size / gate_width); + ram_range_check_gate_count += 1; // we need to add 1 extra addition gates for every distinct range list + + ramcount += ram_range_check_gate_count; + } for (const auto& list : range_lists) { auto list_size = list.second.variable_indices.size(); size_t padding = (gate_width - (list.second.variable_indices.size() % gate_width)) % gate_width; @@ -214,49 +291,60 @@ class UltraComposer : public ComposerBase { rangecount += (list_size / gate_width); rangecount += 1; // we need to add 1 extra addition gates for every distinct range list } - return count + romcount + rangecount; + } + + /** + * @brief Get the final number of gates in a circuit, which consists of the sum of: + * 1) Current number number of actual gates + * 2) Number of public inputs, as we'll need to add a gate for each of them + * 3) Number of Rom array-associated gates + * 4) NUmber of range-list associated gates + * + * @return size_t + */ + virtual size_t get_num_gates() const override + { + // if circuit finalised already added extra gates + if (circuit_finalised) { + return num_gates; + } + size_t count = 0; + size_t rangecount = 0; + size_t romcount = 0; + size_t ramcount = 0; + get_num_gates_split_into_components(count, rangecount, romcount, ramcount); + return count + romcount + ramcount + rangecount; } virtual void print_num_gates() const override { - size_t count = num_gates; + + size_t count = 0; size_t rangecount = 0; - size_t constant_rangecount = 0; size_t romcount = 0; + size_t ramcount = 0; + size_t constant_rangecount = 0; + size_t plookupcount = 0; - for (auto& table : lookup_tables) { + + get_num_gates_split_into_components(count, rangecount, romcount, ramcount); + + for (const auto& table : lookup_tables) { plookupcount += table.lookup_gates.size(); count -= table.lookup_gates.size(); } - for (size_t i = 0; i < rom_arrays.size(); ++i) { - for (size_t j = 0; j < rom_arrays[i].state.size(); ++j) { - if (rom_arrays[i].state[j][0] == UNINITIALIZED_MEMORY_RECORD) { - romcount += 2; - } - } - romcount += (rom_arrays[i].records.size()); - romcount += 1; // we add an addition gate after procesing a rom array - } - constexpr size_t gate_width = ultra_settings::program_width; for (const auto& list : range_lists) { - auto list_size = list.second.variable_indices.size(); - size_t padding = (gate_width - (list.second.variable_indices.size() % gate_width)) % gate_width; - if (list.second.variable_indices.size() == gate_width) - padding += gate_width; - list_size += padding; - rangecount += (list_size / gate_width); - rangecount += 1; // we need to add 1 extra addition gates for every distinct range list - // rough estimate - const size_t constant_cost = static_cast(list.second.target_range / 6); + const auto constant_cost = static_cast(list.second.target_range / 6); constant_rangecount += constant_cost; rangecount -= constant_cost; } - size_t total = count + romcount + rangecount + constant_rangecount + plookupcount; + size_t total = count + romcount + rangecount; std::cout << "gates = " << total << " (arith " << count << ", plookup " << plookupcount << ", rom " << romcount - << ", range " << rangecount << ", range table init cost = " << constant_rangecount - << "), pubinp = " << public_inputs.size() << std::endl; + << ", ram " << ramcount << romcount << ", range " << rangecount + << ", range table init cost = " << constant_rangecount << "), pubinp = " << public_inputs.size() + << std::endl; } void assert_equal_constant(const uint32_t a_idx, @@ -375,11 +463,22 @@ class UltraComposer : public ComposerBase { const std::array& value_witnesses); uint32_t read_ROM_array(const size_t rom_id, const uint32_t index_witness); std::array read_ROM_array_pair(const size_t rom_id, const uint32_t index_witness); - void create_memory_gate(MemoryRecord& record); - void create_sorted_memory_gate(MemoryRecord& record, const bool is_ram_transition_or_rom = false); + void create_ROM_gate(RomRecord& record); + void create_sorted_ROM_gate(RomRecord& record); void process_ROM_array(const size_t rom_id, const size_t gate_offset_from_public_inputs); void process_ROM_arrays(const size_t gate_offset_from_public_inputs); + void create_RAM_gate(RamRecord& record); + void create_sorted_RAM_gate(RamRecord& record); + void create_final_sorted_RAM_gate(RamRecord& record, const size_t ram_array_size); + + size_t create_RAM_array(const size_t array_size); + void init_RAM_element(const size_t ram_id, const size_t index_value, const uint32_t value_witness); + uint32_t read_RAM_array(const size_t ram_id, const uint32_t index_witness); + void write_RAM_array(const size_t ram_id, const uint32_t index_witness, const uint32_t value_witness); + void process_RAM_array(const size_t ram_id, const size_t gate_offset_from_public_inputs); + void process_RAM_arrays(const size_t gate_offset_from_public_inputs); + /** * Member Variables **/ @@ -400,9 +499,26 @@ class UltraComposer : public ComposerBase { std::vector lookup_multi_tables; std::map range_lists; // DOCTODO: explain this. - std::vector ram_arrays; // DOCTODO: explain this. - std::vector rom_arrays; // DOCTODO: explain this. - std::vector memory_records; // Used for ROM. + /** + * @brief Each entry in ram_arrays represents an independent RAM table. + * RamTranscript tracks the current table state, + * as well as the 'records' produced by each read and write operation. + * Used in `compute_proving_key` to generate consistency check gates required to validate the RAM read/write history + */ + std::vector ram_arrays; + + /** + * @brief Each entry in rom_arrays represents an independent ROM table. + * RomTranscript tracks the current table state, + * as well as the 'records' produced by each read operation. + * Used in `compute_proving_key` to generate consistency check gates required to validate the ROM read history + */ + std::vector rom_arrays; + + // Stores gate index of ROM and RAM reads (required by proving key) + std::vector memory_read_records; + // Stores gate index of RAM writes (required by proving key) + std::vector memory_write_records; std::vector recursive_proof_public_input_indices; bool contains_recursive_proof = false; diff --git a/cpp/src/aztec/plonk/composer/ultra_composer.test.cpp b/cpp/src/aztec/plonk/composer/ultra_composer.test.cpp index cce742d1de..9cb3eb6f80 100644 --- a/cpp/src/aztec/plonk/composer/ultra_composer.test.cpp +++ b/cpp/src/aztec/plonk/composer/ultra_composer.test.cpp @@ -581,6 +581,27 @@ TEST(ultra_composer, range_with_gates) bool result = verifier.verify_proof(proof); EXPECT_EQ(result, true); } + +TEST(ultra_composer, range_with_gates_where_range_is_not_a_power_of_two) +{ + UltraComposer composer = UltraComposer(); + auto idx = add_variables(composer, { 1, 2, 3, 4, 5, 6, 7, 8 }); + for (size_t i = 0; i < idx.size(); i++) { + composer.create_new_range_constraint(idx[i], 12); + } + + composer.create_add_gate({ idx[0], idx[1], composer.zero_idx, fr::one(), fr::one(), fr::zero(), -3 }); + composer.create_add_gate({ idx[2], idx[3], composer.zero_idx, fr::one(), fr::one(), fr::zero(), -7 }); + composer.create_add_gate({ idx[4], idx[5], composer.zero_idx, fr::one(), fr::one(), fr::zero(), -11 }); + composer.create_add_gate({ idx[6], idx[7], composer.zero_idx, fr::one(), fr::one(), fr::zero(), -15 }); + auto prover = composer.create_prover(); + auto verifier = composer.create_verifier(); + + proof proof = prover.construct_proof(); + bool result = verifier.verify_proof(proof); + EXPECT_EQ(result, true); +} + TEST(ultra_composer, sort_widget_complex) { { @@ -763,4 +784,75 @@ TEST(ultra_composer, rom) bool result = verifier.verify_proof(proof); EXPECT_EQ(result, true); } + +TEST(ultra_composer, ram) +{ + UltraComposer composer = UltraComposer(); + + uint32_t ram_values[8]{ + composer.add_variable(fr::random_element()), composer.add_variable(fr::random_element()), + composer.add_variable(fr::random_element()), composer.add_variable(fr::random_element()), + composer.add_variable(fr::random_element()), composer.add_variable(fr::random_element()), + composer.add_variable(fr::random_element()), composer.add_variable(fr::random_element()), + }; + + size_t ram_id = composer.create_RAM_array(8); + + for (size_t i = 0; i < 8; ++i) { + composer.init_RAM_element(ram_id, i, ram_values[i]); + } + + uint32_t a_idx = composer.read_RAM_array(ram_id, composer.add_variable(5)); + EXPECT_EQ(a_idx != ram_values[5], true); + + uint32_t b_idx = composer.read_RAM_array(ram_id, composer.add_variable(4)); + uint32_t c_idx = composer.read_RAM_array(ram_id, composer.add_variable(1)); + + composer.write_RAM_array(ram_id, composer.add_variable(4), composer.add_variable(500)); + uint32_t d_idx = composer.read_RAM_array(ram_id, composer.add_variable(4)); + + EXPECT_EQ(composer.get_variable(d_idx), 500); + + // ensure these vars get used in another arithmetic gate + const auto e_value = composer.get_variable(a_idx) + composer.get_variable(b_idx) + composer.get_variable(c_idx) + + composer.get_variable(d_idx); + uint32_t e_idx = composer.add_variable(e_value); + + composer.create_big_add_gate( + { + a_idx, + b_idx, + c_idx, + d_idx, + -1, + -1, + -1, + -1, + 0, + }, + true); + composer.create_big_add_gate( + { + composer.zero_idx, + composer.zero_idx, + composer.zero_idx, + e_idx, + 0, + 0, + 0, + 0, + 0, + }, + false); + + auto prover = composer.create_prover(); + std::cout << "prover num_gates = " << composer.num_gates << std::endl; + + auto verifier = composer.create_verifier(); + + proof proof = prover.construct_proof(); + + bool result = verifier.verify_proof(proof); + EXPECT_EQ(result, true); +} } // namespace plonk \ No newline at end of file diff --git a/cpp/src/aztec/plonk/proof_system/prover/prover.cpp b/cpp/src/aztec/plonk/proof_system/prover/prover.cpp index af956f643b..97b6235306 100644 --- a/cpp/src/aztec/plonk/proof_system/prover/prover.cpp +++ b/cpp/src/aztec/plonk/proof_system/prover/prover.cpp @@ -612,14 +612,30 @@ template void ProverBase::add_plookup_memory_recor // due to the dependence on the `eta` challenge. const fr eta = fr::serialize_from_buffer(transcript.get_challenge("eta").begin()); - const fr eta_sqr = eta.sqr(); + // We need the lagrange-base forms of the first 3 wires to compute the plookup memory record + // value. w4 = w3 * eta^3 + w2 * eta^2 + w1 * eta + read_write_flag; + // a RAM write. See plookup_auxiliary_widget.hpp for details) std::span w_1 = key->polynomial_cache.get("w_1_lagrange"); std::span w_2 = key->polynomial_cache.get("w_2_lagrange"); std::span w_3 = key->polynomial_cache.get("w_3_lagrange"); std::span w_4 = key->polynomial_cache.get("w_4_lagrange"); - for (const auto& gate_idx : key->memory_records) { - w_4[gate_idx] = w_1[gate_idx] + w_2[gate_idx] * eta + w_3[gate_idx] * eta_sqr; + for (const auto& gate_idx : key->memory_read_records) { + w_4[gate_idx] += w_3[gate_idx]; + w_4[gate_idx] *= eta; + w_4[gate_idx] += w_2[gate_idx]; + w_4[gate_idx] *= eta; + w_4[gate_idx] += w_1[gate_idx]; + w_4[gate_idx] *= eta; + } + for (const auto& gate_idx : key->memory_write_records) { + w_4[gate_idx] += w_3[gate_idx]; + w_4[gate_idx] *= eta; + w_4[gate_idx] += w_2[gate_idx]; + w_4[gate_idx] *= eta; + w_4[gate_idx] += w_1[gate_idx]; + w_4[gate_idx] *= eta; + w_4[gate_idx] += 1; } } diff --git a/cpp/src/aztec/plonk/proof_system/widgets/transition_widgets/plookup_auxiliary_widget.hpp b/cpp/src/aztec/plonk/proof_system/widgets/transition_widgets/plookup_auxiliary_widget.hpp index a3b806d68d..894ec072e1 100644 --- a/cpp/src/aztec/plonk/proof_system/widgets/transition_widgets/plookup_auxiliary_widget.hpp +++ b/cpp/src/aztec/plonk/proof_system/widgets/transition_widgets/plookup_auxiliary_widget.hpp @@ -6,21 +6,42 @@ namespace plonk { namespace widget { /** - * Plookup Auxiliary Widget + * @brief Plookup Auxiliary Widget * - * Evaluates polynomial identities associated with the following UltraPlonk custom gates: + * @details Evaluates polynomial identities associated with the following UltraPlonk custom gates: + * * RAM/ROM read-write consistency check + * * RAM timestamp difference consistency check + * * RAM/ROM index difference consistency check + * * Bigfield product evaluation (3 in total) + * * Bigfield limb accumulation (2 in total) * - * RAM/ROM read-write consistency check - * RAM timestamp difference consistency check - * RAM/ROM index difference consistency check - * Bigfield product evaluation (3 in total) - * Bigfield limb accumulation (2 in total) + * Multiple selectors are used to 'switch' aux gates on/off according to the following pattern: * - **/ + * | gate type | q_aux | q_1 | q_2 | q_3 | q_4 | q_m | q_c | q_arith | + * | ---------------------------- | ----- | --- | --- | --- | --- | --- | --- | ------ | + * | Bigfield Limb Accumulation 1 | 1 | 0 | 0 | 1 | 1 | 0 | --- | 0 | + * | Bigfield Limb Accumulation 2 | 1 | 0 | 0 | 1 | 0 | 1 | --- | 0 | + * | Bigfield Product 1 | 1 | 0 | 1 | 1 | 0 | 0 | --- | 0 | + * | Bigfield Product 2 | 1 | 0 | 1 | 0 | 1 | 0 | --- | 0 | + * | Bigfield Product 3 | 1 | 0 | 1 | 0 | 0 | 1 | --- | 0 | + * | RAM/ROM access gate | 1 | 1 | 0 | 0 | 0 | 1 | --- | 0 | + * | RAM timestamp check | 1 | 1 | 0 | 0 | 1 | 0 | --- | 0 | + * | ROM consistency check | 1 | 1 | 1 | 0 | 0 | 0 | --- | 0 | + * | RAM consistency check | 1 | 0 | 0 | 0 | 0 | 0 | 0 | 1 | + * + * N.B. The RAM consistency check identity is degree 3. To keep the overall quotient degree at <=5, only 2 selectors can + * be used to select it. + * + * N.B.2 The q_c selector is used to store circuit-specific values in the RAM/ROM access gate + * + * @tparam Field + * @tparam Getters + * @tparam PolyContainer + */ template class PlookupAuxiliaryKernel { public: static constexpr bool use_quotient_mid = false; - static constexpr size_t num_independent_relations = 3; + static constexpr size_t num_independent_relations = 4; // We state the challenges required for linear/nonlinear terms computation static constexpr uint8_t quotient_required_challenges = CHALLENGE_BIT_ALPHA; // We state the challenges required for updating kate opening scalars @@ -34,10 +55,10 @@ template class PlookupAuxil inline static std::set const& get_required_polynomial_ids() { static const std::set required_polynomial_ids = { - bonk::PolynomialIndex::Q_1, bonk::PolynomialIndex::Q_2, bonk::PolynomialIndex::Q_3, - bonk::PolynomialIndex::Q_4, bonk::PolynomialIndex::Q_M, bonk::PolynomialIndex::Q_AUX, - bonk::PolynomialIndex::W_1, bonk::PolynomialIndex::W_2, bonk::PolynomialIndex::W_3, - bonk::PolynomialIndex::W_4 + bonk::PolynomialIndex::Q_1, bonk::PolynomialIndex::Q_2, bonk::PolynomialIndex::Q_3, + bonk::PolynomialIndex::Q_4, bonk::PolynomialIndex::Q_M, bonk::PolynomialIndex::Q_C, + bonk::PolynomialIndex::Q_ARITHMETIC, bonk::PolynomialIndex::Q_AUX, bonk::PolynomialIndex::W_1, + bonk::PolynomialIndex::W_2, bonk::PolynomialIndex::W_3, bonk::PolynomialIndex::W_4 }; return required_polynomial_ids; } @@ -89,6 +110,11 @@ template class PlookupAuxil Getters::template get_value(polynomials, i); const Field& q_m = Getters::template get_value(polynomials, i); + const Field& q_c = + Getters::template get_value(polynomials, i); + const Field& q_arith = + Getters::template get_value(polynomials, + i); /** * Non native field arithmetic gate 2 @@ -147,84 +173,154 @@ template class PlookupAuxil Field limb_accumulator_identity = limb_accumulator_1 + limb_accumulator_2; limb_accumulator_identity *= q_3; - limb_subproduct = w_1_omega - w_1; - /** * MEMORY * - * A memory record contains a tuple of the following fields: + * A RAM memory record contains a tuple of the following fields: * * i: `index` of memory cell being accessed - * * t: `tiemstamp` of memory cell being accessed (used for RAM, set to 0 for ROM) + * * t: `timestamp` of memory cell being accessed (used for RAM, set to 0 for ROM) * * v: `value` of memory cell being accessed - * * r: `record` of memory cell. record = index + timestamp * eta + value * eta^2 + * * a: `access` type of record. read: 0 = read, 1 = write + * * r: `record` of memory cell. record = access + index * eta + timestamp * eta^2 + value * eta^3 * - * A record gate is structured such that each of the above 4 fields maps to wires 1, 2, 3, 4 - **/ - - /** - * RAM SORTED LIST CHECK + * A ROM memory record contains a tuple of the following fields: + * * i: `index` of memory cell being accessed + * * v: `value1` of memory cell being accessed (ROM tables can store up to 2 values per index) + * * v2:`value2` of memory cell being accessed (ROM tables can store up to 2 values per index) + * * r: `record` of memory cell. record = index * eta + value2 * eta^2 + value1 * eta^3 + * + * When performing a read/write access, the values of i, t, v, v2, a, r are stored in the following wires + + * selectors, depending on whether the gate is a RAM read/write or a ROM read * - * Validate the following at gate `j`: + * | gate type | i | v2/t | v | a | r | + * | --------- | -- | ----- | -- | -- | -- | + * | ROM | w1 | w2 | w3 | -- | w4 | + * | RAM | w1 | w2 | w3 | qc | w4 | * - * 1. (i_{j+1} - i_j)^2 - (i_{j+1} - i_j) = 0 (index increases by 0 or 1) - * 2. (r = i + t * eta + v * eta^2) + * (for accesses where `index` is a circuit constant, it is assumed the circuit will apply a copy constraint on + * `w2` to fix its value) * - * Used for sorted RAM records iff gate `j` is a RAM read and gate `j + 1` is a RAM write **/ - Field memory_sorted_list_check = limb_subproduct.sqr() - limb_subproduct; /** - * ROM CONSISTENT SORTED LIST CHECK + * Memory Record Check * - * Validate the following at gate `j`: + * A ROM/ROM access gate can be evaluated with the identity: * - * 1. (i_{j+1} - i_j)^2 - (i_{j+1} - i_j) = 0 (index increases by 0 or 1) - * 2. (r = i + t * eta + v * eta^2) - * 3. (1 - (i_{j+1} - i_j)) * (r_{j+1} - r_j) (if index does not change, neither does - *value) + * qc + w1 \eta + w2 \eta^2 + w3 \eta^3 - w4 = 0 * - * Used for sorted ROM records - **/ - // TODO: MAKE this work for ram records iff gate `j` is a RAM write and gate `j + 1` is a - // *RAM read - // for RAM we want to compare across the value field (column 3) - // but for ROM, if we compare across the record field (column 4) we can lookup 2 ROM values per gate - Field memory_consistent_sorted_list_check = Field(1) - limb_subproduct; // 1 - (w_1_omega - w_1) - // Field memory_consistent_sorted_list_RAM_check = memory_consistent_sorted_list_check * (w_3_omega - w_3); - memory_consistent_sorted_list_check *= (w_4_omega - w_4); // (1 - (w_1_omega - w_1)) * (w_4_omega - w_4) + * For ROM gates, qc = 0 + */ + Field memory_record_check = w_3; + memory_record_check *= eta; + memory_record_check += w_2; + memory_record_check *= eta; + memory_record_check += w_1; + memory_record_check *= eta; + memory_record_check += q_c; + Field partial_record_check = memory_record_check; // used in RAM consistency check + memory_record_check = memory_record_check - w_4; /** - * RAM TIMESTAMP CHECK + * ROM Consistency Check * - * Validate the following at gate `j`: + * For every ROM read, a set equivalence check is applied between the record witnesses, and a second set of + * records that are sorted. * - * 1. \delta = (1 - ((i_{j+1} - i_j)^2 - (i_{j+1} - i_j))(t_{j+1} - t_j) + * We apply the following checks for the sorted records: * - * i.e. If index does not change, `\delta` = timestamp difference, eles `\delta` = 0 + * 1. w1, w2, w3 correctly map to 'index', 'v1, 'v2' for a given record value at w4 + * 2. index values for adjacent records are monotonically increasing + * 3. if, at gate i, index_i == index_{i + 1}, then value1_i == value1_{i + 1} and value2_i == value2_{i + 1} * - * Used for RAM records to validate consistency between read/writes into the same cell. - * Timestamp check is performed in a separate gate to the checks against the sorted list (with copy constraints - *to map between the two gates) - **/ - Field memory_timestamp_check = memory_consistent_sorted_list_check - w_2; + */ + Field index_delta = w_1_omega - w_1; + Field record_delta = w_4_omega - w_4; - Field memory_record_check = w_3; - memory_record_check *= eta; - memory_record_check += w_2; - memory_record_check *= eta; - memory_record_check += w_1; - memory_record_check -= w_4; + Field index_is_monotonically_increasing = index_delta.sqr() - index_delta; - memory_sorted_list_check *= alpha; - memory_sorted_list_check += memory_record_check; + Field adjacent_values_match_if_adjacent_indices_match = (Field(1) - index_delta) * record_delta; - memory_consistent_sorted_list_check += (memory_sorted_list_check * alpha); + Field ROM_consistency_check_identity = adjacent_values_match_if_adjacent_indices_match; + ROM_consistency_check_identity *= alpha; + ROM_consistency_check_identity += index_is_monotonically_increasing; + ROM_consistency_check_identity *= alpha; + ROM_consistency_check_identity += memory_record_check; - Field memory_identity = memory_consistent_sorted_list_check * q_2; - memory_identity += memory_sorted_list_check * q_3; - memory_identity += memory_timestamp_check * q_4; + /** + * RAM Consistency Check + * + * The 'access' type of the record is extracted with the expression `w_4 - partial_record_check` + * (i.e. for an honest Prover `w1 * eta + w2 * eta^2 + w3 * eta^3 - w4 = access`. + * This is validated by requiring `access` to be boolean + * + * For two adjacent entries in the sorted list if _both_ + * A) index values match + * B) adjacent access value is 0 (i.e. next gate is a READ) + * then + * C) both values must match. + * The gate boolean check is + * (A && B) => C === !(A && B) || C === !A || !B || C + * + * N.B. it is the responsibility of the circuit writer to ensure that every RAM cell is initialized + * with a WRITE operation. + */ + Field access_type = (w_4 - partial_record_check); // will be 0 or 1 for honest Prover + Field access_check = access_type.sqr() - access_type; // check value is 0 or 1 + + // TODO: oof nasty compute here. If we sorted in reverse order we could re-use `partial_record_check` + Field next_gate_access_type = w_3_omega; + next_gate_access_type *= eta; + next_gate_access_type += w_2_omega; + next_gate_access_type *= eta; + next_gate_access_type += w_1_omega; + next_gate_access_type *= eta; + next_gate_access_type = w_4_omega - next_gate_access_type; + + Field value_delta = w_3_omega - w_3; + Field adjacent_values_match_if_adjacent_indices_match_and_next_access_is_a_read_operation = + (Field(1) - index_delta) * value_delta * (Field(1) - next_gate_access_type); + + // We can't apply the RAM consistency check identity on the final entry in the sorted list (the wires in the + // next gate would make the identity fail). + // We need to validate that its 'access type' bool is correct. Can't do + // with an arithmetic gate because of the `eta` factors. We need to check that the *next* gate's access type is + // correct, to cover this edge case + Field next_gate_access_type_is_boolean = next_gate_access_type.sqr() - next_gate_access_type; + + // Putting it all together... + Field RAM_consistency_check_identity = + adjacent_values_match_if_adjacent_indices_match_and_next_access_is_a_read_operation; + RAM_consistency_check_identity *= alpha; + RAM_consistency_check_identity += index_is_monotonically_increasing; + RAM_consistency_check_identity *= alpha; + RAM_consistency_check_identity += next_gate_access_type_is_boolean; + RAM_consistency_check_identity *= alpha; + RAM_consistency_check_identity += access_check; + + /** + * RAM Timestamp Consistency Check + * + * | w1 | w2 | w3 | w4 | + * | index | timestamp | timestamp_check | -- | + * + * Let delta_index = index_{i + 1} - index_{i} + * + * Iff delta_index == 0, timestamp_check = timestamp_{i + 1} - timestamp_i + * Else timestamp_check = 0 + */ + Field timestamp_delta = w_2_omega - w_2; + Field RAM_timestamp_check_identity = (Field(1) - index_delta) * timestamp_delta - w_3; + + /** + * The complete RAM/ROM memory identity + * + */ + Field memory_identity = ROM_consistency_check_identity * q_2; + memory_identity += RAM_timestamp_check_identity * q_4; memory_identity += memory_record_check * q_m; memory_identity *= q_1; + memory_identity += (RAM_consistency_check_identity * q_arith); Field auxiliary_identity = memory_identity + non_native_field_identity + limb_accumulator_identity; auxiliary_identity *= q_aux; diff --git a/cpp/src/aztec/proof_system/proving_key/proving_key.cpp b/cpp/src/aztec/proof_system/proving_key/proving_key.cpp index c3bd3953e9..70fdf7373e 100644 --- a/cpp/src/aztec/proof_system/proving_key/proving_key.cpp +++ b/cpp/src/aztec/proof_system/proving_key/proving_key.cpp @@ -54,7 +54,8 @@ proving_key::proving_key(proving_key_data&& data, std::shared_ptr min_thread_block ? circuit_size : 4 * circuit_size) diff --git a/cpp/src/aztec/proof_system/proving_key/proving_key.hpp b/cpp/src/aztec/proof_system/proving_key/proving_key.hpp index a50e2dbe2b..7e4ab875d4 100644 --- a/cpp/src/aztec/proof_system/proving_key/proving_key.hpp +++ b/cpp/src/aztec/proof_system/proving_key/proving_key.hpp @@ -19,7 +19,8 @@ struct proving_key_data { uint32_t num_public_inputs; bool contains_recursive_proof; std::vector recursive_proof_public_input_indices; - std::vector memory_records; + std::vector memory_read_records; + std::vector memory_write_records; PolynomialCache polynomial_cache; }; @@ -48,7 +49,9 @@ struct proving_key { size_t num_public_inputs; bool contains_recursive_proof = false; std::vector recursive_proof_public_input_indices; - std::vector memory_records; // Used by UltraComposer only; for ROM. + std::vector memory_read_records; // Used by UltraComposer only; for ROM, RAM reads. + std::vector memory_write_records; // Used by UltraComposer only, for RAM writes. + // Note: low-memory prover functionality can be achieved by uncommenting the lines below // which allow the polynomial cache to write polynomials to file as necessary. Similar // lines must also be uncommented in constructor. diff --git a/cpp/src/aztec/proof_system/proving_key/serialize.hpp b/cpp/src/aztec/proof_system/proving_key/serialize.hpp index 25edb21ba9..09118cf3e9 100644 --- a/cpp/src/aztec/proof_system/proving_key/serialize.hpp +++ b/cpp/src/aztec/proof_system/proving_key/serialize.hpp @@ -31,7 +31,8 @@ template inline void read(B& any, proving_key_data& key) read(any, key.contains_recursive_proof); read(any, key.recursive_proof_public_input_indices); - read(any, key.memory_records); + read(any, key.memory_read_records); + read(any, key.memory_write_records); } // Write the pre-computed polynomials @@ -56,7 +57,8 @@ template inline void write(B& buf, proving_key const& key) write(buf, key.contains_recursive_proof); write(buf, key.recursive_proof_public_input_indices); - write(buf, key.memory_records); + write(buf, key.memory_read_records); + write(buf, key.memory_write_records); } template inline void read_mmap(B& is, std::string const& path, proving_key_data& key) @@ -78,7 +80,8 @@ template inline void read_mmap(B& is, std::string const& path, prov } read(is, key.contains_recursive_proof); read(is, key.recursive_proof_public_input_indices); - read(is, key.memory_records); + read(is, key.memory_read_records); + read(is, key.memory_write_records); } template inline void write_mmap(B& os, std::string const& path, proving_key const& key) { @@ -108,7 +111,8 @@ template inline void write_mmap(B& os, std::string const& path, pro } write(os, key.contains_recursive_proof); write(os, key.recursive_proof_public_input_indices); - write(os, key.memory_records); + write(os, key.memory_read_records); + write(os, key.memory_write_records); } } // namespace bonk