- Generated by
1.9.8
|
Barretenberg
The ZK-SNARK library at the core of Aztec
|
RAM/ROM memory relation. More...
#include <memory_relation.hpp>
Public Types | |
| using | FF = FF_ |
Static Public Member Functions | |
| template<typename AllEntities > | |
| static bool | skip (const AllEntities &in) |
| Returns true if the contribution from all subrelations for the provided inputs is identically zero. | |
| template<typename ContainerOverSubrelations , typename AllEntities , typename Parameters > | |
| static void | accumulate (ContainerOverSubrelations &accumulators, const AllEntities &in, const Parameters ¶ms, const FF &scaling_factor) |
Static Public Attributes | |
| static constexpr std::array< size_t, 8 > | SUBRELATION_PARTIAL_LENGTHS |
| static constexpr std::array< bool, 8 > | SUBRELATION_LINEARLY_INDEPENDENT |
RAM/ROM memory relation.
Adds contributions for identities associated with RAM/ROM memory operations custom gates:
Multiple selectors are used to 'switch' memory gates on/off according to the following pattern:
| gate type | q_mem | q_1 | q_2 | q_3 | q_4 | q_m | q_c |
|---|---|---|---|---|---|---|---|
| RAM/ROM access gate | 1 | 1 | 0 | 0 | 0 | 1 | access type (read: 0, write: 1) |
| 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 | 1 | 0 | 0 | 0 |
| ROM LogUp table entry | 1 | 0 | 1 | 0 | 0 | 0 | 0 |
| ROM LogUp read access | 1 | 0 | 0 | 0 | 1 | 0 | 0 |
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
Single-value ROM tables use a LogUp scheme (subrelations 6 and 7); pair-value ROM tables use the sorted-trace permutation argument (ROM_READ / ROM_CONSISTENCY_CHECK gates and subrelations 1 and 2). The two LogUp gate types share the wire layout (w_l = index, w_r = value, w_o = multiplicity (table rows) or zero (read rows), w_4 = inverse helper) and have non-overlapping bitpatterns relative to all other memory gates above (table entry: q_2=1 with q_1=0; read access: q_4=1 with q_1=0).
Definition at line 43 of file memory_relation.hpp.
| using bb::MemoryRelationImpl< FF_ >::FF = FF_ |
Definition at line 45 of file memory_relation.hpp.
|
inlinestatic |
| evals | transformed to evals + C(in(X)...)*scaling_factor |
| in | an std::array containing the totally extended univariate edges. |
| parameters | contains beta, gamma, and public_input_delta, .... |
| scaling_factor | optional term to scale the evaluation before adding to evals. |
MEMORY
A RAM memory record contains a tuple of the following fields:
index of memory cell being accessedtimestamp of memory cell being accessed (used for RAM, set to 0 for ROM)value of memory cell being accessedaccess type of record. read: 0 = read, 1 = writerecord of memory cell. record = access + index * eta + timestamp * η₂ + value * η₃A ROM memory record contains a tuple of the following fields:
index of memory cell being accessedvalue1 of memory cell being accessed (ROM tables can store up to 2 values per index)value2 of memory cell being accessed (ROM tables can store up to 2 values per index)record of memory cell. record = index * eta + value1 * η₂ + value2 * η₃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
| gate type | i | v/t | v2 | a | r |
|---|---|---|---|---|---|
| ROM | w1 | w2 | w3 | – | w4 |
| RAM | w1 | w2 | w3 | qc | w4 |
(for accesses where index is a circuit constant, it is assumed the circuit will apply a copy constraint on w2 to fix its value)
Memory Record Check Degree: 1
A ROM/RAM access gate can be evaluated with the memory_record_check identity:
qc + w1 \eta + w2 η₂ + w3 η₃ - w4 = 0
For ROM gates, qc = 0 Here, informally, w4 is the "record" (a.k.a. fingerprint) of the access gate.
ROM Consistency Check Degree: 5
For every ROM read, we require a multiset check applied between the record witnesses and a second set of records that are sorted. (See the Plookup paper.) In fact, due to our implementation, this is automatic; we implicitly have copy-constraints realizing the multiset equality. In other words, the multiset check will be instantiated by a permutation check.
We apply the following checks for the sorted records:
(1) is witnessed jointly with corresponding other constraints in std::get<0>(accumulators)
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 * η + w2 * η₂ + w3 * η₃ - 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.
We apply the following checks for the sorted records:
RAM Timestamp Consistency Check
The gates constructed to witness the consistency of the jumps in the timestamp have the following form. They are constructed to be sorted, first with respect to index, then with respect to timestamp. (This is the same structure as the sorted RAM gates.) This is enforced by copy constraints (the witness indices of the gates are the same as those of the sorted RAM gates, so we do not need to explicitly check the lexicographic ordering again.)
| 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.
The complete RAM/ROM memory identity Degree: 5
ROM LogUp Sub-Relations (single-value tables)
Wire layout on ROM-LogUp rows: (w_l, w_r, w_o, w_4) = (index, value, multiplicity, inverse). Two selector bitpatterns identify these rows within the q_memory-gated region: q_logup_table = q_2 * (1 - q_1) (table entry: w_o = m_i, the read count) q_logup_read = q_4 * (1 - q_1) (read access: w_o = 0) The (1 - q_1) factor distinguishes these bitpatterns from ROM_CONSISTENCY_CHECK (q_1 = q_2 = 1) and RAM_TIMESTAMP_CHECK (q_1 = q_4 = 1) respectively.
Fingerprint (deg 1): denom = rom_logup_gamma + w_l + eta * w_r + eta_two * q_c where w_l = index, w_r = value, and q_c = ROM array id. The (index, value, array id) coordinates are batched with powers of eta (eta^0, eta^1, eta^2), so for a fixed eta distinct triples yield distinct batched encodings t = index + eta * value + eta_two * array_id with overwhelming probability (the difference of two encodings is a nonzero degre-<=2 polynomial in eta). The additive offset rom_logup_gamma is an independent challenge, not a power of eta: this is what makes the LogUp partial-fraction soundness argument valid. With denom = gamma + t and gamma independent of the t's, the reciprocals 1/(gamma + t) have simple poles at distinct points -t, so the summed identity below being zero forces every net multiplicity to vanish. The array id makes the match array-local: the sum below runs over the whole trace, and q_c is what ties each read to a table entry of the same array.
The independent offset rom_logup_gamma keeps every denominator nonzero (the all-zero row index = value = array id = 0 maps to rom_logup_gamma != 0). w_4 holds the inverse and is filled by the prover during oink, once eta and rom_logup_gamma are known but before w_4 is committed.
Subrelation 6 (per-row vanishing, deg 5): q_memory * (q_logup_table + q_logup_read) * (w_4 * denom - 1) = 0 Forces w_4 = 1 / denom on any row whose bitpattern fires.
Subrelation 7 (linearly dependent — summed across the trace, deg 5): sum_rows [ q_memory * (q_logup_read - q_logup_table * w_o) * w_4 ] = 0 This is the standard LogUp identity: read rows contribute +1/denom, table rows contribute -m_i/denom. Soundness follows from Schwartz-Zippel over the random challenges (eta for the batched encoding, rom_logup_gamma for the additive offset) plus the partial-fraction-decomposition argument (see the soundness discussion in logderiv_lookup_relation.hpp).
Locality: both terms in subrelation 7 are gated by precomputed selector combinations (q_logup_read, q_logup_table), so rows outside the ROM-LogUp bitpatterns contribute 0 regardless of w_o / w_4. No separate locality subrelation of the form (1 - indicator) * count = 0 (as used by the databus lookup relation, whose table values live in dedicated witness columns with no gate selector) is needed here: table entries are gates, and their selector is the indicator.
Definition at line 79 of file memory_relation.hpp.
|
inlinestatic |
Returns true if the contribution from all subrelations for the provided inputs is identically zero.
Definition at line 67 of file memory_relation.hpp.
|
staticconstexpr |
Definition at line 60 of file memory_relation.hpp.
|
staticconstexpr |
Definition at line 47 of file memory_relation.hpp.
1.9.8