Skip to content

Commit 66f1c87

Browse files
authored
docs(avm): Comments in pil file related to range checks of addresses (#6837)
1 parent 7306176 commit 66f1c87

File tree

1 file changed

+13
-4
lines changed

1 file changed

+13
-4
lines changed

barretenberg/cpp/pil/avm/avm_main.pil

Lines changed: 13 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -306,10 +306,19 @@ namespace avm_main(256);
306306
ind_op_c * (1 - ind_op_c) = 0;
307307
ind_op_d * (1 - ind_op_d) = 0;
308308

309-
// TODO - Constraints:
310-
// - mem_idx_a, mem_idx_b, mem_idx_c, mem_idx_d to u32 type
311-
// - ind_a, ind_b, ind_c, ind_d to u32 type
312-
// - 0 <= r_in_tag, w_in_tag <= 6 // Maybe not needed as probably derived by the operation decomposition.
309+
// TODO - Potential constraints to be implemented:
310+
// - mem_idx_a, mem_idx_b, mem_idx_c, mem_idx_d to u32 type:
311+
// - For direct memory accesses, this should be enforced by bytecode validation
312+
// and instruction decomposition. Namely, in this case, only 32-bit immediate
313+
// values should be written into these memory indices.
314+
// - For indirect memory accesses, the memory trace constraints ensure that
315+
// loaded values come from memory addresses with tag u32. This is enforced in the memory trace
316+
// where each memory entry with flag ind_op_x (for x = a,b,c,d) constrains r_int_tag == 3 (u32).
317+
//
318+
// - ind_a, ind_b, ind_c, ind_d to u32 type: Should be guaranteed by bytecode validation and
319+
// instruction decomposition as only immediate 32-bit values should be written into the indirect registers.
320+
//
321+
// - 0 <= r_in_tag, w_in_tag <= 6 // This should be constrained by the operation decomposition.
313322

314323
//====== COMPARATOR OPCODES CONSTRAINTS =====================================
315324
// Enforce that the tag for the ouput of EQ opcode is u8 (i.e. equal to 1).

0 commit comments

Comments
 (0)