Skip to content

Commit c527917

Browse files
authored
chore(avm)!: Apply standard multi-row recipe everywhere (#22279)
Linear issue: [AVM-244](https://linear.app/aztec-labs/issue/AVM-244/review-multi-rows-computation-instances-prevent-truncation)
1 parent b68c855 commit c527917

25 files changed

Lines changed: 636 additions & 621 deletions

barretenberg/cpp/pil/vm2/bitwise.pil

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -87,8 +87,6 @@ namespace bitwise;
8787
////////////////////////////////////////////////
8888
// Multi-row Computation Selectors (standard recipe)
8989
////////////////////////////////////////////////
90-
// Follows the recipe documented in:
91-
// https://github.com/AztecProtocol/aztec-packages/blob/next/barretenberg/cpp/pil/vm2/docs/recipes.md#contiguous-multi-rows-computation-trace
9290

9391
// Selector for active Bitwise block rows.
9492
// In the standard recipe, sel=1 for ALL rows in a block, including error rows.
@@ -99,12 +97,14 @@ sel * (1 - sel) = 0;
9997
#[skippable_if]
10098
sel = 0;
10199

100+
// Follows the recipe documented in:
101+
// https://github.com/AztecProtocol/aztec-packages/blob/next/barretenberg/cpp/pil/vm2/docs/recipes.md#contiguous-multi-rows-computation-trace
102+
102103
// NOTE on start selector:
103104
// start=1 on non-first rows within a block. This is safe because:
104105
// (1) The execution dispatch is a lookup INTO bitwise using bitwise.start as the destination
105106
// selector. Extra start=1 rows are just unclaimed destinations -- harmless.
106-
// (2) Keccak/sha256 use separate selectors (start_keccak/start_sha256) protected by
107-
// #[BITW_START_ONLY_WHEN_SEL].
107+
// (2) Keccak/sha256 use separate selectors (start_keccak/start_sha256) which enforce that start=1.
108108
// (3) Setting start=1 on a middle row triggers #[INTEGRAL_TAG_LENGTH] lookup, which would fail
109109
// because ctr at that row would not match the tag's byte length.
110110
// The start of the computation, used as a selector by a caller.

barretenberg/cpp/pil/vm2/data_copy.pil

Lines changed: 41 additions & 50 deletions
Original file line numberDiff line numberDiff line change
@@ -183,48 +183,39 @@ namespace data_copy;
183183
///////////////////////////////
184184
// Trace Shape
185185
///////////////////////////////
186-
// Trace is contiguous.
187-
#[TRACE_CONTINUITY]
188-
(1 - precomputed.first_row) * (1 - sel) * sel' = 0;
186+
// Multi-row computation selectors.
187+
// See recipe: https://github.com/AztecProtocol/aztec-packages/blob/next/barretenberg/cpp/pil/vm2/docs/recipes.md#contiguous-multi-rows-computation-trace
189188

190-
pol commit sel_start; // @boolean
191-
sel_start * (1 - sel_start) = 0;
189+
pol commit start; // @boolean
190+
start * (1 - start) = 0;
192191
// End controls most of the row propagation, so if we error we also set end to turn off row propagation
193-
pol commit sel_end; // @boolean
194-
sel_end * (1 - sel_end) = 0;
192+
pol commit end; // @boolean
193+
end * (1 - end) = 0;
195194

196-
// sel_end = 1 OR sel_start ==> sel = 1
197-
(sel_start + sel_end) * (1 - sel) = 0;
195+
pol LATCH_CONDITION = end + precomputed.first_row;
198196

199-
// This prevents a computation to be stopped prematurely, i.e., truncating last rows before
200-
// we reach a row where sel_end == 1.
201-
#[COMPUTATION_FINISH_AT_END]
202-
sel * (1 - sel') * (1 - sel_end) = 0;
197+
#[SEL_ON_START_OR_END]
198+
(start + end) * (1 - sel) = 0;
203199

204-
// Latch condition is boolean because sel_end cannot be activated at first row
205-
// because sel is shifted and sel_end implies sel == 1.
206-
pol LATCH_CONDITION = sel_end + precomputed.first_row;
200+
#[TRACE_CONTINUITY]
201+
(1 - LATCH_CONDITION) * (sel - sel') = 0;
207202

208-
// By enforcing the start of a new computation after a latch, we ensure that no superfluous rows are added.
209-
// In combination with the permutations from the execution trace, it follows that each active row is
210-
// part of a genuine computation. We particularly need to be careful that no malicious memory write is
211-
// performed.
212203
#[START_AFTER_LATCH]
213-
sel' * (sel_start' - LATCH_CONDITION) = 0;
204+
sel' * (start' - LATCH_CONDITION) = 0;
214205

215206
////////////////////////////////////////////////
216207
// Dispatch Permutation Selectors
217208
////////////////////////////////////////////////
218209
// These permutations are defined in execution.pil. See #[DISPATCH_TO_CD_COPY] and #[DISPATCH_TO_RD_COPY].
219210

220211
pol commit sel_cd_copy_start; // @boolean (by definition)
221-
sel_cd_copy_start = sel_start * sel_cd_copy;
212+
sel_cd_copy_start = start * sel_cd_copy;
222213

223214
pol commit sel_rd_copy_start; // @boolean (by definition)
224-
sel_rd_copy_start = sel_start * (1 - sel_cd_copy);
215+
sel_rd_copy_start = start * (1 - sel_cd_copy);
225216

226217
// It follows from the above equations that sel_cd_copy_start and sel_rd_copy_start are mutually exclusive
227-
// and that sel_cd_copy_start + sel_rd_copy_start = sel_start.
218+
// and that sel_cd_copy_start + sel_rd_copy_start = start.
228219
// sel_cd_copy also the correct value on the start row:
229220
// sel_cd_copy_start == 1 ==> sel_cd_copy == 1
230221
// sel_rd_copy_start == 1 ==> sel_cd_copy == 0
@@ -253,14 +244,14 @@ namespace data_copy;
253244
// 2) (offset + copy_size) <= src_data_size
254245
// if (1) then read_index_upper_bound = src_data_size, otherwise read_index_upper_bound = (offset + copy_size)
255246
pol commit offset_plus_size;
256-
offset_plus_size = sel_start * (offset + copy_size);
247+
offset_plus_size = start * (offset + copy_size);
257248
pol commit offset_plus_size_is_gt; // @boolean (by lookup into gt)
258249

259250
// Preconditions to `gt` gadget require both inputs to be bounded by 2^128.
260251
// `offset_plus_size` = offset + copy_size (both U32, so < 2^33). `src_data_size` is U32.
261252
// (All involved values are U32 by PRECONDITIONS at the top of this file.)
262253
#[OFFSET_PLUS_SIZE_IS_GT_DATA_SIZE]
263-
sel_start { offset_plus_size, src_data_size, offset_plus_size_is_gt }
254+
start { offset_plus_size, src_data_size, offset_plus_size_is_gt }
264255
in
265256
gt.sel_others { gt.input_a, gt.input_b, gt.res };
266257

@@ -277,19 +268,19 @@ namespace data_copy;
277268

278269
// AVM_MEMORY_SIZE == AVM_HIGHEST_MEM_ADDRESS + 1.
279270
pol commit mem_size; // Lookup constant support: We need this temporarily while we do not allow for aliases in the lookup tuple
280-
sel_start * (mem_size - constants.AVM_MEMORY_SIZE) = 0;
271+
start * (mem_size - constants.AVM_MEMORY_SIZE) = 0;
281272

282273
pol commit src_reads_exceed_mem; // @boolean (by lookup into gt) — clamping flag
283274

284275
pol commit read_addr_upper_bound; // the upper bound of the address that is accessed
285-
read_addr_upper_bound = sel_start * (src_addr + READ_INDEX_UPPER_BOUND);
276+
read_addr_upper_bound = start * (src_addr + READ_INDEX_UPPER_BOUND);
286277
// Preconditions to `gt` gadget require both inputs to be bounded by 2^128.
287278
// `read_addr_upper_bound` = src_addr + read_index_upper_bound (former is U32, latter is < 2^33, so < 2^34).
288279
// `mem_size` = AVM_MEMORY_SIZE = 2^32.
289280
// Note that for a top-level call, src_addr == 0 (enforced in context.pil (#[CD_ADDR_ENQUEUED_CALL_IS_ZERO]))
290281
// and src_reads_exceed_mem == 0.
291282
#[CHECK_SRC_ADDR_IN_RANGE]
292-
sel_start { read_addr_upper_bound, mem_size, src_reads_exceed_mem }
283+
start { read_addr_upper_bound, mem_size, src_reads_exceed_mem }
293284
in
294285
gt.sel_others { gt.input_a, gt.input_b, gt.res };
295286

@@ -305,7 +296,7 @@ namespace data_copy;
305296
// Used to compute reads_left = max(0, clamped - offset), which determines how many rows
306297
// are real memory/column reads vs. zero-padded writes.
307298
pol commit clamped_read_index_upper_bound;
308-
clamped_read_index_upper_bound = sel_start * (READ_INDEX_UPPER_BOUND * (1 - src_reads_exceed_mem) + (mem_size - src_addr) * src_reads_exceed_mem);
299+
clamped_read_index_upper_bound = start * (READ_INDEX_UPPER_BOUND * (1 - src_reads_exceed_mem) + (mem_size - src_addr) * src_reads_exceed_mem);
309300

310301
//////////////////////////////
311302
// Error Handling
@@ -315,40 +306,40 @@ namespace data_copy;
315306
pol commit dst_out_of_range_err; // @boolean (by lookup into gt)
316307

317308
pol commit write_addr_upper_bound;
318-
write_addr_upper_bound = sel_start * (dst_addr + copy_size);
309+
write_addr_upper_bound = start * (dst_addr + copy_size);
319310
// Preconditions to `gt` gadget require both inputs to be bounded by 2^128.
320311
// `write_addr_upper_bound` = dst_addr + copy_size (both U32, so < 2^33).
321312
// `mem_size` = AVM_MEMORY_SIZE = 2^32.
322313
#[CHECK_DST_ADDR_IN_RANGE]
323-
sel_start { write_addr_upper_bound, mem_size, dst_out_of_range_err }
314+
start { write_addr_upper_bound, mem_size, dst_out_of_range_err }
324315
in
325316
gt.sel_others { gt.input_a, gt.input_b, gt.res };
326317

327318
//////////////////////////////
328319
// Control flow management
329320
//////////////////////////////
330-
pol commit sel_start_no_err; // @boolean (by definition)
331-
sel_start_no_err = sel_start * (1 - dst_out_of_range_err);
321+
pol commit start_no_err; // @boolean (by definition)
322+
start_no_err = start * (1 - dst_out_of_range_err);
332323

333324
pol commit sel_write_count_is_zero; // @boolean
334325
sel_write_count_is_zero * (1 - sel_write_count_is_zero) = 0;
335326
pol commit write_count_zero_inv;
336-
// sel_write_count_is_zero = 1 IFF copy_size = 0 (conditioned by sel_start = 1 and there are no errors)
327+
// sel_write_count_is_zero = 1 IFF copy_size = 0 (conditioned by start = 1 and there are no errors)
337328
#[ZERO_SIZED_WRITE]
338-
sel_start_no_err * (copy_size * (sel_write_count_is_zero * (1 - write_count_zero_inv) + write_count_zero_inv) - 1 + sel_write_count_is_zero) = 0;
329+
start_no_err * (copy_size * (sel_write_count_is_zero * (1 - write_count_zero_inv) + write_count_zero_inv) - 1 + sel_write_count_is_zero) = 0;
339330
#[END_IF_WRITE_IS_ZERO]
340-
sel_start_no_err * sel_write_count_is_zero * (sel_end - 1) = 0;
331+
start_no_err * sel_write_count_is_zero * (end - 1) = 0;
341332

342-
pol SEL_PERFORM_COPY = sel_start_no_err * (1 - sel_write_count_is_zero) + sel * (1 - sel_start);
333+
pol SEL_PERFORM_COPY = start_no_err * (1 - sel_write_count_is_zero) + sel * (1 - start);
343334

344335
pol WRITE_COUNT_MINUS_ONE = copy_size - 1;
345336
pol commit write_count_minus_one_inv;
346-
// sel_end = 1 IFF copy_size - 1 = 0;
337+
// end = 1 IFF copy_size - 1 = 0;
347338
#[END_WRITE_CONDITION]
348-
SEL_PERFORM_COPY * (WRITE_COUNT_MINUS_ONE * (sel_end * (1 - write_count_minus_one_inv) + write_count_minus_one_inv) - 1 + sel_end) = 0;
339+
SEL_PERFORM_COPY * (WRITE_COUNT_MINUS_ONE * (end * (1 - write_count_minus_one_inv) + write_count_minus_one_inv) - 1 + end) = 0;
349340

350-
#[END_ON_ERR] // sel_end = 1 if error
351-
sel_start * dst_out_of_range_err * (sel_end - 1) = 0;
341+
#[END_ON_ERR] // end = 1 if error
342+
start * dst_out_of_range_err * (end - 1) = 0;
352343

353344
pol commit reads_left; // Number of reads of the src data, if reads_left = 0 but copy_size != 0 then it is a padding row
354345
// src data elements are read from indices [offset, clamped_read_index_upper_bound), therefore reads_left = clamped_read_index_upper_bound - offset
@@ -358,14 +349,14 @@ namespace data_copy;
358349
// Preconditions to `gt` gadget require both inputs to be bounded by 2^128.
359350
// `clamped_read_index_upper_bound` is at most `src_data_size` which is U32. `offset` is U32.
360351
#[SEL_HAS_READS]
361-
sel_start_no_err { clamped_read_index_upper_bound, offset, sel_has_reads }
352+
start_no_err { clamped_read_index_upper_bound, offset, sel_has_reads }
362353
in
363354
gt.sel_others { gt.input_a, gt.input_b, gt.res };
364355

365356
// If sel_has_reads = 0 (i.e. when offset >= clamped_read_index_upper_bound), reads_left = 0
366357
// otherwise, reads_left = clamped_read_index_upper_bound - offset
367358
#[INIT_READS_LEFT]
368-
sel_start_no_err * (1 - sel_write_count_is_zero) * (reads_left - (clamped_read_index_upper_bound - offset) * sel_has_reads) = 0;
359+
start_no_err * (1 - sel_write_count_is_zero) * (reads_left - (clamped_read_index_upper_bound - offset) * sel_has_reads) = 0;
369360

370361
//////////////////////////////
371362
// Execute Data Copy
@@ -377,11 +368,11 @@ namespace data_copy;
377368

378369
// Data copy size decrements for each row until we end
379370
#[DECR_COPY_SIZE]
380-
sel * (1 - sel_end) * (copy_size' - copy_size + 1) = 0;
371+
sel * (1 - end) * (copy_size' - copy_size + 1) = 0;
381372

382373
// Write address decrements for each row until we end
383374
#[INCR_WRITE_ADDR]
384-
sel * (1 - sel_end) * (dst_addr' - dst_addr - 1) = 0;
375+
sel * (1 - end) * (dst_addr' - dst_addr - 1) = 0;
385376

386377
// Propagate the context ids, clk, and sel_cd_copy
387378
#[SRC_CONTEXT_ID_PROPAGATION]
@@ -401,14 +392,14 @@ namespace data_copy;
401392
// ===== Reading for nested call =====
402393
pol commit read_addr; // The addr to start reading the data from: src_addr + offset;
403394
#[INIT_READ_ADDR] // Only occurs at the start if we have not errored
404-
sel_start_no_err * (1 - sel_write_count_is_zero) * (read_addr - src_addr - offset) = 0;
395+
start_no_err * (1 - sel_write_count_is_zero) * (read_addr - src_addr - offset) = 0;
405396
// Subsequent read addrs are incremented by 1 unless this is a padding row
406397
#[INCR_READ_ADDR]
407-
sel * (1 - padding) * (1 - sel_end) * (read_addr' - read_addr - 1) = 0;
398+
sel * (1 - padding) * (1 - end) * (read_addr' - read_addr - 1) = 0;
408399

409400
// Read count decrements
410401
#[DECR_READ_COUNT]
411-
sel * (1 - padding) * (1 - sel_end) * (reads_left' - reads_left + 1) = 0;
402+
sel * (1 - padding) * (1 - end) * (reads_left' - reads_left + 1) = 0;
412403
pol commit padding; // @boolean If we write, padding = 1 iff reads_left = 0
413404
padding * (1 - padding) = 0;
414405
pol commit reads_left_inv; //@zero-check
@@ -418,7 +409,7 @@ namespace data_copy;
418409

419410
// Once we enter into padding region, we do not get out of it until the end.
420411
#[PADDING_PROPAGATION]
421-
(1 - sel_end) * padding * (1 - padding') = 0;
412+
(1 - end) * padding * (1 - padding') = 0;
422413

423414
// Top level condition:
424415
// is_top_level == 1 if this is an enqueued call, i.e., iff parent_id == 0

0 commit comments

Comments
 (0)