Skip to content

fix(avm)!: add std multi-row computation constraint #21718

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
IlyasRidhuan merged 2 commits into from
Mar 20, 2026
Merged

fix(avm)!: add std multi-row computation constraint #21718

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
ab9dcba
fix(avm)!: add std multi-row computation constraint
IlyasRidhuan Mar 18, 2026
9f2704c
potentially redundant constraint
IlyasRidhuan Mar 19, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
67 changes: 31 additions & 36 deletions barretenberg/cpp/pil/vm2/keccak_memory.pil
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -55,7 +55,7 @@ namespace keccak_memory;
//#################################################################################################
// High-Level Trace Structure Columns
//#################################################################################################
// ctr ctr_end sel start_read last rw addr tag val_0_ val_1_ val_2_ .... val_24_ single_tag_error tag_error
// ctr ctr_end sel start_read end rw addr tag val_0_ val_1_ val_2_ .... val_24_ single_tag_error tag_error
// 1 0 1 1 0 0 38 U64 43 267 17 238 0 0
// 2 0 1 0 0 0 39 U64 267 17 238 0 0
// 3 0 1 0 0 0 40 U64 17 0 0
Expand All @@ -70,17 +70,17 @@ namespace keccak_memory;
// Each column value val_k_ is shifted to the right going bottom-up and finally is laid out
// horizontally in the first row.
// For a read operation, single_tag_error is toggled whenever tag is not U64.
// When this happens, we toggle `last` and stop the multi-rows computation prematurely.
// When this happens, we toggle `end` and stop the multi-rows computation prematurely.
// Therefore, when a tag error occurs the trace looks like:

// ctr ctr_end sel start_read last rw addr tag val_0_ val_1_ val_2_ .... val_24_ single_tag_error tag_error
// ctr ctr_end sel start_read end rw addr tag val_0_ val_1_ val_2_ .... val_24_ single_tag_error tag_error
// 1 0 1 1 0 0 38 U64 43 267 17 0 0 1
// 2 0 1 0 0 0 39 U64 267 17 0 1
// 3 0 1 0 1 0 40 FF 17 0 0 .... 0 1 1

// The selector `last` is defined to be `ctr_end` OR `single_tag_error`.
// The selector `end` is defined to be `ctr_end` OR `single_tag_error`.
// To propagate the single_tag_error value, we use the column `tag_error`.
// Note that we need a separate column because `single_tag_error` defines `last` which
// Note that we need a separate column because `single_tag_error` defines `end` which
// controls when the computation or propagation stops.

pol commit sel; // @boolean
Expand All @@ -90,11 +90,22 @@ sel * (1 - sel) = 0;
#[skippable_if]
sel = 0;

// Weaker than the standard recipe: only prevents 0->1 transitions (not 1->0 mid-block).
// However, this is safe because a truncated block (sel dropping to 0 early) cannot produce a valid
// write: #[WRITE_TO_SLICE] is a permutation requiring round == 24 on a row with sel == 1.
// ==== MULTI-ROW COMPUTATION SELECTORS ====
// See recipe: https://github.com/AztecProtocol/aztec-packages/blob/next/barretenberg/cpp/pil/vm2/docs/recipes.md#contiguous-multi-rows-computation-trace

pol LATCH_CONDITION = end + precomputed.first_row;

// If start_read, start_write, or end is active, sel must be active.
#[SEL_ON_START_OR_END]
(start_read + start_write + end) * (1 - sel) = 0;

// sel is continuous within a computation block: it cannot change except at a latch.
#[TRACE_CONTINUITY]
(1 - precomputed.first_row) * (1 - sel) * sel' = 0;
(1 - LATCH_CONDITION) * (sel - sel') = 0;

// A new computation block must start immediately after a latch.
#[START_AFTER_LATCH]
sel' * (start_read' + start_write' - LATCH_CONDITION) = 0;

pol commit start_read; // @boolean
start_read * (1 - start_read) = 0;
Expand All @@ -115,19 +126,13 @@ pol commit val[25];
// We enforce the initial ctr to be set to 1.
#[CTR_INIT]
(start_read + start_write) * (ctr - 1) = 0;
// It follows that: `start_read == 1 ==> sel == 1` and `start_write == 1 ==> sel == 1`.

#[RW_READ_INIT]
start_read * rw = 0;
#[RW_WRITE_INIT]
start_write * (1 - rw) = 0;
// It follows that `start_read` and `start_write` are mutually exclusive.

// sel == 1 <==> ctr != 0
pol commit ctr_inv;
#[SEL_CTR_NON_ZERO]
ctr * ((1 - sel) * (1 - ctr_inv) + ctr_inv) - sel = 0;

// ctr_end is toggled when all slice rows have been processed.
pol commit ctr_end; // @boolean
ctr_end * (1 - ctr_end) = 0;
Expand All @@ -137,22 +142,13 @@ pol commit state_size_min_ctr_inv;
#[CTR_END]
sel * ((constants.AVM_KECCAKF1600_STATE_SIZE - ctr) * (ctr_end * (1 - state_size_min_ctr_inv) + state_size_min_ctr_inv) + ctr_end - 1) = 0;

// Last ctr of a multi-rows processing of a slice
pol commit last; // @boolean (by definition)

// last == ctr_end || single_tag_error
// `last` is boolean by definition
#[LAST]
last = 1 - (1 - ctr_end) * (1 - single_tag_error);

#[LAST_HAS_SEL_ON]
last * (1 - sel) = 0;
// End of a multi-rows processing of a slice
pol commit end; // @boolean (by definition)

// Latch condition is boolean because `last` cannot be activated at first row due to #[LAST_HAS_SEL_ON].
pol LATCH_CONDITION = last + precomputed.first_row;

#[START_AFTER_LATCH]
sel' * (start_read' + start_write' - LATCH_CONDITION) = 0;
// end == ctr_end || single_tag_error
// `end` is boolean by definition
#[END]
end = 1 - (1 - ctr_end) * (1 - single_tag_error);

#[CTR_INCREMENT]
// Note: sel factor is required for an empty row to satisfy this relation
Expand All @@ -169,7 +165,7 @@ single_tag_error * (1 - single_tag_error) = 0;
rw * single_tag_error = 0;

#[TAG_ERROR_INIT]
last * (tag_error - single_tag_error) = 0;
end * (tag_error - single_tag_error) = 0;

#[TAG_ERROR_PROPAGATION]
(1 - LATCH_CONDITION) * (tag_error - tag_error') = 0;
Expand Down Expand Up @@ -248,13 +244,12 @@ val[24] = (1 - LATCH_CONDITION) * val[23]';
sel { clk, space_id, addr, val[0], tag, rw }
is memory.sel_keccak { memory.clk, memory.space_id, memory.address, memory.value, memory.tag, memory.rw };

// Used to constrain the number of rounds in keccakf1600.pil through the slice_write lookup.
pol commit num_rounds;
sel * (num_rounds - constants.AVM_KECCAKF1600_NUM_ROUNDS) = 0; // Lookup constant support: Can be removed when we support constants in lookups.

/* Prevention of illegal memory operations:
*
* If `sel == 1` (required to trigger a memory operation) we have `ctr != 0` by #[SEL_CTR_NON_ZERO].
* If `sel == 1` (required to trigger a memory operation), the multi-row constraints guarantee this row is part of
* a legitimate computation block starting with `start_read == 1` or `start_write == 1`.
* By #[CTR_INIT], `ctr == 1` on that starting row, and #[CTR_INCREMENT] increments ctr by 1 each row.
* We consider two cases for the previous row above:
* 1) LATCH_CONDITION == 1: By #[START_AFTER_LATCH] we have `start_read == 1` or `start_write == 1` which implies that
* `ctr == 1` which is legitimate.
Expand All @@ -266,7 +261,7 @@ sel * (num_rounds - constants.AVM_KECCAKF1600_NUM_ROUNDS) = 0; // Lookup constan
* `ctr == 1`. This shows that this is a legitimate memory operation.
* Note that if we were to start with a counter larger than AVM_KECCAKF1600_STATE_SIZE, then
* in a bottom-up propagation, we would reach a row with `ctr == AVM_KECCAKF1600_STATE_SIZE`
* and `last` and `LATCH_CONDITION` equal to 1. However, this would contradict that on the
* and `end` and `LATCH_CONDITION` equal to 1. However, this would contradict that on the
* row below `ctr == AVM_KECCAKF1600_STATE_SIZE + 1` and `start_read == 1` or `start_write == 1`.
* Namely, #[CTR_INIT] enforces `ctr == 1`.
*/
94 changes: 43 additions & 51 deletions barretenberg/cpp/pil/vm2/keccakf1600.pil
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -57,7 +57,7 @@ namespace keccakf1600;
//#################################################################################################
// High-Level Trace Structure Columns
//#################################################################################################
// ctr sel start last state_in_00 state_in_01 ....
// ctr sel start end state_in_00 state_in_01 ....
// 1 1 1 0
// 2 1 0 0 ROUND FUNCTION SPECIFICS
// 3 1 0 0
Expand All @@ -76,11 +76,31 @@ sel * (1 - sel) = 0;
#[skippable_if]
sel = 0;

// Weaker than the standard recipe: only prevents 0->1 transitions (not 1->0 mid-block).
// However, this is safe because a truncated block (sel dropping to 0 early) cannot produce a valid
// write: #[WRITE_TO_SLICE] is a permutation requiring round == 24 on a row with sel == 1.
// ==== MULTI-ROW COMPUTATION SELECTORS ====
// See recipe: https://github.com/AztecProtocol/aztec-packages/blob/next/barretenberg/cpp/pil/vm2/docs/recipes.md#contiguous-multi-rows-computation-trace

// First round of a keccak permutation. This is where the multi-rows computation starts and selector start
// is used by the caller to trigger the keccak permutation computation.
pol commit start; // @boolean
start * (1 - start) = 0;

// Selector for the last round of a keccak permutation
pol commit end; // @boolean
end * (1 - end) = 0;

pol LATCH_CONDITION = end + precomputed.first_row;

// If start or end is active, sel must be active.
#[SEL_ON_START_OR_END]
(start + end) * (1 - sel) = 0;

// sel is continuous within a computation block: it cannot change except at a latch.
#[TRACE_CONTINUITY]
(1 - precomputed.first_row) * (1 - sel) * sel' = 0;
(1 - LATCH_CONDITION) * (sel - sel') = 0;

// A new computation block must start immediately after a latch.
#[START_AFTER_LATCH]
sel' * (start' - LATCH_CONDITION) = 0;

// error is defined below after round function
pol commit sel_no_error; // @boolean (by definition)
Expand All @@ -90,42 +110,13 @@ sel * (sel_no_error - 1 + error) = 0;
// Round number which starts at 1 and ends at AVM_KECCAKF1600_NUM_ROUNDS (24).
pol commit round;

// First round of a keccak permutation. This is where the multi-rows computation starts and selector start
// is used by the caller to trigger the keccak permutation computation.
pol commit start; // @boolean
start * (1 - start) = 0;

// We enforce the initial round to be set to 1.
start * (round - 1) = 0;

// sel == 1 <==> round != 0
pol commit round_inv;
#[KECCAK_SEL_ROUND_NON_ZERO]
round * ((1 - sel) * (1 - round_inv) + round_inv) - sel = 0;
// This implies that `start == 1 ==> sel == 1`.

// Selector for the last round of a keccak permutation
// If no error is detected in row where `start == 1`, we have last == 1 <==> round == AVM_KECCAKF1600_NUM_ROUNDS (24)
// This is achieved through #[SEL_SLICE_WRITE] and #[WRITE_TO_SLICE]. If there is no error,
// the former guarantees that the write slice is active whenever `last == 1`. The latter guarantees
// that `round` is equal to 24 (by fixing a constant 24 in the destination permutation tuple).
pol commit last; // @boolean
last * (1 - last) = 0;

// We enforce that `last == 1` whenever `error == 1`.
// We enforce that `end == 1` whenever `error == 1`.
// Note that error is constrained only on the start row.
#[LAST_ON_ERROR]
error * (last - 1) = 0;

#[START_AFTER_LATCH]
sel' * (start' - LATCH_CONDITION) = 0;

#[LAST_HAS_SEL_ON]
last * (1 - sel) = 0;

// `sel == 0` on the first row because of shift relations and thus `last` is mutually
// exclusive with `precomputed.first_row`.
pol LATCH_CONDITION = last + precomputed.first_row;
#[END_ON_ERROR]
error * (end - 1) = 0;

#[KECCAK_ROUND_INCREMENT]
// Note: sel factor is required for an empty row to satisfy this relation
Expand Down Expand Up @@ -1302,7 +1293,7 @@ bitwise.start_keccak { bitwise.op_id, bitwise.acc_ia, bitwise.acc_ib, bitwise.ac
//#############################################################################
// Next state Inputs OR Outputs
//#############################################################################
// If last == 1, state_iota_00 and state_chi_ij's for (i,j) != (0,0) are
// If end == 1, state_iota_00 and state_chi_ij's for (i,j) != (0,0) are
// the output state, otherwise we set the next state_in values for the next round with the current state

#[NEXT_STATE_IN_00]
Expand Down Expand Up @@ -1409,7 +1400,7 @@ error = 1 - (1 - src_out_of_range_error) * (1 - dst_out_of_range_error) * (1 - t
#[SPACE_ID_PROPAGATION]
(1 - LATCH_CONDITION) * (space_id' - space_id) = 0;

// It is crucial to propagate sel_no_error to the bottom (last == 1) as to properly
// It is crucial to propagate sel_no_error to the bottom (end == 1) as to properly
// activate the slice write lookup (see below).
#[SEL_NO_ERROR_PROPAGATION]
(1 - LATCH_CONDITION) * (sel_no_error' - sel_no_error) = 0;
Expand All @@ -1427,22 +1418,22 @@ pol commit sel_slice_write;
#[SEL_SLICE_READ]
sel_slice_read = start * (1 - src_out_of_range_error) * (1 - dst_out_of_range_error);
#[SEL_SLICE_WRITE]
sel_slice_write = sel_no_error * last;
sel_slice_write = sel_no_error * end;

// Prevention of illegitimate writes to memory:
// sel_slice_write == 1 ==> round == 24 (by #[WRITE_TO_SLICE])
// From #[KECCAK_SEL_ROUND_NON_ZERO], we have `sel == 1`.
// Since `last` is a boolean and `sel_no_error` is boolean on an active row,
// `last == 1` and `sel_no_error == 1`.
// sel_slice_write == 1 ==> round == 24 (by #[ROUND_COUNT_AT_WRITE])
// Since sel_slice_write = sel_no_error * end, we have `end == 1` and `sel_no_error == 1`.
// From #[SEL_ON_START_OR_END], `end == 1` implies `sel == 1`.
// This row must have `start == 0` because otherwise `round` would be equal to 1 instead of 24.
// As a consequence, the previous row must have `LATCH_CONDITION == 0` by #[START_AFTER_LATCH]
// which enforces a bottom-up propagation of `sel_no_error` and a decreasing counter for `round`
// by #[SEL_NO_ERROR_PROPAGATION] and #[KECCAK_ROUND_INCREMENT]. When the propagation reaches
// `round == 1`, we have `sel == 1` (#[KECCAK_SEL_ROUND_NON_ZERO]) two possible cases:
// `round == 1`, we have two possible cases:
// 1) The row above is `precomputed.first_row == 1` which implies that `start == 1`.
// 2) Otherwise, by #[TRACE_CONTINUITY], the above row must be active (sel == 1)
// and we cannot decrement `round` anymore (would be zero which contradicts #[KECCAK_SEL_ROUND_NON_ZERO]).
// As a consequence, the above row must have `last == LATCH_CONDITION == 1` which implies that `start == 1`.
// and we cannot decrement `round` anymore (would be zero, contradicting `start * (round - 1) = 0`
// and #[KECCAK_ROUND_INCREMENT]). As a consequence, the above row must have
// `end == LATCH_CONDITION == 1` which implies that `start == 1` on the current row.
// This shows that any "slice write to memory" operation was triggered by a legitimate keccak permutation
// because `start` is the destination selector for the keccak permutation.

Expand All @@ -1464,8 +1455,9 @@ keccak_memory.start_read { keccak_memory.val[0], keccak_memory.val[1], keccak_me
keccak_memory.clk, keccak_memory.addr, keccak_memory.space_id, keccak_memory.tag_error };


// Warning: This lookup also plays a role in constraining the correct number of rounds.
// Therefore, removing it will leave the number of rounds unconstrained.
#[ROUND_COUNT_AT_WRITE]
sel_slice_write * (round - constants.AVM_KECCAKF1600_NUM_ROUNDS) = 0;

// Lookup constant support: Can be replaced with keccak_memory.num_rounds when we support constants in lookups.
#[WRITE_TO_SLICE]
// Standard Keccak layout: memory[(y * 5) + x] = A[x][y]
Expand All @@ -1475,11 +1467,11 @@ sel_slice_write { state_iota_00, state_chi_10, state_chi_20, state_chi_30, state
state_chi_02, state_chi_12, state_chi_22, state_chi_32, state_chi_42,
state_chi_03, state_chi_13, state_chi_23, state_chi_33, state_chi_43,
state_chi_04, state_chi_14, state_chi_24, state_chi_34, state_chi_44,
clk, dst_addr, space_id, round }
clk, dst_addr, space_id }
is // Crucial to be a permutation to prevent any illegal write to memory in keccak_memory.pil.
keccak_memory.start_write { keccak_memory.val[0], keccak_memory.val[1], keccak_memory.val[2], keccak_memory.val[3], keccak_memory.val[4],
keccak_memory.val[5], keccak_memory.val[6], keccak_memory.val[7], keccak_memory.val[8], keccak_memory.val[9],
keccak_memory.val[10], keccak_memory.val[11], keccak_memory.val[12], keccak_memory.val[13], keccak_memory.val[14],
keccak_memory.val[15], keccak_memory.val[16], keccak_memory.val[17], keccak_memory.val[18], keccak_memory.val[19],
keccak_memory.val[20], keccak_memory.val[21], keccak_memory.val[22], keccak_memory.val[23], keccak_memory.val[24],
keccak_memory.clk, keccak_memory.addr, keccak_memory.space_id, keccak_memory.num_rounds };
keccak_memory.clk, keccak_memory.addr, keccak_memory.space_id };
Loading
Loading