Skip to content

Commit 9b3753f

Browse files
MirandaWoodMirandaWood
committed
feat: reduce avm max registers to 4
1 parent 0eec5d9 commit 9b3753f

27 files changed

Lines changed: 475 additions & 687 deletions

File tree

‎barretenberg/cpp/pil/vm2/execution.pil‎

Lines changed: 8 additions & 27 deletions
Original file line numberDiff line numberDiff line change
@@ -462,29 +462,21 @@ sel_instruction_fetching_success {
462462
sel_mem_op_reg[1],
463463
sel_mem_op_reg[2],
464464
sel_mem_op_reg[3],
465-
sel_mem_op_reg[4], // TODO(MW): Remove when reducing max registers
466-
sel_mem_op_reg[5],
467465
// read / write per register
468466
rw_reg[0],
469467
rw_reg[1],
470468
rw_reg[2],
471469
rw_reg[3],
472-
rw_reg[4],
473-
rw_reg[5],
474470
// whether we should perform a tag check on the register
475471
sel_tag_check_reg[0],
476472
sel_tag_check_reg[1],
477473
sel_tag_check_reg[2],
478474
sel_tag_check_reg[3],
479-
sel_tag_check_reg[4],
480-
sel_tag_check_reg[5],
481475
// expected register tag to perform the check against
482476
expected_tag_reg[0],
483477
expected_tag_reg[1],
484478
expected_tag_reg[2],
485-
expected_tag_reg[3],
486-
expected_tag_reg[4],
487-
expected_tag_reg[5]
479+
expected_tag_reg[3]
488480
} in
489481
precomputed.sel_exec_spec {
490482
// execution opcode
@@ -509,29 +501,21 @@ precomputed.sel_exec_spec {
509501
precomputed.sel_mem_op_reg[1],
510502
precomputed.sel_mem_op_reg[2],
511503
precomputed.sel_mem_op_reg[3],
512-
precomputed.sel_mem_op_reg[4],
513-
precomputed.sel_mem_op_reg[5],
514504
// read / write per register
515505
precomputed.rw_reg[0],
516506
precomputed.rw_reg[1],
517507
precomputed.rw_reg[2],
518508
precomputed.rw_reg[3],
519-
precomputed.rw_reg[4],
520-
precomputed.rw_reg[5],
521509
// whether we should perform a tag check on the register
522510
precomputed.sel_tag_check_reg[0],
523511
precomputed.sel_tag_check_reg[1],
524512
precomputed.sel_tag_check_reg[2],
525513
precomputed.sel_tag_check_reg[3],
526-
precomputed.sel_tag_check_reg[4],
527-
precomputed.sel_tag_check_reg[5],
528514
// expected register tag to perform the check against
529515
precomputed.expected_tag_reg[0],
530516
precomputed.expected_tag_reg[1],
531517
precomputed.expected_tag_reg[2],
532-
precomputed.expected_tag_reg[3],
533-
precomputed.expected_tag_reg[4],
534-
precomputed.expected_tag_reg[5]
518+
precomputed.expected_tag_reg[3]
535519
};
536520

537521
//////// ADDRESSING ////////
@@ -556,21 +540,18 @@ pol commit sel_read_registers; // @boolean (by definition)
556540
sel_read_registers = SEL_RESOLVE_ADDRESS - sel_addressing_error;
557541

558542
// Registers
559-
pol commit register[6];
560-
561-
// TODO(MW): Remove when reducing max registers (below prevents IsolatedCommittedColumn)
562-
sel_read_registers * register[5] = 0;
543+
pol commit register[4];
563544

564545
// Memory Accesses
565-
pol commit sel_mem_op_reg[6]; // @boolean (when `sel_instruction_fetching_success == 1`)
546+
pol commit sel_mem_op_reg[4]; // @boolean (when `sel_instruction_fetching_success == 1`)
566547
// Read / Write selectors
567-
pol commit rw_reg[6]; // @boolean (when `sel_instruction_fetching_success == 1`)
548+
pol commit rw_reg[4]; // @boolean (when `sel_instruction_fetching_success == 1`)
568549
// Memory Tag
569-
pol commit mem_tag_reg[6];
550+
pol commit mem_tag_reg[4];
570551
// Whether we should perform a tag check on the register
571-
pol commit sel_tag_check_reg[6]; // @boolean (when `sel_instruction_fetching_success == 1`)
552+
pol commit sel_tag_check_reg[4]; // @boolean (when `sel_instruction_fetching_success == 1`)
572553
// Expected tag
573-
pol commit expected_tag_reg[6];
554+
pol commit expected_tag_reg[4];
574555

575556
// NOTE: Constraints on the registers are in execution/registers.pil.
576557
// The "output we want is" sel_register_read_error from execution/registers.pil.

‎barretenberg/cpp/pil/vm2/execution/registers.pil‎

Lines changed: 8 additions & 21 deletions
Original file line numberDiff line numberDiff line change
@@ -6,15 +6,15 @@ namespace execution;
66
// Columns declared in execution.pil (see temporality groups 3 & 6):
77
//
88
// Inputs for read/write (retrieved through #[EXEC_SPEC_READ]):
9-
// pol commit sel_mem_op_reg[6]; // Memory access (register is active)
10-
// pol commit rw_reg[6]; // Read / Write (only if sel_mem_op_reg[i] = 1)
11-
// pol commit sel_tag_check_reg[6]; // Tag check (only for read)
12-
// pol commit expected_tag_reg[6]; // Expected tag (only if sel_tag_check_reg[i] = 1)
9+
// pol commit sel_mem_op_reg[4]; // Memory access (register is active)
10+
// pol commit rw_reg[4]; // Read / Write (only if sel_mem_op_reg[i] = 1)
11+
// pol commit sel_tag_check_reg[4]; // Tag check (only for read)
12+
// pol commit expected_tag_reg[4]; // Expected tag (only if sel_tag_check_reg[i] = 1)
1313
// pol commit rop[5]; // Resolved operands (for read/write), always addresses here.
1414
//
1515
// Inputs for write, Outputs for read:
16-
// pol commit register[6];
17-
// pol commit mem_tag_reg[6];
16+
// pol commit register[4];
17+
// pol commit mem_tag_reg[4];
1818
//
1919
// Execution.pil temporality group selectors:
2020
// pol commit sel_read_registers; // Register read
@@ -45,7 +45,7 @@ sel_read_registers = 0;
4545
// (b) sel_mem_op_reg[i] is a write and we got to the write temporality group.
4646
// Note that sel_mem_op_reg[i] and rw_reg[i] are defined (constrained) because
4747
// they are retrieved through #[EXEC_SPEC_READ] from temporality group 2 (which happens earlier).
48-
pol commit sel_op_reg_effective[6]; // @boolean (by definition)
48+
pol commit sel_op_reg_effective[4]; // @boolean (by definition)
4949
#[SEL_OP_REG_EFFECTIVE_0]
5050
sel_op_reg_effective[0] = sel_mem_op_reg[0] * (sel_read_registers * (1 - rw_reg[0]) + sel_write_registers * rw_reg[0]);
5151
#[SEL_OP_REG_EFFECTIVE_1]
@@ -54,10 +54,6 @@ sel_op_reg_effective[1] = sel_mem_op_reg[1] * (sel_read_registers * (1 - rw_reg[
5454
sel_op_reg_effective[2] = sel_mem_op_reg[2] * (sel_read_registers * (1 - rw_reg[2]) + sel_write_registers * rw_reg[2]);
5555
#[SEL_OP_REG_EFFECTIVE_3]
5656
sel_op_reg_effective[3] = sel_mem_op_reg[3] * (sel_read_registers * (1 - rw_reg[3]) + sel_write_registers * rw_reg[3]);
57-
#[SEL_OP_REG_EFFECTIVE_4]
58-
sel_op_reg_effective[4] = sel_mem_op_reg[4] * (sel_read_registers * (1 - rw_reg[4]) + sel_write_registers * rw_reg[4]);
59-
#[SEL_OP_REG_EFFECTIVE_5]
60-
sel_op_reg_effective[5] = sel_mem_op_reg[5] * (sel_read_registers * (1 - rw_reg[5]) + sel_write_registers * rw_reg[5]);
6157

6258
// Observe that the following permutations span both temporality groups (activated at most once per instruction).
6359
// That's why we have to properly activate them with the above selectors, which take into account
@@ -74,13 +70,6 @@ is memory.sel_register_op[2] { memory.clk, memory.space_id, memory.address, memo
7470
#[MEM_OP_3]
7571
sel_op_reg_effective[3] { clk, context_id, rop[3], register[3], mem_tag_reg[3], rw_reg[3] }
7672
is memory.sel_register_op[3] { memory.clk, memory.space_id, memory.address, memory.value, memory.tag, memory.rw };
77-
#[MEM_OP_4]
78-
sel_op_reg_effective[4] { clk, context_id, rop[4], register[4], mem_tag_reg[4], rw_reg[4] }
79-
is memory.sel_register_op[4] { memory.clk, memory.space_id, memory.address, memory.value, memory.tag, memory.rw };
80-
// TODO(MW): check when reducing max registers
81-
// #[MEM_OP_5]
82-
// sel_op_reg_effective[5] { clk, context_id, rop[5], register[5], mem_tag_reg[5], rw_reg[5] }
83-
// is memory.sel_register_op[5] { memory.clk, memory.space_id, memory.address, memory.value, memory.tag, memory.rw };
8473

8574
// This error is true iff the following "batch" check failed. That is if some tag is not the expected one.
8675
// Observe that we don't need to know exactly which one failed.
@@ -95,9 +84,7 @@ sel_register_read_error * (1 - sel_register_read_error) = 0;
9584
pol BATCHED_TAGS_DIFF_REG = sel_tag_check_reg[0] * 2**0 * (mem_tag_reg[0] - expected_tag_reg[0])
9685
+ sel_tag_check_reg[1] * 2**3 * (mem_tag_reg[1] - expected_tag_reg[1])
9786
+ sel_tag_check_reg[2] * 2**6 * (mem_tag_reg[2] - expected_tag_reg[2])
98-
+ sel_tag_check_reg[3] * 2**9 * (mem_tag_reg[3] - expected_tag_reg[3])
99-
+ sel_tag_check_reg[4] * 2**12 * (mem_tag_reg[4] - expected_tag_reg[4])
100-
+ sel_tag_check_reg[5] * 2**15 * (mem_tag_reg[5] - expected_tag_reg[5]);
87+
+ sel_tag_check_reg[3] * 2**9 * (mem_tag_reg[3] - expected_tag_reg[3]);
10188
pol commit batched_tags_diff_inv_reg;
10289
pol BATCHED_TAGS_DIFF_X_REG = sel_read_registers * BATCHED_TAGS_DIFF_REG; // Forces 0 if we don't read the register.
10390
pol BATCHED_TAGS_DIFF_Y_REG = batched_tags_diff_inv_reg;

‎barretenberg/cpp/pil/vm2/memory.pil‎

Lines changed: 2 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -119,12 +119,11 @@ sel_addressing_indirect[3] * (1 - sel_addressing_indirect[3]) = 0;
119119
sel_addressing_indirect[4] * (1 - sel_addressing_indirect[4]) = 0;
120120

121121
// Permutation selectors (execution/registers.pil)
122-
pol commit sel_register_op[5]; // @boolean
122+
pol commit sel_register_op[4]; // @boolean
123123
sel_register_op[0] * (1 - sel_register_op[0]) = 0;
124124
sel_register_op[1] * (1 - sel_register_op[1]) = 0;
125125
sel_register_op[2] * (1 - sel_register_op[2]) = 0;
126126
sel_register_op[3] * (1 - sel_register_op[3]) = 0;
127-
sel_register_op[4] * (1 - sel_register_op[4]) = 0;
128127

129128
// Permutation selectors (data_copy.pil).
130129
pol commit sel_data_copy_read; // @boolean
@@ -188,7 +187,7 @@ sel = // Addressing.
188187
+ sel_addressing_indirect[0] + sel_addressing_indirect[1] + sel_addressing_indirect[2] + sel_addressing_indirect[3]
189188
+ sel_addressing_indirect[4]
190189
// Registers.
191-
+ sel_register_op[0] + sel_register_op[1] + sel_register_op[2] + sel_register_op[3] + sel_register_op[4]
190+
+ sel_register_op[0] + sel_register_op[1] + sel_register_op[2] + sel_register_op[3]
192191
// Data Copy.
193192
+ sel_data_copy_read
194193
+ sel_data_copy_write

‎barretenberg/cpp/pil/vm2/precomputed.pil‎

Lines changed: 11 additions & 11 deletions
Original file line numberDiff line numberDiff line change
@@ -296,18 +296,18 @@ pol constant p_decomposition_limb;
296296

297297
// ===== Section 9: Execution instruction spec (EXECUTION_INSTRUCTION_SPEC) =====
298298
// Each valid row encodes: gas costs (L2 opcode, base DA, dynamic L2, dynamic DA),
299-
// per-register flags (memory access, read/write, tag check, expected tag) for 6 registers,
299+
// per-register flags (memory access, read/write, tag check, expected tag) for 4 registers,
300300
// subtrace/gadget dispatch IDs, dynamic gas ID, and address-operand flags for 5 operands.
301301
// Used by the execution subtrace to dispatch and constrain instruction behavior.
302302
//
303303
// Example trace (idx encodes the ExecutionOpCode; array columns use [a,b,...] notation):
304304
//
305-
// idx | sel_exec_spec | opcode_gas | base_da | dyn_l2 | dyn_da | mem_op[0..5] | rw[0..5] | subtrace_id | sub_op_id | dyn_gas_id | is_addr[0..4]
306-
// -----------------+---------------+------------+---------+--------+--------+--------------------+--------------------+-------------+-----------+------------+----------------------
307-
// 0 (ADD) | 1 | 12 | 0 | 0 | 0 | [1,1,1,0,0,0] | [0,0,1,0,0,0] | 1 | 1 | 0 | [1,1,1,0,0]
308-
// 1 (SUB) | 1 | 12 | 0 | 0 | 0 | [1,1,1,0,0,0] | [0,0,1,0,0,0] | 1 | 2 | 0 | [1,1,1,0,0]
309-
// ... | ... | ... | ... | ... | ... | ... | ... | ... | ... | ... | ...
310-
// 45 (TORADIXBE) | 1 | 24 | 0 | 3 | 0 | [1,1,1,1,0,0] | [0,0,0,0,0,0] | 13 | 0 | 4 | [1,1,1,1,1]
305+
// idx | sel_exec_spec | opcode_gas | base_da | dyn_l2 | dyn_da | mem_op[0..3] | rw[0..3] | subtrace_id | sub_op_id | dyn_gas_id | is_addr[0..4]
306+
// -----------------+---------------+------------+---------+--------+--------+--------------+-----------+-------------+-----------+------------+--------------
307+
// 0 (ADD) | 1 | 12 | 0 | 0 | 0 | [1,1,1,0] | [0,0,1,0] | 1 | 1 | 0 | [1,1,1,0,0]
308+
// 1 (SUB) | 1 | 12 | 0 | 0 | 0 | [1,1,1,0] | [0,0,1,0] | 1 | 2 | 0 | [1,1,1,0,0]
309+
// ... | ... | ... | ... | ... | ... | ... | ... | ... | ... | ... | ...
310+
// 45 (TORADIXBE) | 1 | 24 | 0 | 3 | 0 | [1,1,1,1] | [0,0,0,0] | 13 | 0 | 4 | [1,1,1,1,1]
311311

312312
pol constant sel_exec_spec;
313313
// Gas Costs
@@ -316,11 +316,11 @@ pol constant exec_opcode_base_da_gas;
316316
pol constant exec_opcode_dynamic_l2_gas;
317317
pol constant exec_opcode_dynamic_da_gas;
318318
// Registers: Memory Access
319-
pol constant sel_mem_op_reg[6];
320-
pol constant rw_reg[6];
319+
pol constant sel_mem_op_reg[4];
320+
pol constant rw_reg[4];
321321
// Registers: Tag Check
322-
pol constant sel_tag_check_reg[6];
323-
pol constant expected_tag_reg[6];
322+
pol constant sel_tag_check_reg[4];
323+
pol constant expected_tag_reg[4];
324324
// Decomposed Subtrace/Gadget Selector
325325
pol constant dyn_gas_id;
326326
pol constant subtrace_id;

‎barretenberg/cpp/src/barretenberg/aztec/aztec_constants.hpp‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -179,14 +179,14 @@
179179
#define AVM_PUBLIC_INPUTS_COLUMN_2_LENGTH 522
180180
#define AVM_PUBLIC_INPUTS_COLUMN_3_LENGTH 99
181181
#define AVM_PUBLIC_INPUTS_COLUMNS_COMBINED_LENGTH 9989
182-
#define AVM_V2_PROOF_LENGTH_IN_FIELDS 15368
182+
#define AVM_V2_PROOF_LENGTH_IN_FIELDS 15280
183183
#define TX_DA_GAS_OVERHEAD 96
184184
#define PUBLIC_TX_L2_GAS_OVERHEAD 540000
185185
#define AVM_MAX_PROCESSABLE_L2_GAS 6000000
186186
#define MAX_PROCESSABLE_L2_GAS 6540000
187187
#define AVM_PC_SIZE_IN_BITS 32
188188
#define AVM_MAX_OPERANDS 5
189-
#define AVM_MAX_REGISTERS 6
189+
#define AVM_MAX_REGISTERS 4
190190
#define AVM_ADDRESSING_BASE_RESOLUTION_L2_GAS 3
191191
#define AVM_ADDRESSING_INDIRECT_L2_GAS 3
192192
#define AVM_ADDRESSING_RELATIVE_L2_GAS 3

‎barretenberg/cpp/src/barretenberg/vm2/constraining/avm_fixed_vk.hpp‎

Lines changed: 1 addition & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -17,7 +17,7 @@ class AvmHardCodedVKAndHash {
1717
using FF = bb::curve::BN254::ScalarField;
1818

1919
// Precomputed VK hash (hash of all commitments below).
20-
static FF vk_hash() { return FF(uint256_t("0x25167d49ed8dc5563599343ed92c9b30c500ad3b4138567130e9eb6a9a278d6b")); }
20+
static FF vk_hash() { return FF(uint256_t("0x15098946f4348339fa379e7afbf954ce083e615002dc0f7ac1706d63a400b42d")); }
2121

2222
static constexpr std::array<Commitment, NUM_PRECOMPUTED_ENTITIES> get_all()
2323
{
@@ -90,8 +90,6 @@ class AvmHardCodedVKAndHash {
9090
uint256_t("0x1a3c36c4933c956751e6ca5631077a9418cd0ba4ec29e965508eaf8bc1a7ffd4"),
9191
uint256_t(
9292
"0x1203bdd1aab5bfc5f3ed6abbefc30ab303770b847d022c1c9c0f8de202a76560")), // precomputed_expected_tag_reg_3_
93-
Commitment::infinity(), // precomputed_expected_tag_reg_4_
94-
Commitment::infinity(), // precomputed_expected_tag_reg_5_
9593
Commitment(
9694
uint256_t("0x0000000000000000000000000000000000000000000000000000000000000001"),
9795
uint256_t(
@@ -227,8 +225,6 @@ class AvmHardCodedVKAndHash {
227225
uint256_t(
228226
"0x176b78b990ea79d06072fb91fd96b2a8472376baf05016f668d2c3162d0a7984")), // precomputed_rw_reg_2_
229227
Commitment::infinity(), // precomputed_rw_reg_3_
230-
Commitment::infinity(), // precomputed_rw_reg_4_
231-
Commitment::infinity(), // precomputed_rw_reg_5_
232228
Commitment(
233229
uint256_t("0x0752e216f6398f2dc16b86cd762f9bd9f961964f9c6a354530c45b04920f06ab"),
234230
uint256_t(
@@ -281,8 +277,6 @@ class AvmHardCodedVKAndHash {
281277
uint256_t("0x1530ccb47d1198320c163380a82ca8cbaf87b2d40ede856d21c60535e2251262"),
282278
uint256_t(
283279
"0x29dd7ccea05e6d47a7373ea950a7988caed0d20880612e046af575217a21652a")), // precomputed_sel_mem_op_reg_3_
284-
Commitment::infinity(), // precomputed_sel_mem_op_reg_4_
285-
Commitment::infinity(), // precomputed_sel_mem_op_reg_5_
286280
Commitment(
287281
uint256_t("0x089cdab4e8e8381977b093cb267a1b7c8c60f4466c39a99af1247e37fe56ebfe"),
288282
uint256_t(
@@ -407,8 +401,6 @@ class AvmHardCodedVKAndHash {
407401
uint256_t("0x1530ccb47d1198320c163380a82ca8cbaf87b2d40ede856d21c60535e2251262"),
408402
uint256_t(
409403
"0x29dd7ccea05e6d47a7373ea950a7988caed0d20880612e046af575217a21652a")), // precomputed_sel_tag_check_reg_3_
410-
Commitment::infinity(), // precomputed_sel_tag_check_reg_4_
411-
Commitment::infinity(), // precomputed_sel_tag_check_reg_5_
412404
Commitment(
413405
uint256_t("0x2b770f46bb0db9c1447e6010b3ca12f1dc2b2a237ff6d2390d9ddf5a056d09ad"),
414406
uint256_t(

‎barretenberg/cpp/src/barretenberg/vm2/constraining/recursion/two_layer_avm_recursive_verifier.hpp‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -23,7 +23,7 @@
2323

2424
namespace bb::avm2 {
2525

26-
static constexpr size_t NUM_AVM_ULTRA_OPS = 3082;
26+
static constexpr size_t NUM_AVM_ULTRA_OPS = 3058;
2727
static_assert(2 * NUM_AVM_ULTRA_OPS < (1 << CONST_TRANSLATOR_MINI_CIRCUIT_LOG_SIZE) - NUM_DISABLED_ROWS_IN_SUMCHECK,
2828
"AVM ultra ops land in the range reserved for randomness in the Translator mini circuit. If this "
2929
"assertion fails, we need to increase CONST_TRANSLATOR_MINI_CIRCUIT_LOG_SIZE.");

‎barretenberg/cpp/src/barretenberg/vm2/constraining/relations/registers.test.cpp‎

Lines changed: 3 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -50,9 +50,7 @@ TEST(RegistersConstrainingTest, EffectiveRegOpSelectorNoReadNoWrite)
5050
registers::SR_SEL_OP_REG_EFFECTIVE_0,
5151
registers::SR_SEL_OP_REG_EFFECTIVE_1,
5252
registers::SR_SEL_OP_REG_EFFECTIVE_2,
53-
registers::SR_SEL_OP_REG_EFFECTIVE_3,
54-
registers::SR_SEL_OP_REG_EFFECTIVE_4,
55-
registers::SR_SEL_OP_REG_EFFECTIVE_5);
53+
registers::SR_SEL_OP_REG_EFFECTIVE_3);
5654

5755
// Mismatch in effective selector should fail.
5856
trace.set(0,
@@ -100,9 +98,7 @@ TEST(RegistersConstrainingTest, EffectiveRegOpSelectorOnlyRead)
10098
registers::SR_SEL_OP_REG_EFFECTIVE_0,
10199
registers::SR_SEL_OP_REG_EFFECTIVE_1,
102100
registers::SR_SEL_OP_REG_EFFECTIVE_2,
103-
registers::SR_SEL_OP_REG_EFFECTIVE_3,
104-
registers::SR_SEL_OP_REG_EFFECTIVE_4,
105-
registers::SR_SEL_OP_REG_EFFECTIVE_5);
101+
registers::SR_SEL_OP_REG_EFFECTIVE_3);
106102

107103
// Mismatch in effective selector should fail.
108104
trace.set(0,
@@ -150,9 +146,7 @@ TEST(RegistersConstrainingTest, EffectiveRegOpSelectorReadThenWrite)
150146
registers::SR_SEL_OP_REG_EFFECTIVE_0,
151147
registers::SR_SEL_OP_REG_EFFECTIVE_1,
152148
registers::SR_SEL_OP_REG_EFFECTIVE_2,
153-
registers::SR_SEL_OP_REG_EFFECTIVE_3,
154-
registers::SR_SEL_OP_REG_EFFECTIVE_4,
155-
registers::SR_SEL_OP_REG_EFFECTIVE_5);
149+
registers::SR_SEL_OP_REG_EFFECTIVE_3);
156150

157151
// Mismatch in effective selector should fail.
158152
trace.set(0,

0 commit comments

Comments
 (0)